# How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following:

$$\lambda x. x \equiv_{\alpha} \lambda y . y$$

formally. They define a an $$\alpha$$-conversion on page 15 as follows:

$$\lambda x . E = \lambda z.(E[x \leftarrow z])$$

however, I wasn't sure how to formally show the statement I am trying to show. Essentially I guess I don't know how to formally show in a proof that two distinct objects actually belong to this same equivalence class. The intuition and idea is clear, but how do I know if I've shown the statement?

In fact if someone can show me how to do the more complicated one too that would be really helpful too:

$$\lambda x.x (\lambda y . y) \equiv_{\alpha} \lambda y . y (\lambda x. x)$$

how do I know if I've shown what is being asked?

Actually I think page 16 is the one thats confusing me most:

Using the equation above, one has now the possibility to prove $$\lambda$$-expressions "equivalent". To capture this provability relation formally, we let $$E \equiv_{\alpha} E^\prime$$ denote the fact that the equation $$E = E^\prime$$ can proved using standard equational deduction form the equational axioms above (($$\alpha$$) plus those for substitution).

Exercise 3 Prove the following equivalences of $$\lambda$$-expressions:

• $$\lambda x.x \equiv_{\alpha} \lambda y.y$$,
• $$\lambda x.x (\lambda y.y) \equiv_{\alpha} \lambda y.y (\lambda x.x)$$,
• $$\lambda x.x(\lambda y.y) \equiv_\alpha \lambda y.y(\lambda y.y)$$.

what does:

can be proved using standard equational deduction from the equational axioms above

mean?

Since there is already an answer that is not helping (because I don't understand the notation) I will add what I thought was the answer but I'm not sure:

I would have guessed that:

$$\lambda x. x \equiv_{\alpha} \lambda y . y$$

if and only if there is a variable such that if we plug it into the lambda functions evaluates to the same function with the same variables. i.e.

$$\lambda x. x \equiv_{\alpha} \lambda y . y \iff \exists z \in Var : \lambda x . x = \lambda z. ( (\lambda y . y)[y \leftarrow z] )$$

if we set $$z = x$$ we get:

$$\lambda z. ( (\lambda y . y)[y \leftarrow z] )$$ $$\lambda x. ( (\lambda y . y)[y \leftarrow x] )$$ $$\lambda x. (\lambda x .x )$$

which I assume the last line is the same as $$\lambda x .x$$ but I am not sure. If that were true then I'd show I can transform $$\lambda y . y$$ to $$\lambda x . x$$ which is what I assume the equivalence class should look like. Where did I go wrong?

• The two expression $\lambda x.x$ and $\lambda x.(\lambda x.x)$ are definitely different. – Yuval Filmus Oct 11 '18 at 17:27
• @YuvalFilmus what I would have assumed the right proof should look like is, ok I have one function and I can transform it to the other one by calling x = y, oh ok, look the functions now look exactly the same, so they must be in the same equivalence class. Thats what a correct proof I thought would look like... – Pinocchio Oct 11 '18 at 17:28

By definition of substitution we have $$x [x \leftarrow z] = z$$ therefore $$\lambda z . x [x \leftarrow z] = \lambda z . z \tag{1}$$ because $$\lambda$$-abstraction is a congruence (it preserves equality). By the definition of $$\alpha$$-equality we have $$\lambda x . x = \lambda z . x [x \leftarrow z] \tag{2}.$$ By transitivity of equality we get from (1) and (2) that $$\lambda x . x = \lambda z . z$$ If you require more details than this, you should use a computer proof assistant to check the details.

• I think what I found confusing is the fact the definition of equivalence I would have used is, if there exists a variable substitution such that the lambda functions are syntactically equal, then they are equal. Instead they imposed the axiom $\lambda x . E = \lambda z. E[x\leftarrow z]$ as an axiom which seemed less natural to me. – Pinocchio Oct 20 '18 at 20:41
• This is probably too much to ask but Id lve to see this through a theorem prover!!! :D – Pinocchio Oct 20 '18 at 20:45
• Sorry, I don't really have time to formalize stuff like this. – Andrej Bauer Oct 20 '18 at 21:10
• no need to apologize, thanks for the help Andrej! :) – Pinocchio Oct 23 '18 at 2:05

To be at least semi-formal, we can exploit these facts:

1. $$\lambda x.M \equiv_\alpha \lambda y.(M[x \leftarrow y])$$ when $$y$$ is a variable not occurring free in $$M$$
2. The relation $$\equiv_\alpha$$ is an equivalence relation. In particular, it is transitive, so we can perform the renaming of point 1. as many times as we want
3. The relation $$\equiv_\alpha$$ is also a congruence, which means that "we can perform renaming in subterms as well". More formally, when $$A \equiv_\alpha B$$ then we have $$M[x\leftarrow A] \equiv_\alpha M[x\leftarrow B]$$ -- i.e., we can replace any occurrence of $$A$$ in a larger term with $$B$$, and the result will be $$\alpha$$ congruent.

So, for the exercises:

• $$\lambda x.x$$ by point 1 can be rewritten as $$\lambda y.(x[x\leftarrow y])$$ which by definition of substitution is $$\lambda y.y$$
• $$\lambda x.x(\lambda y.y)$$ by point 1 can be rewritten renaming $$x$$ into $$y$$. We can do this since $$y$$ is not free in $$x(\lambda y.y)$$. So, we get $$\lambda y.y(\lambda y.y)$$. Then we can apply the symmetric result we have proven before, i.e. $$\lambda y.y \equiv_\alpha \lambda x.x$$, and get (by congruence, point 3) the wanted $$\lambda y.y(\lambda x.x)$$. Since we performed two renamings, we implicitly relied on transitivity (point 2).

Finally, the sentence

can be proved using standard equational deduction from the equational axioms above

simply means: this can be proved by replacing some subterms with equivalent terms, possibly many times.

"Equational reasoning/deduction" refers to the process of substituting in a larger formula some subformula with an equivalent one, as if the two formulas could be assumed to be "equal", in some sense. This approach applies whenever we are working with a congruence relation.

The operation $$[x \gets z]$$ is defined inductively on the structure of the expression it is applied to. In particular, one of the rules is $$x[x \gets z] = z$$. This immediately implies $$\lambda x.x \equiv_\alpha \lambda y.x[x\gets y] = \lambda y.y$$.

• I know your trying to help but this isn't helping. I wrote what I think a correct proof should look like. Can you take a look at that? – Pinocchio Oct 11 '18 at 17:25
• Perhaps somebody else would come to the rescue. – Yuval Filmus Oct 11 '18 at 17:27
• what does "can be proved using standard equational deduction from the equational axioms above" mean?. Thanks for the help. – Pinocchio Oct 11 '18 at 17:29
• An example of an equational axiom is $x[x\gets y]=y$. An equational deduction also allows substituting equals for equals inside an expression. – Yuval Filmus Oct 11 '18 at 17:32
• it seems that in your answer you said "This immediately implies " which makes me feel that you skipped the step I was looking to see to understand what proof means in this system. Do you mind making it explicit? – Pinocchio Oct 11 '18 at 17:34

My confusion was that the definition is not that there exists a variable name such that the two functions are equal (which I believe is a better definition, probably equivalent to the one provided). Instead they impose the following equational axiom:

$$\lambda x.E = \lambda z.(E[x \leftarrow z])$$

So we have:

$$\lambda x.x = \lambda y.(E[x \rightarrow y])$$

by equational axiom. Then:

$$\lambda y.x[x \rightarrow y] = \lambda y.y$$

by realizing that $$E = x$$ and that substitution of $$x$$ for $$y$$ results in $$y$$ i.e.

$$E[x \rightarrow y] = x[x \rightarrow y] = y$$

which results in:

$$\lambda x.x = \lambda y.(E[x \rightarrow y]) = \lambda y.x[x \rightarrow y] = \lambda y.y$$

all in one line.