1
$\begingroup$

I found this $\alpha$-conversion below in a certain book:

$(\lambda x. x(\lambda z. xy)) = \alpha (\lambda z. z(\lambda x. zy))$

Well... this seems wrong to me, since $z$ is a binding variable in $(\lambda x. x(\lambda z. xy))$.

Am I just not understanding?

$\endgroup$
3
  • $\begingroup$ Three comments on proper use of this site: (1) Please use MathJax to format all mathematical expressions. I have edited your post to add proper MathJax formatting. You can press edit to see the code for how I did this. In particular, $\alpha$ and $\lambda$ are \alpha and \lambda inside dollar signs. (2) You say you saw something in a "certain book". What book? Always cite your sources! (3) No need to write "I ask for help." This is understood! $\endgroup$
    – Alex Kruckman
    Oct 1 at 19:51
  • 1
    $\begingroup$ But they changed the variable to $x$ in the second expression. You can think of this as happening over a couple steps, all $\alpha$-conversions: $$\lambda x.x(\lambda z.xy)\to \lambda x.x(\lambda u.xy)\to \lambda z.z(\lambda u.zy)\to \lambda z.z(\lambda x.zy)$$ $\endgroup$
    – spaceisdarkgreen
    Oct 1 at 20:07
  • $\begingroup$ Got it! Thank you very much! $\endgroup$
    – Paulo Argolo
    Oct 1 at 21:45

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .