ラムダ・キューブ

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

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

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

  • 型に依存した値(多相型): これのみを導入したものは (System F) と呼ばれる。
  • 型に依存した型(型演算): これのみを導入したものはと呼ばれる。System Fと組み合わせると (System Fω) が得られる。
  • 値に依存した型(依存型): これのみを導入したものはないしと呼ばれる。System Fと組み合わせるとが得られる。

これらの他に、すべての計算体系は単純型付きラムダ計算に含まれる値に依存した値(すなわち、通常の関数抽象)を持っている。3つの抽象の全てを導入したものがとよばれ、Calculus of Constructionsに対応する。

参考文献編集

  • Barendregt, Henk, “Lambda Calculi with Types”, Handbook of Logic in Computer Science, Volume II, Oxford University Press, ISBN 0-19-853761-1, ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps