Curry-Howard Correspondence

In Haskell oder Coq. Der Typ Void hat keine Werte. Er entspricht "Falsch" ($\bot$). Eine Funktion Void -> A ("Aus Falsch folgt alles") ist trivial implementierbar (weil man Void nie aufrufen kann). Der Typ Either A B entspricht $A \lor B$. Der Typ (A, B) entspricht $A \land B$.

1. Constructivism

In klassischer Logik (Hilbert) gilt: $A \lor \neg A$ (Tertium Non Datur). Entweder es regnet, oder nicht. In Curry-Howard gilt das nicht automatisch. Denn um $A \lor \neg A$ zu beweisen, bräuchte man ein Programm, das entscheidet, ob A wahr ist oder nicht. (Halteproblem!). Curry-Howard entspricht der intuitionistischen Logik. Ein Beweis muss konstruieren.

2. Lambda Cube

Eine Landkarte der Typ-Systeme.

• Einfache Typen -> Aussagenlogik.
• Polymorphismus (Generics) -> Quantoren 2. Ordnung.
• Dependent Types -> Prädikatenlogik 1. Ordnung. Alle Logik-Systeme lassen sich auf Typ-Systeme abbilden.

1. Die Korrespondenz-Tabelle

Um die Tiefe zu verstehen, muss man die direkten Entsprechungen sehen:

• Aussage (Proposition) $P \implies Q$: Ein Funktionstyp P -> Q.
• Aussage $P \land Q$: Ein Produkt-Typ (Paar) (P, Q).
• Aussage $P \lor Q$: Ein Summen-Typ (Union) Either P Q.
• Beweis durch Induktion: Eine rekursive Funktion über einem induktiven Datentyp.
• Normalisierung eines Beweises: Die Ausführung eines Programms. Wenn ein Beweis "vereinfacht" wird, ist das exakt das Gleiche wie ein Programm, das berechnet wird.

2. Curry-Howard-Lambek Isomorphismus

In der Forschung wird die Korrespondenz oft auf drei Säulen erweitert (Lambek kam hinzu):

1. Logik: Beweistheorie.
2. Informatik: Typentheorie.
3. Mathematik: Kategorientheorie. Eine logische Implikation ist nicht nur ein Funktionstyp, sondern auch ein "exponentielles Objekt" in einer Kategorie. Das bedeutet, dass wir zwischen Logik, Programmen und abstrakten mathematischen Strukturen (Kategorien) verlustfrei übersetzen können. Ein Problem in der Software-Verifikation lässt sich also oft als Problem der Geometrie oder Algebra lösen.

3. Die Grenzen: Vollständigkeit & Konsistenz

Curry-Howard gilt nur in totale Sprachen. In einer Sprache wie Python kannst du eine Funktion schreiben: def cheat(): return cheat(). Diese Funktion hat jeden beliebigen Typ (da sie nie fertig wird). Logisch gesehen bedeutet das: In einer Sprache mit Endlosschleifen ist die Logik inkonsistent, man kann "ALLES" beweisen (Ex Falso Quodlibet). Deshalb nutzen Beweisassistenten wie Coq oder Agda strikte Termination-Checker. Nur wenn das Programm garantiert anhält, ist es ein gültiger Beweis. Das ist der Grund, warum "echte" funktionale Programmierung manchmal so restriktiv wirkt – sie will eine saubere Logik bleiben.