Lambda cube

CRANK

The lambda cube. Direction of each arrow is direction of inclusion.In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt [1] 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, namelyThe different ways to combine these three dimension yield the 8 vertices of the cube, each corresponding to a different kind of typed system.Examples of Systems[edit]Simply Typed Lambda Calculus[edit]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 variable, with the ruleSystem F[edit]In System F, also named λ2, there is another type of abstraction, written with a , that allows terms to depend on types, with the following rule:The terms beginning with a…