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

[Tillmann Rendel]

Jonathan Seldin wrote:
> I think this proof is invalid.  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.  Consider
> 
> (\uv.u)(\x.x)((\z.zz)(\z.zz)).
> 
> This term is clearly not SN, but it reduces to (\x.x), which is SN  
> (and is, in fact, in normal form).

I don't think this is a problem here. Since T_1, T_2 ... T_n are SN, 
every reduction strategy will reduce

   (1)    (\x.xx) T_1 T_2 ... T_n

in a finite number of steps to a term of the form

   (2)    U_1 U_1 U_2 ... U_n

with T_i reduces to U_i. On the other hand, the SN term

   (3)    T_1 T_1 T_2 ... T_n

reduces to (2), so (2) must be SN. Now, if every reduction strategy 
reduces (1) to a SN term, (1) is SN itself.

   Tillmann Rendel