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).

  • $\begingroup$ 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. $\endgroup$ – Rob Arthan Apr 14 at 23:24
  • $\begingroup$ @RobArthan - Can you provide an example of a non-terminating $\lambda$-term without any kind of self-application? $\endgroup$ – Taroccoesbrocco Apr 14 at 23:47
  • $\begingroup$ 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". $\endgroup$ – Derek Elkins Apr 15 at 0:00
  • $\begingroup$ @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? $\endgroup$ – Taroccoesbrocco Apr 15 at 0:40
  • $\begingroup$ @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. $\endgroup$ – Derek Elkins Apr 15 at 1:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.