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.https://dev.to/betelgeuse/prolegomena-k-uvodu-do-zakladu-zavislostnich-typu-4380
Konkrétní hodnoty jednotlivých typů přímo odpovídají důkazům formulí.
Reference
Související články Haskell Brooks Curry
Kategorie:Teorie typů Kategorie:Logika