Lambda cube

λ cc An arrow along each edge indicates the direction of inclusion; a simpler system is a special case of a more complex one.

Lambda cube ( λ-cube ) is a visual classification of eight typed lambda calculi with explicit type assignment ( Church typed systems). The cube is organized in accordance with the possible dependencies between the types and terms of this calculus and forms a natural structure for calculus of constructions . The idea of a λ-cube was proposed in 1991 by the Dutch logician and mathematician Henk Barendregt .

Content

Λ-cube structure

In λ-cube systems, variables are assigned to one of two varieties: $\ast$ ${\ displaystyle \ ast}$ or $\Box$ ${\ displaystyle \ Box}$ . All valid expressions are also sorted. The statement that the expression belongs to the variety is built on the statement of typification, that is, the statement $A : B : C$ ${\ displaystyle A: B: C}$ read like this: element $A$ ${\ displaystyle A}$ has type $B$ ${\ displaystyle B}$ and belongs to the grade $C$ ${\ displaystyle C}$ . Grade $\ast$ ${\ displaystyle \ ast}$ used for ordinary variables and terms of λ-calculus, sort $\Box$ ${\ displaystyle \ Box}$ - for variables and type expressions. Therefore, in the systems of the λ-cube, the types of the variety $\ast$ ${\ displaystyle \ ast}$ and grade elements $\Box$ ${\ displaystyle \ Box}$ are considered as intersecting. For example, term type $(\lambda x:\alpha .\,x):(\alpha \to \alpha ):\ast$ ${\ displaystyle (\ lambda x: \ alpha. \, x): (\ alpha \ to \ alpha): \ ast}$ can be written as an element of a "higher" grade $(\alpha \to \alpha ):\ast :\Box$ ${\ displaystyle (\ alpha \ to \ alpha): \ ast: \ Box}$ . Variety Types $\Box$ ${\ displaystyle \ Box}$ sometimes called childbirth .

Dependence refers to the ability to define and use functions that display elements of one sort in another (or the same). Variety Elements $s_{1}$ ${\ displaystyle s_ {1}}$ depend on the elements of the variety $s_{2}$ ${\ displaystyle s_ {2}}$ , if:

for a valid expression $F[x]:\tau :s_{1}$ ${\ displaystyle F [x]: \ tau: s_ {1}}$ possibly containing a variable $x:\sigma :s_{2}$ ${\ displaystyle x: \ sigma: s_ {2}}$ we can define a lambda abstraction $(\lambda x:\sigma .\,F[x]):(\sigma \to \tau ):s_{1}$ ${\ displaystyle (\ lambda x: \ sigma. \, F [x]): (\ sigma \ to \ tau): s_ {1}}$ ;
for function $G:(\sigma \to \tau ):s_{1}$ ${\ displaystyle G: (\ sigma \ to \ tau): s_ {1}}$ its application to an element must be permissible $Y:\sigma :s_{2}$ ${\ displaystyle Y: \ sigma: s_ {2}}$ , while the result should be an element of type $\tau$ ${\ displaystyle \ tau}$ varieties $s_{1}$ ${\ displaystyle s_ {1}}$ , i.e $(G\,Y):\tau :s_{1}$ ${\ displaystyle (G \, Y): \ tau: s_ {1}}$ .

The base vertex of the cube is the system $\lambda ^{\rightarrow }$ ${\ displaystyle \ lambda ^ {\ rightarrow}}$ corresponding to a simply typed lambda calculus . Terms (grade elements $\ast$ ${\ displaystyle \ ast}$ ) depend on terms; types (grade elements $\Box$ ${\ displaystyle \ Box}$ ) do not participate in dependencies. The three axes emerging from the base vertex generate the following systems:

type-dependent terms: system $\lambda 2$ ${\ displaystyle \ lambda 2}$ (lambda calculus with polymorphic types, system F );
type dependent types: system $\lambda {\underline {\omega }}$ ${\ displaystyle \ lambda {\ underline {\ omega}}}$ (lambda calculus with operators over types);
term dependent types: system $\lambda P$ ${\ displaystyle \ lambda P}$ (lambda calculus with dependent types ).

The remaining systems are various combinations of these dependencies. Richest system $\lambda P\omega$ ${\ displaystyle \ lambda P \ omega}$ (polymorphic lambda calculus of higher order with dependent types) is actually a calculus of constructions .

Properties of λ-cube systems

All lambda cube systems have the property of strong normalization : any admissible term (and type) for a finite number of β-reductions is reduced to a single normal form.

Support in programming languages

Different functional languages support a different subset of the type systems represented in the lambda cube.

Haskell , ML - λ2 ( system F )
In a limited form, Haskell (in the GHC implementation since the latest versions) supports $\lambda {\underline {\omega }}$ ${\ displaystyle \ lambda {\ underline {\ omega}}}$ using type families.
Coq , Agda - $\lambda P\omega$ ${\ displaystyle \ lambda P \ omega}$ ( calculus of constructions )

Links

Henk Barendregt, Lambda Calculi with Types (English) , Handbook of Logic in Computer Science, Volume II, Oxford University Press.
Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate Language
Lennart Augustsson, 2007. Simpler, Easier! (English) Description of the implementation of lambda cube systems in the Haskell language.
Lambda cube on SpbHUG (Russian) with translation by Denis Moskvin of the section on lambda cube from the book Henk Barendregt, Lambda Calculi with Types