Persistence of Termination for Term Rewriting Systems with Ordered Sorts

Authors: Munehiro Iwami

Abstract:

A property is 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. Zantema showed that termination is persistent for term rewriting systems without collapsing or duplicating rules. In this paper, we show that the Zantema's result can be extended to term rewriting systems on ordered sorts, i.e., termination is persistent for term rewriting systems on ordered sorts without collapsing, decreasing or duplicating rules. Furthermore we give the example as application of this result. Also we obtain that completeness is persistent for this class of term rewriting systems.

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

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

References:

[1] T. Aoto and Y. Toyama, "Persistency of confluence," J. Universal Computer Science, 3, pp.1134-1147, 1997.
[2] T. Aoto and Y. Toyama, "Extending persistency of confluence with ordered sorts," Research report, IS-RR-96-0025F, School of Information Science, JAIST, 1996.
[3] 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.
[4] F. Baader and T. Nipkow, "Term rewriting and all that," Cambridge University Press, 1998.
[5] N. Dershowitz and Z. Manna, "Proving termination with multiset orderings," Commun. ACM, 22 (8), pp.465-476, 1979.
[6] 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.
[7] N. Dershowitz, "Termination of rewriting," J. Symbolic Computation, 3, pp.69-116, 1987.
[8] J. A. Goguen and J. Meseguer, "Order-sorted algebra 1: equational deduction for multiple inheritance, overloading, exceptions and partial operations" Theoretical Computer Science, 105, (2), pp.217-273, 1992.
[9] M. Iwami and Y. Toyama, "On the persistency of termination of term rewriting systems with ordered sorts," Proc. 14th Conf. on Japan Society for Software Science and Technology, pp.357-360, 1997 (in Japanese).
[10] M. Iwami, "Termination of higher-order rewrite systems," Ph.D. thesis, JAIST, 1999.
[11] M. Iwami, "Persistence of termination for non-overlapping term rewriting systems," Proc. International Conf. on Information Technology, to appear.
[12] M. Iwami, "Persistence of termination for locally confluent overlay term rewriting systems," Proc. International Conf. on Information Technology, to appear.
[13] M. Iwami, "Persistence of termination for right-linear overlay term rewriting systems," Proc. International Conf. on Information Technology, to appear.
[14] M. Iwami, "Persistence of semi-completeness for term rewriting systems," Proc. International Conf. on Information Technology, to appear.
[15] 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.
[16] M.R.K. Krishna Rao, "Modular proofs for completeness of hierarchical term rewriting systems," Theoretical Computer Science, 151, pp.487-512, 1995.
[17] E. Ohlebusch, "Modular properties of composable term rewriting systems," J. Symbolic Computation, 20, (1), pp.1-41, 1995.
[18] E. Ohlebusch, "A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems," Bullen of the EATCS, 49, pp.178-183, 1993.
[19] E. Ohlebusch, "Advanced topics in term rewriting," Springer-Verlag, 2002.
[20] 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.
[21] H. Ohsaki, "Termination of term rewriting systems: transformation and persistence," Ph.D. thesis, Tsukuba University, 1998.
[22] G. Smolka, W. Nutt, J. A. Goguen and J. Meseguer, "Order-sorted equational computation, resolution of equations in algebraic structures," vol.2, pp.297-367, Academic Press, 1989.
[23] H. Zantema, "Termination of term rewriting: interpretation and type elimination," J. Symbolic Computation, 17, pp.23-50, 1994.