EQUATIONAL TERM GRAPH REWRITING

Article type: Research Article

Authors: Ariola, Zena M. | Klop, Jan Willem

Affiliations: Computer & Information Science Department, University of Oregon, Eugene, OR 97401, USA. E-mail: [email protected] | Department of Software Technology, CWI, Department of Computer Science, Free University, Amsterdam, The Netherlands. E-mail: [email protected]

Abstract: We present an equational framework for term graph rewriting with cycles. The usual notion of homomorphism is phrased in terms of the notion of bisimulation, which is well-known in process algebra and concurrency theory. Specifically, a homomorphism is a functional bisimulation. We prove that the bisimilarity class of a term graph, partially ordered by functional bisimulation, is a complete lattice. It is shown how Equational Logic induces a notion of copying and substitution on term graphs, or systems of recursion equations, and also suggests the introduction of hidden or nameless nodes in a term graph. Hidden nodes can be used only once. The general framework of term graphs with copying is compared with the more restricted copying facilities embodied in the μ-rule. Next, orthogonal term graph rewrite systems, also in the presence of copying and hidden nodes, are shown to be confluent.

DOI: 10.3233/FI-1996-263401

Journal: Fundamenta Informaticae, vol. 26, no. 3-4, pp. 207-240, 1996