<p>I believe $tt$ with $t=(\lambda x. (\lambda y.1) (x x))$ will terminate using $L$ even if it has an infinite reduction.</p>

<p>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$.</p>

<p>The first reduction step with $F_\infty$ is $F_\infty([(\lambda x.(\lambda y.1 (x x))) t]))=(\lambda y.1) (tt)$.</p>

CC BY-SA 2.5
2010-12-15T02:23:25.640Z
2010-12-15T02:23:25.640Z
Radu GRIGore
<p>(I have already asked this at MathOverflow, but got no answers there.)</p>

<h3>Background</h3>

<p>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 <em>reduction strategies</em>. A term $t$ is said to be <em>normalizing</em> if there exists a reduction strategy which brings $t$ to normal form. A term $t$ is said to be <em>strongly normalizing</em> 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.)</p>

<p>A reduction strategy is said to be <em>normalizing</em> (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.</p>

<p>At the other end of the spectrum, a reduction strategy is said to be <em>perpetual</em> (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.</p>

<p>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]]       &amp; \text{if $t$ is strongly normalizing} \\
F_{bk}(C[(\lambda x.s)t])=C[(\lambda x.s)F_{bk}(t)] &amp; \text{otherwise}
\end{array}
and
\begin{array}{ll}
F_\infty(C[(\lambda x.s)t])=C[s[t/x]] &amp; \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)] &amp; \text{otherwise}
\end{array}
(In both cases, the indicated $\beta$-redex is the <em>leftmost</em> one in the term $C[(\lambda x.s)t]$ - and on normal forms, reduction strategies are necessarily identity.) The strategy $F_\infty$ is even <em>maximal</em> - 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.)</p>

<p>Consider now the <em>leftmost-innermost</em> 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
   &amp;\text{if $t$ on normal form}\\
  L(\lambda x.s) = \lambda x. L(s)
   &amp;\text{for $s$ not on normal form}\\
  L(st) = L(s)t
   &amp;\text{for $s$ not on normal form}\\
  L(st) = s L(t)
   &amp;\text{if $s$, but not $t$ is on normal form}\\
  L((\lambda x. s)t) = s[t/x]
   &amp;\text{if $s$, $t$ both on normal form}
\end{array}</p>

<hr>

<p>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...</p>

<blockquote>
  <p>Is leftmost-innermost reduction a perpetual strategy for the untyped $\lambda$-calculus?</p>
</blockquote>

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

CC BY-SA 2.5
2010-12-14T17:38:46.760Z
[Crosspost](http://mathoverflow.net/questions/48278/are-innermost-reductions-perpetual-in-untyped-lambda-calculus) from MO.
Hsien-Chih Chang 張顯之
CC BY-SA 2.5
2010-12-14T17:53:18.300Z
... as mentioned in the very first line.
kow
CC BY-SA 2.5
2010-12-14T18:09:40.090Z
@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](http://meta.cstheory.stackexchange.com/questions/673/changing-policy-on-crossposting/675#675).
Hsien-Chih Chang 張顯之
CC BY-SA 2.5
2010-12-14T18:54:50.427Z
@kow: When you crosspost a question next time, please do not forget to add a link, preferably in both directions.
Tsuyoshi Ito
CC BY-SA 2.5
2010-12-14T19:47:35.347Z
Is there a missing $L$ in the right hand side of $L(st)=L(s)t$?
Kaveh
CC BY-SA 2.5
2010-12-15T01:53:54.810Z
@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
CC BY-SA 2.5
2010-12-15T11:57:29.393Z
@Kaveh Thanks for tagging!  @Radu Yes, exactly.  And that's exactly the kind of nice counterexample I was secretly hoping for.  Thanks!
kow
<pl.programming-languages><lambda-calculus><proof-theory><normalization>
Are innermost reductions perpetual in untyped λ-calculus?
kow
# Are innermost reductions perpetual in untyped λ-calculus?

(Asked by: username_0 on 2010-12-14)

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

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

**Tags:** pl.programming-languages, lambda-calculus, proof-theory, normalization

> **Comments:**
> **username_1**: [Crosspost](http://mathoverflow.net/questions/48278/are-innermost-reductions-perpetual-in-untyped-lambda-calculus) from MO.  
> **username_0**: ... as mentioned in the very first line.  
> **username_1**: @username_0: 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](http://meta.cstheory.stackexchange.com/questions/673/changing-policy-on-crossposting/675#675).  
> **username_2**: @username_0: When you crosspost a question next time, please do not forget to add a link, preferably in both directions.  
> **username_3**: Is there a missing $L$ in the right hand side of $L(st)=L(s)t$?  
> **username_4**: @username_3, 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.)  
> **username_0**: @username_3 Thanks for tagging!  @Radu Yes, exactly.  And that's exactly the kind of nice counterexample I was secretly hoping for.  Thanks!  

---

## 1 answers

### Answer by username_4 on 2010-12-15. Score: 14 | Accepted answer

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


---

