Die Computationale Interpretation von Intermediären Logiken

Eine der bemerkenswertesten Entdeckungen in der Geschichte der Logik ist, dass formale Beweise als zertifizierte Computer-Programme verstanden werden können. Jede Schlussform entspricht einem natürlichen Konstrukt einer funktionalen Programmiersprache. Dieses Resultat wurde zunächst für konstruktive Beweise formuliert und dann auf klassische Beweise übertragen. Letztere können auch nicht- effektive Prinzipien, wie den "Satz vom ausgeschlossenen Dritten" enthalten. Diese Korrespondenz zwischen Beweisen und Programmen wird Curry-Howard- Isomorphismus genannt; sie macht Logik zu einer mächtigen, fehlerfreien Programmiersprache. Heutzutage versteht man wie verschiedene, ausdrucksstarke logische und mathematische Regelsysteme computational interpretiert werden können. Aber darunter sind leider nicht alle Systeme, die relevant wären. Außerdem ist die Interpretation nicht immer so effizient wie möglich. Dieses Projekt zielt darauf ab, eine wichtige Lücke in der Theorie computationaler Beweis-Interpretationen zu schließen. Nämlich für intermediäre Logiken - darunter versteht man Logiken die stärker als intuitionisitsche, aber schwächer als die klassische Logik sind gibt es, von seltenen Ausnahmen abgesehen, bisher keine natürlichen Schlusssysteme, die entsprechende Curry-Howard-Korrespondenzen zulassen würden. Aber sie haben großes Potential aus berechnungs-orientierter Sicht. Tatsächlich enthalten viele intermediäre Logiken nicht-kontstruktive Axiome, haben aber dennoch spezifische konstruktive Eigenschaften und sind generell der intuitionistischen (konstruktiven) Logik näher als der klassischen. Darüber hinaus können damit Programmiermechanismen, wie beispielsweise Parallelität und Nachrichten- Übergabe zwischen nebenläufigen Prozessen modelliert werden. Da viele intermediäre Logiken als Hypersequential-Kalkül (im Sinne Avrons) formalisiert werden können, besteht die Chance auf eine vollständige Theorie entsprechender Curry-Howard-Korrespondenzen.

The goal of this project was to advance our understanding of parallel computation by means of logic. Parallel programs allow to make several different computations at the same time, and thus solve computational problems faster and more efficiently than sequential programs. Unfortunately, parallel programming is prone to error and there are very few methods that can be used to prove correctness of parallel programs. In this project we used logic as a tool to design and reason about parallel functional programs. We discovered in particular that multiplicative linear logic can be used as a type system for a new, simple, yet expressive parallel extension of simply typed lambda calculus, which is the basis of all functional programming languages. All programs that one can type are correct by construction, that is, they terminate, they don't have deadlocks, they give a result, and always give the same result independently from how they are evaluated. Other results of this project show that intermediate logics, that is, logics that encode constructive reasoning but are contained in classical logical reasoning, can act as type systems for expressive functional programming languages. Namely, one can start from a communication topology that programs should employ for exchanging messages, and automatically obtain a logic that types only processes that communicate according to the topology. This allows complex communication mechanisms, whose correctness and termination is guaranteed by the type system itself.