Вычислимое число это такое, которое может быть вычислено на компьютере с любой степенью точности.
Это требует уточнения. "Вычислимое число", или
конструктивное действительное число (КДЧ) — это пара алгоритмов, один из которых вычисляет последовательность рациональных чисел (то есть, по заданному натуральному числу
находит некоторое рациональное число
), а другой называется
регулятором сходимости в себе и по заданному натуральному числу
вычисляет такое натуральное число
, что для любых
,
выполняется неравенство
.
Комбинируя эти алгоритмы, мы можем вычислять число КДЧ с любой заданной точностью.
Понятие КДЧ является достаточно жёстким. Существуют различные ослабления этого понятия.
На популярном уровне алгоритм — это пошаговая инструкция, каждый шаг которой выполняется однозначно (при наличии соответствующего исполнителя, естественно). Результат применения алгоритма к исходным данным определяется в момент завершения выполнения инструкции.
Не предполагается, что этот результат должен быть в каком-нибудь смысле полезным, и даже не предполагается, что выполнение инструкции хоть когда-нибудь должно завершиться.
Существует целый ряд формализаций этого понятия: машина Тьюринга, нормальный алгорифм Маркова, частично рекурсивная функция, … Все известные формализации понятия алгоритма являются эквивалентными.
Интересно, что такое направление конструктивизма, как интуиционизм, считает ограничение понятия вычислимости алгоритмами слишком жёстким.
-- Ср фев 03, 2016 12:21:28 --Забавно, что множество алгоритмов, вычисляющих какое-то число, не перечислимо. Следовательно существуют алгоритмы, вычисляющие это число, для которых не возможно доказать, что они это делают.
Уточнение: не существует алгоритма, проверяющего, вычисляется ли заданное число заданным алгоритмом. Насчёт "невозможно доказать" ситуация более тонкая.
Конечно разрешимо, ведь мы выбросим в корзину любой текст не начинающийся со слова "доказательство".
Разумеется, надо ограничиться формальными теориями, удовлетворяющими определённым требованиям.
Во-первых, алфавит теории должен быть конечным.
Во-вторых, синтаксис теории должен быть алгоритмически распознаваемым.
В-третьих, множества аксиом и правил вывода теории должны быть алгоритмически перечислимыми (по-моему, распознаваемости всё-таки не требуется).
Такие формальные теории первого порядка, как арифметика Пеано или теория множеств ZFC этим условиям удовлетворяют.
Понятия "теорема" (обычно употребляются термины "высказывание" или "формула") и "доказательство" являются синтаксическими, поэтому можно построить алгоритм, перечисляющий тексты в заданном алфавите и проверяющий, являются ли эти тексты доказательствами заданной теоремы.
Проблема в следующем: если доказательство теоремы существует, то наш алгоритм "когда-нибудь" его найдёт. Но предположим, что мы его запустили, он проработал уже
лет и всё ещё результата не выдал. Существует доказательство или нет? Неизвестно.