1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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)
|
