Editing Lambda cube (section)

{{Short description|A framework}}
[[File:Lambda_Cube_img.svg|alt=|frame|The lambda cube. Direction of each arrow is direction of inclusion.]]

In [[mathematical logic]] and [[type theory]], the '''λ-cube''' (also written '''lambda cube''') is a framework introduced by [[Henk Barendregt]]<ref name=":0">{{Cite journal|last=Barendregt|first=Henk|date=1991|title=Introduction to generalized type systems|journal=[[Journal of Functional Programming]]|volume=1|issue=2|pages=125–154|doi=10.1017/s0956796800020025|issn=0956-7968|hdl=2066/17240|s2cid=44757552 |hdl-access=free}}</ref> to investigate the different dimensions in which the [[calculus of constructions]] is a generalization of the [[simply typed λ-calculus]]. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to [[Free variables and bound variables|bind]] a term or type. The respective dimensions of the λ-cube correspond to:

* x-axis (<math>\rightarrow</math>): types that can depend on terms, corresponding to [[dependent type]]s.
* y-axis (<math>\uparrow</math>): terms that can depend on types, corresponding to [[Parametric polymorphism|polymorphism]].
* z-axis (<math>\nearrow</math>): types that can depend on other types, corresponding to (binding) [[type operator]]s.

The different ways to combine these three dimensions yield the 8 vertices of the cube, each corresponding to a different kind of typed system. The λ-cube can be generalized into the concept of a [[pure type system]].