//img.uscri.be/pth/5c8c7136fcacbea1fbfca1504c95b32ae9df8b68
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage, Definitions by rewriting in the lambda-calculus : confluence, reducibility and typing

De
310 pages
Sous la direction de Claude Kirchner, Frédéric Blanqui
Thèse soutenue le 14 décembre 2007: INPL
Cette thèse concerne la combinaison du lambda-calcul et de la réécriture, dont nous étudions principalement deux propriétés : la confluence et la normalisation forte. Nous commençons par étudier sous quelles conditions la combinaison d'une relation de réécriture conditionnelle confluente au lambda-calcul donne une relation de réécriture confluente. Ensuite nous nous intéressons aux preuves de normalisation forte de lambda-calculs typés utilisant la technique de réductibilité. Notre contribution la plus importante est une comparaison de diverses variantes de cette technique, utilisant comme outil de comparaison la manière dont ces variantes s'étendent à la réécriture et dont elles prennent en compte les types unions et les types existentiels implicites. Enfin, nous présentons un critère, basé sur un système de types contraints, pour la normalisation forte de la réécriture conditionnelle combinée au lambda-calcul. Notre approche étend des critères de terminaison existants qui utilisent des annotations de taille. C'est à notre connaissance le premier critère de terminaison pour la réécriture conditionnelle avec membres droits d'ordre supérieur qui prenne en compte, dans l'argument de terminaison, de l'information issue de la satisfaction des conditions des règles de réécriture
-Lambda-calcul
-Réécriture
-Réécriture conditionnelle
-Confluence
-Typage
-Types union
-Normalisation forte
-Candidats de réductibilité
-Ensembles saturés
-Biorthogonalité
-Réécriture
This thesis is about the combination of lambda-calculus with rewriting. We mainly study two properties: confluence and strong normalization. We begin by studying under which conditions the combination of a confluent conditional rewrite relation to the lambda-calculus leads to a confluent relation. Next, we study strong normalization proofs of typed lambda-calculi that use the reducibility technique. Our main contribution is a comparison of variants of this technique, with respect to how they extend to rewriting and how they handle union and implicit existential types. Finally, we present a termination criterion for the combination of conditional rewriting and lambda-calculus based on a constrained type system. Our approach, which extends known criteria that use sized types, is to our knowledge the first termination criterion for conditional rewriting with higher-order right-hand sides that takes into account in the termination argument some information generated by the satisfaction of the conditions of the rewrite rules
-Lambda-calculus
-Saturated sets
-Biorthogonality
-Reducibility candidates
-Rewriting
-Conditional rewriting
-Typing
-Union types
-Strong normalization
Source: http://www.theses.fr/2007INPL102N/document
Voir plus Voir moins


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 au même titre que sa
version papier. 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 entraîne une
poursuite pénale.

Contact SCD INPL : scdinpl@inpl-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
D´epartement de formation doctorale en informatique
´Ecole doctorale IAEM Lorraine
D´efinitions par r´e´ecriture dans le
lambda-calcul :
confluence, r´eductibilit´e et typage
`THESE
pr´esent´ee et soutenue publiquement le 14 d´ecembre 2007
pour l’obtention du
Doctorat de l’Institut National Polytechnique de Lorraine
(sp´ecialit´e informatique)
par
Colin Riba
Composition du jury
Pr´esident : Gilles Barthe Directeur de recherche, INRIA, Sophia-Antipolis, France
Rapporteurs : Thierry Coquand Professeur, Chalmers University, Got¨ eborg, Su`ede
Delia Kesner Professeur, Universit´e Paris 7, Paris, France
Examinateurs : Mariangiola Dezani Professeur, Universit`a di Torino, Italie
´Jean-Yves Marion Professeur, Ecole des Mines de Nancy, INPL, Nancy, France
Fr´ed´eric Blanqui (dir.) Charg´e de recherche, INRIA, Nancy, France
Claude Kirchner (dir.) Directeur de recherche, INRIA, Nancy, France
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Mis en page avec la classe scrbook.It is more important that a proposition be interesting than that it be true.
Alfred North Whitehead
Adventures of Ideas
Permettez-moi de vous répéter ce que je vous disais ici : traiter la nature par le cylindre, la
sphère, le cône, le tout mis en perspective... et les lignes parallèles à l’horizon donnent
l’étendue, soit une réaction à la nature. Les lignes perpendiculaires à cet horizon donnent de
la profondeur. Car la nature, pour nous les hommes, est plus en profondeur qu’en surface.
Lettre de Georges Braque à Émile Bernard4Remerciements
Je tiens tout d’abord à remercier Frédéric Blanqui et Claude Kirchner pour m’avoir
accueilli à Nancy et m’avoir patiemment guidé pendant ces trois années. En particulier
Frédéric pour son soutient sans failles, son engagement et la qualité de son encadrement;
Claude pour l’environnement de travail excellent qu’il a su créer au sein de l’équipe Pro-
theo et l’attention qu’il a toujours porté à mon travail malgré ses multiples occupations.
Je remercie Thierry Coquand et Delia Kesner, qui on eu la gentillesse de bien vouloir
rapporter cette thèse. Delia Kesner pour les discussions enrichissantes que l’on a pu avoir
ainsi que pour l’intérêt qu’elle a manifesté pour mon travail.
Je tiens aussi a remercier les membres de mon jury, tout d’abord pour avoir accepté
d’en faire partie. Mariangiola Dezani pour la gentillesse dont elle fait preuve a mon égard
ainsi que pour l’intérêt des discussions que nous avons pu avoir; Jean-Yves Marion pour
quelquesdiscussionsintéressantesetludiques;etGillesBarthe,ainsiqueleprojetEverest
à Sophia-Antipolis pour m’avoir accueilli dès avant ma soutenance.
Cette thèse doit énormément aux univers scientifiques dans lesquels elle s’insère, et
dont je ne peux énumérer les membres. Mais je me dois de remercier Alexandre Miquel
pour m’avoir introduit aux biorthogonaux pendant l’école d’été Types 2005. Le chapitre
10 de cette thèse doit énormément à cette rencontre. De manière plus brève mais tout
aussi déterminante, ce chapitre doit beaucoup à l’exemple que m’a communiqué Philippe
de Groote. Je tiens aussi à remercier Andreas Abel pour les nombreux échanges que nous
avons eu et les remarques pertinentes qu’il a pu faire sur mon travail.
Je remercie les membres de l’équipe PPS de m’avoir offert un espace appréciable pour
présentermestravaux,enparticulierDeliaKesner,AlexandreMiqueletPaul-AndréMel-
liès. J’ai aussi eu le plaisir d’avoir été longuement cuisiné par les membres de l’équipe
Plume du LIP, en particulier par Daniel Hirschkoff, ainsi que par leurs comparses de
l’équipedelogiqueduLAMA,RenéDavidetChristopheRaffalli.Merciaussiaumembres
du projet LogiCal, en particulier Gilles Dowek pour quelques discussions aux cours des-
quelles j’ai essayé de m’imprégner de sa clarté de pensée, et Jean-Pierre Jouannaud pour
l’interêt qu’il a porté à mes travaux. Je voudrais enfin remercier Rachid Echahed pour
avoir guidé mes premiers pas en recherche, ainsi que pour le temps qu’il m’a offert pour
présenter mes travaux à l’équipe CAPP du LIG.
Merci aux membres et thésards de l’équipe Protheo, en particulier Germain pour sa
patience lors de discussions presqu’interminables et pour sa curiosité scientifique com-
municative; ainsi qu’Antoine, dont le pragmatisme éclairé a souvent dénoué quelques
problèmes métaphysiques. Merci aussi à mes anciens co-bureaux Guillaume, Oana et
Anderson pour leur compagnie et pour m’avoir supporté. Merci à Yves pour son éclai-
ragenouveau,dontj’espèrepouvoirtirerpartiunjour,ainsiquepoursadisponibilitélors
de la préparation de ma soutenance. Merci enfin à Richard pour son accueil chaleureux
5à Nancy, sans lequel la soutenance n’aurait pu avoir lieu.
Je suis très heureux d’avoir pu effectuer ma thèse dans un environnement aussi riche
et varié que le Loria. Certaines personnes y ont très agréablement enrichi mes trois
années passées à Nancy, tout particulièrement Sébastien, Heinrich, mais aussi Romain et
Benjamin,ainsiquebeaucoupd’autres.Quelquesconnaissancesnancéenes,enparticulier
Said, et mes anciens colocataires, dont Fabien.
Enfin ma famille, dont j’ai la chance d’avoir toujours eu le soutient inconditionnel et
à qui cette thèse doit énormément. Je ne peux conclure sans remercier Olivier dont la
patience, la curiosité et l’exigence lors de mes tentatives pour lui expliquer mon travail
ont sûrement beaucoup contribué, bien qu’indirectement, à cette thèse. Une mention
spéciale va à Mary Carmen.
6Table des matières
Introduction 11
Notations et notions de base 19
I Réécriture conditionnelle et lambda-calcul 25
1 Structures de termes 27
1.1 Termes du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1.2 Termes du lambda-calcul et alpha-conversion . . . . . . . . . . . . . . . . 35
1.3 Substitution sans capture . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1.4 Termes du premier ordre parmi les lambda-termes . . . . . . . . . . . . . 44
1.5 Convention de Barendregt locale . . . . . . . . . . . . . . . . . . . . . . . 46
1.6 Termes de de Bruijn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2 Réductions 51
2.1 Systèmes de réduction abstraits . . . . . . . . . . . . . . . . . . . . . . . . 51
2.2 Relations de réécriture et congruences . . . . . . . . . . . . . . . . . . . . 55
2.3 Réduction parallèle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
2.4 Systèmes de réécriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3 Réécriture et lambda-calcul 61
3.1 Réécriture au premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.2 Lambda-calcul non typé . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.3 Lambda-calcul typé . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.3.1 Lambda-calcul pur simplement typé . . . . . . . . . . . . . . . . . 69
3.3.2 Système F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
3.3.2.(a) Types du second ordre . . . . . . . . . . . . . . . . . . . . 70
3.3.2.(b) Système F implicite . . . . . . . . . . . . . . . . . . . . . 72
3.3.2.(c) F explicite . . . . . . . . . . . . . . . . . . . . . 73
3.3.2.(d) Propriétés . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.3.3 Lambda-calculs avec abstractions à la Church . . . . . . . . . . . . 74
3.4 Types de données dans le système F . . . . . . . . . . . . . . . . . . . . . 75
3.4.1 Booléens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.4.2 Paires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.4.3 Entiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.4.4 Vers une extension du lambda-calcul . . . . . . . . . . . . . . . . . 77
7Table des matières
3.4.4.(a) Paires surjectives . . . . . . . . . . . . . . . . . . . . . . . 77
3.4.4.(b) Schéma de récursion . . . . . . . . . . . . . . . . . . . . . 78
3.5 Extensionnalité et théorème de Böhm . . . . . . . . . . . . . . . . . . . . 78
3.6 Réécriture dans le lambda-calcul typé . . . . . . . . . . . . . . . . . . . . 79
3.7 Exemples de combinaisons . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
3.7.1 Lambda-calcul avec produits finis . . . . . . . . . . . . . . . . . . . 82
3.7.2 Système T de Gödel . . . . . . . . . . . . . . . . . . . . . . . . . . 83
3.7.3 Des co-produits à la réécriture d’ordre supérieur . . . . . . . . . . 84
4 Réécriture conditionnelle 87
4.1 Définitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.2 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.2.1 Un système de manipulation de termes . . . . . . . . . . . . . . . . 91
4.2.2 Règles conditionnelles de de Vrijer . . . . . . . . . . . . . . . . . . 92
4.3 Quotient de la réécriture conditionnelle par alpha-conversion . . . . . . . . 92
II Confluence 97
5 Outils pour la confluence 99
5.1 Systèmes orthogonaux et réécriture parallèle . . . . . . . . . . . . . . . . . 99
5.1.1 Systèmes de réécriture de termes . . . . . . . . . . . . . . . . . . . 99
5.1.2 Lambda-calcul . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.2 Confluence de la réécriture conditionnelle . . . . . . . . . . . . . . . . . . 102
5.2.1 Réécriture conditionnelle orthogonale . . . . . . . . . . . . . . . . . 103
5.2.2 Confluence par niveaux et confluence . . . . . . . . . . . . . . . . . 105
5.3 Modularité et extension de la signature . . . . . . . . . . . . . . . . . . . . 106
5.3.1 Systèmes du premier ordre . . . . . . . . . . . . . . . . . . . . . . . 106
5.3.2 Lambda termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.3.3 Une caractérisation de la confluence . . . . . . . . . . . . . . . . . 108
5.3.4 Combinaisons non disjointes et termes infinis . . . . . . . . . . . . 108
6 Réécriture combinée au lambda-calcul 111
6.1 Confluence de la réécriture et du lambda-calcul . . . . . . . . . . . . . . . 111
6.1.1 Combinaisons non typées . . . . . . . . . . . . . . . . . . . . . . . 112
6.1.2 Combinaisons typées . . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.1.3 Importance de l’arité . . . . . . . . . . . . . . . . . . . . . . . . . . 115
6.2 Consistance de la réécriture algébrique extensionnelle . . . . . . . . . . . . 116
6.2.1 Confluence de la réécriture avec l’éta-expansion typée . . . . . . . 117
6.2.2 Consistance de la réécriture avec éta-conversion . . . . . . . . . . . 117
7 Réécriture conditionnelle combinée au lambda-calcul 119
7.1 Confluence de la béta-réduction avec la réécriture conditionnelle . . . . . . 119
7.1.1 Systèmes linéaires à gauche et semi-clos . . . . . . . . . . . . . . . 120
8Table des matières
7.1.2 Confluence sur les termes faiblement normalisants . . . . . . . . . 122
7.2 Confluence avec béta-réduction dans les conditions . . . . . . . . . . . . . 129
7.2.1 Systèmes linéaires à gauche et semi-clos . . . . . . . . . . . . . . . 130
7.2.2 Confluence sur les termes faiblement normalisants . . . . . . . . . 137
7.2.3 Systèmes orthonormaux . . . . . . . . . . . . . . . . . . . . . . . . 139
8 Préservation de la confluence par curryfication 145
8.1 Curryfication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
8.2 Un essai de preuve directe . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
8.3 Paramétrisation partielle d’un système de réécriture . . . . . . . . . . . . 148
8.3.1 Paramétrisation partielle . . . . . . . . . . . . . . . . . . . . . . . . 148
8.3.2 Propriétés de la curryfication . . . . . . . . . . . . . . . . . . . . . 150
8.3.3 Propriétés de la décurryfication . . . . . . . . . . . . . . . . . . . . 150
8.4 Préservation de la confluence . . . . . . . . . . . . . . . . . . . . . . . . . 152
III Normalisation forte et réductibilité 157
9 Normalisation forte dans le lambda-calcul typé 159
9.1 Lambda-calculs avec types simples . . . . . . . . . . . . . . . . . . . . . . 160
9.1.1 Lambda-calcul avec produits . . . . . . . . . . . . . . . . . . . . . 161
9.1.2 Normalisation forte du lambda-calcul simplement typé . . . . . . . 163
9.1.3lisation forte du lambl avec produits . . . . . . . . . 167
9.1.4 Lambda-calcul avec réécriture . . . . . . . . . . . . . . . . . . . . . 171
9.2 Système F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174
9.2.1 Quantification du second ordre et produits infinis . . . . . . . . . . 174
9.2.2 Interprétation du polymorphisme . . . . . . . . . . . . . . . . . . . 178
9.3 Familles de réductibilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
9.3.1 Opérateurs de clôture . . . . . . . . . . . . . . . . . . . . . . . . . 182
9.3.2 Ensembles saturés . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
9.3.3 Ensembles saturés et réécriture . . . . . . . . . . . . . . . . . . . . 185
9.3.4 Candidats de réductibilité . . . . . . . . . . . . . . . . . . . . . . . 187
9.3.5 Biorthogonaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194
9.4 Réécriture du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . 198
10 Unions de familles de réductibilité 201
10.1 Réécriture simple avec types union et intersection . . . . . . . . . . . . . . 202
10.2 Adéquation et complétude pour la normalisation forte . . . . . . . . . . . 205
10.2.1 Adéquation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206
10.2.2 Complétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
10.3 Élimination de l’union et normalisation forte. . . . . . . . . . . . . . . . . 212
10.4 Stabilité par union de familles de réductibilité . . . . . . . . . . . . . . . . 217
10.4.1 Ensembles saturés . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
10.4.2 Candidats de réductibilité . . . . . . . . . . . . . . . . . . . . . . . 218
9