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

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

**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

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

**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: