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.

  • $\begingroup$ Sorry if the language is not perfect, I translated the quotes from german. $\endgroup$
    – magnattic
    Mar 21, 2012 at 18:43

2 Answers 2


$\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.

  • 1
    $\begingroup$ Ok thanks, I think I get it then. My first assumption was that $M \equiv_\beta N$ means that M can somehow be reduced to N, but that does not necessarily have to hold because they are obviously also equivalent if they can be reduced to the same term. Because of your point 3 this can be constructed then, I guess. Thanks, that helped a lot. $\endgroup$
    – magnattic
    Mar 22, 2012 at 9:18
  • $\begingroup$ Isnt the relation infinitly large? Am I not always able to find a Term L for an Term M so that $L \rightarrow_\beta M$? $\endgroup$
    – magnattic
    Mar 25, 2012 at 19:24
  • $\begingroup$ It is, but that shouldn't be problematic. Why are you looking for such an $L$? $\endgroup$ Mar 25, 2012 at 19:29
  • $\begingroup$ I dont know. I was just arguing with my partner if it always would be infinitly large. Thanks for explaining. :) $\endgroup$
    – magnattic
    Mar 25, 2012 at 19:33

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.

  • 2
    $\begingroup$ If you added one final sentence to relate to the question this would be a good answer. $\endgroup$
    – Raphael
    Mar 22, 2012 at 6:50
  • $\begingroup$ It's all so elementary that one comes to the end and wonders "where's the answer, actually?" $\endgroup$ Apr 1, 2016 at 6:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.