Towards an HRS Category in TermCOMP

技術要約：TermCOMPにおけるHRSカテゴリに向けて

問題提起
年次開催のTermination Competition (TermCOMP) には、高階書き換え（higher-order rewriting）のためのカテゴリが含まれている。歴史的に、このカテゴリは、プレーンなマッチングと明示的な $\beta$-簡約ルールに依存する代数関数系 (Algebraic Functional Systems; AFSs) の意味論を利用してきた。一方、$\beta\eta$ モジュロでの書き換えを行い、通常は Miller のパターン (PRSs) や、より新しい決定論的高階パターン書き換えシステム (DPRSs) を用いる Nipkow の高階書き換えシステム (HRSs) は確立された形式体系であるが、これらは TermCOMP の競争フレームワークに完全には統合されていない。課題は、HRS の意味論 ($\beta\eta$ モジュロでの書き換え) を、既存の TermCOMP フレームワーク (AFSs およびメタ置換に基づく) とどのように整合させ、HRS を対象とするツールが AFSs を対象とするツールと直接競い合えるようにするかにある。

手法
著者らは、HRS と現在の TermCOMP 高階意味論（Simply-Typed Meta-Substitution Rewrite Systems; STMRSs として定義される）との間の形式的な架け橋を提案している。その手法は、主に以下の3つのステップで構成される：

1. パターンの一般化： 著者らは、PRS と DPRSs の両方を一般化する Extended Pattern Rewrite Systems (EPRSs) を導入する。EPRSs は「拡張パターン (Extended Patterns; EPATs)」を利用し、DPRSs の決定論的なマッチング制約を緩和しつつ、自由変数が非抽象引数に適用されるという構造を維持している。このクラスは、スタンドアロンの実際的なツールとしてではなく、主に理論的証明を容易にするために定義されている。
2. STMRS 意味論の拡張： 著者らは、左辺が標準的なパターンではなく EPATs であることを許容するように、STMRS ルールの定義（現在の TermCOMP 標準）を拡張する。著者らは、「well-behaved（良好な）」および「quasi-well-behaved（準良好な）」項という概念を導入する。これらの構文的制限は、メタ置換が適用された際に、結果となる項が $\beta$-正規形（具体的には $\beta\eta$-long 正規形）に留まり、追加の簡約ステップを必要とする新たな $\beta$-redex を生成しないことを保証するものである。
3. 正規化書き換えによる実装： 中心となる技術的貢献は、well-behaved な STMRS における書き換えが、対応する EPRS における書き換えをシミュレートすることを確立することである。著者らは、通常の置換（EPRSs で使用される）とメタ置換（STMRSs で使用される）の間の翻訳を定義し、これら2つのシステムが停止性に関して等価であることを証明する。

主要な貢献

• EPRSs の定義： DPRSs を一般化し、管理可能なマッチング特性を保持しながら、より広範なベンチマークを許容する、HRS の新しい構文的サブクラス。
• 等価性のための構文的制限： 「well-behaved」な STMRS ルールの導入。これらのルールは、左辺が well-behaved であり、右辺が quasi-well-behaved であることを制限する。これにより、メタ置換の適用が $\beta$-redex を作成しないことが保証され、項の $\beta$-正規形が保持される。
• 形式的等価性定理： 著者らは、well-behaved な STMRS $R$ と項 $s$（$\beta\eta$-long 正規形）に対して、EPRS の意味論における書き換えステップ ($s \to_R t$) が起こることは、STMRS の意味論における書き換えステップとその後の $\beta$-正規化 ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$) が起こることと同値であることを証明する。

結果
主要な結果は、well-behaved な STMRSs とそれに対応する EPRSs の書き換え関係の対応関係を確立する Theorem 15 である。具体的には：

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ であることは、$s \to_R t$ （$R$ を EPRS として見る）であることと同値である。
• これは Corollary 20 につながり、well-behaved な STMRS における戦略「書き換え、その後に $\beta$-正規化を行う」の停止性は、対応する EPRS の普遍的な停止性と一致することを述べている。

著者らは、この等価性が $\beta\eta$-long 正規形にある項に対して成立することを示している。また、二階 STMRS においては、この対応関係はさらに強く、メタ置換が $\beta$-redex を作成できないため、ステップ間の一対一のマッピングを提供すると指摘している。

意義
本論文は、TermCOMP における HRS (サブ) カテゴリの形式的な基礎を築くものであると主張している。既存の TPDB フォーマット内で、構文的にチェック可能なベンチマークのサブセット（well-behaved な STMRSs）を定義することにより、著者らは以下を可能にした：

1. 直接的な競争： HRS（$\beta\eta$-書き換えを使用）向けに設計されたツールが、提案された意味論の下で停止性が一致することが証明されているため、同一のカテゴリ内で AFSs 向けに設計されたツールと直接競い合うことができる。
2. より広範なツールサポート： 実装結果により、単なるグローバルな停止性だけでなく、ステップごとの対応関係に基づいたシミュレーションに基づいているため、停止性以外の性質の比較も可能になる。
3. 既存研究の洗練： この結果は、AFSMs における PRSs（Kop）や組合せ体系（van Oostrom および van Raamsdonk）の実装を、より一般的なクラスの HRSs (EPRSs) へと拡張し、正規化書き換えと高階書き換えの等価性に関する厳密な証明を提供することで、それらを強化するものである。

著者らは、メタ置換は完全な高階置換よりも厳密に弱いため、この結果が すべての HRSs をカバーするわけではないことを認め、その範囲について謙虚な姿勢を保っている。しかし、定義されたサブクラスは、既存のベンチマークの大部分および彼らの先行研究で導入された特定の DPRSs を収容するのに十分であると主張している。