Im Verlauf des 20. Jahrhunderts wurde ein tiefgreifender und allgemeiner Zusammenhang zwischen Typsystemen und der mathematischen Logik entdeckt. Es verhält sich so, dass jede logische Formel eine Entsprechung als Typ besitzt, wobei jeder der logischen Verknüpfungen eine entsprechende Typkonstruktion zugeordnet ist.
Darüber hinaus vertieft sich dieser Zusammenhang sogar noch, dergestalt dass dem Beweis einer logischen Formel ein Programm entspricht, das einen Wert des Typs konstruiert. Diesen Wert nennt man Zeuge. Wurde ein Zeuge gefunden, muss der Typ mindestens durch diesen bewohnt sein, so ähnlich wie in der Mengenlehre eine Menge nichtleer sein muss, wenn ein Element der Menge gefunden wurde.
Allerdings konstruiert nicht jedes Programm einen Zeugen auf korrekte Art und Weise. Für eine korrekte Konstruktion muss das Programm ein rein funktionales sein und für jedes Argument terminieren. Auf dieser Anforderung aufbauend wurden hinreichend strenge Typsysteme erarbeitet; man nennt sie Typentheorien.
Das Typsystem von Rust genügt diesen Anforderungen nicht. Zudem reicht es lediglich zur Kodierung von Formeln ohne Quantoren. Zur allgemeinen Kodierung von prädikatenlogischer Formeln benötigt man abhängige Typen. Ein Typsystem mit abhängigen Typen ist eine Verallgemeinerung der parametrischen Polymorphie, wo Typen nicht nur durch Typen parametrisiert werden können, sondern durch beliebige Terme.
Zum tieferen Verständnis des Typsystems möchte ich in diesem Kapitel aber trotzdem die Konstruktion von Beweisen durch Programme diskutieren.
Die enge Beziehung zwischen logischen Formeln und Typen nennt man Curry-Howard-Korrespondenz. Sie wird durch die folgende Tabelle vermittelt.
| Bezeichnung | Formel | Typ | Bezeichnung |
|---|---|---|---|
| Konjunktion | A ∧ B | A × B | Produkt |
| Disjunktion | A ∨ B | A + B | Summe |
| Implikation | A → B | A → B | Funktionentyp |
| Allquantifizierung | (∀x∈U)P(x) | ∏x: U P(x) | abhängiges Produkt |
| Existenzquantifizierung | (∃x∈U)P(x) | ∑x: U P(x) | abhängige Summe |
| falsche Formel | falsch | 0 | leerer Typ |
| wahre Formel | wahr | 1 | Einheitstyp |
Wir wollen beweisen, dass es sich bei
A ∧ B → A
um eine tautologische Formel handelt. Zunächst können wir sagen, dass die Formel genau dann tautologisch ist, wenn
(∀A) (∀B) (A ∧ B → A)
eine wahre Aussage ist. Das ist wiederum per Curry-Howard-Korrespondenz damit bedeutungsgleich, dass der Typ
∏A ∏B (A × B → A)
ein bewohnter ist. Dies können wir bestätigen, denn mit der Projektion
proj0 := A ↦ B ↦ (a, b) ↦ a
oder äquivalent notiert
proj0(A)(B)(a, b) := a
ist ein Zeuge des Typs konstruiert. In Rust nimmt diese Projektion die Gestalt
fn proj0<A, B>((a, _): (A, B)) -> A {a}
an. Weil diese Funktion rein funktional und total ist, erbringt dies den Beweis, dass die ursprüngliche Formel tautologisch ist.
Nebenbei bemerkt ist
fn proj0<A, B>(a: A, _: B) -> A {a}
eine äquivalente Formulierung der Funktion, denn eine Funktion mit Tupel als Argument und die entsprechende Funktion in mehreren Argumenten bedeuten im Wesentlichen dasselbe.
Konstruiert man auf die beschriebene Art immer mehr Beiweise, wird mit der Zeit immer klarer erkennbar, dass die Methodik einem vertrauten logischen Kalkül entspricht, der als natürliches Schließen geläufig ist.
Wir betrachten als Beispiel die tautologische Formel
(A ∨ B) ∧ (A → B) ∧ (A → C) → C.
Zunächst erfolgt ein syntaktischer Beweis durch natürliches Schließen.
| Abh. | Nr. | Formel | Notiz |
|---|---|---|---|
| 1 | 1 | A ∨ B | Prämisse |
| 2 | 2 | A → C | Prämisse |
| 3 | 3 | B → C | Prämisse |
| 4 | 4 | A | Annahme |
| 2, 4 | 5 | C | Modus ponens, 2, 4 |
| 6 | 6 | B | Annahme |
| 3, 6 | 7 | C | Modus ponens, 3, 6 |
| 1, 2, 3 | 8 | C | ODER-Beseitigung, 1, 4→5, 6→7 |
Schreibt man die in der Tabelle enthaltenen Schlussfolgerungen strukturiert auf, erkennt man, dass die Methodik äquivalent zum folgenden Programm ist. Die Tabelle schaut recht umständlich aus. Im Wesentlichen steckt da aber lediglich eine Fallunterscheidung drin (in Form der Disjunktions-Beseitigung), und in den beiden Fällen jeweils eine Funktionsapplikation (in Form des Modus ponens).
enum Sum<A, B> {Left(A), Right(B)}
use Sum::{Left, Right};
fn proof<A, B, C>(
s: Sum<A, B>,
fa: fn(A) -> C,
fb: fn(B) -> C
) -> C {
match s {
Left (a) => fa(a),
Right(b) => fb(b)
}
}
Das Beispiel verdeutlicht, dass das natürliche Schließen und die Konstruktion von Zeugen unter Anwendung des Lambda-Kalküls im Wesentlichen dasselbe sind.
Im Unterschied zu den anderen logischen Verknüpfungen besitzt die Negation ¬A keine eigenständige Typkonstruktion. Stattdessen betrachtet man die äquivalente Aussage A → falsch, deren Entsprechung A → 0 ist, das ist die Signatur divergenter Funktionen. Der Typ 0 ist der leere Typ, ein Typ analog zur leeren Menge.
Beispielsweise kann man die Kontraposition
(A → B) → (¬B → ¬A)
zeigen. Hat man nämlich eine Funktion f vom Typ
A → B und
eine Funktion g vom Typ
B → 0, kann man diese
Verketten und erhält als Resultat eine Funktion vom Typ
A → 0. Wir finden
demzufolge den Term
A ↦ B
↦ (f: A → B)
↦ (g: B → 0) ↦ (a: A) ↦ g(f(a)),
zu dem das Programm
gehört. Prinzipiell könnten wir diese Funktion auch schönfinkeln.
Weil es sich mit Closures in Rust allerdings kompliziert verhält,
lassen wir das an dieser Stelle lieber bleiben.
Für die Umkehrung
(¬B → ¬A)
→ (A → B)
gelingt es uns nicht, einen Term zu konstruieren, egal wir sehr
wir uns darum bemühen. Das ist per se unmöglich, solange man sich auf
die intuitionistische Logik beschränkt. Die Hinzunahme der zusätzlichen
axiomatischen Regel ¬¬A → A
führt zur schwächeren klassischen Aussagenlogik. Man bezeichnet sie
als Beseitigung der Doppelnegation. Erst in dieser ist
die Kontraposition eine äquivalente Umformung.
Den Zeugen kann man dann wie folgt konstruieren. Prämisse ist
¬B → ¬A. Daraus erhält man mit
der bereits gezeigten Kontraposition die Formel
¬¬A → ¬¬B.
Es existiert immer eine Abbildung des Typs zu
A → ¬¬A. Nach dem genannten Axiom existiert
nun eine Abbildung des Typs zu
¬¬B → B. Verkettet man die drei
aufgeführten Abbildungen, resultiert dies in der gewünschten Abbildung
des Typs A → B.
Ich will das Programm dazu nicht weiter ausführen. An dieser
Stelle ist es dann wohl günstig, auf ein System wie Coq oder Lean
umzusteigen, wenn man weiter voranschreiten möchte.
Die Regel A → ¬¬A, das ist die
Einführung der Doppelnegation, braucht man nicht axiomatisch
anzunehmen, denn sie gilt selbst in der intuitionistischen Logik, wie
der Zeuge
(a: A)
↦ (f: A → 0) ↦ f(a)
zeigt.
fn proof<A, B>(f: fn(A) -> B, g: fn(B) -> !, a: A) -> ! {
g(f(a))
}
Literatur