# The 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 way of making objects depend on other objects, namely

1. terms allowed to depend on types, corresponding to polymorphism.
2. types depending on terms, corresponding to dependent types.
3. types depending on types, corresponding to 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.

So in the diagram above, we have emblazoned the names of these type systems ordered from lower left to upper right:

• λ→: the simply typed lambda calculus, our base system
• λ2: add 1. above to λ→, giving what is also known as System F or the Girard–Reynolds polymorphic lambda calculus
• λP: add 2. above to λ→
• λ_ω_: add 3. above to λ→
• λP2: combine 1. and 2., λ2 and λP
• λω: combine 1. and 3., λ2 and λ_ω_
• λP_ω_: combine 2. and 3., λP and λ_ω_
• λC: combine 1., 2., and 3., giving the calculus of constructions

https://en.wikipedia.org/wiki/Lambda_cube

http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm

https://en.wikipedia.org/wiki/Calculus_of_constructions

https://en.wikipedia.org/wiki/System_F

[* 11.86, *11.87]

<>

This site uses Akismet to reduce spam. Learn how your comment data is processed.