A Church-Turing tézis egy olyan hipotézis , amely az algoritmikus kiszámíthatóság intuitív fogalma és a részlegesen rekurzív függvény és a Turing-gépen kiszámítható függvény szigorúan formalizált fogalma közötti ekvivalenciát feltételez . Az algoritmikus kiszámíthatóság kezdeti koncepciójának intuitív természetéből adódóan ez a tézis az erről a fogalomról szóló ítélet jellegű, és nem lehet szigorúan bizonyítani vagy megcáfolni [1] . A kiszámítható függvény pontos meghatározása előtt a matematikusok gyakran használták a „hatékonyan kiszámítható” informális kifejezést a papír-ceruza módszerekkel kiszámítható függvények leírására.
A tézist Alonzo Church és Alan Turing terjesztette elő az 1930-as évek közepén [ 2] [3] [4] [5] . A tudomány és a tudományfilozófia számos területén nélkülözhetetlen, beleértve a matematikai logikát , bizonyítási elméletet , számítástechnikát és kibernetikát .
A rekurzióelmélet szempontjából a tézis a kiszámíthatóság intuitív fogalmának pontos leírása az általános rekurzív függvények osztályával . Ezt a megfogalmazást gyakran egyszerűen Church tézisének nevezik [6] .
Egy általánosabb megfogalmazást adott Stephen Kleene , amely szerint minden parciális (vagyis nem feltétlenül minden argumentumértékre definiált) függvény, amely algoritmusokkal kiszámítható, részben rekurzív [7] .
A Turing-számíthatóság tekintetében a dolgozat kimondja, hogy bármely algoritmikusan kiszámítható függvényhez létezik egy Turing-gép , amely kiszámítja annak értékeit [8] . Néha ez a megfogalmazás Turing téziseként jelenik meg . Tekintettel arra, hogy a turingi értelemben vett részlegesen kiszámítható és a részlegesen rekurzív függvények osztályai egybeesnek, az állítás egyetlen Church-Turing tézissé egyesül .
Később a kijelentés más gyakorlati változatai is megfogalmazódtak:
Az 1930-as években a logikusok egyik fontos problémája a felbontási probléma volt : létezik-e mechanikus eljárás a matematikai igazságok és a matematikai hamisságok elválasztására. Ehhez a feladathoz az "algoritmus" vagy a "hatékony kiszámíthatóság" fogalmának rögzítésére volt szükség, legalábbis a feladat elindításához. [9] A kezdetektől a mai napig (2007-től) folyamatos vita folyik: [10] hogy a „hatékony kiszámíthatóság” fogalma (i) „egy axióma vagy axiómák” egy axiomatikus rendszerben, vagy ( ii) csak egy definíció, amely "azonosított" két vagy több mondatot, vagy (iii) egy empirikus hipotézist, amelyet a természeti eseményekkel szemben kell tesztelni, vagy (iv) vagy egyszerűen egy mondat az érvelés kedvéért (azaz "tézis").
A probléma tanulmányozása során Church és tanítványa, Stephen Kleene bevezette a λ-definiálható függvények fogalmát , és be tudták bizonyítani, hogy a számelméletben gyakran előforduló nagy függvényosztályok λ-definiálhatóak. [11] A vita akkor kezdődött, amikor Church azt javasolta Kurt Gödelnek , hogy a „hatékonyan kiszámítható” függvényeket λ-ban definiálható függvényekként határozzák meg. Gödelt azonban nem győzte meg, és "teljesen kielégítőnek" nevezte a javaslatot. [12] Mindazonáltal Gödel Church-lel folytatott levelezésben azt javasolta, hogy axiomatizálják a „hatékony kiszámíthatóság” fogalmát; Kleene és Churchnek írt levelében ezt mondta
Akkoriban csak az volt a gondolata, hogy lehetséges lenne a hatékony számítási képesség fogalmát határozatlan fogalomként definiálni, mint olyan axiómák halmazát, amelyek megtestesítik az adott fogalom általánosan elfogadott tulajdonságait, majd ezek alapján tesznek valamit.
- [13]De Gödel nem adott további utasítást. Csak a rekurziót javasolta , amelyet Herbrand javaslata módosított, amelyet Gödel hosszasan írt 1934-es Princeton New Jersey-i előadásaiban (Kleene és Rosser átírta a jegyzeteket). De nem gondolta, hogy a két elképzelést „heurisztikusan” nem lehet kielégítően meghatározni. [tizennégy]
Ezután azonosítani és igazolni kellett az effektív számíthatóság két fogalmának egyenértékűségét . Stephen Kleene a λ-kalkulussal és az "általános" rekurzióval felszerelt Church és J. Barkley Rosser segítségével bizonyítékokat készített (1933, 1935) annak bizonyítására, hogy a két kalkulus egyenértékű. Church ezt követően módosította módszereit, hogy magában foglalja a Herbrand-Gödel rekurzió használatát, majd bebizonyította (1936), hogy a felbontási probléma eldönthetetlen: nincs olyan általános algoritmus, amely meghatározná, hogy egy jól megfogalmazott képlet „normál formában”-e. [tizenöt]
Sok évvel később, Davisnek írt levelében (körülbelül 1965) Gödel azt mondta, hogy "az 1934-es előadások során egyáltalán nem volt meggyőződve arról, hogy a rekurzió fogalma minden lehetséges rekurziót magában foglal." [16] 1963-ra Gödel elhagyta a Herbrand-Gödel rekurziót és a λ-számítást, és a Turing-gépet választotta az "algoritmus" vagy "mechanikai eljárás" vagy "formális rendszer" definíciójaként. [17]
A természetjoghoz vezető hipotézis ? : 1936 végén Alan Turing dolgozata (amely szintén azt bizonyítja, hogy a felbontási probléma megoldhatatlan) szóban hangzott el, de nyomtatásban még nem jelent meg. [18] Másrészt Emil Post 1936-os dolgozata Turing munkáitól függetlenül jelent meg, és azt hitelesítették. [19] Post határozottan nem értett egyet azzal, hogy Church „azonosítja” a λ-számítással és a rekurzióval való hatékony kiszámíthatóságot, és kijelentette:
Valójában Church és mások munkáiban ez az azonosulás sokkal erősebben érvényesül, mint a munkahipotézis. De ha ezt az azonosítást definíciónak álcázzuk... elvakít bennünket az állandó ellenőrzés szükségességétől.
— [20]A „hatékony kiszámíthatóság” fogalmát inkább csak „munkahipotézisnek” tartotta, amely az induktív érveléssel „természettörvényhez” vezethet, nem pedig „definícióhoz vagy axiómához”. [21] Ezt az ötletet Church "élesen" bírálta. [22]
Így Post 1936-os dolgozatában szintén elutasította Kurt Gödelnek Churchnek 1934–1935-ben tett javaslatát, miszerint egy tézist axiómaként vagy axiómahalmazként lehetne kifejezni. [13]
Turing egy másik definíciót ad hozzá, Rosser mindhármat egyenlővé teszi : Turing (1936-37) „A kiszámítható számokról és a felbontási probléma alkalmazásáról” című tanulmánya rövid időn belül megjelent. [18] Ebben újradefiniálta a "hatékony kiszámíthatóság" fogalmát a-gépei (ma a Turing-gép absztrakt számítási modelljeként ismert) bevezetésével. Az 1936–1937-es dolgozatához „Függelékként” mellékelt demonstratív vázlatban pedig Turing megmutatta, hogy a λ-számítás és a Turing-gép által meghatározott függvényosztályok megegyeznek. [23] Church hamar rájött, mennyire meggyőző Turing elemzése. Turing munkájáról szóló áttekintésében világossá tette, hogy Turing elképzelése „azonnal nyilvánvalóvá tette a hatékonysággal való azonosulást a szokásos (nem kifejezetten meghatározott) értelemben”. [24]
Néhány évvel később (1939) Turing azt javasolta, ahogy Church és Kleene is tették előtte, hogy a mechanikus számítási ágens formális meghatározása helyes. [25] Így 1939-re Church (1934) és Turing (1939) is egyénileg azt javasolta, hogy „formális rendszereik” a „hatékony kiszámíthatóság” definíciói ; [26] ahelyett, hogy állításaikat tézisként fogalmaznák meg .
Rosser (1939) hivatalosan három fogalmat azonosított definícióként:
"Mindhárom definíció egyenértékű, így nem mindegy, hogy melyiket használják."Kleene Church tézisét javasolja : itt marad a Kleene által használt explicit "tézis" kifejezés. „Rekurzív predikátumok és kvantorok” című 1943-as cikkében Klin az „I. TÉZISÉT” ajánlotta fel:
"Ez a heurisztikus tény [az általános rekurzív függvényeket hatékonyan számítják ki] ... késztette Church-ot a következő tézis megfogalmazására ( 22 ). Ugyanez a tézis implicit módon benne van Turing számítógépek leírásában ( 23 ). "TÉZIS I. Minden hatékonyan kiszámítható függvény (hatékonyan eldönthető predikátum) általában [27] rekurzív [dőlt betűs Kleene] "Mivel a fogalom pontos matematikai definíciója, hatékonyan kiszámítható (effektíve eldönthető) lenne kívánatos, elfogadhatjuk ezt a tézist ... e fogalom definíciójaként ..." [28] ( 22 ) utalás a Church 1936-ra ( 23 ) Turing linkje 1936-7Kleene megjegyzi továbbá, hogy:
„… a tézis hipotézis jelleggel bír, erre utalt Post és Turing ( 24 ). Ha egy tézist és annak inverzét tekintjük definíciónak, akkor a sejtés az abból a definícióból levezetett matematikai elmélet alkalmazására vonatkozó sejtés. Amint azt javasoltuk, meglehetősen meggyőző indokok szólnak ennek a hipotézisnek az elfogadására.” [28] ( 24 ) Link a Post 1936-os bejegyzéséhez és a Church's Formális definíciókhoz a sorszámelméletben , Fund. Matek . 28. kötet (1936), 11-21. oldal (lásd 2. hivatkozás, Davis 1965 :286).