diff options
Diffstat (limited to 'fp1/week6')
| -rw-r--r-- | fp1/week6/camil/BewijsMapFlatten.icl | 83 | ||||
| -rw-r--r-- | fp1/week6/mart/BewijsMapFlatten.icl | 97 |
2 files changed, 180 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)
diff --git a/fp1/week6/mart/BewijsMapFlatten.icl b/fp1/week6/mart/BewijsMapFlatten.icl new file mode 100644 index 0000000..59fa5bc --- /dev/null +++ b/fp1/week6/mart/BewijsMapFlatten.icl @@ -0,0 +1,97 @@ +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 naar de lengte van as.
+
+ Basis:
+ aanname: as = [].
+
+ map f ([] ++ bs) = (map f []) ++ (map f bs) basis
+ ********
+ => map f (bs) = (map f []) ++ (map f bs) (1)
+ ********
+ => map f (bs) = [] ++ (map f bs) (3)
+ ****************
+ => map f bs = map f bs (1)
+
+ Inductiestap:
+ aanname: stelling geldt voor zekere as, ofwel:
+ map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
+
+ Te bewijzen: stelling geldt ook voor as, ofwel:
+ map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)
+
+ map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs) basis
+ ************
+ => map f [a:as ++ bs] = (map f [a:as]) ++ (map f bs) (2)
+ ******************
+ => [f a : map f (as ++ bs)] = (map f [a:as]) ++ (map f bs) (4)
+ ************
+ => [f a : map f (as ++ bs)] = [f a : map f as] ++ (map f bs) (4)
+ ****************************
+ => [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)] (4)
+ **************** ************************
+ => map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
+
+ Dus: basis + inductiestap => stelling bewezen.
+
+2.
+Te bewijzen:
+ voor iedere functie f, voor iedere eindige lijst xs:
+
+ flatten (map (map f) xs) = map f (flatten xs)
+
+Bewijs:
+ met inductio van de lengte van xs
+
+ Basis:
+ aanname: xs = [].
+
+ flatten (map (map f) []) = map f (flatten []) basis
+ **************
+ = flatten [] = map f (flatten []) (3)
+ **********
+ = flatten [] = map f [] (5)
+ **********
+ = [] = map f [] (5)
+ *****
+ = [] = [] (3)
+
+ Inductiestap:
+ aanname: stelling geldt voor zekere xs, ofwel:
+ flatten (map (map f) xs) = map f (flatten xs)
+
+ Te bewijzen: stelling geldt ook voor xs, ofwel:
+ flatten (map (map f) [x:xs]) = map f (flatten [x:xs])
+
+ flatten (map (map f) [x:xs]) = map f (flatten [x:xs]) basis
+ ******************
+ => flatten [map f x: map (map f) xs] = map f (flatten [x:xs]) (4)
+ *********************************
+ => (map f x) ++ (flatten (map (map f) xs)) = map f (flatten [x:xs]) (6)
+ **************
+ => (map f x) ++ (flatten (map (map f) xs)) = map f (x ++ (flatten xs)) (6)
+ *************************
+ => (map f x) ++ (flatten (map (map f) xs)) = (map f x) ++ (map f (flatten xs)) (9.4.1)
+ ************************ ****************
+ => flatten (map (map f) xs) = map f (flatten xs) (IH)
+
+ Dus: basis + inductiestap => stelling bewezen.
|