en>Declaration1776: /* Properties */ removed unnecessary article

2013-09-23T00:38:35Z

Properties: removed unnecessary article

New page

{{orphan|date=March 2013}}
In mathematics, the '''Dershowitz–Manna ordering''' is a [[Well-founded relation|well-founded]] ordering on [[multiset]]s named after Nachum Dershowitz and [[Zohar Manna]]. It is often used in context of termination of programs or [[abstract rewriting system|term rewriting systems]].

Suppose that <math>(S,<_S)</math> is a [[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> <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
| last1 = Dershowitz | first1 = Nachum
| last2 = Manna | first2 = Zohar | author2-link = Zohar Manna
| doi = 10.1145/359138.359142
| issue = 8
| journal = [[Communications of the ACM]]
| mr = 540043
| pages = 465–476
| title = Proving termination with multiset orderings
| volume = 22
| year = 1979}}. (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
| last1 = Huet | first1 = G.
| last2 = Oppen | first2 = D. C.
| editor-last = Book | editor-first = R.
| contribution = Equations and rewrite rules: A survey
| location = New York
| pages = 349–405
| publisher = Academic Press
| title = Formal Language Theory: Perspectives and Open Problems
| year = 1980}}.
*{{citation
| last1 = Jouannaud | first1 = Jean-Pierre
| last2 = Lescanne | first2 = Pierre
| doi = 10.1016/0020-0190(82)90107-7
| issue = 2
| journal = [[Information Processing Letters]]
| mr = 675869
| pages = 57–63
| title = On multiset orderings
| volume = 15
| year = 1982}}.

{{DEFAULTSORT:Dershowitz-Manna ordering}}
[[Category:Formal languages]]
[[Category:Logic in computer science]]
[[Category:Rewriting systems]]

Graph power - Revision history

en>Declaration1776: /* Properties */ removed unnecessary article