Quelltext der Seite Curry-Howard-Isomorphismus

Als '''Curry-Howard-Isomorphismus''' (auch '''Curry-Howard-Korrespondenz''') bezeichnet man die Interpretation von [[Datentyp|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 [[Intuitionismus (Logik und Mathematik)|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 (Logik)|Konjunktion]]'' <math>A\land B</math> ist ein Paar von Beweisen, <math>(p,q): A\times B</math> für sowohl <math>A</math> als auch <math>B</math>.

Ein Beweis für eine ''[[Disjunktion]]'' <math>A\lor B</math> ist ein Term aus der disjunkten Vereinigung von <math>A</math> und <math>B</math>, <math>A+B</math>.

Beweise für ''[[Implikationen]]'' <math>A\to B</math> sind totale Funktionen des Typs <math>A\to B</math>.

Die [[Negation#Logik|logische Negation]] <math>\lnot A</math> wird üblicherweise als Abkürzung für <math>A\to \bot</math> definiert, wobei <math>\bot</math> unter dem Curry-Howard-Isomorphismus dem [[Leerer Typ|leeren Typ]] entspricht.

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

== Beweisbeispiel ==
Der [[Satz vom ausgeschlossenen Dritten]] gilt in konstruktiven Logikkalkülen normalerweise nicht (würde er gelten, wäre jede Aussage entscheidbar, was entweder [[Gödelscher Unvollständigkeitssatz|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 <math>A</math>, ein Beweis für
: <math>\lnot\lnot(A\lor\lnot A)</math>,
was unter Curry-Howard und mit Auflösung der Negationsabkürzung ein ''Term'' des Typs
: <math>((A+(A\to\bot))\to\bot)\to\bot</math>
wird. Der [[Lambda-Ausdruck]]
: <math>\lambda f.f(\kappa_2(\lambda a.f(\kappa_1 a)))</math>
stellt einen Term des gewünschten Typs dar, wobei <math>\kappa_1 \colon A\to(A+(A\to\bot))</math> und <math>\kappa_2 \colon (A\to\bot)\to(A+(A\to\bot))</math> die Injektionen in den zweistelligen Summentyp sind.

== Praktische Anwendungen ==
Verfügbare und benutzbare Beweisassistenten/Programmiersprachen wie [[Coq (Software)|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 ==
* [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf Simon Thompson: Type Theory and Functional Programming] (PDF; 1,3&nbsp;MB)
* [http://www.cse.chalmers.se/research/group/logic/book/book.pdf Bengt Nordström, Kent Petersson, Jan M. Smith: Programming in Martin-Löfs Type Theory] (PDF; 709&nbsp;kB)
* [http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf Philip Wadler: Propositions as Types] (PDF; 261&nbsp;kB)

[[Kategorie:Typentheorie]]