Unifying Semantic Path Order and Weighted Path Order

問題
単調意味経路順序（MSPOs）と重み付き経路順序（WPOs）は、項書き換え系（TRS）の停止性を証明するために確立され、強力な還元順序です。両者とも効果的ですが、歴史的には別々のアプローチとして扱われてきました。先行研究は WPO が MSPO のインスタンスであることを示しましたが、MSPO を一般化された WPO のインスタンスとして扱いながら、両者の望ましい性質を保持する統一的な枠組みは、完全に明確化されていませんでした。さらに、既存の構成法は、定理証明に不可欠な基底完全性（ground totality）と、異なる代数および優先順位に基づく設定間での効率的な比較メカニズムを同時に達成することに苦労しています。

方法論
著者らは、**一般化重み付き経路順序（GWPO）およびその単調版である単調一般化重み付き経路順序（MGWPO）**の導入を通じて、これらの順序の統合を提案します。

1. 基礎構造: 統合された順序の中核は、もともと MSPO 向けに導入された還元トリプル $(\geq, \succeq, \succ)$ に基づいています。還元トリプルは、書き換え順序 $\geq$、$\succ$ が整礎である安定した順序対 $(\succeq, \succ)$、および順序と順序対を結びつける調和条件から構成されます。
2. GWPO の定義: GWPO ($>_G$) は、2 つの対の関係 $(\succeq_A, \succ_A)$ と $(\succeq_B, \succ_B)$ を用いて定義されます。項 $s$ が $t$ より大きいとは、
   • $s \succ_A t$ であるか、
   • $s \succeq_A t$ であり、部分項および辞書式比較に関する特定の再帰的条件が成り立ち、さらなる比較のために第 2 の対 $(\succeq_B, \succ_B)$ を利用しうる場合、を意味します。
3. 単調性: 順序が文脈に対して閉じていること（還元順序の要件）を確保するため、MGWPO ($>_{MG}$) は $\geq_A \cap \geq_B \cap >_G$ の共通部分として定義されます。
4. 還元対: この枠組みは、部分ステータス ($\pi$) を組み込んだ還元対 $(\geq, >)$ に拡張されます。これにより、関数引数のより柔軟な処理が可能となり、標準的な WPO アプローチを一般化します。
5. 統合の論理:
   • MGWPO としての WPO: 標準的な WPO は、トリプル A が弱単純代数によって誘導され、トリプル B が優先順位によって誘導される MGWPO であることが示されます。
   • MGWPO としての MSPO: MSPO は、トリプル A が自明であり、トリプル B が MSPO の還元トリプルに対応する MGWPO であることが示されます。逆に、著者らは任意の MGWPO が、基礎となるトリプルの特定の辞書式結合を構成することで MSPO として表現できることを証明します。

主な貢献

• 一般化: 本論文は GWPO と MGWPO を導入し、MSPO と WPO の両方がこの一般化された枠組みの特定のインスタンスであることを実証します。
• 基底完全性: 著者らは、WPO は自然に基底完全性（任意の 2 つの異なる基底項を比較する能力）をサポートするのに対し、MSPO はそうではないことを特定します。MGWPO 枠組みにより、既存の構成法では扱いが難しかった方程式（例えば、組合子 S と K に関するもの）を方向付けられる基底完全な還元順序の構築が可能になります。
• 最適化: 統合された順序は、比較の最適化を提供します。第 1 成分 ($\succ_A$) を通じて厳密な減少が検出された場合、再帰的なチェックなしで比較が即座に終了します。これは、辞書式経路順序（LPO）ではなく、カーン・ベンディックス順序（KBO）の効率性を模倣するものです。
• 複雑性の改善: 厳密順序 $\succ_A$ に部分項性質を課すことで、著者らは項のサイズ（基本関係比較の数で測定）に対して線形時間で MGWPO 比較を決定する手順を導き出します。これは、LPO 風の定義に典型的な二次時間複雑性を改善するものです。
• 還元対の統合: 本論文は、これらの結果を部分ステータスを伴う還元対に拡張し、特定の単純性の条件が満たされれば、MGWPO と MSPO をこの設定でも統合できることを証明します。

結果
著者らは、提案された還元対を用いた依存対法に基づくプロトタイプの停止性ツールの実装を行いました。評価は、Termination Problem Database (TPDB) から 1,528 の有限 TRS を用いて行われ、制限時間は 1 分でした。

• パフォーマンス: GWPO 設定は 591 の系で停止性を証明し、SPO（意味経路順序）設定は 595 の系で証明しました。これに対し、標準的な WPO は 486 でした。
• 比較: 各設定は異なる問題セットを解決しました。SPO 設定は、GWPO に必要な条件である「部分ステータスに対して弱単純でない」代数成分を持つ問題を解決することができました。
• 最先端との比較: 著者らは、自らの手法が標準的な WPO よりも多くの停止性インスタンスを証明する一方で、自らのツールで解決されたすべての問題は、最先端の証明器 AProVE または NaTT によっても解決されていたと指摘しています。したがって、著者らは以前は解決不可能だった新しい問題を解決したとは主張せず、むしろ自らのアプローチの理論的な統合と特定の効率性の向上を実証したに過ぎません。

意義
本論文の意義は、主に 2 つの主要な還元順序クラスの理論的な統合にあります。MSPO が GWPO のインスタンスであることを示す（その逆も同様）ことで、この研究は両者から望ましい性質を継承する単一の枠組みを提供します。

1. 定理証明手法（例えば超位置計算）にとって重要な特徴である基底完全な順序の構築を可能にします。これは、MSPO には自然には存在しなかった機能です。
2. 主要な代数成分で厳密な減少が見つかった際に再帰的なチェックを回避することで、比較を最適化するメカニズムを提供し、特定の設定では線形時間複雑性につながる可能性があります。
3. 代数解釈と優先順位に基づく順序との関係を明確にし、これらとのつながりをカーン・ベンディックス順序および意味経路順序に関する以前の観察にまで遡って説明します。

この研究は、意味経路順序と重み付き経路順序の間のギャップを埋めるための基礎的なステップであり、停止性解析のためのより柔軟で潜在的に効率的なツールキットを提供するものであり、これは第 1 著者の博士論文でさらに詳細に記述されています。