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
app : (a->b) -> a
-----------
-> b
Implikatsiooni sissetoomse (ehk {$\lambda$}-abstraktsiooni) reegel võtab implikatsiooni a->b ja eelduse a ning annab välja b
(\ x => y) : a
---
-> b
Need reeglid on sisse ehitatud -- definitsioone me anda ei saa (ja ei pea).
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
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!