Lexicographic Combination of Reduction Pairs (Extended Version)

技術要約：減少ペアの辞書式結合

問題設定
項書き換えシステム（TRS）の停止性解析は、多くの場合、依存ペア（Dependency Pair）の枠組みに依拠しており、これは問題を特定の制約を満たす「減少ペア（reduction pair）」$(\geq, >)$ を見つける問題へと還元する。減少ペアとは、置換に対して安定な前順序 $\geq$ と、厳密な整列順序 $>$ からなるものであり、$\geq$ は文脈の下でも閉じている（context closure）。辞書式結合は、単純なものから複雑な停止性尺度を構築するための強力な手法であるが、任意の2つの減少ペアの辞書式結合が必ずしも減少ペアになるとは限らないという根本的な障害が存在する。具体的には、結果として得られる前順序が、しばしば文脈の下での閉包性（単調性）を満たさない。この問題を克服するための従来のアプローチ（ルール除去法や反復的なプロセッサの適用など）は、制限的な制約を課すことがあり、非単調な解釈を含む特定のシステムに対して停止性の証明を阻むことがある。

手法
著者らは、2つの減少ペアの辞書式結合が依然として有効な減少ペアであることを保証する、単純な**結合可能性基準（combinability criterion）**を提案している。

1. 結合可能性基準： 2つの項上の順序ペア $(\geq_1, >_1)$ と $(\geq_2, >_2)$ があるとする。$(\geq_1, >_1)$ が $(\geq_2, >_2)$ と結合可能であるとは、以下を満たすことである：

   • $(\geq_1, >_1)$ が**正規（normal）**である（すなわち、$>_1 \subseteq \geq_1$）。
   • すべての関数記号 $f$ とすべての引数位置 $i$ について、その位置が $>_1$-単調（$>_1$-monotone）（第1の順序において厳密に増加する）であるか、あるいは $\geq_2$-不変（$\geq_2$-invariant）（第2の順序において $f$ の解釈が第 $i$ 引数に依存しない）であるかのいずれかである。

2. 理論的正当化： 論文では、2つの減少ペアがこの基準を満たす場合、それらの辞書式結合 $(\geq_{12}, >_{12})$ が減少ペアであることを証明している（定理10）。この証明は、文脈の閉包性が保持されることを示すことに依拠している。すなわち、ある引数が第1コンポーネントで減少した場合、項全体が減少し、もしそれが第1コンポーネントで変化しない場合は、第2コンポーネントにおける不変性が第2コンポーネлоントにおける不変性を保証し、辞書式順序を維持する。

3. 行列解釈への拡張： 著者らは、キャリアが標準的な成分ごとの順序ではなく、辞書式順序（$>_{lex}$）によって順序付けられた行列解釈の変種を調査している。これらにおいて弱単調性を実現するために必要な行列を、**階段形式行列（echelon-form matrices）**として特徴付けている。

   • 行列 $A$ が階段形式であるとは、$A_{k, j-1} = 0$ であるすべての $k < i$ に対して $A_{i,j} = 0$ となることである。
   • 階段形式行列を備えた解釈から構築された解釈は、減少ペアを形成することを証明している。
   • 定理24は、以下の対応関係を確立している：$d$ 個の線形多項式解釈（結合可能性基準を満たすもの）の辞書式結合は、非対角成分がゼロである $d$ 次元の階段形式行列解釈と等価である。

主な貢献

• 一般的な結合可能性基準： 非単調な解釈を、関連する位置において不変であるという条件下で、より「弱い」コンポーネントとして使用することを可能にする、任意のクラスの減少ペア（多項式、行列、およびクヌース・ベッチ順序を含む）を組み合わせるための、単純でチェック可能な条件。
• 階段形式行列解釈： 辞書式順序を用いた行列解釈の新しいクラスの導入。これにより、行列解釈における辞書式順序の使用に関する未解決の問いが解決された。
• 手法の統合： 提案された基準が、従来のフォークロア的な結果（例：2つの単調な減少ペアの結合）を包含し、一般化していることを示している。また、ヘテロジニアスな手法（例：順序数解釈とクヌース・ベッチ順序の組み合わせ）を組み合わせるための形式的な基礎を提供している。

結果と実験
著者らは、これらの手法を依存ペアの枠組みおよびSMTソルバZ3と統合したプロトタイプツールを実装した。Termination Problem Databaseを用いた実験の結果：

• 標準的な停止性： 1,528個の問題に対し、手法の組み合わせ（具体的には、線形解釈、辞書式パス順序、および階段形式行列解釈の辞書式結合）は、649個のシステムに対して停止性を証明した。これには、最先端のツールであるNaTTが逃した8つの証明が含まれる。
• 相対的停止性： 57個の相対的停止性問題に対し、手法の和集合は50個のケースを証明した。特筆すべきは、これにはAProVEが逃した11個の問題と、NaTT（2022年版）が逃した5個の問題が含まれている点である。
• ケーススタディ： 本手法は、「ヘラクレスとヒドラの戦い（Battle of Hercules and Hydra）」（TouzetのTRS）や、標準的な単調減少ペアでは困難であったリスト処理に関する相対的停止性問題（INVY_15/#3.42）を正常に停止させた。

意義
本論文は、提案された基準が、ルール除去法や反復的な減少ペアプロセッサのような既存の手法に対して補完的であることを主張している。その主要な意義は、標準的な単調性の要件によって証明が阻止されるケースを扱う能力にある。特定の（後続のコンポーネントにおいて不変であるという条件下での）非単調な解釈を許容することで、停止性証明の探索空間を拡大している。著者らは、これが特に、標準的な方法では利用可能なルールの基準を適用できない相対的停止性や、順序数解釈と構文的順序のヘテロジニアスな組み合わせが必要とされるヒドラの戦いのような複雑なシステムにおいて効果的であると述べている。また、本研究は、多項式解釈の辞書式結合と階段形式行列解釈との理論的な関係を明確にし、これらの手法に対する統一的な視点を提供している。