Thèse de doctorat de David Baelde
A linear approach to the proof-theory of
least and greatest fixed points
Sous la direction de Dale Miller.
Manuscrit (en anglais): version de la soutenance (PDF).
Jury
- Patrick Baillot (Rapporteur)
- Gilles Dowek
- Olivier Laurent
- Paul-André Melliès
- Dale Miller (Directeur de thèse)
- Gopalan Nadathur
- Christine Paulin-Mohring (Rapporteur)
- Frank Pfenning (Rapporteur)
Résumé
Les constructions de plus petit et plus grand point fixe sont associées aux concepts de définition inductive et coinductive et au raisonnement par induction et coinduction. Nous étudions la théorie de la démonstration de ces concepts, dans le cadre épuré de la logique linéaire, où la dualité entre plus petit et plus grand point fixe s'exprime complètement. Les constructions par point fixe ont l'avantage d'engendrer des infinis structurés, même canoniques. Leur structure, reflétée en logique, permet de dériver certaines propriétés : on retrouve notamment les règles non-linéaires pour certaines formules ; on dérive de façon similaire des propriétés structurelles de la quantification (nabla) générique, reformulée pour bien interagir avec les points fixes. Le coeur de la thèse est l'extension de la notion de focalisation aux points fixes. La focalisation est une propriété fondamentale de la structure des preuves, utilisée aussi bien en recherche de preuve qu'en sémantique des jeux. Nous montrons que ce résultat de focalisation s'étend naturellement dans un cadre intuitionniste, ce qui donne lieu à des applications en démonstration automatique.