Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.
Lipics : Leibniz International Proceedings in Informatics, 2012, p. 69-84
term graphs; infinitary rewriting; simulation; normalising; strong convergence; The Faculty of Science
Main Research Area:
23rd International Conference on Rewriting Techniques and Applications, 2012