Тезис Чёрча — Тьюринга
Те́зис Чёрча — Тью́ринга — логико-математический принцип, устанавливающий эквивалентность между интуитивным понятием
Тезис был высказан
Формулировки
В терминах
Более общая формулировка была дана Стивеном Клини, согласно которой все частичные (то есть не обязательно определённые для всех значений аргументов) функции, вычислимые посредством алгоритмов, являются частично рекурсивными[7].
В терминах вычислимости по Тьюрингу тезис гласит, что для любой алгоритмически вычислимой функции существует вычисляющая её значения машина Тьюринга[8]. Иногда в такой формулировке фигурирует как тезис Тьюринга. Ввиду того, что классы частично вычислимых по Тьюрингу и частично рекурсивных функций совпадают, утверждение объединяют в единый тезис Чёрча — Тьюринга.
Позднее были сформулированы другие практические варианты утверждения:
- физический тезис Чёрча — Тьюринга: любая функция, которая может быть вычислена физическим устройством, может быть вычислена машиной Тьюринга;
- сильный тезис Чёрча — Тьюринга(тезис Чёрча — Тьюринга — Дойча): любой конечный физический процесс, не использующий аппарат, связанный с непрерывностью и бесконечностью, может быть вычислен физическим устройством.
История
Одной из важных проблем для
1930—1952
В ходе изучения проблемы Чёрч и его ученик
Его единственная идея в то время состоит в том, что может быть возможно задать термин эффективной вычислимости как неопределенного понятия в виде набора аксиом, которые бы воплощали общепринятые свойства этого понятия и затем что-то делать на этой основе.
— [13]
Но Гёдель не дал никаких дальнейших указаний. Он предложил только рекурсию, модифицированную предложением Гербранда, о чём Гёдель подробно написал на своих лекциях в 1934 году в Принстоне Нью-Джерси (Клини и Россер расшифровали записи). Но он не думал, что две идеи могут быть удовлетворительно определены «кроме эвристически»[14].
Затем необходимо было идентифицировать и доказать эквивалентность двух понятий эффективной вычислимости. Оснащенный λ-исчислением и «общей» рекурсией, Стивен Клини с помощью Чёрча и Дж. Баркли Россера подготовили доказательства (1933, 1935), чтобы показать, что эти два исчисления эквивалентны. Чёрч впоследствии изменил свои методы, включив использование рекурсии Гербранда-Гёделя, а затем доказал (1936), что проблема разрешения неразрешима: нет обобщенного алгоритма, который может определить, имеет ли корректно сформулированная формула «нормальную форму»[15].
Много лет спустя в письме к Дэвису (около 1965 года) Гёдель сказал, что «он был во время этих [1934] лекций, совсем не убежден в том, что его концепция рекурсии включает все возможные рекурсии»[16]. К 1963 году Гёдель отказался от рекурсии Гербранда-Гёделя и λ-исчисления в пользу машины Тьюринга как определения «алгоритма» или «механической процедуры» или «формальной системы»[17].
Гипотеза, ведущая к
На самом деле в работе Чёрча и других это отождествление излагается значительно сильнее рабочей гипотезы. Но маскировка этого отождествления под определение … ослепляет нас необходимостью постоянной проверки.
— [20]
Скорее, он считал понятие «эффективной вычислимости» просто «рабочей гипотезой», которая могла бы привести индуктивным умозаключением к «естественному закону», а не «определению или аксиоме»[21]. Эта идея была «резко» подвергнута критике со стороны Чёрча[22].
Таким образом, Пост в своей статье 1936 года также отклонял предложение Курта Гёделя Чёрчу в 1934—1935 годах о том, что тезис может быть выражен как аксиома или множество аксиом[13].
Тьюринг добавляет ещё одно определение, Россер приравнивает все три : за короткое время появилась статья (1936-37) Тьюринга «О вычислимых числах и применение к проблеме разрешения».[18] В ней он задал понятие «эффективной вычислимости» по-другому, с введением его а-машин (теперь они известны как абстрактная вычислительная модель машины Тьюринга). И в доказательном эскизе, добавленном как «Приложение» к его статье 1936-37, Тьюринг показал, что классы функций, определяемые λ-исчислением и машинами Тьюринга, совпадают[23]. Чёрч быстро понял, насколько убедительным был анализ Тьюринга. В своем обзоре работы Тьюринга он ясно дал понять, что понятие Тьюринга сделало «отождествление с эффективностью в обычном (не явно определённом) смысле, очевидном сразу»[24].
Через несколько лет (1939) Тьюринг предложил, как это сделали Чёрч и Клини перед ним, что его формальное определение механического вычислительного агента было правильным[25]. Таким образом, к 1939 году и Чёрч (1934), и Тьюринг (1939) индивидуально предложили, чтобы их «формальные системы» были определениями «эффективной вычислимости»[26]; а не сформулировали свои утверждения как тезисы.
Россер (1939) формально отождествил три понятия как определения:
- «Все три определения эквивалентны, поэтому не имеет значения, какое из них используется».
Клини предлагает тезис Чёрча : здесь оставлено явное выражение «тезис», использованное Клини. В своей статье 1943 года «Рекурсивные предикаты и квантификаторы» Клин предложил свой «ТЕЗИС I»:
- "Этот эвристический факт [общерекурсивные функции эффективно рассчитываются] … привел Чёрча к формулировке следующего тезиса (22). Тот же тезис неявен в описании Тьюринга вычислительных машин (23).
- "ТЕЗИС I. Всякая эффективно вычисляемая функция (эффективно разрешимый предикат) является обще[27] рекурсивной [курсив Клини]
- «Поскольку точное математическое определение термина, эффективно вычисляемый (эффективно разрешимый), было бы желательным, мы можем принять этот тезис … как определение этого термина …»[28]
- (22) ссылка на Чёрча 1936
- (23) ссылка Тьюринга 1936-7
Клини далее отмечает, что:
- «… тезис имеет характер гипотезы — пункт, отмеченный Постом и Тьюрингом (24). Если мы рассмотрим тезис и его обратное как определение, то гипотеза является гипотезой о применении математической теории, полученной из этого определения. Для принятия этой гипотезы, как мы предложили, есть довольно убедительные основания»[28]
- (24) ссылка на 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).
Примечания
- ↑ Математическая логика, 1973, с. 280.
- doi:10.2307/2371045. —.
- ↑ Church, Alonzo. A Note on the Entscheidungsproblem (неопр.) // Journal of Symbolic Logic[англ.]. — 1936. — № 1. — С. 40—41.
- ↑ 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
- ↑ 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
- ↑ Жар холодных чисел и пафос бесстрастной логики, 1977, с. 143.
- ↑ Алгоритмы и рекурсивные функции, 1986, с. 12.
- ↑ Новый ум короля, 2003, с. 55.
- ↑ Комментарий Девиса к «Черч 1936 An Unsolvable Problem of Elementary Number Theory» в Davis 1965:88. Чёрч использовал слова «эффективная вычисляемость»(«effective calculability») на странице 100ff.
- ↑ cf Smith (July 11, 2007) Church’s Thesis after 70 Years at http://www.logicmatters.net/resources/pdfs/CTT.pdf Архивная копия от 13 августа 2021 на Wayback Machine
- ↑ cf footnote 3 in Church, 1936a An Unsolvable Problem of Elementary Number Theory in Davis 1965:89
- ↑ Dawson 1997:99.[уточнить дату]
- ↑ 1 2 Sieg 1997:160.
- ↑ Sieg 1997:160 цитирует письмо, написанное в 1935 Чёрчем для Клини, cf Footnote 3 in Gödel 1934 in Davis 1965:44.
- ↑ cf Church 1936 in Davis 1965:105ff
- ↑ Davis’s commentary before Gödel 1934 in Davis 1965:40
- ↑ Детальное обсуждение Гёделевского использования Тьюринговых машин как моделей вычисления см. Shagrir. Goedel on Turing on Computability (PDF) (2006). Дата обращения: 8 февраля 2016. Архивировано 17 декабря 2015 года.
- ↑ 1 2 Turing, 1937
- ↑ cf. Editor’s footnote to Post 1936 Finite Combinatory Process. Formulation I. at Davis 1965:289
- ↑ Post 1936 in Davis 1965:291, footnote 8.
- ↑ Post 1936 in Davis 1952:291
- ↑ Sieg 1997:171 and 176-7
- ↑ Turing 1936-7 in Davis 1965:263ff
- ↑ Church, 1937
- ↑ Turing 1939 in Davis:160
- ↑ cf. Church 1934 in Davis 1965:100, also Turing 1939 in Davis 1965:160
- ↑ Устаревшее использование Клини и другими чтобы отличать Гёделевский (1931) «rekursiv» (несколькими годами позже названный примитивной рекурсией by Rózsa Péter (cf Gandy 1994:68)) от рекурсии Гербранда-Гёделя (1934) то есть примитивной рекурсии с дополнительным μ-оператором, называемой сегодня μ-рекурсией, или проще, «рекурсией».
- ↑ 1 2 Kleene, 1943 in Davis 1965:274
Литература
- Клини С. К. Математическая логика. — М.: Мир, 1973. — 480 с.
- Бирюков Б. В., Тростников В. Н. Жар холодных чисел и пафос бесстрастной логики. — М.: Знание, 1977. — 192 с.
- Мальцев А. И. Алгоритмы и рекурсивные функции. — М.: Наука, 1986. — 368 с.
- Пенроуз Р. Новый ум короля. — М.: Едиториал УРСС, 2003. — 384 с.
- Church, Alonzo. An Unsolvable Problem of Elementary Number Theory (англ.) // doi:10.2307/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. —.