Editing Lambda cube (section)

==Comparison between the systems==

===λ→===

A typical derivation that can be obtained is<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \Pi x : \alpha . \alpha</math>or with the arrow shortcut<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \alpha \to \alpha</math>closely resembling the identity (of type <math display="inline">\alpha</math>) 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 <math display="inline">\vdash * : \square</math>.

The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator).<ref>{{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}}</ref>

===λ2===

In λ2, such terms can be obtained as<math display="block">\vdash (\lambda \beta : * . \lambda x : \bot . x \beta) : \Pi \beta : * . \bot \to \beta</math>with <math display="inline">\bot = \Pi \alpha : * . \alpha</math>. If one reads <math display="inline">\Pi</math> 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 [[Impredicativity|impredicative]] types such as <math display="inline">\bot</math>, that is terms quantifying over all types including themselves.<br />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]].<ref>{{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 }}</ref> 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:<math display="block">\begin{array}{l}\alpha : *, a_0 : \alpha, p : \alpha \to *, q : * \vdash \\ \quad \lambda z : (\Pi x : \alpha . p x \to q) . \\ \quad \lambda y : (\Pi x : \alpha . p x) . \\ \quad (z a_0) (y a_0) : (\Pi x : \alpha . p x \to q) \to (\Pi x : \alpha . p x) \to q \end{array}</math>which corresponds, via  the Curry-Howard isomorphism, to a proof of <math>(\forall x : A, P x \to Q) \to (\forall x : A, P x) \to Q</math>.<br />From the computational point of view, however, having dependent types does not enhance computational power, only the possibility to express more precise type properties.<ref name=":1">{{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 }}</ref>

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 <math>\Gamma \vdash A : P((\lambda x . x)y)</math> and <math>\Gamma \vdash B : \Pi x : P(y) . C</math>, one needs to apply the conversion rule{{efn|name= dependentTypeConvent|1= 
The assumption <math>\Gamma \vdash B' : s</math> in the Conversion rule is a convenience; one could prove a meta-theorem that <math>\Gamma \vdash A : B \land B =_{\beta} B' \Rightarrow \Gamma \vdash B' : s</math> instead.<ref>{{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
}}</ref><ref>{{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
}}</ref>}} to obtain <math>\Gamma \vdash  A : P(y)</math> to be able to type <math>\Gamma \vdash B A : C</math>.

===λω===

In λω, the following operator<math display="block">AND := \lambda \alpha : * . \lambda \beta : * . \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma</math>is definable, that is <math>\vdash AND : * \to * \to *</math>. The derivation<math display="block">\alpha : *, \beta : * \vdash \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma : *</math>can be obtained already in λ2, however the polymorphic <math display="inline">AND</math> can only be defined if the rule <math display="inline">(\square, *)</math> is also present.

From a computing point of view, λω is extremely strong, and has been considered as a basis for programming languages.<ref>{{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}}</ref>

===λC===

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