Persistence of Termination for Non-Overlapping Term Rewriting Systems

Authors: Munehiro Iwami

Abstract:

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.

Keywords: Theory of computing, Model-based reasoning, termrewriting system, termination

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1079732

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.