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 is not involved in either the
guard or the measure for fn, x is used in the body, but 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.
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) 0 (* 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 :guard
requiring both arguments to be nonnegative integers and the :measure
(+ i 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) x 0))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.
If you need to introduce a function with an irrelevant formal,
please explain to the authors why this should be allowed.