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 a polymorphic OCaml function, traditionally named “fold_right” (down the road, we will meet its cousin “fold_left”) and prefixed with “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.)
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.
The type of nat_fold_right is 'a -> ('a -> 'a) -> int -> 'a:
As a function that, given z, s, and n, preserves the structure of its non-negative input (i.e., succ (succ (... (succ 0)...)), n times) into the structure of its output (i.e., s (s (... (s z)...)), n times), nat_fold_right implements a homomorphism.
As an abstraction of a skeleton, nat_fold_right is said to be a “generic” function and programming with fold functions is said to be “generic”.
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
#
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
#
Pablito: 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
#
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
#
Pablito: 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
#
Pablito: 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
#
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.
Along the lines of the previous section, implement make_parity_predicate (from the Post-post-postlude in the chapter about Functional abstraction and instantiations) as an instance of nat_fold_right.
Alfrothul: Wow.
Anton: Wow?
Alfrothul: Exercise 01, in Week 05, was really prescient.
Anton: Prescient?
Alfrothul: Well, yes. Look at Question f.:
Anton: 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;;
Anton: True that. Given a non-negative integer n, this function adds 1 to the left n times, starting with 1.
Pablito: 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.
Pablito: Come again?
Anton: Well, nat_fold_right checks whether its last argument is non-negative.
Pablito: 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.
Anton: So nat_fold_right really implements an iterator for natural numbers.
Pablito: Let me check, let me check.
Alfrothul: By all means.
Pablito: So, Question h.:
Pablito: Lemmesee:
let week_05_exercise_1h n =
nat_fold_right 0 (fun i -> 2 + i) n;;
Anton: So doubling is iterating the addition of 2, starting with 0.
Pablito: Testing, testing:
# test_twice week_05_exercise_1h;;
- : bool = true
#
Pablito: 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.
The goal of this exercise is to understand each of the following four OCaml functions:
let f0 n =
nat_fold_right 0 (fun ih -> 10 * ih) n;;
let f1 n =
nat_fold_right 0 (fun ih -> ih + 10) n;;
let f2 n =
nat_fold_right 1 (fun ih -> 2 * ih) n;;
let f3 n =
let (b0, _, _) = nat_fold_right
(true, false, false)
(fun (b0, b1, b2) ->
(b1, b2, b0))
n
in b0;;
Analyzing the text of these definitions, try to venture a guess about what each of these OCaml functions compute.
Use the scientific method:
Your answers should be concretized as unit-test functions.
Implement four structurally recursive functions that are equivalent to the four OCaml functions above:
let f0_rec n =
...
let f1_rec n =
...
let f2_rec n =
...
let f3_rec n =
...
Fleshed out Exercise 07 some more and aligned it with Exercise 29 [18 Feb 2023]
Killed a minor darling, to celebrate Valentine’s day [14 Feb 2023]
Created [10 Jan 2023]