Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

(I have already asked this at MathOverflow, but got no answers there.)


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.

share|cite|improve this question
Crosspost from MO. – Hsien-Chih Chang 張顯之 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. – Hsien-Chih Chang 張顯之 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. – Tsuyoshi Ito 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.) – Radu GRIGore Dec 15 '10 at 1:53
up vote 13 down vote accepted

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)$.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.