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

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

Problem #60 (Solved !)

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.

Remark

This has been solved positively by Takahito Aoto [Aot01].

References

[Aot01]

Takahito Aoto. Solution to the problem of Zantema on a persistent property of term rewriting systems. Journal of Functional and Logic Programming, 2001(11), December 2001.

[Zan94]

Hans Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.

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

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