Major Section: PROGRAMMING
Let fn be a function of n arguments. Let x be the ith formal
of fn. We say x is ``irrelevant in fn'' if x does not occur
in either the guard or the measure for fn, and the value of
(fn a1...ai...an) is independent of ai.
The easiest way to define a function with an irrelevant formal is simply not
to use the formal in the body of the function. Such formals are said to be
``ignored'' by Common Lisp and a special declaration is provided to allow
ignored formals. ACL2 makes a distinction between ignored and irrelevant
formals. Note however that if a variable is declared ignored or
ignorable, then it will not be reported as irrelevant.
An example of an irrelevant formal is x in the definition of fact
below.
(defun fact (i x) (declare (xargs :guard (and (integerp i) (<= 0 i)))) (if (zerop i) 1 (* i (fact (1- i) (cons i x))))).Observe that
x is only used in recursive calls of fact; it never
``gets out'' into the result. ACL2 can detect some irrelevant formals by a
closure analysis on how the formals are used. For example, if the ith
formal is only used in the ith argument position of recursive calls, then
it is irrelevant. This is how x is used above.It is possible for a formal to appear only in recursive calls but still be
relevant. For example, x is not irrelevant below, even though it
only appears in the recursive call.
(defun fn (i x) (if (zerop i) 0 (fn x (1- i))))The key observation above is that while
x only appears in a recursive
call, it appears in an argument position, namely i's, that is
relevant. (The function above can be admitted with a :measure of
(+ (nfix i) (nfix x)).)Establishing that a formal is irrelevant, in the sense defined above, can be
an arbitrarily hard problem because it requires theorem proving. For
example, is x irrelevant below?
(defun test (i j k x) (if (p i j k) 0 x))Note that the value of
(test i j k x) is independent of x -- thus
making x irrelevant -- precisely if (p i j k) is a theorem. ACL2's
syntactic analysis of a definition does not guarantee to notice all
irrelevant formals.We regard the presence of irrelevant formals as an indication that something
is wrong with the definition. We cause an error on such definitions and
suggest that you recode the definition so as to eliminate the irrelevant
formals. If you must have an irrelevant formal, one way to ``trick'' ACL2
into accepting the definition, without slowing down the execution of your
function, is to use the formal in an irrelevant way in the guard. For
example, to admit fact, above, with its irrelevant x one might use
(defun fact (i x) (declare (xargs :guard (and (integerp i) (<= 0 i) (equal x x)))) (if (zerop i) 0 (* i (fact (1- i) (cons i x)))))For those who really want to turn off this feature, we have provided a way to use the
acl2-defaults-table for this purpose;
see set-irrelevant-formals-ok.
