Dypkoblingen som setter likhetstegn mellom matematiske bevis og dataprogrammer | Quanta Magazine

Noen vitenskapelige funn betyr noe fordi de avslører noe nytt - for eksempel den doble spiralformede strukturen til DNA, eller eksistensen av sorte hull. Noen åpenbaringer er imidlertid dyptgripende fordi de viser at to gamle konsepter, som en gang ble antatt forskjellige, faktisk er de samme. Ta James Clerk Maxwells ligninger som viser at elektrisitet og magnetisme er to aspekter av et enkelt fenomen, eller generell relativitets kobling av tyngdekraften med et buet rom-tid.

Curry-Howard-korrespondansen gjør det samme, men i større skala, og kobler ikke bare separate konsepter innenfor ett felt, men hele disipliner: informatikk og matematisk logikk. Også kjent som Curry-Howard-isomorfismen (et begrep som betyr at det eksisterer en slags en-til-en-korrespondanse mellom to ting), etablerer den en kobling mellom matematiske bevis og dataprogrammer.

Enkelt sagt, antyder Curry-Howard-korrespondansen at to begreper fra informatikk (typer og programmer) er ekvivalente, henholdsvis til proposisjoner og bevis - konsepter fra logikk.

En forgrening av denne korrespondansen er at programmering - ofte sett på som et personlig håndverk - heves til det idealiserte nivået av matematikk. Å skrive et program er ikke bare "koding", det blir en handling for å bevise et teorem. Dette formaliserer handlingen med programmering og gir måter å resonnere matematisk om riktigheten av programmer.

Korrespondansen er oppkalt etter de to forskerne som uavhengig oppdaget den. I 1934 la matematikeren og logikeren Haskell Curry merke til en likhet mellom funksjoner i matematikk og implikasjonsforholdet i logikk, som tar form av "hvis-da"-utsagn mellom to proposisjoner.

Inspirert av Currys observasjon, oppdaget den matematiske logikeren William Alvin Howard en dypere kobling mellom beregning og logikk i 1969, og viste at å kjøre et dataprogram er mye som å forenkle et logisk bevis. Når et dataprogram kjører, blir hver linje "evaluert" for å gi en enkelt utgang. På samme måte, i et bevis, starter du med komplekse utsagn som du kan forenkle (ved å eliminere overflødige trinn, for eksempel, eller erstatte komplekse uttrykk med enklere) til du kommer til en konklusjon - en mer fortettet og kortfattet uttalelse avledet fra mange midlertidige uttalelser .

Selv om denne beskrivelsen formidler en generell følelse av korrespondansen, for å forstå den fullt ut, må vi lære litt mer om det informatikere kaller "typeteori."

La oss starte med et kjent paradoks: I en landsby bor det en barberer som barberer alle mennene som ikke barberer seg, og bare dem. Barberer frisøren seg selv? Hvis svaret er ja, så må han ikke barbere seg (fordi han bare barberer menn som ikke barberer seg selv). Hvis svaret er nei, så må han barbere seg (fordi han barberer alle menn som ikke barberer seg selv). Dette er en uformell versjon av et paradoks Bertrand Russell oppdaget mens han prøvde å etablere grunnlaget for matematikk ved å bruke et konsept kalt sett. Det vil si at det er umulig å definere et sett som inneholder alle sett som ikke inneholder seg selv uten å møte motsetninger.

For å unngå dette paradokset, viste Russell, kan vi bruke "typer." Grovt sett er dette kategorier hvis spesifikke verdier kalles objekter. For eksempel, hvis det er en type kalt "Nat", som betyr naturlige tall, er objektene 1, 2, 3 og så videre. Forskere bruker vanligvis et kolon for å angi typen av et objekt. Tallet 7, av heltallstype, kan skrives som "7: Heltall." Du kan ha en funksjon som tar et objekt av type A og spytter ut et objekt av type B, eller en som kombinerer et par objekter som var type A og type B til en ny type, kalt "A × B."

En måte å løse paradokset på er derfor å sette disse typene inn i et hierarki, slik at de bare kan inneholde elementer på et "lavere nivå" enn seg selv. Da kan ikke en type inneholde seg selv, noe som unngår selvreferensialiteten som skaper paradokset.

I typeteoriens verden kan det å bevise at et utsagn er sant se annerledes ut enn det vi er vant til. Hvis vi ønsker å bevise at heltallet 8 er partall, er det et spørsmål om å vise at 8 faktisk er et objekt av en bestemt type kalt "Even", der regelen for medlemskap er delelig med 2. Etter å ha bekreftet at 8 er delelig med 2 kan vi konkludere med at 8 faktisk er en "innbygger" av typen Even.

Curry og Howard viste at typer er fundamentalt likeverdige med logiske forslag. Når en funksjon "bebor" en type - det vil si når du klarer å definere en funksjon som er et objekt av den typen - viser du effektivt at den tilsvarende proposisjonen er sann. Så funksjoner som tar en inngang av type A og gir en utgang av type B, betegnet som type A → B, må tilsvare en implikasjon: "Hvis A, så B." Ta for eksempel forslaget "Hvis det regner, så er bakken våt." I typeteori vil denne proposisjonen bli modellert av en funksjon med typen "Raining → GroundIsWet." Formuleringene som ser annerledes ut er faktisk matematisk de samme.

Hvor abstrakt den koblingen enn kan høres ut, har den ikke bare endret hvordan utøvere av matematikk og informatikk tenker om arbeidet sitt, men også ført til flere praktiske anvendelser på begge felt. For informatikk gir det et teoretisk grunnlag for programvareverifisering, prosessen med å sikre riktigheten av programvare. Ved å utforme ønsket atferd i form av logiske forslag, kan programmerere matematisk bevise at et program oppfører seg som forventet. Det gir også et sterkt teoretisk grunnlag for å designe kraftigere funksjonelle programmeringsspråk.

Og for matematikk har korrespondansen ført til fødselen av bevisassistenter, også kalt interaktive teorembevisere. Dette er programvareverktøy som hjelper til med å konstruere formelle bevis, for eksempel Coq og Lean. I Coq er hvert trinn i beviset i hovedsak et program, og bevisets gyldighet kontrolleres med typesjekkingsalgoritmer. Matematikere har også brukt bevisassistenter - spesielt Lean teorem bevis — å formalisere matematikk, som innebærer å representere matematiske konsepter, teoremer og bevis i et strengt, dataverifiserbart format. Det gjør at det noen ganger uformelle språket i matematikk kan kontrolleres av datamaskiner.

Forskere utforsker fortsatt konsekvensene av denne koblingen mellom matematikk og programmering. Den originale Curry-Howard-korrespondansen kombinerer programmering med en slags logikk som kalles intuisjonistisk logikk, men det viser seg at flere typer logikk også kan være mottagelig for slike foreninger.

"Det som har skjedd i århundret siden Currys innsikt er at vi stadig oppdager flere og flere tilfeller der 'logisk system X tilsvarer beregningssystem Y'," sa Michael Clarkson, en informatiker ved Cornell University. Forskere har allerede koblet programmering til andre typer logikk som lineær logikk, som inkluderer begrepet "ressurser", og modal logikk, som omhandler begreper om mulighet og nødvendighet.

Og selv om denne korrespondansen bærer Currys og Howards navn, er de på ingen måte de eneste som har oppdaget den. Dette vitner om korrespondansens grunnleggende karakter: Folk legger stadig merke til det igjen og igjen. "Det ser ikke ut til å være tilfeldig at det er en dyp kobling mellom beregning og logikk," sa Clarkson.