2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ The two expression $\lambda x.x$ and $\lambda x.(\lambda x.x)$ are definitely different. $\endgroup$ – Yuval Filmus Oct 11 '18 at 17:27
  • $\begingroup$ @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... $\endgroup$ – Pinocchio Oct 11 '18 at 17:28
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Pinocchio Oct 20 '18 at 20:41
  • $\begingroup$ This is probably too much to ask but Id lve to see this through a theorem prover!!! :D $\endgroup$ – Pinocchio Oct 20 '18 at 20:45
  • $\begingroup$ Sorry, I don't really have time to formalize stuff like this. $\endgroup$ – Andrej Bauer Oct 20 '18 at 21:10
  • $\begingroup$ no need to apologize, thanks for the help Andrej! :) $\endgroup$ – Pinocchio Oct 23 '18 at 2:05
4
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Pinocchio Oct 11 '18 at 17:25
  • $\begingroup$ Perhaps somebody else would come to the rescue. $\endgroup$ – Yuval Filmus Oct 11 '18 at 17:27
  • $\begingroup$ what does "can be proved using standard equational deduction from the equational axioms above" mean?. Thanks for the help. $\endgroup$ – Pinocchio Oct 11 '18 at 17:29
  • 1
    $\begingroup$ An example of an equational axiom is $x[x\gets y]=y$. An equational deduction also allows substituting equals for equals inside an expression. $\endgroup$ – Yuval Filmus Oct 11 '18 at 17:32
  • $\begingroup$ 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? $\endgroup$ – Pinocchio Oct 11 '18 at 17:34
0
$\begingroup$

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.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.