What is beta equivalence?

Question

In the script I am currently reading on the lambda calculus, beta equivalence is defined as this:

The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains $\rightarrow_\beta$.

I have no idea what that means. Can someone explain it in simpler terms? Maybe with an example?

I need it for a lemma following from the Church-Russer theorem, saying

If M $\equiv_\beta$ N then there is a L with M $\twoheadrightarrow_\beta$ L and N $\twoheadrightarrow_\beta$ L.

Answer 1

$\to_\beta$ is the one-step relation between terms in the $\lambda$-calculus. This relation is neither reflexive, symmetric, or transitive. The equivalence relation $\equiv_\beta$ is the reflexive, symmetric, transitive closure of $\to_\beta$. This means

1. If $M\to_\beta M'$ then $M\equiv_\beta M'$.
2. For all terms $M$, $M\equiv_\beta M$ holds.
3. If $M\equiv_\beta M'$, then $M'\equiv_\beta M$.
4. If $M\equiv_\beta M'$ and $M'\equiv_\beta M''$, then $M\equiv_\beta M''$.
5. $\equiv_\beta$ is the smallest relation satisfying conditions 1-4.

More constructively, first apply rules 1 and 2, then repeat rules $3$ and $4$ over and over until they add no new elements to the relation.

Answer 2

It is elementary set theory really. You know what is a reflexive relation, what is a symmetric relation, and what is a transitive relation, right? An equivalence relation is one that satisfies all three of those properties.

You have probably heard of the "transitive closure" of a relation $R$? Well, it is nothing but the least transitive relation that includes $R$. That is what the term "closure" means. Similarly, you can talk about the "symmetric closure" of a relation $R$, the "reflexive closure" of a relation $R$ and the "equivalence closure" of a relation $R$ in exactly the same way.

With some thought, you can convince yourself that the transitive closure of $R$ is $R \cup R^2 \cup R^3 \cup \ldots$. The symmetric closure is $R \cup R^{-1}$. The reflexive closure is $R \cup I$ (where $I$ is the identity relation).

We use the notation $R^*$ for $I \cup R \cup R^2 \cup \ldots$. This is the reflexive transitive closure of $R$. Now notice that if $R$ is symmetric, each of the relations $I$, $R$, $R^2$, $R^3$, ... is symmetric. Hence $R^*$ will also be symmetric.

So the equivalence closure of $R$ is the transitive closure of its symmetric closure, i.e., $(R \cup R^{-1})^*$. This represents a sequence of steps, some of which are forward steps ($R$) and some backward steps ($R^{-1}$).

The relation $R$ is said to have the Church-Rosser property if the equivalence closure is the same as the composite relation $R^* (R^{-1})^*$. This represents a sequence of steps in which all the forward steps come first, followed by all backward steps. So, the Church-Rosser property says that any interleaving of forward and backward steps can be equivalently carried out by doing forward steps first and backward steps later.