Major Section: PROGRAMMING
fn be a function of
n arguments. Let
x be the
ith formal of
x is ``irrelevant in
x is not involved in either the
guard or the measure for
x is used in the body, but the value of
(fn a1...ai...an) is independent of
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
(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
xis 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
xis 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
xonly 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
guardrequiring both arguments to be nonnegative integers and the
(+ 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
xirrelevant -- 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-tablefor 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.