I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong Normalization for the Calculus of Constructions".

I can follow the main line of reasoning well. Geuvers constructs for each type $T$ an interpretation $[\![T]\!]_\xi$ based on some evaluation of type variables $\xi(\alpha)$. And then he constructs some term interpretation $(\!|M|\!)_\rho$ based on some evaluation of term variables $\rho(x)$ and proves that for valid evaluations the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for all $\Gamma\vdash M:T$ holds.

My problem: For easy types (like system F types) the type interpretation $[\![T]\!]_\xi$ is really a set of terms, so the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ makes sense. But for more complex types the interpretation $[\![T]\!]_\xi$ is not a set of terms but a set of functions of some appropriate function space. I think, I almost understand the construction of the function spaces, however it cannot assign any meaning to $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for the more complex types $T$.

Can anybody explain or give links to some more understandable presentations of the proof?

Edit: Let me try to make the question clearer. A context $\Gamma$ has declarations for type variables $\alpha:A$ and object variables. A type valuation is valid, if for all $(\alpha:A) \in \Gamma$ with $\Gamma\vdash A:\square$ then $\xi(\alpha) \in \nu(A)$ is valid. But $\nu(A)$ can be an element of $(SAT)^*$ and not only $SAT$. Therefore no valid term evaluation can be defined for $\rho(\alpha)$. $\rho(\alpha)$ must be a term and not some function of a function space.

Edit 2: Example which does not work

Let's make the following valid derivation: $$ \begin{array}{llll} [] &\vdash & *:\square &\text{axiom} \\ [\alpha:*] &\vdash& \alpha:* &\text{variable introduction} \\ [\alpha:*] &\vdash& *:\square &\text{weaken} \\ [] &\vdash & (\Pi \alpha:*.*):\square &\text{product formation} \\ [\beta:\Pi \alpha:*.*] &\vdash& \beta:(\Pi \alpha:*.*) &\text{variable introduction} \end{array} $$

In the last context a valid type evaluation must satisfy $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$. For this type evaluation there is no valid term evaluation.

  • 1
    $\begingroup$ Half the people reading this will think that $SAT$ is SAT. You should explain what it is. Also, your derivation seems a bit odd. The second line should not mention $\alpha$ in its conclusion, it shoudl read something like $[\alpha : *] \vdash * : \Box$, should it not? $\endgroup$ – Andrej Bauer Nov 5 '18 at 7:38
  • $\begingroup$ I am using the notation of Herman Geuvers (which seems to be standard in this domain). $\text{SAT}$ is the set of all saturated sets of lambda expressions. For the second line of my derivation: Its the introduction rule for variables of a pure type system. This rule reads $\frac{\Gamma \vdash T:s}{\Gamma,x:T\vdash x:T}$ where $s$ is some sort. $\endgroup$ – helmut Nov 5 '18 at 13:47
  • $\begingroup$ I understand how you got the second line but it is not the correct premise for the formation of the third line, is it? What rule gives the third line. $\endgroup$ – Andrej Bauer Nov 5 '18 at 18:14
  • $\begingroup$ The product formation rule of PTS says $\frac{r(s_1,s_2,s_3;\, \Gamma\vdash A:s_1;\: \Gamma,x:A\vdash B:s_2}{\Gamma\vdash (\Pi x:A.B): s_3}$. The calculus of constructions has the rule $r(*,*,*)$. This allows me using the first and the second line to derive the third. However I had a typo in my post. The type in the third line had been missing which I added now. $\endgroup$ – helmut Nov 5 '18 at 20:05
  • $\begingroup$ Shouldn't then the first line read $[] \vdash * : *$? Or did you mix up $*$ and $\Box$ somewhere? The second line cannot be the second premise to the product formation rule, because that would mean you're trying to form something like $\prod \alpha : * . \alpha$ instead of $\prod \alpha : * . *$. $\endgroup$ – Andrej Bauer Nov 5 '18 at 20:43

Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating detail.

I'm not sure I understand the gist of your confusion, but I think one important thing to note, is the following lemma (Corollary 5.2.14), proven in the classic Barendregt text:

$$\Gamma \vdash M:T\ \Rightarrow\ \Gamma \vdash T:*\mbox{ or }\square $$

This means that while $[\![T]\!]_\xi$ can be some complicated function, if $\Gamma \vdash M:T$ holds, then $[\![T]\!]_\xi$ has to be a set of terms.

This is insinuated in the outline (section 3.1), where $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ only if $\Gamma \vdash t:T :*$, which lines up with our expectation, which is that the interpretation of a type must be a set of terms, i.e. ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ (indeed, ${\cal V}(*)=\mathrm{SAT}$!)

It's a common situation in type theory that even though we're only interested in the "base kind" (here $*$), we still have to define semantics for things at higher kinds (hence the need to introduce $\mathrm{SAT}^*$). Things then work out at the end, because only kind which inhabited by types is $*$ (and $\square$, but that's not really important).

  • 1
    $\begingroup$ Thanks for the explanation. That solves my problem of not understanding the functions used in Geuver's proof. I had already a suspicion from reading and rereading Geuver's paper, but you made it crystal clear. $\endgroup$ – helmut Nov 7 '18 at 14:40

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.