8  A lambda calculus for sobriety

In this section we show that SC interprets the restricted λ-calculus, together with the new operation focus. For reference, we first repeat the equation in Remark 4.11.

Definition 8.1 Γ⊢ P:Σ^ΣX is prime if  Γ,  F:Σ³ X ⊢ F P   ⇔   P(λ x.F(λφ.φ x)).

Definition 8.2 The sober λ-calculus is the restricted λ-calculus (Definition 2.1) together with the additional rules

focusI

focusβ

T0

The definition thunka = η_X(a) = λ φ.φ a serves as the elimination rule for focus. Using this, equivalent ways of writing the focusβ and η (T₀) rules are

where P is prime.

Remark 8.3 The restriction of focus to primes is the crucial difference from Thielecke’s force calculus, and is the reason why we gave it a new name. In the focusβ-rule, how can we tell how much of the surrounding expression is the predicate φ that is to become the sub-term of P? For example, for F:Σ^Σ,

So long as P is prime, it doesn’t matter, because these terms are equal. In Remark 11.4 we consider briefly what happens if this side-condition is violated.

Proof    The double transpose H:Σ^X→Σ^Γ of P is a homomorphism with respect to the double transpose J:Σ→Σ^Γ of F.         ▫

The interaction of focus with substitution, i.e. cut elimination, brings no surprises.

Lemma 8.4 If Γ⊢ P:Σ² X is prime then so is Δ⊢ (u^*P):Σ² X for any substitution u:Δ→Γ [Tay99, Section 4.3], and then

Proof    In the context [Δ, F:Σ³ X], since x, φ and F don’t depend on Γ,

so u^*P is prime. Then, in the context [Δ, φ:Σ^X],

using the focusβ-rule, whence the substitution equation follows by T₀.         ▫

Theorem 8.5 SC is a model of the sober λ-calculus.

Proof    Since SC has products and powers of Σ (Proposition 6.11 and Corollary 7.2), it is a model of the restricted λ-calculus. Lemma 7.5 provides the interpretation of focusP and (the second form of) its β- and η-rules.         ▫

Remark 8.6 Let C and D be the categories corresponding to the restricted and sober λ-calculi respectively, as in Remark 2.7. Since the calculi have the same types, and so contexts, D has the same objects as C and SC.

We have shown how to interpret focus in SC, and that the equations are valid there. Hence we have the interpretation functor ⟦−⟧:D→SC in the same way as in Proposition 2.8, where ⟦−⟧ acts as the identity on objects (contexts).

Since D interprets focus by definition, all of the objects of D are sober by Corollary 4.12. The universal property of SC (Theorem 7.6) then provides the inverse of the functor ⟦−⟧, making it an isomorphism of categories.

Alternatively, we can show directly that D has the same morphisms as SC, by proving a normalisation result for the sober λ-calculus. Besides being more familiar, this approach demonstrates that we have stated all of the necessary equations in the new calculus. We have already shown that the new calculus is a sound notation for morphisms of the category SC, and it remains to show that this notation is complete.

We can easily extract any sub-term focusP from a term of power type:

Lemma 8.7 φ[focusP] ⇔ P(λ x.φ[x]).

Proof    [focusP/x]^*φ[x] ⇔ (λ x. φ[x])(focusP), where [ ]^* denotes substitution.         ▫

The term φ in focusβ may itself be of the form focusP:

Lemma 8.8 Let Γ⊢ P:Σ³ X (sic) and Γ⊢ Q:Σ² X be primes. Then

This equation for focusP is the one in Proposition 4.9 and Lemma 7.1.

Proof    (focusP)(focusQ)=Q(focusP) ⇔ P Q using focusβ twice.

In particular, put Q=η_X(x)=λφ.φ x, so x=focusQ. Then

from which the result follows by the λη-rule.         ▫

For the extra structure, we need a symbolic analogue of Proposition 7.9, now including the parameters Γ and m:ℕ. Note that S here is the double transpose of the same letter there.

Lemma 8.9 Let Γ ⊢  Z:Σ² X and Γ, m:ℕ,u:X ⊢  S(m,u):Σ² X be prime. Put

Then R_n is prime and Γ, n:ℕ ⊢  r_n=focusR_n.

[This proof requires equational hypotheses in the context: see Remark E 2.7.]

Proof    We prove

by induction on n. For n=0, since Z is prime,

Suppose that R_n = λ φ.φ(r_n) for some particular n. Then

Since R_n is equal to some λφ.φ(a), it is prime, and the required equation follows by focusη.         ▫

Proposition 8.10 Every term Γ⊢ a:X in the sober λ-calculus is provably equal (in that calculus) to

• some term that is already definable in the restricted calculus, if X is Σ^U, so a is logical in the sense of Notation 2.3; or
• focusP, for some prime Γ⊢ P:Σ² X in the restricted λ-calculus, otherwise, i.e. when X=ℕ, so a is numerical.

Cf. Lemmas 7.1 and 1 respectively.

Proof    By structural recursion on the term a.

1. The result is trivial for variables and constants (⊤, ⊥, 0), where P≡η_X(a).
2. If a≡λ u.φ, φ∧ψ, φ∨ψ or ∃ n.φ[n] then the recursion hypothesis says that φ and ψ, being logical, are provably equal to terms in the restricted calculus, whence so is a.
3. If a≡focusP, the recursion hypothesis says that P:Σ² X is provably equal to a term in the restricted calculus (not a focus, as it is logical). Moreover, if a:Σ^U then Lemma 8.8 rewrites it without using focus.
4. If a≡φ u then (by the recursion hypothesis, and as it is logical) φ is (provably equal to a term that is) defined in the restricted calculus. If u:Σ^V then u is too. Otherwise, u=focusP, and then a=φ(focusP)= Pφ by focusβ.
5. rec(focusN,z,s) = focus(λφ.N(λ n.φ[rec(n,z,s)])) by Lemma 8.7, so the first argument of rec need not involve focus.
6. If a≡rec(n,z,s):X then z,s:X, so they are provably equal to terms in the restricted calculus if X=Σ^U, whilst Lemma 8.9 rewrites a if X=ℕ.
7. succ(focusP)=focus(Σ²succ  P), where (Σ²succ)P is prime by the symbolic version of Lemma 4.6.
8. In anticipation of Remark 9.1,

   ((focusP)=ℕ(focusQ))     may be rewritten as     P(λ x.Q(λ y.x=ℕy)),

   using Lemma 8.7 twice, and similarly for ≠.         ▫

Warning 8.11 Once again, this dramatic simplification of the calculus (that focus is only needed at base types such as ℕ) relies heavily on the restriction on the introduction of focusP for primes only, i.e. on working in SC. Hayo Thielecke shows that force is needed at all types in the larger category HC whose morphisms involve control operators [Thi97a, Section 6.5].

Theorem 8.12 If C is the category generated by the restricted λ-calculus in Definition 2.1 then SC is the category generated by the sober λ-calculus. If C has the extra structure in Remarks 2.4ff then so does SC.

So the extension of the type theory is equivalent to the extension of the category.

Proof    We rely on the construction of the category Cn of contexts and substitutions developed in [Tay99], and have to show that the trapezium commutes.

The categories C, SC and D in Remark 8.6 have the same objects. The morphisms of C and D are generated by weakenings and cuts, where weakenings are just product projections. A cut [a/x]:Γ→Γ× X splits the associated product projection, and corresponds to a term Γ⊢ a:X in the appropriate calculus, modulo its equations.

By Proposition 8.10, the term a of the sober calculus is uniquely of the form focusP, where P is a prime defined in the restricted calculus (so the triangle commutes). Hence [a/x] in D corresponds to the SC-morphism <id,H>, where H is the double exponential transpose of P.         ▫