Syvälinkki, joka rinnastaa matematiikan todisteet ja tietokoneohjelmat | Quanta-lehti

Jotkut tieteelliset löydöt ovat tärkeitä, koska ne paljastavat jotain uutta – esimerkiksi DNA:n kaksoiskierteisen rakenteen tai mustien aukkojen olemassaolon. Jotkut paljastukset ovat kuitenkin syvällisiä, koska ne osoittavat, että kaksi vanhaa käsitettä, jotka kerran pidettiin erillisinä, ovat itse asiassa samat. Otetaan James Clerk Maxwellin yhtälöt, jotka osoittavat, että sähkö ja magnetismi ovat yhden ilmiön kaksi aspektia, tai yleisen suhteellisuusteorian painovoiman ja kaarevan aika-avaruuden yhdistäminen.

Curry-Howard-kirjeenvaihto tekee saman, mutta laajemmassa mittakaavassa, ei yhdistä vain yksittäisiä käsitteitä yhden alan sisällä, vaan kokonaisia ​​tieteenaloja: Tietojenkäsittelyoppi ja matemaattinen logiikka. Tunnetaan myös nimellä Curry-Howard-isomorfismi (termi tarkoittaa, että kahden asian välillä on jonkinlainen yksitellen vastaavuus), se muodostaa yhteyden matemaattisten todisteiden ja tietokoneohjelmien välille.

Yksinkertaisesti sanottuna Curry-Howard-kirjeenvaihto esittää, että kaksi tietojenkäsittelytieteen käsitettä (tyypit ja ohjelmat) vastaavat ehdotuksia ja todisteita - logiikan käsitteitä.

Yksi tämän kirjeenvaihdon seurauksista on se, että ohjelmointi - jota usein pidetään henkilökohtaisena taiteena - on kohotettu matematiikan idealisoidulle tasolle. Ohjelman kirjoittaminen ei ole vain "koodausta", siitä tulee lauseen todistaminen. Tämä formalisoi ohjelmoinnin ja tarjoaa tapoja arvioida matemaattisesti ohjelmien oikeellisuutta.

Kirjeenvaihto on nimetty kahden tutkijan mukaan, jotka löysivät sen itsenäisesti. Vuonna 1934 matemaatikko ja loogikko Haskell Curry huomasi samankaltaisuuden matematiikan funktioiden ja logiikan implikaatiosuhteen välillä, joka on "jos-niin"-lauseiden muodossa kahden väitteen välillä.

Curryn havainnon innoittamana matemaattinen logiikka William Alvin Howard löysi syvemmän yhteyden laskennan ja logiikan välillä vuonna 1969, mikä osoitti, että tietokoneohjelman käyttäminen on paljon kuin loogisen todisteen yksinkertaistamista. Kun tietokoneohjelma suoritetaan, jokainen rivi "evaluoidaan", jolloin saadaan yksi tulos. Vastaavasti todistuksessa aloitat monimutkaisilla lauseilla, joita voit yksinkertaistaa (esimerkiksi poistamalla tarpeettomat vaiheet tai korvaamalla monimutkaiset lausekkeet yksinkertaisemmilla), kunnes päädyt johtopäätökseen - tiivistetympään ja ytimekkäämpään lauseeseen, joka on johdettu monista välilauseista. .

Vaikka tämä kuvaus välittää yleiskuvan vastaavuudesta, ymmärtääksemme sen täysin, meidän on opittava hieman enemmän siitä, mitä tietojenkäsittelytieteilijät kutsuvat "tyyppiteoriaksi".

Aloitetaan kuuluisasta paradoksista: kylässä asuu parturi, joka ajaa parranajon kaikki miehet, jotka eivät ajele itseään, ja vain heidät. Ajeleeko parturi itsensä? Jos vastaus on kyllä, hän ei saa ajella itseään (koska hän ajaa vain miehiä, jotka eivät ajele itseään). Jos vastaus on ei, hänen on ajettava itsensä (koska hän ajaa kaikki miehet, jotka eivät ajele itse). Tämä on epävirallinen versio paradoksista, jonka Bertrand Russell löysi yrittäessään luoda matematiikan perusteita käyttämällä käsitettä nimeltä joukot. Eli on mahdotonta määritellä joukkoa, joka sisältää kaikki joukot, jotka eivät sisällä itseään ilman ristiriitoja.

Russell osoitti tämän paradoksin välttämiseksi, että voimme käyttää "tyyppejä". Karkeasti sanottuna nämä ovat luokkia, joiden tiettyjä arvoja kutsutaan objekteiksi. Jos esimerkiksi on olemassa tyyppi nimeltä "Nat", joka tarkoittaa luonnollisia lukuja, sen objektit ovat 1, 2, 3 ja niin edelleen. Tutkijat käyttävät tyypillisesti kaksoispistettä osoittamaan kohteen tyyppiä. Kokonaislukutyyppinen luku 7 voidaan kirjoittaa muodossa "7: Integer". Sinulla voi olla toiminto, joka ottaa A-tyypin objektin ja sylkee B-tyypin objektin, tai toiminto, joka yhdistää A-tyypin ja B-tyypin objektiparin uudeksi tyypiksi nimeltä "A × B".

Yksi tapa ratkaista paradoksi on siksi asettaa nämä tyypit hierarkiaan, jotta ne voivat sisältää vain "alemman tason" elementtejä kuin he itse. Silloin tyyppi ei voi pitää itsensä sisällään, mikä välttää paradoksin luovan itseviittauksen.

Tyyppiteorian maailmassa väitteen oikeellisuuden todistaminen voi näyttää erilaiselta kuin mihin olemme tottuneet. Jos haluamme todistaa, että kokonaisluku 8 on parillinen, on kyse siitä, että 8 on todellakin tietyn tyyppinen "Parillinen" objekti, jossa jäsenyyden sääntö on jaollinen kahdella. Sen jälkeen kun on varmistettu, että 2 on jaollinen 8:lla voimme päätellä, että 2 on todellakin Even-tyyppinen "asukas".

Curry ja Howard osoittivat, että tyypit vastaavat pohjimmiltaan loogisia ehdotuksia. Kun funktio "astuu" tyyppiin - eli kun voit onnistuneesti määrittää funktion, joka on kyseisen tyypin objekti - osoitat tehokkaasti, että vastaava väite on tosi. Joten funktioiden, jotka ottavat tyypin A syötteen ja antavat tyypin B lähdön, joka on merkitty tyypiksi A → B, on vastattava implikaatiota: "Jos A, niin B." Otetaan esimerkiksi lause "Jos sataa, niin maa on märkä". Tyyppiteoriassa tämä ehdotus mallinnettaisiin funktiolla, jonka tyyppi on "Raining → GroundIsWet". Erinäköiset formulaatiot ovat itse asiassa matemaattisesti samoja.

Niin abstraktilta kuin tämä yhteys kuulostaakin, se ei ole vain muuttanut sitä, miten matematiikan ja tietojenkäsittelytieteen harjoittajat ajattelevat työstään, vaan myös johtanut useisiin käytännön sovelluksiin molemmilla aloilla. Tietojenkäsittelytieteelle se tarjoaa teoreettisen perustan ohjelmistojen todentamiselle, prosessille, jolla varmistetaan ohjelmiston oikeellisuus. Kehystämällä halutut käyttäytymiset loogisten ehdotusten perusteella ohjelmoijat voivat todistaa matemaattisesti, että ohjelma käyttäytyy odotetulla tavalla. Se tarjoaa myös vahvan teoreettisen perustan tehokkaampien toiminnallisten ohjelmointikielten suunnittelulle.

Ja matematiikan osalta kirjeenvaihto on johtanut syntymiseen todistusavustajat, jota kutsutaan myös interaktiivisiksi lauseiden todistajiksi. Nämä ovat ohjelmistotyökaluja, jotka auttavat muodostamaan muodollisia todisteita, kuten Coq ja Lean. Coqissa jokainen todistuksen vaihe on pohjimmiltaan ohjelma ja todistuksen kelpoisuus tarkistetaan tyyppitarkistusalgoritmeilla. Matemaatikot ovat myös käyttäneet todistusapulaisia ​​- erityisesti Lean lauseen todistaja — matematiikan formalisointi, mikä edellyttää matemaattisten käsitteiden, lauseiden ja todisteiden esittämistä tiukassa, tietokoneella todennettavissa olevassa muodossa. Tämä mahdollistaa matematiikan joskus epävirallisen kielen tarkistamisen tietokoneilla.

Tutkijat tutkivat edelleen tämän matematiikan ja ohjelmoinnin välisen yhteyden seurauksia. Alkuperäinen Curry-Howard-kirjeenvaihto sulattaa ohjelmoinnin eräänlaiseen logiikkaan, jota kutsutaan intuitionistiseksi logiikaksi, mutta käy ilmi, että myös useampia logiikkatyyppejä voitaisiin soveltaa tällaisiin yhdistämiseen.

"Se mitä on tapahtunut vuosisadalla Curryn näkemyksen jälkeen, on se, että löydämme yhä enemmän tapauksia, joissa "looginen järjestelmä X vastaa laskennallista järjestelmää Y", sanoi. Michael Clarkson, tietojenkäsittelytieteilijä Cornellin yliopistossa. Tutkijat ovat jo yhdistäneet ohjelmoinnin muun tyyppiseen logiikkaan, kuten lineaariseen logiikkaan, joka sisältää käsitteen "resurssit" ja modaalilogiikkaan, joka käsittelee mahdollisuuden ja välttämättömyyden käsitteitä.

Ja vaikka tämä kirjeenvaihto kantaa Curryn ja Howardin nimiä, he eivät suinkaan ole ainoita, jotka ovat löytäneet sen. Tämä todistaa kirjeenvaihdon perustavanlaatuisen luonteen: ihmiset huomaavat sen yhä uudelleen ja uudelleen. "Ei näytä olevan sattumaa, että laskennan ja logiikan välillä on syvä yhteys", Clarkson sanoi.