Curry-Howard-Isomorphismus

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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.

Halb-formale Beschreibung[Bearbeiten]

Der Begriff der Wahrheit wird ausgetauscht mit dem Begriff der Beweisbarkeit. Man begibt sich also auf intuitionistisches Gebiet. Eine Aussage ist beweisbar, wenn es einen Term gibt, der den zur Aussage passenden Typ hat.

Einfache Junktoren[Bearbeiten]

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

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

Beweise für Implikationen A\to B sind totale Funktionen des Typs A\to B.

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

Quantoren[Bearbeiten]

Eine universell quantifizierte Aussage \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 \exists {a\in A}: {X(a)} muss zwei Dinge liefern: ein A-Element a, und einen Beweis für X(a).

Beweisbeispiel[Bearbeiten]

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 A, ein Beweis für

\lnot\lnot(A\lor\lnot A),

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

((A+(A\to\bot))\to\bot)\to\bot

wird. Der Lambda-Ausdruck

\lambda f.f(\kappa_2(\lambda a.f(\kappa_1 a)))

stellt einen Term des gewünschten Typs dar, wobei \kappa_1:A\to(A+(A\to\bot)) und \kappa_2:(A\to\bot)\to(A+(A\to\bot)) die Injektionen in den zweistelligen Summentyp sind.

Praktische Anwendungen[Bearbeiten]

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[Bearbeiten]