|
|
|---|
|
|
|
|---|
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 (cc x) to return the number of conses in x. The name
stands for “cons count.”
Problem 83.
Prove that cc always returns a non-negative integer.
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 cc is a natural
number, this proof establishes that tree-copy terminates on all
objects.
Problem 86.
Define (rm e x) to return the result of removing the first occurrence
(if any) of e from x.
Thus, (rm 3 '(1 2 3 4 3 2 1)) is (1 2 4 3 2 1).
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 (f23 e x) always return 23. Can you prove that with
our current logical machinery?
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.
Ack always terminates. Why? Don't feel compelled to give a
formal proof, just an informal explanation.
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: