Mutual induction and recursion over natural numbers

The goal of this lecture note is to articulate the mutually inductive specification of a computation over natural numbers and how to program the corresponding mutually recursive functions in OCaml.

Resources

• The OCaml code for the present lecture note (latest version: 29 Feb 2020).

Mutual recursion in OCaml

<expression> ::= ...
               | let rec <formal> = fun <formal> -> <expression> {and <formal> = fun <formal> -> <expression>}* in <expression>

The corresponding typing rule reads as follows:

REC	(f1 : t1 -> t1'), ..., (fN : tN -> tN'), G |- fun x1 -> e1 : t1 -> t1'	...	(f1 : t1 -> t1'), ..., (fN : tN -> tN'), G |- fun xN -> eN : tN -> tN'	(f1 : t1 -> t1'), ..., (fN : tN -> tN'), G |- e0 : t0
	G |- let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0 : t0

In words: in any type environment G, the expression let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0 has type t0 whenever, in an extension of this environment where f1 has type t1 -> t1', ..., fN has type tN -> tN',

1. fun x1 -> e1 has type t1 -> t1',
2. fun x2 -> e2 has type t2 -> t2',

...

14. fun xN -> eN has type tN -> tN', and

0. e0 has type t0.

Even or odd

Let us revisit the even and odd predicates:

let test_evenp candidate =
      (* a few handpicked numbers: *)
  let b1 = (candidate 1 = false)
  and b2 = (candidate 2 = true)
  and b3 = (candidate 3 = false)
  and b4 = (candidate 4 = true)
  and b5 = (candidate 5 = false)
  and b6 = (candidate 1000 = true)
  and b7 = (candidate 1001 = false)
      (* testing the completeness of the even predicate: *)
  and b8 = (let n = Random.int 1000
            in candidate (2 * n) = true)
  and b9 = (let n = Random.int 1000
            in candidate (2 * n + 1) = false)
      (* an instance of the base case: *)
  and bc = (candidate 0 = true)
      (* an instance of the induction step: *)
  and is = (let n' = Random.int 1000
            in candidate (succ n') = not (candidate n'))
  (* etc. *)
  in b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 && b9 && bc && is;;

let test_oddp candidate =
      (* a few handpicked numbers: *)
  let b1 = (candidate 1 = true)
  and b2 = (candidate 2 = false)
  and b3 = (candidate 3 = true)
  and b4 = (candidate 4 = false)
  and b5 = (candidate 5 = true)
  and b6 = (candidate 1000 = false)
  and b7 = (candidate 1001 = true)
      (* testing the completeness of the odd predicate: *)
  and b8 = (let n = Random.int 1000
            in candidate (2 * n) = false)
  and b9 = (let n = Random.int 1000
            in candidate (2 * n + 1) = true)
      (* an instance of the base case: *)
  and bc = (candidate 0 = false)
      (* an instance of the induction step: *)
  and is = (let n' = Random.int 1000
            in candidate (succ n') = not (candidate n'))
  (* etc. *)
  in b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 && b9 && bc && is;;

This time, however, let us define them together, since if a number is odd, its successor is even, and if a number is even, its succcessor is odd:

• base case: 0 is even and 0 is not odd
• induction step: given a number n' such that its evenness is the Boolean ih_even and that its oddness is the Boolean ih_odd, the evenness of succ n' is the oddness of n', i.e., ih_odd, and the oddness of succ n' is the evenness of n', i.e., ih_even

Since the two predicates are defined together, let us test them together:

let test_evenp_and_oddp evenp oddp =
      (* an instance of the base cases: *)
  let b0 = (evenp 0 = true)
  and b1 = (oddp 0 = false)
      (* an instance of the induction steps: *)
  and b2 = (let n' = Random.int 1000
            in evenp (succ n') = oddp n')
  and b3 = (let n' = Random.int 1000
            in oddp (succ n') = evenp n')
  (* etc. *)
  in b0 && b1 && b2 && b3;;

And since the two predicates are defined together, let us implement them together, i.e., in a mutually recursive way:

let rec evenp_v3 n =
  if n = 0
  then true
  else let n' = n - 1
       in oddp_v3 n'
and oddp_v3 n =
  if n = 0
  then false
  else let n' = n - 1
       in evenp_v3 n';;

The two functions evenp_v3 and oddp_v3 call each other. They are mutually recursive, and they pass the unit tests:

# test_evenp evenp_v3;;
- : bool = true
# test_oddp oddp_v3;;
- : bool = true
# test_evenp_and_oddp evenp_v3 oddp_v3;;
- : bool = true
#

To shield them against negative integers, let us provide an interface:

let evenp_v4 n =
  let () = assert (0 <= n)
  in evenp_v3 n;;

let oddp_v4 n =
  let () = assert (0 <= n)
  in oddp_v3 n;;

To visualize the computation, let us instrument these implementations with tracing information. The idea is that every call to evenp_v3 and to oddp_v3 emits a trace, and that so does every return:

let rec traced_evenp_v3 n i =
  let () = Printf.printf "%sevenp_v3 %d ->\n" (indent i) n in
  if n = 0
  then true
  else let n' = n - 1
       in let result = traced_oddp_v3 n' (i + 1)
          in let () = Printf.printf "%sevenp_v3 %d <- %b\n" (indent i) n result
             in result
and traced_oddp_v3 n i =
  let () = Printf.printf "%sodd_v3 %d ->\n" (indent i) n in
  if n = 0
  then false
  else let n' = n - 1
       in let result = traced_evenp_v3 n' (i + 1)
          in let () = Printf.printf "%soddp_v3 %d <- %b\n" (indent i) n result
             in result;;

let traced_evenp_v4 n =
  let () = Printf.printf "evenp_v4 %d ->\n" n in
  let () = assert (0 <= n)
  in let result = traced_evenp_v3 n 1
     in let () = Printf.printf "evenp_v4 %d <- %b\n" n result
        in result;;

let traced_oddp_v4 n =
  let () = Printf.printf "oddp_v4 %d ->\n" n in
  let () = assert (0 <= n)
  in let result = traced_oddp_v3 n 1
     in let () = Printf.printf "oddp_v4 %d <- %b\n" n result
        in result;;

Specifically,

• when traced_evenp_v3 is called on a number n, it emits the trace evenp_v3 n ->,
• when traced_evenp_v3 returns a result b, it emits the trace evenp_v3 n <- b,
• when traced_oddp_v3 is called on a number n, it emits the trace oddp_v3 n ->,
• when traced_oddp_v3 returns a result b, it emits the trace oddp_v3 n <- b,
• when traced_evenp_v4 is called on a number n, it emits the trace evenp_v4 n ->,
• when traced_evenp_v4 returns a result b, it emits the trace evenp_v4 n <- b,
• when traced_oddp_v4 is called on a number n, it emits the trace oddp_v4 n ->, and
• when traced_oddp_v4 returns a result b, it emits the trace oddp_v4 n <- b.

In addition, each call is indented proportionally to its nesting.

Behold the trace of the even predicate (and of the odd predicate too):

# traced_evenp_v4 0;;
evenp_v4 0 ->
  evenp_v3 0 ->
evenp_v4 0 <- true
- : bool = true
# traced_evenp_v4 1;;
evenp_v4 1 ->
  evenp_v3 1 ->
    odd_v3 0 ->
  evenp_v3 1 <- false
evenp_v4 1 <- false
- : bool = false
# traced_evenp_v4 2;;
evenp_v4 2 ->
  evenp_v3 2 ->
    odd_v3 1 ->
      evenp_v3 0 ->
    oddp_v3 1 <- true
  evenp_v3 2 <- true
evenp_v4 2 <- true
- : bool = true
# traced_evenp_v4 3;;
evenp_v4 3 ->
  evenp_v3 3 ->
    odd_v3 2 ->
      evenp_v3 1 ->
        odd_v3 0 ->
      evenp_v3 1 <- false
    oddp_v3 2 <- false
  evenp_v3 3 <- false
evenp_v4 3 <- false
- : bool = false
#

And behold the trace of the odd predicate (and of the even predicate too):

# traced_oddp_v4 0;;
oddp_v4 0 ->
  odd_v3 0 ->
oddp_v4 0 <- false
- : bool = false
# traced_oddp_v4 1;;
oddp_v4 1 ->
  odd_v3 1 ->
    evenp_v3 0 ->
  oddp_v3 1 <- true
oddp_v4 1 <- true
- : bool = true
# traced_oddp_v4 2;;
oddp_v4 2 ->
  odd_v3 2 ->
    evenp_v3 1 ->
      odd_v3 0 ->
    evenp_v3 1 <- false
  oddp_v3 2 <- false
oddp_v4 2 <- false
- : bool = false
# traced_oddp_v4 3;;
oddp_v4 3 ->
  odd_v3 3 ->
    evenp_v3 2 ->
      odd_v3 1 ->
        evenp_v3 0 ->
      oddp_v3 1 <- true
    evenp_v3 2 <- true
  oddp_v3 3 <- true
oddp_v4 3 <- true
- : bool = true
#

A closer look at the definitions of the even and odd predicates

Let us look again at the definitions of evenp_v3 and oddp_v3:

let rec evenp_v3 n =
  if n = 0
  then true
  else let n' = n - 1
       in oddp_v3 n'
and oddp_v3 n =
  if n = 0
  then false
  else let n' = n - 1
       in evenp_v3 n';;

The last thing evenp_v3 does in its alternative branch is to call oddp_v3, and the last thing oddp_v3 does in its alternative branch is to call evenp_v3. Such calls are said to be tail calls, and recursive functions where all calls are tail calls are said to be tail recursive.

Vigfus (popping in): Hi guys! Where is the reward?

Harald: You are coming from the index, aren’t you?

Alfrothul: ‘fraid you’re on our own here.

Brynja: What a lot of owls.

A more faithful trace for the even and odd predicates

Since evenp_v3 and oddp_v3 are tail recursive, let us adjust their trace to not indent and to only trace the final result:

let rec traced_evenp_v5 n =
  let () = Printf.printf "evenp_v5 %d ->\n" n in
  if n = 0
  then true
  else let n' = n - 1
       in traced_oddp_v5 n'
and traced_oddp_v5 n =
  let () = Printf.printf "oddp_v5 %d ->\n" n in
  if n = 0
  then false
  else let n' = n - 1
       in traced_evenp_v5 n';;

let traced_evenp_v6 n =
  let () = Printf.printf "evenp_v6 %d ->\n" n in
  let () = assert (0 <= n)
  in let result = traced_evenp_v5 n
     in let () = Printf.printf "evenp_v6 %d <- %b\n" n result
        in result;;

let traced_oddp_v6 n =
  let () = Printf.printf "oddp_v6 %d ->\n" n in
  let () = assert (0 <= n)
  in let result = traced_oddp_v5 n
     in let () = Printf.printf "oddp_v6 %d <- %b\n" n result
        in result;;

Behold the flat trace of the even predicate (and of the odd predicate too):

# traced_evenp_v6 5;;
evenp_v6 5 ->
evenp_v5 5 ->
oddp_v5 4 ->
evenp_v5 3 ->
oddp_v5 2 ->
evenp_v5 1 ->
oddp_v5 0 ->
evenp_v6 5 <- false
- : bool = false
#

And behold the flat trace of the odd predicate (and of the even predicate too):

# traced_oddp_v6 5;;
oddp_v6 5 ->
oddp_v5 5 ->
evenp_v5 4 ->
oddp_v5 3 ->
evenp_v5 2 ->
oddp_v5 1 ->
evenp_v5 0 ->
oddp_v6 5 <- true
- : bool = true
#

These traces illustrate how in a functional language, iteration (i.e., looping) is provided by tail recursion: all the tail calls share one single return, namely that of the first call. In a nutshell:

• recursive functions with n calls elicit n returns, and
• tail-recursive functions with n (tail) calls elicit 1 return.

Exercise 9

Generalizing from 2 to 3, a number divisible by 3 is said to be ternary, the successor of a ternary number is said to be post-ternary, and the predecessor of a positive ternary number is said to be pre-ternary. Write predicates about whether a given non-negative integer is ternary, pre-ternary, or post-ternary, in the same fashion as for the predicates about a given non-negative integer being even or odd.

Declaring global mutually recursive functions

OCaml provides language support to declare global mutually recursive functions:

<toplevel-expression> ::= <expression>
                        | let <formal> = <definiens>
                        | let rec <formal> = fun <formal> -> <expression>
                        | let rec <formal> = fun <formal> -> <expression> {and <formal> = fun <formal> -> <expression>}*

Resources

• The OCaml code for the present lecture note (latest version: 29 Feb 2020).

Version

Fine-tuned the narrative about recursive functions (n calls and n returns) vs. tail-recursive functions (n tail calls and 1 return), witness their traces [05 Apr 2020]

Updated the resource file to solely use the unparsing functions in the traces [29 Feb 2020]

Created [20 Feb 2020]