Convertibility of Two Lambda Expressions Equivalent to Existence of a Common Reduct

The fact that the existence of a common reduct of two terms $e$ and $b$ implies that $e$ and $f$ are $\beta$-convertible is not a consequence of Church-Rosser theorem, but it follows immediately from the definition of $\beta$-convertibility. Church-Rosser theorem is used to prove the converse implication, that is, if two terms $e$ and $f$ are $\beta$-convertible then they have a common reduct.

To see why, it is necessary to fix some little errors or inaccuracies in the definitions given in the OP.


$\beta$-reduction: one step vs. many steps. In the $\lambda$-calculus, one-step $\beta$-reduction (denoted by $\to_\beta$) is the binary relation on the set of terms defined as follows: $e \to_\beta e'$ if $e = C\langle(\lambda x.f)d\rangle$ and $e' = C\langle f[d/x]\rangle$, for some terms $d,f$ and some context $C$ (a context $C$ is a term with exactly one occurrence of a special variable called hole, and $C\langle e \rangle$ stands for the term obtained from $C$ by replacing the hole with $e$). This is a formal definition of the intuitive idea that to perform one step of $\beta$-reduction in a term $e$, we just look for a subterm in $e$ of the form $(\lambda x.f)d$ and we replace it with $f[d/x]$ (the capture-avoiding substitution of $d$ for each free occurrence of $x$ in $f$), while the rest of the term $e$ is left unchanged. For instance,

$$x((\lambda y. \lambda z. y)(yy)(zz) ) \to_\beta x( \lambda z. yy)(zz)$$

where the context is $x(\_ (zz))$ ($\_$ is the hole), the fired $\beta$-redex is $(\lambda y.\lambda z.y)(yy)$ and $(\lambda z.y)[yy/y] = \lambda z.yy$.

Many-step $\beta$-reduction (denoted by $\twoheadrightarrow_\beta$) is the reflexive-transitive closure of one-step $\beta$-reduction, that is, $e \twoheadrightarrow_\beta e'$ if and only if there are terms $e_0, \dots, e_n $ for some $n \geq 0$ such that $e_0 = e$, $e' = e_n$ and $e_i \to_\beta e_{i+1}$ for all $0 \leq i < n$. Intuitively, $e \twoheadrightarrow_\beta e'$ means that $e$ can be transformed into $e'$ by a sequence of an arbitrary number (possibly $0$) of one-step $\beta$-reduction. For instance, $x((\lambda y. \lambda z. y)(yy)(zz) ) \twoheadrightarrow_\beta x(yy)$ because $$x((\lambda y. \lambda z. y)(yy)(zz) ) \to_\beta x( \lambda z. yy)(zz) \rightarrow_\beta x(yy)$$ by means of two one-step $\beta$-reduction, but note that $x((\lambda y. \lambda z. y)(yy)(zz) ) \not\rightarrow_\beta x(yy)$, that is, it is impossible to reduce $x((\lambda y. \lambda z. y)(yy)(zz) )$ to $x(yy)$ with just one one-step $\beta$-reduction.

Note that many-step $\beta$-reduction is reflexive, that is, $e \twoheadrightarrow_\beta e$ for every term $e$. Roughly, every term $e$ $\beta$-reduces to itself in $0$ steps! Indeed, in the definition of $e \twoheadrightarrow_\beta e'$, take $n = 0$: then, $e = e_0 = e'$ and $e_i \to_\beta e_{i+1}$ for all $0 \leq i < 0$ is vacuously true.


$\beta$-conversion. In the $\lambda$-calculus, $\beta$-conversion (denoted by $=_\beta$, also known as $\beta$-equivalence) is the reflexive-transitive and symmetric closure of one-step $\beta$-reduction, that is, $e =_\beta e'$ if and only if there are terms $e_0, \dots, e_n $ for some $n \geq 0$ such that $e_0 = e$, $e' = e_n$ and $e_i \to_\beta e_{i+1}$ or $e_i {\,}_\beta\!\!\leftarrow e_{i+1}$ for all $0 \leq i < n$. Note the subtle but crucial difference with the definition of many-step $\beta$-reduction: one-step $\beta$-reduction can go in both ways! Intuitively, $e =_\beta e'$ means that $e$ can be transformed into $e'$ by a sequence of an arbitrary number (possibly $0$) of one-step $\beta$-reduction or one-step anti-$\beta$-reduction (one-step $\beta$-reduction in the opposite way).

As in the case of many-step $\beta$-reduction, $\beta$-convertibility is reflexive, that is, $e =_\beta e$ for every term $e$. It suffices to take the case $n = 0$ in the definition.

Let us focus on the main error in the definition of $\beta$-convertibility in the OP. In that definition, anti-$\beta$-reduction is not taken into account. Said differently, in the OP's definition the sequence of terms $e_0, \dots, e_n$ can only $\beta$-reduce (with one or many steps) in the left-to right direction. Essentially, OP's definition of $\beta$-convertibility is actually the definition of many-step $\beta$-reduction. But the property cited at the beginning of the OP refers to the definition of $\beta$-convertibility I mentioned above in my answer!


The end of the story. The definitions I gave above may seem pedantic and too formal, but their advantage is to allow us to prove the desired property (the existence of a common reduct of the terms $e$ and $b$ implies that $e$ and $f$ are $\beta$-convertible) in a easy way, as a straightforward consequence of these definitions.

Let $e$ and $f$ be terms with a common reduct, that is $e \twoheadrightarrow_\beta d$ and $f \twoheadrightarrow_\beta d$ for some term $d$. It should now be clear that from $e \twoheadrightarrow_\beta d {\,}_\beta\!\!\twoheadleftarrow f$ it follows that $e =_\beta f$. But let us see it more in detail.

According to the definition of $\twoheadrightarrow_\beta$, since $e \twoheadrightarrow_\beta d$ and $f \twoheadrightarrow_\beta d$, there exist $e_0, \dots, e_n$ and $f_0, \dots, f_m$ for some $n, m \geq 0$ such that $e_0 = e$, $e_n = d$ and $e_i \to_\beta e_{i+1}$ for all $0 \leq i < n$, and $f_0 = f$, $f_m = d$ and $f_i \to_\beta f_{i+1}$ for all $0 \leq i < m$. Now, consider the sequence of terms $e_0, \dots, e_n = f_m, \dots, f_0$. We have
$$e = e_0 \to_\beta e_1 \to_\beta \dots \to_\beta e_n = d = f_m {\,}_\beta\!\!\leftarrow \cdots {\,}_\beta\!\!\leftarrow f_1 {\,}_\beta\!\!\leftarrow f_0 = f$$ which is perfectly compatible with the definition of $e =_\beta f$. Therefore, $e =_\beta f$.

As you can see, in the proof above we never used the Church-Rosser theorem, we have just applied the hypothesis ($e$ and $f$ have a common reduct) and the$-$correct$-$definition of $\beta$-convertibility.