Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

技術要約：単純型定数領域様式ラムダ計算 I：距離付きベータ簡約と組合せ論理

1. 問題と動機
本論文は、様式論理（modal logic）と型付きラムダ計算の形式的な統合における空白を扱うものである。リチャード・モンタギューとダナ・ガリンは、これらの分野を統合する体系を開発したが、彼らの研究はチャーチの単純型理論（恒等性と量化を含む）に依存しており、状態変数（state variables）の扱いに限定性があった。現代の型付きラムダ計算、特に単純型ラムダ計算（STLC）は、コンピュータサイエンスや言語学の標準的な基礎理論であるが、現代的な意味解析に必要な特定の様式的特徴（複数の状態変数の存在や内包的コンテキストなど）を欠いている。

著者のショーン・ウォルシュは、既存の枠組みにおける2つの主要な欠陥を特定している：

1. 強すぎる点： モンタギューの体系は、チャーチの単純型理論の全リソースを仮定しているため、現代的な応用においては「強すぎる」。一方で、現代のシステムはSTLCのようなより弱い基礎理論を利用することが多い。
2. 弱すぎる点： モンタギューの体系は様式的表現力に関して「弱すぎる」。すなわち、二次元意味論、現実化演算子（actuality operators）、および単一の式内における複数の異なる状態変数の束縛メカニズムを欠いている。

本論文の目的は、様式論理を単純型ラムダ計算と統合した体系である $\lambda\theta$ を開発することによって、この問題を解決することである。中心となる課題は、$\lambda\theta$ の「有限変数」的な性質である。本体系は、各状態型に対して利用可能な変数の数を制御するパラメータ $\theta$ によって、利用可能な変数の数を制限している。この制限により、標準的な $\alpha$-変換の手法を用いて束縛変数をキャプチャせずに名前を変更するための変数が不足する場合、完全性を証明するための標準的な開項モデル（open term models）の使用が不可能になる。

2. 方法論と核となる定義
本論文は、$\theta$ によってパラメータ化された $\lambda\theta$ ファミリーを導入する。ここで $\theta$ は、各状態型を、その型に利用可能な変数の数（1から $\omega$ までの基数）へと写像する。

• 型（Types）： 状態型は関数型の余域になることはできない（すなわち、$A$ が状態型であるとき、$A \to B$ は型ではない）。これにより、状態型の項は厳密に変数または定数となる（命題 2.6）。
• 距離付きベータ簡約（Distanced Beta Reduction）： 新たな貢献は、「距離付き」ベータ簡約の定義である。引数がラムダ抽象に直接適用される標準的なベータ簡約とは異なり、距離付き簡約では、引数 $N$ をラムダ抽象 $\lambda v:A. L$ から一連の中間項 $\vec{M}$ によって分離することができる：
  $(\lambda \vec{x}: \vec{B}. \lambda v:A. L) \vec{M} N \to_\beta (\lambda \vec{x}: \vec{B}. L[v := N]) \vec{M}$
  このメカニズムは、標準的な $\alpha$-変換を実行して変数キャプチャを回避するための変数が不足している場合に、ラムダ抽象の下での簡約を行うために必要である。
• 組合せ論理の基礎： 本論文は、伝統的な SKI 基底ではなく、BCDKW 組合子（B, C, D, K, W）を中心とした組合せ論理の基礎を採用している。Dardinal ($D$) 組合子の包含は、この体系に特有のものであり、定数が関数に代入されるケースを処理する。

3. 主要な貢献と結果

• モデルの組合せ論的特徴付け (Theorem 1.1):
  本論文は、STLCに対するヘンキン・モデルのアンニューズによる特徴付けを様式の設定へと一般化する。フレームが $\lambda\theta$ のモデルであるための必要十分条件は、すべての BCDKW-組合せ項 の表示（denotations）が定義可能であることであることを証明する。この特徴付けは、非最大パラメータ（例：$\lambda_1$）において、$\alpha$-変換のための変数が不足しているために開項モデルが存在しないという問題を回避する（例 3.9）。

• 意味論的保存性と表現力 (Theorems 1.1 & 1.2):
  本論文は、最大系 $\lambda\omega$（すべての状態型について $\theta(A) = \omega$）と制限された系 $\lambda\theta$ の関係に関するツィンマーマン（Zimmermann, 1989）の問いを解決する。

  • 保存性（Conservation）： すべての $\lambda\theta$ のモデルは $\lambda\omega$ のモデルである。したがって、意味論的妥当性は保持される：$\lambda\theta \models M = N$ であることは、$\lambda\omega \models M = N$ であることと同値である。
  • 表現力（Expressibility）： 自由変数および定数が $\lambda\theta$ から抽出されている $\lambda\omega$ の任意の項は、同じ表示を持つ $\lambda\theta$ の項によって表現可能である。
    これらの結果は、「有限変数」の制限が標準的な意味論における表現力を制限しないこと、すなわち最大系は制限された系に対して保守的であることを示唆している。

• 様式および非様式体系間の演繹的関係 (Theorems 1.3 & 1.4):
  本論文は、様式系 $\lambda\omega$ と通常の非様式 STLC ($\lambda$) との関係を確立する。

  • 演繹的保存性： $\lambda\omega$ における項の $\beta\eta$-等価性は、$\lambda$ において成立する場合と同値である。
  • 演繹的表現力： 型および定数が $\lambda\omega$ と互換性のある $\lambda$ の項は、$\lambda\omega$ 内で表現可能である。
    これらの証明は、STLC の標準的な道具（Church-Rosser、強正規化）に依拠しており、比較的簡潔である。

• $\infty$-規則による完全性 (Theorem 1.6):
  $\lambda\theta$（非最大 $\theta$ の場合）は開項モデルを欠き、標準的な $\beta\eta$-簡約において Church-Rosser 性が成立しないため（例 2.26）、本論文は $\infty$-規則 を導入する。この規則は、$M \to_\infty N$ を、最大系 $\lambda\omega$ において $M =_{\beta\eta} N$ である場合に許可する。この規則を加えることで、$\lambda\theta$ はその意味論に対して演繹的に完全となる。

• 弱演繹的保存性 (Theorem 1.7):
  本論文は、簡約や等価性がラムダ抽象の下で保持されない（$\xi$-規則を持たない）「弱い」ラムダ計算を調査する。BCDKW 基底に基づく純粋な内包的組合せ論理（CL$\theta$）を用い、$\lambda\omega$ における弱い $\beta$-等価性が、$\lambda\theta$ における $\beta\eta$-等価へと保守的に拡張されることを証明する（ただし、シグネチャに状態型の定数が含まれない場合に限る）。この結果は、完全な展開（complete developments）を用いたタカハシの手法を用いて、弱組合せ論理の Church-Rosster 性を確立することに依拠している。

4. 意義と主張
本論文は、現代的な STLC のリソースを様式論理と統合した、「現代的な」単純型様式ラムダ計算の最初の徹底的な展開を提供すると主張している。その意義は以下の点にある：

1. ツィンマーマンの問いへの回答： 最大の様式系における表現力が、制限された有限変数設定においても（意味論的、および $\infty$-規則を用いて演繹的に）捕捉されることを概ね肯定している。
2. メタ理論的道具： 「距離付き $\beta$-簡約」と BCDKW 基底の組合せ論理を、変数の可用性が制限されたシステムを扱うための不可欠な道具として導入している。これは標準的な開項モデルの失敗を克服するものである。
3. 内包的意味論： 制限された系 $\lambda\theta$ が最大系 $\lambda\omega$ と意味論的に同値であることを示すことにより、型 $A \to B$ の項が内包的コンテキストにおいても手続きとして解釈され得るという見解を支持している。

本論文は明示的に限界についても述べている。すなわち、標準的な $\beta\eta$-規則のみを用いて $\lambda\theta$ の完全性定理を提供することはない（問い 4.17）こと、および、本体系は到達可能性関係（accessibility relations）のような解釈をそのまま表に出すわけではなく、それらをモデル化するために特定の型規則を必要とすることを認めている。随伴論文では、これらの結果をチャーチの単純型理論へと拡張している。