Infinitary term graph rewriting is simple, sound and complete

TY - GEN

T1 - Infinitary term graph rewriting is simple, sound and complete

AU - Bahr, Patrick

N1 - Conference code: 23

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - Faculty of Science

KW - term graphs

KW - infinitary rewriting

KW - simulation

KW - normalising

KW - strong convergence

U2 - 10.4230/LIPIcs.RTA.2012.69

DO - 10.4230/LIPIcs.RTA.2012.69

M3 - Article in proceedings

T3 - Leibniz International Proceedings in Informatics

SP - 69

EP - 84

BT - 23rd International Conference on Rewriting Techniques and Applications (RTA'12)

A2 - Tiwari, Ashish

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 23rd International Conference on Rewriting Techniques and Applications

Y2 - 28 May 2012 through 2 June 2012

ER -