Title
A Rewriting Calculus for Cyclic Higher-order Term Graphs
Abstract
Introduced at the end of the nineties, the Rewriting Calculus (@r-calculus, for short) is a simple calculus that fully integrates term-rewriting and @l-calculus. The rewrite rules, acting as elaborated abstractions, their application and the obtained structured results are first class objects of the calculus. The evaluation mechanism, generalizing beta-reduction, strongly relies on term matching in various theories. In this paper we propose an extension of the @r-calculus, handling graph like structures rather than simple terms. The transformations are performed by explicit application of rewrite rules as first class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities. The calculus over terms is naturally generalized by using unification constraints in addition to the standard @r-calculus matching constraints. This therefore provides us with the basics for a natural extension of an explicit substitution calculus to term graphs. Several examples illustrating the introduced concepts are given.
Year
DOI
Venue
2005
10.1016/j.entcs.2005.01.034
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
cyclic lambda calculus,natural extension,explicit substitution calculus,simple calculus,rewriting calculus,explicit application,matching and unification constraints,term graphs,term graph,elaborated abstraction,class object,class entity,cyclic higher-order term graphs,simple term,graph matching,higher order,lambda calculus
Discrete mathematics,Normalisation by evaluation,Natural deduction,Computer science,Proof calculus,Calculus of communicating systems,Time-scale calculus,Explicit substitution,Church encoding,Process calculus
Journal
Volume
Issue
ISSN
127
5
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
9
0.56
16
Authors
4
Name
Order
Citations
PageRank
C. Bertolissi1110.93
P. Baldan2514.13
H. Cirstea3110.93
C. Kirchner490.56