ON THE ADEQUACY OF GRAPH REWRITING FOR STIMULATING TERM REWRITING

Several authors have investigated the correspondence between graph rew riting and term rewriting. Almost invariably they have considered only acyclic graphs. Yet cyclic graphs naturally arise from certain optimi zations in implementing functional languages. They correspond to infin ite terms, and their reductions correspond to transfinite term-reducti on sequences, which have recently received detailed attention. We form alize the close correspondence between finitary cyclic graph rewriting and a restricted form of infinitary term rewriting, called rational t erm rewriting. This subsumes the known relation between finitary acycl ic graph rewriting and finitary term rewriting. Surprisingly, the corr espondence breaks down for general infinitary rewriting. We present an example showing that infinitary term rewriting is strictly more power ful than infinitary graph rewriting. The study also clarifies the tech nical difficulties resulting from the combination of collapsing rewrit e rules and cyclic graphs.