Editing Lambda cube (section)

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

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

<math>A := x \mid s \mid A~A \mid \lambda x : A . A \mid \Pi x : A . A</math>

and <math>A \to B</math> denoting <math>\Pi x : A . B</math> when <math>x</math> does not occur free in <math>B</math>.

The environments, as is usual in typed systems, are given by
<math>\Gamma := \emptyset \mid \Gamma, x : A</math>

The notion of β-reduction is common to all systems in the cube. It is written <math>\to_{\beta}</math> and given by the rules<math display="block">\frac{}{(\lambda x : A . B)~C \to_{\beta} B[C/x]}</math><math display="block">\frac{B \to_{\beta} B'}{\lambda x : A . B \to_{\beta} \lambda x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\lambda x : A . B \to_{\beta} \lambda x : A' . B}</math><math display="block">\frac{B \to_{\beta} B'}{\Pi x : A . B \to_{\beta} \Pi x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\Pi x : A . B \to_{\beta} \Pi x : A' . B}</math>Its [[Reflexive transitive closure|reflexive, transitive closure]] is written <math>=_\beta</math>.

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

The difference between the systems is in the pairs of sorts <math display="inline">(s_1,s_2)</math> that are allowed in the following two typing rules:<math display="block">\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash \Pi x : A . B : s_2}\quad\text{(Product)}</math><math>\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : C \quad \Gamma, x : A \vdash C : s_2}{\Gamma \vdash \lambda x : A . B : \Pi x : A . C}\quad\text{(Abstraction)}</math>

The correspondence between the systems and the pairs <math display="inline">(s_1,s_2)</math> allowed in the rules is the following:
{| class="wikitable"
!<math>(s_1, s_2)</math>
!<math>(*,*)</math>
!<math>(*,\square)</math>
!<math>(\square,*)</math>
!<math>(\square,\square)</math>
|-
|λ→
|{{ya}}
|{{na}}
|{{na}}
|{{na}}
|-
|λP
|{{ya}}
|{{ya}}
|{{na}}
|{{na}}
|-
|λ2
|{{ya}}
|{{na}}
|{{ya}}
|{{na}}
|-
|λ<u>ω</u>
|{{ya}}
|{{na}}
|{{na}}
|{{ya}}
|-
|λP2
|{{ya}}
|{{ya}}
|{{ya}}
|{{na}}
|-
|λP<u>ω</u>
|{{ya}}
|{{ya}}
|{{na}}
|{{ya}}
|-
|λω
|{{ya}}
|{{na}}
|{{ya}}
|{{ya}}
|-
|λC
|{{ya}}
|{{ya}}
|{{ya}}
|{{ya}}
|}

Each direction of the cube corresponds to one pair (excluding the pair <math display="inline">(*,*)</math> shared by all systems), and in turn each pair corresponds to one possibility of dependency between terms and types:

* <math display="inline">(*,*)</math> allows terms to depend on terms.
* <math display="inline">(*,\square)</math> allows types to depend on terms.
* <math display="inline">(\square, *)</math> allows terms to depend on types.
* <math display="inline">(\square, \square)</math> allows types to depend on types.