Kodutöö 5
{$\lambda$}-arvutus
Selles praktikumis harjutame {$\lambda$}-arvutust: harjutame vabade muutujate leidmist, substitutsiooni ning {$\alpha$}-võrdsust ning implementeerime Idrise funktsioonid, mis neid teostaksid.
Konspekt
Lambda termide andmestruktuur
Selleks, et saaksime Idrises teostada erinevaid operatsioone termidega, defineerime termide andmestruktuuri. Vaja läheb ka listi ja hulga andmestruktuure.
Põhifaili K5.idr kopeerige järgnev kood:
import Data.List
-- elem
import Data.SortedSet
-- empty, singleton, insert, delete, contains, union
data Lam = Var String | App Lam Lam | Abs String Lam
showLam : Nat -> Lam -> String
showLam _ (Var x) = x
showLam d (App f e) = showParens (d>1) (showLam 1 f++" "++showLam 2 e)
showLam d (Abs x e) = showParens (d>0) ("\\ "++x++". "++showLam 0 e)
-- See on liides -- liideseid vaatame järgmises praksis.
Show Lam where
show = showLam 0
-- t1 := \f. (\g. g x) (\x. f x)
t1 : Lam
t1 = Abs "f" (App (Abs "g" (App (Var "g") (Var "x"))) (Abs "x" (App (Var "f") (Var "x"))))
-- t2 := (\x. (\g. g x)) x
t2 : Lam
t2 = App (Abs "x" (Abs "g" (App (Var "g") (Var "x")))) (Var "x")
-- t3 := \g. (\f. f x) (\x. g x)
t3 : Lam
t3 = Abs "g" (App (Abs "f" (App (Var "f") (Var "x"))) (Abs "x" (App (Var "g") (Var "x"))))
Lisaks tuleb luua ka fail K5.ipkg sisuga:
package K5 depends = contrib
et saaksime importida ja kasutada hulga andmestuktuuri.
Faili laadimiseks kasutage nüüd käsku: rlwrap idris2 --find-ipkg K5.idr või rlwrap idris2 -p contrib K5.idr
Praktikumi ja kodutöö ülesanded
1. Vabade muutujate leidmine
Leia termidest vabad muutujad!
- {$ \text{FV}(\lambda{}f.\ (\lambda{}g.\ g\ x)\ (\lambda{}x.\ f\ x))$}
- {$ \text{FV}((\lambda{}x.\ (\lambda{}g.\ g\ x))\ x)$}
- {$ \text{FV}(\lambda{}g.\ (\lambda{}f.\ f\ x)\ (\lambda{}x.\ g\ x))$}
2. Funktsioon {$\text{FV}$}
Nüüd teeme Idrise funktsiooni, mis vabad muutujad leiab. Vaja läheb termi ja hulga andmestruktuure.
fv : Lam -> SortedSet String fv e = ?fv_rhs -- testimiseks on selgem kasutada liste fvList : Lam -> List String fvList = SortedSet.toList . fv
Proovi REPLis, kas saad samad tulemused, mis 1. ülesandes?
> fvList t1 > fvList t2 > fvList t3
3. Substitutsiooni arvutamine
Arvuta substitutsioonid
- {$ (\lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x))[x \to y]$}
- {$ ((\lambda{}x. (\lambda{}g. g x)) x)[x\to(\lambda{} x.x)]$}
- {$ (\lambda{}g. (\lambda{}f. f x) (\lambda{}x. g x))[x \to f]$}
4. Funktsioon {$\text{subst}$}
Nüüd teeme Idrise funktsiooni, mis arvutab substitutsiooni.
subst : Lam -> String -> Lam -> Lam subst e1 x e2 = ?subst_rhs
NB! Et ei peaks tuletama uut kasutamata muutujat, võime neid läbi proovida. (Siis kasutage kindlasti substitutsiooni definitsiooni siit.) Näiteks proovi lisada muutuja nimele ülakoma:
newv : String -> String newv xs = xs++"'"
Proovi REPLis, kas saad samad tulemused, mis 3. ülesandes?
> :exec printLn (subst t1 "x" (Var "y")) > :exec printLn (subst t2 "x" (Abs "x" (Var "x"))) > :exec printLn (subst t3 "x" (Var "f"))
5. {$\alpha$}-võrdsed avaldised
Kas järgnevad termid on {$\alpha$}-võrdsed?
- {$ \lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x) \;=_\alpha\; (\lambda{}x. (\lambda{}g. g x)) x $}
- {$ \lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x) \;=_\alpha\; \lambda{}g. (\lambda{}f. f x) (\lambda{}x. g x) $}
6. {$\alpha$}-võrdluse arvutamine
Nüüd teeme Idrise funktsiooni, mis arvutab {$\alpha$}-võrdsust.
Algoritm{$^*$} abistruuriga V, mis on hulk võrdsete muutujate paaridest:
{$$
\begin{array}{lclcl}
x & =^?_{V} & y & \equiv
&(x,y) \in V \\
e_1\ e_2 & =^?_{V} & e_3\ e_4 & \equiv
&e_1 =^?_{V} e_3 \land e_2 =^?_{V} e_4 \\
(\lambda x.\ e_1)& =^?_{V} & (\lambda y.\ e_2) & \equiv
&V':=\{(u,v)|(u,v) \in V, x\not=u, y\not=v\}\cup\{(x,y)\}\\
&&&& e_1=^?_{V'} e_2 \\
\_ & =^?_{V} & \_ & \equiv
&\textsf{false}
\end{array}
$$}
Näide: {$$ \begin{array}{c} \lambda x.\ x =^?_{\emptyset} \lambda y.\ y \\ ||| \\ x =^?_{\{(x,y)\}} y \\ ||| \\ (x,y)\in \{(x,y)\}\\ ||| \\ \textsf{true}\\ \end{array} $$}
{$^*$}) See algoritm on lihtsustus, mis töötab kinniste termide korral. Vabade muutujate {$a, b, c$} olemasolul peaks abistruktuuri lisama {$(a,a), (b, b), (c, c)$} s.t mõlemas termis peavad nad olema sama nimega.
Implementeerige funktsioon Idrises:
lamEq : List (String,String) -> Lam -> Lam -> Bool
lamEq v e1 e2 = ?lamEq_rhs
-- See on liides -- liideseid vaatame järgmises praksis.
Eq Lam where
x == y = lamEq [(x,x)| x <- fvList x ++ fvList y] x y
Selles lahenduses on abiks funktsioon elem.
Proovi REPLis, kas saad samad tulemused, mis 5. ülesandes?
> (==) t1 t2 > (==) t1 t3
7. Tagasiside
Kas teil oli meeles tagasisidet anda? Kommenteerige kindlasti, kui mingi ülesanne võttis ootamatult palju aega.