When to use it and why?
My question comes from the sentence: "hash cons with some classes and compare their instances with reference equality"
When to use it and why?
My question comes from the sentence: "hash cons with some classes and compare their instances with reference equality"
Putting everyone's answers together:
ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover.
-- Wiki ACL2
In computer programming, cons (pronounced /ˈkɒnz/ or /ˈkɒns/) is a fundamental function in most dialects of the Lisp programming language. cons constructs (hence the name) memory objects which hold two values or pointers to values. These objects are referred to as (cons) cells, conses, or (cons) pairs. In Lisp jargon, the expression "to cons x onto y" means to construct a new object with (cons x y). The resulting pair has a left half, referred to as the car (the first element), and a right half (the second element), referred to as the cdr.
-- Wiki Cons
Logically, hons is merely another name for cons, i.e., the following is an ACL2 theorem:
(equal (hons x y) (cons x y))
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.
Given your question:
hash cons with some classes and compare their instances with reference equality
It appears that hash cons
is the process of hashing a LISP constructor to determine if an object already exists via equality comparison.
http://en.wikipedia.org/wiki/Hash_cons now redirects.
It is con
s with hashing to allow eq
(reference) comparison instead of a deep one. This is more efficient for memory (because identical objects are stored as references), and is of course faster if comparison is a common operation.
http://www.cs.utexas.edu/~moore/acl2/current/HONS.html describes an implementation for Lisp.