Wikipedia / Lambda cube
Wikipedia / Lambda cube
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt 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 bind a term or type. The respective dimensions of the λ-cube correspond to:
): types that can depend on terms, corresponding to dependent types.
): terms that can depend on types, corresponding to polymorphism.
): types that can depend on other types, corresponding to (binding) type operators.
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.
Examples of systems
(λ→) Simply typed lambda calculus
The simplest system found in the λ-cube is the simply typed lambda calculus, also called λ→. In this system, the only way to construct an abstraction is by making a term depend on a term, with the typing rule:
(λ2) System F
In System F (also named λ2 for the "second-order typed lambda calculus"), that allows terms to depend on types, with the following rule:
are called polymorphic, as they can be applied to different types to get different functions, similarly to polymorphic functions in ML-like languages. For instance, the polymorphic identity of OCaml has type meaning it can take an argument of any type 'a.
(λω) System Fω
a construction is introduced to supply types that depend on other types. This is called a type constructor and provides a way to build "a function with a type as a value".. In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml:
This type constructor can be applied to other types to obtain new types. E.g., to obtain type of trees of integers:
is generally not used on its own, but is useful to isolate the independent feature of type constructors.
(λP) Lambda-P
In the λP system, also named λΠ, which is closely related to the LF Logical Framework, one has so called dependent types. These are types that are allowed to depend on terms. The crucial introduction rule of the system is
corresponds via the Curry-Howard isomorphism to a universal quantifier, and the system λP as a whole corresponds to first-order logic with implication as only connective. An example of these dependent types in concrete programming is the type of vectors on a certain length: the length is a term, on which the type depends.
(λω) System Fω
System Fω. Thus System Fω provides both terms that depend on types and types that depend on types.
(λC) Calculus of constructions
In the calculus of constructions, denoted as λC in the cube or as λPω, are themselves terms with a type.
Formal definition
As for all systems based upon the simply typed lambda calculus, all systems in the cube are given in two steps: first, raw terms, together with a notion of β-reduction, and then typing rules that allow to type those terms.
. The raw terms of the eight systems of the cube are given by the following syntax:
.
Its reflexive, transitive closure.
allowed in the rules is the following: shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types:
allows terms to depend on terms.
allows types to depend on terms.
allows terms to depend on types.
allows types to depend on types.
Comparison between the systems
λ→
.
The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator).
λ2
as a universal quantification, via the Curry-Howard isomorphism, this can be seen as a proof of the principle of explosion. In general, λ2 adds the possibility to have impredicative, that is terms quantifying over all types including themselves.The polymorphism also allows the construction of functions that were not constructible in λ→. More precisely, the functions definable in λ2 are those provably total in second-order Peano arithmetic. In particular, all primitive recursive functions are definable.
λP
.From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties.
, one needs to apply the conversion rule.
λω
is also present.
From a computing point of view, λω is extremely strong, and has been considered as a basis for programming languages.
λC
The calculus of constructions has both the predicate expressiveness of λP and the computational power of λω, hence why λC is also called λPω, so it is very powerful, both on the logical side and on the computational side.
Relation to other systems
The system Automath is similar to λ2 from a logical point of view. The ML-like languages, from a typing point of view, lie somewhere between λ→ and λ2, as they admit a restricted kind of polymorphic types, that is the types in prenex normal form. However, because they feature some recursion operators, their computing power is greater than that of λ2., and the ability to construct inductive types.
Via the Curry-Howard isomorphism, there is a one-to-one correspondence between the systems in the lambda cube and logical systems, namely: in an impredicative way in second and higher order logics. In the weak higher order logics, there are variables for higher order predicates, but no quantification on those can be done.
Common properties
All systems in the cube enjoy
All of these can be proven on generic pure type systems.
Any term well-typed in a system of the cube is strongly normalizing, although this property is not common to all pure type systems. No system in the cube is Turing complete.
Subtyping
Subtyping, known as higher-order bounded quantification, which combines subtyping and polymorphism are of practical interest, and can be further generalized to bounded type operators allow the definition of purely functional objects; these systems were generally developed after the lambda cube paper was published.
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. 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.
See also
In his Habilitation à diriger les recherches, Olivier Ridoux gives a cut-out template of the lambda cube and also a dual representation of the cube as an octahedron, where the 8 vertices are replaced by faces, as well as a dual representation as a dodecahedron, where the 12 edges are replaced by faces.
Notes
Further reading
External links
Barendregt's Lambda Cube in the context of pure type systems by Roger Bishop Jones