The goal of this lecture note is to explore the pattern of structural recursion associated with natural numbers.
Overall, for a variety of examples (twice, add, mul, power, evenp, oddp, nat-of-digits), 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 =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then ...
else let i' = pred i
in let ih = visit i'
in ...
in visit n;;
We then proceeded by
Let us abstract this skeleton into an OCaml function, traditionally called “fold_right” (down the road, we will meet its cousin “fold_left”) and prefixed 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 =
(* nat_fold_right : 'a -> ('a -> 'a) -> int -> 'a *)
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then zero_case
else let i' = pred i
in let ih = visit i'
in succ_case ih
in visit n;;
(Incidentally, in the induction step, the let-expressions that declare i' and ih, in the definition of visit, are cosmetic and so we could unfold them.)
As an abstraction of a skeleton, nat_fold_right is said to be a “generic” function.
The inductive specification of twice reads as follows:
This specification suggests that we could implement twice as an instance of nat_fold_right:
let twice_gen n =
nat_fold_right 0 (fun ih -> succ (succ ih)) n;;
This generic implementation passes the unit test:
# test_twice twice_gen;;
- : bool = true
#
Harald: This definition can be simplified.
Alfrothul: Indeed it can:
let twice_gen' =
nat_fold_right 0 (fun ih -> succ (succ ih));;
Harald: And it passes the unit test too:
# test_twice twice_gen';;
- : bool = true
#
The inductive specification of add reads as follows, given an integer y:
This specification suggests that we could implement add as an instance of nat_fold_right:
let add_gen x y =
nat_fold_right y (fun ih -> succ ih) x;;
This generic implementation passes the unit test:
# test_add add_gen;;
- : bool = true
#
Vigfus: Hehe, even shorter:
let add_gen' x y =
nat_fold_right y succ x;;
Halcyon: And it passes the unit test too:
# test_add add_gen';;
- : 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_gen'' z =
nat_fold_right z succ;;
Harald: Harrumph.
The inductive specification of mul reads as follows, given an integer y:
This specification suggests that we could implement mul as an instance of nat_fold_right:
let mul_gen x y =
nat_fold_right 0 (fun ih -> y + ih) x;;
This generic implementation passes the unit test:
# test_mul mul_gen;;
- : bool = true
#
Vigfus: Hehe, even shorter:
let mul_gen' x y =
nat_fold_right 0 ((+) y) x;;
Halcyon: And it passes the unit test too:
# test_mul mul_gen';;
- : bool = true
#
Vigfus: Or equivalently:
let mul_gen'' x y =
nat_fold_right 0 (Int.add y) x;;
The inductive specification of exponentiation read as follows, given an integer x:
Along the lines of the previous sections, implement the exponentiation function as an instance of nat_fold_right.
The inductive specification of how to test whether a natural number is even read as follows:
This specification suggests that we could implement evenp as an instance of nat_fold_right:
let evenp_gen n =
nat_fold_right true (fun ih -> not ih) n;;
This implementation passes the unit test:
# test_evenp evenp_gen;;
- : bool = true
#
Halcyon: Hehe, even shorter:
let evenp_gen' n =
nat_fold_right true not n;;
Vigfus: Simpler too:
let evenp_gen'' =
nat_fold_right true not;;
The goal of this section is to write a predicate computing whether a given natural number is odd.
Along the lines of the previous section, implement the oddp predicate as an instance of nat_fold_right.
Alfrothul: Wow.
Harald: Wow?
Alfrothul: Exercise 01, in Week 05, was really prescient.
Harald: Prescient?
Alfrothul: Well, yes. Look at Question f.:
Harald: Yes?
Alfrothul: We can express this question as an OCaml function:
let week_05_exercise_1f n =
let () = assert (n >= 0) in
nat_fold_right 1 (fun i -> 1 + i) n;;
Harald: True that. Given a non-negative integer n, this function adds 1 to the left n times, starting with 1.
Vigfus: Hehe, even shorter:
let week_05_exercise_1f n =
let () = assert (n >= 0) in
nat_fold_right 1 succ n;;
Alfrothul: Indeed. Though if you want shorter, here is shorter:
let week_05_exercise_1f n =
nat_fold_right 1 succ n;;
There is always a bigger fish.
Vigfus: Come again?
Harald: Well, nat_fold_right checks whether its last argument is non-negative.
Vigfus: Harrumph.
Alfrothul: At any rate, we can now use OCaml to answer the question:
# week_05_exercise_1f 3;;
- : int = 4
# week_05_exercise_1f 10;;
- : int = 11
#
Alfrothul: Right. We get an implementation of the successor function.
Harald: So nat_fold_right really implements an iterator for natural numbers.
Vigfus: Let me check, let me check.
Alfrothul: By all means.
Vigfus: So, Question h.:
Vigfus: Lemmesee:
let week_05_exercise_1h n =
nat_fold_right 0 (fun i -> 2 + i) n;;
Harald: OK.
Vigfus: Testing, testing:
# test_twice week_05_exercise_1h;;
- : bool = true
#
Vigfus: So the definition of week_05_exercise_1h and the definition of twice_v4 in the section about doubling up a natural number, revisited are the same.
Mimer: Yes. Given a zero case zero_specific, a successor case succ_specific, and, e.g., the non-negative integer 3, i.e., the result of evaluating:
succ (succ (succ 0))
nat_fold_right essentially yields the result of evaluating:
succ_specific (succ_specific (succ_specific zero_specific))
In words, given a non-negative integer n represented as n, evaluating nat_fold_right zero_specific succ_specific n recursively gives rise to n nested applications of succ_specific that mimic the n nested occurrences of succ that constructed n.
Verify that the algorithms in Exercise 01.1.g, Exercise 01.1.i, Exercise 01.1.j, and Exercise 01.1.k in Week 05, are the same as the definitions of add_v4 in the section about adding a natural number to an integer, revisited, mul_v6 in the section about multiplying a natural number with an integer, revisited, and Exercise 01, respectively.
Aligned the essential description of nat_fold_right [14 Apr 2022]
Expanded the narrative and added index entries [29 Mar 2022]
Adjusted more names [19 Mar 2022]
Adjusted names [11 Mar 2022]
Moved Exercise 03 to the next chapter, thanks to Cathy Choo [04 Mar 2022]
Created [19 Feb 2022]