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

[Jonathan Seldin]

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).

On 15-Oct-08, at 9:01 AM, Robin Adams wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote:
>>
>> I would like to know if there exists a set A of strongly  
>> normalizing terms
>> such that the following holds:
>>
>> For all terms T,
>>  [T is in A]
>> iff
>>  [the term T T_1 ... T_n is strongly normalizing
>>   for all natural numbers n and terms T_1,...,T_n in A]
>
> There cannot be such a set.
>
> Proof: Suppose A satisfies the conditions above.  For any T_1, ...,  
> T_n in A,
> we have
>
> 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.
> Therefore, \x.xx is in A.
> Therefore, (\x.xx)(\x.xx) is strongly normalizing.
>
> This is a contradiction.
>
> --
> Robin Adams <robin at cs.rhul.ac.uk>
> Royal Holloway, University of London
>

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4