Functional Programming 2022/23 fall

Kodutöö 5

1. Vabade muutujate leidmine

Leia termidest vabad muutujad!

1. {$ \text{FV}(\lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x))$}
2. {$ \text{FV}((\lambda{}x. (\lambda{}g. g x)) x)$}
3. {$ \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.

import Data.List
-- lookup
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"))))

-- (\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"))))

2. Funktsioon {$\text{FV}$}

Teie ülesanne on defineerida funktsioon hulkadel.

fv : Lam -> SortedSet String
fv e = ?fv_rhs

-- testimiseks on selgem kasutada liste
fvList : Lam -> List String
fvList = SortedSet.toList . fv

3. Substitutsiooni arvutamine

Arvuta substitutsioonid

1. {$ (\lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x))[x \to y]$}
2. {$ ((\lambda{}x. (\lambda{}g. g x)) x)[x\to(\lambda{} x.x)]$}
3. {$ (\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 
  newv xs = xs++"'"

5. {$\alpha$}-võrdsed avaldised

Kas järgnevad termid on {$\alpha$}-võrdsed?

1. {$ \lambda{}f. (\lambda{}g. g x) (\lambda{}x. f x) \;=_\alpha\; (\lambda{}x. (\lambda{}g. g x)) x $}
2. {$ \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:

lamEq : List (String,String) -> Lam -> Lam -> Bool
lamEq 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.