Dershowitz–Manna ordering explained

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 l{M}(S) be the set of all finite multisets on S . For multisets M,N \in l{M}(S) we define the Dershowitz–Manna ordering M < _{DM} N as follows:M < _{DM} N whenever there exist two multisets X,Y \in l{M}(S) with the following properties:X ≠ \varnothing ,X \subseteq N ,M = (N - X) + Y , andX 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 ≠ 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 [July 1979].)
• .
• .