# Are innermost reductions perpetual in untyped λ-calculus?

### Background

In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may produce wildly different results (e.g. $(\lambda x.y)((\lambda x.xx)\lambda x.xx)$ which in one step ($\beta$-)reduces either to $y$ or to itself). Different (sequences of) choices of where to reduce are called reduction strategies. A term $t$ is said to be normalizing if there exists a reduction strategy which brings $t$ to normal form. A term $t$ is said to be strongly normalizing if every reduction strategy brings $t$ to normal form. (I'm not worried about which, but confluence guarantees there can't be more than one possibility.)

A reduction strategy is said to be normalizing (and is in some sense best possible) if whenever $t$ has a normal form, then that's where we'll end up. The leftmost-outermost strategy is normalizing.

At the other end of the spectrum, a reduction strategy is said to be perpetual (and is in some sense worst possible) if whenever there is an infinite reduction sequence from a term $t$, then the strategy finds such a sequence - in other words, we could possibly fail to normalize, then we will.

I know of the perpetual reduction strategies $F_\infty$ and $F_{bk}$ given respectively by: \begin{array}{ll} F_{bk}(C[(\lambda x.s)t])=C[s[t/x]] & \text{if $t$ is strongly normalizing} \\ F_{bk}(C[(\lambda x.s)t])=C[(\lambda x.s)F_{bk}(t)] & \text{otherwise} \end{array} and \begin{array}{ll} F_\infty(C[(\lambda x.s)t])=C[s[t/x]] & \text{if $x$ occurs in $s$, or if $t$ is on normal form} \\ F_\infty(C[(\lambda x.s)t])=C[(\lambda x.s)F_\infty(t)] & \text{otherwise} \end{array} (In both cases, the indicated $\beta$-redex is the leftmost one in the term $C[(\lambda x.s)t]$ - and on normal forms, reduction strategies are necessarily identity.) The strategy $F_\infty$ is even maximal - if it normalities a term, then it has used a longest possible reduction sequence to do so. (See e.g. 13.4 in Barendregt's book.)

Consider now the leftmost-innermost reduction strategy. Informally, it will only reduce a $\beta$-redex which contains no other redexes. More formally, it is defined by \begin{array}{ll} L(t) = t &\text{if $t$ on normal form}\\ L(\lambda x.s) = \lambda x. L(s) &\text{for $s$ not on normal form}\\ L(st) = L(s)t &\text{for $s$ not on normal form}\\ L(st) = s L(t) &\text{if $s$, but not $t$ is on normal form}\\ L((\lambda x. s)t) = s[t/x] &\text{if $s$, $t$ both on normal form} \end{array}

The natural intuition for leftmost-innermost reduction is that it will do all the work - no redex can be lost, and so it ought to be perpetual. Since the corresponding strategy is perpetual for (untyped) combinatory logic (innermost reductions are perpetual for all orthogonal TRWs), this doesn't feel like completely unfettered blue-eyed optimism...

Is leftmost-innermost reduction a perpetual strategy for the untyped $\lambda$-calculus?

If the answer turns out to be 'no', a pointer to a counterexample would be very interesting too.

• Crosspost from MO. Dec 14 '10 at 17:38
• ... as mentioned in the very first line.
– kow
Dec 14 '10 at 17:53
• @kow: Yes you are right, and there is nothing wrong with crossposting :) The link is just for the benefit to follow both the comments and answers in MO, in order to prevent double answering. See the discussion on meta. Dec 14 '10 at 18:09
• @kow: When you crosspost a question next time, please do not forget to add a link, preferably in both directions. Dec 14 '10 at 18:54
• @Kaveh, I suppose L does only one step, otherwise you have to say what's the evaluation strategy for L in $L(L(s)t)$. So L defines the sequence $s$, $L(s)$, $L(L(s))$, etc. (If I understood your question.) Dec 15 '10 at 1:53

I believe $tt$ with $t=(\lambda x. (\lambda y.1) (x x))$ will terminate using $L$ even if it has an infinite reduction.
The first reduction step is: $L(tt)=L(t)t=L(\lambda x.(\lambda y.1) (x x))t=(\lambda x.L((\lambda y.1) (x x)))t=(\lambda x.1)t$.
The first reduction step with $F_\infty$ is $F_\infty([(\lambda x.(\lambda y.1 (x x))) t]))=(\lambda y.1) (tt)$.