[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