The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

技術要約：ベータ・エータ・ノーマル高階書き換えのための計算可能性パス順序（NCPO）

問題提起
高階書き換えは、様々な形式体系を含んでいる。具体的には、「プレーン」な高階書き換え（構文的一致を用い、$\beta$簡約を書き換え規則として扱うもの）と、「ノーマル」な高階書き換え（$\beta\eta$による一致を用い、項を$\beta\eta$-正規形として扱うもの）である。CPO（Computability Path Order）のようなプレーンな書き換えに対しては強力な停止性判定法が存在するが、これをノーマルな高階書き換え（特にNipkow流のHRS）に適応させることは、大きな課題を伴う。

NHORPO（Normal Higher-Order Recursive Path Order）のような既存の手法は、コアとなる順序が失敗する場合に対処するために、「中立化（neutralization）」と呼ばれる変換技術に依存していることが多い。しかし、中立化は自動化を複雑にする。また、標準的なパス順序は、ノーマル書き換えにおいては困難に直面する。なぜなら、$\beta\eta$と互換性のある整列順序は、伝統的な意味での単調性（コンテキストの下での閉性）や安定性（代入の下での閉性）を持たないことが一般的だからである。例えば、ある順序が$\beta\eta$と互換性があり、かつコンテキストの下で閉じている場合、$c > c$といった矛盾を導き、整列性を損なう可能性がある。

手法
著者らは、プレーンな高階書き換えのために定義されたCPOを、$\beta\eta$-正規高階書き換えの設定へと持ち上げることを提案している。得られた順序は、**$\beta\eta$-ノーマル・コンピュタビリティ・パス順序（NCPO）**と呼ばれる。

この手法は、以下の核となる構成要素に基づいている：

1. 簡約順序のペア： JouannaudとRubioのアプローチに従い、著者らは簡約順序を、プライマリ順序である$>$（NCPO）と、その「プレーン」なバリアントである$\sqsupset$（CPO）のペアとして定義する。このペアは$\beta\eta$-ノーマル安定性を満たす。すなわち、$s > t$ならば、全ての代入$\sigma$に対して$s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$が成立する（ここで$\downarrow$は$\beta\eta$-正規化を表す）。これにより、停止性の証明をプレーンなCPO成分の整列性と単調性に依存させることが可能になる。
2. 非汎用項（Nonversatile Terms）： 重要な技術的革新は、順序の適用対象を非汎用項に制限することである。項が非汎用であるとは、代入とその後の$\beta\eta$-正規化が、その項の真の部分項のみに影響を与えることを指す。著者らは、以前の研究と比較して、非汎用性のための改善された十分条件（補題1）を提供しており、これは順序の安定性を証明するために不可欠である。
3. CPOからの拡張： NCPOは、元のCPOから以下の2つの主要な拡張を取り入れている：
   • 到達可能な部分項（Accessible Subterms）： これにより、型位置（正・負の基底型の位置）によって決定される特定のケースにおいて、再帰的な比較を厳密な型の減少をバイパスして行うことができる。
   • スモール記号（Small Symbols）： この機能により、特定の関数記号を「スモール」として扱うことができ、標準的な再帰パス順序が失敗するシステム（例：リスト処理関数）の停止性証明を可能にする。
4. 規則集合： 順序は、関数記号（ビッグおよびスモール）、適用、および抽象化を扱う一連の規則（図1）を通じて帰納的に定義される。注目すべき点として、$\beta$および$\eta$簡約を方向付ける規則は削除されている。これは、順序が正規形に対して直接作用するためである。また、到達可能な部分項の文脈における$\eta$展開を扱うために、新しい規則$\langle \lambda\triangleright\eta \rangle$が導入されている。

主な貢献

• NCPOの定義： 本論文は、到達可能な部分項とスモール記号を統合した、$\beta\eta$-ノーマル高階書き換えのために特別に設計された最初のコンピュタビリティ・パス順序であるNCPOを正式に定義した。
• 正当性の証明： 著者らは、ペア$(>_\tau, \sqsupset_\tau)$が有効な$\beta\eta$-ノーマル高階簡約順序であることを証明し（定理2）、それによってこれと互換性を持つあらゆるHRSの停止性を保証している。
• 改善された非汎用性条件： 本論文は、NHORPOの基礎となる研究で提供されているものよりも強力な、非汎用性のための洗練された十分条件を提示している。
• SAT/SMTによる自動化： 著者らは、NCPOが中立化を伴うNHORPOよりも自動化に適していると主張している。中立化は、記号的なパラメータに依存する変換された項の複雑な構文解析を必要とするため、SMTエンコーディングが困難であるが、NCPOのパラメータ（優先順位、型順序、ステータス）はより直接的にエンコードできる。

結果
著者らは、Hasmtlibパッケージを用いて停止性問題をSMT-LIB 2形式にエンコードし、Z3ソルバーを用いて解くHaskellによるNCPOのプロトタイプを実装した。実験結果（表1）では、NCPOを、中立化の有無を含むNHORPO、およびWANDAやCSI$^{ho}$におけるHORPOの実装と比較している。

• NHORPOに対する優位性： NCPOは、NHORPO（中立化を使用した場合でも）が失敗するいくつかのシステムに対して、停止性を証明することに成功した。具体的には：
  • 例8（リストのインクリメント）： NCPOは、NHORPOにはない機能であるスモール記号を用いて停止性を証明する。
  • 例7（否定標準形）： NCPOは、到達可能な部分項を用いて停止性を証明するが、中立化を用いたNHORPOは、比較において汎用項を扱えないために規則の方向付けに失敗する。
• 比較不能な能力： 本研究は、中立化を用いたNHORPOは成功するがNCPOは失敗するケース（例：neutr.p）を特定しており、両者のアプローチが比較不能な能力を持っていることを示している。
• 効率性： NCPOのパラメータ探索は計算効率が高く、多くの場合、NHORPOの探索と同等の時間を要する一方で、中立化のパラメータ探索は複雑さが爆発することが示されている。

意義と主張
本論文は、NCPOがNHORPOと中立化の組み合わせに対する、強力かつ軽量な代替案を提供すると主張している。著者らは、中立化を用いたNHORPOは強力な競合相手ではあるものの、中立化技術の自動化に伴う複雑さを考慮すると、NCPOの方が自動的なノーマル高階書き換えの停止性証明において、より実用的な選択肢であると強調している。

著者らは、CPOおよびNHORPOにおける$\beta$簡約の包含が非推移性を正当化していることから、NCPOの推移性は依然として未解決の問題であると謙虚に述べており、NCPOの具体的な特性についてはさらなる調査が必要であるとしている。また、NCPOをノーマル高階書き換えのための依存ペア技術へと統合することが論理的な次のステップであると示唆している。最後に、特定の例がNHORPOによって解決可能であるという誤った主張を含む、先行文献に見られるエラーを避けるために、高階停止手法の形式化が必要であることを強調して締めくくっている。