Mercurial > 12ws.info2

comparison exercises/src/Exercise_6.hs @ 15:bef891fc07b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
week 6 tutorial
author Markus Kaiser <markus.kaiser@in.tum.de>
date Wed, 28 Nov 2012 21:18:59 +0100
parents 0d15fb5d5ade
children
comparison
equal deleted inserted replaced
14:0d15fb5d5ade 15:bef891fc07b4
9 9
10 {---------------------------------------------------------------------} 10 {---------------------------------------------------------------------}
11 {- Aufgabe G6.1 -} 11 {- Aufgabe G6.1 -}
12 12
13 instance Num b => Num (a -> b) where 13 instance Num b => Num (a -> b) where
14 f + g = undefined 14 f + g = \x -> f x + g x
15 f - g = undefined 15 f - g = \x -> f x - g x
16 f * g = undefined 16 f * g = \x -> f x * g x
17 negate f = undefined 17 negate f = \x -> negate (f x)
18 abs f = undefined 18 abs f = \x -> abs (f x)
19 signum f = undefined 19 signum f = \x -> signum (f x)
20 fromInteger x = undefined 20 fromInteger x = const (fromInteger x)
21 21
22 22
23 23
24 {---------------------------------------------------------------------} 24 {---------------------------------------------------------------------}
25 {- Aufgabe G6.2 -} 25 {- Aufgabe G6.2 -}
26 26
27 foldl' :: (a -> b -> a) -> a -> [b] -> a
27 foldl' f z [] = z 28 foldl' f z [] = z
28 foldl' f z ( x : xs ) = foldl' f ( f z x ) xs 29 foldl' f z ( x : xs ) = foldl' f ( f z x ) xs
29 30
31 foldr' :: (c -> b -> b) -> b -> [c] -> b
30 foldr' f z [] = z 32 foldr' f z [] = z
31 foldr' f z ( x : xs ) = f x ( foldr' f z xs ) 33 foldr' f z ( x : xs ) = f x ( foldr' f z xs )
32 34
33 35
34 ffoldl = foldl' . foldl' 36 ffoldl = foldl' . foldl'
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
35 56
36 oo = (.).(.) 57 oo = (.).(.)
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
37 67
38 68
39 69
40 {---------------------------------------------------------------------} 70 {---------------------------------------------------------------------}
41 {- Aufgabe G6.3 -} 71 {- Aufgabe G6.3 -}
42 72
43 73 -- First vs. second parameter
44 a1 = (div 5) 74 a1 = (div 5)
45 a2 = (`div` 5) 75 a2 = (`div` 5)
46 76
47 b1 = (+ 7) 77 -- First vs. second parameter
48 b2 = ((+) 7) 78 b1 = (+7)
49 79 b2 = (7+)
50 c1 = map (:[]) 80
51 c2 = map ([]:) 81 c1 = map (:[]) -- [[x] | x <- xs]
52 82 c2 = map ([]:) -- Prepend [] to every list element
83
84 o f g x = f (g x)
85 flip' f x y = f y x
86 -- Both ids, d2 is more general
53 d1 = flip . flip 87 d1 = flip . flip
54 d2 = id 88 d2 = id
55 89
56 e1 x y z = [x, y, z] 90 e1 x y z = [x, y, z] -- z element
57 e2 x y z = x : y : z 91 e2 x y z = x : y : z -- z list
58 92
59 93
60 94
61 {---------------------------------------------------------------------} 95 {---------------------------------------------------------------------}
62 {- Aufgabe G6.4 -} 96 {- Aufgabe G6.4 -}
63 97
64 {- 98 {-
65 Lemma: reverse = foldl (\xs x -> x : xs) [] 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
66 109
67 Base case: 110 Base case:
68 To show: 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)
69 117
70 Induction step: 118 Induction step:
71 IH: 119 IH: reverse zs ++ ys = foldl (\xs x -> x : xs) ys zs for all ys
72 To show: 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
73 -} 138 -}
74 139
75 140
76 141
77 {---------------------------------------------------------------------} 142 {---------------------------------------------------------------------}
78 {- Aufgabe G6.5 -} 143 {- Aufgabe G6.5 -}
79 144
80 f1 xs = map (\x -> x + 1) xs 145 f1 xs = map (+ 1) xs
81 146 f1' = map (+1)
82 f2 xs = map (\x -> 2 * x) (map (\x -> x + 1) xs) 147
83 148 f2 xs = map (2 *) (map (+ 1) xs)
84 f3 xs = filter (\x -> x > 1) (map (\x -> x + 1) xs) 149 f2' = map (\z -> 2*(z+1))
150 f2'' = map ((*2) . (+1))
151 f2''' = map (*2) . map(+1)
152
153 f3 xs = f (g xs)
154 where
155 g = map (+ 1)
156 f = filter (> 1)
157
158 f3' = filter (> 1) . map (+ 1)
85 159
86 f4 f g x = f (g x) 160 f4 f g x = f (g x)
87 161 f4' f g x = (f . g) x
88 f5 f g x y = f (g x y) 162 f4'' f g = f . g
163 f4''' = (.)
164
165 f5 f g x y = f ((g x) y)
166 f5' f g x = f . (g x)
167 --
168 f5'' = (.).(.)
89 169
90 f6 f g x y z = f (g x y z) 170 f6 f g x y z = f (g x y z)
171 f6' f g x y = f . (g x y)
172 --
173 f6'' = (.).(.).(.)
91 174
92 f7 f g h x = g (h (f x)) 175 f7 f g h x = g (h (f x))
93 176 f7' f g h x = g . (h (f x))
177 f7'' f g h = g . h . f
178 --
179 f7''' = flip ((.).(.)) . flip (.)
94 180
95 181
96 {---------------------------------------------------------------------} 182 {---------------------------------------------------------------------}
97 {- Aufgabe H6.1 -} 183 {- Aufgabe H6.1 -}
98 184