Curry-Howardov izomorfizem

Curry-Howardov izomorfizem#

Curry-Howardov izomorfizem povezuje logiko s teorijo tipov. V grobem pravi, da lahko vsaki logični izjavi priredimo ustrezen tip v programskem jeziku, ki ima predstavnika natanko takrat, ko ima izjava dokaz. Curry-Howardov izomorfizem ni pomemben le zaradi globoke in lepe povezave dveh različnih področij, temveč ima tudi praktične posledice, saj na njem slonijo sodobni dokazovalni pomočniki, programi, ki matematične dokaze preverjajo na podoben način, kot OCaml preverja tipe.

O množicah dokazov#

Poglejmo si enostaven primer. Izjavo \(P \land Q\) lahko dokažemo tako, da dokažemo \(P\) in \(Q\) posebej. Obratno lahko iz \(P \land Q\) izpeljemo tako \(P\) kot \(Q\). Torej dokaz izjave \(P \land Q\) ustreza natanko paru dokazov za \(P\) in za \(Q\). Če z \(\mathcal{D}_R\) množico vseh dokazov izjave \(R\), velja \(\mathcal{D}_{P \land Q} \simeq \mathcal{D}_P \times \mathcal{D}_Q\).

Če ne privzamemo aksioma o izključeni tretji možnosti, podobna povezava velja med disjunkcijo in vsoto. Izjavo \(P \lor Q\) dokažemo natanko takrat, kadar dokažemo \(P\) ali dokažemo \(Q\). Oziroma na krajše: \(\mathcal{D}_{P \lor Q} \simeq \mathcal{D}_P + \mathcal{D}_Q\).

Zanimiva je tudi povezava med implikacijo in funkcijami. Izjavo \(P \Rightarrow Q\) dokažemo tako, da ob predpostavki \(P\) dokažemo \(Q\), kar pomeni, da je vsak dokaz izjave \(P \Rightarrow Q\) postopek, ki iz vsakega dokaza izjave \(P\) izpelje dokaz izjave \(Q\), oziroma \(\mathcal{D}_{P \Rightarrow Q} \simeq \mathcal{D}_P \to \mathcal{D}_Q\).

Za primer vzemimo tavtologijo \((P \land Q \Rightarrow R) \Rightarrow (P \Rightarrow (Q \Rightarrow R))\). Kako bi s pomočjo Curry-Howardovega izomorfizma preverili, da je resnična? Po zgornjih pravilih velja:

\[ \mathcal{D}_{(P \land Q \Rightarrow R) \Rightarrow (P \Rightarrow (Q \Rightarrow R))} \simeq (\mathcal{D}_P \times \mathcal{D}_Q \to \mathcal{D}_R) \to (\mathcal{D}_P \to (\mathcal{D}_Q \to \mathcal{D}_R)). \]

Če nam uspe najti funkcijo \((\mathcal{D}_P \times \mathcal{D}_Q \to \mathcal{D}_R) \to (\mathcal{D}_P \to (\mathcal{D}_Q \to \mathcal{D}_R))\) bomo našli tudi dokaz naše izjave. To je enostavno, saj gre le za konkreten primer izomorfizma \((A \times B \to C) \simeq (A \to (B \to C))\), ki velja za poljubne množice \(A, B, C\). Tako obstaja ne le preslikava ampak celo bijekcija \((\mathcal{D}_P \times \mathcal{D}_Q \to \mathcal{D}_R) \to (\mathcal{D}_P \to (\mathcal{D}_Q \to \mathcal{D}_R))\).

Za logično neresnico \(\bot\) seveda velja \(\mathcal{D}_\bot = \emptyset\), za logično resnico \(\top\) pa izberemo enojec \(\mathcal{D}_\top = \{*\}\) z enim samim trivialnim dokazom, ki ga običajno označujemo z \(*\).

Za negacijo lahko iz \(\lnot P = P \Rightarrow \bot\) izpeljemo \(\mathcal{D}_{\lnot P} = \mathcal{D}_P \to \emptyset\). Izjava \(\lnot P\) bo tako imela dokaz takrat, kadar je množica njenih dokazov \(\mathcal{D}_P \to \emptyset\) neprazna. Množica preslikav v prazno množico pa je neprazna natanko takrat, kadar je prazna njena domena, v tem primeru \(\mathcal{D}_P\). Torej ima \(\lnot P\) dokaz natanko takrat, kadar ga \(P\) nima.

Povezava med izjavami in tipi#

V programskem jeziku z dovolj močnimi tipi, kot je OCaml, lahko predstavimo vse zgoraj opisane konstrukcije, kar nam omogoča, da dokazov ne pišemo samo “na papir”, temveč v preverljivo programsko kodo.

Na primer, če želimo pokazati, da izjava \((P \land Q \Rightarrow R) \Rightarrow (P \Rightarrow (Q \Rightarrow R))\) drži za poljubne \(P, Q, R\), je dovolj, da skonstruiramo polimorfno preslikavo tipa (('p * 'q -> 'r) -> ('p -> ('q -> 'r))).

let dokaz_nase_izjave : (('p * 'q -> 'r) -> ('p -> ('q -> 'r))) =
  fun dokaz_iz_p_in_q_sledi_r ->
    fun dokaz_p ->
      fun dokaz_q ->
        let dokaz_p_in_q = (dokaz_p, dokaz_q) in
        let dokaz_r = dokaz_iz_p_in_q_sledi_r dokaz_p_in_q in
        dokaz_r

val dokaz_nase_izjave : ('p * 'q -> 'r) -> 'p -> 'q -> 'r = <fun>

Če bi bili v dokazu malomarni, bi nas OCaml na to opozoril, saj se tipi ne bi ujemali:

let napacen_dokaz : (('p * 'q -> 'r) -> ('p -> ('q -> 'r))) =
  fun dokaz_iz_p_in_q_sledi_r ->
    fun dokaz_p -> dokaz_iz_p_in_q_sledi_r dokaz_p

File "[17]", line 3, characters 43-50:
3 |     fun dokaz_p -> dokaz_iz_p_in_q_sledi_r dokaz_p
                                               ^^^^^^^
Error: This expression has type 'p but an expression was expected of type
         'p * 'q
       The type variable 'p occurs inside 'p * 'q

Mimogrede: isto funkcijo bi lahko napisali tudi na krajše. V resnici smo jo že videli, gre za funkcijo curry, le imena parametrov so druga:

let curry f x y = f (x, y)

val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

V OCamlu imamo že vgrajene ustrezne tipe za konjunkcijo (produkt *), implikacijo (funkcijski tip ->) in resnico (enotski tip unit). Za disjunkcijo lahko vsoto definiramo sami:

type ('p, 'q) sum = Left of 'p | Right of 'q

type ('p, 'q) sum = Left of 'p | Right of 'q

Dokaz izjave \(((P \lor Q) \Rightarrow R) \implies (P \Rightarrow R) \land (Q \Rightarrow R)\) tako ustreza funkciji tipa (('p, 'q) sum -> 'r) -> ('p -> 'r) * ('q -> 'r), ki jo lahko na primer definiramo kot

let dokaz2 : (('p, 'q) sum -> 'r) -> ('p -> 'r) * ('q -> 'r) =
  fun dokaz_iz_p_ali_q_sledi_r -> (
    (fun dokaz_p -> dokaz_iz_p_ali_q_sledi_r (Left dokaz_p)),
    (fun dokaz_q -> dokaz_iz_p_ali_q_sledi_r (Right dokaz_q))
  )

val dokaz2 : (('p, 'q) sum -> 'r) -> ('p -> 'r) * ('q -> 'r) = <fun>

Podobno lahko z naštevnim tipom brez konstruktorjev definiramo prazen tip empty, z njegovo pomočjo pa še tip za negacijo:

type empty
type 'p not = 'p -> empty

type empty

type 'p not = 'p -> empty

let iz_p_sledi_ne_ne_p : 'p -> 'p not not = fun h_p h_ne_p -> h_ne_p h_p

let iz_ne_p_ali_q_sledi_ne_p_in_ne_q : ('p, 'q) sum not -> 'p not * 'q not =
  fun h_ne_p_ali_q -> (
    (fun h_p -> h_ne_p_ali_q (Left h_p)),
    (fun h_q -> h_ne_p_ali_q (Right h_q))
  )
  
let iz_ne_p_in_ne_q_sledi_ne_p_ali_q : 'p not * 'q not -> ('p, 'q) sum not =
 fun (h_ne_p, h_ne_q) -> function
  | Left h_p -> h_ne_p h_p
  | Right h_q -> h_ne_q h_q

val iz_p_sledi_ne_ne_p : 'p -> 'p not not = <fun>

val iz_ne_p_ali_q_sledi_ne_p_in_ne_q : ('p, 'q) sum not -> 'p not * 'q not =
  <fun>

val iz_ne_p_in_ne_q_sledi_ne_p_ali_q : 'p not * 'q not -> ('p, 'q) sum not =
  <fun>

Omejitve OCamla#

Na zgornji način nam lahko OCaml služi kot preprost dokazovalnik. Ima pa več omejitev:

  1. Pisanje dokazov s pomočjo funkcij je precej nerodno. Nekateri dokazovalniki (npr. Lean ali Rocq) tako namesto tega uporabljajo taktike, s pomočjo katerih računalniku dajemo le napotke, kakšne dokaze naj konstruira. Spet v drugih dokazovalnikih (npr. Agda ali Idris) pa dokaze res pišemo neposredno, vendar nam pri tem interaktivno pomaga urejevalnik.

  2. S tipi v OCamlu lahko izrazimo le formule v izjavnem računu, ki ne vsebujejo predikatov in kvantifikatorjev. Razmislimo, čemu bi ustrezal predikat \(S\), ki pove, ali je naravno število sodo. Za vsako število \(n\) imamo torej izjavo \(S(n)\) in zato njej pripadajoč tip. Torej bi v OCamlu predikatu \(S\) ustrezala funkcija, ki vsakemu številu priredi svoj tip! Pri lihih številih bi bil ta tip prazen, pri sodih pa ne. V splošnem bi potrebovali funkcije iz vrednosti v tipe. V OCamlu imamo običajne funkcije iz vrednosti v vrednosti in celo konstruktorje tipov (npr. option, list, …), ki slikajo tipe v tipe. Funkcij iz vrednosti v tipe pa žal nimamo.

  3. S pomočjo rekurzije lahko v OCamlu definiramo funkcije tipov, ki ustrezajo neresničnim izjavam. Na primer, izjava \(P \Rightarrow Q\) v splošnem ne drži, vendar lahko vedno napišemo:

let rec iz_p_sledi_q : 'p -> 'q =
  fun dokaz_p ->
    let dokaz_q = iz_p_sledi_q dokaz_p in
    dokaz_q

val iz_p_sledi_q : 'p -> 'q = <fun>

Res, če tej funkciji kot argument podamo dokaz za \(P\), bo na koncu izvajanja funkcija vrnila dokaz za \(Q\). Se pa znamo malo načakati…

Contents