2

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?

jadn
  • 459
  • 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. – jadn Jul 31 '17 at 21:06

1 Answers1

1

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 …).

k.stm
  • 18,539