Recursion and Induction: Mutual Recursion Inadequacies
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))
(equal (fx x) x)
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.
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.
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.
Define (slash x s) so that it substitutes the expression substitution s into the expression x, e.g., it returns x/s.
Prove that if s is an expression substitution and x is an expression, then (slash x s) is an expression.
(Maybe explore <<mutual-recursion>>?)