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!
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$– Andrej BauerCommented Jun 3, 2019 at 10:34
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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)$.