2 added 70 characters in body edited Jul 18 '18 at 16:13 chi 13.2k2121 silver badges3333 bronze badges (This is not a proper answer, but I wanted to share some thoughts) To have a definitive answer one would need to precisely define what's allowed and what's not. I noticed this, however, which perhaps could help. The term $$M = \lambda xy. x(xy)$$ is typeable in the simply-typed lambda calculus, which is strongly normalizing. Instead, your other two examples, $$\lambda xy. (xy)x$$ and $$\lambda xy.(yx)(yx)$$ are not typeable in STLC. Perhaps exploiting this, and formalizing everything precisely, one can indeed prove that using $$M$$ "alone" does not lead to non termination. It's hard to say, since the STLC constrains the calculus significantly. To have a definitive answer one would need to precisely define what's allowed and what's not. I noticed this, however, which perhaps could help. The term $$M = \lambda xy. x(xy)$$ is typeable in the simply-typed lambda calculus, which is strongly normalizing. Instead, your other two examples, $$\lambda xy. (xy)x$$ and $$\lambda xy.(yx)(yx)$$ are not typeable in STLC. Perhaps exploiting this, and formalizing everything precisely, one can indeed prove that using $$M$$ "alone" does not lead to non termination. It's hard to say, since the STLC constrains the calculus significantly. (This is not a proper answer, but I wanted to share some thoughts) To have a definitive answer one would need to precisely define what's allowed and what's not. I noticed this, however, which perhaps could help. The term $$M = \lambda xy. x(xy)$$ is typeable in the simply-typed lambda calculus, which is strongly normalizing. Instead, your other two examples, $$\lambda xy. (xy)x$$ and $$\lambda xy.(yx)(yx)$$ are not typeable in STLC. Perhaps exploiting this, and formalizing everything precisely, one can indeed prove that using $$M$$ "alone" does not lead to non termination. It's hard to say, since the STLC constrains the calculus significantly. 1 answered Jul 18 '18 at 7:59 chi 13.2k2121 silver badges3333 bronze badges To have a definitive answer one would need to precisely define what's allowed and what's not. I noticed this, however, which perhaps could help. The term $$M = \lambda xy. x(xy)$$ is typeable in the simply-typed lambda calculus, which is strongly normalizing. Instead, your other two examples, $$\lambda xy. (xy)x$$ and $$\lambda xy.(yx)(yx)$$ are not typeable in STLC. Perhaps exploiting this, and formalizing everything precisely, one can indeed prove that using $$M$$ "alone" does not lead to non termination. It's hard to say, since the STLC constrains the calculus significantly.