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ů
$\mathrm{\forall }$	zobecněný součinový typ
$\mathrm{\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