[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #74

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.

Comment sent by Klaus Guenter Dabisch

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.

References

[BvG+87]
Henk Barendregt, M. C. J. D. van Eekelen, J. R. W. Glauert, J. R. Kennaway, M. J. Plasmeijer, and M. R. Sleep. Term graph rewriting. In Proceedings of the European Workshop on Parallel Architectures and Languages, volume 259 of Lecture Notes in Computer Science, pages 141–158, Berlin, 1987. Springer-Verlag.
[HP91]
B. Hoffmann and D. Plump. Implementing term rewriting by jungle evaluation. RAIRO Theoretical Informatics and Applications, 25(5):445–472, 1991.
[Ohl97]
Enno Ohlebusch. Conditional term graph rewriting. In 6th International Conference on Algebraic and Logic Programming, volume 1298 of Lecture Notes in Computer Science, pages 144–158. Springer-Verlag, 1997.
[Plu91]
D. Plump. Implementing term rewriting by graph reduction: Termination of combined systems. In S. Kaplan and M. Okada, editors, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada, June 1990), volume 516 of Lecture Notes in Computer Science, pages 307–317, Berlin, 1991. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]