Funktsionaalprogrammeerimine 2022/23 sügis

Kodutöö 8

Praktikumi teemaks on {$\lambda$}-termide redutseerimine normaalkujule. Konspektis {$\lambda$}-arvutuse peatükist alampeatükid β-reduktsioon ja η-reduktsioon.

Ülesanne 1. Churchi numbritega arvutamine

Väärtusta normaalkujule järgnevad termid:

1. {$\text{add}\ \underline{1}\ \underline{1}$}
2. {$\text{add}\ \underline{0}\ \underline{0}$}
3. {$\text{mul}\ \underline{2}\ \underline{0}$}
4. {$\text{mul}\ \underline{2}\ \underline{3}$}
5. {$\text{exp}\ \underline{2}\ \underline{2}$}
6. {$\text{exp}\ \underline{2}\ \underline{0}$}

Definitsioonid slaidilt:

{$ \begin{array}{lcl} \underline{n} & \equiv & \lambda f\ x.\ f^n\ x \\ \text{succ} & \equiv & \lambda n.\ \lambda f\ x.\ n\ f\ (f\ x) \\ \text{add} & \equiv & \lambda m\ n.\ \lambda f\ x.\ m\ f\ (n\ f\ x) \\ \text{mul} & \equiv & \lambda m\ n.\ \lambda f\ x.\ m\ (n\ f)\ x \\ \text{exp} & \equiv & \lambda m\ n.\ \lambda f\ x.\ n\ m\ f\ x \end{array} $}

Implementeerime redusteerimist:

Andmestruktuurid ja definitsioonid

Esmalt defineerime termid, ja liidesed nende sõneks teisendamiseks ning võrdlemiseks. Lisaks eelneval korral ülesandeks olnud vabade muutujate leidmine ning asendus.

import Data.SortedSet

data Lam  = Var String          -- muutuja
          | App Lam   Lam       -- rakendus
          | Abs String Lam      -- abstraktsioon

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)

Show Lam where
    show = showLam 0

Eq Lam where
    (Var x)   == (Var y)   = x==y
    (App x y) == (App z w) = x==z&&y==w
    (Abs x y) == (Abs z w) = x==z&&y==w
    _         == _         = False


freeVars : Lam -> SortedSet String
freeVars (Var x)   = singleton x 
freeVars (App x y) = freeVars x `union` freeVars y
freeVars (Abs x y) = delete x (freeVars y)

subst : Lam -> String -> Lam -> Lam
subst (Var x) v r = if x==v then r else Var x
subst (App x y) v r = App (subst x v r) (subst y v r)
subst (Abs x y) v r = 
    if v==x then Abs x y 
    else if contains x (freeVars r) then subst (Abs x' (subst y x (Var x'))) v r
    else Abs x (subst y v r)
            where x' : String 
                  x' = x++"'"

Lisaks mõned definitsioonid:

infixl 3 @@
(@@) : Lam -> Lam -> Lam
x @@ y = App x y

true : Lam 
true = Abs "x" (Abs "y" (Var "x"))

false : Lam 
false = Abs "x" (Abs "y" (Var "y"))

cond : Lam 
cond = Abs "t" (Abs "x" (Abs "y" (Var "t" @@ Var "x" @@ Var "y")))


num : Nat -> Lam
num n = Abs "f" (Abs "x" (app_f n)) where 
    app_f : Nat -> Lam
    app_f 0 = Var "x"
    app_f (S k) = (Var "f") @@ (app_f k)

-- (\ x. x x)(\ x. x x)
inf : Lam
inf = Abs "x" (Var "x" @@ Var "x") @@ Abs "x" (Var "x" @@ Var "x")

succ : Lam
succ = Abs "n" (Abs "f" (Abs "x" (Var "n" @@ Var "f" @@ (Var "f" @@ Var "x"))))

add : Lam
add = Abs "m" (Abs "n" (Abs "f" (Abs "x" 
            (Var "m" @@ Var "f" @@ (Var "n" @@ Var "f" @@ Var "x")))))

mul : Lam
mul = Abs "m" (Abs "n" (Abs "f" (Abs "x" 
            (Var "m" @@ (Var "n" @@ Var "f") @@ Var "x"))))

Ülesanne 2. Defineeri astendamine nii, nagu loengus

-- \m n. \ f x. n m f x
expr : Lam
expr = ?expr_rhs

Ülesanne 3: redutseerimine aplikatiivses järjekorras

Kirjuta funktsioon redA, mis redutseerib termi normaalkujule, kasutades aplikatiivjärjekorda.

Vihje: Rakendamise e1 e2 puhul redutseerime e1 normaalkujule. Kui see on lambda, siis asenda lambda kehas termi e2 normaalkujuga ja redutseeri tulemust. Kui polnud lambda, siis jääb termiks funktsiooni rakendamine.

redA : Lam -> Lam
redA (App x y) = ?redA_rhs1
redA (Abs x y) = ?redA_rhs2
redA t = t

näiteks:

(show $ redA (cond @@ true @@ num 2 @@ num 3)) == "\\ f. \\ x. f (f x)"
(show $ redA (add @@ num 2 @@ num 3)) == "\\ f. \\ x. f (f (f (f (f x))))"
show $ redA (cond @@ true @@ num 2 @@ inf)  -- ei termineeru

Ülesanne 4: redutseerimine normaaljärjekorras

Kirjutame funktsioon redN, mis redutseerib termi normaalkujule, kasutades normaaljärjekorda.

Lihtne lahendus ei väärtusta päris normaaljärjekorras:

redNx : Lam -> Lam    
redNx (App x y) = 
    case redNx x of
      Abs z t => redNx (subst t z y)
      nx      => App nx (redNx y)
redNx (Abs x y) = Abs x (redNx y)
redNx t = t

Esiteks vajame abifunktsiooni, mis termi n.n. nõrgale peanormaalkujule. See on nagu normaalkuju aga ei väärtusta lambda all ega rakenduse argumenti. S.t. vaid beeta-reduktsioon ja lihtsustame vaid rakenduse funktsiooni osa

redNwhnf : Lam -> Lam    
redNwhnf t = ?redNwhnf_rhs

Praktilises keeltes rohkem vaja ei olegi. Aga Churchi numbrite evalueerimiseks peame viima päris normaalkujule ...

redN : Lam -> Lam redN (App x y) = ?redN_rhs1 redN (Abs x y) = ?redN_rhs2 redN t = t (:codeend:)

näiteks:

(show $ redN (cond @@ true @@ num 2 @@ num 3)) == "\\ f. \\ x. f (f x)"
(show $ redN (add @@ num 2 @@ num 3)) == "\\ f. \\ x. f (f (f (f (f x))))"
(show $ redN (cond @@ true @@ num 2 @@ inf))  == "\\ f. \\ x. f (f x)"

Väga hea aga tahame näha samme!

Ülesanne 5: aplikatiivjärjekorras esimese reedeksi leidmine

Kirjuta funktsioon redA1, mis teeb ühe reduktsioonisammu, kasutades aplikatiivjärjekorda. Kui sammu teha ei saa, siis Nothing.

Vihje: Rakendamise e1 e2 puhul tuleb lahendusse kolm üksteise sees olevat case-of-i. S.t. esmalt proovime teha sammu e1-s, kui see ei õnnestu, siis e2-s. Kui e2-s ei õnnestu sammu teha, siis vaatame, kas see on lambda.

redA1 : Lam -> Maybe Lam
redA1 (App x y) = ?redA1_rhs1
redA1 (Abs x y) = ?redA1_rhs2
redA1 t = ?redA1_rhs3

-- testimiseks trükime välja kõi sammud.
printSteps : (Lam -> Maybe Lam) -> Lam -> IO ()
printSteps f l = 
    case f l of
        Nothing => printLn l
        Just l' => do printLn l
                      printSteps f l'

näiteks:

(show (redA1 (num 3))) == "Nothing"
(show (redA1 (cond @@ false))) == "Just \\ x. \\ y. (\\ x. \\ y. y) x y"
(show (redA1 (succ @@ num 0))) == "Just \\ f. \\ x. (\\ f. \\ x. x) f (f x)"
(show (redA1 (add @@ (succ @@ (num 0)) @@ num 0))) == "Just (\\ m. \\ n. \\ f. \\ x. m f (n f x)) (\\ f. \\ x. (\\ f. \\ x. x) f (f x)) (\\ f. \\ x. x)"

Ülesanne 6: normaaljärjekorras esimese reedeksi leidmine

Kirjuta funktsioon redN1, mis teeb ühe reduktsioonisammu, kasutades normaaljärjekorda. Kui sammu teha ei saa, siis Nothing.

Vihje: Rakendamise e1 e2 puhul tuleb ka seekord lahendusse kolm üksteise sees olevat case-of-i. Aga nüüd kontrollime esmalt, kas e1 on lambda.

redN1 : Lam -> Maybe Lam
redN1 (App x y) = ?redN1_rhs1
redN1 (Abs x y) = ?redN1_rhs2
redN1 t = ?redN1_rhs3

näiteks:

(show (redN1 (num 3))) == "Nothing"
(show (redN1 (cond @@ false))) == "Just \\ x. \\ y. (\\ x. \\ y. y) x y"
(show (redN1 (succ @@ num 0))) == "Just \\ f. \\ x. (\\ f. \\ x. x) f (f x)"
(show (redN1 (add @@ (succ @@ (num 0)) @@ num 0))) == "Just (\\ n. \\ f. \\ x. (\\ n. \\ f. \\ x. n f (f x)) (\\ f. \\ x. x) f (n f x)) (\\ f. \\ x. x)"

Tärnülesanne: Väärtustamine kitsamas mõttes

Evaluatsioon ehk väärtustamine tähistab meetodit, kus igale termile seatakse vastavusse (s.t. funktsioon) üks matemaatiline objekt.

Nii tahame mööda hiilida substitutsioonidest. Suurte termide teisendamine on aeglane!

Praktikas, kus kasutatakse konstantidega lambda-arvutust, aplikatiivjärjekorda ja kinniseid terme, on see väga lihtne. Lambdad teisendatakse funktsioonideks ja konstandid konstantideks.

Puhta lambda-arvutuse puhul on vaja rohkem vaeva näha:

data Val = FVal (Val -> Val)    -- lambdade jaoks funktsioonid
         | GVar String          -- vabade muutujatejaoks globaalid
         | GApp Val Val         -- vabale muutujale rakenduse jaoks see
         | LazyVal (() -> Val)  -- laiskuse jaoks see

(aplikatiivjärjekorra jaoks ole LazyVal-i vaja)

Kuna puhta lambda-arvutuse väärtused on lambda-termid, peame väärtustamise järel tegema need jälle termideks. Kuna muutujate nimed läksid kaotsi, genereerime uued.

var2lam : Nat -> Val -> (Lam, Nat)
var2lam n (LazyVal f) = var2lam n (f ())
var2lam n (GVar x) = (Var x, n)
var2lam n (GApp f x) = 
    let (fl,n1) = var2lam n f in
    let (xl,n2) = var2lam n1 x in
    (App fl xl, n2)
var2lam n (FVal f) = 
    let (b,n1) = var2lam (n+1) (f (GVar x)) in
    (Abs x b, n1)
        where x : String
              x = "x"++show n

Asendamise asemel kasutame seisundeid

data Env = Empty | InsertEnv String Val Env

lookupEnv : String -> Env -> Maybe Val
lookupEnv n Empty             = Nothing
lookupEnv n (InsertEnv x y z) = if n==x then Just y else lookupEnv n z

Näitena on toodud väärtustamine normaaljärjekorras. See on keerukam. Hiljem on teie ülesandeks teha aplikatiivjärjekorras väärtustaja.

-- funktsioon, mis väärtustab laisad väärtused
evalLazy : Val -> Val
evalLazy (LazyVal f) = evalLazy (f ())
evalLazy t = t

-- normaaljärjekorras väärtustamine
evalN : Lam -> (Env -> Val)
evalN (Var x) env = 
    case lookupEnv x env of
        -- kohalike muutujate jaoks väärtused leiduvad
        Just e  => e    
        -- vabade muutujate jaoks mitte
        Nothing => GVar x
evalN (App f y) env = 
    -- esmalt peame väärtustama f-i, isegi kui see on laisk väärtus
    case evalLazy (evalN f env) of 
      -- kui f oli funktsioon, siis kutsume selle välja
      -- normaaljärjekorra puhul on argument LazyVal
      FVal xf => xf (LazyVal (\ () => evalN y env))
      -- kui f pole funktsioon, kasutame GApp-i
      -- normaaljärjekorra puhul on argument ikka LazyVal
      f       => GApp f (LazyVal (\ () => evalN y env))
evalN (Abs x y) env = 
    -- lambdale vastab funktsioon
    -- lambda kehas lisame argumendi seisundisse
    FVal (\\ xv => evalN y (InsertEnv x xv env))

-- alustame tühja seisundiga ning muutujaid x0-ga 
-- hiljem viskame loenduri ära
evalNLam : Lam -> Lam
evalNLam e = fst (var2lam 0 (evalN e Empty))

(show $ evalNLam (add @@ num 2 @@ num 3)) == "\\ x0. \\ x1. x0 (x0 (x0 (x0 (x0 x1))))"
(show $ evalNLam (cond @@ true @@ num 2 @@ inf)) == "\\ x0. \\ x1. x0 (x0 x1)"

Teie ülesanne on kirjutada aplikatiivjärjekorras väärtustaja! Sisuline erinevus on laiskuse puudumises.

evalA : Lam -> (Env -> Val)
evalA (Var x) env =  ?evalA_rhs_1
evalA (App x y) env = ?evalA_rhs_2
evalA (Abs x y) env = ?evalA_rhs_3

evalALam : Lam -> Lam
evalALam e = fst (var2lam 0 (evalA e Empty))

(show $ evalALam (add @@ num 2 @@ num 3)) == "\\ x0. \\ x1. x0 (x0 (x0 (x0 (x0 x1))))"

Pange tähele!

1. Evaluaatorid on väga kiired, lihtsad ja lühikesed.
2. Praktiliste keelte jaoks pole enamasti var2lam-i vaja.
3. Siin jõuab keelte teooria kompilaatorite praktikale peaaegu järele kuna FVal vastab genereeritud masinkoodi-(viida)-le ja Env funktsiooni call-stack-(viida)le.