Persistence of Termination for Non-Overlapping Term Rewriting Systems

A property is called persistent if for any many-sorted term rewriting system , has the property if and only if term rewriting system , which results from by omitting its sort information, has the property. In this paper,we show that termination is persistent for non-overlapping term rewriting systems and we give the example as application of this result. Furthermore we obtain that completeness is persistent for non-overlapping term rewriting systems.

Authors:

• Munehiro Iwami

Keywords:

• Theory of computing
• Model-based reasoning
• termrewriting system
• termination

References:

[1] T. Aoto and Y. Toyama, "Persistency of confluence," J. Universal
Computer Science, 3, pp.1134-1147, 1997.
[2] T. Aoto, "Solution to the problem of Zantema on a persistent property of
term rewriting systems," Proc. 7th International Conf. on Algebraic and
Logic Programming, LNCS, 1490, Springer-Verlag, pp.250-265, 1998.
[3] F. Baader and T. Nipkow, "Term rewriting and all that," Cambridge
University Press, 1998.
[4] N. Dershowitz and J. P. Jouannaud, Rewrite systems, In Handbook of
Theoretical Computer Science, vol.B, ed. J. van Leeuwen, pp.243-320,
The MIT Press/Elsevier, 1990.
[5] N. Dershowitz, "Termination of rewriting," J. Symbolic Computation,
3, pp.69-116, 1987.
[6] B. Gramlich, "Abstract relations between restricted termination and
confluence properties of rewrite systems," Fundamenta Informaticae,
24, pp.3-23, 1995.
[7] M. Iwami, "Persistence of termination for locally confluent overlay
term rewriting systems," Proc. International Conf. on Information
Technology, to appear.
[8] M. Iwami, "Persistence of termination for right-linear overlay term
rewriting systems," Proc. International Conf. on Information Technology,
to appear.
[9] M. Iwami, "Persistence of termination for term rewriting systems with
ordered sorts," Proc. International Conf. on Information Technology, to
appear.
[10] M. Iwami, "Persistence of semi-completeness for term rewriting systems,"
Proc. International Conf. on Information Technology, to appear.
[11] J. W. Klop, "Term rewriting systems," In Handbook of Logic in
Computer Science, vol.2, pp.1-112, ed. S. Abramsky, D. Gabbay and
T. Mabiaum, Oxford University Press, 1992.
[12] M.R.K. Krishna Rao, "Modular proofs for completeness of hierarchical
term rewriting systems," Theoretical Computer Science, 151, pp.487-
512, 1995.
[13] E. Ohlebusch, "Modular properties of composable term rewriting
systems," J. Symbolic Computation, 20, (1), pp.1-41, 1995.
[14] E. Ohlebusch, "Advanced topics in term rewriting," Springer-Verlag,
2002.
[15] H. Ohsaki and A. Middeldorp, "Type introduction for equational
rewriting," Proc. 4th International Symp. on Logical Foundations of
Computer Science, LNCS, 1234, Springer-Verlag, pp.283-293, 1997.
[16] Y. Toyama, "Counterexamples to termination for the direct sum of term
rewriting systems," Information Processing Letters, 25, pp.141-143,
1987.
[17] H. Zantema, "Termination of term rewriting: interpretation and type
elimination," J. Symbolic Computation, 17, pp.23-50, 1994.