Recursion and Induction: The Definitional Principle
Below we give a new definitional principle that subsumes the previously given Principle of Structural Recursion.
(defun f (v_1 … v_n) β)
is admissible if and only if
If that definition is admissible, then it adds the axiom:
(f v_1 … v_n) = β.
In each of the problems below, admit the proposed definition, i.e., identify the measure and prove the required theorems.
(Maybe explore <<defun>>? Note in particular how the user can explicitly specify the measure and well-founded relation alleged to decrease. When specified, the system will attempt to prove it decreases as per the Definitional Principle. If no measure is specified by the user, the system attempts to find an argument whose ACL2-count decreases according to o<.)
(defun tree-copy (x) (if (atom x) x (cons (tree-copy (first x)) (tree-copy (rest x)))))
(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)))))
Recursion like that in ack allows us to define functions that cannot be defined if we are limited to “primitive recursion” where a given argument is decremented in every recursive call. That is, the new definitional principle is strictly more powerful than the old one. This can be formalized and proved within our system (after we extend the principle of induction below). If you are inclined towards metamathematics, feel free to pursue the formalization and ACL2 proof of this. The existence of non-primitive recursive functions, dating from 1928, by Wilhelm Ackermann, a student of David Hilbert, was one of the important milestones in our understanding of the power and limitations of formal mathematics culminating in Goedel's results of the early 1930s.
(defun f1 (i j) (if (and (natp i) (natp j) (< i j)) (f1 (+ 1 i) j) 1))
(defun f2 (x) (if (equal x nil) 2 (and (f2 (car x)) (f2 (cdr x)))))
(defun f3 (x y) (if (and (endp x) (endp y)) 3 (f3 (cdr x) (cdr y))))
Suppose p, m, up, and dn (“down”) are undefined functions. Suppose however that you know this about p, m, and dn:
Theorem dn-spec (and (o-p (m x)) (implies (p x) (o< (m (dn x)) (m x))))
(defun f4 (x y q) (if (p x) (if q (f4 y (dn x) (not q)) (f4 y (up x) (not q))) 4))
Note that f4 is swapping its arguments. Thus, if q starts at t, say, then in successive calls the first argument is x, y, (dn x), (up y), (dn (dn x)), (up (up y)), etc. I thank Anand Padmanaban for helping me think of and solve this problem.