Lambda cube

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:

$\backslash frac\{\backslash Gamma,\; x\; :\; \backslash sigma\; \backslash ;\backslash vdash\backslash ;\; t\; :\; \backslash tau\}\{\backslash Gamma\; \backslash ;\backslash vdash\backslash ;\; \backslash lambda\; x\; .\; t\; :\; \backslash sigma\; \backslash to\; \backslash tau\}$

In System F (also named λ2 for the "second-order typed lambda calculus"){{cite book |last1=Nederpelt |first1=Rob |last2=Geuvers |first2=Herman |title=Type Theory and Formal Proof |date=2014 |publisher=Cambridge University Press |isbn=9781107036505 |page=69 |url=https://www.cambridge.org/vi/academic/subjects/computer-science/programming-languages-and-applied-logic/type-theory-and-formal-proof-introduction?format=HB }} there is another type of abstraction, written with a $\backslash Lambda$, that allows terms to depend on types, with the following rule:

$\backslash frac\{\backslash Gamma\; \backslash ;\backslash vdash\backslash ;\; t\; :\; \backslash sigma\}\{\backslash Gamma\; \backslash ;\backslash vdash\backslash ;\; \backslash Lambda\; \backslash alpha\; .\; t\; :\; \backslash Pi\; \backslash alpha\; .\; \backslash sigma\}\; \backslash ;\backslash text\{\; if\; \}\; \backslash alpha\backslash text\{\; does\; not\; occur\; free\; in\; \}\backslash Gamma$

The terms beginning with a $\backslash Lambda$ 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 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 $\backslash Pi\; \backslash alpha\; .\; \backslash alpha\; \backslash to\; \backslash alpha$.

In System F$\backslash underline\{\backslash omega\}$ a construction is introduced to supply types that depend on other types. This is called a type constructor and provides a way to build "a function with a type as a value".{{harvnb|Nederpelt|Geuvers|2014|p=85}} An example of such a type constructor is the type of binary trees with leaves labeled by data of a given type $A$: $\backslash mathsf\{TREE\}\; :=\; \backslash lambda\; A\; :\; *\; .\; \backslash Pi\; B\; .\; (A\; \backslash to\; B)\; \backslash to\; (B\; \backslash to\; B\; \backslash to\; B)\; \backslash to\; B$, where "$A:*$" informally means "$A$ is a type". This is a function that takes a type parameter $A$ as an argument and returns the type of $\backslash mathsf\{TREE\}$s of values of type $A$. 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$\backslash underline\{\backslash omega\}$ is generally not used on its own, but is useful to isolate the independent feature of type constructors.{{harvnb|Nederpelt|Geuvers|2014|p=100}}

In the λP system, also named λΠ, and closely related to the LF Logical Framework, one has so called dependent types. These are types that are allowed to depend on terms. The crucial introduction rule of the system is

$\backslash frac\{\backslash Gamma,\; x\; :\; A\; \backslash ;\backslash vdash\backslash ;\; B\; :\; *\}\{\backslash Gamma\; \backslash ;\backslash vdash\backslash ;\; (\backslash Pi\; x\; :\; A\; .\; B)\; :\; *\}$

where $*$ represents valid types. The new type constructor $\backslash Pi$ corresponds via the Curry-Howard isomorphism to a universal quantifier, and the system λP as a whole corresponds to first-order logic 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.

System Fω combines both the $\backslash Lambda$ constructor of System F and the type constructors from System F$\backslash underline\{\backslash omega\}$. Thus System Fω provides both terms that depend on types and types that depend on types.

In the calculus of constructions, denoted as λC in the cube or as λPω,{{rp|130}} 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 $\backslash square$ are themselves terms with a type.

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, and then typing rules that allow to type those terms.

The set of sorts is defined as $S\; :=\; \backslash \{*,\; \backslash square\; \backslash \}$, sorts are represented with the letter $s$. There is also a set $V$ of variables, represented by the letters $x,y,\backslash dots$. The raw terms of the eight systems of the cube are given by the following syntax:

$A\; :=\; x\; \backslash mid\; s\; \backslash mid\; A~A\; \backslash mid\; \backslash lambda\; x\; :\; A\; .\; A\; \backslash mid\; \backslash Pi\; x\; :\; A\; .\; A$

and $A\; \backslash to\; B$ denoting $\backslash Pi\; x\; :\; A\; .\; B$ when $x$ does not occur free in $B$.

The environments, as is usual in typed systems, are given by

$\backslash Gamma\; :=\; \backslash emptyset\; \backslash mid\; \backslash Gamma,\; x\; :\; A$

The notion of β-reduction is common to all systems in the cube. It is written $\backslash to\_\{\backslash beta\}$ and given by the rules$$\backslash frac\{\}\{(\backslash lambda\; x\; :\; A\; .\; B)~C\; \backslash to\_\{\backslash beta\}\; B[C/x]\}$$$$\backslash frac\{B\; \backslash to\_\{\backslash beta\}\; B\text{'}\}\{\backslash lambda\; x\; :\; A\; .\; B\; \backslash to\_\{\backslash beta\}\; \backslash lambda\; x\; :\; A\; .\; B\text{'}\}$$$$\backslash frac\{A\; \backslash to\_\{\backslash beta\}\; A\text{'}\}\{\backslash lambda\; x\; :\; A\; .\; B\; \backslash to\_\{\backslash beta\}\; \backslash lambda\; x\; :\; A\text{'}\; .\; B\}$$$$\backslash frac\{B\; \backslash to\_\{\backslash beta\}\; B\text{'}\}\{\backslash Pi\; x\; :\; A\; .\; B\; \backslash to\_\{\backslash beta\}\; \backslash Pi\; x\; :\; A\; .\; B\text{'}\}$$$$\backslash frac\{A\; \backslash to\_\{\backslash beta\}\; A\text{'}\}\{\backslash Pi\; x\; :\; A\; .\; B\; \backslash to\_\{\backslash beta\}\; \backslash Pi\; x\; :\; A\text{'}\; .\; B\}$$Its reflexive, transitive closure is written $=\_\backslash beta$.

The following typing rules are also common to all systems in the cube:$$\backslash frac\{\}\{\backslash vdash\; *\; :\; \backslash square\}\backslash quad\; \backslash text\{(Axiom)\}$$$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\}\{\backslash Gamma,\; x\; :\; A\; \backslash vdash\; x\; :\; A\; \}\; x\; \backslash not\backslash in\; \backslash Gamma\; \backslash quad\; \backslash text\{(Start)\}$$$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; C\; :\; s\}\{\backslash Gamma,\; x\; :\; C\; \backslash vdash\; A\; :\; B\}\; x\; \backslash not\backslash in\; \backslash Gamma\; \backslash quad\; \backslash text\{(Weakening)\}$$$$\backslash frac\{\backslash Gamma\; \backslash vdash\; C\; :\; \backslash Pi\; x\; :\; A\; .\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; D\; :\; A\}\{\backslash Gamma\; \backslash vdash\; CD\; :\; B[D/x]\}\backslash quad\backslash text\{(Application)\}$$$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; B\; \backslash quad\; B\; =\_\{\backslash beta\}\; B\text{'}\; \backslash quad\; \backslash Gamma\; \backslash vdash\; B\text{'}\; :\; s\}\{\backslash Gamma\; \backslash vdash\; A\; :\; B\text{'}\}\backslash quad\backslash text\{(Conversion)\}$$

The difference between the systems is in the pairs of sorts $(s\_1,s\_2)$ that are allowed in the following two typing rules:$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; :\; s\_2\}\{\backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A\; .\; B\; :\; s\_2\}\backslash quad\backslash text\{(Product)\}$$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; :\; C\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; C\; :\; s\_2\}\{\backslash Gamma\; \backslash vdash\; \backslash lambda\; x\; :\; A\; .\; B\; :\; \backslash Pi\; x\; :\; A\; .\; C\}\backslash quad\backslash text\{(Abstraction)\}$

The correspondence between the systems and the pairs $(s\_1,s\_2)$ 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.
• $(*,\backslash square)$ allows types to depend on terms.
• $(\backslash square,\; *)$ allows terms to depend on types.
• $(\backslash square,\; \backslash square)$ allows types to depend on types.

A typical derivation that can be obtained is$$\backslash alpha\; :\; *\; \backslash vdash\; \backslash lambda\; x\; :\; \backslash alpha\; .\; x\; :\; \backslash Pi\; x\; :\; \backslash alpha\; .\; \backslash alpha$$or with the arrow shortcut$$\backslash alpha\; :\; *\; \backslash vdash\; \backslash lambda\; x\; :\; \backslash alpha\; .\; x\; :\; \backslash alpha\; \backslash to\; \backslash alpha$$closely resembling the identity (of type $\backslash alpha$) 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 $\backslash vdash\; *\; :\; \backslash square$.

The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator).{{Cite journal |last=Schwichtenberg |first=Helmut |author-link=Helmut Schwichtenberg |date=1975 |title=Definierbare Funktionen imλ-Kalkül mit Typen |journal=Archiv für Mathematische Logik und Grundlagenforschung |volume=17 |issue=3–4 |pages=113–114 |doi=10.1007/bf02276799 |s2cid=11598130 |issn=0933-5846 |language=DE}}

In λ2, such terms can be obtained as$$\backslash vdash\; (\backslash lambda\; \backslash beta\; :\; *\; .\; \backslash lambda\; x\; :\; \backslash bot\; .\; x\; \backslash beta)\; :\; \backslash Pi\; \backslash beta\; :\; *\; .\; \backslash bot\; \backslash to\; \backslash beta$$with $\backslash bot\; =\; \backslash Pi\; \backslash alpha\; :\; *\; .\; \backslash alpha$. If one reads $\backslash Pi$ 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 types such as $\backslash bot$, 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.{{cite book |first1=Jean-Yves |last1=Girard |first2=Yves |last2=Lafont |first3=Paul |last3=Taylor |title=Proofs and Types |publisher=Cambridge University Press |year=1989 |isbn=9780521371810 |volume=7 |series=Cambridge Tracts in Theoretical Computer Science }} In particular, all primitive recursive functions are definable.

In λP, the ability to have types depending on terms means one can express logical predicates. For instance, the following is derivable:$$\backslash begin\{array\}\{l\}\backslash alpha\; :\; *,\; a\_0\; :\; \backslash alpha,\; p\; :\; \backslash alpha\; \backslash to\; *,\; q\; :\; *\; \backslash vdash\; \backslash \backslash \; \backslash quad\; \backslash lambda\; z\; :\; (\backslash Pi\; x\; :\; \backslash alpha\; .\; p\; x\; \backslash to\; q)\; .\; \backslash \backslash \; \backslash quad\; \backslash lambda\; y\; :\; (\backslash Pi\; x\; :\; \backslash alpha\; .\; p\; x)\; .\; \backslash \backslash \; \backslash quad\; (z\; a\_0)\; (y\; a\_0)\; :\; (\backslash Pi\; x\; :\; \backslash alpha\; .\; p\; x\; \backslash to\; q)\; \backslash to\; (\backslash Pi\; x\; :\; \backslash alpha\; .\; p\; x)\; \backslash to\; q\; \backslash end\{array\}$$which corresponds, via the Curry-Howard isomorphism, to a proof of $(\backslash forall\; x\; :\; A,\; P\; x\; \backslash to\; Q)\; \backslash to\; (\backslash forall\; x\; :\; A,\; P\; x)\; \backslash to\; Q$.
From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties.{{Cite book|title=Lambda-Prolog de A à Z ... ou presque|last=Ridoux|first=Olivier|date=1998|publisher=[s.n.]|oclc=494473554|url=ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf }}

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 one has $\backslash Gamma\; \backslash vdash\; A\; :\; P((\backslash lambda\; x\; .\; x)y)$ and $\backslash Gamma\; \backslash vdash\; B\; :\; \backslash Pi\; x\; :\; P(y)\; .\; C$, one needs to apply the conversion rule{{efn|name= dependentTypeConvent|1=

The assumption $\backslash Gamma\; \backslash vdash\; B\text{'}\; :\; s$ in the Conversion rule is a convenience; one could prove a meta-theorem that $\backslash Gamma\; \backslash vdash\; A\; :\; B\; \backslash land\; B\; =\_\{\backslash beta\}\; B\text{'}\; \backslash Rightarrow\; \backslash Gamma\; \backslash vdash\; B\text{'}\; :\; s$ instead.{{cite book

| last1 = Angiuli

| first1 = Carlo

| last2 = Gratzer

| first2 = Daniel

| title = Principles of Dependent Type Theory

| publisher = Indiana University and Aarhus University

| year = 2024

| url = https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf

| chapter = 2.1.3 Who type-checks the typing rules? and 2.2 Towards the syntax of dependent type theory

| access-date = 7 September 2024

}}{{cite web

| last = Favier

| first = Naïm

| title = In the Conversion inference rule of the lambda cube, why is Γ ⊢ B′:s necessary?

| website = Computer Science Stack Exchange

| date = August 17, 2023

| url = https://cs.stackexchange.com/a/169633/174020

| access-date = September 7, 2024

}}}} to obtain $\backslash Gamma\; \backslash vdash\; A\; :\; P(y)$ to be able to type $\backslash Gamma\; \backslash vdash\; B\; A\; :\; C$.

In λω, the following operator$$AND\; :=\; \backslash lambda\; \backslash alpha\; :\; *\; .\; \backslash lambda\; \backslash beta\; :\; *\; .\; \backslash Pi\; \backslash gamma\; :\; *\; .\; (\backslash alpha\; \backslash to\; \backslash beta\; \backslash to\; \backslash gamma)\; \backslash to\; \backslash gamma$$is definable, that is $\backslash vdash\; AND\; :\; *\; \backslash to\; *\; \backslash to\; *$. The derivation$$\backslash alpha\; :\; *,\; \backslash beta\; :\; *\; \backslash vdash\; \backslash Pi\; \backslash gamma\; :\; *\; .\; (\backslash alpha\; \backslash to\; \backslash beta\; \backslash to\; \backslash gamma)\; \backslash to\; \backslash gamma\; :\; *$$can be obtained already in λ2, however the polymorphic $AND$ can only be defined if the rule $(\backslash square,\; *)$ is also present.

From a computing point of view, λω is extremely strong, and has been considered as a basis for programming languages.{{Cite book|title=Programming in higher-order typed lambda-calculi |last1=Pierce |first1=Benjamin |first2=Scott |last2=Dietzen |first3=Spiro |last3=Michaylov |date=1989 |publisher=Computer Science Department, Carnegie Mellon University |id=CMU-CS-89-111 ERGO-89-075 |oclc=20442222}}

The calculus of constructions has both the predicate expressiveness of λP and the computational power of λω, hence why λC is also called λPω,{{rp|130}} so it is very powerful, both on the logical side and on the computational side.

The system Automath 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 $\backslash square$, and the ability to construct inductive types.

Pure type systems 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 $\backslash \{*,\; \backslash square\backslash \}$, the only axiom $\backslash \{*,\backslash square\backslash \}$, and a set of rules $R$ such that $\backslash \{(*,*,*)\backslash \}\; \backslash subseteq\; R\; \backslash subseteq\; \backslash \{(*,*,*),\; (*,\backslash square,\; \backslash square),\; (\backslash square,\; *,\; *),\; (\backslash square,\; \backslash square,\; \backslash square)\; \backslash \}$.

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 $\backslash to$ and $\backslash forall$), however one can define other connectives such as $\backslash wedge$ or $\backslash neg$ in an impredicative 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.

All systems in the cube enjoy

• the Church-Rosser property: if $M\; \backslash to\_\backslash beta\; N$ and $M\; \backslash to\_\backslash beta\; N\text{'}$ then there exists $N$ such that $N\; \backslash to^*\_\backslash beta\; N$ and $N\text{'}\; \backslash to^*\_\backslash beta\; N\text{'}\text{'}$;
• the subject reduction property: if $\backslash Gamma\; \backslash vdash\; M\; :\; T$ and $M\; \backslash to\_\backslash beta\; M\text{'}$ then $\backslash Gamma\; \backslash vdash\; M\text{'}\; :\; T$;
• the uniqueness of types: if $\backslash Gamma\; \backslash vdash\; A\; :\; B$ and $\backslash Gamma\; \backslash vdash\; A\; :\; B\text{'}$ then $B\; =\_\backslash beta\; B\text{'}$.

All of these can be proven on generic pure type systems.{{Cite book |last1=Sørensen|first1=Morten Heine|chapter=Pure type systems and the λ-cube|date=2006|title=Lectures on the Curry-Howard Isomorphism|pages=343–359|publisher=Elsevier|isbn=9780444520777|last2=Urzyczyin|first2=Pawel|doi=10.1016/s0049-237x(06)80015-7}}

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 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.{{Cite book|title=Types and programming languages|last=Pierce|first=Benjamin|date=2002|publisher=MIT Press|isbn=978-0262162098|pages=467–490|oclc=300712077 }}

The idea of the cube is due to the mathematician Henk Barendregt (1991). The framework of pure type systems 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.{{harvnb|Pierce|2002|p=466}} 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.

• In his Habilitation à diriger les recherches,{{harvnb|Ridoux|1998|p=70}} 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.
• Logical cube
• Logical hexagon
• Square of opposition
• Triangle of opposition

{{reflist}}

{{notelist}}

• {{cite web |first1=Simon |last1=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 |website=Microsoft |quote=Henk is based directly on the lambda cube, an expressive family of typed lambda calculi. }}

• [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube] in the context of pure type systems by Roger Bishop Jones

Category:Lambda calculus

Category:Type theory