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

Colin Riba

Description

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

Sujets

• Lambda-calcul
• Réécriture
• Confluence
• Type (informatique)

Informations

• Publié par: Thesee
• Nombre de lectures: 106
• Langue: Français
• Poids de l'ouvrage: 2 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 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 : [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
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