# Are innermost reductions perpetual in untyped $\lambda$-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 normalising if there exists a reduction strategy which brings $t$ to normal form. A term $t$ is said to be strongly normalising 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 normalising (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 normalising.

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 normalise, 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 normalising}\\\\ 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 normalises 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.

-
It seems like you'll probably get a better answer to this on the theoretical CS stackexchange. Here's a link: cstheory.stackexchange.com –  Harry Gindi Dec 4 '10 at 17:39
@Harry, I doubt that; this isn't a complexity theory question. –  Adam Dec 4 '10 at 22:14
@Harry, trying there is my backup plan (I'll hold off for a few more days). –  kow Dec 6 '10 at 12:17
@Adam: $\lambda$-calculus is a part of theoretical computer science too. There are questions in this topic that have been answered. –  Hsien-Chih Chang 張顯之 Dec 14 '10 at 17:54
@Hsien-Chih Chang, I agree with you, but the vast majority of people who claim to be "computer science theorists" do not. –  Adam Dec 20 '10 at 10:36

Let $t$ be the term $t=(\lambda x. (\lambda y.z) (x x))$. Then the term $tt$ normalises under $L$ (in fact, $L(tt) = (\lambda x.z)t$), but it is clearly not strongly normalising, since $F_\infty(tt) = (\lambda y.z)(tt)$.