summaryrefslogtreecommitdiffstats
path: root/content/zettel/3c3c.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/3c3c.md')
-rw-r--r--content/zettel/3c3c.md40
1 files changed, 40 insertions, 0 deletions
diff --git a/content/zettel/3c3c.md b/content/zettel/3c3c.md
new file mode 100644
index 0000000..2751f65
--- /dev/null
+++ b/content/zettel/3c3c.md
@@ -0,0 +1,40 @@
++++
+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.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-six20_certif_effic_instr_sched" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">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].</span>
+
+</div>
+
+</div>
+
+ [10.1145/3428197]: https://doi.org/10.1145/3428197