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

[Jonathan Seldin]

Yes, as Tillman Rendel and a number of others have written (some to me  
alone and some to the Types list), Robin Adams proof is, in fact,  
correct.  It does not require the lemma I thought it required, but a  
weaker one that is valid.  The proof is valid, and, as somebody wrote,  
it is, indeed, very elegant.

On 16-Oct-08, at 4:01 PM, Tillmann Rendel wrote:

> 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

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