Major Section: HONS-AND-MEMOIZATION
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 CCL 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) T ? (eq x y) NIL
