Mercurial > 12ws.info2

comparison exercises/src/Exercise_10.hs @ 24:34fea195e238

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
beautify layout
author Markus Kaiser <markus.kaiser@in.tum.de>
date Fri, 21 Dec 2012 01:44:45 +0100
parents f9386825bf71
children ce9610f08925
comparison
equal deleted inserted replaced
23:f9386825bf71 24:34fea195e238
8 8
9 {---------------------------------------------------------------------} 9 {---------------------------------------------------------------------}
10 {- Aufgabe G10.1 -} 10 {- Aufgabe G10.1 -}
11 11
12 {- 12 {-
13 \alpha ist wie in den Folien definiert.
14 13
14 Abstraktionsfunktion alpha:
15
16 \alpha [] = {} -- alpha_empty
17 \alpha (x:xs) = {x} \union \alpha xs -- alpha_cons
15 18
16 Simulationseigenschaften: 19 Simulationseigenschaften:
17 20
18 R_empty: \alpha empty = {} 21 1. \alpha empty = {} -- sim_empty
19 : a empty = {} 22 2. \alpha (insert x xs) = {x} \union \alpha xs -- sim_insert
23 3. isin x xs = x \in \alpha xs -- sim_isin
24 4. size xs = |\alpha xs| -- sim_size
20 25
26 Implementierung 1 - Listen mit Duplikaten:
21 27
22 R_insert: \alpha (insert x xs) = {x} \union \alpha xs 28 empty = [] -- imp_empty
23 : a (insert x xs) = {x} union a xs 29 insert x xs = x : xs -- imp_insert
30 isin x xs = elem x xs -- imp_isin
31 size xs = length (nub xs) -- imp_size
24 32
33 elem _ [] = False -- elem_empty
34 elem x (y:ys) = x == y || elem x ys -- elem_cons
25 35
26 R_isin: isin x xs = x \in \alpha xs 36 nub [] = [] -- nub_empty
27 : isin x xs = x in a xs 37 nub (x:xs) | x `elem` xs = nub xs -- nub_cons_elem
38 | otherwise = x : nub xs -- nub_cons_notelem
28 39
40 Korrektheitsbeweise:
29 41
30 R_size: size xs = |\alpha xs| 42 1. \alpha empty
31 : size xs = |a xs| 43 =
32 44 2. \alpha (insert x xs)
33 45 =
46 3. isin x xs
47 =
48 4. size xs
49 =
34 50
35 Hilfslemmata: 51 Hilfslemmata:
36 52
37 L_elem(xs): elem x xs = x in a xs 53 elem x xs = x \in \alpha xs -- lemma_elem
38 Proof by structural induction on xs
39 54
40 Base case: L_elem([]) 55 Proof by structural induction on xs
41 To show:
42 56
43 Induction step: L_elem(ys) => Lemma(y : ys) 57 Base case: lemma_elem([])
44 IH: 58 To show:
45 To show:
46 59
60 Induction step: lemma_elem(ys) => lemma_elem(y : ys)
61 IH:
62 To show:
47 63
48 L_length(xs): length (nub xs) = |a xs| 64 length (nub xs) = |\alpha xs| -- lemma_length
49 Proof by structural induction on xs
50 65
51 Base case: L_elem([]) 66 Proof by structural induction on xs
52 To show:
53 67
54 Induction step: L_elem(ys) => Lemma(y : ys) 68 Base case: lemma_length([])
55 IH: 69 To show:
56 To show: 70
71 Induction step: lemma_length(ys) => lemma_length(y : ys)
72 IH:
73 To show:
74
75 Proof by cases:
76 Case:
77
78 Case:
57 79
58 -} 80 -}
59 81
60 82
61 83