🔗 Lambda Cube

🔗 Computing 🔗 Mathematics

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:

• y-axis (${\displaystyle \uparrow }$): terms that can bind types, corresponding to polymorphism.
• x-axis (${\displaystyle \rightarrow }$): types that can bind terms, corresponding to dependent types.
• z-axis (${\displaystyle \nearrow }$): types that can bind types, corresponding to (binding) type operators.

The different ways to combine these three dimension 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.