6
大学数学基礎解説
文献あり

ラムダ計算と Calculus of Constructions の定義解説

429
0

この記事は、以下の動画群の内容をより厳密になるように書き直したものです。動画ではかみ砕いた表現を使い、厳密さを欠くかわりにとっつきやすい解説をしています。

https://youtube.com/playlist?list=PLJucEMNgEA4mK12iTTer1nV1jWaTvCKMo

導入

ラムダ計算は、計算を「純粋な関数への適用」のみによって記述する計算模型です。これに型という概念を導入したものを型付きラムダ計算と呼びます。カリー=ハワード同型対応の存在により、型付きラムダ計算を使って証明を構成的に記述することができます。これには次のようなメリットがあります。

  • 完全に構成的で、言葉の曖昧さがない
  • コンピュータによる型チェックを通して、理論の飛躍や破綻がないことを保証できる
  • 証明をアルゴリズムとして再解釈でき、実行できる

この記事では、型付きラムダ計算の一種で豊富な表現力を持つCalculus of Constructions (CoC)の定義を解説します。

構文

CoCで扱う唯一の数学的対象はです。項はラムダ抽象、積、適用、変数、宇宙のどれかであると定義されます(厳密な定義は後に示します)。

厳密さを欠きますが、それぞれの項は一般的な数学で用いられる概念と次のように対応しています。

名称ラムダ計算の表記対応する概念一般的な数学の表記
ラムダ抽象λx:P. Q関数定義f(x):=Q (xP)
[x:P] Q関数の型PQ
適用A B関数の使用A(B)
変数x変数x
宇宙すべての集合のクラスSet

ラムダ抽象(lambda abstraction)は λx:P. Q のように書かれ、関数を表します。変数xを導入することを明示する目的でx束縛する(bind)ラムダ抽象と言うこともあります。ここで、Px(type)であり、xに代入できる値の種類を決定するもので、厳密には集合とは異なります。また、ラムダ抽象は右結合です。すなわち、 λx:P. λy:Q. x y と書いた場合は λx:P. (λy:Q. (x y)) を意味します。

(product)は [x:P] Q のように書かれ、主に関数の型を表します。直観的には関数や写像の種類を表す PQ と同じ意味ですが、積はQの中で変数xを使ってもよいという点で、よりも広い対象を表現できます。積もラムダ抽象と同じく右結合であり、変数を指して「束縛する」という表現を使うことがあります。

適用(application)は A B のように書かれ、Aを関数と見た場合にそれを「呼び出す」操作を表します。ラムダ計算では乗算などの演算が定義されないため、これは A×B を表すものではないことに注意して下さい。また適用は左結合であり、 A B C=(A B) C です。

変数(variables)は名前通り変数で、ラムダ抽象または積によって導入され、上記式の Q の中で使えるようになります。変数の名前は本質的に無意味であり、それを導入したラムダ抽象または積への参照だと考えてください。

最後に、宇宙(universe)はと書き、全ての型の型として機能します(ただし、自身の型はではありません)。を読む際は一般に type と読みます。


項は文脈(context)とオブジェクト(object)の2種類に分類されます。

項・文脈・オブジェクト

全ての文脈の集合 Λo を、次のように帰納的に定義します。

(宇宙)Λo(量化)[x:T]ΔΛowhereTΛ, ΔΛo


全てのオブジェクトの集合 Λi を、次のように帰納的に定義します。

(変数)xΛi(積)[x:T] AΛiwhereTΛ, AΛi(ラムダ抽象)λx:T. AΛiwhereTΛ, AΛi(適用)A BΛiwhereA,BΛi


全ての項の集合 Λ は、上記2つの和集合です。

Λ=ΛoΛi

以降の文では、汎用的な変数としてΓ,Δは文脈を、A,B,P,Qはオブジェクトを、T,U,Vはそのどちらかまたは両方を表すものとして使います。

文脈の解釈と演算

定義より、文脈は常に

Γ=[x1:T1][x2:T2]...[xn:Tn]

という形で表され、これは変数と型の0個以上のリストとみなすことができます。この中に特定の変数xiが含まれていて(xiを束縛していて)その型がTiであることを [xi:Ti]Γ と書くことにします。

文脈の付加

任意の文脈 Γ=[x1:T1][x2:T2]...[xn:Tn] と項Uについて、文脈の付加 Γ[k:U] を次のように定義します。

Γ[k:U]=[x1:T1][x2:T2]...[xn:Tn][k:U]

直観的には、文脈の付加はΓの末尾にある[k:U]に置き換える操作です。

文脈にはいくつかの意味があります。項を解釈する際に「既に分かっている変数のリスト」を表す文脈としての意味のほか、型多相、命題や述語の型を表すのにも使われます。

オブジェクトの解釈

オブジェクトは、論理命題やその証明、関数などを表すのに使われます。CoCは抽象的な計算模型であるため、証明に使う操作(自然演繹)と関数の操作の両方に対して同じ構文を使います。

例えば、 [x:T] U は論理命題 TUλx:T. A はその証明であり、これはTという仮定のもとで命題Uの証明Aを与えているものと解釈できます。従って [x:T] U は全称量化 x:T. U だと考えられます。しかし依然として(関数の型を内包する)積 Πx:T. U としての意味も持ちます。CoCでは、仮定の導入にも関数の型にも共通した [x:T] U という表記を与えています。
同様に、 A B という表記はモーダス・ポネンス(論理学の用語で (PQ)PQ のこと)と関数適用の両方に使われます。

判断

はじめに、判断(judgement)の記号 ΓJ を導入します。これは文脈 Γ のもとで判断J有効であることを表しています。ここで、Γは文脈であり、Jは以下で定義されるいずれかの判断です。

J={Δ(文脈)A:T(型判断)AB(同型)

また、以下では直観主義論理などで使われる表記αβを使います。これはαβと同じ意味です。

文脈と型の判断

文脈判断

ある文脈Γのもとで別の文脈Δが有効であることをΓΔと表します。これは次の規則によって与えられます。

ΓΔΓ[x:Δ]

ΓA:Γ[x:A]

Γ[x:T]ΔΓ[x:T]Δ

Γ は文脈Γ自体が有効であることも同時に表しています。

型判断

ある文脈ΓのもとでATによって有効に型付けされることを ΓA:T と表します。これは次の規則によって与えられます。

(積)Γ[x:T]A:Γ[x:T] A:

(変数)ΓΓx:T([x:T]Γ)

(ラムダ抽象)Γ[x:T]A:UΓ(λx:T. A):[x:T] U

(適用)ΓA:[x:T] UΓB:TΓA B:[B/x]U

(同型)ΓA:TΓTUΓA:U

ここで [B/x]U という表記は、Uの中にある変数xBを代入して得られる項を表します。

適用の規則では、ABの型に共通してTが現れます。これはAの型の一部とBの型が"同じ"でなければならないことを表します。この「同じ」の判断は、次に示す同型の規則によって与えられます。

同型判断

同型判断

ある文脈ΓのもとでTUが"同じ"と判断できることを ΓTU と表します。これは次の規則によって与えられます。

Γ[x:T]A:UΓB:TΓ(λx:T. A) B[B/x]A

この規則は、「β簡約(後述)しても同型である」ことを表しており、同型規則の本質です。残りの規則は、「同型なもの同士から構成されるものは同型である」ことを表しています。

ΓΔΓΔΔ

ΓA:TΓAA

ΓTUΓUT

ΓTUΓUVΓTV

ΓTTΓ[x:T]AAΓ[x:T]A[x:T]A

Γ[x:T]A:UΓTTΓ[x:T]AAΓλx:T. Aλx:T. A

ΓA B:TΓAAΓA BA B

ΓA B:TΓBBΓA BA B

β簡約

同型の規則に従ってある項 (λx:T. A) B をそれと同型な項 [B/x]A に変形することをβ簡約と言い、

(λx:T. A) Bβ[B/x]A

と表します。項の一部分にのみ上記の変形が可能な場合も同様にβ簡約と言います。

β簡約は、CoCの項をプログラムだと解釈する場合に唯一可能な「実行」の操作だと考えることができます。

おわりに(定義ではない解説)

コンピュータによる型チェック

「コンピュータによる型チェック」では、上記規則を使ってある項が正しく構築されているかをチェックします。規則にない項の使い方をしている場合、それは不正な項です。例えば、項の中に現れる適用は常に適用の型付け規則

ΓA:[x:T] UΓB:TΓA B:[B/x]U

に適合するように型付けされていなければなりません。正しく構築された項は「破綻のない証明」であり「正しさが保証されたプログラム」でもあります。

結局何ができるものなのか

コンピュータに型チェックという形で助けてもらいながら証明を書くことができます。型チェックの実装に必要な情報はこの記事の内容で完全に与えられており、それほど大きなプログラムを必要としません(つまり、型をチェックする側に間違いが起きにくい)。
CoCを使って証明を書くことで、人間が文で証明を書く時にありがちな間違いのチェックを一部自動化することができ、広く採用されれば数学の進化スピードを上げることにも繋がると思います。

参考文献

投稿日:202357
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

折り紙の数学って知ってる?

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中
  1. 導入
  2. 構文
  3. 文脈の解釈と演算
  4. オブジェクトの解釈
  5. 判断
  6. 文脈と型の判断
  7. 同型判断
  8. おわりに(定義ではない解説)
  9. コンピュータによる型チェック
  10. 結局何ができるものなのか
  11. 参考文献