ダーショウィッツ-マンナ順序付け

数学において、ダーショウィッツ・マンナ順序は、ナフム・ダーショウィッツとゾハール・マンナにちなんで名付けられた、多重集合上の整礎順序である。これは、プログラムの終了性や項書き換えシステムの文脈でよく用いられる。

仮に${\displaystyle (S,<_{S})}$は整礎半順序であり、$\displaystyle {\mathcal {M}}(S)}$上のすべての有限多重集合の集合とする${\displaystyle S}$多重集合の場合${\displaystyle M,N\in {\mathcal {M}}(S)}$我々はダーショウィッツ・マンナ順序を定義する${\displaystyle M<_{DM}N}$次のように：

${\displaystyle M<_{DM}N}$2 つの多重集合が存在する場合${\displaystyle X,Y\in {\mathcal {M}}(S)}$以下の特性を持つ：

• ${\displaystyle X\neq \varnothing }$、
• ${\displaystyle X\subseteq N}$、
• ${\displaystyle M=(NX)+Y}$、 そして
• ${\displaystyle X}$支配する${\displaystyle Y}$つまり、すべての ${\displaystyle y\in Y}$いくつかあります${\displaystyle x\in X}$そのため${\displaystyle y<_{S}x}$。

同等の定義は、Huet と Oppen によって次のように与えられています。

${\displaystyle M<_{DM}N}$かつその場合に限り

• ${\displaystyle M\neq N}$、 そして
• すべての人々のために${\displaystyle y}$で${\displaystyle S}$、 もし${\displaystyle M(y)>N(y)}$すると、いくつか${\displaystyle x}$で${\displaystyle S}$そのため${\displaystyle y<_{S}x}$そして${\displaystyle M(x)<N(x)}$。

• Dershowitz, Nachum; Manna, Zohar (1979)、「多重集合順序による終了性の証明」、Communications of the ACM、22 (8): 465–476、CiteSeerX 10.1.1.1013.432、doi : 10.1145/359138.359142、MR 0540043、S2CID 17906810   （また、グラーツで開催された国際オートマタ・言語・プログラミングに関するコロキウムの議事録、Lecture Notes in Computer Science 71、Springer-Verlag、pp.  188–202 [1979年7月]にも掲載。）
• Huet, G.; Oppen, DC (1980)、「方程式と書き換え規則：概観」、Book, R. (編)『形式言語理論：展望と未解決問題』、ニューヨーク：Academic Press、pp. 349–405 。
• ジャン・ピエール・ジュアンノー; Lescanne、Pierre (1982)、「マルチセット順序付けについて」、Information Processing Letters、15 (2): 57–63、doi : 10.1016/0020-0190(82)90107-7、MR 0675869 。