Kodutöö 5
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))
Lambda termide andmestruktuur
NB! looge 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
Nüüd teeme Idrise funktsiooni, mis vabad muutujad leiab. Vaja läheb listi ja hulga andmestruktuure. Defineerime termide andmestruktuuri.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 |
import Data.List-- lookupimport Data.SortedSet-- empty, singleton, insert, delete, contains, uniondata Lam = Var String | App Lam Lam | Abs String LamshowLam : Nat -> Lam -> StringshowLam _ (Var x) = xshowLam 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 : Lamt1 = Abs "f" (App (Abs "g" (App (Var "g") (Var "x"))) (Abs "x" (App (Var "f") (Var "x"))))-- (\x. (\g. g x)) xt2 : Lamt2 = App (Abs "x" (Abs "g" (App (Var "g") (Var "x")))) (Var "x") -- t3 := \g. (\f. f x) (\x. g x) t3 : Lamt3 = Abs "g" (App (Abs "f" (App (Var "f") (Var "x"))) (Abs "x" (App (Var "g") (Var "x")))) |
2. Funktsioon \text{FV}
Teie ülesanne on defineerida funktsioon hulkadel.
1 2 3 4 5 6 |
fv : Lam -> SortedSet Stringfv e = ?fv_rhs-- testimiseks on selgem kasutada listefvList : Lam -> List StringfvList = SortedSet.toList . fv |
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.
1 2 |
subst : Lam -> String -> Lam -> Lamsubst 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 newv xs = xs++"'"
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^* abistruktuuriga 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:
1 2 3 4 5 6 |
lamEq : List (String,String) -> Lam -> Lam -> BoollamEq cs 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 lookup.
7. Tagasiside
Kas teil oli meeles tagasisidet anda? Kommenteerige kindlasti, kui mingi ülesanne võttis ootamatult palju aega.