5
$\begingroup$

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 Reductibilité". Can anyone give me a general insight of the reason of this particular definition?

$\endgroup$
4
  • 1
    $\begingroup$ urbandictionary.com/define.php?term=Delucidate although there seems to be a real word in Italian... $\endgroup$ – Will Jagy May 13 '15 at 23:07
  • 1
    $\begingroup$ @WillJagy, I didn't know (I'm italian, indeed, and "delucidare" means "to elucidate"). I'll correct it now, thanks :) $\endgroup$ – meditans May 13 '15 at 23:11
  • 1
    $\begingroup$ 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. $\endgroup$ – Will Jagy May 13 '15 at 23:16
  • 1
    $\begingroup$ found it, mathoverflow.net/questions/89054/… $\endgroup$ – Will Jagy May 13 '15 at 23:19
7
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$ – meditans May 14 '15 at 0:56
  • 1
    $\begingroup$ I'll amend my answer. $\endgroup$ – cody May 14 '15 at 1:06
  • $\begingroup$ 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! $\endgroup$ – meditans May 14 '15 at 13:21

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.