Terminaison à base de tailles : sémantique et généralisations, Size-based termination : semantics and generalizations

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

D’autre part, toute contrefaçon, plagiat, reproduction
illicite encourt une poursuite pénale.


➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm Departement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
Terminaison a base de tailles:
Semantique et generalisations
THESE
presentee et soutenue publiquement le 20 Avril 2011
pour l’obtention du
Doctorat de l’universite Henri Poincare { Nancy 1
(specialite informatique)
par
Cody Roux
Composition du jury
Rapporteurs : Jurgen Giesl
Gilles Barthe
Examinateurs : Claude Kirchner (directeur)
Frederic Blanqui (co-encadrant)
Gilles Dowek
Andreas Abel
Adam Cichon
Laboratoire Lorrain de Recherche en Informatique et ses Applications | UMR 7503Mis en page avec la classe thloria.Remerciements
Le travail de these est un chemin long et parfois dicile, et mon chemin n’aurait pas pu se
faire sans l’aide precieuse des personnes qui m’ont entoure. D’abord celle de Frederic Blanqui,
dont l’impressionnante habilete technique et l’amour de la rigueur ont grandement contribue
a mes realisations techniques. Frederic s’est revele une source quasi-inepuisable d’observations
techniques et de contre-exemples subtils, et a su donner certaines idees importantes du coeur de
ce manuscrit. Vient ensuite celle de Claude Kirchner, dont le soutien moral s’est revele precieux,
ainsi que les conseils scientiques et \humains". Claude a su supporter mes explications parfois
confuses sur mon travail avec une patience in nie. Gilles Dowek a tres genereusement accepte
d’assister dans mon encadrement malgre son emploi du temps tres charge, et ses conseils en
Reecriture, en Logique, en Sciences et en Philosophie qui me serviront bien au-dela de mon
travail de these.
C’est Andreas Abel qui a le plus contribue, je pense, au peu que je comprend en theorie des
types, et je lui en suis tres reconnaissant. Il a eu la gentillesse de m’accueillir a deux reprises
a Munich pour des sejours qui ont de ni une partie de la direction de cette these. Colin Riba
n’arrive pas loin derriere, et j’admirerai toujours ses points de vue tres orginaux sur des sujets
classiques.
Je remercie Jurgen Giesl et Gilles Barthe d’avoir pris le temps et l’energie d’^etre rapporteurs
de mon manuscrit, et d’avoir donne leur point de vue subtil a mes modestes travaux. Je remercie
Adam Cichon d’avoir accepte de presider mon Jury.
Je remercie Makoto Hamana d’avoir pris le temps de donner des explications sur son travail
et pour les discussions importantes qui s’en suivirent.
Une these se produit dans un environnement particulier, et je remercie l’equipe Pareo (anci-
ennement Protheo) et en particulier Pierre-Etienne Moreau, de m’en avoir fourni un particuliere-
ment chaleureux. Je remercie mes co-bureaux, Paul, Clement et Claudia, de m’avoir permis de
travailler dans un cadre joyeux et stimulant. Je remercie les etudiants de l’universite de Ts-
inghua de leur accueil, particulierement Hehua et Dr. Lee. De m^eme je remercie les thesards de
l’equipe Marelle de Sophia-Antipolis, et en particulier Ioana pour son support.
Je remercie les membres de l’ARC Corias de m’avoir permis de me rendre a Paris et pour de
nombreuses discussions tres stimulantes, et Germain pour ses pouvoirs d’organisation. De m^eme
je remercie les membres du projet Mocca pour le travail interessant qui s’est deroule pendant ce
projet.
Je remercie l’equipe Proval de m’avoir accueilli avant d’avoir soutenu ma these et partic-
ulierement Guillaume Melquiond et Xavier Urbain pour m’avoir conseille pour ma presentation.
Je remercie mes parents, qui ont su me donner comprehension et soutien tout au long de ce
travail.
En n je remercie Camille, pour ^etre ce qu’elle est, et je lui dedicace ce travail.
iii\Why is it hard to imagine eternity?" demanded Natasha. \After today comes tomorrow, and
then the next day, and so on for ever; and there was yesterday, and the day before..."
| War and Peace, L. Tolstoy, 1869
iiiivSommaire
Quotation iii
Introduction 1
De nitions 7
1 Relations et termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Reecriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3 Le typage et le theoreme fondamental . . . . . . . . . . . . . . . . . . . . . . 13
Partie I Semantics for size-based termination
Chapter 1 A Type-Based Termination Criterion 23
1.1 The type system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
1.2 Decrease of recursive calls and the main theorem . . . . . . . . . . . . . . . . 30
Chapter 2 Higher Order Algebras 37
2.1 Categorical Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
2.2 Presheaf Algebras and Substitution Monoids . . . . . . . . . . . . . . . . . . 41
2.3 Premodels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
Chapter 3 Semantic Labelling 55
3.1 Labelling of Terms and Rewrite Systems . . . . . . . . . . . . . . . . . . . . 56
3.2 The Fundamental Lemma of Semantic Labelling . . . . . . . . . . . . . . . . 64
3.3 Normalization of the original system . . . . . . . . . . . . . . . . . . . . . . . 66
vSommaire
Chapter 4 The Realizability Algebra 69
4.1 The Realizability Space and the Rank function . . . . . . . . . . . . . . . . . 70
4.2 The Interpretation of Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.3 The Realizability Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
Chapter 5 Correctness of the Criterion 93
5.1 The Termination Criterion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5.2 Termination of the Labelled System . . . . . . . . . . . . . . . . . . . . . . . 97
5.3 Further applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
Chapter 6 Related work 107
Partie II A Type-Based Dependency Analysis
Chapter 1 Dependency Pairs 111
1.1 The Dependency Chain Criterion . . . . . . . . . . . . . . . . . . . . . . . . 112
1.2 Dependency Pair Processors and the Dependency Graph . . . . . . . . . . . 114
Chapter 2 The Type System and the Termination Criterion 121
2.1 The Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
2.2 Minimal Typing and the Dependency Graph . . . . . . . . . . . . . . . . . . 126
2.3 Erased Terms and the Main Theorem . . . . . . . . . . . . . . . . . . . . . . 128
Chapter 3 Correctness 133
3.1 The Type Interpretation and Conditional Correctness . . . . . . . . . . . . . 134
3.2 Higher Order Dependency Chains . . . . . . . . . . . . . . . . . . . . . . . . 140
3.3 Correctness of De ned Function Symbols . . . . . . . . . . . . . . . . . . . . 145
Chapter 4 Related work 149
vi