Otevřít hlavní menu

Curryho–Howardův isomorfismus

vztah mezi počítačovým programem a matematikou

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

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