Lambda cube
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt[1] 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.
The respective dimensions of the λ-cube correspond to: 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.
The simplest system found in the λ-cube is the simply typed lambda calculus, also called λ→.
are called polymorphic, as they can be applied to different types to get different functions, similarly to polymorphic functions in ML-like languages.
In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives.
is generally not used on its own, but is useful to isolate the independent feature of type constructors.
[4] In the λP system, also named λΠ, and closely related to the LF Logical Framework, one has so called dependent types.
In the calculus of constructions, denoted as λC in the cube or as λPω,[1]: 130 these four features cohabit, so that both types and terms can depend on types and terms.
The raw terms of the eight systems of the cube are given by the following syntax:
The following typing rules are also common to all systems in the cube:
shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types: A typical derivation that can be obtained is
as a universal quantification, via the Curry-Howard isomorphism, this can be seen as a proof of the principle of explosion.
More precisely, the functions definable in λ2 are those provably total in second-order Peano arithmetic.
In λP, the ability to have types depending on terms means one can express logical predicates.
.From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties.
From a computing point of view, λω is extremely strong, and has been considered as a basis for programming languages.
[10] The calculus of constructions has both the predicate expressiveness of λP and the computational power of λω, hence why λC is also called λPω,[1]: 130 so it is very powerful, both on the logical side and on the computational side.
The system Automath is similar to λ2 from a logical point of view.
However, because they feature some recursion operators, their computing power is greater than that of λ2.
[7] The Coq system is based on an extension of λC with a linear hierarchy of universes, rather than only one untypable
Pure type systems can be seen as a generalization of the cube, with an arbitrary set of sorts, axiom, product and abstraction rules.
[1] Via the Curry-Howard isomorphism, there is a one-to-one correspondence between the systems in the lambda cube and logical systems,[1] namely: All the logics are implicative (i.e. the only connectives are
in an impredicative way in second and higher order logics.
allow the definition of purely functional objects; these systems were generally developed after the lambda cube paper was published.
[12] The idea of the cube is due to the mathematician Henk Barendregt (1991).
The framework of pure type systems 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.
[13] This framework predates the lambda cube by a couple of years.
In his 1991 paper, Barendregt also defines the corners of the cube in this framework.
