Dershowitz–Manna ordering

"Multiset ordering" redirects here. For the multiset variant of the recursive path ordering, see multiset path 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 ℳ(S) be the set of all finite multisets on S. For multisets M,N∈ℳ(S) we define the Dershowitz–Manna ordering M<DMN as follows:

M<DMN whenever there exist two multisets X,Y∈ℳ(S) with the following properties:

* X≠∅,
* X⊆N,
* M=(N−X)+Y, and
* X dominates Y, that is, for all y∈Y, there is some x∈X such that y<Sx.

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

M<DMN 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<Sx and M(x)<N(x).

## References

* Dershowitz, Nachum (1979), "Proving termination with multiset orderings", Communications of the ACM 22 (8): 465–476, doi:10.1145/359138.359142 . (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].)
* Huet, G.; Oppen, D. C. (1980), "Equations and rewrite rules: A survey", in Book, R., Formal Language Theory: Perspectives and Open Problems, New York: Academic Press, pp. 349–405 .
* "On multiset orderings", Information Processing Letters 15 (2): 57–63, 1982, doi:10.1016/0020-0190(82)90107-7 .

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Dershowitz–Manna ordering. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Dershowitz–Manna_ordering&oldid=3981990"