Alpha Equivalent Hash Consing with Thinnings

This article discusses a technique for hash consing terms with alpha equivalence using thinnings, which are bitvectors describing how to prune a list. It builds on previous work on thinnings and union-find with thinning annotations. The method attaches a thinning to each child node in a hash cons, allowing variable references to be resolved by composing thinnings. This enables sharing of structure across terms that differ only in de Bruijn indices, such as deeply nested lambda abstractions with different variable references. The article includes code snippets for a basic hash cons implementation and explains how thinnings reduce memory usage and improve equality checking for compiler analysis.