Recursion and Induction: Inadequacies of Structural Recursion

Recall that to avoid logical contradictions introduced by “bad”
definitions, we imposed four restrictions. The fourth restriction is very
constraining: we can only recur on a `car`/`cdr` component of some
argument and must ensure that that argument satisfies `consp` before the
recursion.

The intent of this restriction was to guarantee that the newly defined
function terminates. It is beyond the scope of these notes to explain why
termination is linked to consistency, but the intuitive explanation is that
if the recursion cannot go on forever then, for every combination of
constants to which we apply the function, we could compute a value satisfying
the definitional equation (given enough computational resources). From this
observation we can conclude there exists a mathematical function satisfying
the definitional equation – namely, the one that maps inputs to the computed
outputs. Thus, given a model of the theory before we added the definition, we
could extend it to a model of the theory with the new definition added. This
establishes the consistency of the extended theory.
(Remark. In fact,
our definitions produce *conservative extensions*, which we will
briefly discuss below.)
The problem with the current version of our fourth restriction is that it is
too syntactic – it insists, literally, on the use of `consp`, `car`,
and `cdr`. In the ACL2 definitional principle, the fourth restriction is
less syntactic: it requires that we be able to *prove* that the
recursion terminates. That is, when we propose a new definition, a
conjecture is generated and if this conjecture can be proved as a theorem,
then we know the function terminates.

The basic idea of this conjecture is to establish that some measure of the
function's arguments decreases in size as the function recurs, and this
decreasing cannot go on forever. If the size were, say, a natural number,
then we would know the decreasing could not go on forever, because the
arithmetic less-than relation, `<`, is *well-founded* on the natural
numbers. We discuss well-foundedness more in the next section.

**Problem 82. ** Define

**Problem 83. ** Prove that

**Problem 84. ** If we define

(defun atom (x) (not (consp x))) (defun first (x) (car x)) (defun rest (x) (cdr x))

then the following “definition” of `tree-copy` is logically equivalent
to the acceptable version, but it is considered unacceptable by our syntactic
fourth restriction:

(defun tree-copy (x) (if (atom x) x (cons (tree-copy (first x)) (tree-copy (rest x)))))

Write down a conjecture that captures the idea that the argument to
`tree-copy` is getting smaller (as measured by `cc`)
as the function recurs.

**Problem 85. ** Prove the conjecture above. Note that since

**Problem 86. ** Define

**Problem 87. ** Show that the following function terminates.

(defun f23 (e x) (if (mem e x) (f23 e (rm e x)) 23))

Note that no `car`/`cdr` nest around `x` is equal to the result
of `(rm 3 '(1 2 3))`. Thus, `f23` exhibits a kind of recursion
we have not seen previously – but we know it terminates.

**Problem 88. ** It is obvious that

The key to these termination proofs is that the less-than relation is well-founded on the natural numbers. But consider this famous function, known as Ackermann's function,

(defun ack (x y) (if (zp x) 1 (if (zp y) (if (equal x 1) 2 (+ x 2)) (ack (ack (- x 1) y) (- y 1)))))

Observe that `ack` can generate some very large numbers.
For example, `(ack 4 3)` is `65536`.

**Problem 89. **

In the next three sections of this document we will discuss a well-founded
relation far more powerful than less-than on the natural numbers. We will
then connect that well-foundedness machinery to a new version of the
Definitional Principle, so that we can admit many interesting recursive
functions, including `ack`. We will also connect the well-foundedness
machinery to a new version of the Induction Principle, so that we can prove
that `(f23 e x)` is `23` – and far more interesting theorems.

Next: