THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 Litp /
Litp research reports
127 pages - Novembre/November 1995 - French document.
PostScript : Ko /Kb
Titre / Title: Séquents qu'on calcule
De l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes
Abstract : In this thesis, we study the computational aspects of Gentzen's LJ and LK-like formal systems (these systems are commonly called "sequent calculi"). In these systems, the computational mechanism is cut-elimination. Two interpretations are considered.
Lambda-calculus is the framework of the first interpretation. We give a Curry-Howard-like correspondence between LJ and a syntactical variant of lambda-calculus. This variant includes an explicit "let _ in _" substitution operator. A confluent and strongly normalizing normalisation/cut-elimination procedure is given. The extension to LK is done by using the mu operator of Parigot's lambda-mu-calculus.
Game theory is the framework of the second interpretation: sequent calculi proofs are seen as winning strategies in two-players games (dialogues) about the validity of the proved formula. We give two results.
In a first place, we study the E-dialogues that Lorenzen has defined in order to investigate a game-theoretic foundation of provability. We show that if we consider the restrictions LJQ (resp LKQ) of LJ (resp LK), we get a bijection between the proofs of these systems and the intuitionistic (resp classical) E-dialogues. This result generalises and makes more precise a result of Felscher about the equivalence between the existence of a proof of A in LJ and the existence of a winning strategy for the first player in a E-dialogue about A.
In a second place, we study an infinitary propositional variable-free logic that Coquand used in describing a proof of terminating debate between proofs seen as winning strategies. We show an operational correspondence between this debate and the "weak head" cut-elimination. The "weak head" cut-elimination is independently proved terminating
Publications internes Litp 1995 / Litp research reports 1995