NORMED

Major Section:  HONS-AND-MEMOIZATION

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

In Common Lisp, we can tell whether an ACL2 object is normed or not, but there is no way for an ordinary ACL2 function to see whether an object is normed. Hence, whether or not an object is normed is an implementation-level concept.

The fundamental property of normed objects is that if A and B are both normed, then (equal A B) holds if and only if (eql A B) holds. For strings and conses, (eql A B) holds only when (eq A B), so any normed conses or strings are equal precisely when they are eq. The potential benefits of having normed objects include: constant-time equality comparisons, reduced memory usage, fast association lists, and function memoization.

Note that in our implementation, all symbols, characters, and numbers are automatically normed, and whenever a cons is normed its car and cdr must also be normed.

The Meaning of Normed in Common Lisp.

Recall that the ACL2 Objects are certain "good" Common Lisp symbols, characters, strings, and numbers, and the conses which can be recursively formed from these good atoms.

Not all properties of these objects are visible in the ACL2 logic. An example of an invisible property is the pointer identity of an object. For example, suppose we write the following.

 (defconst *x* (cons 1 2))
 (defconst *y* (cons 1 2))

In Common Lisp, cons is guaranteed to provide a new pair that is distinct from any previously created pair, so we know that *x* and *y* will be distinct objects and we will be able to tell them apart from one another using eq. But this difference is not visible in the ACL2 logic, and no ACL2 function can tell *x* apart from *y*.

The normed-ness of an object is a similarly invisible property. In Common Lisp, invisible to ACL2, we maintain a data structure called a "Hons Space" that records which objects are normed. So, being normed is not an intrinsic property of an object, but instead is determined by whether the object is mentioned in this Hons Space.

Notes about Garbage Collection.

The Hons Space includes tables with pointers to every normed cons and string. One consequence of this is that normed objects cannot be reclaimed by Lisp's ordinary garbage collector, even after they have become unreachable from the perspective of an ACL2 program.

For CCL users only, hons-wash is a special kind of garbage collection that allows normed conses to be reclaimed. For other Lisps, the only option is to occasionally, manually clear out these Hons Space tables with hons-clear.