The graph rewriting calculus: properties and expressive capabilities

Thèse en cotutelle entre le INRIA/LORIA (France) et l'Universita degli Studi di Udine (Italie). Directeurs de thèse: Claude Kirchner (INRIA) et Furio Honsell (UDINE).The last few years have seen the development of the rewriting calculus (also called rho-calculus) that uniformly integrates first-order term rewriting and lambda-calculus.This thesis is devoted to the study of the expressiveness of the rewritingcalculus, with special interest for higher-order rewritingand the possibility of dealing with graph-like structures.The first part of the thesis is dedicated to the relationship between the rewriting calculusand higher-order term rewriting, namely the Combinatory Reduction Systems (CRSs).First, an original matching algorithm for CRSs terms that uses a simple term translation and the classical higher-order pattern matching of lambda terms is proposed and thenan encoding of CRSs in the rho-calculus based on a translation of each possible CRS-reduction into a corresponding rho-reduction is presented.The second part of the thesis is devoted to an extension of the rho-calculus,called graph rewriting calculus (or Rg-calculus), handling terms with sharing and cycles.The calculus over terms is naturally generalised by using unification constraints in addition to standard rho-calculus matching constraints.The Rg-calculus is shown to be confluent over equivalence classes of terms, undersome linearity restrictions on patterns, and expressive enough to simulatefirst-order term graph rewriting and cyclic lambda-calculus.Ces dernières années, on a assisté au développement ducalcul de réécriture, encore appelé rho-calcul, qui intègre defaçon uniforme la réécriture de premier ordre et le lambda-calcul.Cette thèse est dédiée à l'étude des capacités d'expression du calcul de réécriture, avec un intérêt particulier pour la réécriture d'ordre supérieur et la possibilité de manipuler des graphes.Dans la première partie de cette thèse, la relation entre le calcul de réécriture et la réécriture d'ordre supérieur, en particulier les Combinatory Reduction Systems (CRSs), est étudiée.Nous présentons d'abord un algorithme de filtrage originalpour les CRSs qui utilise une traduction des termes CRS enlambda-termes et le filtrage d'ordre supérieur classique du lambda-calcul. Nous proposons ensuite un encodage des CRSs dans le rho-calculbasé sur la traduction de chaque réduction CRSen une réduction correspondante dans le rho-calcul.Dans la deuxième partie, nous présentons une extension du rho-calcul,appelé calcul de réécriture de graphes (ou Rg-calcul),qui gère des termes avec partage et cycles.Le calcul sur les termes est généralisé de manière naturelle en utilisant des contraintes d'unification en plus des contraintes de filtrage standard du rho-calcul.Le Rg-calcul est alors montré confluent sur des classesd'équivalence de termes, sous certaines restrictions de linéarité sur les motifs, et assezexpressif pour simuler la réécriture de termes graphes et lelambda-calcul cyclique