Curry-Howard levelezés

A Curry-Howard megfeleltetés ( Curry-Howard isomorphism , angol formulaæ-as-types interpretation ) egy megfigyelhető szerkezeti egyenértékűség a matematikai bizonyítások és programok között , amely izomorfizmusként formalizálható a logikai rendszerek és a tipizált kalkulusok között.

Haskell Curry [1] és William Howard2] , hogy a bizonyítás felépítése hasonló a számítások leírásához, a konstruktív logika állításai pedig szerkezetüket tekintve hasonlóak a számítógépre szánt, kiszámított kifejezések típusaihoz . Ennek a kapcsolatnak a korai megnyilvánulásai a Brouwer-Heiting-Kolmogorov értelmezés (1925), amely az intuicionista logika szemantikáját bizonyítások kiszámításával határozza meg, valamint Kleene (1945) megvalósíthatósági elmélete

A Curry-Howard levelezés a modern felfogásban nem korlátozódik egyetlen logikára vagy típusrendszerre sem. Például a propozíciós logika egy egyszerű tipusú λ-kalkulusnak , a másodrendű logika egy λ-számításnak a predikátumszámítás pedig egy függő típusokkal rendelkező λ- kalkulusnak felel meg .

A Curry-Howard izomorfizmus keretein belül a következő szerkezeti elemek tekinthetők egyenértékűnek:

Logikai rendszerek	Programozási nyelvek
nyilatkozat	Típusú
Az állítás igazolása $P$	Kifejezés (kifejezés) típusa $P$
Az állítás bizonyítható $P$	Típus lakott $P$
következmény $P\Rightarrow Q$	funkcionális típus $P\rightarrow Q$
Konjunkció $P\land Q$	Műalkotás típusa (párok) $P\times Q$
Diszjunkció $P\lor Q$	Összeg típusa (diszkriminált szakszervezet) $P+Q$
Igazi Forma	egyetlen típus
Hamis képlet	Üres típus ( ) $\bot$
Univerzális kvantor $\mindenkinek$	Függő terméktípus ( -típus ) $\Pi$
Létezési kvantor $\létezik$	Függő összeg típusa ( -típus ) $\Sigma$

A Curry-Howard megfeleltetés legegyszerűbb példája egy egyszerű tipizált λ-számítás és egy intuíciós propozíciós logika közötti izomorfizmus , amely csak implikációt tartalmaz . Például egy típus egy egyszerű típusos lambda-számításban megfelel a propozíciós logika propozíciójának. Ennek az állításnak a bizonyításához meg kell alkotni egy adott típusú tagot (ha ez megtehető, akkor a típusról azt mondják, hogy lakott vagy lakott ), ebben az esetben megadhatja a kívánt kifejezést: , és ez azt jelenti, hogy a tautológia bizonyított. $(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))$

A Curry-Howard izomorfizmus használata lehetővé tette funkcionális programozási nyelvek egész osztályának létrehozását, amelyek futtatókörnyezete egyben automatikus próbarendszer is , mint például a Coq , az Agda és az Epigram .

Jegyzetek

↑ Curry, HB, Feys, R. Combinatory Logic Vol. I. - Amszterdam : Észak-Hollandia , 1958.
↑ Howard, WA A képletek, mint típusok fogalma a konstrukcióról // HB Curryhez: Esszék a kombinatív logikáról, a lambdaszámításról és a formalizmusról. - Boston: Academic Press , 1980. - 479-490 .

Irodalom

Pierce, Benjamin C. Típusok és programozási nyelvek. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Orosz nyelvű fordítás: Pierce B. Típusok programozási nyelvekben. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .