# Explanation of the definition of Saturated Sets in Lambda Calculus

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?

• urbandictionary.com/define.php?term=Delucidate although there seems to be a real word in Italian... – Will Jagy May 13 '15 at 23:07
• @WillJagy, I didn't know (I'm italian, indeed, and "delucidare" means "to elucidate"). I'll correct it now, thanks :) – meditans May 13 '15 at 23:11
• My best exchange on language here was a question where I said I was expired by a previous question rather than inspired by it. A French guy asked me if i were serious and said that the analogous phrase (inspired by) in French is also used too much. – Will Jagy May 13 '15 at 23:16
• found it, mathoverflow.net/questions/89054/… – Will Jagy May 13 '15 at 23:19

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.

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", 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.

• Hi cody, this is exactly the type of answer I was looking for, thank you very much! Before I mark this as accepted, could you clarify a bit the justification for the first property? Why should I apply the substitution $t\, [\vec{x} := \vec{x}]$, in the context of this proof for STLC? – meditans May 14 '15 at 0:56
• I'll amend my answer. – cody May 14 '15 at 1:06
• Ok, I got it now, I was missing the fact that, in order to show that $\lambda x.b[\vec{x}:=\vec{g}] \in [\![\alpha \rightarrow \beta]\!]$, I had also to show that $\lambda x.b [\vec{x} := \vec{g}]$ is strongly normalizing, so it's important for a saturated set to contain all the variables in order to do the sostitution you hinted to, hence the first condition. Thank you again, wish I could upvote your answer more than once! – meditans May 14 '15 at 13:21