Confluent rewriting of bisimilar term graphs
Zena M. Ariola, Jan Willem Klop, Detlef Plump · Electronic Notes in Theoretical Computer Science · 1997
We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for four different kinds of term graph rewriting: besides plain applications of rewrite rules, extensions with the operations of collapsing and copying, and with both operations together are considered. Collapsing and copying together constitute bisimilarity of term graphs. We establish sufficient conditions for, and counterexamples to, confluence and confluence modulo bisimilarity of term graph rewriting over various classes of term rewriting systems.