7
$\begingroup$

I am interested in the alpha equivalence relation in languages with variable bindings, such as:

t := x:y    'x belong to y'
  | bot     'False'
  | t -> t  'implication'
  | Ax.t    'forall x, t'

Or the pure lambda calculus:

t := x       'variable'
  | (t t)    'application '
  | Lx.t     'abstraction: \x -> t'

I am looking for an algorithm allowing me to determine whether two terms of the language are alpha-equivalent or not. Any published reference is very welcome too. I am assuming a data representation of the terms as a standard recursive type, for example in Haskell:

newtype Var = Var Int 
data Term = Belong Var Var
          | Bot
          | Imply Term Term
          | Forall Var Term 
$\endgroup$
9
$\begingroup$

There are several ways to do what you want. One of them is to use a different syntax representation under which $\alpha$-equivalent terms are actually equal. Such representations go under the name nameless or locally nameless syntax. A popular one uses de Bruijn indices. See my blog posts How to implement dependent type theory I, II and III for a blitz introduction to implementing this sort of thing (part III has de Bruijn indices explained).

If you insist on your representation, then we may still secretly use de Bruijn indices, as follows. As we descend inside a subterm during comparison, we keep a list of pairs of bound variables so far encountered. For example, when comparing Forall x1 e1 and Forall x2 e2, we add the pair (x1, x2) to the list and recursively compare e1 and e2. When asked to compare variables x and y, we search down the list: either they must both appear in the same spot (they were bound by the same quantifier) or neither appears and they are equal (they are both free and they are equal).

I am not well-versed with Haskell, but you'd get something like this:

newtype Var = Var Int deriving Eq

data Term = Belong Var Var
          | Bot
          | Imply Term Term
          | Forall Var Term

equalVar :: [(Var,Var)] -> Var -> Var -> Bool
equalVar [] x y = (x == y)
equalVar ((x,y):bound) z w = (x == z && y == w) || (x /= z && y /= w && equalVar bound z w)

equal' :: [(Var, Var)] -> Term -> Term -> Bool
equal' bound (Belong x1 y1) (Belong x2 y2) = (equalVar bound x1 x2 && equalVar bound y1 y2)
equal' bound Bot Bot = True
equal' bound (Imply u1 v1) (Imply u2 v2) = equal' bound u1 u2 && equal' bound v1 v2
equal' bound (Forall x u) (Forall y v) = equal' ((x,y):bound) u v
equal' _ _ _ = False

equal :: Term -> Term -> Bool
equal e1 e2 = equal' [] e1 e2
$\endgroup$
  • $\begingroup$ Andrej, this works perfectly thank you! $\endgroup$ – Sven Williamson Jun 10 '17 at 16:25

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.