How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

技術的要約：「アコーディオンの弾き方：$\lambda$-計算の線形近似における一様性と（非）保存性」

問題提起
本論文は、EhrhardとRegnierによる微分$\lambda$-計算およびリソース計算の枠組みにおける、$\lambda$-計算の線形近似の**保存性（conservativity）**を調査している。テイラー展開 $T(M)$ が $\lambda$ 項 $M$ の $\beta$ 還元をシミュレートできること（すなわち、$M \to_\beta N$ ならば $T(M) \twoheadrightarrow_r T(N)$ であること）は確立されているが、逆の問い、すなわち「リソース計算における還元は、元の $\lambda$ 計算における実際の還元によって誘導されるのか？」という問いが残されている。

形式的には、リソース計算（無限のリソース項の無限線形結合を扱う）における還元 $T(M) \twoheadrightarrow_r T(N)$ が与えられたとき、$\beta$ 還元列 $M \to_\beta N$ が存在するかどうかを問うている。著者らは、以下の2つの設定を区別している：

1. 有限 $\lambda$-計算： 項は有限であり、還元は有限の系列である。
2. 無限 $\lambda$-計算 ($\lambda^{001}$)： 項は無限（共帰的）であり得、還元は無限の系列 ($\to^{001}_\beta$) となり得る（ただし、赤簡（redex）は深さが増すにつれて実行される）。

中心となる問題は、これらの設定において線形近似が元の計算の**保存的拡張（conservative extension）**であるかどうかである。

手法
著者らは、書き換え理論、共帰的定義、および「マッシュアップ（mashup）」技法（ソース項とそのリソース近似量を関連付ける手法）を組み合わせて用いている。

1. 有限ケースの解析： 有限の項に対して、著者らはKerinecとVaux Auclairによるマッシュアップ証明技法を適応させている。彼らは $\lambda$ 項とそのリソース近似量を結びつける関係 $\vdash$ を定義する。$T(M) \twoheadrightarrow_r T(N)$ ならば $M \vdash T(N)$ であり、さらに $M \vdash T(N)$ が $M \to^*_\beta N$ を含意することを証明することで、有限ケースにおける保存性を確立する。
2. 無限の反例（アコーディオン）： 無限の設定に対処するため、著者らは特定の反例である**アコーディオン（Accordion, $A$）**を構成している。この項は、その構造を「引き伸ばし（stretch）」、「圧縮（compress）」する無限の還元系列をシミュレートするように設計されている。
   • 項 $A$ は、無限項 $\bar{A} = (\langle T \rangle)(\langle F \rangle)\omega$ を近似する一連の項へと還元される。
   • 極めて重要な点として、$T(A) \twoheadrightarrow_r T(\bar{A})$ は成立するものの、著者らは有効な無限 $\beta$ 還元 $A \to^{001}_\beta \bar{A}$ は存在しないことを証明している。$A$ の還元パスは、無限 $\beta$ 還元の要件である層化条件（Lemma 2.5）に違反する、限定された深さでの「グローバル」なステップを必要とするためである。
3. 一様性とコヒーレンス： 無限の設定において保存性を回復するために、著者らはEhrhardとRegnierの著作において中心的な概念であった一様性（uniformity）を導入する。彼らはリソース項に対するコヒーレンス関係 ($\bowtie$) を定義し、還元関係を一様和（uniform sums）（すべての要素が互いにペアごとにコヒーレントである和）に制限する。
   • 彼らは、一様リソース還元 ($\to^{\curvearrowright}_r$) とその無限閉包 ($\to^{\curvearrowright \infty}_r$) を定義する。
   • この制限により、リソース計算における還元は、実際の $\beta$ 還元に厳密に対応するようになり、ソース計算に対応しない「非一様」なパスが排除される。
4. $\beta_\perp$ への拡張： 著者らはこれらの結果を $\beta_\perp$ 還元（未定義の項を $\bot$ に崩壊させる還元）へと拡張し、一様性が $\bot$ 還元を含む場合でも保存性を維持することを示す。

主な貢献

1. 有限項に対する保存性： 線形近似が有限 $\lambda$ 計算に対して保存的であることを示す厳密な証明を提供した（Theorem 3.1）。
2. 無限項に対する非保存性： 標準的な点別リソース還元 ($\twoheadrightarrow_r$) が無限 $\lambda$ 計算に対して非保存的であることを示した。著者らはアコーディオン項 $A$ という反例を構築し、$T(A) \twoheadrightarrow_r T(\bar{A})$ が $A \to^{001}_\beta \bar{A}$ を含意しないことを証明した（Theorem 4.4）。
3. 一様性による回復： 著者らは、一様性が無限の設定における保存性を回復するために必要な欠けていた要素であることを特定した。リソース計算を一様還元 ($\to^{\curvearrowright \infty}_r$) に制限することで、線形近似が無限 $\lambda$ 計算の保存的拡張になることを証明した（Theorem 5.10）。
4. $\beta_\perp$ への拡張： これらの結果を $\beta_\perp$ 還元へと一般化し、一様アプローチが $\bot$ 還元を含む還元を正しくシミュレートし、保存することを示した（Theorem 5.18 および 5.19）。

結果

• 有限の設定： リソース還元による有限 $\beta$ 還元のシミュレーションは保存的である。
• 無限の設定（標準）： 標準的な点別リソース還元による無限 $\beta$ 還道のシミュレーションは非保存的である。アコーディオン項 $A$ はリソース計算において $\bar{A}$ へと還元されるが、$\lambda$ 計算においてはならない。
• 無限の設定（一様）： 一様リソース還元による無限 $\beta$ 還元のシミュレーションは保存的である。
• $\beta_\perp$ 設定： 非保存性は $\beta_\perp$ 還元にも及び、一方で一様還元は $\beta_\perp$ に対しても保存的である。

意義
本論文は、線形近似が $\lambda$ 計算のダイナミクスを忠実なモデルとして機能するための正確な条件を明らかにしている。これは、量的な線形近似が無限の設定において非保存的であるという、第一著者の博士論文における予想を解決するものである。

主要な意義は、一様性が単なるテイラー展開の意味論的特性であるだけでなく、保存性を確保するために必要な、還元関係そのものに対する構文的な制約であることを特定した点にある。この制限がなければ、リソース計算は、特に無限項が存在する場合に、ソース計算に対応するものを持たない「ゴースト」の還元を許容してしまう。本研究は、「正規化は近似と可換である」という交換定理（commutation theorem）の理解を精緻化し、シミュレーションと保存性の違いを明確にすることで、シミュレーションは一般に成立するものの、保存性にはより厳格な一様フレームワークが必要であることを示した。

著者らは、反例と一様性の結果に対する完全な証明を提供し、さらに $\beta_\perp$ 還元への拡張（これは項をそのベーム木（Böhm tree）に関連付ける上で極めて重要である）を行うことで、以前の会議版の成果を改善していると明言している。