diff options
Diffstat (limited to 'ws2015/ffp/blaetter/04')
| -rw-r--r-- | ws2015/ffp/blaetter/04/FFP_U04_Lazy.hs | 543 |
1 files changed, 543 insertions, 0 deletions
diff --git a/ws2015/ffp/blaetter/04/FFP_U04_Lazy.hs b/ws2015/ffp/blaetter/04/FFP_U04_Lazy.hs new file mode 100644 index 0000000..36c0578 --- /dev/null +++ b/ws2015/ffp/blaetter/04/FFP_U04_Lazy.hs | |||
| @@ -0,0 +1,543 @@ | |||
| 1 | -- Fortgeschrittene Funktionale Programmierung, | ||
| 2 | -- LMU, TCS, Wintersemester 2015/16 | ||
| 3 | -- Steffen Jost, Alexander Isenko | ||
| 4 | -- | ||
| 5 | -- Übungsblatt 04. 11.11.2015 | ||
| 6 | -- | ||
| 7 | -- Thema: | ||
| 8 | -- | ||
| 9 | -- Anweisung: | ||
| 10 | -- Gehen Sie diese Datei durch und bearbeiten Sie | ||
| 11 | -- alle Vorkommen von undefined bzw. die mit -- !!! TODO !!! | ||
| 12 | -- markierten Stellen. Testen Sie Ihre Lösungen mit GHCi! | ||
| 13 | -- | ||
| 14 | -- | ||
| 15 | |||
| 16 | import qualified Data.Map as Map | ||
| 17 | import Data.Map (Map) | ||
| 18 | import qualified Data.Set as Set | ||
| 19 | import Data.Set (Set) | ||
| 20 | import qualified Data.List as List ((\\)) | ||
| 21 | |||
| 22 | import Data.Maybe (fromMaybe) | ||
| 23 | import Data.Tuple (swap) | ||
| 24 | |||
| 25 | import Control.Applicative (Applicative(..), (<$>)) | ||
| 26 | |||
| 27 | ---- A4-1 Verzögerte Auswertung | ||
| 28 | -- Gegeben ist folgendes Programm: | ||
| 29 | xs = [1..] | ||
| 30 | foo x = 2 * x | ||
| 31 | ys = foo <$> xs | ||
| 32 | rs = take 1 $ drop 1 ys | ||
| 33 | |||
| 34 | {-Skizzieren Sie mit Papier und Bleistift, | ||
| 35 | wie am Ende der Speicher aussieht, wenn lediglich | ||
| 36 | rs | ||
| 37 | ausgewertet wurde (z.B. durch Anzeige am Bildschirm). | ||
| 38 | |||
| 39 | Welche Strukturen gibt es im Speicher? | ||
| 40 | Wie viele Thunks befinden sich noch im Speicher? | ||
| 41 | Auf welche Adressen zeigen xs, ys, rs in den von Ihnen skizzierten Speicher? | ||
| 42 | |||
| 43 | Hinweise: | ||
| 44 | - An jeder Speicheraddresse sollte sich entweder ein Thunk (also ein Programmausdruck) | ||
| 45 | oder ein Wert befinden. | ||
| 46 | - Für Datentypen wird der Wert dargestellt als Tupel aus Konstruktor | ||
| 47 | und den Speicheraddressen seiner Argumente. | ||
| 48 | - Funktionsdefinitonen lassen wir zur Vereinfachung aus dem Speicher heraus. | ||
| 49 | - Speicheraddressen dürfen Sie völlig willkürlich wählen | ||
| 50 | |||
| 51 | BEISPIEL: | ||
| 52 | |||
| 53 | -- Programm: | ||
| 54 | zs = [27..] | ||
| 55 | ts = take 1 $ drop 2 zs | ||
| 56 | x = head ts | ||
| 57 | |||
| 58 | -- Nach Auswertung von x haben wir den Zustand: | ||
| 59 | |||
| 60 | [ <01>,(:),<11>,<02> | <02>,(:),<12>,<03> | <03>,(:),<13>,<04> | <04>,"[30..]" | ||
| 61 | | <11>,Int,27 | <12>,Int,27+1 | <13>,Int,29 | ||
| 62 | | <21>,(:),<13>,<22> | <22>,[] | ||
| 63 | ] | ||
| 64 | |||
| 65 | Thunks: <04>,<12> | ||
| 66 | |||
| 67 | zs -> <01> | ||
| 68 | ts -> <21> | ||
| 69 | x -> <13> | ||
| 70 | -} | ||
| 71 | |||
| 72 | {- | ||
| 73 | |||
| 74 | | 10 | (:) 1 <30> | | ||
| 75 | | 20 | [3..] | | ||
| 76 | | 30 | (:) 2 <20> | | ||
| 77 | | 40 | (:) <50> <60> | | ||
| 78 | | 50 | (*) 2 <20> | | ||
| 79 | | 60 | 4 | | ||
| 80 | | 61 | (<$>) ((*) 2) <20> | | ||
| 81 | | 70 | (:) <60> <71> | | ||
| 82 | | 71 | [] | | ||
| 83 | |||
| 84 | Thunks: 20, 50, 61 | ||
| 85 | |||
| 86 | xs = <10> | ||
| 87 | ys = <40> | ||
| 88 | rs = <70> | ||
| 89 | |||
| 90 | -} | ||
| 91 | |||
| 92 | |||
| 93 | ---- A4-2 Zirkularität | ||
| 94 | -- a) | ||
| 95 | -- Schreiben Sie ein zirkuläres Programm transcl, | ||
| 96 | -- welches zu einer gegebenen Relation r :: a -> [a] | ||
| 97 | -- und einer als Liste gegebenen Menge, | ||
| 98 | -- die transitive Hülle dieser Menge zu der Relation berechnet. | ||
| 99 | -- | ||
| 100 | -- Eine Relation r :: a -> [a] ist dabei so kodiert, | ||
| 101 | -- das r x die Menge aller Elemente ist, welche zu x in Relation stehen. | ||
| 102 | -- | ||
| 103 | -- HINWEIS: | ||
| 104 | -- Das Ergebnis soll eine Menge modellieren, es darf also kein Element | ||
| 105 | -- doppelt vorkommen. Die Reigenfolge der Elemente in der Liste ist aber egal. | ||
| 106 | -- | ||
| 107 | -- BEISPIELE: | ||
| 108 | -- | ||
| 109 | -- > transCl rel1 [22] | ||
| 110 | -- [33,44] | ||
| 111 | -- > transCl rel1 [2,5] | ||
| 112 | -- [2,5,4,6,8,1,3,7,9] | ||
| 113 | -- | ||
| 114 | -- > sort $ transCl rel2 [42,8,9] | ||
| 115 | -- [1,2,4,5,7,8,9,10,11,13,14,16,17,20,21,22,26,28,32,34,40,42,52,64] | ||
| 116 | -- | ||
| 117 | -- HINWEIS: Folgen Sie dem nub2 Beispiel aus Folie 3-30 | ||
| 118 | |||
| 119 | |||
| 120 | transCl :: Eq a => (a -> [a]) -> [a] -> [a] | ||
| 121 | transCl r xs = res | ||
| 122 | where | ||
| 123 | res = build xs 0 | ||
| 124 | |||
| 125 | build [] _ = [] | ||
| 126 | build xs n = xs' ++ build xs' (n + length xs') | ||
| 127 | where | ||
| 128 | xs' = strikeKnown n $ concatMap r xs | ||
| 129 | |||
| 130 | strikeKnown _ [] = [] | ||
| 131 | strikeKnown 0 xs = xs | ||
| 132 | strikeKnown n (x:xs) | ||
| 133 | | x `elem` take n res = strikeKnown n xs | ||
| 134 | | otherwise = x : strikeKnown n xs | ||
| 135 | |||
| 136 | -- Zum Testen: | ||
| 137 | rel1 :: Integer -> [Integer] | ||
| 138 | rel1 11 = [22] | ||
| 139 | rel1 22 = [33] | ||
| 140 | rel1 33 = [44] | ||
| 141 | rel1 n | ||
| 142 | | even n, n>=1, n<=9 = [2,4,6,8] | ||
| 143 | | odd n, n>=1, n<=9 = [1,3,5,7,9] | ||
| 144 | | otherwise = [n] | ||
| 145 | |||
| 146 | rel1S :: Integer -> Set Integer | ||
| 147 | rel1S = Set.fromList . rel1 | ||
| 148 | |||
| 149 | rel2 :: Integer -> [Integer] | ||
| 150 | rel2 n | ||
| 151 | | even n = [n,n `div` 2] | ||
| 152 | | otherwise = [3*n+1,n] | ||
| 153 | |||
| 154 | rel2S :: Integer -> Set Integer | ||
| 155 | rel2S = Set.fromList . rel2 | ||
| 156 | |||
| 157 | |||
| 158 | -- b) | ||
| 159 | -- Implementieren Sie die Aufgabe noch mal ganz schnell | ||
| 160 | -- ohne Rücksicht auf Zirkularität oder Effizienz, | ||
| 161 | -- sondern ganz bequem mit der Standardbibliothek für Data.Set | ||
| 162 | |||
| 163 | -- The implementation below seems to me no nicer than a :( | ||
| 164 | |||
| 165 | transClS :: (Ord a) => (a -> Set a) -> Set a -> Set a | ||
| 166 | transClS rel xs = build xs Set.empty | ||
| 167 | where | ||
| 168 | res = build xs Set.empty | ||
| 169 | |||
| 170 | build xs known | ||
| 171 | | Set.null xs = Set.empty | ||
| 172 | | otherwise = xs' `Set.union` build xs' (xs' `Set.union` known) | ||
| 173 | where | ||
| 174 | xs' = Set.foldr Set.union Set.empty (Set.map rel xs) Set.\\ known | ||
| 175 | |||
| 176 | |||
| 177 | |||
| 178 | |||
| 179 | ---- A4-3 Verzögerte Auswertung | ||
| 180 | {-Ein Kollege von Dr Jost meinte einmal, dass man Dinge am Besten durch Implementation erlernt. | ||
| 181 | Also wollen wir in dieser Aufgabe verzögerte Auswertung für einen Fragment von Haskell Implementieren. | ||
| 182 | Wir machen uns das Leben einfach und nehemen nur folgendes, minimales Fragment her: | ||
| 183 | * Variablen z.B. "y" | ||
| 184 | * Anonyme Funktionen z.B. "\x->x" | ||
| 185 | * Funktionsanwendung z.B. "(\x->x) y" evaluiert zu "y" | ||
| 186 | Wir verzichten also auf sehr viel: keine Pattern-Matching, kein if-then-else,... | ||
| 187 | ...sogar auf Basisdatentypen wie Int oder Bool verzichten wir! | ||
| 188 | |||
| 189 | Die Terme unseres Sprach-Fragments modellieren wir durch folgenden Datentyp: | ||
| 190 | -} | ||
| 191 | |||
| 192 | data Term = Var Variable | Abs Variable Term | App Term Term | ||
| 193 | deriving (Eq) | ||
| 194 | |||
| 195 | type Variable = String | ||
| 196 | |||
| 197 | {- | ||
| 198 | Einige Hilfsfunktionen, sowie einige Beispiel-Terme sind weiter unten, | ||
| 199 | im Anhang dieser Datei definiert. Ebenso wurde eine vernünftige Show-Instanz vorgegeben. | ||
| 200 | so dass die Terme wie Haskell-Code ausschauen: | ||
| 201 | *Main> Abs "x" (App (Var "f") (Var "x" )) | ||
| 202 | \x -> f x | ||
| 203 | |||
| 204 | Von den Hilfsfunktionen sollten Sie eigentlich nur | ||
| 205 | subst :: (Variable, Term) -> Term -> Term | ||
| 206 | benötigen. Der Ausdruck "subst (x,t1) t2" bedeutet "t2[t1/x]", | ||
| 207 | also im Ausdruck t2 werden alle Vorkommen von x durch t1 ersetzt. | ||
| 208 | |||
| 209 | |||
| 210 | NEBENBEMERKUNG; | ||
| 211 | zum Lösen dieser Aufgabe nicht wichtig: | ||
| 212 | |||
| 213 | Richtig, es handelt sich dabei erneut um den Lambda-Kalkül, | ||
| 214 | wie wir ihn schon in Aufgaben A1-1g und A2-2 kennengelernt haben. | ||
| 215 | Anstatt "\x->x" würde man im Lambda-Kalkül eher "λx.x" schreiben, aber | ||
| 216 | das ist auch der einzige Unterschied. O | ||
| 217 | bwohl wir hier auf so viel verzichten, handelt es sich übrigens immer noch um eine Turing-Vollständige Sprache! | ||
| 218 | Also wollen wir hier die verzögerte Auswertestrategie anhand des Lambda-Kalküls üben... ;) | ||
| 219 | -} | ||
| 220 | |||
| 221 | |||
| 222 | -- a) Einfache Auswertung | ||
| 223 | -- | ||
| 224 | -- Wir schreiben uns zuerst eine simple Auswertung von Lambda-Ausdrücken, also | ||
| 225 | -- eine Funktion "eval :: Term -> Term". Das vorgehen ist wie folgt: | ||
| 226 | -- | ||
| 227 | -- 1) Variablen werten zu sich selbst aus (d.h. sind bereits ausgewertet); nichts zu tun. | ||
| 228 | -- | ||
| 229 | -- 2) Abstraktionen sind auch bereits ausgewertet; nichts zu tun. | ||
| 230 | -- (Wenn man will, dann könnte man auch erst noch den Rumpf auswerten, soweit möglich. | ||
| 231 | -- Dies ist eine reine Definitionsfrage, darf jeder machen wie er will. | ||
| 232 | -- Im Allgemeinen wird nicht unter einem Lambda reuduziert, aber beim Testen | ||
| 233 | -- werden die Terme leichter verständlich, wenn man unter dem Lambda reduziert.) | ||
| 234 | -- | ||
| 235 | -- 3) Zum Auswerten einer Applikationen "App" muss man zuerst die Funktion auswerten. | ||
| 236 | -- Erhält man einen Lambda-Ausdruck "Abs", so ersetzt man alle Vorkommen | ||
| 237 | -- der abstrahierten Variable durch das zuvor ausgewertete Funktionsargument. | ||
| 238 | -- (Ansonsten liefert man einfach die gesamte Applikation zurück.) | ||
| 239 | -- | ||
| 240 | -- Hinweis: Im 3. Fall muss man noch aufpassen, das keine freien Variablen eingefangen werden. | ||
| 241 | -- Glücklicherweise ist dies für uns bereits implementiert. Verwenden Sie einfach die Funktion "subst" | ||
| 242 | -- zur Substitution des Funktionsparameters im Rumpf der Funktion. | ||
| 243 | -- (Die Funktion "subst" ist weiter unten im Anhang dieser Datei definiert.) | ||
| 244 | -- | ||
| 245 | -- Einfache Implementierung der Auswertung : | ||
| 246 | eval :: Term -> Term | ||
| 247 | eval (App f x) = case eval f of | ||
| 248 | (Abs v t) -> eval $ subst (v, x) t | ||
| 249 | t -> eval $ t | ||
| 250 | eval x = x | ||
| 251 | |||
| 252 | |||
| 253 | {- Beispiele, ohne Auswertung unter einem Lambda, Konstanten cK, c1, usw. sind weiter unten, im Anhang der Datei definiert. | ||
| 254 | |||
| 255 | *Main> eval $ App (App cK c1) vX | ||
| 256 | \f -> \a -> f a | ||
| 257 | |||
| 258 | *Main> eval $ App cISNULL (App cSUCC c0) | ||
| 259 | \x -> \y -> y | ||
| 260 | |||
| 261 | -} | ||
| 262 | |||
| 263 | |||
| 264 | -- b) | ||
| 265 | -- | ||
| 266 | -- Da Haskell eine Sprache mit verzögerter Auswertung ist, | ||
| 267 | -- vererbt sich dies bereits auch auf unsere Implementierung von eval: | ||
| 268 | -- *Main> eval $ App (App cK c1) cOmega | ||
| 269 | -- \f -> \x -> f x | ||
| 270 | -- | ||
| 271 | -- Bei der Auswertestrategie "Call-By-Value" sollte dies eigentlich gar nicht auswerten, | ||
| 272 | -- da cOmega nicht endlich auswertbar ist. | ||
| 273 | -- | ||
| 274 | -- Eine Möglichkeit ist es, die Auswertung genauer zu simulieren. | ||
| 275 | -- Dazu nutzen wir jetzt eine Map zur Modellierung unseres Speichers: | ||
| 276 | |||
| 277 | type Memory = Map Variable Term | ||
| 278 | |||
| 279 | -- Ein Wert des Typs "Memory" bildet also Werte des Typs "Variable" auf Werte des Typs "Term" ab. | ||
| 280 | -- | ||
| 281 | -- Zur Anzeige eines Terms benötigen wir nun natürlich auch den Speicher, um den Kontext der Variablen zu haben. | ||
| 282 | -- Verwenden Sie zur Anzeige also diese gegebene Funktion: | ||
| 283 | showMem :: (Memory,Term) -> Term | ||
| 284 | showMem (m,t) = Map.foldlWithKey (\r v s -> subst (v,s) r) t m | ||
| 285 | |||
| 286 | -- Diese Anzeige bauchen wir gleich in unsere Auswertefunktion ein: | ||
| 287 | evalStrict :: Term -> Term | ||
| 288 | evalStrict t = showMem $ evalS0 t | ||
| 289 | |||
| 290 | -- Die Funktion evalS0 ist nur eine Kurzform, um die Auswertung mit leerem Speicher zu starten: | ||
| 291 | evalS0 :: Term -> (Memory, Term) | ||
| 292 | evalS0 = evalS Map.empty | ||
| 293 | |||
| 294 | -- Ihre Aufgabe ist es also, evalS zu implementieren: | ||
| 295 | |||
| 296 | evalS :: Memory -> Term -> (Memory, Term) | ||
| 297 | evalS m x@(Var v) = (,) m $ fromMaybe x $ Map.lookup v m | ||
| 298 | evalS m t@(App f x) = case f' of | ||
| 299 | (Abs v t) -> let | ||
| 300 | usedVars = Set.unions $ (Map.keysSet m'' :) $ map freeVars $ Map.elems m'' | ||
| 301 | v' = generateFreshVar usedVars | ||
| 302 | (m'', x') = evalS m' x | ||
| 303 | m''' = Map.insert v' x' m'' | ||
| 304 | in evalS m''' $ subst (v,Var v') t | ||
| 305 | _ -> (m, t) | ||
| 306 | where | ||
| 307 | (m', f') = evalS m f | ||
| 308 | evalS m x = (m, x) | ||
| 309 | |||
| 310 | -- Dabei verfolgen wir folgende Auswertestrategie: | ||
| 311 | -- | ||
| 312 | -- 1) Der Wert einer Variablen wird im Speicher nachgeschlagen. | ||
| 313 | -- Freie Variablen werten nach wie vor zu sich selbst aus. | ||
| 314 | -- | ||
| 315 | -- 2) Unverändert: Abstraktionen sind bereits ausgewertet. | ||
| 316 | -- | ||
| 317 | -- 3) Bei der Auswertung von Applikationen verzichten wir auf Substitution. | ||
| 318 | -- Stattdessen legen wir das ausgewertete Argument im Speicher | ||
| 319 | -- unter der abstrahierten Variable ab. | ||
| 320 | -- | ||
| 321 | -- Im Fall 3) treten einige Probleme auf: | ||
| 322 | -- - Der Speicher muss durch die rekursiven Aufruf von evalS hindurchgefädelt werden. | ||
| 323 | -- Es sollte immer nur auf den neuesten Speicher zugegriffen werden, | ||
| 324 | -- damit die Modellierung stimmt! | ||
| 325 | -- | ||
| 326 | -- - OPTIONAL: Wenn es aber nur einen Speicher gibt, kann es zu Namenskonflikten im Speicher | ||
| 327 | -- kommen. Dies kann vermieden werden, wenn Variable vor dem Speichern in frische Variablen | ||
| 328 | -- umbenannt werden. Verwenden Sie dazu die Hilfsfunktionen: freeVars, generateFreshVar & subst. | ||
| 329 | -- | ||
| 330 | -- Wenn Sie es richtig gemacht haben, sollte das obige Beispiel mit cOmega jetzt nicht mehr terminieren. | ||
| 331 | |||
| 332 | |||
| 333 | -- c) Nun wollen wir es wieder verbessern, in dem wir verzögerte Auswertung explizit simulieren. | ||
| 334 | -- | ||
| 335 | -- Im Fall 1) updaten wir den Speicher nach der Auswertung des abgespeicherten Terms, | ||
| 336 | -- um wiederholte Auswertung zu vermeiden. | ||
| 337 | -- (Der Einfachheit verzichten wir auf eine Prüfung/Flag ob im Speicher ein Thunk ist oder nicht: | ||
| 338 | -- wir werten und updaten immer - wenn es schon ein Wert war, dann geht die Auswertung ja schnell) | ||
| 339 | -- | ||
| 340 | -- Fall 2) Abs bleibt Unverändert | ||
| 341 | -- | ||
| 342 | -- Im Fall 3) App legen wir also nur den unausgewerten Term im Speicher ab. | ||
| 343 | -- | ||
| 344 | |||
| 345 | evalLazy :: Term -> Term | ||
| 346 | evalLazy t = showMem $ evalL0 t | ||
| 347 | |||
| 348 | evalL0 ::Term -> (Memory, Term) | ||
| 349 | evalL0 = evalL Map.empty | ||
| 350 | |||
| 351 | evalL :: Memory -> Term -> (Memory, Term) | ||
| 352 | evalL m x@(Var v) = case Map.lookup v m of | ||
| 353 | Nothing -> (m, x) | ||
| 354 | Just t -> let | ||
| 355 | (m', t') = evalL m t | ||
| 356 | in (Map.insert v t' m', t') | ||
| 357 | evalL m t@(App f x) = case f' of | ||
| 358 | (Abs v t) -> let | ||
| 359 | usedVars = Set.unions $ (Map.keysSet m' :) $ map freeVars $ Map.elems m' | ||
| 360 | v' = generateFreshVar usedVars | ||
| 361 | m'' = Map.insert v' x m' | ||
| 362 | in evalL m'' $ subst (v,Var v') t | ||
| 363 | _ -> (m, t) | ||
| 364 | where | ||
| 365 | (m', f') = evalL m f | ||
| 366 | evalL m x = (m, x) | ||
| 367 | |||
| 368 | |||
| 369 | |||
| 370 | -- I am of the considered opinion that the above exercises call for State. Therefore: | ||
| 371 | |||
| 372 | data State s a = State { unState :: s -> (a, s) } | ||
| 373 | |||
| 374 | instance Functor (State s) where | ||
| 375 | fmap f (State g) = State ((\(a, s) -> (f a, s)) . g) | ||
| 376 | |||
| 377 | instance Applicative (State s) where | ||
| 378 | pure a = State (\s -> (a, s)) | ||
| 379 | (State f) <*> (State g) = State (\s -> (\(g', s) -> (\(f', s') -> (f' g', s')) $ f s) $ g s) | ||
| 380 | |||
| 381 | instance Monad (State s) where | ||
| 382 | return = pure | ||
| 383 | (State f) >>= g = State ((\(a, s) -> (unState $ g a) s) . f) | ||
| 384 | |||
| 385 | get :: State s s | ||
| 386 | get = State (\s -> (s, s)) | ||
| 387 | |||
| 388 | put :: s -> State s () | ||
| 389 | put s = State (\_ -> ((), s)) | ||
| 390 | |||
| 391 | modify :: (s -> s) -> State s () | ||
| 392 | modify f = (f <$> get) >>= put | ||
| 393 | |||
| 394 | evalStrict' :: Term -> Term | ||
| 395 | evalStrict' t = showMem $ evalS0' t | ||
| 396 | where | ||
| 397 | evalS0' = evalS' Map.empty | ||
| 398 | |||
| 399 | evalLazy' :: Term -> Term | ||
| 400 | evalLazy' t = showMem $ evalL0' t | ||
| 401 | where | ||
| 402 | evalL0' = evalL' Map.empty | ||
| 403 | |||
| 404 | evalS' :: Memory -> Term -> (Memory, Term) | ||
| 405 | evalS' m t = swap $ (unState $ eval t) m | ||
| 406 | where | ||
| 407 | eval :: Term -> State Memory Term | ||
| 408 | eval t@(Var v) = (fromMaybe t . Map.lookup v) <$> get | ||
| 409 | eval t@(App f x) = do | ||
| 410 | f' <- eval f | ||
| 411 | case f' of | ||
| 412 | (Abs v t) -> do | ||
| 413 | x' <- eval x | ||
| 414 | mem <- get | ||
| 415 | let | ||
| 416 | boundInTerms = Set.unions . map freeVars $ Map.elems mem | ||
| 417 | usedVars = boundInTerms `Set.union` Map.keysSet mem | ||
| 418 | v' = generateFreshVar usedVars | ||
| 419 | modify $ Map.insert v' x' | ||
| 420 | eval $ subst (v, Var v') t | ||
| 421 | _ -> pure t | ||
| 422 | eval t = pure t | ||
| 423 | |||
| 424 | evalL' :: Memory -> Term -> (Memory, Term) | ||
| 425 | evalL' m t = swap $ (unState $ eval t) m | ||
| 426 | where | ||
| 427 | eval :: Term -> State Memory Term | ||
| 428 | eval t@(Var v) = do | ||
| 429 | t' <- Map.lookup v <$> get | ||
| 430 | case t' of | ||
| 431 | Nothing -> return t | ||
| 432 | Just t -> do | ||
| 433 | t' <- eval t | ||
| 434 | modify $ Map.insert v t' | ||
| 435 | return t' | ||
| 436 | eval t@(App f x) = do | ||
| 437 | f' <- eval f | ||
| 438 | case f' of | ||
| 439 | (Abs v t) -> do | ||
| 440 | mem <- get | ||
| 441 | let | ||
| 442 | boundInTerms = Set.unions . map freeVars $ Map.elems mem | ||
| 443 | usedVars = boundInTerms `Set.union` Map.keysSet mem | ||
| 444 | v' = generateFreshVar usedVars | ||
| 445 | modify $ Map.insert v' x | ||
| 446 | eval $ subst (v, Var v') t | ||
| 447 | _ -> pure t | ||
| 448 | eval t = pure t | ||
| 449 | |||
| 450 | ----------------------------------------------------------------------- | ||
| 451 | -- ANHANG | ||
| 452 | -- | ||
| 453 | -- Für erweiterten Komfort gegeben wir noch einige Definitionen vor! | ||
| 454 | -- | ||
| 455 | |||
| 456 | |||
| 457 | -- Hier einige Lambda-Terme zum Testen: | ||
| 458 | vX = Var "x" | ||
| 459 | vY = Var "y" | ||
| 460 | vZ = Var "z" | ||
| 461 | lTest1 = App (App vX vY) vZ | ||
| 462 | lTest2 = App vX (App vY vZ) | ||
| 463 | |||
| 464 | -- Combinators (allgmein bekannte Lambda-Terme) | ||
| 465 | cI = Abs "x" $ Var "x" -- \x -> x | ||
| 466 | cK = Abs "x" $ Abs "y" $ Var "x" -- \x y -> x | ||
| 467 | cS = Abs "z" $ Abs "y" $ Abs "x" $ App (App (Var "z") (Var "x")) (App (Var "y") (Var "x")) -- \z y x -> (z x) (y x) | ||
| 468 | cT = Abs "x" $ App (Var "x") (Var "x") -- \x -> x x | ||
| 469 | cOmega = App cT cT -- (\x -> x x) (\x -> x x) | ||
| 470 | |||
| 471 | -- Church Booleans (wer keine eingebauten Datentypen hat, bastelt sich halt selbst welche, so wie es uns Alonzo Church zeigte) | ||
| 472 | cTRUE = Abs "x" $ Abs "y" $ Var "x" -- \x y -> x | ||
| 473 | cFALSE = Abs "x" $ Abs "y" $ Var "y" -- \x y -> y | ||
| 474 | cCOND = Abs "x" $ Abs "y" $ Abs "z" $ App (App vX vY) vZ -- \x y z -> (x y) z | ||
| 475 | |||
| 476 | -- Church Numerals (wer keine eingebauten Zahlen hat, kann sich auch diese selbst stricken) | ||
| 477 | c0 = Abs "f" $ Abs "x" $ Var "x" -- \f x -> x | ||
| 478 | c1 = Abs "f" $ Abs "x" $ App (Var "f") (Var "x") -- \f x -> f x | ||
| 479 | c2 = eval $ App cSUCC c1 -- \f -> \x -> f (f x) | ||
| 480 | c3 = eval $ App cSUCC c2 -- \f -> \x -> f (f (f x)) | ||
| 481 | cSUCC = Abs "n" $ Abs "f" $ Abs "x" $ App (Var "f") $ App (App (Var "n" ) (Var "f")) (Var "x") -- \n f x -> f ((n f) x) | ||
| 482 | cPLUS = Abs "m" $ Abs "n" $ Abs "f" $ Abs "x" $ App (App (Var "m") (Var "f")) $ App (App (Var "n" ) (Var "f")) (Var "x") -- \m n f x -> (m f) ((n f) x) | ||
| 483 | cISNULL = Abs "x" $ App (App (Var "x") (Abs "x" cFALSE)) cTRUE -- \x -> x (\x -> (\x y -> y))) (\x y -> x)) | ||
| 484 | |||
| 485 | -- Lambda Terme hübsch anzeigen, in Haskell Notation, also anstatt "λf.λx.f x" schreiben wir hier "\f-> \x-> f x". | ||
| 486 | instance Show Term where | ||
| 487 | showsPrec _ (Var x) = showString x | ||
| 488 | showsPrec n (App s t) = showParen (n>1) $ (showsPrec 1 s) . showString " " . showsPrec 2 t | ||
| 489 | showsPrec n (Abs x t) = showParen (n>0) $ showString ('\\':x) . showString " -> " . showsPrec n t | ||
| 490 | |||
| 491 | ----------------------------- | ||
| 492 | -- Nützliche Hilfsfunktionen | ||
| 493 | -- | ||
| 494 | |||
| 495 | -- Substitution, welche das Einfangen freier Variablen verhindert. | ||
| 496 | -- Alle _freien_ Vorkommen einer Variable werden durch einen Term ersetzt. | ||
| 497 | -- Gebundene Variablen werden ggf. ersetzt, damit es nicht zu Namenskonflikten kommt: | ||
| 498 | -- [y/x] ( \y -> x y ) == \z -> y z | ||
| 499 | -- subst ("x", Var "y") (Abs "y" $ App (Var "x") (Var "y")) | ||
| 500 | -- | ||
| 501 | -- Wenn wir die Variable "x" durch den Term "y" ersetzen wollen, dann müssen wir | ||
| 502 | -- aufpassen, dass keine gebundenen Variablen 'eingefangen' werden, denn | ||
| 503 | -- "\y->x y" ist ja äquivalent zu "\z ->x z". | ||
| 504 | -- Also soll auch "(\y->x y)[y/x]" äquivalent zu "(\z ->x z)[y/x]" == "\z->y z" sein. | ||
| 505 | -- Wenn wir aber nur blind einsetzen würden, gilt das nicht, denn wir bekämen "\y->y y". | ||
| 506 | -- | ||
| 507 | |||
| 508 | subst :: (Variable, Term) -> Term -> Term | ||
| 509 | subst (x,e) o@(Var y) | ||
| 510 | | x == y = e | ||
| 511 | | otherwise = o | ||
| 512 | subst s (App e1 e2) = App (subst s e1) (subst s e2) | ||
| 513 | subst s@(x,e) o@(Abs y e1) | ||
| 514 | | x == y = o | ||
| 515 | | y `Set.notMember` fv_e = Abs y (subst s e1) | ||
| 516 | | otherwise = Abs freshV (subst (x,e) $ subst (y, Var freshV) e1) -- avoiding capture | ||
| 517 | where | ||
| 518 | fv_e = freeVars e | ||
| 519 | fv_e1 = freeVars e1 | ||
| 520 | freshV = generateFreshVar (fv_e `Set.union` fv_e1) | ||
| 521 | |||
| 522 | |||
| 523 | -- Freie Variablen eines Terms | ||
| 524 | freeVars :: Term -> Set Variable | ||
| 525 | freeVars (Var x) = Set.singleton x | ||
| 526 | freeVars (App e1 e2) = Set.union (freeVars e1) (freeVars e2) | ||
| 527 | freeVars (Abs x e1) = Set.delete x $ freeVars e1 | ||
| 528 | |||
| 529 | -- Frische Variable berechnen | ||
| 530 | generateFreshVar :: Set Variable -> Variable | ||
| 531 | generateFreshVar vs | ||
| 532 | | v `Set.notMember` vs = v | ||
| 533 | | otherwise = succString $ Set.findMax vs | ||
| 534 | where | ||
| 535 | v = "a" | ||
| 536 | |||
| 537 | -- Note that Ord String has "z" > "aa", so succString s = s ++ "a" would suffice | ||
| 538 | -- Ensure that "s" < succString "s" | ||
| 539 | succString :: String -> String | ||
| 540 | succString "" = "a" | ||
| 541 | succString ('z':s) = 'z' : succString s | ||
| 542 | succString ( c :s) = (succ c) : s | ||
| 543 | |||
