Generic programming with natural numbers

The goal of this lecture note is to explore the pattern of structural recursion associated to natural numbers.

Resources

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

The big picture

Overall, for a variety of examples (twice, add, mul, power, evenp, oddp), we have specified a computation by mathematical induction, and then we have implemented the corresponding function in OCaml by structural recursion. In each case, we started from the following skeleton:

let ... n_given =
  let () = assert (n_given >= 0) in
  let rec visit n =
    if n = 0
    then ...
    else let n' = n - 1
         in let ih = visit n'
            in ...
  in visit n_given;;

We then proceeded by

• naming the OCaml function,
• implementing the base case, and
• implementing the induction step.

Let us abstract this skeleton into an OCaml function, traditionally called “fold_right” (down the road, we will meet its cousin “fold_left”) and pre-indexed with the name “nat” (the name of the type of natural numbers, i.e., non-negative integers here):

let nat_fold_right zero_case succ_case n_given =
 (* nat_fold_right : 'a -> ('a -> 'a) -> int -> 'a *)
  let () = assert (n_given >= 0) in
  let rec visit n =
    if n = 0
    then zero_case
    else let n' = n - 1
         in let ih = visit n'
            in succ_case ih
  in visit n_given;;

(Incidentally, in the induction step, the let-expressions that declare n' and ih, in the definition of visit, are cosmetic and so we could unfold them.)

Doubling up a natural number, revisited

The inductive specification of twice read as follows:

• base case: doubling up 0 yields 0
• induction step: given a number n' such that doubling it yields ih (which is the induction hypothesis), doubling succ n' should yield succ (succ ih)

This specification suggests that we could implement twice as an instance of nat_fold_right:

let twice_v4 n =
  nat_fold_right 0 (fun ih -> succ (succ ih)) n;;

This implementation passes the unit test:

# test_twice twice_v4;;
- : bool = true
#

Express interlude

Harald: This definition can be simplified.

Alfrothul: Indeed it can:

let twice_v5 =
  nat_fold_right 0 (fun ih -> succ (succ ih));;

Harald: And it passes the unit test too:

# test_twice twice_v5;;
- : bool = true
#

Adding a natural number to an integer, revisited

The inductive specification of add read as follows, given an integer y:

• base case: adding 0 to y yields y
• induction step: given a number x' such that adding it to y yields ih (which is the induction hypothesis), adding succ x' to y should yield succ ih

This specification suggests that we could implement add as an instance of nat_fold_right:

let add_v3 x y =
  nat_fold_right y (fun ih -> succ ih) x;;

This implementation passes the unit test:

# test_add add_v3;;
- : bool = true
#

Express interlude

Vigfus: Hehe, even shorter:

let add_v4 x y =
  nat_fold_right y succ x;;

Halcyon: And it passes the unit test too:

# test_add add_v4;;
- : bool = true
#

Harald: We however can’t simplify it, since x is not the last formal parameter.

Alfrothul: Well, it could be. The addition function is commutative, right?

Vigfus: I guess it is:

let add_v5 z =
  nat_fold_right z succ;;

Harald: Harrumph.

Multiplying a natural number with an integer, revisited

The inductive specification of mul read as follows, given an integer y:

• base case: multiplying 0 and y yields 0
• induction step: given a number x' such that multiplying it to y yields ih (which is the induction hypothesis), multiplying succ x' and y should yield y + ih (or again add_v4 y ih, should the + key still be inoperative)

This specification suggests that we could implement mul as an instance of nat_fold_right:

let mul_v5 x y =
  nat_fold_right 0 (fun ih -> y + ih) x;;

This implementation passes the unit test:

# test_mul mul_v5;;
- : bool = true
#

Exponentiating two integers, revisited

The inductive specification of exponentiation read as follows, given an integer x:

• base case: exponentiating x with 0 yields 1
• induction step: given a number n’ such that exponentiating x with n’ yields ih (which is the induction hypothesis), exponentiating x with succ n' should yield x * ih (or again mul_v5 x ih, should the * key still be inoperative)

Exercise 1

Along the lines of the previous sections, implement the exponentiation function as an instance of nat_fold_right.

The even predicate, revisited

The inductive specification of how to test whether a natural number is even read as follows:

• base case: 0 is even
• induction step: given a number n' such that its evenness is the Boolean ih (which is the induction hypothesis), the evenness of succ n' is not ih

This specification suggests that we could implement evenp as an instance of nat_fold_right:

let evenp_v2 n =
  nat_fold_right true (fun ih -> not ih) n;;

This implementation passes the unit test:

# test_evenp evenp_v2;;
- : bool = true
#

Express interlude

Halcyon: Hehe, even shorter:

let evenp_v3 n =
  nat_fold_right true not n;;

Vigfus: Simpler too:

let evenp_v4 =
  nat_fold_right true not;;

The odd predicate, revisited

The goal of this section is to write a predicate computing whether a given natural number is odd.

Exercise 2

Along the lines of the previous section, implement the oddp predicate as an instance of nat_fold_right.

Resources

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

Version

Fixed a typo in the section revisiting the exponentiation of two integers, thanks to Chiau Ren Yu’s eagle eye [20 Feb 2021]

Created [20 Feb 2021]