Cours de Réécriture
Présentation
La théorie de la réécriture
est une produit dérivé de la
théorie de la démonstration,
la tentative de comprendre les propriétés
dynamiques du calcul, au-delà
des cas particuliers de l'élimination des coupures
en calcul des séquents, ou de la beta-réduction
en lambda-calcul.
Nous exposerons quelques modèles de réécriture:
lambda-calcul, calcul des séquents,
réseaux d'interaction, réseaux de Petri,
calculs de processus concurrents.
Puis, nous étudierons ces différents calculs
du point de vue diagrammatique, en nous concentrant sur
les propriétés de confluence, standardisation,
factorisation. Cela nous amèra au point central du cours:
le rapport entre systèmes de réécriture
et structures d'évènement.
Notes de cours
Les
notes de cours sont encore en cours de rédaction...
Examen
Examen 2001-2002
Edimbourg 1998
Page du
cours de réécriture donné à
l'université d'Edimbourg en 1998.
Bibliographie
Jan Willem Klop
Term Rewriting Systems.
Handbook of Logic in Computer Science, volume 2.
S. Abramsky, Dov M. Gabbay, T.S.E. Maibaum eds
Oxford Science Publications
1992.
Barnaby Hilken
Towards a proof theory of rewriting: the simply typed 2-lambda-calculus.
Theoretical Computer Science 170, pp 407-444.
1996.
Paul-André Melliès
Axiomatic Rewriting Theory I
A diagrammatic standardization theorem.
2001.
Paul-André Melliès
Axiomatic Rewriting Theory III
A factorization theorem in rewriting theory
Proceedings of the 7th Conference on Category Theory
and Computer Science.
Lecture Notes in Computer Science 1290, pp. 49-68.
Springer, 1997.
The happy fews
Jérome Creci ---
jeromecreci@yahoo.fr
Antonin Guilloux ---
aguillou@clipper.ens.fr
Edouard Maurel-Segala ---
emaurel@clipper.ens.fr
Matthieu Objois ---
matthieuobjois@minitel.net
Jérome Rocheteau ---
rocheteau.jerome@libertysurf.fr
Alexis Saurin ---
saurin@clipper.ens.fr
Projets de stage de DEA.
Projet 1.
Généralisation de la théorie axiomatique.
Dans un article ``Towards a proof-theory of rewriting:
the simply-typed 2-lambda-calculus'', Barnaby Hilken
caractérise les formes normales beta-eta-longues du lambda-calcul
de manière élégante:
ce sont les lambda-termes P tels que tout chemin
de beta-eta réduction P-->Q est accompagné
d'un chemin de réduction Q-->P tel que P-->Q-->P
soit l'identité.
La théorie de B. Hilken ne rentre pas dans le cadre axiomatique
de la réécriture que j'ai défini
dans une série d'articles (ART I, II, III et IV).
Le sujet du stage sera d'analyser la construction de B. Hilken,
en vue d'une généralisation ultérieure
de la théorie axiomatique.
Projet 2.
Lambda calcul avec substitutions explicites.
Dans tout système de réécriture axiomatique,
il est possible de caractériser catégoriquement
la notion de ``réductions de tete'' --- voir ART IV.
En fait, on démontre qu'à partir
de tout terme P, il existe un cone de telles
réductions h:P-->V qui transforment P
en une forme normale de tete V.
Dans le lambda-calcul, ce cone ne contient qu'une réduction au plus,
qu'on appelle la réduction de tete.
Mais en général, dans un système
de réécriture non d&'eterministe,
le cone contient plusieurs réductions incompatibles.
Dans le cas du lambda sigma calcul, un lambda calcul
avec substitutions explicites, il est possible de montrer
que toutes les réductions du cone à partir
d'un lambda-sigma terme P se projettent
par interprétation sur la réduction
de tete (unique) du lambda-calcul.
La démonstration donnée en ART II est syntaxique.
Le sujet du stage sera d'en trouver une présentation abstraite.
Liens utiles
Bruno Guillaume
Emmanuel Polonovski
|