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.

  • 1
    $\begingroup$ 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. $\endgroup$ – quicksort Dec 5 '16 at 18:10
  • 1
    $\begingroup$ 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. $\endgroup$ – Euge Dec 5 '16 at 18:28

Your Answer

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

Browse other questions tagged or ask your own question.