= Solution
Write $\to^*$ for the <reflexive closure> of the <transitive closure of a relation> $\to$, and $\leftrightarrow^*$ for its generated <equivalence relation>. The <diamond property> requires every pair $a\to b,a\to c$ to admit a one-step join $b\to d\leftarrow c$. The <Church-Rosser property> requires a possibly longer join whenever $b\leftrightarrow^*c$. Equivalently, every pair of finite reductions with the same source has a common finite reduct. Identity steps may be included in the diamond convention without affecting the counterexample below.
Let $A=(\lambda z.z)y$ and consider the <lambda term> $M=(\lambda x.xx)A$. Contracting its outer <beta-redex> gives $AA$, whereas contracting the inner <beta-redex> gives $(\lambda x.xx)y$. The only one-step reducts of $AA$ are $yA$ and $Ay$; the other branch has the sole one-step reduct $yy$. These terms are different even under <alpha equivalence>. Thus \b[one-step beta reduction has no diamond property]. Both branches do reach $yy$ by finite <beta reduction>.
For the positive result, use <parallel beta reduction> $\Rightarrow$, with rules
$$
x\Rightarrow x,\qquad \frac{P\Rightarrow P'}{\lambda x.P\Rightarrow\lambda x.P'},\qquad \frac{P\Rightarrow P'\quad Q\Rightarrow Q'}{PQ\Rightarrow P'Q'},\qquad \frac{P\Rightarrow P'\quad Q\Rightarrow Q'}{(\lambda x.P)Q\Rightarrow P'[x:=Q']}.
$$
<Structural induction>, renaming binders to avoid capture, proves the substitution lemma: $P\Rightarrow P'$ and $Q\Rightarrow Q'$ imply $P[x:=Q]\Rightarrow P'[x:=Q']$. Define the <complete development of a lambda term> by
$$
x^\bullet=x,\qquad (\lambda x.P)^\bullet=\lambda x.P^\bullet,\qquad ((\lambda x.P)Q)^\bullet=P^\bullet[x:=Q^\bullet],
$$
and $(PQ)^\bullet=P^\bullet Q^\bullet$ when the application is not initially a root <beta-redex>. Induction on a parallel derivation, using the substitution lemma in the contracting case, proves
$$
M\Rightarrow N\quad\Longrightarrow\quad N\Rightarrow M^\bullet.
$$
Consequently any two parallel reducts have the common successor $M^\bullet$. The ordinary one-step relation is included in the parallel relation, and every parallel step expands into finitely many ordinary steps; their finite closures therefore coincide. A finite grid of parallel diamonds joins any two finite parallel reductions. Finally a finite zigzag of forward and backward reductions can be joined inductively using that confluence. Hence \b[beta reduction has the Church-Rosser property], although its individual steps do not have the <diamond property>.
Back to article page
