Curryho–Howardův isomorfismus

Curryho–Howardův isomorfismus je v logice a teorii typů rovnocennost mezi typy a formulemi, resp. jejich důkazy. Logickým objektům (konektivům a konstantám) odpovídají typy takto:

Výroková logika	Teorie typů
implikace	funkční typ
konjunkce	součinový typ
disjunkce	součtový typ
pravda	jednotkový typ
nepravda	prázdný typ

Kvantifikátory v logice prvního řádu odpovídají závislostním typům:

Predikátová logika	Teorie typů
$\forall$	zobecněný součinový typ
$\exists$	zobecněný součtový typ

Pro rovnost se používá zvláštní typ $a=_{A}b$, jehož jedinou hodnotou je Refl.

Konkrétní hodnoty jednotlivých typů přímo odpovídají důkazům formulí.

Související články

• Haskell Brooks Curry

Autoritní data	BNF: cb151164792 (data) LCCN: sh2001002954 NLI: 987007532525705171