|
23
|
1 module Exercise_10 (module Join, module SafeMap) where |
|
|
2 |
|
|
3 {- Library DO NOT CHANGE -} |
|
|
4 import SafeMap (SafeMap, empty, update, lookup) |
|
|
5 import Join (Field, doJoin, doJoinFormat, parseFormat) |
|
|
6 {- End Library -} |
|
|
7 |
|
|
8 |
|
|
9 {---------------------------------------------------------------------} |
|
|
10 {- Aufgabe G10.1 -} |
|
|
11 |
|
|
12 {- |
|
24
|
13 |
|
|
14 Abstraktionsfunktion alpha: |
|
23
|
15 |
|
24
|
16 \alpha [] = {} -- alpha_empty |
|
|
17 \alpha (x:xs) = {x} \union \alpha xs -- alpha_cons |
|
23
|
18 |
|
|
19 Simulationseigenschaften: |
|
|
20 |
|
24
|
21 1. \alpha empty = {} -- sim_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 |
|
23
|
25 |
|
24
|
26 Implementierung 1 - Listen mit Duplikaten: |
|
23
|
27 |
|
24
|
28 empty = [] -- imp_empty |
|
|
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 |
|
23
|
32 |
|
24
|
33 elem _ [] = False -- elem_empty |
|
|
34 elem x (y:ys) = x == y || elem x ys -- elem_cons |
|
23
|
35 |
|
24
|
36 nub [] = [] -- nub_empty |
|
|
37 nub (x:xs) | x `elem` xs = nub xs -- nub_cons_elem |
|
|
38 | otherwise = x : nub xs -- nub_cons_notelem |
|
23
|
39 |
|
24
|
40 Korrektheitsbeweise: |
|
23
|
41 |
|
24
|
42 1. \alpha empty |
|
|
43 = |
|
|
44 2. \alpha (insert x xs) |
|
|
45 = |
|
|
46 3. isin x xs |
|
|
47 = |
|
|
48 4. size xs |
|
|
49 = |
|
23
|
50 |
|
|
51 Hilfslemmata: |
|
|
52 |
|
24
|
53 elem x xs = x \in \alpha xs -- lemma_elem |
|
|
54 |
|
|
55 Proof by structural induction on xs |
|
23
|
56 |
|
24
|
57 Base case: lemma_elem([]) |
|
|
58 To show: |
|
23
|
59 |
|
24
|
60 Induction step: lemma_elem(ys) => lemma_elem(y : ys) |
|
|
61 IH: |
|
|
62 To show: |
|
|
63 |
|
|
64 length (nub xs) = |\alpha xs| -- lemma_length |
|
23
|
65 |
|
24
|
66 Proof by structural induction on xs |
|
23
|
67 |
|
24
|
68 Base case: lemma_length([]) |
|
|
69 To show: |
|
23
|
70 |
|
24
|
71 Induction step: lemma_length(ys) => lemma_length(y : ys) |
|
|
72 IH: |
|
|
73 To show: |
|
23
|
74 |
|
24
|
75 Proof by cases: |
|
|
76 Case: |
|
|
77 |
|
|
78 Case: |
|
23
|
79 |
|
|
80 -} |
|
|
81 |
|
|
82 |
|
|
83 |
|
|
84 {---------------------------------------------------------------------} |
|
|
85 {- Aufgabe G10.2 -} |
|
|
86 |
|
|
87 {- siehe SetPairList.hs -} |
|
|
88 |
|
|
89 |
|
|
90 |
|
|
91 {---------------------------------------------------------------------} |
|
|
92 {- Aufgabe G10.3 -} |
|
|
93 |
|
|
94 {- siehe Queue.hs und SuperQueue.hs -} |
|
|
95 |
|
|
96 {- |
|
|
97 Definition von \alpha: |
|
|
98 |
|
|
99 \alpha (Queue front kcab) = undefined |
|
|
100 |
|
|
101 |
|
|
102 Simulationseigenschaften: (5) |
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 Beweise: |
|
|
107 -} |
|
|
108 |
|
|
109 |
|
|
110 |
|
|
111 {---------------------------------------------------------------------} |
|
|
112 {- Aufgabe H10.1 -} |
|
|
113 |
|
|
114 {- siehe SafeMap.hs -} |
|
|
115 |
|
|
116 |
|
|
117 |
|
|
118 {---------------------------------------------------------------------} |
|
|
119 {- Aufgabe H10.2 -} |
|
|
120 |
|
|
121 {- siehe Join.hs -} |
|
|
122 |
|
|
123 |
|
|
124 |
|
|
125 {---------------------------------------------------------------------} |
|
|
126 {- Aufgabe H10.3 -} |
|
|
127 |
|
24
|
128 {- siehe Morsi.hs -} |
