formals that are used but only insignificantly
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 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.