Curry-Howard, Spielsemantik und der Satz von Herbrand

Der berühmte Satz von Herbrand sagt, dass wenn wir einen Beweis in der klassischen Prädikatenlogik erster Stufe von der Existenz eines Elements haben, das eine gewisse propositionale Aussage erfüllt, dann können wir daraus eine Herbrand-Disjunktion extrahieren: eine vollständige endliche Liste von möglichen Zeugen---also Elementen, die diese Aussage erfüllen. Der Satz von Herbrand gibt Aufschluss über den direkten komputationalen Inhalt der klassischen Prädikatenlogik: nämlich die Liste der Zeugen, die in einer Herbrand-Disjunktion enthalten sind. Unter dieser Sichtweise ist es von großem Interesse, automatisch Beweise in Computerprogramme zu übersetzen, um dadurch aus jedem prädikatenlogischen Beweis einer Existenzaussage eine passende Liste von Zeugen zu berechnen. Es ist eine der bemerkenswertesten Entdeckungen in der Geschichte der Logik, dass Beweise sich nicht nur als zertifizierte Computerprogramme sehen lassen, sondern in der Tat auch solche sind. Ein jeder logische Schluss entspricht einem natürlichen Sprachelement einer funktionalen Programmiersprache. Dies wurde zunächst für konstruktive Beweise festgestellt, und ist, obwohl es vernünftig scheint, nicht ganz trivial zu beweisen. Das Ergebnis wurde in Folge auf klassische Beweise ausgedehnt, also auf Beweise, die auch ineffective Regeln wie den Satz vom ausgeschlossenen Dritten verwenden können. Diese Korrespondenz zwischen Beweisen und Programmen wird Curry-Howard-Isomorphismus genannt. Vor kurzem hat der Antragsteller eine Curry-Howard-Interpretation der klassischen Prädikatenlogik eingeführt, die einen eleganten und natürlichen Beweis vom Satz von Herbrand ermöglicht. Diese Interpretation beschreibt klassische Beweise als lernende Computerprogramme, die auf eine logisch korrekte Weise eine Versuch-und-Irrtum-Methode implementieren: sie formulieren Hypothesen, überprüfen diese, und korrigieren sie, wenn sie sich als falsch herausgestellt haben. Diese konstruktive Interpretation ist von Coquands Spielsemantik inspiriert, und hat mit dieser auch eine enge Verbindung: ein Programm liefert eine berechenbare Gewinnstrategie mit Backtracking für eine Klasse von einfachen Spielen, in der die beiden Spieler über die Wahrheit einer Aussage diskutieren. Das Ziel dieses Projekts ist es, mit Hilfe dieser Curry-Howard-Interpretation und Spielsemantik neue Ergebnisse über den Satz von Herbrand zu gewinnen. Mit Hilfe der Spielsemantik wollen wir zeigen, dass bei Expansionsbäumen mit Schnitt die Schnitt- Elimination immer terminiert. Über die Herbrand-Disjunktionen, die durch unsere Curry- Howard-Korrespondenz entstehen, wollen wir ein Konfluenzresultat formulieren und beweisen; dies ist besonders signifikant, da im Allgemeinen klassische Kalküle nicht konfluent sind. Wir wollen außerdem beweisen, dass unser Kalkül eine semi- intuitionistische Logik interpretieren kann, die eine klassisch starke Form des Markov- Prinzips beweist, und eine komputational reichhaltigere Version des Satzes von Herbrand erlaubt, bei dem die Zeugen in der Herbrand-Disjunktion auch bei beliebig komplizierten existenzquantifizierten Formeln immer abgeschlossene Terme sind.Schließlich möchten wir unsere Curry-Howard-Interpretation auch auf diePrädikatenlogik zweiter Stufe ausdehnen, und mit den ersten Schritten zur Implementierung beginnen.

In the modern world, computing devices are everywhere and not only can operate in parallel, but also communicate with each other by sending and receiving messages. This computing paradigm is known as concurrency. With this project we have connected in a new way logic to concurrent computation. We have obtained concurrent functional programming languages which corresponds to logical proofs. Thanks to this correspondence, known in general as Curry-Howard isomorphism, one can study more easily their complicated computational properties. In particular, we have found that Gödel propositional logic, Dummetts first-order logic, Markovs logic can give type systems for concurrent programs. We also used in a new way game semantics to estimate the cost of running functional programs. Thanks to famous results in logic, evaluation of simply typed functional programs can be seen as a game-like interaction of strategies for certain games. Proving general results about lengths of two-players games brings therefore automatically complexity bounds on the execution of programs. We focused on a very general mathematical definition of game that includes standard games like chess. We obtained refined results about interaction between strategies that can revise and change their previous moves and found a method to measure strategy-complexity. As a consequence, one can compute new, more tight bounds about the complexity of evaluating typed functional programs.