		Search-engine friendly clone of the ACL2 documentation.

Recursion-and-induction

R-and-i-definitions-revisited

Recursion and Induction: Definitions Revisited

Problem 27.
Suppose we define

(defun f (x) 1)

and then prove some theorems and then “redefine” f with

(defun f (x) 2)

Now prove that (equal 'June' 'July), using the theorems that (equal (f x) 1), proved before redefining f, and (equal (f x) 2), proved after.

Flesh out your argument using axioms presented earlier (see r-and-i-axioms and see r-and-i-definitions-revisited).

A consequence is that since anything provable is valid, then the formula (equal 'June 'July) ≠ nil is true, hence 'June = 'July, a contradiction! In the following Problems we explore further such consequences of permitting “bad” definitions.

Problem 28.
Suppose we define

(defun f (x) (cons x y))

Prove (equal 1 2). (Remark. The definition f in this problem has nothing to do with the definition of f in the previous problem! We tend to “re-use” function names like f, g and h from time to time simply to avoid inventing new names.)

Problem 29.
Suppose we define

(defun f (x) (not (f x)))

Prove (equal t nil).

These problems should disturb you! We often think of “definitions” as being logically innocuous, allowing us to abbreviate complicated expressions. And we think of proof as a way to determine truth. So it is disturbing if after making a “definition” we are suddenly able to prove things we know aren't true, like that June is July or that t is nil! Something has gone terribly wrong.

To prevent this kind of logical inconsistency, we impose some restrictions on our ability to introduce definitions. The restrictions we'll impose will prevent us from defining many useful functions but guarantee that we don't ruin the logic with “definitions” like those shown above. ACL2 is much more generous in its restrictions but they are spiritually similar: both here and in ACL2 the restrictions on definitions will guarantee that every defined function terminates. We do not explain in this document why termination is enough to avoid inconsistencies.

One way to make sure a function terminates is to insist that there is an argument that is being car'd and/or cdr'd at least once every time the function recurs and that before it recurs the definition tests that the argument is a cons-pair. For example, (defun f (x) (not (f x))) is disallowed by this restriction, and so is (defun f (x) (not (f (cdr x)))). But

(defun f (x) 
  (if (consp x) 
      (and (not (f (car x))) 
           (not (f (cdr (cdr x))))) 
      t))

is allowed because x is car'd and/or cdr'd in every recursion and the function tests (consp x) before recurring. We say (consp x) “rules” the two recursive calls above.

So we have to define the notions of a “car/cdr” nest and what terms “rule” the recursive calls.

A car/cdr nest around v is (car v), (cdr v), or a car/cdr nest around (car v) or (cdr v). Thus, (car (cdr (car x))) is a car/cdr nest around x.

The idea in this next definition is to take a term β and a particular occurrence r of some subterm in β and define the set of tests that rule r. Then, if you have a function definition like (defun f (v_1 … v_k) β) you can let r be a particular recursive call of f in β and then determine which tests rule that call.

The rulers of an occurrence of a term r in another term β is the set defined as follows:

if β is (if p x y) and r is in x, then the rulers of r in β is the set obtained by adding p to the set of rulers of r in x;
if β is (if p x y) and r is in y, then the rulers of r in β is the set obtained by adding (NOT p) to the set of rulers of r in y;
otherwise, the rulers of r in β is the empty set.

Thus, in the term (if a (if b (h c) (h d)) (g c)), both a and b rule the first occurrence of c and the occurrence of (h c). In addition, a and (not b) rule the occurrences of d and (h d). Finally, (not a) rules the second occurrence of c and (g c).

Note that our definition of “rulers” does not include every test that has to be true in order to reach the occurrence in question. For example, p does not rule the occurrence of a in (car (if p a b)) even though the only way evaluation can reach a is if p is true. The rulers of the occurrence of a in that term is the empty set, because that term is not a call of if. However, p does rule the occurrence of a in the equivalent term (if p (car a) (car b)). The reason we've defined rulers this way has to do with heuristics in the ACL2 theorem prover.

Principle of Structural Recursion: A definition, (defun f (v_1 … v_n) β) will be allowed (for now) only if it satisfies these four restrictions:

The symbol being defined, f, must be “new,” i.e., not already in use as a function symbol in any axiom.
The formal variables, v_1, … , v_n, must be distinct variable symbols.
The body, β, must be a term, it must use no new function symbol other than (possibly) f, and the only variable symbols in it are among the formals.
There is an i such that (consp v_i) rules every recursive call of f in β and for every recursive call (f a_1 ... a_n) in β, a_i is a car/cdr nest around v_i. We call v_i a measured formal.

An acceptable definition adds the axiom (f v_1 … v_n) = β.

(Maybe explore <<defun>>? Be advised, however, that ACL2's Definitional Principle does not insist on the last condition above, about there being a car/cdr nest in a certain argument of every recursive call. Instead it insists that “some measure of the arguments decreases” in every recursive call. We'll make that clearer later. But ACL2's Definitional Principle allows all the definitions described above.)

Problem 30.
Explain why these restrictions rule out the spurious definitions of f in the problems above.

Problem 31.
Is the following definition allowed under the above restrictions?

(defun f (x) 
  (if (consp x) 
      (if (consp (cdr x)) 
          (f (cdr (cdr x))) 
          nil) 
      t))

Problem 32.
Is the following definition allowed?

(defun f (x y) 
  (if (consp x) 
      (f (cons nil x) (cdr y)) 
      y))

Problem 33.
Is the following definition allowed?

(defun f (x y) 
  (if (consp x) 
      (f (cons nil y) (cdr x)) 
      y))

Problem 34.
Is the following definition allowed?

(defun f (x) 
  (if (not (consp x)) 
      x 
      (f (cdr (cdr x)))))

Problem 35.
Is the following sequence of definitions allowed?

(defun endp (x) (not (consp x))) 
 
(defun f (x) 
  (if (endp x) 
      nil 
      (cons nil (f (cdr x)))))

Problem 36.
Is the following definition allowed?

(defun f (x y) 
  (if (consp x) 
      (f (cdr x) (cons nil y)) 
      y))

Problem 37.
Is the following definition allowed?

(defun f (x y) 
  (if (consp x) 
      (f (cdr x) 
         (f (cdr x) y)) 
      y))

Problem 38.
Is the following sequence of definitions allowed?

(defun f (x) 
  (if (consp x) 
      (g (cdr x)) 
      x)) 
 
(defun g (x) 
  (if (consp x) 
      (f (cdr x)) 
      x))

Next: Structural Induction (or Table of Contents)