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

Cody Roux

Description

Sous la direction de Claude Kirchner
Thèse soutenue le 14 juin 2011: Nancy 1
Ce manuscrit présente une réflexion sur la terminaison des systèmes de réécriture d'ordres supérieurs. Nous nous concentrons sur une méthode particulière, la terminaison à base de tailles. La terminaison à base de tailles utilise le typage pourdonner une approximation syntaxique à la taille d'un élément du langage. Notre contribution est double: premièrement, nous permettons d'aborder de manière structurée le problème de la correction des approches à base de taille. Pour ce faire, nous montrons qu'elle peut être traitée par une version de la méthode des annotations sémantiques. Cette dernière utilise des annotations sur les termescalculés à partir de la sémantique des sous-termes dans un certain prémodèle équationnel. Nous montrons la correction de notre approche par annotations sémantiques, ainsi que du critère qui permet de traiter le système annoté, et nous construisons un prémodèle pour le système qui correspond intuitivement à lasémantique du système de réécriture. Nous montrons alors que le système annoté passe le critère de terminaison. D'un autre côté nous modifions l'approche classique de la terminaison à base de tailles et montrons que le système modifiépermet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approxime, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit à montrer la terminaison de tout terme bien typé
-Réécriture
-Ordre supérieur
-Typage
-Normalisation
-Tailles
-Annotations sémantiques
-Prémodèle
-Paires de dépendance
The present manuscript is a reflection on termination of higher-order rewrite systems. We concentrate our efforts on a particular approach, size-based termination. This method uses typing to give a syntactic approximation to the size of an element of the language. Our contribution is twofold: first we give a structured approach to proving the correctness of size-based termination. To do this, we show that it is possible to apply a certain version of semantic labelling. This technique uses annotations on terms computed using the semantics of subterms in a certain equational premodel. We show correctness of our labelling framework and of the criterion that allows us to prove termination of the labelled system, and we build a premodel of the rewrite system that intuitively corresponds to the rewrite system. We show that the system labelled using these semantics passes the termination criterion. Furthermore we show that a modification of the classical size-types approach allows us to perform a fine control-flow analysis in a higher-order language. This allows us to build an approximated dependency graph, and show that if a certain syntactic criterion issatisfied by the graph, then all well-typed terms are terminating
Source: http://www.theses.fr/2011NAN10034/document

Sujets

• Réécriture
• Type (informatique)
• Normalisation
• Tailles

Informations

• Publié par: Thesee
• Nombre de lectures: 20
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

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 : [e-mail]




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