21
$\begingroup$

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.

|cite|improve this question
$\endgroup$

migrated from cstheory.stackexchange.com Mar 21 '12 at 23:38

This question came from our site for theoretical computer scientists and researchers in related fields.

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

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

|cite|improve this answer
$\endgroup$
  • 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 '12 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 '12 at 19:24
  • $\begingroup$ It is, but that shouldn't be problematic. Why are you looking for such an $L$? $\endgroup$ – Dave Clarke Mar 25 '12 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 '12 at 19:33
11
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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