ラムダ・キューブ
ラムダキューブ(lambda cube)
$ \rightarrow : x軸: 依存型
$ \uparrow : y軸: 多相型(ポリモーフィズム)
$ \nearrow : z軸: 型コンストラクタ(type operator)
λ→
単純型付きラムダ計算
λP
(→ λ→) → λP
単純型付きラムダ計算 + 依存型
$ \lambda \underline{\omega}
($ \nearrow λ→) → λP
単純型付きラムダ計算 + 型コンストラクタ
λ2
($ \uparrow λ→) → λ2
単純型付きラムダ計算 + 多相型
λω
単純型付きラムダ計算 + 多相型 + 型コンストラクタ
λ2 → λω or $ \lambda \underline{\omega} → λω
λP2
単純型付きラムダ計算 + 依存型 + ポリモーフィズム
λ2 → λP2 or λP → λP2
$ λP\underline{\omega}
単純型付きラムダ計算 + 依存型 + 型コンストラクタ
λP → λPω or $ \lambda \underline{\omega} → λPω
λC
単純型付きラムダ計算 + 依存型 + 型コンストラクタ + 多相型
λω → λC
λP2 → λC
$ λP\underline{\omega} → λC
Calculus of Constructions(CoC)
確認用
Q. ラムダキューブ
調査用
Google.icon ラムダ・キューブ(日)
Google.icon Lambda cube(英)
Wikipedia.icon
ラムダ・キューブ - Wikipedia(日)
ラムダ・キューブ(検索) - Wikipedia(日)
Wikipedia.icon
Lambda cube - Wikipedia(英)
Lambda cube(検索) - Wikipedia(英)