Dershowitz–Manna ordering
   HOME

TheInfoList



OR:

In mathematics, the Dershowitz–Manna ordering is a
well-founded In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s& ...
ordering on multisets named after Nachum Dershowitz and
Zohar Manna Zohar Manna (1939 – 30 August 2018) was an Israeli-American computer scientist who was a professor of computer science at Stanford University. Biography He was born in Haifa, Israel. He earned his Bachelor of Science (BS) and Master of Scienc ...
. It is often used in context of termination of programs or term rewriting systems. Suppose that (S, <_S) is a
well-founded In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s& ...
partial order and let \mathcal(S) be the set of all finite multisets on S. For multisets M,N \in \mathcal(S) we define the Dershowitz–Manna ordering M <_ N as follows: M <_ N whenever there exist two multisets X,Y \in \mathcal(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 <_ N if and only if *M \neq 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 uly 1979) *. *. {{DEFAULTSORT:Dershowitz-Manna ordering Formal languages Logic in computer science Rewriting systems