論文「Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation」の技術的サマリー

1. 概要と背景

この論文は、ラムダ計算における**証明関連性（proof-relevant）を持つクリエーグ補間定理（Craig Interpolation Theorem）**の再検討と、その形式化を扱っています。著者らは、Čubrić による単純型付きラムダ計算（和型と空型を含む、STLC+）における補間定理の証明を、**双方向型付け（bidirectional typing）**の原理に基づいて再構築し、証明支援系 Rocq（Coq の新世代）を用いて形式化しました。

従来の補間定理は、論理的帰結 $A \vdash B$ が、$A$ と $B$ の共通の概念のみを用いた中間式 $I$ を介して $A \vdash I \vdash B$ と分解できることを示すものでしたが、証明関連性のバージョンでは、単に式だけでなく**証明項（proof terms）**の分解も保証します。すなわち、証明項 $t$ が $A \vdash B$ を証明している場合、$A \vdash u : I$ および $I \vdash v : B$ となる証明項 $u, v$ を構成でき、これらを合成したものが元の $t$ と等価（または $\beta$-正規化により等価）になることを示します。

2. 問題設定

従来の証明の課題

Čubrić の元の証明は、項のサイズに関する帰納法を用いており、部分項を徐々に変数に置き換えるという手法でした。しかし、この証明には以下の問題点がありました：

1. 複雑さと美しさの欠如: 証明の核心部分が複雑で、特に「前の場合と同じ」として処理されたケース（Subcase 6.3.2）が実際には類似していなかったなど、厳密性に欠ける部分がありました。
2. 和型（Sum Types）の扱い: 和型や空型を含む場合、単なる $\beta$-正規形だけでは「部分式性（subformula property）」を満たさないため、補間証明が機能しません。
3. 形式化の困難さ: 従来の証明は形式化が困難であり、特に和型を含むラムダ計算の正規化理論の形式化は未着手でした。

双方向型付けとの関係

双方向型付けは、型推論（inference）と型検査（checking）を区別する手法ですが、これと「部分式性」や「正規形」の関係は以前から指摘されていました。しかし、和型がある場合、双方向型付けが部分式性を満たす正規形と一致するかどうかは議論の余地がありました。著者らは、この関係が和型を含む場合でも成り立つことを明確に示す必要があります。

3. 手法とアプローチ

著者らは、以下のステップで新しい証明と形式化を構築しました。

3.1 双方向型付けによる正規形の記述

STLC+ における正規形（normal forms）と中立項（neutral forms）を、双方向型付けシステムを用いて帰納的に記述しました。

• 推論（Inference, $\triangleright$）: 項から型を推論する（中立項や変数、部分項の推論結果など）。
• 検査（Checking, $\triangleleft$）: 項が特定の型を持つことを確認する（構成子や $\lambda$ 抽象、部分式性を持つ項など）。
• 部分式性の確保: この双方向システムは、証明項が「部分式性」を満たすように設計されており、これが補間定理の証明の基盤となります。

3.2 可換変換（Commuting Conversions）の導入

和型や空型を含む場合、$\beta$-正規化だけでは不十分です。著者らは**可換変換（commuting conversions）**と呼ばれる規則を導入し、これによる正規化を扱いました。

• 例：$\langle \text{if}(s, b_l, b_r) \mid e \rangle \leadsto \text{if}(s, \langle b_l \mid e \rangle, \langle b_r \mid e \rangle)$
• これにより、消去子（eliminator）が正の型（和型や空型）の上で移動し、部分式性を維持した正規形のクラスが得られます。

3.3 論理関係（Logical Relations）による正規化定理の証明

すべての型付き項が正規形に帰着することを示すため、論理関係を用いた証明を行いました。

• 値（Values）と被覆（Covering）: 正の型（和型、空型）における項の構造を捉えるために「被覆（covering）」の概念を導入し、項が「中立項による被覆」を持つことを定義しました。
• 再帰的定義: 負の型（関数型、積型）では通常の正規形、正の型では「被覆された項」を値として定義し、これらが正規化の目標となることを示しました。
• Rocq による形式化: この論理関係に基づく正規化定理（Normalisation）を Rocq で初めて形式化しました。

3.4 補間定理の証明

正規形と双方向型付けの構造を利用して、補間定理を証明しました。

• 文脈の分割（Context Partition）: 証明の帰納法において、文脈 $\Gamma$ を「ソース側（$\Gamma_s$）」と「ターゲット側（$\Gamma_t$）」に分割し、補間項が両者の共通語彙のみを使用することを追跡します。
• 相互帰納法: 正規項（Normal forms）と中立項（Neutral forms）に対して相互帰納法を用いて証明を行います。これにより、Čubrić の元の証明よりも直感的で形式化しやすい構造を得ました。
• 定数と方程式の一般化: 定数や任意の方程式を含む言語に対しても定理が拡張可能であることを示しました。

4. 主要な貢献と結果

1. 証明の再構築と簡素化:

   • Čubrić の証明を、双方向型付けに基づく帰納的な構造に再構築しました。これにより、証明がより明確になり、形式化が容易になりました。
   • 和型を含む場合の「部分式性」と「双方向型付け」の関係を明確化し、和型があっても双方向型付けが部分式性を捉えることを示しました。

2. Rocq による形式化:

   • STLC+ のメタ理論（型付け、簡約、正規化定理）を Rocq で初めて形式化しました。
   • 可換変換を含む正規化定理の形式化: 和型と可換変換を含む計算体系の正規化定理を形式化したのは、これが初めてです。
   • 形式化コードは約 4,000 行（AutoSubst 生成コード 800 行含む）で、既存の補間定理の形式化（例：Férée et al. の 10 倍の規模）と比較して非常にコンパクトです。

3. 証明関連補間（Proof-Relevant Interpolation）の確立:

   • 項 $t$ が $A \vdash B$ を証明している場合、共通語彙のみを持つ型 $I$ と、$A \vdash u : I$、$I \vdash v : B$ となる項 $u, v$ を構成し、$(\lambda y. v) u \leadsto^* t$ が成り立つことを示しました。
   • 定数を含む場合や、文脈の分割を考慮した一般化された定理を提示しました。

4. 自動化ツールの利用と課題:

   • 置換計算の処理には AutoSubst2-OCaml を、型付けの証明には Rocq の証明探索機能（Hint database）や Std++ の集合論ソルバーを多用しました。
   • 置換方程式の完全性や速度に関する課題に直面しましたが、これらを克服することで形式化を完了しました。

5. 意義と将来展望

• 理論的意義: 証明関連性を持つ補間定理が、単なる論理式の話ではなく、計算（証明項）の構造と密接に関係していることを示しました。また、双方向型付けが部分式性を自然に捉えるメカニズムであることを再確認しました。
• 実用的意義: 形式化されたメタ理論は、他の型理論や論理体系への拡張の基盤となります。特に、Rocq での実装は、依存型理論やより複雑な論理系への応用への道を開きます。
• 将来の課題:
  • 非正規項への拡張: 現在の定理は正規項に限定されています。赤子（redex）を含む項に対しても、カット公式の語彙制約を満たす限り補間が可能かどうかの検討。
  • 一様補間（Uniform Interpolation）: 特定の証明に依存せず、型のみから補間項を生成する「一様」な証明関連補間の確立。
  • 依存型理論への拡張: 依存型理論では可換変換が型付けされない場合があるため、その克服と定理の拡張。

この論文は、ラムダ計算の補間定理に関する古典的な結果を、現代の形式化技術と双方向型付けの知見を融合させることで、より堅牢で拡張可能な形で再構築した重要な業績です。