Function memoization and unique object representation for ACL2 functions

We have developed an extension of ACL2 that includes the implementation of hash-based association lists and function memoization; this makes some algorithms execute more quickly. This extension, enabled partially by the implementation of Hash-CONS, represents ACL2 objects in a canonical way, thus the comparison of any two such objects can be determined without the cost of descending through their CONS structures. A restricted set of ACL2 user-defined functions may be memoized; the underlying implementation may conditionally retain the values of such function calls so that if a repeated function application is requested, a previously computed value may instead be returned. We have defined a fast association list access and update functions using hash tables. We provide a file reader that identifies and eliminates duplicate representations of repeated objects, and a file printer that produces output with no duplicate subexpressions. General Terms Function Memoization, Hash CONS, AC...

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Robert S. Boyer, Warren A. Hunt Jr.
• Keywords: ACL2, ACL2 2006, Association List, Computational Linguistics, Function Memoization