# How to prove equivalence relation in this case?

I am working on $\lambda$-terms and trying to prove the $=$ is an equivalence relation on $\lambda$-terms. My problem is proving reflexive relation.

$\frac{}{\theta \vdash x = x}$

$\frac{ \theta,x \# N, y \# M \vdash M = [y := x]N } { \theta \vdash \texttt{$\lambda x.M=\lambda y.N$} }$

$\frac{\theta \vdash M_1 = M_2 \quad N_1 = N_2 } { \theta \vdash \texttt{$M_1 \, N_1=M_2 \,N_2$} }$

I put two restrictions on such $\lambda$-terms.First, bound variables are distinct. For example, there are no two terms such as $\lambda x.M$ and $\lambda x.N$. Second, multiple bindings of a variable is not allowed. For example, $\lambda x. \lambda x.M$ should be written as $\lambda y. \lambda x.M$. To sum up, every bound variable should be distinct. $[y := x]N$ means variable $x$ replaces variable $y$ in term $N$. $x \# N$ means $x$ does not occur in $N$. $\theta$ is a set of $\#$. Also, $\alpha$-equivalence is assumed for the terms. For example, $\lambda x.x = \lambda y.y$

I tried to prove that the $=$ shown in above rules is an equivalence relation on such terms.

For equivalence relation, I have to prove the following three relations.

reflexive: $\theta \vdash M=M$.

symmetric : $\theta \vdash M=N$ implies $\theta \vdash N=M$.

transitive: $\theta \vdash M=N$ and $\theta \vdash N=P$ implies $\theta \vdash M=P$.

The proof of reflexive relation is the following.

when $M$ is a variable such as $x$, then $x = x$.

when $M$ is an application such as $M_1 \,N_1$), then I have $M_1 \,N_1$ = $M_1 \,N_1$, so it is true.

when $M$ is an abstraction such as $\lambda x.M$, from $\lambda x.M = \lambda x.M$, I have $x \# M \vdash | M=[x:=x]M$, which is not true becuase $x \in M$. Also, as I said, there are no two terms such as $\lambda x.M$ and $\lambda x.M$, so I cannot show $M=M$ for an abstraction.

Since $\alpha$-equivalence is assumed for terms. I assume that $M=\lambda x.M_1 =\lambda y.M_2$. Therefore, I will have $x \# M_2, y \# M_2 \vdash M_1=[y:=x]M_2$? is this the right way to prove reflexivity?

I would appreciate your kind help.

• It seems impossible to me to prove $\lambda x.x = \lambda x.x$ with those restrictions. Can you actually prove that?
– chi
Mar 15 '17 at 12:36
• @chi I think I can't write $\lambda x.x = \lambda y.y$ because of the restriction. Any idea?
– alim
Mar 15 '17 at 13:32
• I'm quite unsure about this. It seems that reflexivity fails on $\lambda x.x$. If so, the system can not be reflexive, unless the restrictions are relaxed or the definition is adapted somehow.
– chi
Mar 15 '17 at 13:49
• @chi how about write $\lambda y.y = \lambda x.x$ since both are the same lambda term. Since $\lambda x.x$ represents a class of terms. Do you think this is possible?
– alim
Mar 15 '17 at 14:01
• Yes that should be provable, one starts from $x=x$ which is the same as $x=[y:=x]y$. Then, since $x\# y$ and $y\# x$ one can have $\lambda x.x = \lambda y.y$. If you consider $\alpha$-convertible terms as equal, then the relations above might be reflexive, after all (I'm unsure at the moment).
– chi
Mar 15 '17 at 14:33

I will only prove reflexivity $A=A$. We proceed by induction on the structure of $A$.

If $A\equiv x$, then $x=x$ follows from rule 1.

If $A\equiv \lambda x. M$, then by induction hypothesis we can assume $M=M$ is provable. Now, take any $y$ not free in $M$. We have $M \equiv [y:=x][x:=y]M$ by construction. Let $N \equiv [x:=y]M$. Rule two states

$$\dfrac{ x\# N, y\# M \vdash M=[y:=x]N }{ \vdash \lambda x.M = \lambda y.N }$$

We indeed have $x\# N$, since the $x$ variable was renamed as $y$ in $N \equiv [x:=y]N$. We also have $y\# M$ by our choice of $y$. Induction hypothesis states $M=M$, which is $M=[y:=x]N$. Hence, the conclusion of the rule holds, which is $\lambda x. M = \lambda y. [x:=y]M$. If terms are identified up-to $\alpha$, then this equality is the same as $\lambda x.M = \lambda x.M$.

If $A=MN$, the induction hypotheses and rule 3 suffice.

• I usually follow my intuition, and I am not good at presenting them. With discussing with you above and after reading your proof, I clarified some points which were not clear to me. Thank you, helped me a lot.
– alim
Mar 18 '17 at 17:29