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

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

Problem #28

Originator: Pierre Lescanne
Date: April 1991

Summary: Develop effective methods to decide whether a system decreases with respect to some exponential interpretation.

Polynomial and exponential interpretations have been used to prove termination. For the former there are some reasonable methods [CL87, Lan79] that can help determine if a particular interpretation decreases with each application of a rule. Are there other implementable methods suitable for exponential interpretations?

Remark

Some work on this problem has been reported in [Les92].

References

[CL87]

Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–159, October 1987.

[Lan79]

Dallas S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, May 1979. Revised October 1979.

[Les92]

Pierre Lescanne. Termination of rewrite systems by elementary interpretations. In Hélène Kirchner and Giorgio Levi, editors, 3th International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 21–36, Volterra, Italy, September 1992. Springer-Verlag.

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

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