[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #86

Originator: Hans Zantema
Date: April 1995

Summary: Is the union of two totally terminating rewrite systems, which do not share any symbols, totally terminating?

When there exists a monotonic well-ordering (monotonic means that replacing a subterm with a smaller one decreases the whole term) of ground terms that shows termination of a rewrite system, the system is called totally terminating. The union of two totally terminating rewrite systems which do not share any symbols is totally terminating if at least one of them does not contain a rule that has more occurrences of some variable on the right than on the left [FZ93, FZ96]. What if variables are duplicated?

References

[FZ93]

M. C. F. Ferreira and Hans Zantema. Total termination of term rewriting. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 213–227, Montreal, Canada, June 1993. Springer-Verlag. Extended version as [FZ96].

[FZ96]

M. C. F. Ferreira and Hans Zantema. Total termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing, 7(2):133–162, 1996.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]