2
$\begingroup$

In exercise 1.8 of the book 'Type Theory and Formal Proof: An Introduction', it is asked to show that $$(\lambda x. x\,x) y$$ is not beta convertible to $$(\lambda xy. y\,x) x\,x.$$ Using the book's notation abbreviations, this is equivalent to showing $$(\lambda x. (x\,x))\; y \neq_{\beta} (\lambda x (\lambda y. (y\;x)))\; x\;x. $$ Using the book's theorems, I proved that if they reduce to two $\beta$-normal forms that are not equal ($\alpha$-convertible) then they are not $\beta$-convertible.

However, both my calculations and checks with online tools, lead me to the first reducing to $(y\, y)$ and the second to $(x\, x)$ which are obviously equal ($alpha$-convertible).

Where is my mistake? or is there a mistake in the exercise itself?

$\endgroup$
  • $\begingroup$ A simply justification I thought of is that if $xx =_{\alpha} yy$, then also $x =_{\alpha} y$, and then, basically, all variables 'collapse' under $\alpha$-equivalence, which is probably not what one wants. $\endgroup$ – weakmoons Jul 31 '17 at 21:06
1
$\begingroup$

For the notion of $α$-conversion I know of, $α$-conversion only concerns bound variables. As $x$ and $y$ are both free in $t = (x~x)$ and $s = (y~y)$ respectively, the terms $t$ and $s$ are not $α$-convertible.

As a side note: Also, even if they were $α$-convertible, any two terms $β$-reducing to some same term might still not be $β$-convertible. For example, $(λx.x)~y$ and $(λx. y)~x$ both reduce to $y$, but neither one of them $β$-reduces to the other (as far as I can tell – it’s been a while …).

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