Dershowitz–Manna ordering

In mathematics, the Dershowitz–Manna ordering is a well-founded ordering on multisets named after Nachum Dershowitz and Zohar Manna. It is often used in context of termination of programs or term rewriting systems.

Suppose that is a well-founded partial order and let be the set of all finite multisets on . For multisets we define the Dershowitz–Manna ordering as follows:

whenever there exist two multisets with the following properties:

  • ,
  • ,
  • , and
  • dominates , that is, for all , there is some such that .

An equivalent definition was given by Huet and Oppen as follows:

if and only if

  • , and
  • for all in , if then there is some in such that and .

References

edit
  • Dershowitz, Nachum; Manna, Zohar (1979), "Proving termination with multiset orderings", Communications of the ACM, 22 (8): 465–476, CiteSeerX 10.1.1.1013.432, doi:10.1145/359138.359142, MR 0540043, S2CID 17906810. (Also in Proceedings of the International Colloquium on Automata, Languages and Programming, Graz, Lecture Notes in Computer Science 71, Springer-Verlag, pp. 188–202 [July 1979].)
  • Huet, G.; Oppen, D. C. (1980), "Equations and rewrite rules: A survey", in Book, R. (ed.), Formal Language Theory: Perspectives and Open Problems, New York: Academic Press, pp. 349–405.
  • Jouannaud, Jean-Pierre; Lescanne, Pierre (1982), "On multiset orderings", Information Processing Letters, 15 (2): 57–63, doi:10.1016/0020-0190(82)90107-7, MR 0675869.