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
Hugo Herbelin · HAL (Le Centre pour la Communication Scientifique Directe) · 1995
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.