1
$\begingroup$

The hash function should be invariant under alpha-renaming. Using de Bruijn notation seems to be possible, but it requires alpha-converting the whole tree when a binding is created, and has the unhappy consequence that a substructure of an abt is not a well-formed abs (since the de Bruijn indices are broken). So, is there a good (neat, elegant and/or efficient) way to construct such a function? By the way, is there any study on this matter? Any help is appreciated!

$\endgroup$
1
  • $\begingroup$ Just use de Bruijn indices and live with the overhead. It's smaller than anything else I know of. Regarding subexpressions being broken: no they're not broken, you just need to redefine your notion of "subexpression" because it is not "subtree" anymore (because some nodes in your trees are binders). $\endgroup$ Jun 3, 2019 at 10:34

1 Answer 1

0
$\begingroup$

I found a paper published two years later. Hashing modulo alpha-equivalence. This provides an asymptotically faster way to achieve the goal, improving from $O(n^2)$ to $O(n \log^2 n)$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.