14/03/2002: Claude Kirchner (LORIA et INRIA)
Le calcul de réécriture.
Résumé
La notion usuelle de règle de réécriture donne lieu à plusieurs
concepts.
-- la relation de réécriture, plus particulièrement étudiée depuis les
années 70, et ayant souvent servi à opérationaliser la logique
équationelle.
-- la logique de réécriture, explicitée par José Meseguer au début des
années 90, généralise la logique équationelle en supprimant la
symétrie de l'égalité,
-- plus récemment nous avons introduit avec Horatiu Cirstea le calcul
de réécriture qui permet de comprendre la flèche de réécriture comme
une abstraction dont l'application explicite à un terme produit un
ensemble de résultats. Ce calcul généralise le lambda calcul et offre
par son mécanisme de passage de paramètre controlé par filtrage un
outil puissant de modélisation et de preuve.
Nous motiverons puis présenterons le calcul de réécriture et ses
propriétés. Nous montrerons également comment l'opérateur
d'abstraction introduit permet de définir des systèmes de types
généralisant ceux du lambda-cube. Enfin le système ELAN de
programmation par règle et stratégie qui implante partiellement le
calcul de réécriture sera brièvement présenté.