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

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

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

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 }}.