6
$\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?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ urbandictionary.com/define.php?term=Delucidate although there seems to be a real word in Italian... $\endgroup$
    – Will Jagy
    Commented May 13, 2015 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
    Commented May 13, 2015 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
    Commented May 13, 2015 at 23:16
  • 1
    $\begingroup$ found it, mathoverflow.net/questions/89054/… $\endgroup$
    – Will Jagy
    Commented May 13, 2015 at 23:19

1 Answer 1

Reset to default
8
$\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.

Improve this answer
$\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
    Commented May 14, 2015 at 0:56
  • 1
    $\begingroup$ I'll amend my answer. $\endgroup$
    – cody
    Commented May 14, 2015 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
    Commented May 14, 2015 at 13:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .