パス順序付け（項の書き換え）

理論計算機科学、特に項書き換えにおいて、パス順序付けとは、すべての項の集合上の整基礎の 厳密な全順序（>）であり、

f (...) > g ( s ₁ ,..., s _n ) 、 f ^. > g   かつ   f (...) > s _i（i =1,..., n の場合   ）

ここで、( ^{. >) は、すべての}関数シンボルの集合におけるユーザ指定の全体的な優先順位です。

直感的には、項f (...) は、優先順位の低いルート記号g を使用してf (...)より小さい項s _iから構築されたどの項g (...)よりも大きくなります。特に、構造的帰納法により、項f (...) は、 fより小さい記号のみを含むどの項よりも大きくなります。

パス順序は、項書き換え、特にKnuth-Bendix 補完アルゴリズムにおける簡約順序としてよく使用されます。たとえば、数式を「掛け算する」項書き換えシステムには、 x *( y + z ) → ( x * y ) + ( x * z ) という規則を含めることができます。停止性を証明するには、項x *( y + z ) が項 ( x * y )+( x * z )よりも大きくなる簡約順序(>) を見つける必要があります。前者の項には後者よりも関数記号と変数が少ないため、これは簡単ではありません。ただし、優先順位 (*) ^. > ( + ) を設定すると、 x *( y + z ) > x * yとx *( y + z ) > x * zはどちらも簡単に実現できる ため、パス順序を使用できます。

特定の一般的な再帰関数に対するシステムも存在する可能性があり、たとえばアッカーマン関数のシステムにはA( a ⁺、 b ⁺ )→A( a、A( a ⁺、b ))という規則が含まれる場合があります^[1]。ここでb ^+はbの後続を表します。

2 つの項sとt が与えられ、それぞれルート記号fとgが与えられている場合、それらの関係を決定するために、まずそれらのルート記号を比較します。

• f < ^. gの場合、s の s部分項の 1 つが t を支配している場合にのみ、s はt を支配できます。
• f ^. > gの場合、 s がtの各部分項より優勢であれば、sはt より優勢です。
• f = gの場合、sとtの直近の部分項を再帰的に比較する必要があります。特定の方法に応じて、パス順序のさまざまなバリエーションが存在します。^{[2] [3]}

後者のバリエーションには次のものがあります:

• 多重集合パス順序付け（mpo）、元々は再帰パス順序付け（rpo）と呼ばれていた^[4]
• 辞書式パス順序（lpo）^[5]
• mpoとlpoの組み合わせ。Dershowitz 、Jouannaud (1990) ^{[6] [7] [8]によって}再帰パス順序付けと呼ばれている。

ダーショウィッツ、オカダ（1988）はさらに多くの変種を挙げ、それらをアッカーマンの順序表記法のシステムと関連付けている。特に、 n個の関数記号を持つ再帰的パス順序付けの順序型に与えられた上限は、大きな可算順序数に対するヴェブレン関数を使用して、 φ( n ,0)である。 ^[7]

多重集合パス順序（>）は次のように定義される：^[9]

どこ

• (≥) はmpo (>) の反射的閉包を表す。
• { s ₁ ,..., s _m } はsの部分項の多重集合を表し、 tについても同様であり、
• (>>)は(>)の多重集合拡張を表し、{ s ₁ ,..., s _m } >> { t ₁ ,..., t _n }によって定義され、{ t ₁ ,..., t _n }は{ s ₁ ,..., s _m }から取得できる。
  • 少なくとも1つの要素を削除するか、
  • ある要素を厳密に小さい（mpoに関して）要素の多重集合に置き換えることによって。^[10]

より一般的には、順序関数とは、順序を別の順序にマッピングし、以下の性質を満たす関数Oである。 ^[11]

• (>) が推移的であれば、O (>) も推移的です。
• (>) が非反射的であれば、 O (>) も非反射的です。
• s > tの場合、f (..., s ,...) O (>) f (..., t ,...) となります。
• Oは関係に関して連続である、すなわち、R ₀、R ₁、R ₂、R ₃、...が関係の無限列である場合、O (∪^∞
  _{i =0} R _i ) = ∪^∞
  _{i =0} O ( R _i ) 。

上記の (>) を上記の (>>) にマッピングする多重集合拡張は、順序関数の一例です: (>>)= O (>)。別の順序関数は、辞書式パス順序付けにつながる辞書式拡張です。