patternMajor
What is beta equivalence?
Viewed 0 times
betaequivalencewhat
Problem
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.
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.
Solution
$\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
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.
- If $M\to_\beta M'$ then $M\equiv_\beta M'$.
- For all terms $M$, $M\equiv_\beta M$ holds.
- If $M\equiv_\beta M'$, then $M'\equiv_\beta M$.
- If $M\equiv_\beta M'$ and $M'\equiv_\beta M''$, then $M\equiv_\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.
Context
StackExchange Computer Science Q#634, answer score: 21
Revisions (0)
No revisions yet.