Haskell and Lambda-Calculus: Implementing Alpha-Congruence (Alpha-Equivalence)
haskell, lambda-calculus
Solution
You are misunderstanding: different free variables are not alpha equivalent. So `y /= x`, and `\w.wy /= \w.wx`, and `\x.xy /= \y.yx`. Similarly, `\x.yxy /= \z.wzw` because `y /= w`.
Your book says nothing about free variables being allowed to be uniformly renamed because they are not allowed to be uniformly renamed.
(Think of it this way: if I haven't yet told you the definition of `not` and `id`, would you expect `\x. not x` and `\x. id x` to be equivalent? I sure hope not!)
Problem
I am implementing an impure untyped lambda-calculus interpreter in Haskell. I'm presently stuck on implementing "alpha-congruence" (also called "alpha-equivalence" or "alpha-equality" in some textbooks). I want to be able to check whether two lambda-expressions are equal or not equal to each other. For example, if I enter the following expression into the interpreter it should yield True (`\` is used to indicate the lambda symbol): ``` >\x.x == \y.y True ``` The problem is understanding whether the following lambda-expressions are considered alpha-equivalent or not: ``` >\x.xy == \y.yx ??? >\x.yxy == \z.wzw ??? ``` In the case of `\x.xy == \y.yx` I would guess that the answer is `True`. This is because `\x.xy => \z.zy` and `\y.yx => \z.zy` and the right-hand sides of both are equal (where the symbol `=>` is used to denote alpha-reduction). In the cae of `\x.yxy == \z.wzw` I would likewise guess that the answer is `True`. This is because `\x.yxy => \a.yay` and `\z.wzw => \a.waw` which (I think) are equal. The trouble is that all of my textbooks' definitions state that only the names of the bound variables need to be changed for two lambda-expressions to be considered equal. It says nothing about the free variables in an expression needing to be renamed uniformly also. So even though `y` and `w` are both in their correct places in the lambda-expressions, how would the program "know" that the first `y` represents the first `w` and the second `y` represents the second `w`. I would need to be consistent about this in an implementation. In short, how would I go about implementing an error-free version of a function `isAlphaCongruent`? What are the exact rules that I need to follow in order for this to work? I would prefer to do this without using de Bruijn indices.