# Confluence of beta expansion

Let $$\to_\beta$$ be $$\beta$$-reduction in the $$\lambda$$-calculus. Define $$\beta$$-expansion $$\leftarrow_\beta$$ by $$t'\leftarrow_\beta t \iff t\to_\beta t'$$.

Is $$\leftarrow_\beta$$ confluent? In other words, do we have that for any $$l,d,r$$, if $$l \to_\beta^* d\leftarrow_\beta^* r$$, then there exists $$u$$ such that $$l\leftarrow_\beta^* u \to_\beta^* r$$?

Keywords: Upward confluence, upside down CR property

I started by looking at the weaker property: local confluence (i.e. if $$l \to_\beta d\leftarrow_\beta r$$, then $$l\leftarrow_\beta^* u \to_\beta^* r$$). Even if this were true, it would not imply confluence since $$\beta$$-expansion is non-terminating, but I thought that it would help me understand the obstacles.

(Top) In the case where both reductions are at top-level, the hypothesis becomes $$(\lambda x_1.b_1)a_1\rightarrow b_1[a_1/x_1]=b_2[a_2/x_2]\leftarrow (\lambda x_2.b_2)a_2$$. Up to $$\alpha$$-renaming, we can assume that $$x_1\not =x_2$$, and that neither $$x_1$$ nor $$x_2$$ is free in those terms.

(Throw) If $$x_1$$ is not free in $$b_1$$, we have $$b_1=b_2[a_2/x_2]$$ and therefore have $$(\lambda x_1.b_1)a_1=(\lambda x_1.b_2[a_2/x_2])a_1\leftarrow(\lambda x_1.(\lambda x_2.b_2)a_2)a_1\rightarrow (\lambda x_2.b_2)a_2$$.

A naive proof by induction (on $$b_1$$ and $$b_2$$) for the case (Top) would be as follows:

• If $$b_1$$ is a variable $$y_1$$,

• If $$y_1=x_1$$, the hypothesis becomes $$(\lambda x_1.x_1)a_1\rightarrow a_1=b_2[a_2/x_2]\leftarrow (\lambda x_2.b_2)a_2$$, and we indeed have $$(\lambda x_1.x_1)a_1=(\lambda x_1.x_1)(b_2[a_2/x_2])\leftarrow (\lambda x_1.x_1)((\lambda x_2.b_2)a_2)\rightarrow (\lambda x_2.b_2)a_2$$.

• If $$y_1\not=x_1$$, then we can simply use (Throw).

• The same proofs apply is $$b_2$$ is a variable.

• For $$b_1=\lambda y.c_1$$ and $$b_2=\lambda y.c_2$$, the hypothesis becomes $$(\lambda x_1.\lambda y. c_1)a_1\rightarrow \lambda y.c_1[a_1/x_1]=\lambda y.c_2[a_2/x_2]\leftarrow (\lambda x_2.\lambda y.c_2)a_2$$ and the induction hypothesis gives $$d$$ such that $$(\lambda x_1.c_1)a_1\leftarrow d\rightarrow (\lambda x_2.c_2)a_2$$ which implies that $$\lambda y.(\lambda x_1.c_1)a_1\leftarrow \lambda y.d\rightarrow \lambda y.(\lambda x_2.c_2)a_2$$. Unfortunately, we do not have $$\lambda y.(\lambda x_2.c_2)a_2\rightarrow (\lambda x_2.\lambda y.c_2)a_2$$. (This makes me think of $$\sigma$$-reduction.)

• A similar problem arises for applications: the $$\lambda$$s are not where they should be.

• @chi Unless I'm mistaken, $(\lambda b.yb)y\leftarrow(\lambda a. (\lambda b. a b)y)y\rightarrow (\lambda a. a y)y$ works. – xavierm02 Nov 5 '18 at 19:06
• I somewhat agree with @chi that it seems confluent after you think about it and see a couple of counter-examples. But actually, what about $(\lambda x.x\;x\;y)\;y \to y\;y\;y \leftarrow (\lambda x.y\;x\;x)\;y$? – Rodolphe Lepigre Nov 5 '18 at 19:25
• Although it'd be convenient for me if it were true, I'm a little more pessimistic. A colleague of mine made the following remark which makes it seem unlikely: it'd imply that any two arbitrary programs that compute the same (church) integer can be combined. – xavierm02 Nov 5 '18 at 19:44
• The answer is no. Exercise 3.5.11 in Barendregt gives a counter-example attributed to Plotkin, but without a reference: $(\lambda x. b x (b c)) c$ and $(\lambda x. x x) (b c)$. I'm going to look for a proof. – Gilles 'SO- stop being evil' Nov 5 '18 at 20:03
• I've posted the counterexample as an answer, with what I thought would be a proof, but there's a step I can't figure out. If someone can figure it out, please post an answer and I'll delete mine. – Gilles 'SO- stop being evil' Nov 6 '18 at 0:15

Two counterexamples are:

• $$(\lambda x. b x (b c)) c$$ and $$(\lambda x. x x) (b c)$$ (Plotkin).
• $$(\lambda x. a (b x)) (c d)$$ and $$a ((\lambda y. b (c y)) d)$$ (Van Oostrom).

The counterexample detailed below is given in The Lambda Calculus: Its Syntax and Semantics by H.P. Barenredgt, revised edition (1984), exercise 3.5.11 (vii). It is attributed to Plotkin (no precise reference). I give an incomplete proof which is adapted from a proof by Vincent van Oostrom of a different counterexample, in Take Five: an Easy Expansion Exercise (1996) [PDF].

The basis of the proof is the standardization theorem, which allows us to consider only beta expansions of a certain form. Intuitively speaking, a standard reduction is a reduction that makes all of its contractions from left to right. More precisely, a reduction is non-standard iff there is a step $$M_i$$ whose redex is a residual of a redex to the left of the redex of a previous step $$M_j$$; “left” and “right” for a redex are defined by the position of the $$\lambda$$ that is eliminated when the redex is contracted. The standardization theorem states that there if $$M \rightarrow_\beta^* N$$ then there is a standard reduction from $$M$$ to $$N$$.

Let $$L = (\lambda x. b x (b c)) c$$ and $$R = (\lambda x. x x) (b c)$$. Both terms beta-reduce to $$b c (b c)$$ in one step.

Suppose that there is a common ancestor $$A$$ such that $$L \leftarrow_\beta^* A \rightarrow_\beta^* R$$. Thanks to the standardization theorem, we can assume that both reductions are standard. Without loss of generality, suppose that $$A$$ is the first step where these reductions differ. Of these two reductions, let $$\sigma$$ be the one where the redex of the first step is to the left of the other, and write $$A = C_1[(\lambda z. M) N]$$ where $$C_1$$ is the context of this contraction and $$(\lambda z. M) N$$ is the redex. Let $$\tau$$ be the other reduction.

Since $$\tau$$ is standard and its first step is to the right of the hole in $$C_1$$, it cannot contract at $$C_1$$ nor to the left of it. Therefore the final term of $$\tau$$ is of the form $$C_2[(\lambda z. M') N']$$ where the parts of $$C_1$$ and $$C_2$$ to the left of their holes are identical, $$M \rightarrow_\beta^* M'$$ and $$N \rightarrow_\beta^* N'$$. Since $$\sigma$$ starts by reducing at $$C_1$$ and never reduces further left, its final term must be of the form $$C_3[S]$$ where the part of $$C_3$$ to the left of its hole is identical to the left part of $$C_1$$ and $$C_2$$, and $$M[z \leftarrow N] \rightarrow_\beta^* S$$.

Observe that each of $$L$$ and $$R$$ contains a single lambda which is to the left of the application operator at the top level. Since $$\tau$$ preserves the lambda of $$\lambda z. M$$, this lambda is the one in whichever of $$L$$ or $$R$$ is the final term of $$\tau$$, and in that term the argument of the application is obtained by reducing $$N$$. The redex is at the toplevel, meaning that $$C_1 = C_2 = C_3 = []$$.

• If $$\tau$$ ends in $$R$$, then $$M \rightarrow_\beta^* z z$$, $$N \rightarrow_\beta^* b c$$ and $$M[z \leftarrow N] \rightarrow_\beta^* (\lambda x. b x (b c)) c$$. If $$N$$ has a descendant in $$L$$ then this descendant must also reduce to $$b c$$ which is the normal form of $$N$$. In particular, no descendant of $$N$$ can be a lambda, so $$\sigma$$ cannot contract a subterm of the form $$\check{N} P$$ where $$\check{N}$$ is a descendant of $$N$$. Since the only subterm of $$L$$ that reduces to $$b c$$ is $$b c$$, the sole possible descendant of $$N$$ in $$L$$ is the sole occurrence of $$b c$$ itself.

• If $$\tau$$ ends in $$L$$, then $$M \rightarrow_\beta^* b z (b c)$$, $$N \rightarrow_\beta^* c$$, and $$M[z \leftarrow N] \rightarrow_\beta^* (\lambda x. x x) (b c)$$. If $$N$$ has a descendant in $$R$$ then this descendant must also reduce to $$c$$ by confluence.

At this point, the conclusion should follow easily according to van Oostrom, but I'm missing something: I don't see how tracing the descendants of $$N$$ gives any information about $$M$$. Apologies for the incomplete post, I'll think about it overnight.

Note that $$\beta$$-reduction can make any term disappear. Assuming that variable $$x$$ does not appear free in a term $$v$$, you have $$(\lambda x.v)\;t_1 \to_\beta v$$ and $$(\lambda x.v)\;t_2 \to_\beta v$$ for any terms $$t_1$$ and $$t_2$$. As a consequence, the fact that reverse $$\beta$$-reduction is confluent is somewhat equivalent to: for all terms $$t_1$$ and $$t_2$$, there is a term $$u$$ such that $$u \to_\beta^\ast t_1$$ and $$u \to_\beta^\ast t_2$$. This seems very false to me!

• Unless I'm mistaken, $(\lambda x .v) t_1\leftarrow (\lambda x .(\lambda x .v) t_1)t_2\rightarrow (\lambda x .v) t_2$ works for those two terms. – xavierm02 Nov 5 '18 at 18:37
• Damn, you're right! I'll try to think of something else later, I don't have time right now. – Rodolphe Lepigre Nov 5 '18 at 18:46