ラムダ・キューブ
ラムダキューブ(lambda cube)
$ \rightarrow : x軸: 依存型
$ \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
確認用
Q. ラムダキューブ
調査用
Wikipedia.icon
Wikipedia.icon