[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |