ラムダ・キューブ

ラムダ・キューブ。上向きの軸が多相型、奥向きの軸が型演算、右向きの軸が依存型にそれぞれ対応する。

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

ラムダ・キューブの原点は単純型付きラムダ計算に相当し，それぞれの座標軸には次の依存関係が対応付けられている:

型に依存した値（多相型）: これのみを導入したものは $\lambda 2$ (System F) と呼ばれる。
型に依存した型（型演算）: これのみを導入したものは $\lambda\underline{\omega}$ と呼ばれる。System Fと組み合わせると $\lambda\omega$ (System F_ω) が得られる。
値に依存した型（依存型）: これのみを導入したものは $\lambda\Pi$ ないし $\lambda P$ と呼ばれる。System Fと組み合わせると $\lambda\Pi 2$ が得られる。