# if an argument of a lambda only passes itself if it is further evaluated, is runtime always finite?

In order for a lambda expression to run forever, there must be at least one lambda in the expression in which an argument is passed to itself. For example the following runs forever.

$$(\lambda x.xx)(\lambda x.xx)$$

However, I am curious if an expression could run forever if arguments were only passed to themselves like in $\lambda x.x(xy)$ in that each time it is passed, it becomes further evaluated. I suspect that this is true (that it can be evaluated in finite time) however am unsure how to prove this formally. Informally the idea is that each recursive call is guaranteed to leave the lambda in a further reduced state since the original cannot be preserved.

So my question is:

What is a formal proof or counterexample to this claim?

A few notes:

The opposite is definitely not true, expressions of the form $\lambda xy.(xy)x$ can run forever. For example, the following runs indefinitely.

$$(\lambda xy.(xy)x)(\lambda xG.(Gx)G)(Lx.x)$$

Also, if when passed to itself both parts are passed an additional argument, such as $\lambda xy.(yx)(yx)$ it can run forever. For example

$$(\lambda xy.(yx)(yx))(\lambda x.x)(\lambda xy.(yx)(yx))$$

Additionally, I am assuming all lambdas within the expression meet the criteria, not just some subset of them. So something like the following would not be a counterexample

$$(\lambda x.x(xy))(\lambda x.xx)(\lambda x.xx)$$

Edit:

As chi pointed out below, I had not given a very good definition of the criteria for this question, so I've added one.

A lambda is reduced in X if it can be written in the following form (as <reduced-lambda>)

<id> := [[all valid variable names except X]]
<id-list> := <id> <id-list> | <epsilon>
<filler> := <epsilon> | <nonempty-filler>
<nonempty-filler> := (lambda <id> <id-list> . <nonempty-filler>) <filler> | <id> <filler> | (<nonempty-filler>) <filler>
<reduction> := (X <filler> <reduction>) | (X <nonempty-filler>)
<base-reduction> := (lambda <id> <id-list> . <filler> <base-reduction> <filler>) | (<filler> <base-reduction> <filler>) | <reduction> | X
<reduced-lambda> := (lambda <id-list> X <id-list> . <filler> <base-reduction> <filler>)


An expression E is reduced if for every lambda L in E, for every argument A in L, L is reduced in A.

And the more precise question becomes: does every reduced expression terminate?

Edit 2:

I did change the above formulation slightly, the old version is in the edit history and is incorrect (twice)

• Upvoted for the effort, even if, with high probability, I won't be able to give a real answer. – chi Jul 18 '18 at 18:34

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

• What exactly do you mean when you say I "need to precisely define what's allowed and what's not"? Would saying that at each step of solving the expression, I can apply a lambda to the argument immediately following it be sufficiently specific? – rtpax Jul 18 '18 at 13:15
• @rtpax Concretely: what is the set of lambda terms you allow, under your restriction? We need a formal, unambiguous definition. Saying "like this" and "not like this" helps intuition, but it's not enough. Related: if I start within that set and I perform a beta reduction step, can I end up outside that set? – chi Jul 18 '18 at 15:47
• I've taken your advice and edited the OP with a more precise definition, I'd appreciate it if you'd have a look at it. Thanks for the help! – rtpax Jul 18 '18 at 17:51