Irrelevant-formals
Formals that are used but only insignificantly
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 anywhere in its definition. 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, or if it occurs free in an xargs term associated with
:measure, :guard, or :split-types, 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 (zp 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; let us call these the ``clearly
irrelevant formals.'' For example, if the ith formal is only used in the
ith argument position of recursive calls, then it is clearly irrelevant.
This is how x is used above.
It is possible for a formal to appear only in recursive calls but not be
clearly irrelevant, or even irrelevant at all. For example, x is
not irrelevant below, even though it only appears in the recursive
call.
(defun fn (i x y)
(if (zp i) y (fn (1- i) y x)))
The following examples show the relevance of x.
ACL2 !>(fn 1 3 0)
3
ACL2 !>(fn 1 4 0)
4
ACL2 !>
The key observation for the definition of fn is that while x only
appears in a recursive call, it appears in the argument position for a formal
that is not clearly irrelevant, namely y's.
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 to determine the ``clearly
irrelevant'' formals 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. By default, ACL2 causes an error on
such definitions. In most cases the best remedy for such an error is to
recode the definition so as to eliminate the irrelevant formals. Another
option is to declare the irrelevant formals, for example as
follows.
(defun fact (i x)
(declare (irrelevant x))
(if (zp i) 0 (* i (fact (1- i) (cons i x)))))
Note that an irrelevant declaration is only legal for a defun form, not in other contexts that allow declarations (let,
etc.).
To turn off the checking of irrelevant formals globally (though we do not
recommend avoiding those checks), see set-irrelevant-formals-ok. In
that case ACL2 will ignore every irrelevant declaration. But otherwise,
and by default, if you provide an irrelevant declaration (see declare), then it must specify exactly the formals that ACL2 determines to be
irrelevant, what we call the ``clearly irrelevant'' formals above: any formal
declared irrelevant that is not clearly irrelevant will cause an error.
Subtopics
- Irrelevant-formals-info
- Determine whether irrelevant-formals are OK in definitions.
- Chk-irrelevant-formals-ok
- Check irrelevant-formals in definitions.
