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

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?

Short answer: Self-application might jeopardize termination, but not necessarily. Indeed, avoiding any kind of self-application is a sufficient but not necessary condition for termination.

Long answer (updated after Rob Arthan's and Derek Elkins' remarks): There exist terminating terms that contain self-application: for instance (as you said), $$(\lambda x. x) \lambda x.x$$ which reduces to to the normal term $$\lambda x. x$$. So, self-application is not a sufficient condition for non-termination.

Anyway, we can say, roughly speaking, that some kind of self-application is a necessary condition for non-termination. Indeed, simply typed $$\lambda$$-calculus is a restriction to the untyped $$\lambda$$-calculus where, in particular, (roughly) any kind self-application is forbidden, and all terms in the simply typed $$\lambda$$-calculus are strongly normalizing.

Unfortunately, it is not possible (or at least, I am not able) to give a precise definition of the kind of self application that yields non-terminating terms, because the issue is quite technical and not trivial and, as far as I know, in the literature there is no clear result about that. Anyway, it is possible to see what happens in the simply typed $$\lambda$$-calculus.

Terms of the simply typed $$\lambda$$-calculus are the "typable" ones i.e. the ones that can be derived in a type system that forbids self-application. According to this type system, a term $$tu$$ is typable if and only if $$t$$ is typable with a type of the form $$A \to B$$, and $$u$$ is typable with a type of the form $$A$$. The type system is conceived so that no term $$s$$ can be typed by both $$A \to B$$ and $$A$$, thus the term $$ss$$ is not typable. In this way, self-application is forbidden in the simply typed $$\lambda$$-calculus: this is the key-property that allows us to prove that all terms in the simply typed $$\lambda$$-calculus are strongly normalizing.

But the expressive power of the simply typed $$\lambda$$-calculus is quite limited. For instance the harmless term $$(\lambda x.x) \lambda x .x$$ is not typable in such a system. More importantly, self-application is crucial to define recursion and fixpoint combinators, which are required to represent many important computable functions. So, a question naturally arises:

Is it possible to define laxer type systems that allows some harmless (with respect to termination) forms of self-applications?

Yes! Take for instance the system of intersection types, which characterizes all and only the terminating terms. For instance, the self-applying term $$(\lambda x.x)\lambda x.x$$ is typable with intersection types, but the non-terminating $$(\lambda x. xx) \lambda x.xx$$ is not. Roughly, intersection types allows us to discriminate harmless and harmful forms of self-application. For more details about intersection types, I suggest the reading of this paper (or at least its first part).

• Your claim that self-application is necessary for non-termination sounds wrong to me. What do you (and the OP) mean by self-application? There are $\lambda$-terms that have no subterms of the form $t\,t$ but that have no normal form. – Rob Arthan Apr 14 at 23:24
• @RobArthan - Can you provide an example of a non-terminating $\lambda$-term without any kind of self-application? – Taroccoesbrocco Apr 14 at 23:47
• Presumably you can get situations where you have $FG$ and $GF$ rather than direct self-applications like $FF$ and presumably variants where you represent mutual recursion with tupling. The "self-application" may not be direct (or at least isn't obviously required to be direct) hence Rob Arthan asking about what is meant by "self-application". – Derek Elkins Apr 15 at 0:00
• @DerekElkins - I'm not sure I understand what you mean. To me, a term contains self-application if it is $\beta$-equivalent to a term containing a subterm of the form $tt$ for some term $t$. Do you have any example of a non-terminating term that does not contain any self-application? – Taroccoesbrocco Apr 15 at 0:40
• @Taroccoesbrocco I'm not saying you're wrong (though, I think you are but in a way that could be fixed). I'm saying you've not demonstrated that "containing a subterm of the form $tt$" is necessary. You've merely asserted it without reference. (The Wikipedia article does not say this. At best, it shows a possible definition of the fixed point operator that does utilize self-application.) This is also the most substantial part of the OP's question. The OP had already demonstrated that you can have normalizing terms that contain self-application. – Derek Elkins Apr 15 at 1:18