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