On the Adequacy of Graph Rewriting for Simulating Term Rewriting

Abstract

Several authors have investigatedthe correspondence between graph rewriting and term rewriting.Almost invariably they have considered only acyclic graphs.Yet cyclic graphs naturally arise from certain optimizations 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 formalize 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 .