patternMinor
Confluence of beta expansion
Viewed 0 times
betaexpansionconfluence
Problem
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
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
Solution
Two counterexamples are:
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.
- $(\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.
Context
StackExchange Computer Science Q#99492, answer score: 8
Revisions (0)
No revisions yet.