Djuplänken som likställer matematiska bevis och datorprogram | Quanta Magazine

Vissa vetenskapliga upptäckter spelar roll eftersom de avslöjar något nytt - den dubbla spiralformade strukturen hos DNA, till exempel, eller förekomsten av svarta hål. Vissa uppenbarelser är dock djupgående eftersom de visar att två gamla begrepp, som en gång troddes olika, faktiskt är desamma. Ta James Clerk Maxwells ekvationer som visar att elektricitet och magnetism är två aspekter av ett enda fenomen, eller generell relativitets koppling av gravitation med en krökt rum-tid.

Curry-Howard-korrespondensen gör samma sak men i större skala, och länkar inte bara separata begrepp inom ett område, utan hela discipliner: Datavetenskap och matematisk logik. Även känd som Curry-Howard-isomorfismen (en term som betyder att det finns någon form av en-till-en-överensstämmelse mellan två saker), upprättar den en koppling mellan matematiska bevis och datorprogram.

Enkelt uttryckt hävdar Curry-Howard-korrespondensen att två begrepp från datavetenskap (typer och program) är likvärdiga respektive påståenden och bevis - begrepp från logik.

En förgrening av denna korrespondens är att programmering - ofta ses som ett personligt hantverk - höjs till den idealiserade nivån av matematik. Att skriva ett program är inte bara "kodning", det blir en handling för att bevisa ett teorem. Detta formaliserar handlingen att programmera och ger sätt att resonera matematiskt om korrektheten av program.

Korrespondensen är uppkallad efter de två forskare som oberoende upptäckte den. 1934 märkte matematikern och logikern Haskell Curry en likhet mellan funktioner i matematik och implikationsförhållandet i logik, som tar formen av "om-då"-påståenden mellan två propositioner.

Inspirerad av Currys observation upptäckte den matematiska logikern William Alvin Howard en djupare koppling mellan beräkning och logik 1969, vilket visade att att köra ett datorprogram är ungefär som att förenkla ett logiskt bevis. När ett datorprogram körs "utvärderas" varje rad för att ge en enda utdata. På samma sätt, i ett bevis, börjar du med komplexa påståenden som du kan förenkla (genom att till exempel eliminera överflödiga steg eller ersätta komplexa uttryck med enklare) tills du kommer till en slutsats - ett mer sammanfattat och kortfattat uttalande som härrör från många interimspåståenden .

Även om den här beskrivningen förmedlar en allmän känsla av korrespondensen, för att helt förstå den måste vi lära oss lite mer om vad datavetare kallar "typteori".

Låt oss börja med en berömd paradox: I en by bor det en barberare som rakar alla män som inte rakar sig själva, och bara dem. Rakar frisören sig själv? Om svaret är ja, då får han inte raka sig (eftersom han bara rakar män som inte rakar sig själva). Om svaret är nej, då måste han raka sig (eftersom han rakar alla män som inte rakar sig själva). Detta är en informell version av en paradox som Bertrand Russell upptäckte när han försökte fastställa grunderna för matematik med hjälp av ett koncept som kallas mängder. Det vill säga, det är omöjligt att definiera en mängd som innehåller alla mängder som inte innehåller sig själva utan att stöta på motsägelser.

För att undvika denna paradox, visade Russell, kan vi använda "typer." Grovt sett är detta kategorier vars specifika värden kallas objekt. Till exempel, om det finns en typ som heter "Nat", vilket betyder naturliga tal, är dess objekt 1, 2, 3 och så vidare. Forskare använder vanligtvis ett kolon för att beteckna typen av ett föremål. Siffran 7, av heltalstyp, kan skrivas som "7: Heltal." Du kan ha en funktion som tar ett objekt av typ A och spottar ut ett objekt av typ B, eller en som kombinerar ett par objekt som var typ A och typ B till en ny typ, kallad "A × B."

Ett sätt att lösa paradoxen är därför att placera dessa typer i en hierarki, så att de bara kan innehålla element på en "lägre nivå" än de själva. Då kan inte en typ innehålla sig själv, vilket undviker självreferensialiteten som skapar paradoxen.

I typteorins värld kan bevis på att ett påstående är sant se annorlunda ut än vad vi är vana vid. Om vi ​​vill bevisa att heltal 8 är jämnt, så är det en fråga om att visa att 8 verkligen är ett objekt av en specifik typ som kallas "Jämn", där regeln för medlemskap är delbart med 2. Efter att ha verifierat att 8 är delbart med 2 kan vi dra slutsatsen att 8 verkligen är en "invånare" av typen Even.

Curry och Howard visade att typer i grunden är likvärdiga med logiska propositioner. När en funktion "bebor" en typ - det vill säga när du framgångsrikt kan definiera en funktion som är ett objekt av den typen - visar du effektivt att motsvarande proposition är sann. Så funktioner som tar en ingång av typ A och ger en utdata av typ B, betecknad som typ A → B, måste motsvara en implikation: "Om A, då B." Ta till exempel förslaget "Om det regnar, då är marken blöt." I typteorin skulle denna proposition modelleras av en funktion med typen "Raining → GroundIsWet." De olika formuleringarna är i själva verket matematiskt desamma.

Hur abstrakt den kopplingen än kan låta har den inte bara förändrat hur utövare av matematik och datavetenskap tänker kring sitt arbete, utan också lett till flera praktiska tillämpningar inom båda områdena. För datavetenskap ger det en teoretisk grund för mjukvaruverifiering, processen för att säkerställa att programvaran är korrekt. Genom att rama in önskade beteenden i termer av logiska propositioner kan programmerare matematiskt bevisa att ett program beter sig som förväntat. Det ger också en stark teoretisk grund för att designa mer kraftfulla funktionella programmeringsspråk.

Och för matematik har korrespondensen lett till födelsen av bevisassistenter, även kallade interaktiva satsbevisare. Dessa är mjukvaruverktyg som hjälper till att konstruera formella bevis, som Coq och Lean. I Coq är varje steg av beviset i huvudsak ett program, och bevisets giltighet kontrolleras med typkontrollalgoritmer. Matematiker har också använt bevisassistenter - särskilt Lean theorem prover — Att formalisera matematik, vilket innebär att matematiska begrepp, satser och bevis representeras i ett rigoröst, datorverifierbart format. Det gör att det ibland informella språket i matematik kan kontrolleras av datorer.

Forskare undersöker fortfarande konsekvenserna av denna koppling mellan matematik och programmering. Den ursprungliga Curry-Howard-korrespondensen förenar programmering med en sorts logik som kallas intuitionistisk logik, men det visar sig att fler typer av logik också skulle kunna vara mottagliga för sådana sammanslagningar.

"Vad som har hänt under århundradet sedan Currys insikt är att vi fortsätter att upptäcka fler och fler fall där 'logiskt system X motsvarar beräkningssystem Y'", sa Michael Clarkson, en datavetare vid Cornell University. Forskare har redan kopplat programmering till andra typer av logik som linjär logik, som inkluderar begreppet "resurser", och modal logik, som handlar om begrepp om möjlighet och nödvändighet.

Och även om den här korrespondensen bär Currys och Howards namn, är de inte alls de enda som har upptäckt den. Detta vittnar om korrespondensens grundläggande karaktär: Folk lägger märke till det om och om igen. "Det verkar inte vara någon tillfällighet att det finns en djup koppling mellan beräkning och logik," sa Clarkson.