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 [math]\displaystyle{ (S, \lt _S) }[/math] is a well-founded partial order and let [math]\displaystyle{ \mathcal{M}(S) }[/math] be the set of all finite multisets on [math]\displaystyle{ S }[/math]. For multisets [math]\displaystyle{ M,N \in \mathcal{M}(S) }[/math] we define the Dershowitz–Manna ordering [math]\displaystyle{ M \lt _{DM} N }[/math] as follows:

[math]\displaystyle{ M \lt _{DM} N }[/math] whenever there exist two multisets [math]\displaystyle{ X,Y \in \mathcal{M}(S) }[/math] with the following properties:

• [math]\displaystyle{ X \neq \varnothing }[/math],
• [math]\displaystyle{ X \subseteq N }[/math],
• [math]\displaystyle{ M = (N-X)+Y }[/math], and
• [math]\displaystyle{ X }[/math] dominates [math]\displaystyle{ Y }[/math], that is, for all [math]\displaystyle{ y \in Y }[/math], there is some [math]\displaystyle{ x\in X }[/math] such that [math]\displaystyle{ y \lt _S x }[/math].

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

[math]\displaystyle{ M \lt _{DM} N }[/math] if and only if

• [math]\displaystyle{ M \neq N }[/math], and
• for all [math]\displaystyle{ y }[/math] in [math]\displaystyle{ S }[/math], if [math]\displaystyle{ M(y) \gt N(y) }[/math] then there is some [math]\displaystyle{ x }[/math] in [math]\displaystyle{ S }[/math] such that [math]\displaystyle{ y \lt _S x }[/math] and [math]\displaystyle{ M(x) \lt N(x) }[/math].

References

• Dershowitz, Nachum (1979), "Proving termination with multiset orderings", Communications of the ACM 22 (8): 465–476, doi:10.1145/359138.359142 . (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., Formal Language Theory: Perspectives and Open Problems, New York: Academic Press, pp. 349–405 .
• "On multiset orderings", Information Processing Letters 15 (2): 57–63, 1982, doi:10.1016/0020-0190(82)90107-7 .