Corespondență Curry-Howard

Corespondența Curry-Howard ( Curry-Howard isomorphism , în engleză formulæ-as-types interpretation ) este o echivalență structurală observabilă între demonstrații și programe matematice care poate fi formalizată ca izomorfism între sisteme logice și calcule tipizate.

Haskell Curry [1] și William Howard2] că construcția dovezi constructive este similară cu descrierea calculelor, iar enunțurile logicii constructive sunt similare în structura lor cu tipurile de expresii calculate - programe pentru calculator . Manifestările timpurii ale acestei conexiuni sunt interpretarea Brouwer-Heiting-Kolmogorov (1925), care definește semantica logicii intuiționiste prin calculul demonstrațiilor și teoria realizabilității Kleene (1945).

Corespondența Curry-Howard în viziunea modernă nu se limitează la nici un sistem de logică sau tip. De exemplu, logica propozițională corespunde unui λ-calcul tip simplu , logica de ordinul doi corespunde unui λ-calcul iar calculul predicat corespunde unui λ-calcul cu tipuri dependente .

În cadrul izomorfismului Curry-Howard, următoarele elemente structurale sunt considerate echivalente:

Sisteme logice	Limbaje de programare
afirmație	Tip de
Dovada afirmației $P$	Tip de termen (expresie). $P$
Afirmația este dovedibilă $P$	Tip locuit $P$
implicare $P\Rightarrow Q$	tip functional $P\rightarrow Q$
Conjuncție $P\land Q$	Tipul operei de artă (perechi) $P\time Q$
Disjuncția $P\lor Q$	Tipul sumei (uniunea discriminată) $P+Q$
Adevărata formulă	un singur tip
Formula falsă	Tip gol ( ) $\bot$
Cuantificator universal $\pentru toți$	Tip de produs dependent ( -tip) $\Pi$
Cuantificator de existență $\există$	Tipul sumei dependente ( -tip) $\Sigma$

Cel mai simplu exemplu de corespondență Curry-Howard este un izomorfism între un simplu λ-calcul tipat și o bucată de logică propozițională intuiționistă care include doar implicația . De exemplu, un tip dintr-un calcul lambda tip simplu corespunde unei propoziții de logică propozițională. Pentru a demonstra această afirmație, este necesar să construiți un termen de tipul specificat (dacă acest lucru se poate face, atunci se spune despre tipul că este locuit sau locuit ), în acest caz, puteți prezenta termenul dorit: , și asta înseamnă că tautologia a fost dovedită. $(P\rightarrow Q\rightarrow R)\rightarrow (P\rightarrow Q)\rightarrow P\rightarrow R$ $(P\Săgeată la dreapta (Q\Săgeată la dreapta R))\Săgeată la dreapta ((P\Săgeată la dreapta Q)\Săgeată la dreapta (P\Săgeată la dreapta R))$ $\lambda fgx\rightarrow fx(gx)$ $(P\Săgeată la dreapta (Q\Săgeată la dreapta R))\Săgeată la dreapta ((P\Săgeată la dreapta Q)\Săgeată la dreapta (P\Săgeată la dreapta R))$

Utilizarea izomorfismului Curry-Howard a făcut posibilă crearea unei întregi clase de limbaje de programare funcționale al căror mediu de rulare este, de asemenea, un sistem de demonstrare automată , cum ar fi Coq , Agda și Epigram .

Note

↑ Curry, HB, Feys, R. Combinatory Logic Vol. I. - Amsterdam : Olanda de Nord , 1958.
↑ Howard, WA Noțiunea de formule ca tipuri de construcție // Către HB Curry: Eseuri despre logica combinatorie, calculul lambda și formalismul. - Boston: Academic Press , 1980. - pp. 479-490 .

Literatură

Pierce, Benjamin C. Tipuri și limbaje de programare. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Traducere în rusă: Pierce B. Tipuri în limbaje de programare. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .