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.

Improve this question
$\endgroup$
8
  • 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$ Commented Nov 5, 2018 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$ Commented Nov 5, 2018 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$ Commented Nov 5, 2018 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$ Commented Nov 5, 2018 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$ Commented Nov 6, 2018 at 0:15

2 Answers 2

Reset to default
8
+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.

Improve this answer
$\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!

Improve this answer
$\endgroup$
2
  • 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$ Commented Nov 5, 2018 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$ Commented Nov 5, 2018 at 18:46

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.