HAL - INRIA :: [inria-00000744, version 1] The graph rewriting calculus: confluence and expressiveness

inria-00000744, version 1

%% inria-00000744, version 1
%% http://hal.inria.fr/inria-00000744/en/
@inproceedings{BERTOLISSI:2005:INRIA-00000744:1,
	title = { {T}he graph rewriting calculus: confluence and expressiveness},
	author = {{B}ertolissi, {C}lara},
	abstract = {{I}ntroduced at the end of the nineties, the {R}ewriting {C}alculus (rho-calculus, for short) is a simple calculus that uniformly integrates term-rewriting and lambda-calculus. {T}he {R}hog has been recently introduced as an extension of the rho-calculus, handling structures with cycles and sharing. {T}he calculus over terms is naturally generalized by using unification constraints in addition to the standard rho-calculus matching constraints. {T}his leads to a term-graph representation in an equational style where terms consist of unordered lists of equations. {I}n this paper we show that the (linear) {R}hog is confluent. {T}he 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. {W}e also show that the {R}hog 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 {R}hog.},
	keywords = {term graph rewriting; matching; cyclic lambda calculus},
	language = {{E}nglish},
	affiliation = {{PROTHEO} - {INRIA} {L}orraine - {LORIA} - {INRIA} - {CNRS} : {UMR}7503 - {U}niversit{\'e} {H}enri {P}oincar{\'e} - {N}ancy {I} - {U}niversit{\'e} {N}ancy {II} - {I}nstitut {N}ational {P}olytechnique de {L}orraine },
	booktitle = {9th {I}talian {C}onference on {T}heoretical {C}omputer {S}cience, {ICTCS} 2005 {T}heoretical {C}omputer {S}cience: 9th {I}talian {C}onference, {ICTCS} 2005, {S}iena, {I}taly, {O}ctober 12-14, 2005. {P}roceedings },
	publisher = {{S}pringer-{V}erlag },
	pages = {113 - 127 },
	address = {{I}talie },
	volume = {3701 / 2005 },
	note = {{F}.: {T}heory of {C}omputation },
	audience = {not specified },
    month = {10},
    year = {2005},
    URL = {http://hal.inria.fr/inria-00000744/en/},
    URL = {http://hal.inria.fr/inria-00000744/PDF/final.pdf},
}

The graph rewriting calculus: confluence and expressiveness

Clara Bertolissi (

) ¹

(2005)

Access to full text
PDF

9th Italian Conference on Theoretical Computer Science, ICTCS 2005 3701 / 2005 (2005) 113 - 127

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.

1:	PROTHEO (INRIA Lorraine - LORIA)
	INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine

Domain

Computer Science/Other

Keywords : term graph rewriting – matching – cyclic lambda calculus


inria-00000744, version 1
http://hal.inria.fr/inria-00000744/en/
oai:hal.inria.fr:inria-00000744_v1
From: Clara Bertolissi <>
Submitted on: Tuesday, 15 November 2005 16:25:44
Updated on: Monday, 3 July 2006 15:11:38