[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Hans Zantema
Date: June 1993
Summary: Does termination of a many-sorted rewrite system reduce to the one-sorted case in case all variables are of the same sort?
Let R be a many-sorted term-rewriting system and R′ the one-sorted system consisting of the same rules, but in which all operation symbols are considered to be of the same sort. Any rewrite in R is also a rewrite in R′. The converse does not hold, since terms and rewrite steps in R′ are allowed that are not well-typed in R. In [Zan94] it was shown that termination of R is in general not equivalent to termination of R′, but it is if R does not contain both collapsing and duplicating rules. Are termination of R and of R′ equivalent in the case where all variables occurring in R are of the same sort? If this statement holds, it would follow that simulating operation symbols of arity n greater than 2 by n−1 binary symbols in a straightforward way does not affect termination behavior.
This has been solved positively by Takahito Aoto [Aot01].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |