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

[Robin Adams]

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