Why does alpha equivalence not apply to free variables?

Asked Sep 17 '23 at 19:53

Active Sep 17 '23 at 19:53

Viewed 55 times

It's mentioned in the book "Haskell programming from first principles" in the first chapter that one free variables don't have equivalence that is:

$$ \lambda x.xy \overset{\alpha-\text{eq.}}{\neq} \lambda x.xb$$

Could someone explain why this is so? What is the problem if we allow equivalence for free variables just like bound variables?

asked Sep 17 '23 at 19:53

Hmm okay but that's only an issue if you choose a specific "y" to begin with @MarianoSuárez-Álvarez – tryst with freedom Sep 18 '23 at 05:01
1

And on the contrary, not choosing “a specific $y$” is what binding the variable $y$ means. – sparusaurata Sep 18 '23 at 07:30
Ah okay, now I understood. Thank you @sparusaurata – tryst with freedom Sep 18 '23 at 07:36

0 Answers0