Le calcul de réécriture de graphes : propriétés et capacités d'expression

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 rewriting calculus, with special interest for higher-order rewriting and the possibility of dealing with graph-like structures. The first part of the thesis is dedicated to the relationship between the rewriting calculus and 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 then an 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, under some linearity restrictions on patterns, and expressive enough to simulate first-order term graph rewriting and cyclic lambda-calculusCes dernières années, on a assisté au développement du calcul de réécriture, encore appelé rho-calcul, qui intègre de faç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 original pour les CRSs qui utilise une traduction des termes CRS en lambda-termes et le filtrage d'ordre supérieur classique du lambda-calcul. Nous proposons ensuite un encodage des CRSs dans le rho-calcul basé sur la traduction de chaque réduction CRS en 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 classes d'équivalence de termes, sous certaines restrictions de linéarité sur les motifs, et assez expressif pour simuler la réécriture de termes graphes et le lambda-calcul cycliqu