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

[Derek Dreyer]

Actually, Jonathan, I'm pretty sure this proof step is perfectly
valid, but the lemma you were assuming it depended on is too strong.
The appropriate one to use is the "head expansion" lemma:

If P[Q/x] T_2 ... T_n is SN, and Q is SN, then (\x.P) Q T_2 ... T_n is SN.

Instantiate P = xx, and Q = T_1.

Derek

On Thu, Oct 16, 2008 at 9:32 PM, Jonathan Seldin
<jonathan.seldin at uleth.ca> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>
>