Relation of self-application to non termination in the untyped lambda calculus.

116 Views Asked by At

I was reading the following question: Self-application in Church's untyped lambda calculus

First, we can have terms which, if applied to themselves, still have normal form. For example, $(\lambda x . x) (\lambda x . x)$.

Similarly, $(\lambda x . x x) (\lambda x . x x)$ does not have a normal form. Assuming we are considering strong normalization, my question is:

Does the fact that a term contains self application, as a subterm, tell us anything about whether it is strongly normalizing?