diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2015-11-13 23:45:26 +0000 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2015-11-13 23:45:26 +0000 |
commit | ab9484b343abd995cba915bb0ba4be8907dfa6ec (patch) | |
tree | f441968094bec070499d24e45e8a29f1315da1f4 /ws2015/ffp/blaetter | |
parent | 14dc76bda755c850f859a4b974c793e694f2b0b4 (diff) | |
download | uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.gz uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.bz2 uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.xz uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.zip |
Shorter lecture names
Diffstat (limited to 'ws2015/ffp/blaetter')
-rw-r--r-- | ws2015/ffp/blaetter/02/FFP_U02_Typklassen.hs | 206 | ||||
-rw-r--r-- | ws2015/ffp/blaetter/03/FFP_U03_Funktoren.hs | 191 | ||||
-rw-r--r-- | ws2015/ffp/blaetter/04/FFP_U04_Lazy.hs | 543 |
3 files changed, 940 insertions, 0 deletions
diff --git a/ws2015/ffp/blaetter/02/FFP_U02_Typklassen.hs b/ws2015/ffp/blaetter/02/FFP_U02_Typklassen.hs new file mode 100644 index 0000000..5f2d936 --- /dev/null +++ b/ws2015/ffp/blaetter/02/FFP_U02_Typklassen.hs | |||
@@ -0,0 +1,206 @@ | |||
1 | -- Fortgeschrittene Funktionale Programmierung, | ||
2 | -- LMU, TCS, Wintersemester 2015/16 | ||
3 | -- Steffen Jost, Alexander Isenko | ||
4 | -- | ||
5 | -- Übungsblatt 02. 28.10.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 | -- | A2-1 Funktionsdefinitionen | ||
16 | -- | ||
17 | -- Implementieren Sie folgende grundlegenden, | ||
18 | -- bekannten Funktionen in Haskell. | ||
19 | -- Selbst wenn Sie die Funktion nicht kennen, | ||
20 | -- sollte Ihnen der Typ die korrekte Lösung ermöglichen! | ||
21 | -- | ||
22 | |||
23 | import Prelude hiding (uncurry,flip,(.),map,zip,zipWith,zip,foldl) | ||
24 | |||
25 | import qualified Data.Map as P | ||
26 | |||
27 | -- Hinweis: Das import-Statement müssen Sie jetzt noch nicht verstehen, | ||
28 | -- es ist nur notwendig zur Vermeidung von Namenskonflikten mit der | ||
29 | -- Standardbibliothek, welche die meisten dieser Funktionen bereits enthält. | ||
30 | |||
31 | -- a) Uncurrying | ||
32 | -- > uncurry (/) (1,2) == 0.5 | ||
33 | uncurry :: (a -> b -> c) -> ((a,b) -> c) | ||
34 | uncurry f (a,b) = f a b | ||
35 | |||
36 | -- b) Anwendung einer Funktion mit zwei Argumenten auf ein Paar | ||
37 | -- > (1,2) ||> (/) == 0.5 | ||
38 | (||>) :: (a,b) -> (a -> b -> c) -> c | ||
39 | p ||> f = uncurry f p | ||
40 | |||
41 | |||
42 | -- c) Vertauschung der Reihenfolge der Funktionsargumente | ||
43 | -- > flip (/) 2 1 == 0.5 | ||
44 | flip :: (a -> b -> c) -> (b -> a -> c) | ||
45 | flip f b a = f a b | ||
46 | |||
47 | |||
48 | -- d) Funktionskomposition | ||
49 | -- > ((\x->x+3) . (\y->y*2)) 1 == 5 | ||
50 | (.) :: (b -> c) -> (a -> b) -> a -> c | ||
51 | (.) f g x = f $ g x | ||
52 | |||
53 | |||
54 | -- e) Map (im Gegensatz zu A1-3 dieses Mal ohne List-Comprehension) | ||
55 | -- > map (+10) [1,2,3,4] == [11,12,13,14] | ||
56 | map :: (a -> b) -> [a] -> [b] | ||
57 | map _ [] = [] | ||
58 | map f (x:xs) = f x : map f xs | ||
59 | |||
60 | |||
61 | -- f) zip: | ||
62 | -- > zip ['a','b','c'] [1,2,3,4,5] = [('a',1),('b',2),('c',3)] | ||
63 | zip :: [a] -> [b] -> [(a,b)] | ||
64 | zip [] _ = [] | ||
65 | zip _ [] = [] | ||
66 | zip (x:xs) (y:ys) = (x, y) : zip xs ys | ||
67 | |||
68 | |||
69 | -- g) Zippen mit Funktionsanwendung: | ||
70 | -- > zipWith (+) [1..] [1..3] == [2,4,6] | ||
71 | zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] | ||
72 | zipWith f xs ys = map (uncurry f) $ zip xs ys | ||
73 | |||
74 | |||
75 | -- h) Falten nach links: | ||
76 | -- > foldl (flip (:) ) [] [1..3] == [3,2,1] | ||
77 | -- > foldl (\acc x -> x : acc)) [] [1..3] == [3,2,1] | ||
78 | foldl :: (b -> a -> b) -> b -> [a] -> b | ||
79 | foldl _ x [] = x | ||
80 | foldl f x (y:ys) = foldl f (f x y) ys | ||
81 | |||
82 | |||
83 | |||
84 | -- | A2-2 LambdaTerme | ||
85 | -- | ||
86 | -- Betrachten Sie die Lösung zur A1-1 g): | ||
87 | |||
88 | data LambdaTerm = LVar Char | ||
89 | | LAbs Char LambdaTerm | ||
90 | | LApp LambdaTerm LambdaTerm | ||
91 | |||
92 | -- Ein paar Lambda Terme zum Testen: | ||
93 | lTerm_x = LVar 'x' | ||
94 | lTerm_y = LVar 'y' | ||
95 | lTerm_id = LAbs 'x' lTerm_x | ||
96 | lTerm_xx = LApp lTerm_x lTerm_x | ||
97 | lTerm_t = LAbs 'x' $ LApp lTerm_y lTerm_xx | ||
98 | lTerm_yk = LAbs 'y' $ LApp lTerm_t lTerm_t | ||
99 | |||
100 | -- a) Implementieren Sie eine Eq-Instanz für den Datentyp LambdaTerm! | ||
101 | -- | ||
102 | -- (Wer Lambda-Kalkül kennt: Zur Vereinfachung der Aufgabe | ||
103 | -- ignorieren wir die übliche alpha-Äquivalenz, d.h. | ||
104 | -- (LAbs 'x' $ LVar 'x') und (LAbs 'y' $ LVar 'y') | ||
105 | -- dürfen als verschieden betrachtet werden) | ||
106 | |||
107 | instance Eq LambdaTerm where | ||
108 | (LVar a) == (LVar b) = a == b | ||
109 | (LVar _) == _ = False | ||
110 | (LAbs a t_a) == (LAbs b t_b) = a == b && t_a == t_b | ||
111 | (LAbs _ _) == _ = False | ||
112 | (LApp t_a t'_a) == (LApp t_b t'_b) = t_a == t_b && t'_a == t'_b | ||
113 | (LApp _ _) == _ = False | ||
114 | |||
115 | -- b) Implementieren Sie die eine Show-Instanz für LambdaTerm. | ||
116 | -- Achten Sie dabei auf eine korrekte Klammerung, aber | ||
117 | -- verschwenden Sie erst einmal keine Zeit darauf, | ||
118 | -- überflüssige Klammern zu vermeiden. | ||
119 | |||
120 | instance Show LambdaTerm where | ||
121 | show (LVar a) = "LVar '" ++ pure a ++ "'" | ||
122 | show (LAbs a t) = "LAbs '" ++ pure a ++ "' (" ++ show t ++ ")" | ||
123 | show (LApp t t') = "LApp (" ++ show t ++ ") (" ++ show t' ++ ")" | ||
124 | |||
125 | |||
126 | -- | A2-3 Klassendeklaration | ||
127 | -- | ||
128 | -- a) Deklarieren Sie eine Klasse "FinMap" für endliche partielle Abbildungen, welche folgende Operationen bereitsstellt: | ||
129 | -- 1) "emptyM" liefert eine leere Abbildung | ||
130 | -- 2) "insertM x a m" fügt die Abbildung [x->a] in die Abbildung m ein. | ||
131 | -- Falls x schon enthalten war, dann wird es überschrieben. | ||
132 | -- 3) "lookupM x m" liefert Nothing zurück, falls x nicht in m enthalten ist; | ||
133 | -- ansonsten wird der für x gespeicherte Wert z zurückgeliefert (in Just verpackt) | ||
134 | -- Die Funktion "lookupM" darf dabei annehmen, dass für x eine Vergleichsoperation vorliegt!?! | ||
135 | |||
136 | class FinMap m where | ||
137 | emptyM :: m k v | ||
138 | insertM :: Ord k => k -> v -> m k v -> m k v | ||
139 | lookupM :: Ord k => k -> m k v -> Maybe v | ||
140 | -- Can we get around using constraints here without using the MultiParamTypeClasses language extension? | ||
141 | |||
142 | -- b) Machen Sie folgenden Datentyp zu einer Instanz der Typklasse Map: | ||
143 | |||
144 | -- data AL a b = AL [(a,b)] | ||
145 | newtype AL a b = AL [(a,b)] -- Äquivalent zur vorherigen Zeile. | ||
146 | -- newtype kann und darf verwenden werden, | ||
147 | -- wenn man nur einen Konstruktor mit nur einem Argument hat. | ||
148 | -- Dies erlaubt GHC eine Optimierung durchzuführen. | ||
149 | deriving (Show, Read, Eq) | ||
150 | |||
151 | instance FinMap AL where | ||
152 | emptyM = AL $ [] | ||
153 | insertM x a (AL m) = AL $ (x, a) : [p | p@(x', _) <- m, x' /= x] | ||
154 | lookupM x (AL m) = listToMaybe [y | (x', y) <- m, x' == x] -- Due to lazyness this is no slower than explicitly short-circuiting the search | ||
155 | where | ||
156 | -- This is part of Data.Maybe | ||
157 | listToMaybe [] = Nothing | ||
158 | listToMaybe (x:_) = Just x | ||
159 | |||
160 | |||
161 | ---- Werte zum anschließendem Testen, auskommentieren, | ||
162 | ---- sobald Klasse und Instanz definiert wurden: | ||
163 | testMap0 :: AL Int Bool | ||
164 | testMap0 = emptyM | ||
165 | testMap1 = insertM 1 False testMap0 | ||
166 | testMap2 = insertM 3 False testMap1 | ||
167 | testMap3 = insertM 4 True testMap2 | ||
168 | testMap4 = insertM 2 True testMap3 | ||
169 | |||
170 | |||
171 | -- Hinweis: | ||
172 | -- Partielle Abbildungen wie hier durch Assoziationslisten zu implementieren, | ||
173 | -- ist nicht bensonders effizient, da der Zugriff auf ein Element im Allgemeinen | ||
174 | -- den Aufwand O(n) hat (man muss die ganze Liste abklappern - es könnte sich ja | ||
175 | -- um das letzte Element der Liste handeln). | ||
176 | -- Mit Suchbäumen läßt sich der Aufwand bekanntermaßen auf O(log n) reduzieren. | ||
177 | -- Wer noch Lust & Zeit hat, kann versuchen, dies selbst zu implementieren | ||
178 | -- und zur einer weiteren Instanz von FinMap machen. | ||
179 | -- | ||
180 | -- Die Standardbibliothek sieht zur Abstraktion hier keine solche Klasse vor, | ||
181 | -- sondern bietet lediglich eine konkrete, effiziente Implementierung von | ||
182 | -- endlichen Abbildungen an: Data.Map, welche wir in der kommenden Vorlesung | ||
183 | -- betrachten werden. | ||
184 | -- | ||
185 | -- Dies kann man natürlich ganz schnell zu einer Instanz von FinMap machen. Wie? | ||
186 | |||
187 | data Map k v = Tip | ||
188 | | Branch k v (Map k v) (Map k v) | ||
189 | |||
190 | instance FinMap Map where | ||
191 | emptyM = Tip | ||
192 | insertM k v Tip = Branch k v Tip Tip | ||
193 | insertM k v (Branch k' v' lt gt) | ||
194 | | k == k' = Branch k v lt gt | ||
195 | | k < k' = Branch k' v' (insertM k v lt) gt | ||
196 | | otherwise = Branch k' v' lt (insertM k v gt) | ||
197 | lookupM _ Tip = Nothing | ||
198 | lookupM k (Branch k' v' lt gt) | ||
199 | | k == k' = Just v' | ||
200 | | k < k' = lookupM k lt | ||
201 | | otherwise = lookupM k gt | ||
202 | |||
203 | instance FinMap P.Map where | ||
204 | emptyM = P.empty | ||
205 | insertM = P.insert | ||
206 | lookupM = P.lookup | ||
diff --git a/ws2015/ffp/blaetter/03/FFP_U03_Funktoren.hs b/ws2015/ffp/blaetter/03/FFP_U03_Funktoren.hs new file mode 100644 index 0000000..88ee00f --- /dev/null +++ b/ws2015/ffp/blaetter/03/FFP_U03_Funktoren.hs | |||
@@ -0,0 +1,191 @@ | |||
1 | -- Fortgeschrittene Funktionale Programmierung, | ||
2 | -- LMU, TCS, Wintersemester 2015/16 | ||
3 | -- Steffen Jost, Alexander Isenko | ||
4 | -- | ||
5 | -- Übungsblatt 03 am 3.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 Data.List (groupBy) | ||
17 | import Data.Function (on) | ||
18 | |||
19 | -- Bearbeiten Sie zuerst Übungsblatt 02 vollständig! | ||
20 | |||
21 | |||
22 | ---- A3-1 Funktoren | ||
23 | -- | ||
24 | -- Machen Sie folgende Datentypen zur einer Instanz der Klasse Functor. | ||
25 | -- Versuchen Sie dabei, möglichst nicht in die Folien zu schauen! | ||
26 | -- (Falls Sie doch in die Folien schauen, dann möglichst nur 2-25 und 2-31ff.; | ||
27 | -- da die Beispiele 2-28 und 2-29 nahezu die komplette Lösung verraten.) | ||
28 | |||
29 | |||
30 | -- a) | ||
31 | data Options a = None | One a | Two a a | Three a a a | ||
32 | deriving (Ord, Show) | ||
33 | |||
34 | -- Wenn wir nur die ersten beiden Konstuktoren von "Options" betrachten, | ||
35 | -- dann haben wir genau den Datentyp "Maybe" aus der Standardbibliothek. | ||
36 | |||
37 | instance Functor Options where | ||
38 | fmap _ None = None | ||
39 | fmap f (One a) = One (f a) | ||
40 | fmap f (Two a b) = Two (f a) (f b) | ||
41 | fmap f (Three a b c) = Three (f a) (f b) (f c) | ||
42 | |||
43 | -- Zum Testen: | ||
44 | testO0 = None | ||
45 | testO1 = One 4.2 | ||
46 | testO2 = Two 4.2 6.9 | ||
47 | -- Tests auskommentierbar, sobald Functor Instanz definiert: | ||
48 | testa1 = None == fmap (+2) testO0 | ||
49 | testa2 = Two 8.4 13.8 == fmap (*2) testO2 | ||
50 | |||
51 | |||
52 | -- b) | ||
53 | data Tree a = Node a [Tree a] | ||
54 | deriving (Eq, Show) | ||
55 | |||
56 | --Hilfsfunktion | ||
57 | leaf :: a -> Tree a | ||
58 | leaf x = Node x [] | ||
59 | |||
60 | instance Functor Tree where | ||
61 | fmap f (Node a xs) = Node (f a) $ map (fmap f) xs | ||
62 | |||
63 | -- Zum Testen: | ||
64 | testT1 = Node 1 [Node 2 [Node 3 [], leaf 4, Node 5 [leaf 6, leaf 7, leaf 8]], leaf 9, Node 10 [leaf 11]] | ||
65 | testT2 = Node False [Node True [Node False [],leaf True,Node False [leaf True,leaf False,leaf True]],leaf False,Node True [leaf False]] | ||
66 | -- Test auskommentierbar, sobald Functor Instanz definiert: | ||
67 | testb1 = testT2 == (fmap even testT1) | ||
68 | |||
69 | |||
70 | |||
71 | |||
72 | ---- A3-2 Funktor (->) a | ||
73 | -- | ||
74 | -- Die Standardbibliothek definiert eine Funktor-Instanz für den Typ "(->) a". | ||
75 | -- Wir wollen hier herausfinden, was dies bedeutet: | ||
76 | -- | ||
77 | -- Der Typ "(->) a" ist ein Typ mit einem ``Loch'', | ||
78 | -- so wie die Typen "Tree" oder "[ ]" auch. | ||
79 | -- Die runde Klammer bedeutet lediglich Präfix-Notation anstatt Infix-Notation. | ||
80 | -- Wenn wir also einen Typ "b" hineingeben wird daraus der Typ (im vertrauten Infix) | ||
81 | -- a -> b | ||
82 | -- ganz analog wird aus "Tree" oder "[ ]" zu "Tree b" oder "[b]". | ||
83 | -- | ||
84 | |||
85 | -- a) Welchen konkreten Typ bekommt die Funktion "fmap" | ||
86 | -- für die Funktor-Instanz von "(->) a"? | ||
87 | -- | ||
88 | -- Hinweis: Ein Beispiel findet sich auf Folie 2-26. | ||
89 | -- Oben ist der allgemeine Typ von fmap angegeben. | ||
90 | -- Unten dann nochmal konkreter für die Listen-Instanz. | ||
91 | |||
92 | {- | ||
93 | fmap :: Functor f => (a -> b) -> f a -> f b | ||
94 | fmap :: (a -> b) -> (x -> a) -> (x -> b) | ||
95 | -} | ||
96 | |||
97 | -- b) Die Standardbibliothek enthält bereits eine Funktion des in a) gefundenen Typs! | ||
98 | -- Wie heisst diese Funktion und was macht sie? | ||
99 | -- Testen Sie anschließend in GHCI, ob sie die Funktion | ||
100 | -- tatsächlich mit fmap vertauschen können! | ||
101 | -- | ||
102 | -- Hinweis: Diese Funktion wird Ihnen in einer Vorlesung über | ||
103 | -- funktionaler Programmierung mit Sicherheit begegnet sein, | ||
104 | -- da sie von fundamentaler Bedeutung ist. | ||
105 | -- (Jedoch sicherlich nicht als Funktor behandelt... ;) ) | ||
106 | |||
107 | {- | ||
108 | fmap ist hier identisch zu (.) | ||
109 | λ ((\a -> (a, a)) `fmap` (+ 2)) 2 | ||
110 | (4,4) | ||
111 | -} | ||
112 | |||
113 | |||
114 | |||
115 | |||
116 | ---- A3-3 Unendliche Listen | ||
117 | -- | ||
118 | -- a) Definieren Sie die unendliche Liste alle Zweierpotenzen: [1,2,4,8,16,32,64,128,256,..] | ||
119 | |||
120 | quadrate :: [Integer] | ||
121 | quadrate = map (2^) [0..] | ||
122 | |||
123 | quadrate' :: [Integer] -- More efficient (probably) | ||
124 | quadrate' = 1 : [2 * x | x <- quadrate'] | ||
125 | |||
126 | -- Zum Testen: | ||
127 | q1 = take 5 quadrate | ||
128 | -- > q1 | ||
129 | -- [1,2,4,8,16] | ||
130 | q2 = quadrate !! 10 | ||
131 | -- > q2 | ||
132 | -- 1024 | ||
133 | |||
134 | |||
135 | -- b) Definieren Sie eine unendliche Liste, welche alle | ||
136 | -- erdenklichen Strings aus den Buchstaben ['a','b','c','d']. | ||
137 | -- Die Reihenfolge ist relativ egal, aber kürzere Strings sollen vor längeren Erscheinen; | ||
138 | -- d.h. "dd" kommt nach "b", aber vor "abc" | ||
139 | |||
140 | alleVariablen :: [String] | ||
141 | alleVariablen = seed : alleVariablen' [seed] | ||
142 | where | ||
143 | seed = "" | ||
144 | vars = ['a','b','c','d'] | ||
145 | alleVariablen' prevs = now ++ alleVariablen' now | ||
146 | where | ||
147 | now = [v : p | v <- vars, p <- prevs] | ||
148 | |||
149 | alleVariablen' :: [String] -- Preferred. | ||
150 | alleVariablen' = "" : [v : p | p <- alleVariablen', v <- vars] | ||
151 | where | ||
152 | vars = ['a', 'b', 'c', 'd'] | ||
153 | |||
154 | -- Zum Testen: | ||
155 | check l x = (map length . groupBy ((==) `on` length)) (take x l) | ||
156 | |||
157 | -- Beispielimplementierung (muss nicht identisch sein): | ||
158 | -- > take 30 alleVariablen | ||
159 | -- ["" | ||
160 | -- ,"a" ,"b" ,"c" ,"d" | ||
161 | -- ,"aa" ,"ab" ,"ac" ,"ad" ,"ba" ,"bb" ,"bc" ,"bd" ,"ca" ,"cb","cc","cd","da","db","dc","dd" | ||
162 | -- ,"aaa","aab","aac","aad","aba","abb","abc","abd","aca"] | ||
163 | -- | ||
164 | -- Prüfe Längen: | ||
165 | -- > check alleVariablen 30 | ||
166 | -- [1,4,16,9] | ||
167 | |||
168 | |||
169 | |||
170 | |||
171 | -- A3-4 Instanzen | ||
172 | -- Wer sich mit Klassen und Instanzen noch nicht so sicher fühlt, | ||
173 | -- sollte zur Übung die automatisch abgeleiteten Instanzdeklaration | ||
174 | -- für die Datentypdeklarationen in A3-1 von Hand deklarieren; | ||
175 | -- also z.B. | ||
176 | -- von "Options" zur Typklassen "Eq" | ||
177 | -- von "Tree a" zur Typklasse "Ord" | ||
178 | -- | ||
179 | -- sie müssen oben in den Datentypdeklarationen dann natürlich | ||
180 | -- die entsprechenden Klassen aus Zeile mit "deriving" herauslöschen | ||
181 | -- da es ja immer nur _eine_ Instanzdeklaration pro Typ/Klassen-Paar geben darf | ||
182 | |||
183 | instance Eq a => Eq (Options a) where | ||
184 | None == None = True | ||
185 | One a == One a' = a == a' | ||
186 | Two a b == Two a' b' = a == a' && b == b' | ||
187 | Three a b c == Three a' b' c' = a == a' && b == b' && c == c' | ||
188 | _ == _ = False | ||
189 | |||
190 | instance Ord a => Ord (Tree a) where | ||
191 | compare (Node x xs) (Node x' xs') = compare x x' `mappend` compare xs xs' | ||
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 | |||