Functional Programming 2024/25 fall

Tõestamine Idrises

Tuletusreeglid Idrises

Loogikareegel

 P1 P2 ... Pn
 ------------ r
      P

on Idrises

 r : P1 -> P2 -> .. -> Pn 
     --------------------
   ->          P
 r = ...

Kui me kõik loengus tutvustatud loomuliku tuletuse reeglid tõestada saame, oleme näidanud, et Idris on vähemalt sama võimas kui loengus toodud loomulik tuletus.

Tuleb välja, et kõik reeglid, v.a. klassikalise loogika reegel ja implikatsiooni sissetoomine, on võimalik mõistlikult tuua Idrises definitsioonidena.

implikatsioon P1⊃P2 on P1->P2 (-tüüp)

Idris-e loogika aluseks on keelde sisse ehitatud implikatsion (ehk funktsioonitüüp).

Implikatsiooni väljaviimise (ehk funktsiooni rakenduse) reegel võtab implikatsiooni a->b ja eelduse a ning annab välja b

 ?f ?x : (a->b) -> a
         ----------- 
      ->      b

Implikatsiooni sissetoomse (ehk {$\lambda$}-abstraktsiooni) reegli järgi saame järeldada implikatsiooni a->b -- eeldusel, et saame näidata b kui meile on antud a.

 (\ x => ?y) :   a
                 .
                 .
                 .
                 b
               ------
          ->   a -> b

Reegli nime asemel kasutame vastavalt funktsioonirakendust või funktsiooni defineerimise süntaksit.

Kõik teised konstruktsioonid saame sisse tuua data abil loodud andmestruktuuridega. Kontruktoriteks on sissetoomise reeglid.

Konjunktsioon P1∧P2 on paar (P1, P2) (-tüüp)

sissetoomine:

conI : p1 -> p2 
       --------
    -> (p1, p2)
conI x y = (x,y)

väljaviimine:

conEl : (p1, p2) 
        --------
     ->   p1 
conEl (x,y) = x

conEr : (p1, p2) 
        --------
     ->   p2
conEr (x,y) = y

Disjunktsioon P1∨P2 on Either P1 P2 (-tüüp)

  data Either a b = Left a | Right b

sissetoomine:

disIl :       p1 
         -------------
      ->  Either p1 p2
disIl = Left

disIr :      p2 
         ------------
      -> Either p1 p2
disIr = Right

väljaviimine:

disE : Either p1 p2 -> (p1 -> q) -> (p2 -> q) 
       --------------------------------------
     ->                q
disE (Left x)  f g = f x
disE (Right x) f g = g x

Tõene on () ja Väär on Void (-tüüp)

 data () = ()
 data Void : Type where  
   -- see on meelega tühi! 

sissetoomine:

truI : ----
        ()
truI = ()

väljaviimine:

falsE : Void 
        ----
     ->   p
falsE x impossible 

Eitus ¬P on not p (-tüüp)

not: Type -> Type
not t = t -> Void

sissetoomine:

notI : (p->Void) 
       ---------
    ->   not p
notI q = \p => q p 

väljaviimine:

notE: not p -> p 
      ----------
   ->    Void
notE f x = f x

Võrdused ja rewrite

Võrduste teooria on standardteegis defineeritud põhimõtteliselt nii:

 data (=) : Type -> Type -> Type where
     Refl : {a:Type}
           ----------
          -> a = a

(Nii saame defineerida üldisi võrdusi ja ei pea enam iga kasutuse jaoks tõestama uut teoreemi, nagu idVec sõltuvat tüüpide loengus.)

Võrduse väljaviimiseks on rewrite .. in .. reegel.

  rewrite .. in .. : a=b -> Pb 
                     ----------
                 ->     Pa

S.t. kui meil on vaja tõestada S (n+0) = S n ja me teame võrdust eq: n+0 = n siis rewrite eq asendab eesmärgis n+0-d n-dega. Jääb tõestada S n = S n.

Muide, rewrite-i saab ka ise implementeerida, aga seda on ebamugavam kasutada. Idrise sisseehitatud rewrite suudab P ise tuletada aga myrewrite puhul on vaja see argumendiks anda.

myrewrite : (p:a -> Type) -> {x:a} -> {y:a} -> x=y -> p y -> p x
myrewrite p Refl h = h

Predikaat p tuleb tuletada tõestamise eesmärgist. Näiteks, kui meil oli vaja tõestada S (n+0) = S n siis tuleks predikaadiks võtta \ z => S z = S n ehk asendatav komponent tuleb teha parameetriks.

Klassikaline loogika

classic: (not (not p)) -> p
classic f = ?q 

Kuna Idris pole klassikaline loogika, pole võimalik tõestada, kui me juba ei tea, et p.

Saame classic-u teha aksioomiks aga siis pole seda võimalik programmina käima panna!