Comparing syntax trees modulo alpha conversion

Question

I am working on a compiler/proof checker, and I was wondering, if I had a syntax tree such as this, for example:

data Expr
    = Lambdas (Set String) Expr
    | Var String
    | ...

if there were a way to check the alpha-equivalence (equivalence modulo renaming) of Exprs. This Expr, however, is different from the lambda calculus in that the set of variables in a lambda is commutative -- i.e. the order of parameters does not factor in to the checking.

(For simplicity, however, Lambda ["x","y"] ... is distinct from Lambda ["x"] (Lambda ["y"] ...), and in that case the order does matter).

In other words, given two Exprs, how can one efficienly find a renaming from one to the other? This kind of combinatorial problem smells of NP-complete.

Answer 1

The commutativity of the parameters does hint at an exponential comparision, true.

But I suspect you can normalize the parameter lists so you only have to compare them in single order. Then a tree compare with renaming would be essentially linear in the size of the trees.

What I suggest doing is that for each parameter list, visit the subtree in (in-order, postorder, doesn't matter as long as you are consistent) and sort the parameter by the index of the order in which the visit first encounter a parameter use. So if you have

  lambda(a,b):  .... b .....  a  ... b ....

you'd sort the parameter list as:

  lambda(b,a)

because you encounter b first, then a second, and the additional encounter of b doesn't matter. Compare the trees with the normalized parameters list.

Life gets messier if you insist the the operators in a lambda clause can be commutative. My guess is that you can still normalize it.