Lambda cube

In mathematical logic and type theory, the λ-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:
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
formula_4
(λ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 formula_5, that allows terms to depend on types, with the following rule:
formula_6
The terms beginning with a formula_5 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 
fun x -> x
of OCaml has type 
'a -> 'a
meaning it can take an argument of any type codice_1 and return an element of that type. This type corresponds in λ2 to the type formula_8.
(λω) System Fω.
In System Fformula_9 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 formula_10, where "formula_11" informally means "formula_12 is a type". This is a function that takes a type parameter formula_12 as an argument and returns the type of formula_14s of values of type formula_12. 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:
type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree
This type constructor can be applied to other types to obtain new types. E.g., to obtain type of trees of integers:type int_tree = int tree
System Fformula_9 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 ΛΠ, and 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
formula_17
where formula_18 represents valid types. The new type constructor formula_19 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.
(Fω) System Fω.
System Fω combines both the formula_5 constructor of System F and the type constructors from System Fformula_9. 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 (λPω is the λC corner of the cube), these four features cohabit, so that both types and terms can depend on types and terms. The clear border that exists in λ→ between terms and types is somewhat abolished, as all types except the universal formula_22 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 set of sorts is defined as formula_23, sorts are represented with the letter formula_24. There is also a set formula_25 of variables, represented by the letters formula_26. The raw terms of the eight systems of the cube are given by the following syntax:
formula_27
and formula_28 denoting formula_29 when formula_30 does not occur free in formula_31.
The environment, as is usual in typed systems, are given by
formula_32
The notion of β-reduction is common to all systems in the cube. It is written formula_33 and given by the rulesformula_34formula_35formula_36formula_37formula_38Its reflexive, transitive closure is written formula_39.
The following typing rules are also common to all systems in the cube:formula_40formula_41formula_42formula_43formula_44The difference between the systems is in the pairs of sorts formula_45 that are allowed in the following two typing rules:formula_46formula_47
The correspondence between the systems and the pairs formula_45 allowed in the rules is the following:
Each direction of the cube corresponds to one pair (excluding the pair formula_49 shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types:
Comparison between the systems.
λ→.
A typical derivation that can be obtained isformula_54or with the arrow shortcutformula_55closely resembling the identity (of type formula_56) of the usual λ→. Note that all types used must appear in the context, because the only derivation that can be done in an empty context is formula_57.
The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator).
λ2.
In λ2, such terms can be obtained asformula_58with formula_59. If one reads formula_60 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 formula_61, 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 System F 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:formula_62which corresponds, via the Curry-Howard isomorphism, to a proof of formula_63.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 you have formula_64 and formula_65, you need to apply the conversion rule to obtain formula_66 to be able to type formula_67.
λω.
In λω, the following operatorformula_68is definable, that is formula_69. The derivationformula_70can be obtained already in λω, however the polymorphic formula_71 can only be defined if the rule formula_52 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 λω, so it is very powerful, both on the logical side and on the computational side. (λPω is the λC corner of the cube)
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. The Coq system is based on an extension of λC with a linear hierarchy of universes, rather than only one untypable formula_73, and the ability to construct inductive types.
Pure Type Systems can be seen as a generalization of the cube, with an arbitrary set of sorts, axiom, product and abstraction rules. Conversely, the systems of the lambda cube can be expressed as Pure Type Systems with two sorts formula_74, the only axiom formula_75, and a set of rules formula_76 such that formula_77.
Via the Curry-Howard isomorphism, there is a one-to-one correspondence between the systems in the lambda cube and logical systems, namely:
All the logics are implicative (i.e. the only connectives are formula_78 and formula_79), however one can define other connectives such as formula_80 or formula_81 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 however is not represented in the cube, even though systems like formula_93, known as higher-order bounded quantification, which combines subtyping and polymorphism are of practical interest, and can be further generalized to bounded type operators. Further extensions to formula_93 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.