Editing Lambda cube (section)

===λ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>.