Korespondence Curry-Howard

Curry-Howardova korespondence ( Curry-Howard isomorphism , anglický formulæ-as-types výklad ) je pozorovatelná strukturální ekvivalence mezi matematickými důkazy a programy , která může být formalizována jako izomorfismus mezi logickými systémy a typizovanými výpočty.

Haskell Curry [1] a William Howard2] , že konstrukce důkazu je podobná popisu výpočtů a výroky konstruktivní logiky jsou svou strukturou podobné typům počítaných výrazů – programů pro počítač . Prvními projevy tohoto spojení jsou Brouwer-Heiting-Kolmogorovova interpretace (1925), která definuje sémantiku intuicionistické logiky prostřednictvím výpočtu důkazů, a teorie realizovatelnosti Kleene (1945).

Curry-Howardova korespondence v moderním pohledu není omezena na žádný logický nebo typový systém. Například výroková logika odpovídá jednoduchému typovanému λ-kalkulu , druhého řádu odpovídá λ-kalkulu a kalkulu odpovídá λ-počet se závislými typy .

V rámci Curryho-Howardova izomorfismu jsou následující strukturní prvky považovány za ekvivalentní:

Logické systémy	Programovací jazyky
tvrzení	Typ
Důkaz prohlášení $P$	Typ termínu (výrazu). $P$
Výrok je prokazatelný $P$	Typ obydlený $P$
implikace $P\Rightarrow Q$	funkční typ $P\rightarrow Q$
Spojení $P\land Q$	Typ uměleckého díla (páry) $P\times Q$
Disjunkce $P\lor Q$	Typ součtu (diskriminovaná unie) $P+Q$
Opravdová formule	jediný typ
Falešný vzorec	Prázdný typ ( ) $\bot$
Univerzální kvantifikátor $\pro všechny$	Typ závislého produktu ( -type) $\Pí$
Kvantifikátor existence $\existuje$	Typ závislého součtu ( -type) $\Sigma$

Nejjednodušším příkladem Curry-Howardovy korespondence je izomorfismus mezi jednoduchým typovaným λ-kalkulem a kusem intuicionistické výrokové logiky , která zahrnuje pouze implikaci . Například typ v jednoduchém typu lambda kalkulu odpovídá tvrzení výrokové logiky. K prokázání tohoto tvrzení je nutné zkonstruovat termín zadaného typu (pokud to lze provést, pak o typu říkají, že je obydlený nebo obydlený ), v tomto případě můžete uvést požadovaný termín: , a to znamená, že tautologie byla prokázána. $(P\rightarrow Q\rightarrow R)\rightarrow (P\rightarrow Q)\rightarrow P\rightarrow R$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$ $\lambda fgx\rightarrow fx(gx)$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$

Použití Curryho-Howardova izomorfismu umožnilo vytvořit celou třídu funkčních programovacích jazyků , jejichž runtime prostředí je také automatickým důkazním systémem , jako jsou Coq , Agda a Epigram .

Poznámky

↑ Curry, HB, Feys, R. Kombinační logika sv. I. - Amsterdam : North-Holland , 1958.
↑ Howard, WA Pojem konstrukce jako formule // To HB Curry: Essays on Combinatory Logic, Lambda Calculus and formalism. - Boston: Academic Press , 1980. - s. 479-490 .

Literatura

Pierce, Benjamin C. Typy a programovací jazyky. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Překlad do ruštiny: Pierce B. Typy v programovacích jazycích. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .