Curry–Howard-isomorfisme

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[bewerken | brontekst bewerken]

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 bekend staat 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 bekend staat 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 abstractie maken van de eigenaardigheden van beide formalismen, ontstaat de volgende veralgemening: een bewijs is een programma, en de formule die het bewijst is het type voor het programma. Meer informeel kan dit worden gezien als een analogie die stelt dat het retourtype van een functie (d.w.z. het type waarden dat door een functie wordt 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 weergegeven als programma's, en vooral als lambdatermen, of 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 getypte functionele programmeertaal te fungeren. Dit omvat de intuïtionistische typetheorie van Martin-Löf en Coquands Calculus of Constructions. 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 getypte lambdacalculi afgeleid van het Curry-Howard-paradigma leidden tot software als Coq waarin bewijzen die als programma's worden gezien, kunnen worden geformaliseerd, gecontroleerd en uitgevoerd.

De correspondentie tussen Curry en Howard 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 voorzetting 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 bekend staan als call-by-name en call-by-value.

Vanwege de mogelijkheid om niet-eindigende programma's te schrijven, moeten Turingvolledige rekenmodellen (zoals talen met willekeurige recursieve functies) met zorg worden geïnterpreteerd, aangezien naïeve toepassing 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 afsluitende code te scheiden van potentieel niet-eindigende code.

Algemene formulering[bewerken | brontekst bewerken]

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 is 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
voegwoord	producttype
disjunctie	somtype
echte formule	unittype of toptype
valse formule	leeg type of bottomtype

Op het niveau van bewijssystemen en rekenmodellen toont de correspondentie voornamelijk de identiteit van de structuur:

Tussen enkele specifieke formuleringen van systemen die bekend staan als het Hilbert-stijl deductiesysteem en combinatorische logica.
Tussen enkele specifieke formuleringen van bekende systemen. zoals natuurlijke deductie en lambdacalculus.

Logische kant	Programmeerkant
Hilbert-stijl deductiesysteem	typesysteem voor combinatorische logica
natuurlijke deductie	typesysteem voor lambdacalculus

Tussen het natuurlijke deductiesysteem en de lambdacalculus zijn er de volgende overeenkomsten:

Logische kant	Programmeerkant
hypothesen	vrije variabelen
implicatie-eliminatie (modus ponens)	functietoepassing
implicatie introductie	abstractie

Overeenkomstige systemen[bewerken | brontekst bewerken]

Intuïtionistische deductiesystemen in Hilbert-stijl en getypte combinatorische logica[bewerken | brontekst bewerken]

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.

Getypte 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 één-op-één 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	Getypte combinatorische logica
${\frac {\alpha \in \Gamma }{\Gamma \vdash \alpha }}\qquad \qquad {\text{Assum}}$	${\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}$
${\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}\qquad {\text{Ax}}_{K}$	${\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}$
${\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}\;{\text{Ax}}_{S}$	${\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\quad {\text{Modus Ponens}}$	${\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}$

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 éénpuntsbasis 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 getypte lambdacalculus[bewerken | brontekst bewerken]

Nadat Curry de syntactische overeenkomst tussen intuïtionistische deductie in Hilbert-stijl en getypte combinatorische logica had benadrukt, maakte Howard in 1969 een syntactische analogie expliciet tussen de programma's van eenvoudig getypte lambdacalculus en de bewijzen van natuurlijke deductie. Hieronder formaliseert de linkerkant de intuïtionistische implicationele natuurlijke deductie als een calculus van sequenten (het gebruik van sequenten is standaard in discussies over het Curry-Howard-isomorfisme, omdat hierdoor de deductieregels duidelijker kunnen worden geformuleerd) met impliciete verzwakking. De rechterkant toont de typeregels van lambdacalculus. Aan de linkerkant duiden Γ, Γ ₁ en Γ ₂ geordende reeksen formules aan, terwijl ze aan de rechterkant reeksen benoemde (d.w.z. getypte) formules aanduiden met allemaal verschillende namen.

Intuïtionistische implicatieve natuurlijke deductie	Toewijzingsregels voor het type lambdacalculus
${\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}$	${\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$
${\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I$	${\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash (\lambda x\!:\!\alpha .~t):\alpha \rightarrow \beta }}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E$	${\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\beta }}$

Om de correspondentie te parafraseren: het bewijzen van Γ ⊢ α betekent dat je een programma hebt dat, gegeven waarden met de typen vermeld in Γ, een object van het type α produceert. Een axioma/hypothese komt overeen met de introductie van een nieuwe variabele met een nieuw, onbeperkt type, de → I regel komt overeen met functie-abstractie en de → E regel komt overeen met functietoepassing. Merk op dat de overeenkomst niet exact is als de context Γ wordt opgevat als een reeks formules, zoals bijvoorbeeld de λ-termen λ x . λy . x en λx . λy . y van het type α → α → α zou in de correspondentie niet worden onderscheiden. Voorbeelden worden hieronder gegeven.

Howard toonde aan dat de correspondentie zich uitstrekt tot andere verbindingen van de logica en andere constructies van de eenvoudig getypte lambdacalculus. Op abstract niveau gezien kan de correspondentie vervolgens worden samengevat zoals weergegeven in de volgende tabel. Het laat vooral ook zien dat de notie van normale vormen in lambdacalculus overeenkomt met Prawitz' notie van normale deductie in natuurlijke deductie, waaruit volgt dat de algoritmen voor het type-bewoningsprobleem kunnen worden omgezet in algoritmen voor het bepalen van de intuïtionistische bewijsbaarheid.

Logische kant	Programmeerkant
axioma/hypothese	variabele
introductieregel	constructor
eliminatie regel	destructor
normale aftrek	normaalvorm
normalisatie van aftrekposten	zwakke normalisatie
bewijsbaarheid	type bewoningsprobleem
intuïtionistische tautologie	universeel bewoond type

Howards correspondentie strekt zich uiteraard uit tot andere uitbreidingen van natuurlijke deductie en de eenvoudig getypte lambdacalculus. Hier is een niet-uitputtende lijst:

Girard-Reynolds Systeem F als een gemeenschappelijke taal voor zowel propositielogica van de tweede orde als polymorfe lambda-calculus,
logica van hogere orde en Girards System F
inductieve typen als algebraïsch gegevenstype
noodzaak $\Box$ in modale logica en gefaseerde berekeningen
mogelijkheid $\Diamond$ in modale logica en monadische typen voor effecten
De λ_I-calculus (waarbij de abstractie beperkt is tot λx . E, waarbij x minstens één keer vrij voorkomt in E) en CL_I- calculus komen overeen met relevante logica.
De lokale waarheidsmodaliteit (∇) in de Grothendieck-topologie of de equivalente "laxe" modaliteit (◯) van Benton, Bierman en de Paiva (1998) komt overeen met CL-logica die "berekeningstypen" beschrijft.

Klassieke logica en controle-operatoren[bewerken | brontekst bewerken]

Ten tijde van Curry, en ook ten tijde van Howard, had de correspondentie met bewijzen als programma's alleen betrekking op intuïtionistische logica, dat wil zeggen een logica waarin met name de wet van Peirce niet afleidbaar was. De uitbreiding van de overeenkomst met de wet van Peirce en dus met de klassieke logica werd duidelijk uit het werk van Griffin over typeoperatoren die de evaluatiecontext van een bepaalde programma-uitvoering vastleggen, zodat deze evaluatiecontext later opnieuw kan worden geïnstalleerd. De basiscorrespondentie in Curry-Howard-stijl voor klassieke logica wordt hieronder gegeven. Let op de overeenkomst tussen de vertaling met dubbele ontkenning die wordt gebruikt om klassieke bewijzen aan intuïtionistische logica toe te wijzen, en de vertaling in continuation-passing-stijl die wordt gebruikt om lambda-termen waarbij controle betrokken is, om te zetten in pure lambda-termen. Meer in het bijzonder hebben vertalingen in call-by-name-continuation-passing-stijl betrekking op Kolmogorovs dubbele ontkenningsvertaling, en call-by-value vervolg-passing-stijl vertalingen hebben betrekking op een soort dubbele-negatievertaling als gevolg van Kuroda.

Logische kant	Programmeerkant
De wet van Peirce: (( α → β ) → α ) → α	call-with-current-continuation
vertaling met dubbele ontkenning	vertaling in continuation-passing-stijl

Er bestaat een fijnere Curry-Howard-correspondentie voor klassieke logica als men de klassieke logica niet definieert door een axioma zoals de wet van Peirce toe te voegen, maar door verschillende conclusies in opeenvolgende volgorde toe te staan. In het geval van klassieke natuurlijke deductie bestaat er een bewijzen-als-programma-correspondentie met de getypte programma's van Parigots λμ-calculus.

Sequentiële calculus[bewerken | brontekst bewerken]

Een bewijzen-als-programma's-correspondentie kan worden uitgedrukt voor het formalisme dat bekend staat als Gentzens sequentiële calculus, maar het is geen correspondentie met een goed gedefinieerd, reeds bestaand rekenmodel zoals het was voor Hilbert-stijl en natuurlijke deducties.

Sequentiële calculus wordt gekenmerkt door de aanwezigheid van linkerintroductieregels, rechterintroductieregel en een cut-regel die kan worden geëlimineerd. De structuur van sequentiële calculus heeft betrekking op een calculus waarvan de structuur dicht bij die van sommige abstracte machines ligt. De informele correspondentie luidt als volgt:

Logische kant	Programmeerkant
cut-eliminatie	reductie in een vorm van abstracte machine
rechterintroductieregels	constructors van code
linkerintroductieregels	constructors van evaluatiestacks
prioriteit aan de rechterkant bij cut-eliminatie	call-by-name- reductie
prioriteit aan de linkerkant bij cut-eliminatie	call-by-value- reductie

Gerelateerde bewijzen-als-programma's-correspondenties[bewerken | brontekst bewerken]

De rol van de Bruijn[bewerken | brontekst bewerken]

N.G. de Bruijn gebruikte de lambdanotatie voor het weergeven van bewijzen in Automath, en presenteerde stellingen als "categorieën" van hun bewijzen. Het was eind jaren zestig, in dezelfde periode waarin Howard zijn manuscript schreef; de Bruijn was waarschijnlijk niet op de hoogte van het werk van Howard en drukte de correspondentie onafhankelijk uit (Sørensen & Urzyczyn [1998] 2006, pp 98-99). Sommige onderzoekers hebben de neiging om de term Curry-Howard-de Bruijn-correspondentie te gebruiken in plaats van Curry-Howard-correspondentie.

BHK-interpretatie[bewerken | brontekst bewerken]

De BHK-interpretatie interpreteert intuïtionistische bewijzen als functies, maar specificeert niet de klasse van functies die relevant zijn voor de interpretatie. Als men de lambdacalculus voor deze klasse van functies neemt, zegt de BHK-interpretatie hetzelfde als Howards correspondentie tussen natuurlijke deductie en de lambdacalculus.

Realiseerbaarheid[bewerken | brontekst bewerken]

Kleenes recursieve realiseerbaarheid splitst bewijzen van intuïtionistische rekenkunde op in het paar van een recursieve functie en een bewijs van een formule, dat uitdrukt dat de recursieve functie 'realiseert', dat wil zeggen dat de disjuncties en existentiële kwantificatoren van de initiële formule correct worden geïnstantieerd, zodat de formule als waar wordt geëvalueerd.

De gewijzigde realiseerbaarheid van Kreisel is van toepassing op intuïtionistische predicaatlogica van hogere orde en laat zien dat de eenvoudig getypte lambdaterm die inductief uit het bewijs wordt gehaald, de initiële formule realiseert. In het geval van propositionele logica valt dit samen met de uitspraak van Howard: de geëxtraheerde lambdaterm is het bewijs zelf (gezien als een ongetypeerde lambdaterm) en de realiseerbaarheidsverklaring is een parafrase van het feit dat de geëxtraheerde lambdaterm het type heeft dat de formule betekent (gezien als een type).

Gödels dialectica-interpretatie realiseert (een uitbreiding van) de intuïtionistische rekenkunde met berekenbare functies. Het verband met lambdarekening is onduidelijk, zelfs in het geval van natuurlijke deductie.

De Curry-Howard-Lambek-correspondetie[bewerken | brontekst bewerken]

Joachim Lambek toonde begin jaren zeventig aan dat de bewijzen van intuïtionistische propositielogica en de combinatoren van getypeerde combinatorische logica een gemeenschappelijke equational theorie delen, de theorie van cartesiaans gesloten categorieën. De uitdrukking Curry-Howard-Lambek-correspondentie wordt nu door sommige mensen gebruikt om te verwijzen naar de relaties tussen intuïtionistische logica, getypte lambdacalculus en cartesiaanse gesloten categorieën, waarbij objecten worden geïnterpreteerd als typen of proposities en morfismen als termen of bewijzen. Lambeks correspondentie is een correspondentie van equational theorieën, waarbij wordt geabstraheerd van de dynamiek van berekeningen zoals bètareductie en termnormalisatie. Het is niet de uitdrukking van een syntactische identiteit van structuren zoals het geval is voor elk van Currys en Howards correspondenties. Dit wil zeggen de structuur van een goed gedefinieerd morfisme in een cartesiaans gesloten categorie niet vergelijkbaar is met de structuur van een bewijs van het overeenkomstige oordeel in logica in Hilbert-stijl of natuurlijke deductie. Het is bijvoorbeeld niet mogelijk om te stellen of te bewijzen dat een morfisme normaliseert, een stelling van het Church-Rosser-type vast te stellen, of te spreken van een ‘sterk normaliserende’ cartesiaanse gesloten categorie. Om dit onderscheid te verduidelijken, wordt de onderliggende syntactische structuur van cartesiaanse gesloten categorieën hieronder opnieuw geformuleerd.

Objecten (typen) worden gedefinieerd door

$\top$ is een voorwerp
als α en β objecten zijn, dan zijn $\alpha \times \beta$ en $\alpha \rightarrow \beta$ objecten.

Morfismen (termen) worden gedefinieerd door

$id$ , $\star$ , $\operatorname {eval}$ , $\pi _{1}$ en $\pi _{2}$ zijn morfismen
als t een morfisme is, is λ t een morfisme
als t en u morfismen zijn, dan zijn $(t,u)$ en $u\circ t$ morfismen.

Goed gedefinieerde morfismen (getypeerde termen) worden gedefinieerd door de volgende typeregels (waarin de gebruikelijke categorische morfismenotatie $f:\alpha \to \beta$ wordt vervangen door sequentiële calculusnotatie $f:\!\!-~~\alpha ~\vdash ~\beta$ ).

Identiteit:

{\frac {}{id:\!\!-~~\alpha ~\vdash ~\alpha }}

Compositie:

{\frac {t:\!\!-~~\alpha ~\vdash ~\beta \qquad u:\!\!-~~\beta ~\vdash ~\gamma }{u\circ t:\!\!-~\alpha ~\vdash ~\gamma }}

Eenheidstype ( terminaal object):

{\frac {}{\star :\!\!-~~\alpha ~\vdash ~\top }}

Cartesiaans product:

{\frac {t:\!\!-~~\alpha ~\vdash ~\beta \qquad u:\!\!-~~\alpha ~\vdash ~\gamma }{(t,u):\!\!-~~\alpha ~\vdash ~\beta \times \gamma }}

Linker- en rechterprojectie:

{\frac {}{\pi _{1}:\!\!-~~\alpha \times \beta ~\vdash ~\alpha }}\qquad {\frac {}{\pi _{2}:\!\!-~~\alpha \times \beta ~\vdash ~\beta }}

Currying:

{\frac {t:\!\!-~~\alpha \times \beta ~\vdash ~\gamma }{\lambda t:\!\!-~~\alpha ~\vdash ~\beta \rightarrow \gamma }}

Functietoepassing:

{\frac {}{eval:\!\!-~~(\alpha \rightarrow \beta )\times \alpha ~\vdash ~\beta }}

Ten slotte zijn de vergelijkingen van de categorie:

$id\circ t=t$
$t\circ id=t$
$(v\circ u)\circ t=v\circ (u\circ t)$
$\star =id$ (mits goed getypt)
$\star \circ u=\star$
$\pi _{1}\circ (t,u)=t$
$\pi _{2}\circ (t,u)=u$
$(\pi _{1},\pi _{2})=id$
$(t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)$
$eval\circ (\lambda t\circ \pi _{1},\pi _{2})=t$
$\lambda eval=id$
$\lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))$

Deze vergelijkingen impliceren het volgende $\eta$ -wetten:

$(\pi _{1}\circ t,\pi _{2}\circ t)=t$
$\lambda (eval\circ (t\circ \pi _{1},\pi _{2}))=t$

Nu bestaat t zodat $t:\!\!-~\alpha _{1}\times \ldots \times \alpha _{n}\vdash \beta$ als en slechts als $\alpha _{1},\ldots ,\alpha _{n}\vdash \beta$ bewijsbaar is in de impliciete intuïtionistische logica.

Voorbeeld[bewerken | brontekst bewerken]

Dankzij de Curry-Howard-correspondentie is een getypte uitdrukking waarvan het type overeenkomt met een logische formule analoog aan een bewijs van die formule. Hieronder volgt een voorbeeld.

De identiteitscombinator wordt gezien als een bewijs van α → α in logica in Hilbert-stijl[bewerken | brontekst bewerken]

Beschouw als voorbeeld een bewijs van de stelling α → α. In de lambdacalculus is dit het type identiteitsfunctie I = λ x.x en in de combinatorische logica wordt de identiteitsfunctie verkregen door S = λfgx tweemaal toe te passen op K = λ xy . X. Dat wil zeggen, I = ((S K) K). Als beschrijving van een bewijs zegt dit dat de volgende stappen kunnen worden gebruikt om α → α te bewijzen:

instantieer het tweede axiomaschema met de formules α, β → α en α om een bewijs te verkrijgen van (α → ((β → α) → α)) → ((α → (β → α)) → (α → α)) ,
Instantieer het eerste axiomaschema één keer met α en β → α om een bewijs te verkrijgen van α → ((β → α) → α) ,
instantieer het eerste axiomaschema een tweede keer met α en β om een bewijs te verkrijgen van α → (β → α) ,
pas modus ponens tweemaal toe om een bewijs te verkrijgen van α → α

Over het algemeen is de procedure dat wanneer het programma een toepassing van het vorm (P Q) bevat, deze stappen moeten worden gevolgd:

Bewijs eerst de stellingen die overeenkomen met de typen P en Q.
Omdat P wordt toegepast op Q, moet het type P de vorm α → β hebben en het type Q moet voor sommige α en β de vorm α hebben. Daarom is het mogelijk om de conclusie, β, los te maken via de modus ponens-regel.

Andere toepassingen[bewerken | brontekst bewerken]

Het isomorfisme is voorgesteld geweest als een manier om de verdeling van de zoekruimte in genetische programmering (GP) te definiëren. De methode indexeert verzamelingen van genotypen (de programmabomen die door het GP-systeem worden geëvolueerd) op basis van hun Curry-Howard-isomorfe bewijs (ook wel een species genoemd).

Zoals opgemerkt door INRIA-onderzoeksdirecteur Bernard Lang, vormt de Curry-Howard-correspondentie een argument tegen de octrooieerbaarheid van software: aangezien algoritmen wiskundige bewijzen zijn, zou de octrooieerbaarheid van eerstgenoemde de octrooieerbaarheid van laatstgenoemde impliceren. Een stelling kan privébezit zijn; een wiskundige zou moeten betalen voor het gebruik ervan. De wiskundige zou het bedrijf moeten vertrouwen dat het verkoopt, maar het bewijs geheim houdt en de verantwoordelijkheid voor eventuele fouten afwijst.

Veralgemeningen[bewerken | brontekst bewerken]

De hier opgesomde overeenkomsten gaan veel verder en dieper. Cartesiaanse gesloten categorieën worden bijvoorbeeld veralgemeend door gesloten monoïdale categorieën. De interne taal van deze categorieën is het lineaire typesysteem (overeenkomend met lineaire logica), dat eenvoudig getypeerde lambdacalculus veralgemeent als de interne taal van cartesiaanse gesloten categorieën. Bovendien kan worden aangetoond dat deze overeenkomen met cobordismen, die een cruciale rol spelen in de snaartheorie.

Een uitgebreide reeks equivalenties wordt ook onderzocht in homotopietypetheorie. Hier wordt de typetheorie uitgebreid met het univalentie-axioma ("equivalentie is gelijkwaardig aan gelijkheid"), waardoor homotopietypetheorie kan worden gebruikt als basis voor de hele wiskunde (inclusief de verzamelingenleer en de klassieke logica, waardoor nieuwe manieren worden geboden om het keuzeaxioma uit te drukken en vele andere zaken). Dat wil zeggen, het Curry-Howard-isomorfisme dat stelt dat bewijzen elementen zijn van bewoonde typen, wordt veralgemeend naar het idee van homotopische equivalentie van bewijzen (als paden in de ruimte, waarbij het identiteitstype of gelijkheidstype van de typetheorie wordt geïnterpreteerd als een pad). Onder andere de Fieldsmedaillewinnaar Vladimir Vojevodski werkte aan homotopietypetheorie.