hash cons

This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization.

Logically, hons is merely another name for cons, i.e., the following is an ACL2 theorem.

(equal (hons x y) (cons x y))
However, hons creates a special kind of cons pair, which we call a hons pair or, for short, hons.

Hons generally runs slower than cons because in creating a hons, an attempt is made to see whether a hons already exists with the same car and cdr. This involves search and the use of hash-tables. In the worst case, honsing can be arbitrarily slow, but our experience in OpenMCL is that honsing is generally about 20 times as slow as consing.

In our implementation, every hons really is a cons pair, but not every cons pair is a hons, as can be determined by using eq in raw Common Lisp. For example, consider this interaction in raw Common Lisp.

? (setq x (cons 1 2))
(1 . 2)
? (setq y (hons 1 2))
(1 . 2)
? (setq z (hons 1 2))
(1 . 2)
? (eq y z)
? (eq x y)