Английская Википедия:Dershowitz–Manna ordering

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Шаблон:Redirect 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 <math>(S, <_S)</math> is a well-founded partial order and let <math>\mathcal{M}(S)</math> be the set of all finite multisets on <math>S</math>. For multisets <math>M,N \in \mathcal{M}(S)</math> we define the Dershowitz–Manna ordering <math>M <_{DM} N</math> as follows:

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

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

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

<math>M <_{DM} N</math> if and only if

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

References

• Шаблон: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].)
• Шаблон:Citation.
• Шаблон:Citation.