Vivek Nigam’s PhD Thesis [pdf] [presentation]
Exploiting non-canonicity in the sequent calculus
Thesis Advisor: Dale Miller
Prepared at LIX, Ecole Polytechnique, PARSIFAL team.
Public defense at 14:30 on 18 September 2009.
Location: Amphi Lagarrigue – Ecole Polytechnique, Palaiseau, France
Instructions on how to reach Ecole Polytechnique can be found here.
You can find here a video where I am declared Docteur.
Jury
Jean-Marc Andreoli - Reviewer
Iliano Cervesato
Roy Dyckhoff - Reviewer
Ian Mackie
Damiano Mazza
Dale Miller - Advisor
Elaine Pimentel
Abstract
Although logic and proof theory have been successfully used as a framework for the specification of computation systems, there is still an important gap between the systems that logic can capture and the systems used in practice. This thesis attempts to reduce this gap by exploiting, in the context of the computation-as-proof-search paradigm, two non-canonical aspects of sequent calculus, namely the polarity assignment in focused proofs and the linear logic exponentials. We exploit these aspects in three different domains of computer science: tabled deduction, logical frameworks, and algorithmic specifications.
This thesis provides a proof theoretic explanation for tabled deduction by exploiting the fact that in intuitionistic logic atoms can be assigned arbitrary polarity. A table is a partially ordered set of formulas and is incorporated into a proof via multicut derivations. Here, we consider two cases: the first case is when tables contain only finite successes and the second case is when tables may also contain finite failures. We propose a focused proof system for each one of these cases and show that, in some subsets of logic, the only proofs and open derivations available in these systems are those that do not attempt to reprove tabled formulas. We illustrate these results with some examples, such as simulation, winning strategies, and let polymorphism typechecking.
We show that linear logic can be used as a general framework for encoding proof systems for minimal, intuitionistic, and classical logics. First, we demonstrate that with a single linear logic theory, one can faithfully account for natural deduction (normal and non-normal), sequent calculus (with and without cut), natural deduction with general elimination rules, free deduction and tableaux proof systems by using logical equivalences and different polarity assignments to meta-level literals. Then we exploit the fact that linear logic exponentials are not canonical and propose linear logic theories that faithfully encode different proof systems; for example, a multi-conclusion system for intuitionistic logic and several focusing proof systems.
The last contribution of this thesis investigates what type of algorithms can be expressed by using linear logic’s non-canonical exponentials. In particular, we use different exponentials to “locate” multisets of data, and then we show that focused proof search can be precisely linked to a simple algorithmic specification language that contains while-loops, conditionals, and insertion into and deletion from multisets. Finally, we illustrate this result with several graph algorithms, such as Dijkstra’s algorithm for finding the shortest distances in a positively weighted graph and an algorithm for checking if a graph is bipartite.
Lambda-Prolog Codes
Let-polymorphism typechecking – Example 3.38: [sig] [mod]
Bag Examples – Chapter 7: [sig] [mod]