Sügav link, mis võrdsustab matemaatikatõestused ja arvutiprogrammid | Quanta ajakiri

Mõned teaduslikud avastused on olulised, sest need paljastavad midagi uut – näiteks DNA topeltspiraalset struktuuri või mustade aukude olemasolu. Mõned ilmutused on aga sügavad, sest näitavad, et kaks vana mõistet, mida kunagi peeti erinevaks, on tegelikult samad. Võtke James Clerk Maxwelli võrrandid, mis näitavad, et elekter ja magnetism on ühe nähtuse kaks aspekti või üldrelatiivsusteooria gravitatsiooni seos kõvera aegruumiga.

Curry-Howardi kirjavahetus teeb sama, kuid suuremas plaanis, ühendades mitte ainult ühe valdkonna eraldiseisvad mõisted, vaid terved erialad: Arvutiteadus ja matemaatiline loogika. Tuntud ka kui Curry-Howardi isomorfism (termin, mis tähendab, et kahe asja vahel on mingi üks-ühele vastavus), see loob seose matemaatiliste tõestuste ja arvutiprogrammide vahel.

Lihtsamalt öeldes eeldab Curry-Howardi kirjavahetus, et kaks arvutiteaduse mõistet (tüübid ja programmid) on võrdväärsed väidete ja tõestustega - loogika mõistetega.

Selle kirjavahetuse üks tagajärgi on see, et programmeerimine – mida sageli peetakse isiklikuks käsitööks – on tõstetud matemaatika idealiseeritud tasemele. Programmi kirjutamine ei ole lihtsalt "kodeerimine", sellest saab teoreemi tõestamise toiming. See vormistab programmeerimise toimingu ja annab võimaluse programmide õigsuse üle matemaatiliselt arutleda.

Kirjavahetus on nimetatud kahe teadlase järgi, kes selle iseseisvalt avastasid. 1934. aastal märkas matemaatik ja loogik Haskell Curry sarnasust matemaatika funktsioonide ja loogika implikatsiooniseoste vahel, mis väljendub kahe väite vahel "kui-siis"-lausetena.

Curry tähelepanekutest inspireerituna avastas matemaatiline loogik William Alvin Howard 1969. aastal sügavama seose arvutamise ja loogika vahel, näidates, et arvutiprogrammi käitamine sarnaneb paljuski loogilise tõestuse lihtsustamisega. Kui arvutiprogramm töötab, "hinnatakse" iga rida ühe väljundi saamiseks. Sarnaselt alustate tõestuses keeruliste väidetega, mida saate lihtsustada (nt kõrvaldades üleliigsed sammud või asendades keerukad avaldised lihtsamatega), kuni jõuate järeldusele – see on paljudest vahelausetest tuletatud tihedam ja sisutihedam väide. .

Kuigi see kirjeldus annab edasi üldise tähenduse kirjavahetusest, peame selle täielikuks mõistmiseks õppima natuke rohkem selle kohta, mida arvutiteadlased nimetavad "tüübiteooriaks".

Alustame kuulsast paradoksist: ühes külas elab juuksur, kes raseerib kõik mehed, kes end ei raseeri, ja ainult neid. Kas juuksur raseerib ennast? Kui vastus on jaatav, siis ta ei tohi end raseerida (sest ta ajab habet ainult neid mehi, kes ennast ei raseeri). Kui vastus on eitav, siis peab ta end raseerima (sest ta ajab raseerima kõik mehed, kes ennast ei raseeri). See on mitteametlik versioon paradoksist, mille Bertrand Russell avastas, kui ta püüdis luua matemaatika aluseid, kasutades kontseptsiooni, mida nimetatakse hulkadeks. See tähendab, et on võimatu määratleda hulka, mis sisaldab kõiki komplekte, mis ei sisalda iseennast, ilma et tekiks vastuolusid.

Russell näitas, et selle paradoksi vältimiseks võime kasutada "tüüpe". Jämedalt öeldes on need kategooriad, mille konkreetseid väärtusi nimetatakse objektideks. Näiteks kui on olemas tüüp nimega "Nat", mis tähendab naturaalarve, on selle objektid 1, 2, 3 jne. Teadlased kasutavad tavaliselt objekti tüübi tähistamiseks koolonit. Täisarvu tüüpi arvu 7 saab kirjutada kui "7: Integer". Teil võib olla funktsioon, mis võtab A-tüüpi objekti ja sülitab välja B-tüüpi objekti või ühendab A-tüüpi ja B-tüüpi objektide paari uueks tüübiks, mida nimetatakse "A × B".

Seetõttu on üks viis paradoksi lahendamiseks paigutada need tüübid hierarhiasse, nii et nad saaksid sisaldada ainult nendest „madalama taseme” elemente. Siis ei suuda tüüp ennast hoida, mis väldib paradoksi tekitavat enesereferentsiaalsust.

Tüüpideooria maailmas võib väite tõesuse tõestamine tunduda erinev sellest, millega oleme harjunud. Kui tahame tõestada, et täisarv 8 on paaris, tuleb näidata, et 8 on tõepoolest kindlat tüüpi objekt nimega "Paaris", kus liikmelisuse reegel jagub 2-ga. Pärast kontrollimist, et 8 on jagatav 2 järgi võime järeldada, et 8 on tõepoolest Even tüüpi "elanik".

Curry ja Howard näitasid, et tüübid on põhimõtteliselt samaväärsed loogiliste väidetega. Kui funktsioon "asustab" tüüpi – st kui suudate edukalt määratleda funktsiooni, mis on seda tüüpi objekt –, näitate tõhusalt, et vastav väide on tõene. Seega peavad funktsioonid, mis võtavad A-tüüpi sisendi ja annavad B-tüüpi väljundi, mida tähistatakse kui tüüp A → B, vastama implikatsioonile: "Kui A, siis B." Võtke näiteks ettepanek "Kui sajab vihma, siis on maa märg." Tüüpideoorias modelleeriks seda väidet funktsiooniga tüüp „Raining → GroundIsWet”. Erineva välimusega formuleeringud on tegelikult matemaatiliselt samad.

Nii abstraktselt kui see seos ka ei kõla, pole see mitte ainult muutnud seda, kuidas matemaatika ja arvutiteaduse praktikud oma tööst mõtlevad, vaid toonud kaasa ka mitmeid praktilisi rakendusi mõlemas valdkonnas. Arvutiteaduse jaoks annab see teoreetilise aluse tarkvara verifitseerimiseks, tarkvara õigsuse tagamise protsessiks. Soovitud käitumise kujundamisel loogiliste väidete alusel saavad programmeerijad matemaatiliselt tõestada, et programm käitub ootuspäraselt. See annab ka tugeva teoreetilise aluse võimsamate funktsionaalsete programmeerimiskeelte kujundamiseks.

Ja matemaatika jaoks on kirjavahetus viinud sünnini tõestusabilised, mida nimetatakse ka interaktiivseteks teoreemide tõestajateks. Need on tarkvaratööriistad, mis aitavad luua formaalseid tõendeid, nagu Coq ja Lean. Coqis on iga tõestuse samm sisuliselt programm ja tõestuse kehtivust kontrollitakse tüübikontrolli algoritmidega. Matemaatikud on kasutanud ka tõestusassistente - eriti Lahja teoreemi tõestaja — matemaatika formaliseerimine, mis hõlmab matemaatiliste mõistete, teoreemide ja tõestuste esitamist ranges arvutiga kontrollitavas vormingus. See võimaldab arvutite abil kontrollida matemaatika mõnikord mitteametlikku keelt.

Teadlased uurivad endiselt matemaatika ja programmeerimise vahelise seose tagajärgi. Algne Curry-Howardi kirjavahetus ühendab programmeerimise teatud loogikaga, mida nimetatakse intuitsionistlikuks loogikaks, kuid selgub, et sellistele ühendamistele võiks sobida ka mitut tüüpi loogikat.

"See, mis on juhtunud sajandi jooksul pärast Curry arusaama, on see, et me avastame üha rohkem juhtumeid, kus" loogiline süsteem X vastab arvutussüsteemile Y "," ütles ta. Michael Clarkson, Cornelli ülikooli arvutiteadlane. Teadlased on juba ühendanud programmeerimise teist tüüpi loogikatega, nagu lineaarne loogika, mis sisaldab mõistet "ressurss" ja modaalne loogika, mis käsitleb võimalikkuse ja vajaduse mõisteid.

Ja kuigi see kirjavahetus kannab Curry ja Howardi nime, pole nad sugugi ainsad, kes selle avastasid. See kinnitab kirjavahetuse põhiolemust: inimesed märkavad seda ikka ja jälle. "Näib, et arvutuste ja loogika vahel on sügav seos, ei ole juhuslik, " ütles Clarkson.