[TYPES] questiuon about strong normalization in untyped lambda-calculus

[Laurent Regnier]

Hello,

> The inference
> 
>> > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
>> > Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
> 
> seems to use the inference
> 
> If M reduces to N and N is SN, so is M.
> 
> This is false.

Actually this is false in general but true in the case investigated here. More
precisely Adams implicitely uses a standard result in lambda-calculus theory,
sometimes known as the strict lemma, that states that:

   If M reduces to N by a *strict* reduction (involving no K-redex) and if N is
   SN then so is M.

This is proved in a form or another by various authors (Barendregt, Danos, De
Vrijer, Tortora, ...); I have a proof of it in my 1994 TCS paper "Une
équivalence sur les lambda-termes" (the paper is in french). I can't find
another precise reference at the moment but certainly somebody on this list
may provide one.

I therefore believe Adam's argument is correct; I furthermore found it elegant
and concise, I wish I had found it myself!

Laurent Regnier
---------------
(1) Precisely the strict lemma used by Adams is that: