Lambda cube
Encyclopedia : L : LA : LAM : Lambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a (3-D) cube placed at the origin, and the calculus of constructions (= higher order dependently-typed polymorphic lambda calculus) as its diametric opposite vertex. Each axis of the cube represents a new form of abstraction:
- Terms depending on types, or polymorphism (as in System F),
- Types depending on types, or type operators, and
- Types depending on terms, or dependent types (as in LF).
The idea of the cube is due to the mathematician Henk Barendregt (1991).
See also
References
- H.P. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, 1(2):125-154, April 1991.
- [Barendregt's Lambda Cube]
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.