<p>Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try <a href="http://prosecco.gforge.inria.fr/personal/hritcu/temp/snforcc.pdf" rel="noreferrer">this</a> note from Chris Casinghino which gives an account of several proofs in excruciating detail.</p>

<p>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 <a href="http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf" rel="noreferrer">classic Barendregt text</a>:</p>

<p><span class="math-container">$$\Gamma \vdash M:T\ \Rightarrow\ \Gamma \vdash T:*\mbox{ or }\square $$</span></p>

<p>This means that while <span class="math-container">$[\![T]\!]_\xi$</span> <em>can</em> be some complicated function, <em>if</em> <span class="math-container">$\Gamma \vdash M:T$</span> holds, then <span class="math-container">$[\![T]\!]_\xi$</span> <em>has to be a set of terms</em>.</p>

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

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

CC BY-SA 4.0
2018-11-07T14:40:56.470Z
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.
helmut
CC BY-SA 4.0
2018-11-06T21:06:44.920Z
2018-11-06T21:06:44.920Z
cody
<p>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".</p>

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

<p>My problem: For easy types (like system F types) the type interpretation <span class="math-container">$[\![T]\!]_\xi$</span> is really a set of terms, so the assertion <span class="math-container">$(\!|M|\!)_\rho \in [\![T]\!]_\xi$</span> makes sense. But for more complex types the interpretation <span class="math-container">$[\![T]\!]_\xi$</span> 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 <span class="math-container">$(\!|M|\!)_\rho \in [\![T]\!]_\xi$</span> for the more complex types <span class="math-container">$T$</span>.</p>

<p>Can anybody explain or give links to some more understandable presentations of the proof?</p>

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

<p>Edit 2: Example which does not work</p>

<p>Let's make the following valid derivation:
<span class="math-container">$$
\begin{array}{llll}
[] &amp;\vdash  &amp; *:\square &amp;\text{axiom} 
\\
[\alpha:*] &amp;\vdash&amp; \alpha:* &amp;\text{variable introduction}
\\
[\alpha:*] &amp;\vdash&amp; *:\square &amp;\text{weaken}
\\
[] &amp;\vdash &amp; (\Pi \alpha:*.*):\square   &amp;\text{product formation}
\\
[\beta:\Pi \alpha:*.*] &amp;\vdash&amp; \beta:(\Pi \alpha:*.*) &amp;\text{variable introduction}
\end{array}
$$</span></p>

<p>In the last context a valid type evaluation must satisfy <span class="math-container">$\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$</span>. For this type evaluation there is no valid term evaluation.</p>

CC BY-SA 4.0
2018-11-05T07:38:55.137Z
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?
Andrej Bauer
CC BY-SA 4.0
2018-11-05T13:47:07.017Z
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.
helmut
CC BY-SA 4.0
2018-11-05T18:14:06.763Z
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.
Andrej Bauer
CC BY-SA 4.0
2018-11-05T20:05:05.357Z
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.
helmut
CC BY-SA 4.0
2018-11-05T20:43:19.273Z
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 : * . *$.
Andrej Bauer
CC BY-SA 4.0
2018-11-06T01:33:15.347Z
I have used the weakening rule implicitly which I have now made explicit.
helmut
<lo.logic><type-theory><lambda-calculus><typed-lambda-calculus>
Understanding the Proof of Strong Normalization of the Calculus of Constructions
helmut
# Understanding the Proof of Strong Normalization of the Calculus of Constructions

(Asked by: username_0 on 2018-11-04)

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.

**Tags:** lo.logic, type-theory, lambda-calculus, typed-lambda-calculus

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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.  
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: 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 : * . *$.  
> **username_0**: I have used the weakening rule implicitly which I have now made explicit.  

---

## 1 answers

### Answer by username_2 on 2018-11-06. Score: 7 | Accepted answer

Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try [this](http://prosecco.gforge.inria.fr/personal/hritcu/temp/snforcc.pdf) 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](http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf):

$$\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).

> **Comments:**
> **username_0**: 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.  

---

