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.
hons is merely another name for
cons, i.e., the
following is an ACL2 theorem.
(equal (hons x y) (cons x y))However,
honscreates 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
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
raw Common Lisp. For example, consider this interaction in raw
? (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