10  Normalisation for terms

In the previous section we defined the translation   X  of each type X simply by erasing comprehensions. Although the inclusion map i_X:X↣  X  was more complicated, we shall now see that the corresponding translation   a  of terms is equally simple: erase the connectives i and admit, but replace (the in any case unnatural) I with   E .

Notation 10.1 By structural recursion on terms, we define the translation

For the variable x:X, the symbol   x  (either as a term or as a λ-binding) is not a translation as such, but a new variable of type   X . We shall also define

Notice that focus is not translated into focus, and we shall not allow terms to involve it in the main part of the discussion. The problem is that the translation Γ⊢  P :Σ²  X  does not respect the equation that says that P is prime and so justifies use of the focus operator. However, from Lemma 8.13 and Proposition A 8.10, focus is only needed on the outside of a term, and then only for type ℕ, so we shall deal with it separately at the end of the section.

Notation 10.2 For any context Γ, define Γ by replacing each typed variable x:X in Γ by   x :  X . Similarly, let i_Γ:Γ↣Γ be the list of [i_X(x)/  x ]:X↣  X . We write i_X^* and i_Γ^* for the substitutions that relate terms involving these free variables, whereas Σ^i_X relates the corresponding λ-abstractions, cf. Lemma 10.7 below. Hence

Most of this section is devoted to proving

Theorem 10.3 For any term Γ⊢ a:X in the comprehension calculus without focus, Γ⊢  a :  X  is well formed in the original calculus, whilst

are provable in the comprehension calculus, i.e. the square

commutes. The two forms are equivalent by the {}β and {}η rules, Lemmas 9.9 and 9.10.

In particular, if Γ and X don’t involve comprehension then Γ⊢ a=  a :X.

The proof is by structural induction on the term Γ⊢ a:X, and therefore has a case for each connective: λ, i, admit, I, etc. Each of these cases is a lemma below, whereas the lemmas in the previous section were self-contained. To avoid repetitious language, the enunciation of each lemma is simply the introduction or elimination rule that defines the connective; by this we mean to assert that “if the premises (sub-terms) obey the equation a=admit_X(i_Γ^*  a ) then so does the conclusion”.

Since the transformation is also applied to nuclei (Lemma 10.10), the proof is actually on the history of formation of a, rather than simply on the expression without type annotations.

Variables, constants and algebraic operations

Lemma 10.4 For x:X⊢ x:X, we have admit_X(i_X^*  x ) = x.

Proof    i_X^*  x  = [i_X x/  x ]^*  x  = i_X x, and admit_X(i_X x)=x by Lemma 9.10 ({}η for X).         ▫

There is nothing to prove for the constants ⊤, ⊥ and 0, and almost nothing for succ, so we just consider ∧ as (an example of) an algebraic operation.

Lemma 10.5

Recall from the statement of Theorem 10.3 that, by displaying this rule, we mean to claim that if φ and ψ satisfy a certain equation then so does φ∧ψ.

Proof    The general plan is to expand the term in the conclusion of the rule (here φ∧ψ), using the induction hypothesis for the sub-terms (here φ and ψ) and the formulae for admit (Notation 9.2) and i_Γ^* (Notation 10.2), then apply the extended “rules” from the previous section, followed by the same procedure in reverse to obtain the translation of the term in question.

Lemma 10.6

Proof    

The lambda calculus

The difference between Σ^i_Y and i_Y^* is that Σ^i_Y acts on the exponent of the type by λ-reduction, whilst i_Y^* acts on the context by substitution.

Lemma 10.7 If Γ,   y :  Y ⊢θ:Σ  ^Z  then Γ⊢Σ^{i_Y× i_Z}λ  y .θ = λ y.Σ^i_Zi_Y^*θ:Σ^{Y× Z}.

Proof    

Lemma 10.8

Proof    We use Lemma 10.7 with Γ,   y :  Y ⊢θ  ≡ i_Γ^*  φ :Σ  ^Z .

Lemma 10.9

Proof    

Subtypes

Here is where we use the main induction hypothesis in Theorem 10.3 for the nucleus E that defines the subtype {X ∣ E}. The prohibition on focus is not a problem: it can be eliminated, as the type of E is Σ^X (Proposition A 8.10).

Lemma 10.10     Σ^i_X·  E =E·Σ^i_X and E_{{X ∣ E}}=I_X· E·Σ^i_X=  E .

Proof    The induction hypothesis for Eφ and φ yields

so E(Σ^i_X  φ )  =  Σ^i_X(  E   φ ), which is the first equation. The induction hypothesis also says that E_X=  E_X , since the type of E_X doesn’t involve comprehension. Then

by Notation 10.2 and Lemmas 9.4, 10.9 and 9.8.         ▫

Lemma 10.11

Proof    

Lemma 10.12

Proof    

Lemma 10.13

Proof    

Recursion

Lemma 10.14

[This proof requires equational hypotheses (Remark E 2.7).]

Proof    Let Γ⊢ z′=i_Γ^*  z :  X  and Γ,  m:ℕ,  x :  X  ⊢ s′(m,  x )=i_Γ^*  s (m,  x ):  X .

So the induction hypotheses say that Γ⊢ n=i_Γ^*  n :ℕ,  Γ⊢ z=admit_X z′:X and

We use Lemma 8.14, or rather its analogue with the extended rules of Section 9 in place of the {}β- and η-rules; the symbols   x , z′ and s′ here correspond to y, z and s there.

Sobriety

We have now completed the proof of Theorem 10.3, that, for any term Γ⊢ a:X in the comprehension calculus without focus,

There are two ways of handling a term focusP:ℕ.

Remark 10.15 Lemma 8.11 says that ℕ≅{Σ²ℕ ∣ E_ℕ}, where E_ℕ characterises primes. This makes use of admit instead of focus. More generally, {ℕ ∣ E}≅{Σ²ℕ ∣ E′}, where E′ encodes the composite inclusion. Another way of saying this is that, in Notation 9.2, we define the base case ℕ as Σ²ℕ instead of ℕ. This way we only ever deal with subspaces of injectives (cf. Corollary 5.3), and never need to use focus.

Remark 10.16 Alternatively, if Γ⊢ P:Σ² X is a prime not involving focus,

Lemma A 8.4 actually said

and we’re trying to use its converse, which is not valid. Although Γ⊢ i_Γ^*  P :Σ²  X  is prime, Γ⊢  P :Σ²  X  need not be. This is why we write force instead of focus here.

Semantically, Γ↣Γ is a subspace, on which the relevant equation holds, but it need not hold on the ambient space Γ. That such a situation arises is more obvious for descriptions (Remark A 9.13): any predicate Γ⊢φ:Σ^ℕ becomes a description when restricted to the locally closed subspace Γ↣Γ defined by

In the terms of this paper, the equation in Definition 4.5 defining a (prime or) homomorphism on a subspace {Y₁ ∣ E₁} involves E₁, and does not imply the form without it.

Nevertheless, it is a legitimate alternative way of treating focusP to translate it into force  P . For, if Γ⊢ψ:Σ^X then

using the unrestricted β-rule for force.

As we know from Section A 8 and 11, and the work on computational effects cited there, we may obtain different terms Γ⊢  a :  X  by applying or reversing the β- and η-rules of the λ-calculus with force. So, for such a calculus to be defined consistently, an order of evaluation must be specified.

However, these computational terms with possibly different denotations on Γ become equal when we apply i_Γ^* to restrict them to the required context Γ. In other words, as we know very well from experience, there are different programs Γ⊢  a :  X , possibly involving computational effects, to compute the same denotational value Γ⊢ a:X.

Categorical equivalence

Theorem 10.17 Let S and D be the categories generated by the restricted λ-calculus (possibly with the extra structure) and the comprehension calculus. Then there is an equivalence of categories S≃D whose effect on types is

where the notation {X ∣ E} in S is the categorical one in Section 4, whilst in D it is understood as the comprehension calculus in Section 8.

Proof    The previous section defined the transformation D→S on types, and showed that the composite D→S→D is isomorphic to the identity: Proposition 9.11 provided mutually inverse terms in the comprehension calculus that relate any type X to {  X  ∣ E_X}. The other composite is the identity on types, so we just have to show that S→D is full and faithful.

Let X₁ and X₂ be types that are defined without comprehension, and E₁ and E₂ nuclei on them. We shall show that there is a bijection between the S-morphisms

defined in Section 4 and the terms

that we have just expressed in normal form. Of course   {X₁ ∣ E₁} =X₁, and we write i₁=i_X1, etc.

In each of the categories, these morphisms correspond bijectively to homomorphisms

but first we consider ordinary maps, without the homomorphism requirement.

By Proposition 6.2 for S, Σ^{{X ∣ E}}≅{Σ^X ∣ Σ^E}, which is simply a retract of the power type Σ^X in S (the restricted λ-calculus), so a S-morphism J:Σ^{{X₂ ∣ E₂}}→Σ^{{X₁ ∣ E₁}} is a S-morphism J:Σ^X₂→Σ^X₁ such that E₂;J=J=J;E₁.

The corresponding power type in D is also a retract, and Theorem 10.3 characterised its morphisms H in the same fashion. Hence HS≃HD.

Now, homomorphisms are characterised equationally amongst all maps, and we have already shown that the functor is full and faithful for them, i.e. that maps and their equations agree, so the homomorphisms also agree.

In S, the equation that defines homomorphisms is more clearly understood by means of Lemma 6.6, i.e. with reference to the subtypes {X_i ∣ E_i}, rather than using Definition 4.5, which transfers the condition to the ambient types X_i. We have seen the same phenomenon in D, where the translation   P  of a prime P relative to the sub-types need not be prime with respect to the translated types.

That deals with single-type contexts, but that is enough as products may be encoded as comprehension types in each category.         ▫

Therefore our first construction, adjoining formal Σ-split equalisers to the category in Sections 4–6, is equivalent to the third, the extension of the λ-calculus in Sections 8–10.