Leanest Quasi-orderings

Preliminary Version
  • Nachum Dershowitz
  • E. Castedo Ellerman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Jouannaud, J.-P., Lescanne, P.: On multiset orderings. Information Processing Letters 15(2), 57–63 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Martin, U.: Extension functions for multiset orderings. Information Processing Letters 26, 181–186 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Martin, U.: A geometrical approach to multiset orderings. Information Processing Letters 67, 37–54 (1989)zbMATHGoogle Scholar
  6. 6.
    Martin, U., Scott, E.: The order types of termination orderings on monadic terms, strings and multisets. J. Symbolic Logic 62(2), 624–635 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Serebrenik, A., Schreye, D.D.: On termination of meta-programs. Theory and Practice of Logic Programming. To appear, available at
  8. 8.
    Smyth, M.B.: Powerdomains. J. of Computer and System Sciences 16(1), 23–36 (1978)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Nachum Dershowitz
    • 1
  • E. Castedo Ellerman
    • 2
  1. 1.School of Computer ScienceTel Aviv UniversityRamat Aviv, Tel AvivIsrael
  2. 2. CambridgeUSA

Personalised recommendations