![Lambda_Cube_img](https://upload.wikimedia.org/wikipedia/commons/c/cd/Lambda_Cube_img.svg)
In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
and
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
, the λ-cube (also written lambda cube) is a framework introduced by
Henk Barendregt
Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory.
Life and work
Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...
to investigate the different dimensions in which the
calculus of constructions
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, ...
is a generalization of the
simply typed λ-calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
. 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
BIND () is a suite of software for interacting with the Domain Name System (DNS). Its most prominent component, named (pronounced ''name-dee'': , short for ''name daemon''), performs both of the main DNS server roles, acting as an authoritative ...
a term or type. The respective dimensions of the λ-cube correspond to:
* x-axis (
): types that can bind terms, corresponding to
dependent type
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
s.
* y-axis (
): terms that can bind types, corresponding to
polymorphism.
* z-axis (
): types that can bind types, corresponding to (binding)
type operator
In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Som ...
s.
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 __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and d ...
.
Examples of Systems
(λ→) Simply typed lambda calculus
The simplest system found in the λ-cube is the
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda cal ...
, 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
In type theory, a typing rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well-typed and what type expressions have. ...
(λ2) System F
In
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
(also named λ2 for the "second-order typed lambda calculus") 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
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
OCaml ( , formerly Objective Caml) is a general-purpose programming language, general-purpose, multi-paradigm programming language which extends the Caml dialect of ML (programming language), ML with object-oriented programming, object-oriented ...
has type
'a -> 'a
meaning it can take an argument of any type
'a
and return an element of that type. This type corresponds in λ2 to the type
.
(λω) System Fω
In System F
a construction is introduced to supply types that depend on other types. This is called a
type constructor
In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. S ...
and provides a way to build "a function with a type as a ''value''". An example of such a type constructor is
, where "
" informally means "
is a type". This is a function that takes a type parameter
as an argument and returns the type of
s of values of type
. 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 F
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
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
. These are types that are allowed to depend on terms. The crucial introduction rule of the system is
where
represents valid types. The new type constructor
corresponds via the
Curry-Howard isomorphism to a universal quantifier, and the system λP as a whole corresponds to
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
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
constructor of System F and the type constructors from System F
. 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
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, ...
, denoted as λC in the cube or as λPω,
[ 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 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
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation th ...
, and then typing rules that allow to type those terms.
The set of sorts is defined as , sorts are represented with the letter . There is also a set of variables, represented by the letters . The raw terms of the eight systems of the cube are given by the following syntax:
and denoting when does not occur free in .
The environment, as is usual in typed systems, are given by
The notion of β-reduction is common to all systems in the cube. It is written and given by the rulesIts reflexive, transitive closure is written .
The following typing rules are also common to all systems in the cube:The difference between the systems is in the pairs of sorts that are allowed in the following two typing rules:
The correspondence between the systems and the pairs allowed in the rules is the following:
Each direction of the cube corresponds to one pair (excluding the pair shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types:
* allows terms to depend on terms.
* allows types to depend on terms.
* allows terms to depend on types.
* allows types to depend on types.
Comparison between the systems
λ→
A typical derivation that can be obtained isor with the arrow shortcutclosely resembling the identity (of type ) 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 .
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 aswith . If one reads 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
In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
types such as , 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 λ2 are those provably total in second-order Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
. 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:which corresponds, via the Curry-Howard isomorphism, to a proof of .
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 and , you need to apply the conversion rule to obtain to be able to type .
λω
In λω, the following operatoris definable, that is . The derivationcan be obtained already in λ2, however the polymorphic can only be defined if the rule 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 λω, hence why λC is also called λPω,[ so it is very powerful, both on the logical side and on the computational side.
]
Relation to other systems
The system Automath
Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
Ove ...
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 , and the ability to construct inductive types.
Pure type system __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and d ...
s 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 , the only axiom , and a set of rules such that .
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 and ), however one can define other connectives such as or in an impredicative
In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
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
* the Church-Rosser property: if and then there exists such that and ;
* the subject reduction property: if and then ;
* the uniqueness of types: if and then .
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
In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutabilit ...
however is not represented in the cube, even though systems like , 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 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
Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory.
Life and work
Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...
(1991). The framework of pure type system __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and d ...
s 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.
See also
* In his Habilitation à diriger les recherches, Olivier Ridoux gives a cut-out template of the lambda cube and also a dual representation of the cube as an octahedron, where the 8 vertices are replaced by faces, as well as a dual representation as a dodecahedron, where the 12 edges are replaced by faces.
* Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
Notes
Further reading
* {{cite web , first=Simon , last=Peyton Jones , first2=Erik , last2=Meijer , year=1997 , url=https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf , title=Henk: A Typed Intermediate Language , quote=Henk ''is based directly on the lambda cube'', an expressive family of typed lambda calculi.
External links
Barendregt's Lambda Cube
in the context of pure type systems __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and ...
by Roger Bishop Jones
Lambda calculus
Type theory