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

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

Тезис был высказан Алонзо Чёрчем и Аланом Тьюрингом в середине 1930-х годов^[2][3][4][5]. Существенен для многих областей науки и философии науки, в том числе для математической логики, теории доказательств, информатики, кибернетики.

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

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

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

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

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

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

История

Одной из важных проблем для логиков в 1930-х годах была проблема разрешения: существует ли механическая процедура для отделения математических истин от математических ложностей. Эта задача требовала, чтобы понятие «алгоритм» или «эффективная вычислимость» было закреплено, по крайней мере, чтобы приступить к задаче^[9] С самого начала и по сей день (по состоянию на 2007 год) продолжаются дебаты:^[10]. было ли понятие «эффективной вычислимости» (i) «аксиомой или аксиомами» в аксиоматической системе или (ii) просто определением, которое «идентифицировало» два или более предложений или (iii) эмпирической гипотезой, которую следует проверить на естественных событиях или (iv) или просто предложением ради аргумента (то есть «тезиса»).

1930—1952

В ходе изучения проблемы Чёрч и его ученик Стивен Клини ввели понятие λ-определимых функций, и они смогли доказать, что несколько больших классов функций, часто встречающихся в теории чисел, были λ-определимыми^[11]. Дискуссия началась, когда Чёрч предложил Курту Гёделю определить «эффективно вычислимые» функции как λ-определимые функции. Однако Гёдель не был убеждён и назвал это предложение «полностью неудовлетворительным»^[12]. Тем не менее Гёдель в переписке с Чёрчем предложил аксиоматизировать понятие «эффективной вычислимости»; В письме Клини и Чёрчу он сообщил, что

Его единственная идея в то время состоит в том, что может быть возможно задать термин эффективной вычислимости как неопределенного понятия в виде набора аксиом, которые бы воплощали общепринятые свойства этого понятия и затем что-то делать на этой основе.

— ^[13]

Но Гёдель не дал никаких дальнейших указаний. Он предложил только рекурсию, модифицированную предложением Гербранда, о чём Гёдель подробно написал на своих лекциях в 1934 году в Принстоне Нью-Джерси (Клини и Россер расшифровали записи). Но он не думал, что две идеи могут быть удовлетворительно определены «кроме эвристически»^[14].

Затем необходимо было идентифицировать и доказать эквивалентность двух понятий эффективной вычислимости. Оснащенный λ-исчислением и «общей» рекурсией, Стивен Клини с помощью Чёрча и Дж. Баркли Россера подготовили доказательства (1933, 1935), чтобы показать, что эти два исчисления эквивалентны. Чёрч впоследствии изменил свои методы, включив использование рекурсии Гербранда-Гёделя, а затем доказал (1936), что проблема разрешения неразрешима: нет обобщенного алгоритма, который может определить, имеет ли корректно сформулированная формула «нормальную форму»^[15].

Много лет спустя в письме к Дэвису (около 1965 года) Гёдель сказал, что «он был во время этих [1934] лекций, совсем не убежден в том, что его концепция рекурсии включает все возможные рекурсии»^[16]. К 1963 году Гёдель отказался от рекурсии Гербранда-Гёделя и λ-исчисления в пользу машины Тьюринга как определения «алгоритма» или «механической процедуры» или «формальной системы»^[17].

Гипотеза, ведущая к естественному закону? : В конце 1936 года статья Алана Тьюринга (также доказывающая, что проблема разрешения неразрешима) была озвучена в устной форме, но ещё не появилась в печати^[18]. С другой стороны, появилась статья Эмиля Поста 1936 года и была сертифицирована независимо от работы Тьюринга^[19]. Пост категорически не согласился с Чёрчевским «отождествлением» (identification) эффективной вычислимости c λ-исчислением и рекурсией, заявив:

На самом деле в работе Чёрча и других это отождествление излагается значительно сильнее рабочей гипотезы. Но маскировка этого отождествления под определение … ослепляет нас необходимостью постоянной проверки.

— ^[20]

Скорее, он считал понятие «эффективной вычислимости» просто «рабочей гипотезой», которая могла бы привести индуктивным умозаключением к «естественному закону», а не «определению или аксиоме»^[21]. Эта идея была «резко» подвергнута критике со стороны Чёрча^[22].

Таким образом, Пост в своей статье 1936 года также отклонял предложение Курта Гёделя Чёрчу в 1934—1935 годах о том, что тезис может быть выражен как аксиома или множество аксиом^[13].

Тьюринг добавляет ещё одно определение, Россер приравнивает все три : за короткое время появилась статья (1936-37) Тьюринга «О вычислимых числах и применение к проблеме разрешения».^[18] В ней он задал понятие «эффективной вычислимости» по-другому, с введением его а-машин (теперь они известны как абстрактная вычислительная модель машины Тьюринга). И в доказательном эскизе, добавленном как «Приложение» к его статье 1936-37, Тьюринг показал, что классы функций, определяемые λ-исчислением и машинами Тьюринга, совпадают^[23]. Чёрч быстро понял, насколько убедительным был анализ Тьюринга. В своем обзоре работы Тьюринга он ясно дал понять, что понятие Тьюринга сделало «отождествление с эффективностью в обычном (не явно определённом) смысле, очевидном сразу»^[24].

Через несколько лет (1939) Тьюринг предложил, как это сделали Чёрч и Клини перед ним, что его формальное определение механического вычислительного агента было правильным^[25]. Таким образом, к 1939 году и Чёрч (1934), и Тьюринг (1939) индивидуально предложили, чтобы их «формальные системы» были определениями «эффективной вычислимости»^[26]; а не сформулировали свои утверждения как тезисы.

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

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

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

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

"ТЕЗИС I. Всякая эффективно вычисляемая функция (эффективно разрешимый предикат) является обще^[27] рекурсивной [курсив Клини]

«Поскольку точное математическое определение термина, эффективно вычисляемый (эффективно разрешимый), было бы желательным, мы можем принять этот тезис … как определение этого термина …»^[28]

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

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

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

«… тезис имеет характер гипотезы — пункт, отмеченный Постом и Тьюрингом (²⁴). Если мы рассмотрим тезис и его обратное как определение, то гипотеза является гипотезой о применении математической теории, полученной из этого определения. Для принятия этой гипотезы, как мы предложили, есть довольно убедительные основания»^[28]

(²⁴) ссылка на 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, Davis 1965:286).

Примечания

1. Математическая логика, 1973, с. 280.
2. Church, Alonzo. An Unsolvable Problem of Elementary Number Theory (англ.) // American Journal of Mathematics : journal. — 1936. — Vol. 58, no. 58. — P. 345—363. — doi:10.2307/2371045. — JSTOR 2371045.
3. Church, Alonzo. A Note on the Entscheidungsproblem (неопр.) // Journal of Symbolic Logic^[англ.]. — 1936. — № 1. — С. 40—41.
4. Turing A. On Computable Numbers, with an Application to the Entscheidungsproblem (англ.) // Proceedings of the London Mathematical Society — London Mathematical Society, 1937. — Vol. s2-42, Iss. 1. — P. 230—265. — ISSN 0024-6115; 1460-244X; 0024-6115 — doi:10.1112/PLMS/S2-42.1.230
5. Turing A. M. On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction (англ.) // Proceedings of the London Mathematical Society — London Mathematical Society, 1938. — Vol. s2-43, Iss. 6. — P. 544—546. — ISSN 0024-6115; 1460-244X; 0024-6115 — doi:10.1112/PLMS/S2-43.6.544
6. Жар холодных чисел и пафос бесстрастной логики, 1977, с. 143.
7. Алгоритмы и рекурсивные функции, 1986, с. 12.
8. Новый ум короля, 2003, с. 55.
9. Комментарий Девиса к «Черч 1936 An Unsolvable Problem of Elementary Number Theory» в Davis 1965:88. Чёрч использовал слова «эффективная вычисляемость»(«effective calculability») на странице 100ff.
10. cf Smith (July 11, 2007) Church’s Thesis after 70 Years at http://www.logicmatters.net/resources/pdfs/CTT.pdf Архивная копия от 13 августа 2021 на Wayback Machine
11. cf footnote 3 in Church, 1936a An Unsolvable Problem of Elementary Number Theory in Davis 1965:89
12. Dawson 1997:99.^{[уточнить дату]}
13. Sieg 1997:160.
14. Sieg 1997:160 цитирует письмо, написанное в 1935 Чёрчем для Клини, cf Footnote 3 in Gödel 1934 in Davis 1965:44.
15. cf Church 1936 in Davis 1965:105ff
16. Davis’s commentary before Gödel 1934 in Davis 1965:40
17. Детальное обсуждение Гёделевского использования Тьюринговых машин как моделей вычисления см. Shagrir. Goedel on Turing on Computability  (неопр.) (PDF) (2006). Дата обращения: 8 февраля 2016. Архивировано 17 декабря 2015 года.
18. Turing, 1937
19. cf. Editor’s footnote to Post 1936 Finite Combinatory Process. Formulation I. at Davis 1965:289
20. Post 1936 in Davis 1965:291, footnote 8.
21. Post 1936 in Davis 1952:291
22. Sieg 1997:171 and 176-7
23. Turing 1936-7 in Davis 1965:263ff
24. Church, 1937
25. Turing 1939 in Davis:160
26. cf. Church 1934 in Davis 1965:100, also Turing 1939 in Davis 1965:160
27. Устаревшее использование Клини и другими чтобы отличать Гёделевский (1931) «rekursiv» (несколькими годами позже названный примитивной рекурсией by Rózsa Péter (cf Gandy 1994:68)) от рекурсии Гербранда-Гёделя (1934) то есть примитивной рекурсии с дополнительным μ-оператором, называемой сегодня μ-рекурсией, или проще, «рекурсией».
28. Kleene, 1943 in Davis 1965:274

Литература

• Клини С. К. Математическая логика. — М.: Мир, 1973. — 480 с.
• Бирюков Б. В., Тростников В. Н. Жар холодных чисел и пафос бесстрастной логики. — М.: Знание, 1977. — 192 с.
• Мальцев А. И. Алгоритмы и рекурсивные функции. — М.: Наука, 1986. — 368 с.
• Пенроуз Р. Новый ум короля. — М.: Едиториал УРСС, 2003. — 384 с.
• Church, Alonzo. An Unsolvable Problem of Elementary Number Theory (англ.) // American Journal of Mathematics : journal. — 1936a. — April (vol. 58, no. 2). — P. 345—363. — doi:10.2307/2371045. — JSTOR 2371045.
• The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York : Raven Press, 1965. Includes original papers by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this section.
• Gandy, Robin. Church's Thesis and the Principles for Mechanisms // The Kleene Symposium / H. J. Barwise ; H. J. Keisler ; K. Kunen. — North-Holland Publishing Company, 1980. — P. 123–148.
• Gandy, Robin. The universal Turing Machine: A Half-Century Survey. — New York : Wien Springer–Verlag, 1994. — P. 51ff. — ISBN 978-3-211-82637-9.
• Church, Alonzo. Review: A. M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem (англ.) // Journal of Symbolic Logic : journal. — 1937. — March (vol. 2, no. 1). — P. 42—43. — doi:10.2307/2268810.
• Kleene, Stephen Cole. Recursive Predicates and Quantifiers (англ.) // American Mathematical Society Transactions. — 1943. — Vol. 54, no. 1. — P. 41—73. — doi:10.2307/1990131. — JSTOR 1990131.