A rewriting calculus for cyclic higher-order term graphs

• Published in: Mathematical structures in computer science 2007-06, Vol.17 (3), p.363-406
• Main Authors: BALDAN, PAOLO, BERTOLISSI, CLARA, CIRSTEA, HORATIU, KIRCHNER, CLAUDE
• Format: Article
• Language: English
• Subjects: Calculus; Computer Science; Graph theory; Mathematics; Programming Languages
• ISSN: 0960-1295; 1469-8072
• DOI: 10.1017/S0960129507006093

The Rewriting Calculus (ρ-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories. In this paper we propose an extension of the ρ-calculus, called ρg-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard ρ-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the ρ-calculus, 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. We show that the ρg-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that ρg-calculus-terms are considered modulo an equational theory. We also show that the ρg-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and α-calculus with explicit recursion (modelled using a letrec-like construct).