Curry-Howard-Isomorphismus

Als Curry-Howard-Isomorphismus (auch Curry-Howard-Korrespondenz) bezeichnet man die Interpretation von Typen als logische Aussagen und von Termen eines bestimmten Typs als Beweise der zum Typ gehörenden Aussage; und umgekehrt. Benannt ist er nach den Mathematikern Haskell Brooks Curry und William Alvin Howard.

Halb-formale Beschreibung

Der Begriff der Wahrheit wird ausgetauscht mit dem Begriff der Beweisbarkeit, folgt also dem intuitionistischen Verständnis von Mathematik. Eine Aussage ist beweisbar, wenn es einen Term gibt, der den zur Aussage passenden Typ hat.

Einfache Junktoren

Ein Beweis für eine Konjunktion ${\displaystyle A\land B}$ ist ein Paar von Beweisen, ${\displaystyle (p,q):A\times B}$ für sowohl ${\displaystyle A}$ als auch ${\displaystyle B}$.

Ein Beweis für eine Disjunktion ${\displaystyle A\lor B}$ ist ein Term aus der disjunkten Vereinigung von ${\displaystyle A}$ und ${\displaystyle B}$, ${\displaystyle A+B}$.

Beweise für Implikationen ${\displaystyle A\to B}$ sind totale Funktionen des Typs ${\displaystyle A\to B}$.

Die logische Negation ${\displaystyle \lnot A}$ wird üblicherweise als Abkürzung für ${\displaystyle A\to \bot }$ definiert, wobei ${\displaystyle \bot }$ unter dem Curry-Howard-Isomorphismus dem leeren Typ entspricht.

Quantoren

Eine universell quantifizierte Aussage ${\displaystyle \forall {a\in A}:{X(a)}}$ wird zu einer Funktion, bei der der Typ des Funktionswertes vom Wert des Funktionsarguments abhängig ist. Hier trifft man also auf dependent types.

Der Beweis einer existenziell quantifizierten Aussage ${\displaystyle \exists {a\in A}:{X(a)}}$ muss zwei Dinge liefern: ein ${\displaystyle A}$-Element ${\displaystyle a}$, und einen Beweis für ${\displaystyle X(a)}$.

Beweisbeispiel

Der Satz vom ausgeschlossenen Dritten gilt in konstruktiven Logikkalkülen normalerweise nicht (würde er gelten, wäre jede Aussage entscheidbar, was entweder Ausdrucksschwäche oder Inkonsistenz nach sich zieht). Eine Version mit doppelter Negation unterhalb der Allquantisierung über Aussagen lässt sich jedoch durch Angabe eines Beweisterms belegen. Gesucht ist, für beliebige Aussagen ${\displaystyle A}$, ein Beweis für

${\displaystyle \lnot \lnot (A\lor \lnot A)}$,

was unter Curry-Howard und mit Auflösung der Negationsabkürzung ein Term des Typs

${\displaystyle ((A+(A\to \bot ))\to \bot )\to \bot }$

wird. Der Lambda-Ausdruck

${\displaystyle \lambda f.f(\kappa _{2}(\lambda a.f(\kappa _{1}a)))}$

stellt einen Term des gewünschten Typs dar, wobei ${\displaystyle \kappa _{1}\colon A\to (A+(A\to \bot ))}$ und ${\displaystyle \kappa _{2}\colon (A\to \bot )\to (A+(A\to \bot ))}$ die Injektionen in den zweistelligen Summentyp sind.

Praktische Anwendungen

Verfügbare und benutzbare Beweisassistenten/Programmiersprachen wie Coq, Epigram und Agda machen vom Curry-Howard-Isomorphismus Gebrauch, indem sie es gestatten, Beweise als Programme und Aussagen als Typen anzugeben. Der Typprüfer übernimmt dabei die Aufgabe, die angegebenen Beweise zu verifizieren.

Quellen

• Simon Thompson: Type Theory and Functional Programming (PDF; 1,3 MB)
• Bengt Nordström, Kent Petersson, Jan M. Smith: Programming in Martin-Löfs Type Theory (PDF; 709 kB)
• Philip Wadler: Propositions as Types (PDF; 261 kB)