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. Benannt ist er nach den Mathematikern Haskell Brooks Curry und William Alvin Howard.

Halb-formale Beschreibung[Bearbeiten | Quelltext 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 | Quelltext bearbeiten]

Ein Beweis für eine Konjunktion ist ein Paar von Beweisen, für sowohl als auch .

Ein Beweis für eine Disjunktion ist ein Term aus der disjunkten Vereinigung von und , .

Beweise für Implikationen sind totale Funktionen des Typs .

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

Quantoren[Bearbeiten | Quelltext bearbeiten]

Eine universell quantifizierte Aussage 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 muss zwei Dinge liefern: ein -Element , und einen Beweis für .

Beweisbeispiel[Bearbeiten | Quelltext 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 , ein Beweis für

,

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

wird. Der Lambda-Ausdruck

stellt einen Term des gewünschten Typs dar, wobei und die Injektionen in den zweistelligen Summentyp sind.

Praktische Anwendungen[Bearbeiten | Quelltext 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 | Quelltext bearbeiten]