[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: D. Plump, Bruno Courcelle
Date: June 1993, January 1998
Summary: How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?
Graph rewriting systems that implement term rewriting systems (see, for example, [BvG^{+}87][HP91]) are terminating whenever term rewriting is. The converse, however, does not hold [Plu91]. How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?
It would be interesting to see an example not too artificial where the termination proof is difficult. Graph rewriting systems implementing term rewriting do not duplicate subgraphs. So the major source of difficulty in termination proofs disappears.
Date: Mon Mar 9 13:44:57 MET 1998
This problem was solved intuitively in [Ohl97]. One could solve the difficult termination proofs in this way: The Gross-Knuth reduction is defined by: Contract all redexes simultaneously [BvG^{+}87]. Then, however, one has to prove that the result is unequivocal.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |