In de programmeertaaltheorie en bewijstheorie is het Curry-Howard-isomorfisme (ook bekend als de Curry-Howard-correspondentie of -equivalentie, of de interpretatie van bewijzen als programma's en proposities of formules als typen) de directe relatie tussen computerprogramma's en wiskundige bewijzen.
Het is een veralgemening van een syntactische analogie tussen systemen van formele logica en computationele berekeningen die werd ontdekt door de Amerikaanse wiskundige Haskell Curry en de logicus William Alvin Howard. Het is de link tussen logica en berekening die gewoonlijk wordt toegeschreven aan Curry en Howard, hoewel het idee verband houdt met de operationele interpretatie van intuïtionistische logica die in verschillende formuleringen wordt gegeven door L.E.J. Brouwer, Arend Heyting en Andrey Kolmogorov (zie Brouwer-Heyting-Kolmogorov-interpretatie) en Stephen Kleene. De relatie is uitgebreid naar de categorietheorie als de drievoudige Curry-Howard-Lambek-correspondentie.
Oorsprong, omvang en gevolgen Het begin van het Curry-Howard-isomorfisme ligt in verschillende observaties:
In 1934 merkte Curry op dat de typen van combinatoren kunnen worden gezien als axiomaschema's voor intuïtionistische implicatielogica. In 1958 merkte hij op dat een bepaald soort bewijssysteem, deductiesystemen in Hilbert-stijl genoemd, voor een bepaald fragment samenvalt met het getypeerde fragment van een standaard rekenmodel dat bekendstaat als combinatorische logica. In 1969 merkte Howard op dat een ander bewijssysteem, natuurlijke deductie genoemd, in zijn intuïtionistische versie direct kan worden geïnterpreteerd als een getypeerde variant van het rekenmodel dat bekendstaat als lambdacalculus.
Het Curry-Howard-isomorfisme is de observatie dat er een isomorfisme bestaat tussen de bewijssystemen en de rekenmodellen. Het is de bewering dat deze twee families van formalismen als identiek kunnen worden beschouwd.
Als we abstraheren van de eigenaardigheden van beide formalismen, ontstaat de volgende veralgemening: een bewijs is een programma, en de formule die het bewijst is het type van dat programma. Meer informeel kan dit worden gezien als een analogie die stelt dat het type van de returnwaarde van een functie (dat wil zeggen het type van de waarden die door een functie worden geretourneerd) analoog is aan een logische stelling, onderworpen aan hypothesen die overeenkomen met de typen van de argumentwaarden van de functie. Het programma om die functie te berekenen is analoog aan een bewijs van die stelling. Hierdoor wordt een vorm van logisch programmeren op een rigoureuze basis gezet: bewijzen kunnen worden gerepresenteerd als programma's, in het bijzonder als lambdatermen, en bewijzen kunnen worden uitgevoerd.
De Curry-Howard-correspondentie was het startpunt van een groot spectrum aan nieuw onderzoek, dat met name heeft geleid tot een nieuwe klasse van formele systemen die zijn ontworpen om zowel als bewijssysteem als een getypeerde functionele programmeertaal te fungeren. Dit omvat de intuïtionistische typetheorie van Martin-Löf en Calculus of Constructions van Coquand. Dit zijn twee calculi waarin bewijzen reguliere objecten van het discours zijn. Men kan in deze calculi de eigenschappen van bewijzen op dezelfde manier uitdrukken als elk programma. Dit onderzoeksgebied wordt gewoonlijk de moderne typetheorie genoemd.
Dergelijke van het Curry-Howard-paradigma afgeleide getypeerde lambdacalculi leidden tot software als Coq waarin bewijzen, die als programma's worden gezien, kunnen worden geformaliseerd, gecontroleerd en uitgevoerd.
De Curry-Howard-correspondentie riep ook nieuwe vragen op over de computationele inhoud van bewijsconcepten die niet aan bod kwamen in de originele werken van Curry en Howard. In het bijzonder is aangetoond dat klassieke logica overeenkomt met het vermogen om de voortzetting van programma's te manipuleren en met de symmetrie van sequentiële calculus om de dualiteit uit te drukken tussen de twee evaluatiestrategieën die bekendstaan als call-by-name en call-by-value.
Omdat het mogelijk is hierin niet-eindigende programma's te schrijven, moeten Turingvolledige rekenmodellen (zoals talen met willekeurige recursieve functies) zorgvuldig worden geïnterpreteerd, aangezien het naïef toepassen van de correspondentie tot een inconsistente logica leidt. De beste manier om vanuit logisch oogpunt met willekeurige berekeningen om te gaan is nog steeds een onderzoeksvraag waar actief over wordt gedebatteerd, maar een populaire benadering is gebaseerd op het gebruik van monaden om aantoonbaar eindigende code te scheiden van mogelijk niet-eindigende code.
Algemene formulering In zijn meer algemene formulering is het zogenaamde Curry-Howard-isomorfisme of de Curry-Howard-correspondentie een correspondentie tussen formele bewijscalculi en typesystemen voor rekenmodellen. In het bijzonder splitst het zich in twee correspondenties: Op het niveau van formules en typen dat onafhankelijk is van welk specifiek bewijssysteem of rekenmodel wordt overwogen. Op het niveau van bewijzen en computerprogramma's die, deze keer, specifiek zijn voor de specifieke keuze van het bewijssysteem en het rekenmodel dat wordt beschouwd.
Op het niveau van formules en typen zegt de correspondentie dat implicatie zich hetzelfde gedraagt als een functietype, conjunctie als een "product"-type (dit kan een tupel, een struct, een lijst of een andere term worden genoemd, afhankelijk van de taal), disjunctie als somtype (dit type kan een unie worden genoemd), de valse formule als het lege type en de ware formule als het eenheidstype (waarvan het enige lid het nulobject is). Kwantificatoren komen overeen met afhankelijke functieruimte of producten (indien van toepassing). Dit is samengevat in de volgende tabel: Logische kant Programmeerkant universele kwantificering veralgemeend producttype (Π-type) existentiële kwantificering veralgemeend somtype (Σ-type) implicatie functietype conjunctie producttype disjunctie somtype logische constante "waar" unittype logische constante "onwaar" leeg type Op het niveau van bewijssystemen en rekenmodellen toont de correspondentie voornamelijk de identiteit van de structuur:
tussen enkele specifieke formuleringen van systemen die bekendstaan als het Hilbert-stijl deductiesysteem aan de ene kant en combinatorische logica aan de andere kant; en tussen enkele specifieke formuleringen van systemen die bekendstaan als natuurlijke deductie aan de ene kant en de lambdacalculus aan de andere kant.
Logische kant Programmeerkant Hilbert-stijl deductiesysteem typesysteem voor combinatorische logica natuurlijke deductie typesysteem voor lambdacalculus Tussen natuurlijke deductie en de lambdacalculus zijn er de volgende overeenkomsten: Logische kant Programmeerkant hypothesen vrije variabelen implicatie-eliminatie (modus ponens) functietoepassing implicatie-introductie abstractie
Overeenkomstige systemen
Intuïtionistische deductiesystemen in Hilbert-stijl en getypeerde combinatorische logica Het was in het begin een opmerking in het boek van Curry en Feys uit 1958 over combinatorische logica: de eenvoudigste typen voor de basiscombinatoren K en S van combinatorische logica kwamen verrassend genoeg overeen met de respectieve axiomaschema's α → ( β → α ) en ( α → ( β → γ )) → (( α → β ) → ( α → γ )) gebruikt in deductiesystemen in Hilbert-stijl. Om deze reden worden deze schema's nu vaak axioma's K en S genoemd. Voorbeelden van programma's die als bewijzen worden gezien in een logica in Hilbert-stijl worden hieronder gegeven.
Als we ons beperken tot het impliciete intuïtionistische fragment, is een eenvoudige manier om logica in Hilbert-stijl te formaliseren als volgt. Laat Γ een eindige verzameling formules zijn, beschouwd als hypothesen. Dan is δ af te leiden uit Γ, aangeduid met Γ ⊢ δ, in de volgende gevallen:
δ is een hypothese, d.w.z. het is een formule van Γ, δ is een voorbeeld van een axiomaschema; dat wil zeggen, onder het meest voorkomende axiomasysteem: δ heeft de vorm α → ( β → α ), of δ heeft de vorm ( α → ( β → γ )) → (( α → β ) → ( α → γ )), δ volgt door deductie, d.w.z. voor sommige α, zijn zowel α → δ als α al af te leiden uit Γ (dit is de regel van modus ponens)
Dit kan worden geformaliseerd met behulp van inferentieregels, zoals in de linkerkolom van de volgende tabel.
Getypeerde combinatorische logica kan worden geformuleerd met behulp van een vergelijkbare syntaxis: laat Γ een eindige verzameling variabelen zijn, geannoteerd met hun typen. Een term T (ook geannoteerd met zijn type) zal afhangen van deze variabelen [Γ ⊢ T: δ ] wanneer:
T is een van de variabelen in Γ, T is een basiscombinator; dat wil zeggen, onder de meest gebruikelijke combinatorbasis: T is K: α → ( β → α ) [waarbij α en β de typen argumenten aangeven], of T is S:( α → ( β → γ )) → (( α → β ) → ( α → γ )), T is de samenstelling van twee subtermen die afhankelijk zijn van de variabelen in Γ.
De hier gedefinieerde generatieregels worden weergegeven in de rechterkolom hieronder. Currys opmerking stelt simpelweg dat beide kolommen een-op-een corresponderen. De beperking van de correspondentie tot intuïtionistische logica betekent dat sommige klassieke tautologieën, zoals de wet van Peirce (( α → β ) → α ) → α, van de correspondentie worden uitgesloten. Intuïtionistische implicatielogica in Hilbert-stijl Getypeerde combinatorische logica Op een meer abstract niveau bekeken, kan de overeenkomst opnieuw worden geformuleerd, zoals weergegeven in de volgende tabel. Vooral de deductiestelling die specifiek is voor logica in Hilbert-stijl komt overeen met het proces van abstractie-eliminatie van combinatorische logica. Logische kant Programmeerkant aanname variabele axiomaschema's combinatoren modus ponens functietoepassing deductiestelling eliminatie van abstractie Dankzij de correspondentie kunnen resultaten uit combinatorische logica worden overgedragen naar logica in Hilbert-stijl en omgekeerd. Het idee van reductie van termen in combinatorische logica kan bijvoorbeeld worden overgedragen naar logica in Hilbert-stijl en biedt een manier om bewijzen canoniek om te zetten in andere bewijzen van dezelfde bewering. Men kan de notie van normale termen ook overbrengen naar een notie van normale bewijzen, waarbij men uitdrukt dat de hypothesen van de axioma's nooit allemaal los hoeven te staan (omdat er anders een vereenvoudiging kan plaatsvinden).
Omgekeerd kan de niet-bewijsbaarheid in de intuïtionistische logica van de wet van Peirce worden teruggevoerd naar de combinatorische logica: er is geen getypeerde term van de combinatorische logica die typbaar is met type
(( α → β ) → α ) → α .
Resultaten over de volledigheid van sommige verzamelingen van combinatoren of axioma's kunnen ook worden overgedragen. Het feit dat de combinator X een eenpuntsbasis vormt van (extensionele) combinatorische logica impliceert bijvoorbeeld dat het enkele axiomaschema
((( α → ( β → γ )) → (( α → β ) → ( α → γ ))) → (( δ → ( ε → δ )) → ζ )) → ζ ,
wat het hoofdtype van X is, een adequate vervanging is voor de combinatie van de axiomaschema's
α → ( β → α ) en ( α → ( β → γ )) → (( α → β ) → ( α → γ )).
Intuïtionistische natuurlijke deductie en getypeerde lambdacalculus