View source for Close-packing of equal spheres

[[Image:Lambda_cube.png|frame|The lambda cube. Direction of each arrow is direction of inclusion. ]]
__NOTOC__
In [[mathematical logic]] and [[type theory]], the '''λ-cube''' is a framework for exploring the axes of refinement in [[Thierry Coquand|Coquand]]'s [[calculus of constructions]], starting from the [[simply typed lambda calculus]] (written as <math>\lambda\rightarrow</math> in the cube diagram to the right) as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus; written as λPω in the diagram) as its diametrically opposite vertex.  Each axis of the cube represents a new form of abstraction:
* Terms depending on types, or [[Polymorphism (computer science)|polymorphism]]. [[System F]], aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
* Types depending on types, or [[type operator]]s. [[Simply typed lambda-calculus with type operators]], λ<sub>ω</sub> (the diagram underlines the ω), is obtained by imposing only this property. Combined with [[System F]] it yields [[System F#System Fω|System F<sub>ω</sub>]] (written as λω without the underline in the diagram).
* Types depending on terms, or [[Dependent type theory|dependent types]]. Imposing only this property yields λΠ (written as λP in the diagram), a type system closely related to [[LF (logical framework)|LF]]. 

All eight calculi include the most basic form of abstraction, terms depending on terms, ordinary functions as in the simply-typed lambda calculus. The richest calculus in the cube, with all three abstractions, is the [[calculus of constructions]]. All eight calculi are [[Normalization property (lambda-calculus) |strongly normalizing]].

[[Subtyping]] however is not represented in the cube, even though systems like <math>F^\omega_{<:}</math>, known as [[higher-order bounded quantification]], which combines subtyping and polymorphism are of practical interest, and can be further generalized to [[bounded type operator]]s. Further extensions to <math>F^\omega_{<:}</math> allow the definition of [[purely functional objects]]; these systems were generally developed after the lambda cube paper was published.<ref>Pierce, 2002, chapters 31 and 32</ref>

The idea of the cube is due to the mathematician [[Henk Barendregt]] (1991). The framework of [[pure type system]]s generalizes the lambda cube in the sense that all corners of the cube, as well as many other systems can be represented as instances of this general framework.<ref>Pierce, 2002, p. 466</ref> This framework predates lambda cube a couple of years. In his 1991 paper, Barendregt also defines the corners of the cube in this framework.

==See also==

* Some of the systems included in the cube were first defined in [[Automath]].

== Notes ==
{{reflist}}

==References==
{{refbegin}}
* Morten Heine Sørensen, Paweł Urzyczyn, ''Lectures on the Curry-Howard isomorphism'', Elsevier, 2006, ISBN 0-444-52077-5, chapter 14, "Pure type systems and the lambda cube"<!-- this covers pretty much everything in this article, except the subtyping stuff, which is only discussed by Pierce -->
* [[H.P. Barendregt]], [http://dare.ubn.kun.nl/bitstream/2066/17240/1/13256.pdf Introduction to generalized type systems], ''Journal of Functional Programming'', 1(2):125-154, April 1991.
* {{cite book|last=Pierce|first=Benjamin|title=Types and Programming Languages|publisher=MIT Press|date=2002|id=ISBN 0-262-16209-1}}
{{refend}}

==Further reading==
* Simon Peyton Jones and Erik Meijer, 1997. [http://citeseer.ist.psu.edu/peytonjones97henk.html ''Henk: A Typed Intermediate Language'']<!-- Not clear why this is given as ref since it's never mentioned in the article, but the article could mention it-->

== External links ==
* [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube] in the context of [[pure type systems]] by Roger Bishop Jones

[[Category:Lambda calculus]]
[[Category:Type theory]]