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

$M <_{DM} N$ whenever there exist two multisets $X,Y \in \mathcal{M}(S)$ with the following properties:

$X \neq \varnothing$ ,
$X \subseteq N$ ,
$M = (N-X)+Y$ , and
$X$ dominates $Y$ , that is, for all $y \in Y$ , there is some $x\in X$ such that $y <_S x$ .

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

$M <_{DM} N$ if and only if

$M \neq N$ , and
for all $y$ in $S$ , if $M(y) > N(y)$ then there is some $x$ in $S$ such that $y <_S x$ and $M(x) < N(x)$ .

References

Dershowitz, Nachum; Manna, Zohar (1979), "Proving termination with multiset orderings", Communications of the ACM 22 (8): 465–476, doi:10.1145/359138.359142, MR 540043 . (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 .
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 675869 .