diff options
| -rw-r--r-- | week6/camil/9.4.1 | 23 | ||||
| -rw-r--r-- | week6/camil/9.4.2 | 24 | ||||
| -rw-r--r-- | week6/camil/BewijsMapFlatten.icl | 80 |
3 files changed, 80 insertions, 47 deletions
diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1 deleted file mode 100644 index d9b2608..0000000 --- a/week6/camil/9.4.1 +++ /dev/null @@ -1,23 +0,0 @@ -9.4.1 - proof by induction over as - -Induction base: - Suppose as = []. Then we have: - - map f (as ++ bs) // assumption as = [] - = map f ([] ++ bs) // definition of ++, rule 1 - = map f bs // definition of ++, rule 1 - = [] ++ (map f bs) // definition of map, rule 3 - = (map f []) ++ (map f bs) // assumption as = [] - = (map f as) ++ (map f bs). - -Induction step: - Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have: - - map f ([a:as] ++ bs) // definition of ++, rule 2 - = map f [a:as ++ bs] // definition of map, rule 4 - = [f a : map f (as ++ bs)] // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs) - = [f a : (map f as) ++ (map f bs)] // rewriting list - = [f a : map f as] ++ (map f bs) // definition of map, rule 4 - = (map f [a:as]) ++ (map f bs). - -By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs.
\ No newline at end of file diff --git a/week6/camil/9.4.2 b/week6/camil/9.4.2 deleted file mode 100644 index bc95352..0000000 --- a/week6/camil/9.4.2 +++ /dev/null @@ -1,24 +0,0 @@ -9.4.2 - proof by induction over xs - -Induction base: - Suppose xs = []. Then we have: - - flatten (map (map f) xs) // assumption xs = [] - = flatten (map (map f) []) // definition of map, rule 3 - = flatten [] // definition of flatten, rule 5 - = [] // definition of map, rule 3 - = map f [] // definition of flatten, rule 5 - = map f (flatten []) // assumption xs = [] - = map f (flatten xs). - -Induction step: - Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have: - - flatten (map (map f) [x:xs]) // definition of map, rule 4 - = flatten [map f x : map (map f) xs] // definition of flatten, rule 6 - = (map f x) ++ flatten (map (map f) xs) // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs) - = (map f x) ++ (map f (flatten xs)) // by 9.4.1 - = map f (x ++ (flatten xs)) // definition of flatten, rule 6 - = map f (flatten [x:xs]). - -By the principle of induction we have now proven that flatten (map (map f) xs) = map f (flatten xs) for any list of finite length xs.
\ No newline at end of file diff --git a/week6/camil/BewijsMapFlatten.icl b/week6/camil/BewijsMapFlatten.icl new file mode 100644 index 0000000..44cf7c1 --- /dev/null +++ b/week6/camil/BewijsMapFlatten.icl @@ -0,0 +1,80 @@ +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)
\ No newline at end of file |