Problem Detail: 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.
Asked By : atticae
Answered By : Dave Clarke
$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
- If $Mto_beta M'$ then $Mequiv_beta M'$.
- For all terms $M$, $Mequiv_beta M$ holds.
- If $Mequiv_beta M'$, then $M'equiv_beta M$.
- If $Mequiv_beta M'$ and $M'equiv_beta M''$, then $Mequiv_beta M''$.
- $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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/634
