1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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
|
