14
$\begingroup$

I've been thinking about these questions:

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrea Asperti Mar 15 '17 at 16:25
  • $\begingroup$ @AndreaAsperti you're correct, of course. I'll amend the question. $\endgroup$ – cody Mar 15 '17 at 18:14
7
+200
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – cody Mar 19 '17 at 16:27
  • $\begingroup$ Good point. I just updated the answer. $\endgroup$ – Andrew Polonsky Mar 19 '17 at 22:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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