HONS-ACONS

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.

Logically, hons-acons is like acons except that its guard does not require alistp; we leave it enabled and would think it odd to ever prove a theorem about it.

Under the hood, two things are done differently. First, the key is copied with hons-copy; this lets us use EQL-based hash tables instead of EQUAL-based hash tables for better performance. Second, assuming there is a valid hash table associated with this alist, we destructively update the hash table by binding key to val. The hash table will no longer be associated with alist, but will instead be associated with the new alist returned by hons-acons.

Hash Table Creation

A new hash table is created by hons-acons whenever alist is an atom. Unlike ordinary acons, we do not require that alist be nil, and in fact you may wish to use a non-nil value for one of two reasons.

1. As a size hint

By default, the new hash table will be given a quite modest default capacity of 60 elements. As more elements are added, the table may need to be resized to accommodate them, and this resizing has some runtime cost.

When a natural number is used as a fast alist's name, we interpret it as a size hint. For example, (hons-acons 'foo 'bar 1000) instructs us to use 1000 as the initial size for this hash table and binds 'foo to 'bar. The resulting table should not need to be resized until more than 1000 elements are added. We ignore size hints that request fewer than 60 elements.

Because of hash collisions, hash tables typically need to have a larger size than the actual number of elements they contain. The hash tables for fast alists are told to grow when they reach 70% full. So, an easy rule of thumb might be: multiply the expected number of elements you need by 1.5 to keep your hash tables about 2/3 full.

2. As an alist name

We also frequently use a symbol for alist, and think of this symbol as the name of the new alist. We have found that naming alists can be valuable for two reasons:

First, the name can be helpful in identifying fast alists that should have been freed, see fast-alist-summary.

Second, names can sometimes be used to avoid a subtle and insidious table-stealing phenomenon that occurs when using fast-alists that are themselves normed; see hons-acons!.

At the moment, there is no way to simultaneously name a fast alist and also give it a size hint. We may eventually allow strings to include embedded name and size components, but for now we have not implemented this capability.