Тезис Чёрча — Тьюринга

Те́зис Чёрча — Тью́ринга — логико-математический принцип, устанавливающий эквивалентность между интуитивным понятием алгоритмической вычислимости и строго формализованными понятиями частично рекурсивной функции и функции, вычислимой на машине Тьюринга. В связи с интуитивностью исходного понятия алгоритмической вычислимости, данный тезис носит характер суждения об этом понятии и его невозможно строго доказать или опровергнутьШаблон:Sfn. Перед точным определением вычислимой функции математики часто использовали неофициальный термин, «эффективно вычислимый» для описания функций, которые можно вычислить с помощью «бумажно-карандашных» методов.

Тезис был высказан Алонзо Чёрчем и Аланом Тьюрингом в середине 1930-х годов<ref>Шаблон:Статья</ref><ref>Шаблон:Статья</ref><ref>Шаблон:Source </ref><ref>Шаблон:Source </ref>. Существенен для многих областей науки и философии науки, в том числе для математической логики, теории доказательств, информатики, кибернетики.

Формулировки

В терминах теории рекурсии, тезис формулируется как точное описание интуитивного понятия вычислимости классом общерекурсивных функций. В этой формулировке часто упоминается как просто тезис ЧёрчаШаблон:Sfn.

Более общая формулировка была дана Стивеном Клини, согласно которой все частичные (то есть не обязательно определённые для всех значений аргументов) функции, вычислимые посредством алгоритмов, являются частично рекурсивнымиШаблон:Sfn.

В терминах вычислимости по Тьюрингу тезис гласит, что для любой алгоритмически вычислимой функции существует вычисляющая её значения машина ТьюрингаШаблон:Sfn. Иногда в такой формулировке фигурирует как тезис Тьюринга. Ввиду того, что классы частично вычислимых по Тьюрингу и частично рекурсивных функций совпадают, утверждение объединяют в единый тезис Чёрча — Тьюринга.

Позднее были сформулированы другие практические варианты утверждения:

• физический тезис Чёрча — Тьюринга: любая функция, которая может быть вычислена физическим устройством, может быть вычислена машиной Тьюринга;
• сильный тезис Чёрча — Тьюринга (тезис Чёрча — Тьюринга — Дойча): любой конечный физический процесс, не использующий аппарат, связанный с непрерывностью и бесконечностью, может быть вычислен физическим устройством.

История

Одной из важных проблем для логиков в 1930-х годах была проблема разрешения: существует ли механическая процедура для отделения математических истин от математических ложностей. Эта задача требовала, чтобы понятие «алгоритм» или «эффективная вычислимость» было закреплено, по крайней мере, чтобы приступить к задаче<ref>Комментарий Девиса к «Черч 1936 An Unsolvable Problem of Elementary Number Theory» в Davis 1965:88. Чёрч использовал слова «эффективная вычисляемость»(«effective calculability») на странице 100ff.</ref> С самого начала и по сей день (по состоянию на 2007 год) продолжаются дебаты:<ref>cf Smith (July 11, 2007) Church’s Thesis after 70 Years at http://www.logicmatters.net/resources/pdfs/CTT.pdf Шаблон:Wayback</ref>. было ли понятие «эффективной вычислимости» (i) «аксиомой или аксиомами» в аксиоматической системе или (ii) просто определением, которое «идентифицировало» два или более предложений или (iii) эмпирической гипотезой, которую следует проверить на естественных событиях или (iv) или просто предложением ради аргумента (то есть «тезиса»).

1930—1952

В ходе изучения проблемы Чёрч и его ученик Стивен Клини ввели понятие λ-определимых функций, и они смогли доказать, что несколько больших классов функций, часто встречающихся в теории чисел, были λ-определимыми<ref>cf footnote 3 in Шаблон:Harvnb An Unsolvable Problem of Elementary Number Theory in Шаблон:Harvcolnb</ref>. Дискуссия началась, когда Чёрч предложил Курту Гёделю определить «эффективно вычислимые» функции как λ-определимые функции. Однако Гёдель не был убеждён и назвал это предложение «полностью неудовлетворительным»<ref>Dawson 1997:99.Шаблон:Full citation needed</ref>. Тем не менее Гёдель в переписке с Чёрчем предложил аксиоматизировать понятие «эффективной вычислимости»; В письме Клини и Чёрчу он сообщил, что

{{#ifexpr: 0 mod 2 = 0 and 0 != 4 and 0 != 104 |

}}{{#if: |

:

}}

{{#ifexpr: 0 mod 2 = 0 and 0 != 4 and 0 != 104 |

}} Его единственная идея в то время состоит в том, что может быть возможно задать термин эффективной вычислимости как неопределённого понятия в виде набора аксиом, которые бы воплощали общепринятые свойства этого понятия и затем что-то делать на этой основе. {{#if: <ref name="sieg160">Sieg 1997:160.</ref>

|

— <ref name="sieg160">Sieg 1997:160.</ref>

}}

Но Гёдель не дал никаких дальнейших указаний. Он предложил только рекурсию, модифицированную предложением Эрбрана, о чём Гёдель подробно написал на своих лекциях в 1934 году в Принстоне Нью-Джерси (Клини и Россер расшифровали записи). Но он не думал, что две идеи могут быть удовлетворительно определены «кроме эвристически»<ref>Sieg 1997:160 цитирует письмо, написанное в 1935 Чёрчем для Клини, cf Footnote 3 in Gödel 1934 in Шаблон:Harvcolnb.</ref>.

Затем необходимо было идентифицировать и доказать эквивалентность двух понятий эффективной вычислимости. Оснащённый λ-исчислением и «общей» рекурсией, Стивен Клини с помощью Чёрча и Россера подготовили доказательства (1933, 1935), чтобы показать, что эти два исчисления эквивалентны. Чёрч впоследствии изменил свои методы, включив использование рекурсии Эрбрана — Гёделя, а затем доказал (1936), что проблема разрешения неразрешима: нет обобщённого алгоритма, который может определить, имеет ли корректно сформулированная формула «нормальную форму»<ref>cf Church 1936 in Шаблон:Harvcolnb</ref>.

Много лет спустя в письме к Дэвису (около 1965 года) Гёдель сказал, что «он был во время этих [1934] лекций, совсем не убеждён в том, что его концепция рекурсии включает все возможные рекурсии»<ref>Davis’s commentary before Gödel 1934 in Шаблон:Harvcolnb</ref>. К 1963 году Гёдель отказался от рекурсии Эрбрана — Гёделя и λ-исчисления в пользу машины Тьюринга как определения «алгоритма» или «механической процедуры» или «формальной системы»<ref>Детальное обсуждение гёделевского использования тьюринговых машин как моделей вычисления см. Шаблон:Cite web</ref>.

В конце 1936 года статья Алана Тьюринга (также доказывающая, что проблема разрешения неразрешима) была озвучена в устной форме, но ещё не появилась в печати<ref name="On Computable">Шаблон:Harvnb</ref>. С другой стороны, появилась статья Эмиля Поста 1936 года и была сертифицирована независимо от работы Тьюринга<ref>cf. Editor’s footnote to Post 1936 Finite Combinatory Process. Formulation I. at Шаблон:Harvcolnb</ref>. Пост категорически не согласился с Чёрчевским «отождествлением» (identification) эффективной вычислимости c λ-исчислением и рекурсией, заявив:

{{#ifexpr: 0 mod 2 = 0 and 0 != 4 and 0 != 104 |

}}{{#if: |

:

}}

{{#ifexpr: 0 mod 2 = 0 and 0 != 4 and 0 != 104 |

}} На самом деле в работе Чёрча и других это отождествление излагается значительно сильнее рабочей гипотезы. Но маскировка этого отождествления под определение … ослепляет нас необходимостью постоянной проверки. {{#if: <ref>Post 1936 in Шаблон:Harvcolnb, footnote 8.</ref>

|

— <ref>Post 1936 in Шаблон:Harvcolnb, footnote 8.</ref>

}}

Скорее, он считал понятие «эффективной вычислимости» просто «рабочей гипотезой», которая могла бы привести индуктивным умозаключением к «естественному закону», а не «определению или аксиоме»<ref>Post 1936 in Davis 1952:291</ref>. Эта идея была «резко» подвергнута критике со стороны Чёрча<ref>Sieg 1997:171 and 176-7</ref>.

Таким образом, Пост в своей статье 1936 года также отклонял предложение Курта Гёделя Чёрчу в 1934—1935 годах о том, что тезис может быть выражен как аксиома или множество аксиом<ref name="sieg160" />.

Тьюринг добавляет ещё одно определение, Россер приравнивает все три : за короткое время появилась статья (1936-37) Тьюринга «О вычислимых числах и применение к проблеме разрешения».<ref name="On Computable"/> В ней он задал понятие «эффективной вычислимости» по-другому, с введением его а-машин (теперь они известны как абстрактная вычислительная модель машины Тьюринга). И в доказательном эскизе, добавленном как «Приложение» к его статье 1936-37, Тьюринг показал, что классы функций, определяемые λ-исчислением и машинами Тьюринга, совпадают<ref>Turing 1936-7 in Шаблон:Harvcolnb</ref>. Чёрч быстро понял, насколько убедительным был анализ Тьюринга. В своем обзоре работы Тьюринга он ясно дал понять, что понятие Тьюринга сделало «отождествление с эффективностью в обычном (не явно определённом) смысле, очевидном сразу»<ref>Шаблон:Harvnb</ref>.

Через несколько лет (1939) Тьюринг предложил, как это сделали Чёрч и Клини перед ним, что его формальное определение механического вычислительного агента было правильным<ref>Turing 1939 in Davis:160</ref>. Таким образом, к 1939 году и Чёрч (1934), и Тьюринг (1939) индивидуально предложили, чтобы их «формальные системы» были определениями «эффективной вычислимости»<ref>cf. Church 1934 in Шаблон:Harvcolnb, also Turing 1939 in Шаблон:Harvcolnb</ref>; а не сформулировали свои утверждения как тезисы.

Россер (1939) формально отождествил три понятия как определения:

«Все три определения эквивалентны, поэтому не имеет значения, какое из них используется».

Клини предлагает тезис Чёрча : здесь оставлено явное выражение «тезис», использованное Клини. В своей статье 1943 года «Рекурсивные предикаты и квантификаторы» Клин предложил свой «ТЕЗИС I»:

"Этот эвристический факт [общерекурсивные функции эффективно рассчитываются] … привел Чёрча к формулировке следующего тезиса (²²). Тот же тезис неявен в описании Тьюринга вычислительных машин (²³).

"ТЕЗИС I. Всякая эффективно вычисляемая функция (эффективно разрешимый предикат) является обще<ref>Устаревшее использование Клини и другими чтобы отличать Гёделевский (1931) «rekursiv» (несколькими годами позже названный примитивной рекурсией by Rózsa Péter (cf Шаблон:Harvcolnb)) от рекурсии Эрбрана — Гёделя (1934) то есть примитивной рекурсии с дополнительным μ-оператором, называемой сегодня μ-рекурсией, или проще, «рекурсией».</ref> рекурсивной [курсив Клини]

«Поскольку точное математическое определение термина, эффективно вычисляемый (эффективно разрешимый), было бы желательным, мы можем принять этот тезис … как определение этого термина …»<ref name="Davis274">Шаблон:Harvnb in Шаблон:Harvcolnb</ref>

(²²) ссылка на Чёрча 1936

(²³) ссылка Тьюринга 1936-7

Клини далее отмечает, что:

«… тезис имеет характер гипотезы — пункт, отмеченный Постом и Тьюрингом (²⁴). Если мы рассмотрим тезис и его обратное как определение, то гипотеза является гипотезой о применении математической теории, полученной из этого определения. Для принятия этой гипотезы, как мы предложили, есть довольно убедительные основания»<ref name="Davis274" />

(²⁴) ссылка на Post 1936 of Post and Church’s Formal definitions in the theory of ordinal numbers, Fund. Math. vol 28 (1936) pp.11-21 (see ref. #2, Шаблон:Harvcolnb).

Литература

• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Cite book Includes original papers by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this section.
• Шаблон:Cite book
• Шаблон:Cite book
• Шаблон:Статья
• Шаблон:Статья