versions of a function using different equality tests
Major Section:  PROGRAMMING

The ACL2 environment includes not only a logic but also a programming language, which is based on Common Lisp. Execution efficiency may be increased by using fast equality tests: eq for symbols and eql for numbers, symbols, and characters (see eqlablep). Several list-processing functions built into ACL2 thus have three variants, depending on whether the equality function used is eq, eql, or equal; a list is provided below. ACL2 has taken measures to ensure that one can reason about a single logical function even when one uses these different variants.

Consider for example the case of list membership. Common Lisp provides a utility for this purposes, member, which can take a :TEST keyword argument, default eql. So for example, one might write

(member a x :TEST 'eq)
if either a is a symbol or x is a list of symbols, so that the fastest equality test (eq) may be used when comparing a to successive elements of the list, x. One might elsewhere write (member b (foo y)), which is equivalent to (member b (foo y) :TEST 'eql), for example if b is a number. If one wants to reason about both (member a x :TEST 'eq) and (member b y), it might be helpful for both calls of member to be the same logically, even though Common Lisp will execute them differently (using eq or eql, respectively). ACL2 arranges that in fact, both references to member generate calls of member-equal in the theorem prover.

In fact, since member can take the optional :TEST keyword argument, then in ACl2 it must be defined as a macro, not a function (see defun). ACL2 arranges that a call of member generates a corresponding call of the function member-equal, regardless of the value of TEST, in a manner that produces member-equal in prover output. More generally, you can expect ACL2 to treat your use of member as though you had written member-equal, for example in the way it stores rewrite rules and other kinds of rules as well (see rule-classes). We say little here about how this is all arranged by ACL2, other than to mention that mbe is utilized (so, you might see mention in proof logs) of the function return-last that implements mbe. Such details, which probably can be ignored by most users, may be found elsewhere; see equality-variants-details.

As a convenience to the user, the macro member-eq is provided that expands to a corresponding call of member with :TEST 'eq, as follows.

ACL2 !>:trans1 (member-eq (foo x) (bar y))
ACL2 !>

For efficiency we recommend using the -equal equality variant, for example member-equal or ... :TEST 'equal, in certain contexts: defmacro, defpkg, defconst, and value-triple forms. However, the implementation of equality variants has been designed so that when defining a function, one may choose freely in a definition an equality variant of primitive F, to get efficient execution but where subsequent reasoning is about F-equal. For details about the above recommendation and for a discussion of the implementation, see equality-variants-details.

The following alphabetical list includes all primitives that have equality variants. Each macro F listed below takes an optional :TEST keyword argument of 'eq, 'eql, or 'equal, where 'eql is the default. For each such F, a function F-equal is defined such that for logical purposes (in particular theorem proving), each call of F expands to a corresponding call of F-equal. For convenience, a macro F-eq is also defined, so that a call of F-eq expands to a corresponding call of F with :TEST 'eq.

intersection$ ; (see Note below)
set-difference$ ; (see Note below)
union$ ; (see Note below)

Note: Three of the macros above have names ending with the character, `$': intersection$, set-difference$, and union$. In each case there is a corresponding Common Lisp primitive without the trailing `$': intersection, set-difference, and union. However, Common Lisp does not specify the order of elements in the list returned by those primitives, so ACL2 has its own. Nevertheless, the only use of the trailing `$' is to distinguish the primitives; associated functions and macros, for example union-eq and intersection-equal, do not include the `$' character in their names.

Some Related Topics