Church-Turingin teesi on hypoteesi , joka olettaa ekvivalenssia intuitiivisen algoritmisen laskettavuuden käsitteen ja osittain rekursiivisen funktion ja Turingin koneella laskettavissa olevan funktion tiukasti formalisoitujen käsitteiden välillä . Alkuperäisen algoritmisen laskettavuuden käsitteen intuitiivisuudesta johtuen tämä opinnäytetyö on luonteeltaan tätä käsitettä koskeva tuomio, eikä sitä voida tiukasti todistaa tai kumota [1] . Ennen laskettavan funktion tarkkaa määritelmää matemaatikot käyttivät usein epävirallista termiä "tehokkaasti laskettava" kuvaamaan funktioita, jotka voidaan laskea paperi- ja kynämenetelmillä.
Väitöskirjan esittivät Alonzo Church ja Alan Turing 1930-luvun puolivälissä [ 2] [3] [4] [5] . Olennainen monille tieteen ja tiedefilosofian aloille, mukaan lukien matemaattinen logiikka , todistusteoria , tietojenkäsittelytiede ja kybernetiikka .
Rekursioteorian kannalta opinnäytetyö on muotoiltu tarkaksi kuvaukseksi intuitiivisesta laskettavuuden käsitteestä yleisten rekursiivisten funktioiden luokassa . Tätä muotoilua kutsutaan usein yksinkertaisesti kirkon teesiksi [6] .
Stephen Kleene antoi yleisemmän muotoilun , jonka mukaan kaikki algoritmien laskettavissa olevat osittaiset (eli eivät välttämättä ole määritelty kaikille argumenttiarvoille) funktiot ovat osittain rekursiivisia [7] .
Turingin laskettavuuden osalta väitöskirjassa todetaan, että mille tahansa algoritmisesti laskettavalle funktiolle on olemassa Turingin kone , joka laskee sen arvot [8] . Joskus tämä muotoilu esiintyy Turingin teesinä . Ottaen huomioon, että Turingin merkityksessä osittain laskettavien ja osittain rekursiivisten funktioiden luokat ovat yhteneväisiä, lause yhdistetään yhdeksi Church-Turingin teesiksi .
Myöhemmin lausunnosta muotoiltiin muita käytännön versioita:
Eräs 1930-luvun loogikoiden tärkeä ongelma oli resoluutioongelma : onko olemassa mekaanista menetelmää matemaattisten totuuksien erottamiseksi matemaattisista vääristymistä. Tämä tehtävä edellytti, että käsite "algoritmi" tai "tehokas laskettavuus" korjataan ainakin tehtävän aloittamiseksi. [9] Alusta lähtien tähän päivään (vuodesta 2007 lähtien) on käyty jatkuvaa keskustelua: [10] oliko "tehokkaan laskettavuuden" käsite (i) " aksiooma tai aksioomit" aksiomaattisessa järjestelmässä vai ( ii) vain määritelmä, joka "tunnisti" kaksi tai useampia lauseita tai (iii) empiirinen hypoteesi, joka testataan luonnontapahtumia vastaan tai (iv) tai yksinkertaisesti lause argumentin vuoksi (eli "teesi").
Ongelmaa tutkiessaan Church ja hänen oppilaansa Stephen Kleene esittelivät λ-määriteltävissä olevien funktioiden käsitteen ja pystyivät todistamaan, että useat lukuteoriassa usein kohtaavat suuret funktioluokat olivat λ-määriteltävissä. [11] Keskustelu alkoi, kun Church ehdotti Kurt Gödelille , että "tehokkaasti laskettavat" funktiot määritellään λ-määritettäviksi funktioiksi. Gödel ei kuitenkaan ollut vakuuttunut ja kutsui ehdotusta "täysin epätyydyttäväksi". [12] Siitä huolimatta Gödel ehdotti kirjeenvaihdossa Churchin kanssa "tehokkaan laskettavuuden" käsitteen aksiomatisoimista ; Kirjeessä Kleenelle ja Churchille hän sanoi sen
Hänen ainoa ajatuksensa tuolloin oli, että termi tehokas laskettavuus voisi olla mahdollista määritellä määrittelemättömäksi käsitteeksi aksioomien joukoksi, jotka ilmentävät käsitteen yleisesti hyväksyttyjä ominaisuuksia ja sitten tekevät jotain sen perusteella.
- [13]Mutta Gödel ei antanut muita ohjeita. Hän ehdotti vain rekursiota , jota oli muokattu Herbrandin ehdotuksella, jonka Gödel kirjoitti pitkästi vuoden 1934 Princeton New Jersey -luennoissaan (Kleene ja Rosser litteroivat muistiinpanot). Mutta hän ei uskonut, että nämä kaksi ideaa voitaisiin määritellä tyydyttävästi "paitsi heuristisesti". [neljätoista]
Sitten oli tarpeen tunnistaa ja todistaa kahden tehokkaan laskettavuuden käsitteen vastaavuus . Varustettuna λ-laskeella ja "yleisellä" rekursiolla Stephen Kleene, Churchin ja J. Barkley Rosserin avulla, tuotti todisteita (1933, 1935) osoittaakseen, että nämä kaksi laskentaa ovat samanarvoisia. Myöhemmin Church muutti menetelmiään sisällyttämään Herbrand-Gödel-rekursion käytön, ja sitten osoitti (1936), että resoluutioongelma on ratkaisematon : ei ole olemassa yleistä algoritmia, joka voisi määrittää, onko hyvin muotoiltu kaava "normaalissa muodossa". [viisitoista]
Monia vuosia myöhemmin, kirjeessä Davisille (noin 1965), Gödel sanoi, että "hän ei ollut näiden [1934] luentojen aikana ollenkaan vakuuttunut siitä, että hänen käsitteensä rekursiosta sisälsi kaikki mahdolliset rekursiot." [16] Vuoteen 1963 mennessä Gödel oli hylännyt Herbrand-Gödel-rekursion ja λ-laskennan Turingin koneen sijaan "algoritmin" tai "mekaanisen menettelyn" tai "muodollisen järjestelmän" määritelmänä. [17]
Luonnonlakiin johtava hypoteesi ? : Vuoden 1936 lopulla Alan Turingin artikkeli (joka myös osoittaa, että resoluutioongelma on ratkaisematon) puhuttiin suullisesti, mutta se ei ole vielä ilmestynyt painettuna. [18] Toisaalta Emil Postin vuoden 1936 paperi ilmestyi ja se sertifioitiin Turingin työstä riippumatta. [19] Post oli jyrkästi eri mieltä siitä, että Church "tunnisti" tehokkaan laskettavuuden λ-laskennan ja rekursion avulla, ja totesi:
Itse asiassa kirkon ja muiden työssä tämä samaistuminen ilmaistaan paljon vahvemmin kuin työhypoteesi. Mutta tämän tunnistamisen naamioiminen määritelmäksi... sokaisee meidät jatkuvan todentamisen tarpeelta.
— [20]Pikemminkin hän piti käsitettä "tehokas laskettavuus" vain "työhypoteesina", joka voisi johtaa induktiivisen päättelyn avulla "luonnonlakiin" "määritelmän tai aksiooman" sijaan. [21] Kirkko kritisoi tätä ajatusta "jyrkästi". [22]
Siten Post hylkäsi vuoden 1936 kirjoituksessaan myös Kurt Gödelin ehdotuksen Churchille vuosina 1934-1935, että teesi voitaisiin ilmaista aksioomana tai aksioomijoukona. [13]
Turing lisää toisen määritelmän, Rosser rinnastaa kaikki kolme : Turingin paperi (1936-37) "On Computable Numbers and Application to the Resolution Problem" ilmestyi lyhyessä ajassa. [18] Siinä hän määritteli uudelleen käsitteen "tehokas laskettavuus" ottamalla käyttöön a-koneensa (tunnetaan nykyään Turingin koneen abstraktina laskennallisena mallina). Ja demonstratiivisessa luonnoksessa, joka lisättiin "Liitteenä" hänen vuosien 1936-37 kirjoitukseensa, Turing osoitti, että λ-laskennan ja Turingin koneiden määrittämät funktioluokat ovat samat. [23] Church ymmärsi nopeasti, kuinka vakuuttava Turingin analyysi oli. Katsauksessaan Turingin työstä hän teki selväksi, että Turingin käsitys teki "tehokkuuden tunnistamisen tavanomaisessa (ei eksplisiittisesti määritellyssä) merkityksessä välittömästi ilmeiseksi". [24]
Muutamaa vuotta myöhemmin (1939) Turing ehdotti, kuten Church ja Kleene olivat tehneet ennen häntä, että hänen muodollinen määritelmänsä mekaanisesta laskennallisesta agentista oli oikea. [25] Siten vuoteen 1939 mennessä sekä Church (1934) että Turing (1939) ehdottivat erikseen, että heidän "muodolliset järjestelmänsä" ovat "tehokkaan laskettavuuden" määritelmiä ; [26] sen sijaan, että muotoilisivat lausuntonsa teeseiksi .
Rosser (1939) määritteli muodollisesti kolme käsitettä:
"Kaikki kolme määritelmää ovat samanarvoisia, joten sillä ei ole väliä kumpaa käytetään."Kleene ehdottaa Churchin teesiä : Kleenen käyttämä eksplisiittinen ilmaus "teesi" on jätetty tähän. Vuoden 1943 artikkelissaan "Recursive Predicates and Quantifiers" Klin tarjosi "TEESI I":
"Tämä heuristinen tosiasia [yleiset rekursiiviset funktiot lasketaan tehokkaasti] ... sai Churchin muotoilemaan seuraavan teesin ( 22 ). Sama teesi sisältyy implisiittisesti Turingin kuvaukseen tietokoneista ( 23 ). "TEESI I. Jokainen tehokkaasti laskettava funktio (tehokkaasti päätettävissä oleva predikaatti) on yleensä [27] rekursiivinen [kursiivi Kleene] "Koska termin tarkka matemaattinen määritelmä, tehokkaasti laskettava (tehokkaasti päätettävissä) olisi toivottavaa, voimme hyväksyä tämän opinnäytetyön ... tämän termin määritelmäksi ..." [28] ( 22 ) viittaus kirkkoon 1936 ( 23 ) Turingin linkki 1936-7Kleene huomauttaa lisäksi, että:
”… väitöskirjalla on hypoteesin luonne, jonka huomauttavat Post ja Turing ( 24 ). Jos pidämme teesiä ja sen käänteistä määritelmänä, niin olettamus on olettamus siitä määritelmästä johdetun matemaattisen teorian soveltamisesta. Kuten olemme ehdottaneet, on melko vakuuttavia perusteita hyväksyä tämä hypoteesi." [28] ( 24 ) Linkki Post 1936 -julkaisuun Post and Church's Formal määritelmät järjestyslukujen teoriassa , Fund. Matematiikka . osa 28 (1936) s. 11-21 (katso viite #2, Davis 1965 :286).