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

$M <_ N$ whenever there exist two multisets $X,Y \in \mathcal(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 <_ 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

*. (Also in ''Proceedings of the International Colloquium on Automata, Languages and Programming'', Graz, Lecture Notes in Computer Science 71, Springer-Verlag, pp. 188–202 uly 1979)
*.
*.

{{DEFAULTSORT:Dershowitz-Manna ordering
Formal languages
Logic in computer science
Rewriting systems