The Deep Link, der sidestiller matematiske beviser og computerprogrammer | Quanta Magasinet

Nogle videnskabelige opdagelser betyder noget, fordi de afslører noget nyt - den dobbelte spiralformede struktur af DNA, for eksempel, eller eksistensen af ​​sorte huller. Nogle åbenbaringer er dog dybtgående, fordi de viser, at to gamle begreber, der engang blev tænkt adskilte, faktisk er de samme. Tag James Clerk Maxwells ligninger, der viser, at elektricitet og magnetisme er to aspekter af et enkelt fænomen, eller generel relativitets kobling af tyngdekraften med et buet rum-tid.

Curry-Howard-korrespondancen gør det samme, men i større skala, og forbinder ikke kun separate begreber inden for ét felt, men hele discipliner: Datalogi , matematisk logik. Også kendt som Curry-Howard isomorfismen (et udtryk, der betyder, at der eksisterer en form for en-til-en-korrespondance mellem to ting), etablerer den en forbindelse mellem matematiske beviser og computerprogrammer.

Enkelt sagt hævder Curry-Howard korrespondancen, at to begreber fra datalogi (typer og programmer) er ækvivalente med henholdsvis påstande og beviser - begreber fra logik.

En forgrening af denne korrespondance er, at programmering - ofte set som et personligt håndværk - er hævet til det idealiserede niveau af matematik. At skrive et program er ikke bare "kodning", det bliver en handling for at bevise et teorem. Dette formaliserer programmeringshandlingen og giver måder at ræsonnere matematisk på om programmernes rigtighed.

Korrespondancen er opkaldt efter de to forskere, der uafhængigt af hinanden opdagede den. I 1934 bemærkede matematikeren og logikeren Haskell Curry en lighed mellem funktioner i matematik og implikationsforholdet i logik, som tager form af "hvis-så"-udsagn mellem to påstande.

Inspireret af Currys observation opdagede den matematiske logiker William Alvin Howard en dybere sammenhæng mellem beregning og logik i 1969, hvilket viste, at det at køre et computerprogram er meget som at forenkle et logisk bevis. Når et computerprogram kører, "evalueres" hver linje for at give et enkelt output. På samme måde starter du i et bevis med komplekse udsagn, som du kan forenkle (ved at eliminere overflødige trin, f.eks. eller erstatte komplekse udtryk med simplere), indtil du når til en konklusion - en mere fortættet og kortfattet udsagn afledt af mange foreløbige udsagn .

Selvom denne beskrivelse formidler en generel følelse af korrespondancen, for fuldt ud at forstå den, er vi nødt til at lære lidt mere om, hvad dataloger kalder "typeteori."

Lad os starte med et berømt paradoks: I en landsby bor der en barber, som barberer alle de mænd, der ikke barberer sig selv, og kun dem. Barberer barberen sig selv? Hvis svaret er ja, så må han ikke barbere sig (fordi han kun barberer mænd, der ikke barberer sig selv). Hvis svaret er nej, så skal han barbere sig (fordi han barberer alle de mænd, der ikke barberer sig selv). Dette er en uformel version af et paradoks, Bertrand Russell opdagede, mens han forsøgte at etablere grundlaget for matematik ved hjælp af et begreb kaldet mængder. Det vil sige, at det er umuligt at definere et sæt, der indeholder alle sæt, der ikke indeholder sig selv, uden at støde på modsigelser.

For at undgå dette paradoks, viste Russell, kan vi bruge "typer." Det er groft sagt kategorier, hvis specifikke værdier kaldes objekter. For eksempel, hvis der er en type kaldet "Nat", hvilket betyder naturlige tal, er dens objekter 1, 2, 3 og så videre. Forskere bruger typisk et kolon til at angive typen af ​​et objekt. Tallet 7, af heltalstypen, kan skrives som "7: Heltal." Du kan have en funktion, der tager et objekt af type A og spytter et objekt af type B ud, eller en, der kombinerer et par objekter, der var type A og type B, til en ny type, kaldet "A × B."

En måde at løse paradokset på er derfor at sætte disse typer ind i et hierarki, så de kun kan indeholde elementer af et "lavere niveau" end dem selv. Så kan en type ikke rumme sig selv, hvilket undgår den selv-referentialitet, der skaber paradokset.

I typeteoriens verden kan bevis for, at et udsagn er sandt, se anderledes ud, end vi er vant til. Hvis vi vil bevise, at hele tallet 8 er lige, så er det et spørgsmål om at vise, at 8 faktisk er et objekt af en specifik type kaldet "Lige", hvor reglen for medlemskab er delelig med 2. Efter at have verificeret, at 8 er delelig med 2 kan vi konkludere, at 8 faktisk er en "indbygger" af typen Even.

Curry og Howard viste, at typer grundlæggende svarer til logiske påstande. Når en funktion "bebor" en type - det vil sige, når du med succes kan definere en funktion, der er et objekt af den type - viser du effektivt, at den tilsvarende proposition er sand. Så funktioner, der tager et input af type A og giver et output af type B, betegnet som type A → B, skal svare til en implikation: "Hvis A, så B." Tag for eksempel forslaget "Hvis det regner, så er jorden våd." I typeteori ville dette forslag være modelleret af en funktion med typen "Raining → GroundIsWet." De anderledes udseende formuleringer er faktisk matematisk ens.

Hvor abstrakt den sammenhæng end kan lyde, har den ikke kun ændret, hvordan udøvere af matematik og datalogi tænker om deres arbejde, men også ført til adskillige praktiske anvendelser på begge områder. For datalogi giver det et teoretisk grundlag for softwareverifikation, processen med at sikre korrektheden af ​​software. Ved at formulere ønsket adfærd i form af logiske propositioner kan programmører matematisk bevise, at et program opfører sig som forventet. Det giver også et stærkt teoretisk grundlag for at designe mere kraftfulde funktionelle programmeringssprog.

Og for matematik har korrespondancen ført til fødslen af bevisassistenter, også kaldet interaktive sætningsbeviser. Disse er softwareværktøjer, der hjælper med at konstruere formelle beviser, såsom Coq og Lean. I Coq er hvert trin i beviset i det væsentlige et program, og bevisets gyldighed kontrolleres med typekontrolalgoritmer. Matematikere har også brugt bevisassistenter - især Lean teorem bevis — at formalisere matematik, som indebærer at repræsentere matematiske begreber, sætninger og beviser i et stringent, computerverificerbart format. Det gør det muligt at kontrollere matematikkens til tider uformelle sprog af computere.

Forskere udforsker stadig konsekvenserne af denne forbindelse mellem matematik og programmering. Den originale Curry-Howard korrespondance fusionerer programmering med en slags logik kaldet intuitionistisk logik, men det viser sig, at flere typer logik også kunne være modtagelige for sådanne ensretninger.

"Det, der er sket i århundredet siden Currys indsigt er, at vi bliver ved med at opdage flere og flere tilfælde, hvor 'logisk system X svarer til beregningssystem Y'," sagde Michael Clarkson, en datalog ved Cornell University. Forskere har allerede koblet programmering til andre typer logik som lineær logik, som inkluderer begrebet "ressourcer" og modal logik, som omhandler begreber om mulighed og nødvendighed.

Og selvom denne korrespondance bærer Currys og Howards navne, er de på ingen måde de eneste, der har opdaget det. Dette vidner om korrespondancens grundlæggende karakter: Folk bliver ved med at bemærke det igen og igen. "Det ser ikke ud til at være tilfældigt, at der er en dyb forbindelse mellem beregning og logik," sagde Clarkson.