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!

  • $\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 Bauer Jun 3 '19 at 10:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.