| Simulating Term Rewriting (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| ABSTRACT Several authors have investigated the correspondence between graph rewriting and term rewriting. Almost invariably they have considered only acyclic graphs. Yet cyclic graphs naturally arise from certain optimisations in implementing functional languages. They correspond to infinite terms, and their reductions correspond to transfinite term reduction sequences, which have recently received detailed attention. We formalise the close correspondence between finitary cyclic graph rewriting and a restricted form of infinitary term rewriting, called rational term rewriting. This subsumes the known relation between finitary acyclic graph rewriting and finitary term rewriting. Surprisingly, the correspondence breaks down for general infinitary rewriting. We present an example showing that infinitary term rewriting is strictly more powerful than infinitary graph rewriting. The study also clarifies the technical difficulties resulting from the combination of collapsing rewrite rules and cyclic graphs. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||