ラムダ計算と Calculus of Constructions の定義解説
この記事は、以下の動画群の内容をより厳密になるように書き直したものです。動画ではかみ砕いた表現を使い、厳密さを欠くかわりにとっつきやすい解説をしています。
https://youtube.com/playlist?list=PLJucEMNgEA4mK12iTTer1nV1jWaTvCKMo
導入
ラムダ計算は、計算を｢純粋な関数への適用｣のみによって記述する計算模型です。これに型という概念を導入したものを型付きラムダ計算と呼びます。カリー＝ハワード同型対応の存在により、型付きラムダ計算を使って証明を構成的に記述することができます。これには次のようなメリットがあります。
- 完全に構成的で、言葉の曖昧さがない
- コンピュータによる型チェックを通して、理論の飛躍や破綻がないことを保証できる
- 証明をアルゴリズムとして再解釈でき、実行できる
この記事では、型付きラムダ計算の一種で豊富な表現力を持つCalculus of Constructions (CoC)の定義を解説します。
構文
CoCで扱う唯一の数学的対象は項です。項はラムダ抽象、積、適用、変数、宇宙のどれかであると定義されます(厳密な定義は後に示します)。
厳密さを欠きますが、それぞれの項は一般的な数学で用いられる概念と次のように対応しています。
| 名称 | ラムダ計算の表記 | 対応する概念 | 一般的な数学の表記 |
|---|---|---|---|
| ラムダ抽象 | $λx:P. ~ Q$ | 関数定義 | $f(x) := Q ~ (x \in P)$ |
| 積 | $[x: P] ~ Q$ | 関数の型 | $P → Q$ |
| 適用 | $A ~ B$ | 関数の使用 | $A(B)$ |
| 変数 | $x$ | 変数 | $x$ |
| 宇宙 | $*$ | すべての集合のクラス | $\text{Set}$ |
ラムダ抽象(lambda abstraction)は $λx:P. ~ Q$ のように書かれ、関数を表します。変数$x$を導入することを明示する目的で$x$を束縛する(bind)ラムダ抽象と言うこともあります。ここで、$P$は$x$の型(type)であり、$x$に代入できる値の種類を決定するもので、厳密には集合とは異なります。また、ラムダ抽象は右結合です。すなわち、 $λx:P. ~ λy:Q. ~ x ~ y$ と書いた場合は $λx:P. ~ (λy:Q. ~ (x ~ y))$ を意味します。
積(product)は $[x:P] ~ Q$ のように書かれ、主に関数の型を表します。直観的には関数や写像の種類を表す $P→Q$ と同じ意味ですが、積は$Q$の中で変数$x$を使ってもよいという点で、$→$よりも広い対象を表現できます。積もラムダ抽象と同じく右結合であり、変数を指して｢束縛する｣という表現を使うことがあります。
適用(application)は $A ~ B$ のように書かれ、$A$を関数と見た場合にそれを｢呼び出す｣操作を表します。ラムダ計算では乗算などの演算が定義されないため、これは $A × B$ を表すものではないことに注意して下さい。また適用は左結合であり、 $A ~ B ~ C = (A ~ B) ~ C$ です。
変数(variables)は名前通り変数で、ラムダ抽象または積によって導入され、上記式の $Q$ の中で使えるようになります。変数の名前は本質的に無意味であり、それを導入したラムダ抽象または積への参照だと考えてください。
最後に、宇宙(universe)は$*$と書き、全ての型の型として機能します(ただし、$*$自身の型は$*$ではありません)。$*$を読む際は一般に type と読みます。
項は文脈(context)とオブジェクト(object)の2種類に分類されます。
全ての文脈の集合 $\Lambda_o$ を、次のように帰納的に定義します。
$$ \begin{align} \tag{宇宙} * &\in \Lambda_o \\ \tag{量化} [x: T]\Delta &\in \Lambda_o \quad \text{where} \quad T \in \Lambda , ~ \Delta \in \Lambda_o \end{align} $$
全てのオブジェクトの集合 $\Lambda_i$ を、次のように帰納的に定義します。
$$ \begin{align} \tag{変数} x &\in \Lambda_i \\ \tag{積} [x: T] ~ A &\in \Lambda_i \quad \text{where} \quad T \in \Lambda , ~ A \in \Lambda_i \\ \tag{ラムダ抽象} λx: T. ~ A &\in \Lambda_i \quad \text{where} \quad T \in \Lambda , ~ A \in \Lambda_i \\ \tag{適用} A ~ B &\in \Lambda_i \quad \text{where} \quad A,B \in \Lambda_i \end{align} $$
全ての項の集合 $\Lambda$ は、上記2つの和集合です。
$$ \Lambda = \Lambda_o \cup \Lambda_i $$
以降の文では、汎用的な変数として$\Gamma, \Delta$は文脈を、$A, B, P, Q$はオブジェクトを、$T, U, V$はそのどちらかまたは両方を表すものとして使います。
文脈の解釈と演算
定義より、文脈は常に
$$ \Gamma = [x_1:T_1][x_2:T_2]...[x_n:T_n]* $$
という形で表され、これは変数と型の0個以上のリストとみなすことができます。この中に特定の変数$x_i$が含まれていて($x_i$を束縛していて)その型が$T_i$であることを $[x_i: T_i] \in \Gamma$ と書くことにします。
任意の文脈 $\Gamma = [x_1:T_1][x_2:T_2]...[x_n:T_n]*$ と項$U$について、文脈の付加 $\Gamma[k: U]$ を次のように定義します。
$$ \Gamma[k: U] = [x_1:T_1][x_2:T_2]...[x_n:T_n][k:U]* $$
直観的には、文脈の付加は$\Gamma$の末尾にある$*$を$[k:U]*$に置き換える操作です。
文脈にはいくつかの意味があります。項を解釈する際に｢既に分かっている変数のリスト｣を表す文脈としての意味のほか、型多相、命題や述語の型を表すのにも使われます。
オブジェクトの解釈
オブジェクトは、論理命題やその証明、関数などを表すのに使われます。CoCは抽象的な計算模型であるため、証明に使う操作(自然演繹)と関数の操作の両方に対して同じ構文を使います。
例えば、 $[x:T] ~ U$ は論理命題 $T ⇒ U$ 、 $λx: T. ~ A$ はその証明であり、これは$T$という仮定のもとで命題$U$の証明$A$を与えているものと解釈できます。従って $[x:T] ~ U$ は全称量化 $∀x:T. ~ U$ だと考えられます。しかし依然として(関数の型を内包する)積 $\Pi x:T. ~ U$ としての意味も持ちます。CoCでは、仮定の導入にも関数の型にも共通した $[x: T] ~ U$ という表記を与えています。
同様に、 $A ~ B$ という表記はモーダス・ポネンス(論理学の用語で $(P ⇒ Q) ∧ P ⊢ Q$ のこと)と関数適用の両方に使われます。
判断
はじめに、判断(judgement)の記号 $\Gamma ⊢ J$ を導入します。これは文脈 $\Gamma$ のもとで判断$J$が有効であることを表しています。ここで、$\Gamma$は文脈であり、$J$は以下で定義されるいずれかの判断です。
$$ J = \begin{cases} \Delta \quad & \text{(文脈)} \\ A : T \quad & \text{(型判断)} \\ A ≅ B \quad & \text{(同型)} \end{cases} $$
また、以下では直観主義論理などで使われる表記$\dfrac{\alpha}{\beta}$を使います。これは$\alpha ⇒ \beta$と同じ意味です。
文脈と型の判断
ある文脈$\Gamma$のもとで別の文脈$\Delta$が有効であることを$\Gamma ⊢ \Delta$と表します。これは次の規則によって与えられます。
$$ * ⊢ * $$
$$ \dfrac{\Gamma ⊢ \Delta}{\Gamma[x: \Delta] ⊢ *} $$
$$ \dfrac{\Gamma ⊢ A : *}{\Gamma[x: A] ⊢ *} $$
$$ \dfrac{\Gamma[x: T] ⊢ \Delta}{\Gamma ⊢ [x: T]\Delta} $$
$\Gamma ⊢ *$ は文脈$\Gamma$自体が有効であることも同時に表しています。
ある文脈$\Gamma$のもとで$A$が$T$によって有効に型付けされることを $\Gamma ⊢ A : T$ と表します。これは次の規則によって与えられます。
$$ \tag{積} \dfrac{\Gamma[x: T] ⊢ A : * }{\Gamma ⊢ [x: T] ~ A : * } $$
$$ \tag{変数} \dfrac{\Gamma ⊢ *}{\Gamma ⊢ x : T} \quad ([x:T] \in \Gamma) $$
$$ \tag{ラムダ抽象} \dfrac{\Gamma[x: T] ⊢ A : U}{\Gamma ⊢ (λx:T. ~ A) : [x: T] ~ U} $$
$$ \tag{適用} \dfrac{\Gamma ⊢ A: [x: T] ~ U \quad \Gamma ⊢ B : T}{\Gamma ⊢ A ~ B : [B/x]U} $$
$$ \tag{同型} \dfrac{\Gamma ⊢ A : T \quad \Gamma ⊢ T ≅ U}{\Gamma ⊢ A : U} $$
ここで $[B/x]U$ という表記は、$U$の中にある変数$x$に$B$を代入して得られる項を表します。
適用の規則では、$A$と$B$の型に共通して$T$が現れます。これは$A$の型の一部と$B$の型が"同じ"でなければならないことを表します。この｢同じ｣の判断は、次に示す同型の規則によって与えられます。
同型判断
ある文脈$\Gamma$のもとで$T$と$U$が"同じ"と判断できることを $\Gamma ⊢ T ≅ U$ と表します。これは次の規則によって与えられます。
$$ \dfrac{\Gamma[x: T] ⊢ A : U \quad \Gamma ⊢ B : T}{\Gamma ⊢ (λx: T. ~ A) ~ B ≅ [B/x]A} $$
この規則は、｢β簡約(後述)しても同型である｣ことを表しており、同型規則の本質です。残りの規則は、｢同型なもの同士から構成されるものは同型である｣ことを表しています。
$$ \dfrac{\Gamma ⊢ \Delta}{\Gamma ⊢ \Delta ≅ \Delta} $$
$$ \dfrac{\Gamma ⊢ A : T}{\Gamma ⊢ A ≅ A} $$
$$ \dfrac{\Gamma ⊢ T ≅ U}{\Gamma ⊢ U ≅ T} $$
$$ \dfrac{\Gamma ⊢ T ≅ U \quad \Gamma ⊢ U ≅ V}{\Gamma ⊢ T ≅ V} $$
$$ \dfrac{\Gamma ⊢ T ≅ T' \quad \Gamma[x: T] ⊢ A ≅ A'}{\Gamma ⊢ [x: T]A ≅ [x: T']A'} $$
$$ \dfrac{\Gamma[x: T] ⊢ A : U \quad \Gamma ⊢ T ≅ T' \quad \Gamma[x: T] ⊢ A ≅ A'}{\Gamma ⊢ λx: T. ~ A ≅ λx: T'. ~ A'} $$
$$ \dfrac{\Gamma ⊢ A ~ B : T \quad \Gamma ⊢ A ≅ A'}{\Gamma ⊢ A ~ B ≅ A' ~ B} $$
$$ \dfrac{\Gamma ⊢ A ~ B : T \quad \Gamma ⊢ B ≅ B'}{\Gamma ⊢ A ~ B ≅ A ~ B'} $$
同型の規則に従ってある項 $(λx: T. ~ A) ~ B$ をそれと同型な項 $[B/x]A$ に変形することをβ簡約と言い、
$$ (λx: T. ~ A) ~ B \xrightarrow{β} [B/x]A $$
と表します。項の一部分にのみ上記の変形が可能な場合も同様にβ簡約と言います。
β簡約は、CoCの項をプログラムだと解釈する場合に唯一可能な｢実行｣の操作だと考えることができます。
おわりに(定義ではない解説)
コンピュータによる型チェック
｢コンピュータによる型チェック｣では、上記規則を使ってある項が正しく構築されているかをチェックします。規則にない項の使い方をしている場合、それは不正な項です。例えば、項の中に現れる適用は常に適用の型付け規則
$$ \dfrac{\Gamma ⊢ A: [x: T] ~ U \quad \Gamma ⊢ B : T}{\Gamma ⊢ A ~ B : [B/x]U} $$
に適合するように型付けされていなければなりません。正しく構築された項は｢破綻のない証明｣であり｢正しさが保証されたプログラム｣でもあります。
結局何ができるものなのか
コンピュータに型チェックという形で助けてもらいながら証明を書くことができます。型チェックの実装に必要な情報はこの記事の内容で完全に与えられており、それほど大きなプログラムを必要としません(つまり、型をチェックする側に間違いが起きにくい)。
CoCを使って証明を書くことで、人間が文で証明を書く時にありがちな間違いのチェックを一部自動化することができ、広く採用されれば数学の進化スピードを上げることにも繋がると思います。