• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Recursion-and-induction

R-and-i-definitional-principle

Recursion and Induction: The Definitional Principle

Below we give a new definitional principle that subsumes the previously given Principle of Structural Recursion.

The definition

(defun f  (v_1 … v_n) β)

is admissible  if and only if

1. f  is a new function symbol,
2. the v_i  are distinct variable symbols,
3. β  is a term that mentions no variable other than the v_i  and calls no new function symbol other than (possibly) f, and
4. there is a term m  (called the measure) such that the following are theorems:
   • Ordinal Conjecture

     (o-p m)

   • Measure Conjecture(s)  For each recursive call of (f a_1 … a_n) in β  and the conjunction q  of tests ruling it,

     (implies q  (o< m/σ  m))

     where σ  is {v_1←a_1,  … , v_n←a_n}.

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<.)

Problem 95.

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

Problem 96.

(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))))) 

Problem 97.
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.

Problem 98.

(defun f1 (i j) 
  (if (and (natp i) 
           (natp j) 
           (< i j)) 
      (f1 (+ 1 i) j) 
      1)) 

Problem 99.

(defun f2 (x) 
  (if (equal x nil) 
      2 
      (and (f2 (car x)) 
           (f2 (cdr x))))) 

Problem 100.

(defun f3 (x y) 
  (if (and (endp x) 
           (endp y)) 
      3 
      (f3 (cdr x) (cdr y)))) 

Problem 101.
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))))

Then admit

(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.

Next: The Induction Principle (or Table of Contents)