I have a question on the definition of *Saturated Sets*, as particular subset of the set of strongly normalizing terms in lambda calculus.


Here is the definition: a set $S$ of strongly normalizing $\lambda$-terms is
said *saturated* if:


1) For all $x : var$ and for all sequences $a\_{1} \dots a\_{n}$ of strongly
 normalizing terms we have $x\, a\_{1} \dots a\_{n} \in S$.


2) For all strongly normalizing term strongly normalizing $a$ we have that $c[x:=a] \, a\_{1} \dots a\_{n} \in
 S$ implies $(\lambda x . c)\, a \, a\_{1} \dots a\_{n} \in S$.


Now, I'd like to know why this definition is the way it is. I understand that
originally the definition came from Girard, in a paper on "Candidats De
Reductibilité". Can anyone give me a general insight of the reason of this particular definition?



Explanation of the definition of Saturated Sets in Lambda Calculus
Aha! I can give *some* answer to this one: saturated sets are a tool, designed specifically to allow the proof of strong normalization of [System F](http://en.wikipedia.org/wiki/System_F).


First notice that the strongly normalizing terms are a *particular instance* of saturated sets. However they are not the only one! In particular, there is another important example, the **neutral terms**, i.e. the terms that reduce to a term of the form
$$ x\ a\_1\ldots a\_n$$
Note that this set does not contain any $\lambda$-abstractions, for example.


The crucial use of this concept is the proof that every well type term in say, the STLC is normalizing: in particular, simple induction over the typing rules does *not* work, as in the application case
$$ \frac{\Gamma \vdash t: A\rightarrow B\quad \Gamma\vdash u:A}{\Gamma\vdash t\ u:B}$$
you cannot conclude that $t\ u$ is SN even though $t$ and $u$ are.


The trick is to associate to each type $A$ a set $[\![ A ]\!]\subseteq \mathrm{SN}$ of *computable terms of that type*, and show that well-typed terms of type $A$ are in fact in $[\![A]\!]$. The fundamental trick here is to define
$$ [\![A\rightarrow B]\!] = \{t\in\mathrm{SN}\mid \forall u\in[\![A]\!],\ t\ u\in[\![B]\!]\}$$
But the proof still doesn't go through! The problem is now on the $\lambda$ case!
$$ \frac{\Gamma, x:A\vdash t:B}{\Gamma\vdash\lambda x.t: A\rightarrow B} $$
the proof doesn't go through because the induction hypothesis only says $t\in[\![B]\!]$ which doesn't help much to show that $\lambda x.t\in [\![A\rightarrow B]\!]$ (which requires a quantification over *all* $u\in[\![A]\!]$).


Ugh. The solution now is to carry around a *suspended substitution*, in which you prove $t[\vec{x}:=\vec{u}]\in [\![A]\!]$ instead of just $t\in [\![A]\!]$. So what does that give us in the $\lambda$ case:



> 
> $(\lambda x.t)[\vec{x}:=\vec{u}]\in [\![A\rightarrow B]\!]$, **provided** for all $u\in [\![A]\!]$, $(\lambda x.t)[\vec{x}:=\vec{u}]\ u\in [\![B]\!]$
> 
> 
> 


Ah, but this is looking a lot like condition 2) for Saturated Sets! Very conveniently, your induction hypothesis gives
$$ t[x,\vec{x}:=u,\vec{u}]\in [\![B]\!]$$
Squinting a little (applications instead of suspended substitutions), if $[\![B]\!]$ is a saturated set the conclusion follows directly.


What about condition 1)? Well we have shown that a certain *substitution* applied to our term is SN. If we are to show that that $t$ itself is SN, it would be nice to apply the previous theorem ($t[\vec{x}:=\vec{u}]$ is SN for all computable $\vec{u}$) with the substitution $t[\vec{x}:=\vec{x}]=t$. This is exactly what condition 1) allows you to do, by showing that every variable is computable.


Alright, we see that (modulo a bit of squinting), being saturated is exactly the property required of $[\![A]\!]$ to make the proof go through. But why consider saturated sets on their own instead of just proving that each individual type $[\![A]\!]$ is saturated?


The answer there is that this *does not work* for system F. In system F the rule for universal quantification is
$$ \frac{\Gamma \vdash t:A}{\Gamma\vdash t:\forall X.A}$$
provided $X$ is free in $\Gamma$. So how do you define $[\![\forall X.A]\!]$? Girard's brilliant idea is that one may take the *intersection*
$$ \bigcap\_S [\![A]\!]\_{X:=S}$$
where $[\![X]\!]\_{X:=S}=S$. This uses an implicit quantification over *all* subset of the set of (SN) terms! But $S$ can't be any arbitrary set of terms: it has to make the proof go through! So you must restrict $S$ to being a *saturated set* of terms. This is exactly what allows the above proof to generalize to system F.




---


Now after all these explanations, it sounds a lot like the definition of saturated sets is "just because it makes the proof go through". Unfortunately, that is somewhat the case. It would be really nice to have a higher-level understanding of the reducibility proofs that *explain* why these properties and not others are what is needed in the definition of saturated sets.


One attempt to do this that I know of is Jean Gallier's *[On Girard's "Candidats de Reducibilite"](http://www.researchgate.net/publication/213877133_On_Girard%27s_Candidats_De_Reductibilite)*, which describes a variant of saturated sets using the language of sheaves! Unfortunately, I don't know of a satisfying tie-in to the main corpus of work on models of typed $\lambda$-calculi, so this work is a bit of a lone wolf, so to speak.


