Church-Turing-afhandlingen er en hypotese , der postulerer en ækvivalens mellem den intuitive forestilling om algoritmisk beregnelighed og de strengt formaliserede forestillinger om en delvist rekursiv funktion og en funktion, der kan beregnes på en Turing-maskine . På grund af den intuitive karakter af det indledende begreb om algoritmisk beregnelighed, har denne afhandling karakter af en bedømmelse af dette koncept og kan ikke strengt bevises eller afkræftes [1] . Før en præcis definition af en beregnelig funktion brugte matematikere ofte det uformelle udtryk "effektivt beregnelig" til at beskrive funktioner, der kan beregnes ved hjælp af papir-og-blyant-metoder.
Specialet blev fremsat af Alonzo Church og Alan Turing i midten af 1930'erne [2] [3] [4] [5] . Væsentligt for mange områder af videnskab og videnskabsfilosofi, herunder matematisk logik , bevisteori , datalogi , kybernetik .
Med hensyn til rekursionsteori er afhandlingen formuleret som en præcis beskrivelse af den intuitive forestilling om beregnelighed af en klasse af generelle rekursive funktioner . Denne formulering omtales ofte som blot Kirkens tese [6] .
En mere generel formulering blev givet af Stephen Kleene , ifølge hvilken alle partielle (det vil sige ikke nødvendigvis definerede for alle argumentværdier) funktioner, der kan beregnes af algoritmer, er delvist rekursive [7] .
Med hensyn til Turing-beregnelighed, fastslår afhandlingen, at for enhver algoritmisk beregnelig funktion er der en Turing-maskine , der beregner dens værdier [8] . Nogle gange fremstår denne formulering som Turings afhandling . I lyset af det faktum, at klasserne af delvist beregnelige i betydningen Turing og delvist rekursive funktioner er sammenfaldende, er udsagnet kombineret til en enkelt Church-Turing-afhandling .
Senere blev andre praktiske versioner af udtalelsen formuleret:
Et vigtigt problem for logikere i 1930'erne var løsningsproblemet : om der er en mekanisk procedure til at adskille matematiske sandheder fra matematiske falskheder. Denne opgave krævede, at begrebet "algoritme" eller "effektiv beregnelighed" blev fastsat, i det mindste for at starte opgaven. [9] Fra begyndelsen til i dag (fra 2007) har der været en løbende debat: [10] om begrebet "effektiv beregnelighed" var (i) "et aksiom eller aksiomer" i et aksiomatisk system, eller ( ii) blot en definition, der "identificerede" to eller flere sætninger eller (iii) en empirisk hypotese, der skal testes mod naturlige begivenheder eller (iv) eller blot en sætning for argumentets skyld (dvs. "tese").
I løbet af undersøgelsen af problemet introducerede Church og hans elev Stephen Kleene begrebet λ-definerbare funktioner , og de var i stand til at bevise, at flere store klasser af funktioner, der ofte stødes på i talteorien, var λ-definerbare. [11] Diskussionen begyndte, da Kirken foreslog Kurt Gödel , at "effektivt beregnelige" funktioner defineres som λ-definerbare funktioner. Gödel var dog ikke overbevist og kaldte forslaget "fuldstændig utilfredsstillende". [12] Ikke desto mindre foreslog Gödel i korrespondance med Church at aksiomatisere begrebet "effektiv beregningsevne"; I et brev til Kleene og Kirke sagde han det
Hans eneste idé på det tidspunkt var, at det kunne være muligt at definere begrebet effektiv beregnelighed som et ubestemt begreb som et sæt af aksiomer, der legemliggør de generelt accepterede egenskaber ved dette begreb og derefter gøre noget baseret på det.
- [13]Men Gödel gav ingen yderligere instruktioner. Han foreslog kun rekursion , modificeret af Herbrands forslag, som Gödel skrev udførligt i sine Princeton New Jersey -forelæsninger fra 1934 (Kleene og Rosser transskriberede noterne). Men han mente ikke, at de to ideer kunne defineres tilfredsstillende "undtagen heuristisk". [fjorten]
Derefter var det nødvendigt at identificere og bevise ækvivalensen af de to begreber om effektiv beregnelighed. Udstyret med λ-regningen og den "generelle" rekursion fremstillede Stephen Kleene med hjælp fra Church og J. Barkley Rosser beviser (1933, 1935) for at vise, at de to kalkulationer er ækvivalente. Church modificerede efterfølgende sine metoder til at omfatte brugen af Herbrand-Gödel rekursion og beviste derefter (1936), at løsningsproblemet er uafgørligt: der er ingen generel algoritme, der kan afgøre, om en velformuleret formel er i "normal form". [femten]
Mange år senere, i et brev til Davis (ca. 1965), sagde Gödel, at "han var under disse [1934] forelæsninger slet ikke overbevist om, at hans begreb om rekursion omfattede alle mulige rekursioner." [16] I 1963 havde Gödel opgivet Herbrand-Gödel rekursion og λ-regning til fordel for Turing-maskinen som definition af "algoritme" eller "mekanisk procedure" eller "formelt system". [17]
Hypotese, der fører til naturlov ? : I slutningen af 1936 blev Alan Turings papir (som også beviser, at løsningsproblemet er uløseligt) talt mundtligt, men er endnu ikke udkommet på tryk. [18] På den anden side udkom Emil Posts papir fra 1936 og blev certificeret uafhængigt af Turings arbejde. [19] Post var meget uenig i Kirkens "identifikation" af effektiv beregnelighed med λ-regning og rekursion, idet den sagde:
Faktisk er denne identifikation i Kirkens og andres arbejde fremført meget stærkere end arbejdshypotesen. Men at skjule denne identifikation som en definition ... blinder os for behovet for konstant verifikation.
— [20]Han betragtede snarere begrebet "effektiv beregnelighed" som en "arbejdshypotese", der ved induktiv ræsonnement kunne føre til en "naturlov" snarere end en "definition eller aksiom". [21] Denne idé blev "skarpt" kritiseret af Church. [22]
Således afviste Post i sit papir fra 1936 også Kurt Gödels forslag til Kirken i 1934-5 om, at en tese kunne udtrykkes som et aksiom eller et sæt af aksiomer. [13]
Turing tilføjer en anden definition, Rosser sidestiller alle tre : Turings papir (1936-37) "On Computable Numbers and Application to the Resolution Problem" udkom på kort tid. [18] I den omdefinerede han begrebet "effektiv beregningsevne" med introduktionen af hans a-maskiner (nu kendt som den abstrakte beregningsmodel af en Turing-maskine). Og i en demonstrativ skitse tilføjet som et "tillæg" til hans papir fra 1936-37, viste Turing, at klasserne af funktioner defineret af λ-regningen og Turing-maskinerne er de samme. [23] Church indså hurtigt, hvor overbevisende Turings analyse var. I sin gennemgang af Turings arbejde gjorde han det klart, at Turings forestilling gjorde "identifikation med effektivitet i den sædvanlige (ikke eksplicit definerede) betydning umiddelbart indlysende". [24]
Et par år senere (1939) foreslog Turing, som Church og Kleene havde gjort før ham, at hans formelle definition af en mekanisk beregningsagent var korrekt. [25] Således havde både Church (1934) og Turing (1939) i 1939 individuelt foreslået, at deres "formelle systemer" var definitioner af "effektiv beregningsevne"; [26] i stedet for at formulere deres udsagn som teser .
Rosser (1939) identificerede formelt tre begreber som definitioner:
"Alle tre definitioner er ækvivalente, så det er lige meget, hvilken der bruges."Kleene foreslår Kirkens tese : det eksplicitte udtryk "tese" brugt af Kleene er tilbage her. I sit papir fra 1943 "Recursive Predicates and Quantifiers" tilbød Klin sin "TESES I":
"Denne heuristiske kendsgerning [generelle rekursive funktioner beregnes effektivt] ... fik Kirken til at formulere følgende tese ( 22 ). Den samme tese er implicit i Turings beskrivelse af computere ( 23 ). "TESE I. Enhver effektivt beregnelig funktion (effektivt afgøreligt prædikat) er generelt [27] rekursiv [kursiv Kleene] "Da en præcis matematisk definition af begrebet, der kan beregnes (effektivt afgøres), ville være ønskelig, kan vi acceptere denne afhandling ... som definitionen af dette begreb ..." [28] ( 22 ) henvisning til Kirken 1936 ( 23 ) Turings forbindelse 1936-7Kleene bemærker endvidere, at:
"... afhandlingen har karakter af en hypotese, en pointe bemærket af Post og Turing ( 24 ). Hvis vi betragter en afhandling og dens inverse som en definition, så er en formodning en formodning om anvendelsen af den matematiske teori afledt af denne definition. Der er, som vi har foreslået, ganske overbevisende grunde til at acceptere denne hypotese." [28] ( 24 ) Link til Post 1936 af Post og kirkes formelle definitioner i teorien om ordenstal , Fond. Matematik . bind 28 (1936) s. 11-21 (se ref. #2, Davis 1965 :286).