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:

  • x-axis (<math>\rightarrow</math>): types that can depend on terms, corresponding to dependent types.
  • y-axis (<math>\uparrow</math>): terms that can depend on types, corresponding to polymorphism.
  • z-axis (<math>\nearrow</math>): 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:

<math>\frac{\Gamma, x : \sigma \;\vdash\; t : \tau}{\Gamma \;\vdash\; \lambda x . t : \sigma \to \tau}</math>

(λ2) System F

In System F (also named λ2 for the "second-order typed lambda calculus") there is another type of abstraction, written with a <math>\Lambda</math>, that allows terms to depend on types, with the following rule:

<math>\frac{\Gamma \;\vdash\; t : \sigma}{\Gamma \;\vdash\; \Lambda \alpha . t : \Pi \alpha . \sigma} \;\text{ if } \alpha\text{ does not occur free in }\Gamma</math>

The terms beginning with a <math>\Lambda</math> 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 <syntaxhighlight lang="ocaml">

fun x -> x

</syntaxhighlight>of OCaml has type <syntaxhighlight lang="ocaml">

'a -> 'a

</syntaxhighlight>meaning it can take an argument of any type <code>'a</code> and return an element of that type. This type corresponds in λ2 to the type <math>\Pi \alpha . \alpha \to \alpha</math>.

(λ<u>ω</u>) System F<u>ω</u>

In System F<math>\underline{\omega}</math> 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". An example of such a type constructor is the type of binary trees with leaves labeled by data of a given type <math>A</math>: <math>\mathsf{TREE} := \lambda A : * . \Pi B . (A \to B) \to (B \to B \to B) \to B</math>, where "<math>A:*</math>" informally means "<math>A</math> is a type". This is a function that takes a type parameter <math>A</math> as an argument and returns the type of <math>\mathsf{TREE}</math>s of values of type <math>A</math>. 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:<syntaxhighlight lang="ocaml">

type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree

</syntaxhighlight>

This type constructor can be applied to other types to obtain new types. E.g., to obtain type of trees of integers:<syntaxhighlight lang="ocaml">type int_tree = int tree</syntaxhighlight>

System F<math>\underline{\omega}</math> 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

<math>\frac{\Gamma, x : A \;\vdash\; B : *}{\Gamma \;\vdash\; (\Pi x : A . B) : *}</math>

where <math>*</math> represents valid types. The new type constructor <math>\Pi</math> 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ω combines both the <math>\Lambda</math> constructor of System F and the type constructors from System F<math>\underline{\omega}</math>. 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ω,

λ2

In λ2, such terms can be obtained as<math display="block">\vdash (\lambda \beta : * . \lambda x : \bot . x \beta) : \Pi \beta : * . \bot \to \beta</math>with <math display="inline">\bot = \Pi \alpha : * . \alpha</math>. If one reads <math display="inline">\Pi</math> 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 types such as <math display="inline">\bot</math>, that is terms quantifying over all types including themselves.<br />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

In λP, the ability to have types depending on terms means one can express logical predicates. For instance, the following is derivable:<math display="block">\begin{array}{l}\alpha : *, a_0 : \alpha, p : \alpha \to *, q : * \vdash \\ \quad \lambda z : (\Pi x : \alpha . p x \to q) . \\ \quad \lambda y : (\Pi x : \alpha . p x) . \\ \quad (z a_0) (y a_0) : (\Pi x : \alpha . p x \to q) \to (\Pi x : \alpha . p x) \to q \end{array}</math>which corresponds, via the Curry-Howard isomorphism, to a proof of <math>(\forall x : A, P x \to Q) \to (\forall x : A, P x) \to Q</math>.<br />From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties.

The conversion rule is strongly needed when dealing with dependent types, because it allows to perform computation on the terms in the type.

For instance, if one has <math>\Gamma \vdash A : P((\lambda x . x)y)</math> and <math>\Gamma \vdash B : \Pi x : P(y) . C</math>, one needs to apply the conversion rule to obtain <math>\Gamma \vdash A : P(y)</math> to be able to type <math>\Gamma \vdash B A : C</math>.

λω

In λω, the following operator<math display="block">AND := \lambda \alpha : * . \lambda \beta : * . \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma</math>is definable, that is <math>\vdash AND : * \to * \to *</math>. The derivation<math display="block">\alpha : *, \beta : * \vdash \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma : *</math>can be obtained already in λ2, however the polymorphic <math display="inline">AND</math> can only be defined if the rule <math display="inline">(\square, *)</math> 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ω,

Any term well-typed in a system of the cube is strongly normalizing,

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.
  • Logical cube
  • Logical hexagon
  • Square of opposition
  • Triangle of opposition

Notes

Further reading

  • Barendregt's Lambda Cube in the context of pure type systems by Roger Bishop Jones