Computing with sequents: on the interpretation of sequent calculus as a calculus of lambda-terms and as a calculus of winning strategies
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
Résumé
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.
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.
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en « l'élimination des coupures ». Deux interprétations sont considérées.
Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.
La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.
Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.
Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.
Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.
La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.
Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.
Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.
Loading...