Church-Turing-avhandlingen är en hypotes som postulerar en motsvarighet mellan den intuitiva uppfattningen om algoritmisk beräkningsbarhet och de strikt formaliserade föreställningarna om en delvis rekursiv funktion och en funktion som kan beräknas på en Turing-maskin . På grund av den intuitiva karaktären hos det initiala konceptet med algoritmisk beräkningsbarhet, har denna avhandling karaktären av en bedömning av detta koncept och kan inte strikt bevisas eller vederläggas [1] . Innan en exakt definition av en beräkningsbar funktion använde matematiker ofta den informella termen "effektivt beräkningsbar" för att beskriva funktioner som kan beräknas med papper-och-pennametoder.
Avhandlingen lades fram av Alonzo Church och Alan Turing i mitten av 1930-talet [2] [3] [4] [5] . Viktigt för många områden av vetenskap och vetenskapsfilosofi, inklusive matematisk logik , bevisteori , datavetenskap , cybernetik .
I termer av rekursionsteori är avhandlingen formulerad som en exakt beskrivning av den intuitiva föreställningen om beräkningsbarhet av en klass av generella rekursiva funktioner . Denna formulering kallas ofta för kyrkans tes [6] .
En mer allmän formulering gavs av Stephen Kleene , enligt vilken alla partiella (det vill säga inte nödvändigtvis definierade för alla argumentvärden) funktioner som är beräkningsbara av algoritmer är delvis rekursiva [7] .
När det gäller Turings beräkningsbarhet, anger avhandlingen att för alla algoritmiskt beräkningsbara funktioner finns det en Turing-maskin som beräknar dess värden [8] . Ibland framstår denna formulering som Turings avhandling . Med tanke på det faktum att klasserna av delvis beräkningsbara i betydelsen Turing och delvis rekursiva funktioner sammanfaller, kombineras påståendet till en enda Church-Turing-avhandling .
Senare formulerades andra praktiska versioner av uttalandet:
Ett viktigt problem för logiker på 1930-talet var upplösningsproblemet : om det finns en mekanisk procedur för att skilja matematiska sanningar från matematiska falskheter. Denna uppgift krävde att begreppet "algoritm" eller "effektiv beräkningsbarhet" fixerades, åtminstone för att starta uppgiften. [9] Från början till denna dag (från och med 2007) har det pågått en debatt: [10] huruvida begreppet "effektiv beräkningsbarhet" var (i) "ett axiom eller axiom" i ett axiomiskt system, eller ( ii) bara en definition som "identifierade" två eller flera meningar eller (iii) en empirisk hypotes som ska testas mot naturliga händelser eller (iv) eller helt enkelt en mening för argumentets skull (d.v.s. "avhandling").
Under loppet av att studera problemet introducerade Church och hans elev Stephen Kleene begreppet λ-definierbara funktioner , och de kunde bevisa att flera stora klasser av funktioner som ofta möttes i talteorin var λ-definierbara. [11] Diskussionen började när kyrkan föreslog Kurt Gödel att "effektivt beräkningsbara" funktioner skulle definieras som λ-definierbara funktioner. Gödel var dock inte övertygad och kallade förslaget "fullständigt otillfredsställande". [12] Ändå föreslog Gödel, i korrespondens med kyrkan, att axiomatisera begreppet "effektiv beräkningsbarhet"; I ett brev till Kleene och Church sa han det
Hans enda idé vid den tiden var att det kunde vara möjligt att definiera termen effektiv beräkningsbarhet som ett obestämt begrepp som en uppsättning axiom som förkroppsligar de allmänt accepterade egenskaperna hos det begreppet och sedan göra något utifrån det.
- [13]Men Gödel gav inga ytterligare instruktioner. Han föreslog endast rekursion , modifierad av Herbrands förslag, som Gödel skrev utförligt i sina föreläsningar i Princeton New Jersey 1934 (Kleene och Rosser transkriberade anteckningarna). Men han trodde inte att de två idéerna kunde definieras på ett tillfredsställande sätt "förutom heuristiskt". [fjorton]
Sedan var det nödvändigt att identifiera och bevisa likvärdigheten mellan de två begreppen effektiv beräkningsbarhet. Utrustad med λ-kalkyl och "allmän" rekursion producerade Stephen Kleene, med hjälp av Church och J. Barkley Rosser, bevis (1933, 1935) för att visa att de två kalkylerna är likvärdiga. Church modifierade därefter sina metoder för att inkludera användningen av Herbrand-Gödel-rekursion, och bevisade sedan (1936) att lösningsproblemet är obestämbart: det finns ingen generell algoritm som kan avgöra om en välformulerad formel är i "normal form". [femton]
Många år senare, i ett brev till Davis (cirka 1965), sa Gödel att "han var, under dessa [1934] föreläsningar, inte alls övertygad om att hans uppfattning om rekursion innefattade alla möjliga rekursioner." [16] År 1963 hade Gödel övergett Herbrand-Gödel-rekursionen och λ-kalkylen till förmån för Turing-maskinen som definitionen av "algoritm" eller "mekanisk procedur" eller "formellt system". [17]
Hypotes som leder till naturlag ? : I slutet av 1936 talades Alan Turings papper (som också bevisar att lösningsproblemet är olösligt) muntligt, men har ännu inte dykt upp i tryck. [18] Å andra sidan dök Emil Posts papper från 1936 upp och certifierades oberoende av Turings arbete. [19] Post höll inte mycket med kyrkans "identifiering" av effektiv beräkningsbarhet med λ-kalkyl och rekursion, och angav:
I själva verket, i kyrkans och andras arbete, anges denna identifikation mycket starkare än arbetshypotesen. Men att dölja denna identifikation som en definition ... gör oss blinda för behovet av ständig verifiering.
— [20]Snarare ansåg han begreppet "effektiv beräkningsbarhet" bara en "arbetshypotes" som genom induktiva resonemang kunde leda till en "naturlag" snarare än en "definition eller axiom". [21] Denna idé kritiserades "skarpt" av kyrkan. [22]
Sålunda avvisade Post också i sin uppsats från 1936 Kurt Gödels förslag till kyrkan 1934-5 att en tes skulle kunna uttryckas som ett axiom eller en uppsättning axiom. [13]
Turing lägger till en annan definition, Rosser likställer alla tre : Turings artikel (1936-37) "On Computable Numbers and Application to the Resolution Problem" dök upp på kort tid. [18] I den omdefinierade han begreppet "effektiv beräkningsbarhet" med introduktionen av hans a-maskiner (nu känd som den abstrakta beräkningsmodellen av en Turing-maskin). Och i en demonstrativ skiss som lades till som en "bilaga" till hans 1936-37 uppsats, visade Turing att klasserna av funktioner som definieras av λ-kalkylen och Turing-maskinerna är desamma. [23] Church insåg snabbt hur övertygande Turings analys var. I sin recension av Turings arbete gjorde han det klart att Turings föreställning gjorde "identifiering med effektivitet i den vanliga (inte explicit definierade) meningen omedelbart uppenbar". [24]
Några år senare (1939) föreslog Turing, som Church och Kleene hade gjort före honom, att hans formella definition av en mekanisk beräkningsagent var korrekt. [25] Sålunda 1939 hade både Church (1934) och Turing (1939) individuellt föreslagit att deras "formella system" var definitioner av "effektiv beräkningsbarhet"; [26] snarare än att formulera sina uttalanden som teser .
Rosser (1939) identifierade formellt tre begrepp som definitioner:
"Alla tre definitionerna är likvärdiga, så det spelar ingen roll vilken som används."Kleene föreslår kyrkans tes : det explicita uttrycket "tes" som används av Kleene lämnas här. I sin artikel "Rekursiva predikat och kvantifierare" från 1943 erbjöd Klin sin "TESIS I":
"Detta heuristiska faktum [allmänna rekursiva funktioner beräknas effektivt] ... fick kyrkan att formulera följande tes ( 22 ). Samma tes är implicit i Turings beskrivning av datorer ( 23 ). "TES I. Varje effektivt beräkningsbar funktion (effektivt avgörbart predikat) är i allmänhet [27] rekursiv [kursiv Kleene] "Eftersom en exakt matematisk definition av termen, effektivt beräkningsbar (effektivt avgörbar), skulle vara önskvärd, kan vi acceptera denna tes ... som definitionen av denna term ..." [28] ( 22 ) hänvisning till kyrkan 1936 ( 23 ) Turings länk 1936-7Kleene noterar vidare att:
”... avhandlingen har karaktären av en hypotes, en poäng som Post och Turing noterade ( 24 ). Om vi betraktar en avhandling och dess invers som en definition, så är en gissning en gissning om tillämpningen av den matematiska teorin som härrör från den definitionen. Det finns, som vi har föreslagit, ganska övertygande skäl för att acceptera denna hypotes.” [28] ( 24 ) Länk till Post 1936 av Post och Kyrkans formella definitioner i teorin om ordningstal , Fond. Matematik . vol 28 (1936) s. 11-21 (se ref. #2, Davis 1965 :286).