Simple recursion occurs when the definition of a named expression includes references to the expression itself - the expression depends on itself. By contrast, mutual recursion is where 2 or more named expressions form a dependency cycle. For example, these definitions of IsEven and IsOdd are mutually dependent:
# assume IsZero, True, False & Pred already defined
IsEven = \ n . (IsZero n) True (IsOdd (Pred n));
^^^^^
IsOdd = \ n . (IsZero n) False (IsEven (Pred n));
^^^^^^IsEven depends on IsOdd which depends on IsEven which depends on... etc
We would like to re-use the approach taken with simple recursion - but that only works for a single self-referencing definition. Therefore we must somehow combine all the mutually recursive definitions (2 in the above example) into a single simply-recursive definition. Furthermore, the original functions (IsEven and IsOdd) must still be recoverable from the combined function. This process is described below after a quick note about combining things using lambda calculus.
Aside: combining arbitrary items
Any list of items, e.g. a, b and c, can be combined into a single expression like this: λ f . f a b c. Note that the f parameter is a function, so this is a higher-order function. This can be considered as a crude list. The list elements can be recovered by applying the list to an accessor function. For example (λ x y z . y) accesses the middle item from a 3 item list because it reduces like this:
=====list==== ==accessor==
(λ f ⋅ f a b c) (λ x y z ⋅ y) // apply the get-middle-item accessor to the list [a, b, c]
(λ x y z ⋅ y) a b c
(λ y z ⋅ y) b c
(λ z ⋅ b) c
b // 'b' has been succesfully extracted from list!These are all the accessors for a 3 item list:
=====list==== ==accessor==
(λ f . f a b c) (λ x y z . x) = a // acessing the 1st item of list [a, b, c]
(λ f . f a b c) (λ x y z . y) = b // acessing the 2nd item of list [a, b, c]
(λ f . f a b c) (λ x y z . z) = c // acessing the 3rd item of list [a, b, c]Thus we can easily combine a list of expressions into a single expression and recover them later using an appropriate accessor. Obviously this approach can be applied to lists of any fixed finite length
Returning to our problem, begin by combining the definitions of IsEven and IsOdd into a 2 element list called F. We use the approach described above, which gives an expression of the form λ f . f a b where a is the definition of IsEven and b is the definition of IsOdd:
F = λ f . f (λn.(IsZero n) True (IsOdd (Pred n))) (λn.(IsZero n) False (IsEven (Pred n)))
^^^^^^^^^^^^^^IsEven^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^IsOdd^^^^^^^^^^^^^^^^^^Notice that the definition of F still includes explicit references to IsEven and IsOdd which we need to remove.
As noted in the aside above, the elements of list F (the definitions of IsEven and IsOdd) can be retrieved using accessors, giving:
IsEven = F (λ x y . x) // (λ x y . x) is the get-first-item accessor
IsOdd = F (λ x y . y) // (λ x y . y) is the get-second-item accessor
These are definitions of IsEven and IsOdd in terms of F, which we can substitute back into the definition of F (to remove the explicit references to IsEven and IsOdd) :
F = λ f . f (λn.(IsZero n) True (F (λ x y . y) (Pred n))) (λn.(IsZero n) False (F (λ x y . x) (Pred n)))
^^^^IsOdd^^^ ^^^^IsEven^^^There are no explicit references to IsEven or IsOdd in this equation. This is a definition of F that includes references to F in its body - i.e. this is an example of simple recursion.
Now we produce a non-recursive definition of F by following the procedure for simple recursion - let's call the result F'. The final step is to re-use the equations above for IsEven and IsOdd (but using the non-recursive F' instead of the equivalent (but recursive) F) :
IsEven = F' (λ x y . x)
IsOdd = F' (λ x y . y)The process is complete: we started with mutually recursive definitions of IsEven and IsOdd and finished with non-recursive definitions. Generalising from the above example gives this procedure for dealing with mutually-recursive functions:
# start with n mutualy recursive named expressions:
# each body term stands for an expression that may include mutiple references to E1 .. En
E1 = bodyE1
E2 = bodyE2
: :
En = bodyEn
# combine into a single expression:
F = λ f . f (bodyE1) (bodyE2) ... (bodyEn)
# replace every reference Ei in the right-hand side bodies with: F (λ x1 x2 ... xn . xi)
# call the transformed bodies: bodyE1' bodyE2' ... bodyEn', giving:
F = λ f . f (bodyE1') (bodyE2') ... (bodyEn')
# F is simply-recursive and can be re-defined non-recursively as, say, F'
# finally define:
E1 = F' (λ x1 x2 ... xn . x1)
E2 = F' (λ x1 x2 ... xn . x2)
: :
En = F' (λ x1 x2 ... xn . xn)