tel-00529021, version 1

Preuves constructives de complétude et contrôle délimité

Danko Ilik () ^1, 2, 3

Ecole Polytechnique X (22/10/2010), Hugo Herbelin (Dir.)

• 1 :  Laboratoire d'informatique de l'école polytechnique (LIX)
• http://www.lix.polytechnique.fr/
  CNRS : UMR7161 – Polytechnique - X Route de Saclay 91128 PALAISEAU CEDEX France
• 2 :  PI.R2 (INRIA Paris - Rocquencourt)
• 
  INRIA – Université Paris VII - Paris Diderot – CNRS : UMR7126 France
• 3 :  Preuves, Programmes et Systèmes (PPS)
• http://www.pps.jussieu.fr
  CNRS : UMR7126 – Université Paris VII - Paris Diderot Université Denis Diderot 2 Place Jussieu - case 7014 75005 PARIS France

Références bibliographiques

• Type de publication : Thèses
• titre : Preuves constructives de complétude et contrôle délimité
• titre en anglais : Constructive Completeness Proofs and Delimited Control
• date de soutenance : 22/10/2010
• résumé : Motivés par la facilitation du raisonnement sur des méta-théories logiques à l'intérieur de l'assistant de preuve Coq, nous étudions les versions constructives de certains théorèmes de complétude. Nous commençons par l'analyse des preuves de Krivine et Berardi-Valentini qui énoncent que la logique classique est constructivement complète au regard des modèles booléens relaxés, ainsi que l'analyse de l'algorithme de cette preuve. En essayant d'élaborer une preuve de complétude plus canonique pour la logique classique, inspirés par la méthode de la normalisation-par-évaluation (NPE) de Berger et Schwichtenberg, nous concevons une preuve de complétude pour la logique classique en introduisant une notion de modèle dans le style des modèles de Kripke, dont le contenu calculatoire est l'élimination des coupures, ou la normalisation. Nous nous tournons ensuite vers la NPE pour une logique de prédicats intuitionniste (en considérant tous les connecteurs logiques), c'est-à-dire, vers sa complétude par rapport aux modèles de Kripke. Inspirés par le programme informatique de Danvy pour la normalisation des termes du $\lambda$-calcul avec sommes, lequel utilise des opérateurs de contrôle délimité, nous développons une notion d'un modèle, encore une fois semblable aux modèles de Kripke, qui est correct et complet pour la logique de prédicats intuitionniste, et qui est, par coïncidence, très similaire à la notion de modèle de Kripke introduit pour la logique classique. Finalement, en se fondant sur des observations de Herbelin, nous montrons que l'on peut avoir une logique intuitionniste étendue avec des opérateurs de contrôle délimité qui est equiconsistante avec la logique intuitionniste, qui préserve les propriétés de disjonction et d'existence, et qui est capable de dériver le schéma « Double Negation Shift » et le principe de Markov.
• résumé en anglais : Motivated by facilitating reasoning with logical meta-theory inside the Coq proof assistant, we investigate the constructive versions of some completeness theorems. We start by analysing the proofs of Krivine and Berardi-Valentini, that classical logic is constructively complete with respect to (relaxed) Boolean models, and the algorithm behind the proof. In an effort to make a more canonical proof of completeness for classical logic, inspired by the normalisation-by-evaluation (NBE) methodology of Berger and Schwichtenberg, we design a completeness proof for classical logic by introducing a notion of model in the style of Kripke models. We then turn our attention to NBE for full intuitionistic predicate logic, that is, to its completeness with respect to Kripke models. Inspired by the computer program of Danvy for normalising terms of $\lambda$-calculus with sums, which makes use of delimited control operators, we develop a notion of model, again similar to Kripke models, which is sound and complete for full intuitionistic predicate logic, and is coincidentally very similar to the notion of Kripke-style model introduced for classical logic. Finally, based on observations of Herbelin, we show that one can have an intuitionistic logic extended with delimited control operators which is equi-consistent with intuitionistic logic, preserves the disjunction and existence properties, and is able to derive the Double Negation Shift schema and Markov's Principle.
• domaine :

  Informatique/Génie logiciel

  Mathématiques

• organisme de délivrance : Ecole Polytechnique X
• langue : Anglais
• directeur de thèse : Hugo Herbelin
• composition du Jury : Hugo Herbelin (directeur)
  Ulrich Berger (rapporteur)
  Thierry Coquand (rapporteur)
  Olivier Danvy (rapporteur)
  Gilles Dowek (examinateur)
  Paul-André Melliès (examinateur)
  Alexandre Miquel (examinateur)
  Wim Veldman (examinateur)
• mots-clés : preuves de complétude – normalisation par évaluation – opérateurs de contrôle délimites
• mots-clés en anglais : completeness proofs, normalization by evaluation, delimited control operators

Liste des fichiers attachés à ce document :

• tel-00529021, version 1
• http://tel.archives-ouvertes.fr/tel-00529021
• oai:tel.archives-ouvertes.fr:tel-00529021
• Contributeur : Danko Ilik <>
• Soumis le : Dimanche 24 Octobre 2010, 08:32:42
• Dernière modification le : Lundi 25 Octobre 2010, 08:36:37