Funktsionaalprogrammeerimine - Kursused

6. - 7. Praktikum

Vahekontrolltöö näidisülesanded

Esimese kontrolltöö näidisülesandeid saad vaadata siit: Kt1_pre.idr

Praktikumide teemaks on {$\lambda$}-termide redutseerimine normaalkujule.

Lisalugemine (vabatahtlik):

Type-Driven development with Idris peatükid:

Chapter 12. Writing programs with state, sissejuhatus ja alampeatükid:
- 12.1. Working with mutable state
  - 12.1.1. The tree-traversal example
  - 12.1.2. Representing mutable state using a pair
  - 12.1.3. State, a type for describing stateful operations
  - 12.1.4. Tree traversal with State
- 12.2. A custom implementation of State
  - 12.2.1. Defining State and runState
  - 12.2.2. Defining Functor, Applicative, and Monad implementations for State

Kasutame järgnevaid abimooduleid (panna samasse kataloogi kui praksi lahenduse fail, ei tule Moodle-s esitada):

Set.idr

Defineeritakse tüübid Set a, kus a on hulga elementide tüüp. On defineeritud tühi hulk empty, üheelemendiline hulk single, sisalduvuse kontroll mem, ühe elemendi lisamine add, ühe elemendi eemaldamine delete, hulga lahutamine (\\), foldl, foldr, teisendamised listiks ja listist listToSet, setToList, cast, ühend union, suurus size, võrdsus läbi Eq tüübiklassi instantsi.

Sisemiselt on hulgad listid, aga väljastpoolt vaadates on tegemist abstraktse andmetüübiga. S.t. peab kasutama eelnevalt nimetatud funktsioone ja väärtuseid.

StateT.idr

Defineeritakse seisunditeisendusmonaadi jaoks tüübid St m s a. Parameeter m peab olema mingi monaadi tüüp (Monad instants, näiteks IO, Maybe, List). Parameeter s on seisundi tüüp. Parameeter a on seisundi-teisendis-monaadi tagastustüüp.

Seisunditeisendusmonaadi kasutatakse selleks, et varjata seisundi eksplitsiitset edastamist läbi funktsiooni parameetrite. Ettenägelikult seisundimonaadi kasutades, ei pea seisundi andmestruktuuri muutumisel (kui on seisundisse midagi vaja lisada) igat funktsiooni refaktoreerima. Nii (ka monaadidega üldiselt) saab kirjutada ilusamat koodi, kus programmi kõrgem loogika on eraldatud madalamatest detailidest.

St-l on defineeritud monaadi operatsioonid (saame kasutada do-süntaksit)

pure : Monad m => a -> St m s a
(>>=) : Monad m => St m s a -> (a -> St m s b) -> St m s b

Operatsiooni (>>=) enamasti käsitsi ei kasuta, vaid kasutame do-süntaksit. Aga pure kasutatakse tihti do-avaldise viimase lausena, et arvutatud puhast väärtust tagastada.

Lisaks seisundimonaadi spetsiifilised funktsioonid:

get : Monad m => St m s s s.t. st <- get seob nime st tolle hetke seisundga
set : Monad m => s -> St m s () s.t. set d seab uueks seisundi väärtuseks d
update : Monad m => (s -> s) -> St m s () -- update f muudab seisundit funktsiooniga f

Andmestruktuurid ja definitsioonid

Esmalt defineerime termid, ja liidesed nende sõneks teisendamiseks ning võrdlemiseks:

import Set
import StateT

data Term = Var String          -- Var "x"    ===  x
          | App Term   Term     -- App f e    ===  f e
          | Lam String Term     -- Lam "x" e  ===  \ x. e
          | Con Int             -- Con 5      ===  5

showTerm : Nat -> Term -> String
showTerm _ (Con n)   = show n
showTerm _ (Var x)   = x
showTerm d (App f e) = 
    showParens (d>1) (showTerm 1 f++" "++showTerm 2 e)
showTerm d (Lam x e) = 
    showParens (d>0) ("\\ "++x++". "++showTerm 0 e)

Show Term where
    show = showTerm 0

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

Näiteks ja testimiseks on sellised termid:

tI : Term    -- show tI == "\ a. a"
tI = Lam "a" (Var "a")

tK : Term    -- show tK == "\ a. \ b. a"
tK = Lam "a" (Lam "b" (Var "a"))

tS : Term    -- show tS == "\ a. \ b. \ c. a c (b c)"
tS = Lam "a" (Lam "b" (Lam "c" 
        (App (App (Var "a") (Var "c")) 
            (App (Var "b") (Var "c")))))

test : Term   -- "(\ a. \ b. \ c. a c (b c)) (\ a. a) (\ a. a) (\ a. a)"
test = App (App (App tS tI) tI) tI

test1 : Term  -- "(\ a. a) ((\ b. b) (\ c. c))"
test1 = (Lam "a" (Var "a")) `App` 
    ((Lam "b" (Var "b")) `App` (Lam "c" (Var "c")))

add : Term -> Term -> Term
add x y = App (App (Var "add") x) y

test2 : Term  -- show test2 == "add 1 2"
test2 = add (Con 1) (Con 2)

test3 : Term  -- "add (add 1 2) (add (add 1 1) 3)"
test3 = add (add (Con 1) (Con 2)) (add (add (Con 1) (Con 1)) (Con 3))

test4 : Term  -- show test4 == "(\ x. add x x) (add 1 2)"
test4 = App (Lam "x" (add (Var "x") (Var "x"))) (add (Con 1) (Con 2))

selfapp : Term
selfapp = Lam "y" (App (Var "y") (Var "y"))

test5 : Term  -- "(\ x. 5) ((\ y. y y) (\ y. y y))"
test5 = App (Lam "x" (Con 5)) (App selfapp selfapp)

test6 : Term  -- show test6 == "\ x. y"
test6 = Lam "x" (Var "y")

test7 : Term  -- show test7 == "(\ a. a) 5"
test7 = App tI (Con 5)

Tüüpimata {$\lambda$}-termide reduktsioon

Ülesanne 1: vabade muutujate leidmine

Funktsioon freeVars tagastab igale termile vastava vabade muutujate hulga.

freeVars : Term -> Set String
freeVars t = ?fv1

Näiteks:

freeVars (Con 5) == empty
freeVars test2 == listToSet ["add"]

Ülesanne 2: esimest järku termide väärtustamine

Abistruktuur: kujutis sõnedest tüüpi a. Kasutame seda andmestruktuuri muutujate seisundite hoidmiseks.

SMap : Type -> Type
SMap a = String -> Maybe a

emptyMap : SMap a
emptyMap _ = Nothing

addFunMap: Eq a => String -> a -> SMap a -> SMap a
addFunMap x v m y = if x==y then Just v else m y

Uurige järgnevat funktsiooni (funktsioon eksplitsiitse seisundiga):

evalSimple1 : SMap Int -> Term -> Maybe Int
evalSimple1 r (Var x) = r x
evalSimple1 r (App (App (Var "add") x) y) = 
    do xv <- evalSimple1 r x
       yv <- evalSimple1 r y
       pure (xv+yv)
evalSimple1 r (App (Lam x z) y) = 
    do v <- evalSimple1 r y
       evalSimple1 (addFunMap x v r) z
evalSimple1 r (Con x) = pure x
evalSimple1 r _  = Nothing

Kirjutage evalSimple2, mis teeb sama arvutust seisundimonaadiga:

fail : St Maybe a b
fail = MkSt (\z => Nothing)

getVar : String -> St Maybe (SMap Int) Int
getVar x = do r <- get
              case r x of
                Nothing  => fail
                (Just x) => pure x

evalSimple2 : Term -> St Maybe (SMap Int) Int
evalSimple2 (Var x) = ?es1
evalSimple2 (App (App (Var "add") x) y) = ?es2
evalSimple2 (App (Lam x z) y) = ?es3
evalSimple2 (Con x) = ?es4
evalSimple2 _ = ?es5

Näiteks:

map fst (runSt (evalSimple2 test2) emptyMap) == Just 3
map fst (runSt (evalSimple2 test3) emptyMap) == Just 8
map fst (runSt (evalSimple2 (App tI test2)) emptyMap) == Just 3

Esimese näite selgitus. Tahame testida evalSimple2 termil test2. Selleks on vaja see arvutus käivitada mingi muutujate algseisundiga. Kuna test2 on kinnine, pole vahet mis seisundi võtame. Kasutame näiteks tühja map-i. Seega: runSt (evalSimple2 test2) emptyMap. Tulemuseks on väärtus tüübiga Maybe (Int, SMap Int). Tahame kontrollida, et see väärtus oleks Just ning paari esimene komponent oleks kolm (kuna 1+2==3). Teist komponenti siin ei kontrolli -- seega teeme map fst, et paari teine komponent lõpptulemusest eemaldada.

PS! Tegelikult tuleks siin kasutada n.n. Reader monaadi. Seisundimonaadiga peab selles ülesandes peale lambda keha töötlemist lambda eelse seisundi taastama.

Ülesanne 3: "värske muutuja" loomine

Muutuja kujul xn, kus n on seisundi loenduri väärtus. Lisaks tuleb seisundi loendurit suurendada ühe võrra.

newVar : St Maybe Int String
newVar = ?nvst1

Näiteks:

runSt newVar 0 == Just ("x0", 1)
runSt newVar 2 == Just ("x2", 3)
runSt (do {x <- newVar; y <- newVar; pure (x++y)}) 1 == Just ("x1x2", 3)

Esimese näite selgitus. Seisunditeisendusmonaadi arvutus newVar käivitatakse algseisundiga 0. Arvutus tagastab "x0" ja lõppseisund on 1.

Ülesanne 4: substitutsioon

(Vaata loengu slaide!)

substSt : Term -> (String, Term) -> St Maybe Int Term
substSt t (x,e) = subst' t
    where fvs : Set String
          fvs = freeVars e 
          subst' : Term -> St Maybe Int Term
          subst' (Con y) = ?subst1
          subst' (Var y) = ?subst2
          subst' (App y z) = ?subst3
          subst' (Lam y e1) = ?subst4

näiteks:

runSt (substSt tI ("a", tK)) 0 == Just (tI, 0)
runSt (substSt test6 ("y", Var "x")) 0 == Just (Lam "x0" (Var "x"), 1)

Teise näite selgitus. Termis test6 (\ x. y) asendatakse muutuja y muutujaga x. Kuna arvutuse substSt seisundi tüüp on Int, peame andma täisarvulise algseisu. Näiteks võtame (runSt teiseks argumendiks) algseisundiks 0. Ootame, et arvutus õnnestuks (Just), et lõppseisundiks oleks 1 ja tagastusväärtus oleks \ x0. x.

Ülesanne 5: reedeks olemise predikaat

Test, kas kogu term on reedeks. Esialgu piisab lambda rakendusest ja liitmisest. Vaja kontrollida, kas term on beeta- või delta-reedeks. Beeta-reedeks on kujul (\ x. t1) t2, kus x on suvaline muutuja ja t1 ning t2 suvalised termid. Delta-reedeks on kujul add x y, kus x ja y on konstandid.

canContract : Term -> Bool
canContract t = ?cc1

näiteks:

canContract test2 == True
canContract test3 == False
canContract test4 == True
canContract test5 == True

Ülesanne 6: reedeksi redutseerimine

Eelnevas ülesandes kirjeldatud reedeksite redutseerimine (üks samm). Kui kogu term pole reedeks, siis nurjumine (fail).

contract : Term -> St Maybe Int Term
contract t = ?c1

näiteks:

runSt (contract test2) 0 == Just (Con 3, 0)
runSt (contract test3) 0 == Nothing
runSt (contract test4) 0 == Just (add (add (Con 1) (Con 2)) (add (Con 1) (Con 2)),0)

Käivitades contract test2 algseisundis 0, tagastatakse Con 3; lõppseisund on samuti 0. Käivitades contract test3 algseisundis 0, toimub nurjumine -- tegemist pole reedeksiga.

Ülesanne 7: aplikatiivjärjekorras esimese reedeksi leidmine

Tagastatava paari esimene komponent on reedeks; teine komponent on kontekst. Implementeerimiseks kasutada case-of konstruktsiooni ning canContract funktsiooni.

Kontekst arvutatakse rekursiivsest kutsest tagasitulevale reedeksile. Näiteks, kui vaatluse all on term T=Lam x E, ja focusA E == Just (r, c), ehk termi E reedeks on r ja kontekst c. Siis termi T jaoks on reedeks r aga kontekst \z => Lam x (c z).

Aplikatiivjärjekord: alati redutseerida vasakpoolne sisemine reedeks.

focusA : Term -> Maybe (Term, Term -> Term)
focusA t = ?fa1

näiteks:

map fst (focusA test7) == Just test7
map fst (focusA test2) == Just test2
map fst (focusA test4) == Just (add (Con 1) (Con 2))
(map snd (focusA test4) <*> Just (Con 3)) == Just (App (Lam "x" (add (Var "x") (Var "x"))) (Con 3))
map fst (focusA test5) == Just (App selfapp selfapp)
(map snd (focusA test5) <*> Just (Con 0)) == Just (App (Lam "x" (Con 5)) (Con 0))

Selgitus. Aplikatiivjärjekorras on test7 ja test2 puhul vaja teha reduktsioon kogu termile. Kuna (==) pole defineeritud funktsioonide peale, peame map fst-ga kontekstid (mis peaks olema identsusfunktsioonid) ära viskama. Neljas test kontrollib konteksti paikapidavust test4 korral -- aga kuna funktsioon on Maybe tüübi sees, ei saa argumenti otse anda, vaid peab tegema rakenduse ka Maybe all.

Ülesanne 8: normaaljärjekorras esimese reedeksi leidmine

Paari esimene komponent on reedeks; teine komponent on kontekst. Sarnaselt eelmisele ülesandele, aga normaaljärjekorras.

Normaaljärjekord: alati redutseerida vasakpoolne väline reedeks.

focusN : Term -> Maybe (Term, Term -> Term)
focusN t = ?fn1

näiteks:

map fst (focusN test7) == Just test7
map fst (focusN test2) == Just test2
map fst (focusN test4) == Just test4
map fst (focusN test5) == Just test5
map fst (focusN (Lam "x" test2)) == Just test2

Ülesanne 9: üks lihtsustussamm

Otsib redutseeriva avaldise, redutseerib selle ja paneb selle konteksti tagasi.

step : (Term -> Maybe (Term, Term -> Term)) -> Term -> St Maybe Int Term
step focus t = ?st1

näiteks:

runSt (step focusN test2) 0 == Just (Con 3, 0)
runSt (step focusA test2) 0 == Just (Con 3, 0)
runSt (step focusN test5) 0 == Just (Con 5, 0)
runSt (step focusA test5) 0 == Just (test5, 0)

Testimine

Võttes argumendiks lihtsustussammu funktsiooni, trükib termi lihtsustamise sammud kuni normaalkujuni välja.

printRed : (Term -> St Maybe Int Term) -> Term -> IO ()
printRed step t = do printLn t
                     runSteps t 0
    where runSteps : Term -> Int -> IO ()
          runSteps t n = 
            case runSt (step t) n of
              Just (e', n') => do printLn e'
                                  runSteps e' n'
              _ => pure ()

Kutsuda näiteks nii:

  :exec printRed (step focusA) test1

või

  :exec printRed (step focusN) test1

Refocus*

Probleem: reduktsioon pole efektiivne, kuna kogu aeg tuleb terme lahti võtta ja uuesti kokku panna.

Olivier Danvy: Pole vaja kokku panna, kui kontekst teha andmestruktuuriks.

data Ctx = CNil | CApp1 Term Ctx
         | CApp2 Term Ctx | CLam String Ctx

Ctx on nagu list instruktsioone, kuidas andmestruktuuri ehitada.

  (\z -> Lam "x" (App a (App z b))) == CApp1 b (CApp2 a (CLam "x" CNil))

Ülesanne 10*: kontekti paigutamine

Harjutamiseks implementeerige konteksti tagasi paigutamine.

plug : Term -> Ctx -> Term 
plug t c = ?pl1

näiteks:

plug tI CNil == tI
plug tI (CApp1 tS CNil) == App tI tS
plug tI (CApp2 tS CNil) == App tS tI
plug tI (CApp1 (Var "b") (CApp2 (Var "a") (CLam "x" CNil))) == Lam "x" (App (Var "a") (App tI (Var "b")))

Ülesanne 11*: aplikatiivse järjekorra järgmise reedeksi otsimine

Tänu kontekstile saab termi AST-is liikuda nii sissepoole kui väljapoole:

Sisse: teeme termi väiksemaks (mustrisobitusega) ja konteksti rekursiivsel kutsel suuremaks.
Välja: teeme konteksti väiksemaks (mustrisobitusega) ja termi rekursiivsel kutsel suuremaks.

Aplikatiivne järjekord: peale applikatsiooni (funktsiooni ja) argumendi redutseerimist (väljapoole faasis) kontrollime kas vastav aplikatsioon on reedeks.

mutual 
    -- astub termis "väljapoole"
    refocusAaux : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusAaux t c = ?rfa1

    -- astub termis "sissepoole"
    refocusA : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusA t c = ?rfa2

Ülesanne 12*: normaaljärjekorra järgmise reedeksi otsimine

canContract asemel on natuke keerukam funktsioon, kuna peame {$\beta$}-reduktsiooni tegema esimesel võimalusel -- ja neid võimalike kohti on rohkem.

getRedexN : Term -> Ctx -> Maybe (Term, Ctx)
getRedexN (Con b) (CApp2 (App (Var "add") (Con a)) c) = 
    Just ((Var "add" `App` Con a) `App` Con b, c)
getRedexN (Var "add") (CApp1 (Con a) (CApp1 (Con b) c)) = 
    Just ((Var "add" `App` Con a) `App` Con b, c)
getRedexN (Var "add" `App` Con a) (CApp1 (Con b) c) = 
    Just ((Var "add" `App` Con a) `App` Con b, c)
getRedexN ((Var "add" `App` Con a) `App` Con b) c = 
    Just ((Var "add" `App` Con a) `App` Con b, c)
getRedexN (Lam z x) (CApp1 y c) = 
    Just (Lam z x `App` y, c) 
getRedexN (Lam z x `App` y) c = 
    Just (Lam z x `App` y, c) 
getRedexN _ _ = 
    Nothing

Normaaljärjekord: igal sammul (nii sisse kui välja) peame kontrollima getRedexN-ga, kas juba saame redutseerida. Muidu termi läbimine sarnaselt aplikatiivjärejekorrale.

mutual 
    -- astub termis "väljapoole", kontroll getRedexN-ga
    refocusNaux : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusNaux t c = ?rfna1

    -- eeldus, et getRedexN nurjus
    refocusNaux' : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusNaux' t c = ?rfna2

    -- astub termis "sissepoole", kontroll getRedexN-ga
    refocusN : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusN t c = ?rfn1

    -- eeldus, et getRedexN nurjus
    refocusN' : Term -> Ctx -> St Maybe Int (Term, Ctx)
    refocusN' t c = ?rfn2

Testimine

Võttes argumendiks lihtsustussammu funktsiooni, trükib termi lihtsustamise sammud kuni normaalkujuni välja.

printRed' : (Term -> Ctx -> St Maybe Int (Term, Ctx)) -> Term -> IO ()
printRed' focus t = do printLn t
                       runSteps t CNil 0
    where focus_beta : Term -> Ctx -> St Maybe Int (Term, Ctx)
          focus_beta t c = do (e,c') <- focus t c
                              e' <- contract e
                              pure (e', c')
          runSteps : Term -> Ctx -> Int -> IO ()
          runSteps t c n = 
            case runSt (focus_beta t c) n of
              Just ((e', c'), n') => do printLn (plug e' c')
                                        runSteps e' c' n'
              _ => pure ()

Kutsuda näiteks nii:

  :exec printRed' refocusA test1

või

  :exec printRed' refocusN test1

Funktsionaalprogrammeerimine 2021/22 sügis

6. - 7. Praktikum

Vahekontrolltöö näidisülesanded

Lisalugemine (vabatahtlik):

Set.idr

StateT.idr

Andmestruktuurid ja definitsioonid

Tüüpimata {$\lambda$}-termide reduktsioon

Ülesanne 1: vabade muutujate leidmine

Ülesanne 2: esimest järku termide väärtustamine

Ülesanne 3: "värske muutuja" loomine

Ülesanne 4: substitutsioon

Ülesanne 5: reedeks olemise predikaat

Ülesanne 6: reedeksi redutseerimine

Ülesanne 7: aplikatiivjärjekorras esimese reedeksi leidmine

Ülesanne 8: normaaljärjekorras esimese reedeksi leidmine

Ülesanne 9: üks lihtsustussamm

Testimine

Refocus*

Ülesanne 10*: kontekti paigutamine

Ülesanne 11*: aplikatiivse järjekorra järgmise reedeksi otsimine

Ülesanne 12*: normaaljärjekorra järgmise reedeksi otsimine

Testimine