Prove that equality is symmetric in lambda calculus

47 Views Asked by At

I want to prove that = is symmetric in lambda calculus. ie. If $E=E'$ then $E'=E$.

From text I came across that if for instance

$$ E_1 \to_\beta E_2 \to_\beta E_3 $$

and $E \equiv E_1$ and $E' \equiv E_3$ then $E=E'$.

From this to prove that $E'=E$ so to prove that they are symmetric, I think somehow I need to show that

$$ E_3 \to E_2 \to E_1 $$

via either $\alpha$ or $\beta$ or $\eta$ conversion.

How can I prove that $E'=E$ so to prove that = is symmetric?

Thanks a bunch!

1

There are 1 best solutions below

0
On

Here's my first try at this.

If $E=E'$ then by Leibnitz's law

$$ \lambda V.E = \lambda V.E' $$

If we apply $E^*$ to both since they are the same function

$$ EE^* = E'E^* $$

and

$$ E'E^* = EE^* $$

Hence, if $E=E'$ then $E'=E$.

$\square$