Lambda cubeとは - わかりやすく解説 Weblio辞書

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

ラムダ・キューブ

(Lambda cube から転送)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/12 15:56 UTC 版)

ナビゲーションに移動検索に移動

ラムダ・キューブの図。上向き軸はパラメトリック多相、奥向き軸は型オペレータ、右向き軸は依存型。

型理論において、ラムダ・キューブ (Lambda cube) とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、Calculus of Constructions (CoC)（英語版）を導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。

（右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点の $\lambda \Pi \omega$ は、Calculus of Constructionsに相当する。

各頂点は、以下の通りである:

λ→: 項に依存した項（単純型付きラムダ計算）; 一階命題論理; （これを以下全てが含む。）
λ2: 型に依存した項（System F）; パラメトリック多相; 二階命題論理
λω: 型に依存した型（System Fω）; 型オペレータ; 弱性高階命題論理
λω: 型に依存した型、型に依存した項（System Fω）; 型構築子; 高階命題論理; λ2とλωの融合
λP: 項に依存した型（ $\lambda \Pi$ ）; 依存型; 一階述語論理
λP2: 型に依存した項、項に依存した型（ $\lambda \Pi 2$ ）; 依存型; 二階述語論理; λPとλ2の融合
λPω: 項に依存した型、型に依存した型（ $\lambda \Pi {\underline {\omega }}$ ）; 依存型; 弱性高階述語論理; λPとλωの融合
λC: 型に依存した型、型に依存した項、項に依存した型（ $\lambda \Pi \omega$ ）; CoC; 高階述語論理; λP2とλPωの融合