[TYPES] questiuon about strong normalization in untyped lambda-calculus
Andrei Popescu
uuomul at yahoo.com
Tue Oct 14 00:24:03 EDT 2008
Apologies for asking an untyped question on a typed forum. :)
Assume (pure) untyped lambda calculus under beta reduction (and the infix notation for application associates to the left as usual).
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]
I do not even know where to start for trying to construct such a set (a greatest fixed point definition is not possible, since the property is contravariant). Or is there any obvious (or known) reason for why such
a set could not exist?
Thank you in advance for any hint on this,
Andrei Popescu
More information about the Types-list
mailing list