ラムダ・キューブ
Lambda Cube
原点の単純型付きラムダ計算から、Calculus of Constructionsを導く
Henk Barendregt
多相型、型演算、依存型を図で表したもの
ラムダ・キューブをさらに一般化したものとして純粋型システムがある
https://gyazo.com/9b11591e32cbf035f08c6d32ce1b97d8
対応
原点
$ \lambda_\to: 単純型付きラムダ計算
基礎的な抽象化
$ \lambda2: System F
型に依存した値
パラメトリック多相
λP
依存型をあつかう
値に依存した型
$ \lambda\underline{\omega}: 高階多相型
型に依存した型
kindなどを扱う
組み合わせたもの
$ \lambda P\underline{\omega}
ここってあまりないのかなmrsekut.icon
wikiや本にもあまり書かれていない
$ \lambda P2: 依存型 + System F
$ \lambda\omega: System Fω
高階多相型 + System F
全部入り
$ \lambda P\omega: Calculus of Constructions
$ \lambda Cとも書く
関連
LF
https://en.wikipedia.org/wiki/Logical_framework#LF
参考
龍田『型理論』 8章
ラムダ・キューブ - Wikipedia
https://ja.wikipedia.org/wiki/依存型#ラムダ・キューブ
https://en.wikipedia.org/wiki/Lambda_cube