Dershowitz–Manna ordering

Template:Orphan 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$ $S$, if $M(y)>N(y)$ then there is some $x$ in $S$ such that $y<_{S}x$ and $M(x)<N(x)$.

References

• {{#invoke:citation/CS1|citation

|CitationClass=citation }}. (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].)

• {{#invoke:citation/CS1|citation

|CitationClass=citation }}.

• {{#invoke:citation/CS1|citation

|CitationClass=citation }}.