Просмотр кода страницы Тезис Чёрча — Тьюринга

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

Тезис был высказан [[Чёрч, Алонзо|Алонзо Чёрчем]] и [[Тьюринг, Алан|Аланом Тьюрингом]] в середине [[1930-е|1930-х годов]]<ref>{{статья |заглавие=An Unsolvable Problem of Elementary Number Theory |издание=[[American Journal of Mathematics]] |номер=58 |страницы=345—363 |jstor=2371045 |том=58 |doi=10.2307/2371045 |язык=en |автор=Church, Alonzo |год=1936 |тип=journal}}</ref><ref>{{статья |заглавие=A Note on the Entscheidungsproblem |издание={{iw|Journal of Symbolic Logic}} |номер=1 |страницы=40—41 |язык= |автор=Church, Alonzo |год=1936}}</ref><ref>{{source|Q25864184|ref=Turing|ref-year=1937}} <!-- On Computable Numbers, with an Application to the Entscheidungsproblem // Proceedings of the London Mathematical Society --></ref><ref>{{source|Q27638524|ref=Turing|ref-year=1938}} <!-- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction // Proceedings of the London Mathematical Society --></ref>. Существенен для многих областей науки и философии науки, в том числе для [[Математическая логика|математической логики]], [[Теория доказательств|теории доказательств]], [[Информатика|информатики]], [[Кибернетика|кибернетики]].

== Формулировки ==
В терминах [[Теория рекурсии|теории рекурсии]], тезис формулируется как точное описание интуитивного понятия вычислимости классом [[общерекурсивная функция|общерекурсивных функций]]. В этой формулировке часто упоминается как просто тезис Чёрча{{sfn|Жар холодных чисел и пафос бесстрастной логики|1977|с=143}}.

Более общая формулировка была дана [[Клини, Стивен Коул|Стивеном Клини]], согласно которой все частичные (то есть не обязательно определённые для всех значений аргументов) функции, вычислимые посредством алгоритмов, являются частично рекурсивными{{sfn|Алгоритмы и рекурсивные функции|1986|с=12}}.

В терминах вычислимости по Тьюрингу тезис гласит, что для любой алгоритмически вычислимой функции существует вычисляющая её значения [[машина Тьюринга]]{{sfn|Новый ум короля|2003|с=55}}. Иногда в такой формулировке фигурирует как '''тезис Тьюринга'''. Ввиду того, что классы [[Вычислимая функция|частично вычислимых по Тьюрингу]] и частично рекурсивных функций совпадают, утверждение объединяют в единый ''тезис Чёрча — Тьюринга''.

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

== История ==
Одной из важных проблем для [[Логика|логиков]] в 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|url=http://www.logicmatters.net/resources/pdfs/CTT.pdf |date=20210813075909 }}</ref>. было ли понятие «эффективной вычислимости» (i) «[[Аксиома|аксиомой]] или аксиомами» в аксиоматической системе или (ii) просто определением, которое «идентифицировало» два или более предложений или (iii) эмпирической гипотезой, которую следует проверить на естественных событиях или (iv) или просто предложением ради аргумента (то есть «тезиса»).

=== 1930—1952 ===
В ходе изучения проблемы Чёрч и его ученик [[Стивен Клини]] ввели понятие [[Лямбда-исчисление|λ-определимых функций]], и они смогли доказать, что несколько больших классов функций, часто встречающихся в теории чисел, были λ-определимыми<ref>cf footnote 3 in {{harvnb|Church|1936a}} ''An Unsolvable Problem of Elementary Number Theory'' in {{harvcolnb|Davis|1965|p=89}}</ref>. Дискуссия началась, когда Чёрч предложил [[Гёдель, Курт|Курту Гёделю]] определить «эффективно вычислимые» функции как λ-определимые функции. Однако Гёдель не был убеждён и назвал это предложение «полностью неудовлетворительным»<ref>Dawson 1997:99.{{Full citation needed|date=November 2017}}</ref>. Тем не менее Гёдель в переписке с Чёрчем предложил [[аксиома]]тизировать понятие «эффективной вычислимости»; В письме Клини и Чёрчу он сообщил, что

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

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

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

Много лет спустя в письме к Дэвису (около 1965 года) Гёдель сказал, что «он был во время этих [1934] лекций, совсем не убеждён в том, что его концепция рекурсии включает все возможные рекурсии»<ref>Davis’s commentary before Gödel 1934 in {{harvcolnb|Davis|1965|p=40}}</ref>. К 1963 году Гёдель отказался от рекурсии Эрбрана — Гёделя и λ-исчисления в пользу машины Тьюринга как определения «алгоритма» или «механической процедуры» или «формальной системы»<ref>Детальное обсуждение гёделевского использования тьюринговых машин как моделей вычисления см. {{cite web |author=Shagrir |date=2006 |url=http://moon.cc.huji.ac.il/oron-shagrir/papers/Goedel_on_Turing_on_Computability.pdf |format=PDF |title=Goedel on Turing on Computability |accessdate=2016-02-08 |archiveurl=https://web.archive.org/web/20151217145831/http://moon.cc.huji.ac.il/oron-shagrir/papers/Goedel_on_Turing_on_Computability.pdf |archivedate=2015-12-17 }}</ref>.

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

{{начало цитаты}}
На самом деле в работе Чёрча и других это отождествление излагается значительно сильнее рабочей гипотезы. Но маскировка этого отождествления под определение … ослепляет нас необходимостью постоянной проверки.
{{конец цитаты|источник=<ref>Post 1936 in {{harvcolnb|Davis|1965|p=291}}, 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|Davis|1965|p=263ff}}</ref>. Чёрч быстро понял, насколько убедительным был анализ Тьюринга. В своем обзоре работы Тьюринга он ясно дал понять, что понятие Тьюринга сделало «отождествление с эффективностью в обычном (не явно определённом) смысле, очевидном сразу»<ref>{{harvnb|Church|1937}}</ref>.

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

Россер (1939) формально отождествил три понятия как определения:
: «Все три ''определения'' эквивалентны, поэтому не имеет значения, какое из них используется».

'''Клини предлагает ''тезис Чёрча''''' : здесь оставлено явное выражение «тезис», использованное Клини. В своей статье 1943 года «Рекурсивные предикаты и квантификаторы» Клин предложил свой «ТЕЗИС I»:
: "Этот эвристический факт [общерекурсивные функции эффективно рассчитываются] … привел Чёрча к формулировке следующего тезиса (<sup>22</sup>). Тот же тезис неявен в описании Тьюринга вычислительных машин (<sup>23</sup>).
:: "ТЕЗИС I. ''Всякая эффективно вычисляемая функция (эффективно разрешимый предикат) является обще<ref>Устаревшее использование Клини и другими чтобы отличать Гёделевский (1931) «rekursiv» (несколькими годами позже названный [[Примитивно рекурсивная функция|примитивной рекурсией]] by [[Rózsa Péter]] (cf {{harvcolnb|Gandy|1994|p=68}})) от рекурсии Эрбрана — Гёделя (1934) то есть примитивной рекурсии с дополнительным [[Частично рекурсивная функция|μ-оператором]], называемой сегодня μ-рекурсией, или проще, «рекурсией».</ref> рекурсивной'' [курсив Клини]
: «Поскольку точное математическое определение термина, эффективно вычисляемый (эффективно разрешимый), было бы желательным, мы можем принять этот тезис … как определение этого термина …»<ref name="Davis274">{{harvnb|Kleene|1943}} in {{harvcolnb|Davis|1965|p=274}}</ref>
:: (<sup>22</sup>) ссылка на Чёрча 1936
:: (<sup>23</sup>) ссылка Тьюринга 1936-7
Клини далее отмечает, что:
: «… тезис имеет характер гипотезы — пункт, отмеченный Постом и Тьюрингом (<sup>24</sup>). Если мы рассмотрим тезис и его обратное как определение, то гипотеза является гипотезой о применении математической теории, полученной из этого определения. Для принятия этой гипотезы, как мы предложили, есть довольно убедительные основания»<ref name="Davis274" />
::: (<sup>24</sup>) ссылка на 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|Davis|1965|p=286}}).

== Примечания ==
{{Примечания}}

== Литература ==
* {{книга
 | автор           = [[Клини, Стивен Коул|Клини С. К.]]
 | заглавие      = Математическая логика
 | место          = М.
 | издательство  = Мир
 | год           = 1973
 | страниц    = 480
 | isbn =
 | ref             = Математическая логика
 }}
* {{книга|автор=Бирюков Б. В., [[Тростников, Виктор Николаевич|Тростников В. Н.]]|заглавие=Жар холодных чисел и пафос бесстрастной логики|место=М.|издательство=Знание|год=1977|страниц=192|isbn=|ref=Жар холодных чисел и пафос бесстрастной логики}}
* {{книга
 | автор           = [[Мальцев, Анатолий Иванович|Мальцев А. И.]]
 | заглавие      = Алгоритмы и рекурсивные функции
 | место          = М.
 | издательство  = Наука
 | год           = 1986
 | страниц    = 368
 | isbn =
 | ref             = Алгоритмы и рекурсивные функции
 }}
* {{книга
 | автор           = [[Пенроуз, Роджер|Пенроуз Р.]]
 | заглавие      = [[Новый ум короля]]
 | место          = М.
 | издательство  = Едиториал УРСС
 | год           = 2003
 | страниц    = 384
 | isbn =
 | ref             = Новый ум короля
 }}
* {{статья |заглавие=An Unsolvable Problem of Elementary Number Theory |издание=[[American Journal of Mathematics]] |номер=2 |страницы=345—363 |jstor=2371045 |том=58 |doi=10.2307/2371045 |ref=Church |язык=en |автор=Church, Alonzo |месяц=4 |год=1936a |тип=journal}}
* {{cite book|title=The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions|url=https://archive.org/details/undecidablebasic0000davi|url-access=registration|editor-link=Martin Davis (mathematician)|editor-last=Davis|editor-first=Martin|publisher=Raven Press|location=New York|year=1965|ref=Davis}} Includes original papers by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this section.
* {{cite book|last=Gandy|first=Robin|title=The Kleene Symposium|editor=H. J. Barwise |editor2=H. J. Keisler |editor3=K. Kunen|publisher=North-Holland Publishing Company|year=1980|pages=123–148|chapter=Church's Thesis and the Principles for Mechanisms|author-link=Robin Gandy|ref=Gandy}}
* {{cite book|last=Gandy|first=Robin|title=The universal Turing Machine: A Half-Century Survey|editor-first=Rolf |editor-last=Herken|publisher=Wien Springer–Verlag|location=New York|year=1994|pages=51ff|isbn=978-3-211-82637-9}}
* {{статья |заглавие=Review: A. M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem |издание=Journal of Symbolic Logic |том=2 |номер=1 |страницы=42—43 |doi=10.2307/2268810 |ref=Church |язык=en |тип=journal |автор=Church, Alonzo |месяц=3 |год=1937}}
* {{статья |заглавие=Recursive Predicates and Quantifiers |издание=American Mathematical Society Transactions |том=54 |номер=1 |страницы=41—73 |doi=10.2307/1990131 |jstor=1990131 |ref=Kleene |язык=en|автор=Kleene, Stephen Cole |год=1943}}

[[Категория:Теория алгоритмов]]
[[Категория:Алан Тьюринг]]