Funktsionaalprogrammeerimine - Kursused

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.

Funktsionaalprogrammeerimine 2023/24 sügis