Equivalences in Lambda Calculus

$\alpha$-equivalence

Two abstractions $M$ and $N$ are $\alpha$-equivalent, and we write $M{=}_{\alpha }N$, if they differ only in the name of their bound variables.

Formally:

$$\lambda x.M{=}_{\alpha }\lambda y.M[x:=y]$$

Identity ($\equiv$)

Two applications $M$ and $N$ are identical, and we write $M\equiv N$, if they are precisely equal, symbol for symbol.

Note that sometimes Identity and $\alpha$-equivalence are grouped together under the same $\equiv$ symbol.

---

tags: lambda-calculus