2 added 70 characters in body
source | link

(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
source | link

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.