# $\lambda$-terms equal modulo $\alpha$-renaming, is this an equivalence relation?

Want to clarify few things.

It is said that two $\lambda$-terms are equal up to renaming of bound variables, such as $\lambda x.x$ equals $\lambda y.y$, so I think it is a relation actually, about how two terms are equal.

Is that (such equality up to renaming) is same as equivalence relation?

To show a relation is an equivalence relation on a set, have to prove it is reflexive, symmetric, or transitive. I know, but have not done any practice on it.

Let's say, I want to prove following

1. $\frac{}{x = x}$ \two variables
2. $\frac{ t_1 = t_3 \,\,\, t_2=t_4 } {t_1 \, t_2 \, = \,t_3 \, t_4}$ \applications
3. $\frac{ t_2=[y / x]t_2 }{\lambda x.t_1 \, = \, \lambda y.t_2}$ \abstractions

where $[y / x]t_2$ replace $x$ by $y$ in $t_2$ and $y$ is not occur in $t_2$.

I think above 3 rules are true.

How can I show proof of they holds? does that proof related to the proof of $\alpha$-equivalence is an equivalence relation on $\lambda$-terms?

I am bit fonfused, it would be great if anyone help me clear things for me.

• It certainly is an equivalence relation: terms that are equal up to an alpha conversion are colloquially referred as "equal". Let S be a set and let r be a subset of S x S. How do you prove that r is an equivalence relation? It seems you already understand that. Now, let S be "the set of lambda terms" and let r(x, y) be "there exists an alpha conversion that turns x into y", and prove each property individually. – quicksort Dec 5 '16 at 18:10
• You don't need to prove those rules. Those rules are the definition of $\alpha$-equality (you can write $=_{\alpha}$ instead of $=$). To prove it is an equivalence relation you have to prove reflexivity, symmetry, and transitivity, as you already stated. – Euge Dec 5 '16 at 18:28