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 Expr
s. 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.
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With