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

https://hal.inria.fr/inria-00000744
Contributor : Clara Bertolissi <>
Submitted on : Tuesday, November 15, 2005 - 4:25:44 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Tuesday, September 11, 2012 - 12:50:43 PM

Files

Identifiers

  • HAL Id : inria-00000744, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

258

Files downloads

187