この記事は、以下の動画群の内容をより厳密になるように書き直したものです。動画ではかみ砕いた表現を使い、厳密さを欠くかわりにとっつきやすい解説をしています。
https://youtube.com/playlist?list=PLJucEMNgEA4mK12iTTer1nV1jWaTvCKMo
ラムダ計算は、計算を「純粋な関数への適用」のみによって記述する計算模型です。これに型という概念を導入したものを型付きラムダ計算と呼びます。カリー=ハワード同型対応の存在により、型付きラムダ計算を使って証明を構成的に記述することができます。これには次のようなメリットがあります。
この記事では、型付きラムダ計算の一種で豊富な表現力を持つCalculus of Constructions (CoC)の定義を解説します。
CoCで扱う唯一の数学的対象は項です。項はラムダ抽象、積、適用、変数、宇宙のどれかであると定義されます(厳密な定義は後に示します)。
厳密さを欠きますが、それぞれの項は一般的な数学で用いられる概念と次のように対応しています。
名称 | ラムダ計算の表記 | 対応する概念 | 一般的な数学の表記 |
---|---|---|---|
ラムダ抽象 | 関数定義 | ||
積 | 関数の型 | ||
適用 | 関数の使用 | ||
変数 | 変数 | ||
宇宙 | すべての集合のクラス |
ラムダ抽象(lambda abstraction)は
積(product)は
適用(application)は
変数(variables)は名前通り変数で、ラムダ抽象または積によって導入され、上記式の
最後に、宇宙(universe)は
項は文脈(context)とオブジェクト(object)の2種類に分類されます。
全ての文脈の集合
全てのオブジェクトの集合
全ての項の集合
以降の文では、汎用的な変数として
定義より、文脈は常に
という形で表され、これは変数と型の0個以上のリストとみなすことができます。この中に特定の変数
任意の文脈
直観的には、文脈の付加は
文脈にはいくつかの意味があります。項を解釈する際に「既に分かっている変数のリスト」を表す文脈としての意味のほか、型多相、命題や述語の型を表すのにも使われます。
オブジェクトは、論理命題やその証明、関数などを表すのに使われます。CoCは抽象的な計算模型であるため、証明に使う操作(自然演繹)と関数の操作の両方に対して同じ構文を使います。
例えば、
同様に、
はじめに、判断(judgement)の記号
また、以下では直観主義論理などで使われる表記
ある文脈
ある文脈
ここで
適用の規則では、
ある文脈
この規則は、「β簡約(後述)しても同型である」ことを表しており、同型規則の本質です。残りの規則は、「同型なもの同士から構成されるものは同型である」ことを表しています。
同型の規則に従ってある項
と表します。項の一部分にのみ上記の変形が可能な場合も同様にβ簡約と言います。
β簡約は、CoCの項をプログラムだと解釈する場合に唯一可能な「実行」の操作だと考えることができます。
「コンピュータによる型チェック」では、上記規則を使ってある項が正しく構築されているかをチェックします。規則にない項の使い方をしている場合、それは不正な項です。例えば、項の中に現れる適用は常に適用の型付け規則
に適合するように型付けされていなければなりません。正しく構築された項は「破綻のない証明」であり「正しさが保証されたプログラム」でもあります。
コンピュータに型チェックという形で助けてもらいながら証明を書くことができます。型チェックの実装に必要な情報はこの記事の内容で完全に与えられており、それほど大きなプログラムを必要としません(つまり、型をチェックする側に間違いが起きにくい)。
CoCを使って証明を書くことで、人間が文で証明を書く時にありがちな間違いのチェックを一部自動化することができ、広く採用されれば数学の進化スピードを上げることにも繋がると思います。