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ů |
|---|---|
| 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í.
