lambda cube

ウィキペディア

ラムダ・キューブ

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/12 15:56 UTC 版)

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