У теорији израчунљивости, Черч-Тјурингова теза (такође позната као Тјуринг-Черчова теза, Черч-Тјурингове претпоставке, Черчова теза, Черчова претпоставка и Тјурингова теза) је хипотеза ("теза") о природи израчунљивих функција. Једноставно речено, Черч-Тјурингова теза гласи да је функција на природним бројевима израчунљива у неформалном смислу (тј израчунљива од стране људског бића коришћењем метода оловке и папира, игноришући ограничења ресурса) ако и само ако је израчунљива Тјуринговом машином. Теза је добила име по америчком математичару Алонзу Черчу и британском математичару Алану Тјурингу.
Пре прецизног дефинисања израчунљивих функција, математичари често користе неформалан термин ефективно израчунљив да опишу функције које су за израчунљиве методама папира и оловке-. 1930-их, било је неколико независних покушаја да се формализује појам Израчунљивости: 1933, Аустријски-Амерички математичар Курт Гедел, са Жаком Ербраном, је направио дормалну дефиницију класа под називом општа рекурзивна функција. Класа општих рекурзивних функција је најмања класа функција (могуће са више од једног аргумента) која укључује константне функције, пројекте, функцију наследног, и који је затворен у сложеној функцији и рекурзији. 1936, Алонзо Черч је створио метод за дефинисање функција под називом Ламбда рачун. У оквиру ламбда рачуна он је дефинисао кодирање природних бројева под називом Черчови бројеви. Функција над природним бројевима се зове ламбда израчунљива ако се одговарајућа функција на Черчовим бројевима може представити у тајању ламбда рачуна. Такође 1936, пре проучавања Черчовог рада, Алан Тјуринг је створио теоретски модел за машине, који се сада зове Тјурингове машине, које се могу побринути за рачунање из улаза манипулацијом симбола на траци. С обзиром на одговарајуће кодирање природних бројева као секвенце симбола, функција природних бројева се назива Тјуринг израчунљива ако неке Тјурингове машине израчунају одговарајућу функцију над кодираним природним бројевима.
Черч и Тјуринг су доказали да се ове три формално дефинисане класе израчунљивих функција поклапају: функција је ламбда израчуљива ако и само ако је Тјуринг израчунљива и акко је опште рекурзивна. Ово је натерало математичаре и информатичаре да поверују да је концепт израчунљивости тачно окарактерисан овим трома еквивалентним процесима. Остали формални покушаји да се карактерише израчунљивост је касније ојачао снагу овог веровања (погледати испод).
С друге стране, Черч-Тјурингова теза наводи да су горенаведене три формално дефинисане класе израчинљивих функција поклапају са неформалном појмом ефикасно прорачунљиве функције. Пошто, као неформални појам, концепт ефективне предвидивости нема формалну дефиницију, теза, иако има скоро универзалну прихваћеност, не може бити формално доказана.
Од свог оснивања, варијације на основној тези су се појавиле, укључујући изјаве о томе шта ће моћи физички бити реализовано уз помоћ рачунара у нашем универзуму (физичка Черч-Тјуринг теза) и шта ће моћи бити ефикасно израчунато (Сложеност-теоријски Черч-Тјурингова теза). Ове варијације нису због Черча или Тјуринга, али проистичу из каснијег рада у теорији сложености и дигиталне физике. Теза има импликације за филозофију духа.
Искази у Черчовим и Тјуринговим речима Џ. Б. Росер (1939) бави се појмом "ефективне израчунљивости" на следећи начин: "Јасно постојање ЦЦ и РЦ (Черчови је и Росерови докази) претпоставља прецизну дефиницију 'ефективног' 'Ефективни метод" се овде користи у веома посебном смислу методе сви кораци који су прецизно унапред одређени и који сигурно произведе одговор у коначном броју корака. „Такосе прилог-придев "ефективан" користи у смислу "1А: производећи одлучујућег, убедљивог, или жељеног ефекта" и "способан да произведе резултат".Merriam Webster's Ninth New Collegiate Dictionary"See also" Merriam-Webster's Online Dictionary, 11th Edition (accessed July 26, 2014), which also gives these definitions for "effective" – the first ["producing a decided, decisive, or desired effect"] as the definition for sense "1a" of the word "effective", and the second ["capable of producing a result"] as part of the "Synonym Discussion of EFFECTIVE" there, (in the introductory part, where it summarizes the similarities between the meanings of the words "effective", "effectual", "efficient", and "efficacious").
У наставку, речи "ефикасно израчунљив" ће значити "произведен од стране било ког интуитивног 'ефективног' значи уопште" и "ефективно подложан рачунању" ће значити "произведени од стране Тјурингове-машине или еквивалентног механичког уређаја". Тјурингова "дефиниција" дата у фусноти у својој 1939. докторирао тезу Системи логике базираних на редним бројевима под надзором Черча, су готово исти: "† Ми ћемо користити израз" израчунљива функција ' да означимо функцију израчунату на машини, и пустимо ' ефективно израчунате 'да се односи на интуитивну идеју без посебне идентификације са било којим од ових дефиниција. " Теза може гласити као следеће: Свака ефективно израчунљива функција је функција подлежна рачунању. Тјуринг је то изјавио на овај начин: "Констатовано је да је ..." функција је ефективно израчунљива ако се њене вредности могу наћи помоћу неког чисто механичког процеса. " Можемо узети дословно, схватајући да је чисто механички процес онај који може да се обавља помоћу машине ... доводи до ... идентификације израчунљивости † са ефективном предвидивошчу. "(† је фуснота изнад, Ибид.)
Историја Један од важних проблема за логичаре 1930. био је Давид Хилбертов Entscheidungsproblem, која је затражила да ли је механички поступак за одвајање математичких истина од математичких неистина. Овој потрази је потребно да појам "алгоритма" или "ефективне предвидивост" буду приковани, барем довољно добро за трагање за почетак. Али од самог почетка покушаја Алонза Черча је почела са дебатом која се наставља до данашњег дана. Да ли је појам "ефективне предвидивост" да буде (и) "аксиом или аксиоми" у аксиоматског систему, или (ии) само дефиниција да је "идентификовао" два или више предлога, или (иии) емпиријска хипотеза да се утврди посматрањем природних догађаја, или (ив) или само предлог зарад аргумента (односно "теза").In his review of Church's Thesis after 70 Years edited by Adam Olszewski et al. 2006, Peter Smith's criticism of a paper by Muraswski and Wolenski suggests 4 "lines" re the status of the Church–Turing Thesis: (1) empirical hypothesis (2) axiom or theorem, (3) definition, (4) explication. But Smith opines that (4) is indistinguishable from (3), cf Smith (July 11, 2007) Church's Thesis after 70 Years at http://www.logicmatters.net/resources/pdfs/CTT.pdf
Период 1930—1952. У току студирања проблема, Черч и његов студент Стивен Клини увео је појам λ дефинисане функције, и они су били у стању да докажу да се неколико великих класа функција често срећу у теорији бројева λ-дефинисани.cf footnote 3 in Church 1936 An Unsolvable Problem of Elementary Number Theory in Davis 1965:89 Расправа је почела када је Черч предложио да Гедел треба дефинисати "ефективно израчунљиве" функције као λ дефинисане функције. Гедел, међутим, није био убеђен и назвао предлог "темељно не задовољава". Уместо тога, у преписци са Черчом (ца 1934-5), Гедел је предложио акиоматизинг појам "ефективне предвидивости"; Заиста, 1935 у писму Клину, Черч је известио да: "Његова [Геделов] једина идеја у то време била је да би то било могуће, у смислу ефикасне предвидивост као недефинисаног појма, да наведе скуп аксиома који би отеловљавали општеприхваћена својства овог појма, и да уради нешто на тој основи ". Али Гедел није понудио даља упутства. На крају, он би предложио своју (примитивну) рекурзију, модификовану од стране Хербранда сугестију, коју је Гедел детаљисао у својим предавањима из 1934 Принстон НЈ(Клини и Росер преписали су белешке). Али "није мислио да две идеје могу на задовољавајући начин бити идентификоване " осим хеуристички ".
Даље, било је неопходно да се идентификују и докаже еквивалентност два појма ефикасне предвидивост. Опремљен ламбда-рачуном и "примитивном" рекурзијом, Стивен Клини уз помоћ Черча и Џ. Б. Росера производи доказе (1933, 1935) да покаже да су два рачуна еквивалентна. Черч накнадно измењује своје методе укључују употребу Хербранд-Гедел рекурзије, а затим је доказао (1936) да је Entscheidungsproblem нерешив: Не постоји уопштен "ефективнан обрачун" (метод, алгоритам) који може да одреди да ли су или не формуле у било којој рекурзији - или ламбда рачуну "важеће" (прецизније: нема методе да се покаже да добро формирана формула има "нормалнан облик").
Много година касније, у писму упућеном Дејвису (ца 1965), Гедел би признао да је "он био, у време ових предавања, уопште убеђен да његов концепт рекурзије чини све могуће рекурзије". По 1963-4 Гедел би одрекао Хербранд-Гедел рекурзију и λ-рачуницу у корист Тјурингове машине као дефиниције "алгоритма" или "механичког поступка" или "формалног система".
Хипотеза која је довела до природног закона ?: Крајем 1936 Алан Тјурингов рад (такође доказује да је Entscheidungsproblem нерешив) је досрављен усмено, али се још није појавио у штампи. С друге стране, Емил Постов рад 1936 се појавио и био сертификован независно од рада Тјуринговог рада. Пост се снажно не слаже са Черчовом "идентификацијом" ефективне израчунљивости са λ-рачуном и рекурзијом, наводећи: "Заправо посао је већ урађен од стране Черча и других носи ову идентификацију знатно изван радне фазе хипотезе. Али да прикрије ову идентификацију под дефиницијом ... заслепљује нас на потребу њене непрекидне верификације." Уместо тога, он сматра појам "ефективне предвидивости" као само "радна хипотеза" која може да се доведе индукционим образложењем до "природно право", пре него "дефиницију или аксиом". Ову идеју је "оштро" критиковао Черч.
Тако је Пост у свом раду 1936 такође дисконтовао Курт Геделову сугестију Черчу 1934-5 да теза може бити изражена као аксиом или скуп аксиома.
Тјуринг додаје још једну дефиницију, Росер изједначава све три: У само кратком времену, Тјурингов рад 1936-37 "На израчунљивим бројева, са применом у Entscheidungsproblem" се појавио. У њој је навео још један појам "ефективне израчунљивости" са увођењем својих А-машина (сада познате као Тјурингова машина - апстрактан рачунарски модел). У доказу-скици додаје као "Прилог" у свој рад 1936-37 , Тјуринг је показао да су се класе функција дефинисана λ-рачуном и Тјурингова машина поклопиле. Черч је брзо препознао колико је убедљива Тјурингова анализа. У свом прегледу Тјуринговог рада рекао је да је јасно да је Тјурингова идеја "идентификација са ефикасности у обичном (не експлицитно дефинисаном) смислу евидентна одмах".
За неколико година (1939) Тјуринг би предложио, као Черч и Клини пре њега, да је његова формална дефиниција механичке израчунљивости био исправан. Тако, 1939. године, и Черч (1934) и Тјуринг (1939) су индивидуално предложили да њихови "формални системи" буду дефиниције "ефективне предвидивост"; нико није урамио њихове изјаве као тезу.
Росер (1939) је формално идентификовао три појма као дефиниције: "Све три дефиниције су еквивалентне, тако да није битно која се користи." Клини предлаже Черчову тезу : Ово је оставило отворен израз једне "тезе" Клинију. У свом раду 1943 Рекурзивни Предикати и квантификатори Клини је предложио своју "ТЕЗУ И": "Ова хеуристичка чињеница [опште рекурзивне функције су ефикасно израчунате] ... довела је Черча да наведе следећу тезу (22). Иста теза је садржана у Тјуринговом опису рачунских машина (23). "ТЕЗА И. Свака ефективно израчунљива функција (ефективно одлучив предикат) је опште рекурзивна [Клинијев курзив] "Од прецизне математичке дефиниције појма ефективно израчунљиве (ефективно одлучиве) је хтео, можемо искористити ову тезу ... као дефиницију тога ..." "(22) референце Черча 1936 "(23) референце Тјуринга 1936–7 Клини иде у белешки да :