|
14
|
1 module Exercise_6 where |
|
|
2 import Data.Char |
|
|
3 import Test.QuickCheck |
|
|
4 |
|
|
5 {- Library DO NOT CHANGE -} |
|
|
6 type PairList = [(Int,Int)] |
|
|
7 {- End Library -} |
|
|
8 |
|
|
9 |
|
|
10 {---------------------------------------------------------------------} |
|
|
11 {- Aufgabe G6.1 -} |
|
|
12 |
|
|
13 instance Num b => Num (a -> b) where |
|
15
|
14 f + g = \x -> f x + g x |
|
|
15 f - g = \x -> f x - g x |
|
|
16 f * g = \x -> f x * g x |
|
|
17 negate f = \x -> negate (f x) |
|
|
18 abs f = \x -> abs (f x) |
|
|
19 signum f = \x -> signum (f x) |
|
|
20 fromInteger x = const (fromInteger x) |
|
14
|
21 |
|
|
22 |
|
|
23 |
|
|
24 {---------------------------------------------------------------------} |
|
|
25 {- Aufgabe G6.2 -} |
|
|
26 |
|
15
|
27 foldl' :: (a -> b -> a) -> a -> [b] -> a |
|
14
|
28 foldl' f z [] = z |
|
|
29 foldl' f z ( x : xs ) = foldl' f ( f z x ) xs |
|
|
30 |
|
15
|
31 foldr' :: (c -> b -> b) -> b -> [c] -> b |
|
14
|
32 foldr' f z [] = z |
|
|
33 foldr' f z ( x : xs ) = f x ( foldr' f z xs ) |
|
|
34 |
|
|
35 |
|
|
36 ffoldl = foldl' . foldl' |
|
15
|
37 {- |
|
|
38 foldl' :: (a -> b -> a) -> a -> [b] -> a |
|
|
39 |
|
|
40 f :: (a -> b -> a) |
|
|
41 |
|
|
42 inner :: a -> [b] -> a |
|
|
43 |
|
|
44 z :: a |
|
|
45 |
|
|
46 xs :: [[b]] |
|
|
47 |
|
|
48 ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a |
|
|
49 -} |
|
|
50 ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a |
|
|
51 ffoldl' f z xs = outer inner z xs |
|
|
52 where |
|
|
53 inner = (foldl' f) |
|
|
54 outer = foldl' |
|
|
55 |
|
14
|
56 |
|
|
57 oo = (.).(.) |
|
15
|
58 oo' w = (.) ((.) w) |
|
|
59 oo'' w x = (.) ((.) w) x |
|
|
60 oo''' w x = ((.) w) . x |
|
|
61 oo'''' w x y = (.) w (x y) |
|
|
62 oo''''' w x y = w . (x y) |
|
|
63 |
|
|
64 oo'''''' :: (c -> d) -> (a -> b -> c) -> a -> b -> d |
|
|
65 oo'''''' f g u v = f (g u v) |
|
|
66 |
|
14
|
67 |
|
|
68 |
|
|
69 |
|
|
70 {---------------------------------------------------------------------} |
|
|
71 {- Aufgabe G6.3 -} |
|
|
72 |
|
15
|
73 -- First vs. second parameter |
|
14
|
74 a1 = (div 5) |
|
|
75 a2 = (`div` 5) |
|
|
76 |
|
15
|
77 -- First vs. second parameter |
|
|
78 b1 = (+7) |
|
|
79 b2 = (7+) |
|
14
|
80 |
|
15
|
81 c1 = map (:[]) -- [[x] | x <- xs] |
|
|
82 c2 = map ([]:) -- Prepend [] to every list element |
|
14
|
83 |
|
15
|
84 o f g x = f (g x) |
|
|
85 flip' f x y = f y x |
|
|
86 -- Both ids, d2 is more general |
|
14
|
87 d1 = flip . flip |
|
|
88 d2 = id |
|
|
89 |
|
15
|
90 e1 x y z = [x, y, z] -- z element |
|
|
91 e2 x y z = x : y : z -- z list |
|
14
|
92 |
|
|
93 |
|
|
94 |
|
|
95 {---------------------------------------------------------------------} |
|
|
96 {- Aufgabe G6.4 -} |
|
|
97 |
|
|
98 {- |
|
15
|
99 Lemma reverse = foldl (\xs x -> x : xs) [] |
|
|
100 Proof by extensionality |
|
|
101 To show: |
|
|
102 *: reverse xs = foldl (\xs x -> x : xs) [] xs for all xs |
|
|
103 Too specialized for an induction! |
|
|
104 |
|
|
105 Generalization |
|
|
106 To show: |
|
|
107 GEN: reverse xs ++ ys = foldl (\xs x -> x : xs) ys xs for all xs, ys |
|
|
108 Proof by structural induction on xs |
|
14
|
109 |
|
|
110 Base case: |
|
15
|
111 To show: reverse [] ++ ys = foldl (\xs x -> x : xs) ys [] for all ys |
|
|
112 reverse [] ++ ys |
|
|
113 == [] ++ ys (by reverse_Nil) |
|
|
114 == ys (by append_Nil) |
|
|
115 foldl (\xs x -> x : xs) ys [] |
|
|
116 == ys (by foldl_Nil) |
|
14
|
117 |
|
|
118 Induction step: |
|
15
|
119 IH: reverse zs ++ ys = foldl (\xs x -> x : xs) ys zs for all ys |
|
|
120 To show: reverse (z : zs) ++ ys = foldl (\xs x -> x : xs) ys (z : zs) for all ys |
|
|
121 reverse (z : zs) ++ ys |
|
|
122 == (reverse zs ++ [z]) ++ ys (by reverse_Cons) |
|
|
123 == reverse zs ++ ([z] ++ ys) (by append_assoc) |
|
|
124 == reverse zs ++ z : ([] ++ ys) (by append_Cons) |
|
|
125 == reverse zs ++ z : ys (by append_Nil) |
|
|
126 == foldl (\xs x -> x : xs) (z : ys) zs (by IH with z : ys instead of ys) |
|
|
127 foldl (\xs x -> x : xs) ys (z : zs) |
|
|
128 == foldl (\xs x -> x : xs) ((\xs x -> x : xs) ys z) zs (by foldl_Cons) |
|
|
129 == foldl (\xs x -> x : xs) ((\x -> x : ys) z) zs (by eval of lambda) |
|
|
130 == foldl (\xs x -> x : xs) (z : ys) zs (by eval of lambda) |
|
|
131 |
|
|
132 QED for GEN |
|
|
133 |
|
|
134 To prove * we instantiate GEN with [] for ys and apply append_Nil2. |
|
|
135 |
|
|
136 QED |
|
|
137 |
|
14
|
138 -} |
|
|
139 |
|
|
140 |
|
|
141 |
|
|
142 {---------------------------------------------------------------------} |
|
|
143 {- Aufgabe G6.5 -} |
|
|
144 |
|
15
|
145 f1 xs = map (+ 1) xs |
|
|
146 f1' = map (+1) |
|
14
|
147 |
|
15
|
148 f2 xs = map (2 *) (map (+ 1) xs) |
|
|
149 f2' = map (\z -> 2*(z+1)) |
|
|
150 f2'' = map ((*2) . (+1)) |
|
|
151 f2''' = map (*2) . map(+1) |
|
14
|
152 |
|
15
|
153 f3 xs = f (g xs) |
|
|
154 where |
|
|
155 g = map (+ 1) |
|
|
156 f = filter (> 1) |
|
|
157 |
|
|
158 f3' = filter (> 1) . map (+ 1) |
|
14
|
159 |
|
|
160 f4 f g x = f (g x) |
|
15
|
161 f4' f g x = (f . g) x |
|
|
162 f4'' f g = f . g |
|
|
163 f4''' = (.) |
|
14
|
164 |
|
15
|
165 f5 f g x y = f ((g x) y) |
|
|
166 f5' f g x = f . (g x) |
|
|
167 -- |
|
|
168 f5'' = (.).(.) |
|
14
|
169 |
|
|
170 f6 f g x y z = f (g x y z) |
|
15
|
171 f6' f g x y = f . (g x y) |
|
|
172 -- |
|
|
173 f6'' = (.).(.).(.) |
|
14
|
174 |
|
|
175 f7 f g h x = g (h (f x)) |
|
15
|
176 f7' f g h x = g . (h (f x)) |
|
|
177 f7'' f g h = g . h . f |
|
|
178 -- |
|
|
179 f7''' = flip ((.).(.)) . flip (.) |
|
14
|
180 |
|
|
181 |
|
|
182 {---------------------------------------------------------------------} |
|
|
183 {- Aufgabe H6.1 -} |
|
|
184 |
|
|
185 wellformed :: PairList -> Bool |
|
|
186 wellformed = undefined |
|
|
187 |
|
|
188 |
|
|
189 empty :: PairList |
|
|
190 empty = undefined |
|
|
191 |
|
|
192 |
|
|
193 member :: Int -> PairList -> Bool |
|
|
194 member = undefined |
|
|
195 |
|
|
196 |
|
|
197 insert :: Int -> PairList -> PairList |
|
|
198 insert = undefined |
|
|
199 |
|
|
200 |
|
|
201 union :: PairList -> PairList -> PairList |
|
|
202 union = undefined |
|
|
203 |
|
|
204 |
|
|
205 delete :: Int -> PairList -> PairList |
|
|
206 delete = undefined |
|
|
207 |
|
|
208 |
|
|
209 |
|
|
210 {---------------------------------------------------------------------} |
|
|
211 {- Aufgabe H6.2 -} |
|
|
212 |
|
|
213 {-WETT-} |
|
|
214 anonymize :: String -> String |
|
|
215 anonymize = undefined |
|
|
216 {-TTEW-} |
