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:

x-axis (

→

{\displaystyle \rightarrow }

): types that can depend on terms, corresponding to dependent types.

y-axis (

↑

{\displaystyle \uparrow }

): terms that can depend on types, corresponding to polymorphism.

z-axis (

↗

{\displaystyle \nearrow }

): 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:

Γ

,

x

:

σ

⊢

t

:

τ

Γ

⊢

λ

x

.