-
Notifications
You must be signed in to change notification settings - Fork 4
/
impossible-programs.lhs
209 lines (133 loc) · 6.64 KB
/
impossible-programs.lhs
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
> {-# LANGUAGE FlexibleInstances #-}
> module Main where
> import Data.Maybe
*** Scheinbar unmögliche Programme
Mit [Bool] meinen wir den Typ der unendlichen 0/1-Folgen.
> p1, p2, p3 :: [Bool] -> Bool
> p1 xs = xs!!3
> p2 xs = xs!!4
> p3 xs = xs!!(2+1) && (xs!!8 || not (xs!!8))
> test1 = p1 == p2
> test2 = p1 == p3
Das liefert einen Fehler über eine fehlende `Eq`-Instanz, oder?
Weit gefehlt! Beide Programme terminieren. `test1` hat den Wert `False`,
`test2` hat den Wert `True`.
Das ist umso erstaunlicher, wenn man bedenkt, dass `[Bool]` *überabzahlbar
unendlich groß ist*.
*** Hintergrund: Abzählbarkeit und Überabzählbarkeit
Eine Menge heißt genau dann *abzählbar*, wenn es eine unendliche Liste gibt, in
der alle Elemente der Menge vorkommen.
Prototypbeispiel: Die Menge N der natürlichen Zahlen ist abzählbar.
0, 1, 2, 3, 4, ...
Die Menge Z der ganzen Zahlen ist ebenfalls abzählbar, insbesondere also genau
so groß wie die Menge der natürlichen Zahlen:
0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, ...
Übungsaufgabe: Zeige, dass auch die Menge Q der rationalen Zahlen abzählbar ist.
Eine Menge heißt genau dann *überabzählbar*, wenn sie nicht abzählbar ist.
Beispiel (Cantor): Die Menge R der reellen Zahlen ist überabzählbar.
Oder: Die Menge [Bool] aller unendlichen 0/1-Folgen ist überabzählbar.
Beweis durch das Cantorsche Diagonalargument:
Keine Liste von 0/1-Folgen kann *alle* 0/1-Folgen enthalten. Denn wenn zum
Beispiel folgende Liste gegeben ist:
01000101011011011...
11101011111101111...
10101010101010101...
11100011100010010...
10010101100100000...
11010101100100000...
.
.
.
Wenn man nun die Diagonale (von oben links nach unten rechts) durchgeht,
und jeweils die Gegenziffer wählt, erhält man eine 0/1-Folge, die sicher
nicht in der Liste vorkommt. Im Beispiel wäre das
100110...
Diese 0/1-Folge kann nicht das erste Element der Liste sein, denn sie
unterscheidet sich vom ersten Element ja an der vordersten Stelle. Sie kann
auch nicht das zweite Element der Liste sein, denn sie unterscheidet sich
vom zweiten Element ja an der zweitvordersten Stelle. Und so weiter!
*** Epsilon
Sei `p :: [Bool] -> Bool` ein beliebiges Prädikat.
Falls `p` erfüllbar ist, d.h. falls es eine 0/1-Folge `xs` gibt, sodass `p xs`,
dann soll `epsilon p` irgendeine 0/1-Folge sein, sodass `p (epsilon p)`.
Falls `p` nicht erfüllbar ist, dann kann `epsilon p` sein, was es möchte.
> epsilon :: ([Bool] -> Bool) -> [Bool]
> epsilon p = if p (False : xs)
> then False : xs
> else True : epsilon (p . (True:))
> where xs = epsilon (p . (False:))
Etwas schneller geht es dank Laziness so:
epsilon :: ([Bool] -> Bool) -> [Bool]
epsilon p = h : epsilon (p . (h:))
where
h = not $ p (False : epsilon (p . (False:)))
Wer es noch schneller möchte -- sodass auch Code wie `epsilon $ \xs -> xs !!
(10^10)` funktioniert, kann sich den Code von Martín Escardó ansehen.
*** Exists
Sei `p :: [Bool] -> Bool` ein beliebiges Prädikat.
Falls `p` erfüllbar ist, dann soll `exists p` ein Zeuge dieser Erfüllbarkeit
sein (in einem Maybe verpackt), also eine 0/1-Folge `xs`, sodass `p xs`.
Falls `p` nicht erfüllbar ist, soll `exists p` `Nothing` sein.
> exists :: ([Bool] -> Bool) -> Maybe [Bool]
> exists p = if p xs then Just xs else Nothing
> where xs = epsilon p
*** Forall
Sei `p :: [Bool] -> Bool` ein beliebiges Prädikat.
`forall p` soll dann und nur dann True sein, falls ``p auf jeder 0/1-Folge
konstant `True` ist.
> forall :: ([Bool] -> Bool) -> Bool
> forall p = isNothing $ exists (not . p)
Punktfrei geht es auch:
forall = not . isJust . exists . (not .)
*** Eq-Instanz für Funktionen [Bool] -> Bool
> instance Eq ([Bool] -> Bool) where
> f == g = forall $ \xs -> f xs == g xs
> -- "zwei Prädikate sind genau dann gleich, wenn sie auf jedem Argument
> -- gleich sind"
*** Exkurs: Beispiel für eine unstetige Funktion
Eine Funktion von R nach R ist genau dann stetig, wenn man ihren Graph zeichnen
kann, ohne den Stift abzusetzen. Eine stetige Funktion darf also keine
Sprungstellen besitzen.
f : R --> R
x |-> if x < 0 then -1 else if x == 0 then 0 else 1
Die Signumfunktion!
Sie ist aber nur definiert auf der Teilmenge
{ x in R | x < 0 oder x = 0 oder x > 0 }.
Konstruktiv kann man nicht zeigen, dass diese Teilmenge ganz R ist.
Die Funktion ist also nicht als total nachweisbar.
*** Wieso funktionieren die "scheinbar unmöglichen Programme"?
1. In Haskell kann man nur stetige Funktionen implementieren. (Wie in manchen
Schulen konstruktiver Mathematik auch.) Jede Funktion vom Typ `[Bool] -> Bool`
ist stetig.
2. In der Topologie gibt es folgenden Satz: Jede stetige Funktion, deren
Definitionsmenge kompakt ist, ist schon gleichmäßig stetig.
Die Menge `[Bool]` ist kompakt. (Eigentlich sollte man "Raum" statt "Menge"
sagen. Für Topologie-Fans: Das folgt sofort aus dem Satz von Tychonoff.)
3. Im Spezialfall von Funktionen `[Bool] -> Bool` bedeutet gleichmäßig
stetig: Eine solche Funktion ist genau dann gleichmäßig stetig, wenn es eine
Schranke `m` gibt, sodass die Funktion zur Berechnung ihres Ergebnisses nur
die ersten `m` Bits der Folge benötigt (unabhängig von der speziellen
Eingabefolge).
4. `epsilon` ruft sich selbst rekursiv auf. Wenn `p` als Schranke `m` hat, dann
hat das im rekursiven Aufruf verwendete Prädikat `(p . (False:))` als
Schranke `m-1`. Also terminiert nach `m` rekursiven Aufrufen das Verfahren.
*** Und die Moral von der Geschicht
In der Frage, ob Gleichheit von Funktionen vom Typ `A -> Bool` entscheidbar
ist, ist es nicht relevant, ob `A` endlich ist oder nicht. Tatsächlich
entscheidend ist, ob `A` *kompakt* ist oder nicht.
* Endliche Typen sind kompakt.
* `[Bool]` ist kompakt.
* Sind `A` und `B` kompakt, so auch der Produkttyp `(A,B)`.
* `Nat` und `Integer` sind nicht kompakt.
* Der Datentyp der "lazy naturals", welche auch `+infty` enthalten, ist kompakt.
Übungsaufgaben:
1. Übertrage die Funktion `epsilon` -- und damit auch `exists` und `forall`,
auf den Fall von Funktionen `NAT -> Bool` (statt `[Bool] -> Bool`). Dabei
soll `NAT` der Typ der "lazy naturals" sein, zum Beispiel definiert durch:
data NAT = Zero | Succ NAT
infty = Succ infty
2. Definiere eine Typklasse `Compact` und implementiere Instanzen für
`[Bool]` und `NAT` sowie eine generische Instanz `(Compact a, Compact b) =>
Compact (a,b)`.
3. Schreibe eine Funktion, die den größten Funktionswert einer gegebenen
Funktion `[Bool] -> Nat` bestimmt. (Lösung in impossible-maximum.hs.)