Abstract
A convenient method for defining a quasi-ordering, such as those used for proving termination of rewriting, is to choose the minimum of a set of quasi-orderings satisfying some desired traits. Unfortunately, a minimum in terms of set inclusion can be non-existent even when an intuitive “minimum” exists. We suggest an alternative to set inclusion, called “leanness”, show that leanness is a partial ordering of quasi-orderings, and provide sufficient conditions for the existence of a “leanest” ordering.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)
Dershowitz, N., Reingold, E.M.: Ordinal arithmetic with list expressions. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol. 620, pp. 117–126. Springer, Heidelberg (1992)
Jouannaud, J.-P., Lescanne, P.: On multiset orderings. Information Processing Letters 15(2), 57–63 (1982)
Martin, U.: Extension functions for multiset orderings. Information Processing Letters 26, 181–186 (1987)
Martin, U.: A geometrical approach to multiset orderings. Information Processing Letters 67, 37–54 (1989)
Martin, U., Scott, E.: The order types of termination orderings on monadic terms, strings and multisets. J. Symbolic Logic 62(2), 624–635 (1997)
Serebrenik, A., Schreye, D.D.: On termination of meta-programs. Theory and Practice of Logic Programming. To appear, available at http://arxiv.org/abs/cs.PL/0110035
Smyth, M.B.: Powerdomains. J. of Computer and System Sciences 16(1), 23–36 (1978)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N., Ellerman, E.C. (2005). Leanest Quasi-orderings. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)