Comparison of syntax trees modulo alpha conversion

Question

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

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

if there was a way to test alpha equivalence (equivalence modulo renaming) Expr s. However, this Expr differs from lambda calculus in that the set of variables in lambda is commutative, i.e. The order of the parameters does not affect the validation.

(For simplicity, however, Lambda ["x","y"] ... is different from Lambda ["x"] (Lambda ["y"] ...) , in which case the order matters).

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

Answer 1

Commutativity of parameters hints at exponential comparison, true.

But I suspect that you can normalize parameter lists, so you only need to compare them in one order. Then comparing the tree with the renaming will be essentially linear in size of the trees.

What I propose to do is that for each list of parameters, visiting a subtree in (in order, in order, does not matter as long as you are consistent) and sorting the parameter by the index of the order in which the visit occurs first meet the use parameter. Therefore, if you have

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

you should sort the parameter list as:

  lambda(b,a) 

because you will meet b first, then the second, and the extra b meeting does not matter. Compare trees with a normalized list of parameters.

Life becomes merciless if you insist that operators in the lambda condition can be commutative. I guess you can still normalize it.

Answer 2

We can turn to Daan Leijen HMF for a few ideas. (It deals with binders for "foralls", which also occur as commutative ones.

In particular, he rechecks the variables in the order they appear in the body.

Then a comparison of terms involves simultaneously sliding and comparing the results.

We can do this better by replacing this skolemization pass with a locally nameless view .

 data Bound ta = Bound {-# UNPACK #-} !Int t | Unbound a instance Functor (Bound t) where ... instance Bifunctor Bound where ... data Expr a = Lambdas {-# UNPACK #-} !Int (Expr (Bound () a)) | Var a 

So, now the occurrences of Bound under the lambda are variables connected directly by the lambda, as well as any type information that you want to insert, here I just used ().

Now, closed terms are polymorphic in 'a', and if you sort lambda elements on your site (and you can guarantee that you can always canonicalize lambda by removing unused terms) alpha-equivalent terms are compared simply with (==), and if you need open terms, you can work with Expr String or some other representation.

A more anal retentive version of the signature for Expr and Bound will use the existential type and the level type natural to determine the number of related variables and use the “Fin” in the Bound constructor, but since you must already maintain the invariant, you are binding more variables than # occurring in lambda, and that type information matches all Var (Bound n _) with the same n , which is not too important to maintain another.

Update. You can use my bound package to make it a better version in a completely autonomous way!