Skip to Main content Skip to Navigation
Conference papers

The graph rewriting calculus: confluence and expressiveness

Clara Bertolissi 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) is a simple calculus that uniformly integrates term-rewriting and lambda-calculus. The Rhog has been recently introduced as an extension of the rho-calculus, handling structures with cycles and sharing. The calculus over terms is naturally generalized by using unification constraints in addition to the standard rho-calculus matching constraints. This leads to a term-graph representation in an equational style where terms consist of unordered lists of equations. In this paper we show that the (linear) Rhog is confluent. The proof of this result is quite elaborated, due to the non-termination of the system and to the fact that we work on equivalence classes of terms. We also show that the Rhog can be seen as a generalization of first-order term-graph rewriting, in the sense that for any term-graph rewrite step a corresponding sequence of rewritings can be found in the Rhog.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Clara Bertolissi Connect in order to contact the contributor
Submitted on : Tuesday, November 15, 2005 - 4:25:44 PM
Last modification on : Friday, February 4, 2022 - 3:29:54 AM
Long-term archiving on: : Tuesday, September 11, 2012 - 12:50:43 PM



  • HAL Id : inria-00000744, version 1



Clara Bertolissi. The graph rewriting calculus: confluence and expressiveness. 9th Italian Conference on Theoretical Computer Science, ICTCS 2005, Oct 2005, Italie, pp.113 - 127. ⟨inria-00000744⟩



Record views


Files downloads