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.
The corresponding typing rule reads as follows, where G and G' stand for <type_environment>, f1, x1, ..., fN, and xN stand for <formal>, e0, e1, ... and eN stand for <expression>, and t0, t1, t1', ..., tN, and tN' stand for <type>:
| REC | G' |- fun x1 -> e1 : t1 -> t1' | ... | G' |- fun xN -> eN : tN -> tN' | G' |- e0 : t0 | where G' = (f1 : t1 -> t1'), ..., (fN : tN -> tN'), G |
| 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',
...
Note: f1, ..., and fN must be distinct from each other.
Furthermore,
to evaluate let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0,
we first evaluate the definienses, i.e., fun x1 -> e1, ..., and fun xN -> eN, in an extension of the current environment where f1 denotes the result of evaluating fun x1 -> e1, ..., and fN denotes the result of evaluating fun xN -> eN in this extended environment; it is this self-reference that enables the recursive definitions of f1, ..., and fN;
evaluating let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0 then reduces to evaluating e0 in this extended environment;
the binding of f1, ..., and fN are local: they vanish once e0 is evaluated.
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)
(* a random instance of the induction step: *)
and is = (let i' = Random.int 1000
in candidate (succ i') = not (candidate i'))
(* 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)
(* a random 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:
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)
(* random instances of the induction steps: *)
and b2 = (let i' = Random.int 1000
in evenp (succ i') = oddp i')
and b3 = (let i' = Random.int 1000
in oddp (succ i') = evenp i')
(* 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 i =
if i = 0
then true
else let i' = pred i
in oddp_v3 i'
and oddp_v3 i =
if i = 0
then false
else let i' = pred i
in evenp_v3 i';;
The two functions evenp_v3 and oddp_v3 call each other. They are mutually recursive, i.e., indirectly self-referential, like the last sentences of Exercise 21 – self-referential sentences and like Exercise 27 – multiple-choice questions in Week 01, 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 (n >= 0) in
evenp_v3 n;;
let oddp_v4 n =
let () = assert (n >= 0) 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 indentation =
let () = Printf.printf "%sevenp_v3 %d ->\n" (indent indentation) n in
if n = 0
then true
else let n' = pred n
in let result = traced_oddp_v3 n' (indentation + 1)
in let () = Printf.printf "%sevenp_v3 %d <- %b\n" (indent indentation) n result in
result
and traced_oddp_v3 n indentation =
let () = Printf.printf "%sodd_v3 %d ->\n" (indent indentation) n in
if n = 0
then false
else let n' = pred n
in let result = traced_evenp_v3 n' (indentation + 1)
in let () = Printf.printf "%soddp_v3 %d <- %b\n" (indent indentation) n result in
result;;
let traced_evenp_v4 n =
let () = Printf.printf "evenp_v4 %d ->\n" n in
let () = assert (n >= 0) 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 (n >= 0) in
let result = traced_oddp_v3 n 1
in let () = Printf.printf "oddp_v4 %d <- %b\n" n result in
result;;
Specifically,
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
#
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' = pred n
in oddp_v3 n'
and oddp_v3 n =
if n = 0
then false
else let n' = pred n
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.
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' = pred n
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' = pred n
in traced_evenp_v5 n';;
let traced_evenp_v6 n =
let () = Printf.printf "evenp_v6 %d ->\n" n in
let () = assert (n >= 0) 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 (n >= 0) 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:
Generalizing from 2 to 3, a non-negative integer 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. The goal of this exercise is to implement 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. To this end:
If you feel inspired to trace your implementations, do so as in the section about A more faithful trace for the even and odd predicates, just above.
OCaml provides language support to declare global mutually recursive functions:
Stated that the instances of the induction step is random in test_evenp, test_oddp, and test_evenp_and_oddp [04 Mar 2023]
Quantified the variables in the type-inference rules [23 Jan 2023]
Created [16 Sep 2022]