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á logikaTeorie typů
implikacefunkční typ
konjunkcesoučinový typ
disjunkcesoučtový typ
pravdajednotkový typ
nepravdaprázdný typ

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

Predikátová logikaTeorie typů
zobecněný součinový typ
zobecněný součtový typ

Pro rovnost se používá zvláštní typ , jehož jedinou hodnotou je Refl.[1]

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

Reference

Související články