<p>There are several aspects to this very nice question, so I will structure this answer accordingly.
$\newcommand{\setof}[1]{\{#1\}}$
$\newcommand{\thra}{\twoheadrightarrow}$
$\newcommand{\codeof}[1]{\lceil #1 \rceil}$</p>

<p>1.
The answer to the boxed question is <strong>no</strong>.  The term $\Omega_3 = (\lambda x.xxx)(\lambda x.xxx)$ suggested by your friend is indeed a counterexample.</p>

<p>It was earlier noticed in the comments that one has counterexamples like the "ogre" $K^\infty=Y K$, until the question is restricted to terms without weak head normal form.  Such terms are known as <em>zero terms</em>.  These are terms which never reduce to a lambda, under any substitution.</p>

<p>For any fixed point combinator (fpc) $Y$, $Y I$ is a so-called <em>mute</em> (AKA "root-active") term: every reduct of it reduces further to a redex.</p>

<p>$K^\infty$ is not mute; neither is $\Omega_3$ $-$ as is manifest by inspecting its set of reducts, which is
$$\setof{\Omega_3 \underbrace{(\lambda x. xxx) \cdots (\lambda x. xxx)}_k \mid k \in \mathbb{N}}$$</p>

<p>Rather than give a precise argument why $Y I$ is mute for all fpcs $Y$ (indeed, for any looping combinator) $-$ which may be laborious yet hopefully clear enough $-$ I will treat the obvious generalization of your question, restricting to mute terms as well.</p>

<p>Mute terms are a subclass of zero terms which are a subclass of unsolvable terms.  Together these are perhaps the most popular choices for the concept of "meaningless" or "undefined" in the lambda calculus, corresponding to the trivial Berarducci, Levy-Longo, and B\"ohm trees, respectively.  The lattice of notions of meaningless terms has been analyzed in detail by Paula Severi and Fer-Jan de Vries. [1] The mute terms constitute the bottom element in this lattice, i.e., the most restrictive notion of "undefined".</p>

<p>2.
Let $M$ be a mute term, and $Y$ be a looping combinator with the property that $YI = M$.</p>

<p>First we argue that, for a fresh variable $z$, $Yz$ actually looks a lot like the $Y_M$ you described, obtained by "sprinkling $z$ around" some reduct of $M$.</p>

<p>By Church-Rosser, $YI$ and $M$ have a common reduct, $M'$.  Take a standard reduction $R : YI \thra_s M'$.  Every subterm of $M'$ corresponds to a unique subterm of $YI\equiv Yz[z:=I]$ under this reduction.  For any subterm $C[N]=M'$, $R$ factors as $YI \thra C[N_0] \thra_{wh} C[N_1] \thra_i C[N]$, where the middle leg is a weak head reduction (and final leg is internal).  $N$ is "guarded" by a $z$ iff this second leg contracts some redex $I P$, with $I$ a descendant of the substitution $[z:=I]$.</p>

<p>Obviously, $Y$ has to guard <em>some</em> subterms of $M$, for otherwise it would be mute as well.  On the other hand, it must be careful not to guard those subterms which are needed for non-termination, for otherwise it could not develop the infinite B\"ohm tree of a looping combinator.</p>

<p>It thus suffices to find a mute term in which every subterm, of every reduct, is needed for non-normalization, in the sense that putting a variable in front of that subterm yields a normalizing term.</p>

<p>Consider $\Psi = W W$, where $W = \lambda w. w I w w$.  This is like $\Omega$, but at every iteration, we check that the occurrence of $W$ in the argument position is not "blocked" by a head variable, by feeding it an identity. Putting a $z$ in front of any subterm will eventually yield a normal form of shape $zP_1\cdots P_k$, where each $P_i$ is either $I$, $W$ or a "$z$-sprinkling" of these.  So $\Psi$ is a counterexample to the generalized question.</p>

<p>THEOREM.  There is no looping combinator $Y$ such that $YI = \Psi$.</p>

<p>PROOF.  The set of all reducts of $\Psi$ is $\setof{WW,WIWW,IIIIWW,IIIWW,IIWW,IWW}$.  In order to be convertible with $\Psi$, $YI$ must reduce to one of these.  The argument is identical in all cases; for concreteness, suppose that $YI \thra IIWW$.</p>

<p>Any standard reduction $YI \thra_s IIWW$ can be factored as
\begin{align*}
YI \thra_w P N_4, P \thra_w Q N_3, Q \thra_w N_1 N_2, \text{thus }
YI \thra_w N_1 N_2 N_3 N_4\\
N_1 \thra I, N_2 \thra I,
N_3 \thra W, N_4 \thra W
\end{align*}</p>

<p>Let us refer to the reduction $YI \thra_w N_1 N_2 N_3 N_4$ as $R_0$, and the reductions starting from $N_i$ as $R_i$.</p>

<p>These reductions can be lifted over the substitution $[z:=I]$ to yield
\begin{align*}
R^z_0 : Yz \thra z^k(M_1 M_2 M_3 M_4)\\
N_i \equiv M_i[z:=I]
\end{align*}
so that $R_0$ is the composition $YI \stackrel{R^z_0[z:=I]}{\thra} I^k(N_1 \cdots N_4) \thra^k_w N_1 \cdots N_4$.</p>

<p>Similarly, we can lift each $R_i : N_i \thra N \in \setof{I,W}$ as
\begin{align*}
R^z_i : M_i \thra N^z_i\\
R_i : N_i \stackrel{R^z_i[z:=I]}{\thra} N^z_i[z:=I] \thra_I N
\end{align*}</p>

<p>The second leg of this factorization of $R_i$ consists precisely of contracting those $I$-redexes which are created by the substitution $N^z_i[z:=I]$.  (In particular, since $N$ is a normal form, so is $N^z_i$.)</p>

<p>$N^z_i$ is what we called a "$z$-sprinkling of $N$", obtained by placing any number of $z$s around any number of subterms of $N$.  Since $N \in \setof{I,W}$, the shape of $N^z_i$ will be one of</p>

<p>\begin{align*}
&amp;z^{k_1}(\lambda x. z^{k_2}(x))\\
&amp;z^{k_1}(\lambda w.
  z^{k_2}(
    z^{k_3}(
       z^{k_5}(
         z^{k_7}(w)
         z^{k_8}(\lambda x. z^{k_9}(x))
       )
       z^{k_6}(w)
    )
    z^{k_4}(w)
  ))
\end{align*}</p>

<p>So $M_1 M_2 M_3 M_4 \thra N^z_1 N^z_2 N^z_3 N^z_4$, with $N^z_i$ a $z$-sprinkling of $I$ for $i =1,2$ and of $W$ for $i=3,4$.</p>

<p>At the same time, the term $N^z_1 N^z_2 N^z_3 N^z_4$ should yet reduce to yield the infinite fpc Bohm tree $z(z(z(\cdots)))$.  So there must exist a "sprinkle" $z^{k_j}$ in one of the $N^z_i$ which comes infinitely often to the head of the term, yet does not block further reductions of it.</p>

<p>And now we are done.  By inspecting each $N^z_i$, for $i \le 4$, and each possible value of $k_j$, for $j \le 2+7\lfloor \frac{i-1}{2} \rfloor$, we find that no such sprinkling exists.</p>

<p>For example, if we modify the last $W$ in $IIWW$ as $W^z = \lambda w. z(wIww)$, then we get the normalizing reduction
$$ IIWW^z \to I W W^z \to WW^z \to W^z I W^z W^z
\to z (I I I I) W^z W^z \thra z I W^z W^z $$</p>

<p>(Notice that $\Omega$ admits such a sprinkling precisely because a certain subterm of it can be "guarded" without affecting non-normalization.  The variable comes in head position, but enough redexes remain below.)</p>

<p>3.
The "sprinkling transformation" has other uses.  For example, by placing $z$ in front of every redex in $M$, we obtain a term $N = \lambda z. M_z$ which is a normal form, yet satisfies the equation $N I = M$.  This was used by Statman in [2], for example.</p>

<p>4.
Alternatively, if you relax the requirement that $Y I = M$, you can find various (weak) fpcs $Y$ which simulate the reduction of $M$, while outputting a chain of $z$s along the way.  I am not sure this would answer your general question, but there are certainly a number of (computable) transformations $M \mapsto Y_M$ which output looping combinators for every mute $M$, in such a way that the reduction graph of $Y_M$ is structurally similar to that of $M$.  For example, one can write
$$
 Y \codeof{M} z =
\begin{cases}
z (Y \codeof{P[x:=Q]} z)
&amp;M\equiv (\lambda x.P)Q\\
Y \codeof{N} z &amp;M \text{ is not a redex and }M \to_{wh} N
\end{cases}$$</p>

<p>[1] Severi P., de Vries FJ. (2011) Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus. In: Beklemishev L.D., de Queiroz R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science, vol 6642.</p>

<p>[2] Richard Statman. There is no hyperrecurrent S,K combinator. Research
Report 91–133, Department of Mathematics, Carnegie Mellon
University, Pittsburgh, PA, 1991.</p>

CC BY-SA 3.0
2017-03-19T16:27:28.843Z
This answer is great, and I will likely accept it. However, I'm not sure what the actual theorems you are describing, other than "there is no looping combinator $Y$ such that $Y\ I=\Omega_3$". I think stating the theorems separately will make the arguments much easier to follow.
cody
CC BY-SA 3.0
2017-03-19T22:39:12.130Z
Good point.  I just updated the answer.
Andrew Polonsky
CC BY-SA 3.0
2017-03-18T20:44:48.557Z
2017-03-19T22:37:33.333Z
2017-03-19T22:37:33.333Z
Andrew Polonsky
<p>I've been thinking about these questions:</p>

<p><a href="https://cstheory.stackexchange.com/questions/31280/is-there-a-typed-lambda-calculus-which-is-consistent-and-turing-complete">Is there a typed lambda calculus which is consistent and Turing complete?</a></p>

<p><a href="https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-the-type-system-inconsistent">https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-the-type-system-inconsistent</a></p>

<p>and there are already some hard to answer related questions in the <em>untyped</em> setting! More specifically, I'm curious to know whether we can recover Turing-completeness from non-termination in the following way:</p>

<blockquote>
  <p><strong>Question:</strong> Given a (pure) $\lambda$-term $t$ with <em>no</em> weak head normal form, does there <em>always</em> exist a fixed-point combinator $Y_t$ such that
  $$ Y_t\ (\lambda x.x) = t$$</p>
</blockquote>

<p>Equalities are all taken modulo $\beta\eta$.</p>

<p>I actually suspect this version of the question to be <em>false</em>, so one can relax the question to <strong>looping combinators</strong>, where a looping combinator $Y$ is defined to be a term such that for every $f$
$$ Y\ f=f\ (Y'\ f)$$
where $Y'$ is again required to be a looping combinator. This is enough to define recursive functions as usual, of course.</p>

<p><strong>More generally, I'm interested in finding "natural" ways to go from a non-terminating $t$ to a looping combinator, even if the above equation isn't satisfied.</strong></p>

<p>I'm also interested in weaker versions of the above question, e.g. $t$ may be taken to be an application $t\equiv t_1\ t_2\ldots t_n$ with each $t_i$ in normal form (though I'm not sure that really helps).</p>

<hr>

<p>So far: the natural approach is to take $t$ and "pepper" applications of $f$ throughout, e.g.</p>

<p>$$ \Omega:=(\lambda x.x\ x)(\lambda x.x\ x)$$</p>

<p>becomes the usual</p>

<p>$$Y_\Omega:= \lambda f.(\lambda x. f\ (x\ x))\ (\lambda x.f\ (x\ x))$$</p>

<p>The idea is to reduce the head of $t$ to a lambda application $\lambda x. t'$ and replace it with $\lambda x.f\ t'$, but the next step is unclear (and I'm skeptical that this can lead to anything).</p>

<p>I'm not sure I understand enough about Böhm trees to see whether they have anything to say, but I highly doubt it, since $\Omega$'s Böhm tree is simply $\bot$, which looks nothing like the one for $Y_\Omega$: an infinite tree of abstractions.</p>

<hr>

<p><strong>Edit</strong>: A friend of mine remarked that this naive approach does not work with the term:
$$ (\lambda x.x\ x\ x)(\lambda x.x\ x\ x)$$
The naive approach would give
$$ (\lambda x.f\ (x\ x\ x))(\lambda x.f\ (x\ x\ x))$$
But this is <em>not</em> a fixed point combinator! This can be fixed by replacing the second application of $f$ by $\lambda y z.f\ y$, but then $f\mapsto \mathrm{I}$ does not give the original term. It's not clear whether this term is a counter-example to the original question though (and it certainly is not a counter example to the more general one).</p>

CC BY-SA 3.0
2017-03-15T16:25:39.637Z
I believe the requirement that t has no head normal form should be strengthened to also exclude weak head normal forms. If t is able to produce a lambda, then, since in head position you always have a fixpoint combinator (starting with f=id), the lambda should be produced by it, that is not possible.
Andrea Asperti
CC BY-SA 3.0
2017-03-15T18:14:43.587Z
@AndreaAsperti you're correct, of course. I'll amend the question.
cody
<lambda-calculus><combinatory-logic>
How can non-terminating $\lambda$-terms be turned into fixed-point combinators?
cody
# How can non-terminating $\lambda$-terms be turned into fixed-point combinators?

(Asked by: username_0 on 2016-11-02)

I've been thinking about these questions:

[Is there a typed lambda calculus which is consistent and Turing complete?](https://cstheory.stackexchange.com/questions/31280/is-there-a-typed-lambda-calculus-which-is-consistent-and-turing-complete)

<https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-the-type-system-inconsistent>

and there are already some hard to answer related questions in the *untyped* setting! More specifically, I'm curious to know whether we can recover Turing-completeness from non-termination in the following way:

> **Question:** Given a (pure) $\lambda$-term $t$ with *no* weak head normal form, does there *always* exist a fixed-point combinator $Y\_t$ such that
> $$ Y\_t\ (\lambda x.x) = t$$

Equalities are all taken modulo $\beta\eta$.

I actually suspect this version of the question to be *false*, so one can relax the question to **looping combinators**, where a looping combinator $Y$ is defined to be a term such that for every $f$
$$ Y\ f=f\ (Y'\ f)$$
where $Y'$ is again required to be a looping combinator. This is enough to define recursive functions as usual, of course.

**More generally, I'm interested in finding "natural" ways to go from a non-terminating $t$ to a looping combinator, even if the above equation isn't satisfied.**

I'm also interested in weaker versions of the above question, e.g. $t$ may be taken to be an application $t\equiv t\_1\ t\_2\ldots t\_n$ with each $t\_i$ in normal form (though I'm not sure that really helps).

---

So far: the natural approach is to take $t$ and "pepper" applications of $f$ throughout, e.g.

$$ \Omega:=(\lambda x.x\ x)(\lambda x.x\ x)$$

becomes the usual

$$Y\_\Omega:= \lambda f.(\lambda x. f\ (x\ x))\ (\lambda x.f\ (x\ x))$$

The idea is to reduce the head of $t$ to a lambda application $\lambda x. t'$ and replace it with $\lambda x.f\ t'$, but the next step is unclear (and I'm skeptical that this can lead to anything).

I'm not sure I understand enough about Böhm trees to see whether they have anything to say, but I highly doubt it, since $\Omega$'s Böhm tree is simply $\bot$, which looks nothing like the one for $Y\_\Omega$: an infinite tree of abstractions.

---

**Edit**: A friend of mine remarked that this naive approach does not work with the term:
$$ (\lambda x.x\ x\ x)(\lambda x.x\ x\ x)$$
The naive approach would give
$$ (\lambda x.f\ (x\ x\ x))(\lambda x.f\ (x\ x\ x))$$
But this is *not* a fixed point combinator! This can be fixed by replacing the second application of $f$ by $\lambda y z.f\ y$, but then $f\mapsto \mathrm{I}$ does not give the original term. It's not clear whether this term is a counter-example to the original question though (and it certainly is not a counter example to the more general one).

**Tags:** lambda-calculus, combinatory-logic

> **Comments:**
> **username_1**: I believe the requirement that t has no head normal form should be strengthened to also exclude weak head normal forms. If t is able to produce a lambda, then, since in head position you always have a fixpoint combinator (starting with f=id), the lambda should be produced by it, that is not possible.  
> **username_0**: @AndreaAsperti you're correct, of course. I'll amend the question.  

---

## 1 answers

### Answer by username_2 on 2017-03-18. Score: 9 | Accepted answer

There are several aspects to this very nice question, so I will structure this answer accordingly.
$\newcommand{\setof}[1]{\{#1\}}$
$\newcommand{\thra}{\twoheadrightarrow}$
$\newcommand{\codeof}[1]{\lceil #1 \rceil}$

1.
The answer to the boxed question is **no**. The term $\Omega\_3 = (\lambda x.xxx)(\lambda x.xxx)$ suggested by your friend is indeed a counterexample.

It was earlier noticed in the comments that one has counterexamples like the "ogre" $K^\infty=Y K$, until the question is restricted to terms without weak head normal form. Such terms are known as *zero terms*. These are terms which never reduce to a lambda, under any substitution.

For any fixed point combinator (fpc) $Y$, $Y I$ is a so-called *mute* (AKA "root-active") term: every reduct of it reduces further to a redex.

$K^\infty$ is not mute; neither is $\Omega\_3$ $-$ as is manifest by inspecting its set of reducts, which is
$$\setof{\Omega\_3 \underbrace{(\lambda x. xxx) \cdots (\lambda x. xxx)}\_k \mid k \in \mathbb{N}}$$

Rather than give a precise argument why $Y I$ is mute for all fpcs $Y$ (indeed, for any looping combinator) $-$ which may be laborious yet hopefully clear enough $-$ I will treat the obvious generalization of your question, restricting to mute terms as well.

Mute terms are a subclass of zero terms which are a subclass of unsolvable terms. Together these are perhaps the most popular choices for the concept of "meaningless" or "undefined" in the lambda calculus, corresponding to the trivial Berarducci, Levy-Longo, and B\"ohm trees, respectively. The lattice of notions of meaningless terms has been analyzed in detail by Paula Severi and Fer-Jan de Vries. [1] The mute terms constitute the bottom element in this lattice, i.e., the most restrictive notion of "undefined".

2.
Let $M$ be a mute term, and $Y$ be a looping combinator with the property that $YI = M$.

First we argue that, for a fresh variable $z$, $Yz$ actually looks a lot like the $Y\_M$ you described, obtained by "sprinkling $z$ around" some reduct of $M$.

By Church-Rosser, $YI$ and $M$ have a common reduct, $M'$. Take a standard reduction $R : YI \thra\_s M'$. Every subterm of $M'$ corresponds to a unique subterm of $YI\equiv Yz[z:=I]$ under this reduction. For any subterm $C[N]=M'$, $R$ factors as $YI \thra C[N\_0] \thra\_{wh} C[N\_1] \thra\_i C[N]$, where the middle leg is a weak head reduction (and final leg is internal). $N$ is "guarded" by a $z$ iff this second leg contracts some redex $I P$, with $I$ a descendant of the substitution $[z:=I]$.

Obviously, $Y$ has to guard *some* subterms of $M$, for otherwise it would be mute as well. On the other hand, it must be careful not to guard those subterms which are needed for non-termination, for otherwise it could not develop the infinite B\"ohm tree of a looping combinator.

It thus suffices to find a mute term in which every subterm, of every reduct, is needed for non-normalization, in the sense that putting a variable in front of that subterm yields a normalizing term.

Consider $\Psi = W W$, where $W = \lambda w. w I w w$. This is like $\Omega$, but at every iteration, we check that the occurrence of $W$ in the argument position is not "blocked" by a head variable, by feeding it an identity. Putting a $z$ in front of any subterm will eventually yield a normal form of shape $zP\_1\cdots P\_k$, where each $P\_i$ is either $I$, $W$ or a "$z$-sprinkling" of these. So $\Psi$ is a counterexample to the generalized question.

THEOREM. There is no looping combinator $Y$ such that $YI = \Psi$.

PROOF. The set of all reducts of $\Psi$ is $\setof{WW,WIWW,IIIIWW,IIIWW,IIWW,IWW}$. In order to be convertible with $\Psi$, $YI$ must reduce to one of these. The argument is identical in all cases; for concreteness, suppose that $YI \thra IIWW$.

Any standard reduction $YI \thra\_s IIWW$ can be factored as
\begin{align\*}
YI \thra\_w P N\_4, P \thra\_w Q N\_3, Q \thra\_w N\_1 N\_2, \text{thus }
YI \thra\_w N\_1 N\_2 N\_3 N\_4\\
N\_1 \thra I, N\_2 \thra I,
N\_3 \thra W, N\_4 \thra W
\end{align\*}

Let us refer to the reduction $YI \thra\_w N\_1 N\_2 N\_3 N\_4$ as $R\_0$, and the reductions starting from $N\_i$ as $R\_i$.

These reductions can be lifted over the substitution $[z:=I]$ to yield
\begin{align\*}
R^z\_0 : Yz \thra z^k(M\_1 M\_2 M\_3 M\_4)\\
N\_i \equiv M\_i[z:=I]
\end{align\*}
so that $R\_0$ is the composition $YI \stackrel{R^z\_0[z:=I]}{\thra} I^k(N\_1 \cdots N\_4) \thra^k\_w N\_1 \cdots N\_4$.

Similarly, we can lift each $R\_i : N\_i \thra N \in \setof{I,W}$ as
\begin{align\*}
R^z\_i : M\_i \thra N^z\_i\\
R\_i : N\_i \stackrel{R^z\_i[z:=I]}{\thra} N^z\_i[z:=I] \thra\_I N
\end{align\*}

The second leg of this factorization of $R\_i$ consists precisely of contracting those $I$-redexes which are created by the substitution $N^z\_i[z:=I]$. (In particular, since $N$ is a normal form, so is $N^z\_i$.)

$N^z\_i$ is what we called a "$z$-sprinkling of $N$", obtained by placing any number of $z$s around any number of subterms of $N$. Since $N \in \setof{I,W}$, the shape of $N^z\_i$ will be one of

\begin{align\*}
&z^{k\_1}(\lambda x. z^{k\_2}(x))\\
&z^{k\_1}(\lambda w.
z^{k\_2}(
z^{k\_3}(
z^{k\_5}(
z^{k\_7}(w)
z^{k\_8}(\lambda x. z^{k\_9}(x))
)
z^{k\_6}(w)
)
z^{k\_4}(w)
))
\end{align\*}

So $M\_1 M\_2 M\_3 M\_4 \thra N^z\_1 N^z\_2 N^z\_3 N^z\_4$, with $N^z\_i$ a $z$-sprinkling of $I$ for $i =1,2$ and of $W$ for $i=3,4$.

At the same time, the term $N^z\_1 N^z\_2 N^z\_3 N^z\_4$ should yet reduce to yield the infinite fpc Bohm tree $z(z(z(\cdots)))$. So there must exist a "sprinkle" $z^{k\_j}$ in one of the $N^z\_i$ which comes infinitely often to the head of the term, yet does not block further reductions of it.

And now we are done. By inspecting each $N^z\_i$, for $i \le 4$, and each possible value of $k\_j$, for $j \le 2+7\lfloor \frac{i-1}{2} \rfloor$, we find that no such sprinkling exists.

For example, if we modify the last $W$ in $IIWW$ as $W^z = \lambda w. z(wIww)$, then we get the normalizing reduction
$$ IIWW^z \to I W W^z \to WW^z \to W^z I W^z W^z
\to z (I I I I) W^z W^z \thra z I W^z W^z $$

(Notice that $\Omega$ admits such a sprinkling precisely because a certain subterm of it can be "guarded" without affecting non-normalization. The variable comes in head position, but enough redexes remain below.)

3.
The "sprinkling transformation" has other uses. For example, by placing $z$ in front of every redex in $M$, we obtain a term $N = \lambda z. M\_z$ which is a normal form, yet satisfies the equation $N I = M$. This was used by Statman in [2], for example.

4.
Alternatively, if you relax the requirement that $Y I = M$, you can find various (weak) fpcs $Y$ which simulate the reduction of $M$, while outputting a chain of $z$s along the way. I am not sure this would answer your general question, but there are certainly a number of (computable) transformations $M \mapsto Y\_M$ which output looping combinators for every mute $M$, in such a way that the reduction graph of $Y\_M$ is structurally similar to that of $M$. For example, one can write
$$
Y \codeof{M} z =
\begin{cases}
z (Y \codeof{P[x:=Q]} z)
&M\equiv (\lambda x.P)Q\\
Y \codeof{N} z &M \text{ is not a redex and }M \to\_{wh} N
\end{cases}$$

[1] Severi P., de Vries FJ. (2011) Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus. In: Beklemishev L.D., de Queiroz R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science, vol 6642.

[2] Richard Statman. There is no hyperrecurrent S,K combinator. Research
Report 91–133, Department of Mathematics, Carnegie Mellon
University, Pittsburgh, PA, 1991.

> **Comments:**
> **username_0**: This answer is great, and I will likely accept it. However, I'm not sure what the actual theorems you are describing, other than "there is no looping combinator $Y$ such that $Y\ I=\Omega_3$". I think stating the theorems separately will make the arguments much easier to follow.  
> **username_2**: Good point.  I just updated the answer.  

---

