10
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ @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. $\endgroup$ – xavierm02 Nov 5 '18 at 19:06
  • 1
    $\begingroup$ 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$? $\endgroup$ – Rodolphe Lepigre Nov 5 '18 at 19:25
  • 2
    $\begingroup$ 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. $\endgroup$ – xavierm02 Nov 5 '18 at 19:44
  • 2
    $\begingroup$ 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. $\endgroup$ – Gilles Nov 5 '18 at 20:03
  • 1
    $\begingroup$ 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. $\endgroup$ – Gilles Nov 6 '18 at 0:15
7
+150
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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!

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – xavierm02 Nov 5 '18 at 18:37
  • $\begingroup$ Damn, you're right! I'll try to think of something else later, I don't have time right now. $\endgroup$ – Rodolphe Lepigre Nov 5 '18 at 18:46

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.