• 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
        • R-and-i-problematic-nested-recursion
        • R-and-i-mutual-recursion-inadequacies
    • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• R-and-i-more-inadequacies-of-the-definitional-principle

R-and-i-mutual-recursion-inadequacies

Recursion and Induction: Mutual Recursion Inadequacies

Problem 118.
Mutual recursion is (still) not allowed by our statement of the Definitional Principle. However, suppose that somehow the axioms produced by the following pair of definitions were available.

(defun fx (x) 
  (if (consp x) 
      (cons (fx (car x)) 
            (gx (cdr x))) 
      x)) 
 
(defun gx (x) 
  (if (consp x) 
      (cons (gx (car x)) 
            (fx (cdr x))) 
      x)) 

Prove

(equal (fx x) x) 

Problem 119.
Develop a methodology for dealing with mutual recursion. That is, explain how you can use our Definitional Principle to introduce two functions fx and gx that can be shown to satisfy the “defining equations” for fx and gx above. Your methodology should work for any clique of mutually recursive functions that can be shown to terminate under the o< relation.

Problem 120.
We say x is an expression  if (a) x is a symbol or (b) x is a list of the form (f  e_1   …  e_n), where f  is a symbol and the e_i  are expressions. Define (expr x) to recognize expressions.

Problem 121.
An expression substitution  is a list of 2-tuples of the form (v  expr), where v  is a symbol and expr  is an expression. Define substitution to recognize expression substitutions.

Problem 122.
Define (slash x s) so that it substitutes the expression substitution s into the expression x, e.g., it returns x/s.

Problem 123.
Prove that if s is an expression substitution and x is an expression, then (slash x s) is an expression.

(Maybe explore <<mutual-recursion>>?)

Next: Problematic Nested Recursion (or Table of Contents)