+++ title = "Hash consing" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3c3b"] forwardlinks = ["3c3d", "3c3c1"] zettelid = "3c3c" +++ Hash consing is a property that can be used to perform faster equality checks between abstract terms, without having to go through each term sequentially. This is basically done by having a hash table that gets assigned terms of the same structure. This means that each term of the same structure will get the same pointer, which means that one just has to compare pointers to confirm structural equality. The following property has, however, not been formally proven in \[1\], which instead is left as an unproven assumption that: $$ p = q \rightarrow *p = *q $$ Which should be true for hash consed terms.
\[1\] C. Six, S. Boulmé, and D. Monniaux, “Certified and efficient instruction scheduling: Application to interlocked VLIW processors,” *Proc. ACM Program. Lang.*, vol. 4, no. OOPSLA, Nov. 2020, doi: [10.1145/3428197].
[10.1145/3428197]: https://doi.org/10.1145/3428197