diff options
| author | Mart Lubbers | 2015-04-16 21:22:20 +0200 |
|---|---|---|
| committer | Mart Lubbers | 2015-04-16 21:22:20 +0200 |
| commit | 6f604b19d3f5966e5c1d7c4fdf3703bd6ff0861c (patch) | |
| tree | 96d580507249f7f58368476d9113007d4afcd748 /fp1/week6/camil/BewijsMapFlatten.icl | |
| parent | Added student numbers (diff) | |
update to fp2 yay, public and licence
Diffstat (limited to 'fp1/week6/camil/BewijsMapFlatten.icl')
| -rw-r--r-- | fp1/week6/camil/BewijsMapFlatten.icl | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/fp1/week6/camil/BewijsMapFlatten.icl b/fp1/week6/camil/BewijsMapFlatten.icl new file mode 100644 index 0000000..7f2474e --- /dev/null +++ b/fp1/week6/camil/BewijsMapFlatten.icl @@ -0,0 +1,83 @@ +// Mart Lubbers, s4109503
+// Camil Staps, s4498062
+
+Zij gegeven:
+
+(++) :: [a] [a] -> [a]
+(++) [] xs = xs (1)
+(++) [y:ys] xs = [y : ys ++ xs] (2)
+
+map :: (a -> b) [a] -> [b]
+map f [] = [] (3)
+map f [x:xs] = [f x : map f xs] (4)
+
+flatten :: [[a]] -> [a]
+flatten [] = [] (5)
+flatten [x:xs] = x ++ (flatten xs) (6)
+
+1.
+Te bewijzen:
+ voor iedere functie f, eindige lijst as en bs:
+
+ map f (as ++ bs) = (map f as) ++ (map f bs)
+
+Bewijs:
+Met inductie over as.
+
+Inductiebasis:
+Stel as = []. Dan hebben we:
+
+ map f (as ++ bs) // aanname as = []
+ = map f ([] ++ bs) // definitie van ++, regel 1
+ = map f bs // definitie van ++, regel 1
+ = [] ++ (map f bs) // definitie van map, regel 3
+ = (map f []) ++ (map f bs) // aanname as = []
+ = (map f as) ++ (map f bs).
+
+Inductiestap:
+Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we:
+
+ map f ([a:as] ++ bs) // definitie van ++, regel 2
+ = map f [a:as ++ bs] // definitie van map, regel 4
+ = [f a : map f (as ++ bs)] // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs)
+ = [f a : (map f as) ++ (map f bs)] // lijst herschrijven
+ = [f a : map f as] ++ (map f bs) // definitie van map, regel 4
+ = (map f [a:as]) ++ (map f bs).
+
+Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs:
+
+ map f (as ++ bs) = (map f as) ++ (map f bs) (9.4.1)
+
+2.
+Te bewijzen:
+ voor iedere functie f, voor iedere eindige lijst xs:
+
+ flatten (map (map f) xs) = map f (flatten xs)
+
+Bewijs:
+Met inductie over xs.
+
+Inductiebasis:
+Stel xs = []. Dan hebben we:
+
+ flatten (map (map f) xs) // aanname xs = []
+ = flatten (map (map f) []) // definitie van map, regel 3
+ = flatten [] // definitie van flatten, regel 5
+ = [] // definitie van map, regel 3
+ = map f [] // definitie van flatten, regel 5
+ = map f (flatten []) // aanname xs = []
+ = map f (flatten xs).
+
+Inductiestap:
+Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we:
+
+ flatten (map (map f) [x:xs]) // definitie van map, regel 4
+ = flatten [map f x : map (map f) xs] // definitie van flatten, regel 6
+ = (map f x) ++ flatten (map (map f) xs) // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs)
+ = (map f x) ++ (map f (flatten xs)) // 9.4.1
+ = map f (x ++ (flatten xs)) // definitie van flatten, regel 6
+ = map f (flatten [x:xs]).
+
+Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt:
+
+ flatten (map (map f) xs) = map f (flatten xs)
|