So the computational content of mathematical induction is nat_fold_right, a generic function that embodies the programming pattern of structural recursion over natural numbers:
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 (* <-- succ_case takes one argument *)
in visit n;;
In logical circles, the associated expressive power is known as primitive iteration.
Another expressive power is known as primitive recursion, and its added expressivity is that succ_case is given not just the result of the current recursive call, but also the value to which the corresponding induction hypothesis applies (i.e., the argument to the recursive call to visit). In functional-programming circles, the corresponding fold-right function is known as a “paramorphism”, so in reference to that, here is nat_parafold_right:
let nat_parafold_right zero_case succ_case n =
(* nat_parafold_right : 'a -> (int -> '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 i' ih (* <-- succ_case takes two arguments *)
in visit n;;
The goal of this lecture note is to investigate primitive recursion, which includes programming a function that maps the index of a Factorial number (say, n) to this Factorial number (i.e., n!).
As pointed out in the postlude about nat-fold-right and before it in Exercise 01 in Week 05, applying nat_fold_right to z, s, and, say, 3 gives rise to the following nested application:
s (s (s z))
where s is applied 3 times. For example:
# nat_fold_right 0 succ 3;;
- : int = 3
# nat_fold_right 1 succ 3;;
- : int = 4
# nat_fold_right 1 (fun ih -> 10 * ih) 3;;
- : int = 1000
#
In words:
The first interaction gives rise to evaluating succ (succ (succ 0)):
# succ (succ (succ 0));;
- : int = 3
#
The second interaction gives rise to evaluating succ (succ (succ 1)):
# succ (succ (succ 1));;
- : int = 4
#
Letting times_10 denote fun ih -> 10 * ih, the third interaction gives rise to evaluating times_10 (times_10 (times_10 0)):
# (fun ih -> 10 * ih) ((fun ih -> 10 * ih) ((fun ih -> 10 * ih) 1));;
- : int = 1000
# let times_10 n = 10 * n;;
val times_10 : int -> int = <fun>
# times_10 (times_10 (times_10 1));;
- : int = 1000
#
Likewise, applying nat_parafold_right to z, s, and, say, 3 gives rise to the following nested application:
s 2 (s 1 (s 0 z))
For example:
# nat_parafold_right 1 (fun i ih -> succ i * ih) 3;;
- : int = 6
# nat_parafold_right 1 (fun i ih -> (2 * (succ i) + 1) + ih) 3;;
- : int = 16
#
In words:
Letting foo denote fun i ih -> succ i * ih, the first interaction gives rise to evaluating foo 2 (foo 1 (foo 0 1)):
# (fun i ih -> succ i * ih) 2 ((fun i ih -> succ i * ih) 1 ((fun i ih -> succ i * ih) 0 1));;
- : int = 6
# let foo i ih = succ i * ih;;
val foo : int -> int -> int = <fun>
# foo 2 (foo 1 (foo 0 1));;
- : int = 6
#
Letting bar denote fun i ih -> (2 * (succ i) + 1) + ih, the second interaction gives rise to evaluating bar 2 (bar 1 (bar 0 1)):
# (fun i ih -> (2 * (succ i) + 1) + ih) 2 ((fun i ih -> (2 * (succ i) + 1) + ih) 1 ((fun i ih -> (2 * (succ i) + 1) + ih) 0 1));;
- : int = 16
# let bar i ih = (2 * (succ i) + 1) + ih;;
val bar : int -> int -> int = <fun>
# bar 2 (bar 1 (bar 0 1));;
- : int = 16
#
Along the lines of the previous postlude, implement nat_of_digits (from Chapter Polynomials revisited) as an instance of nat_fold_right or of nat_parafold_right, your choice.
Implement a predecessor function over non-negative integers using nat_parafold_right and no numerical operations whatsoever. This predecessor function should satisfy the following unit tests:
let test_predecessor candidate =
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 0)
and b2 = (candidate 2 = 1)
and b3 = (candidate 3 = 2)
and b4 = (let n = Random.int 1000
in candidate (succ n) = n)
in b0 && b1 && b2 && b3 && b4;;
Loki suggested we change the last test to read:
and b4 = (let n = Random.int 1000
in candidate n = pred n)
Would this change be OK to test your predecessor function?
Disregarding Loki’s suggestion, suppose we adjust the first test to read:
let b0 = (candidate 0 = min_int)
Adjust your predecessor function so that it passes the adjusted unit tests.
Suppose we revise the first test to read:
let b0 = (candidate 0 = -1)
Revise your predecessor function so that it passes the revised unit tests.
Loki suggested that, in the revised unit tests, we also revise the last test to read:
and b4 = (let n = Random.int 1000
in candidate n = pred n)
Would this further revision be OK to test your revised predecessor function?
Implement a predecessor function over non-negative integers using nat_fold_right and succ. This predecessor function should satisfy the following unit tests:
let test_predecessor candidate =
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 0)
and b2 = (candidate 2 = 1)
and b3 = (candidate 3 = 2)
and b4 = (let n = Random.int 1000
in candidate (succ n) = n)
in b0 && b1 && b2 && b3 && b4;;
Note: There are at least two solutions.
As a continuation of Exercise 17 in Week 03, implement two summatorial functions: one should make as many recursive calls as the natural number it is applied to, and the other one should not even be recursive. Verify that both functions pass your unit test, and express the first using nat_parafold_right.
N.B.: You will need to start from scratch, i.e., with the inductive specification of the summatorial function.
The goal of this section is to implement the summation operator in mathematics:
sigma f n = f(0) + f(1) + f(2) + ... + f(n-1) + f(n)
For any given function f mapping integers to integers, sigma is specified inductively over its second argument as follows:
The goal of this section is to implement a generalized version of the summation operator in mathematics:
generalized_sum f i j = f(i) + f(i + 1) + f(i + 2) + ... + f(j - 1) + f(j)
Keeping in mind that 0 is the first natural number, 1 is the second natural number, and any non-negative integer n is the “n+1”th natural number, let us revisit Factorial numbers. As seen before already, e.g., in the section about the Mathematical specification of factorial numbers, they are defined inductively over their index:
In words, n! = n * (n - 1) * ... * 3 * 2 * 1 * 1.
Let us enumerate the first Factorial numbers, based on their inductive specification:
0!
= {because of the base case}
1
1!
= {because of the induction step}
1 * 0!
= {because of the equality just above}
1 * 1
=
1
2!
= {because of the induction step}
2 * 1!
= {because of the equality just above}
2 * 1
=
2
3!
= {because of the induction step}
3 * 2!
= {because of the equality just above}
3 * 2
=
6
4!
= {because of the induction step}
4 * 3!
= {because of the equality just above}
4 * 6
=
24
5!
= {because of the induction step}
5 * 4!
= {because of the equality just above}
5 * 24
=
120
Let us render this enumeration into a unit-test function:
let test_fac candidate =
(* the base case: *)
let b0 = (candidate 0 = 1)
(* some intuitive cases: *)
and b1 = (candidate 1 = 1)
and b2 = (candidate 2 = 2)
and b3 = (candidate 3 = 6)
and b4 = (candidate 4 = 24)
and b5 = (candidate 5 = 120)
(* instance of the induction step: *)
and b6 = (let n = Random.int 20
in candidate (succ n) = (succ n) * candidate n)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
Let us transliterate the inductive specification into the following skeleton of a structurally recursive function expecting non-negative integers, where visit is a traditional name but, e.g., walk, countdown, helper, fac_aux, or whichever telling name we fancy would do just as well:
let fac_v0 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;;
This implementation embodies the inductive specification above:
Concretely:
let fac_v0 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 1
else let i' = pred i
in let ih = visit i'
in (succ i') * ih
in visit n;;
let fac_v1 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 1
else let i' = pred i
in let ih = visit i'
in i * ih
in visit n;;
Both implementations are structurally recursive and they pass the unit test:
# test_fac fac_v0;;
- : bool = true
# test_fac fac_v1;;
- : bool = true
#
The first one is simple to express using nat_parafold_right:
let fac_gen n =
nat_parafold_right 1 (fun i' ih -> (succ i') * ih) n;;
This implementation passes the unit test:
# test_fac fac_gen;;
- : bool = true
#
Alfrothul: We have seen fun i ih -> (succ i) * ih before.
Harald: We did?
Alfrothul: It was named foo in the section about primitive recursion at work.
Harald: I see.
Define the factorial function using nat_fold_right.
Note: There are at least two solutions.
Mimer: Check out the interlude and then Exercise 14 in the chapter about Fibonacci numbers and consider implementing a facfac function.
Yoda: There are...
Mimer: Beg pardon?
Yoda: I say, there are...
Mimer: Yes?
Yoda: There are...
Mimer (patiently): There are?
Yoda: Thanks. At least...
Mimer: At least?
Yoda: Yes.
Mimer: Yes?
Yoda: Thanks. Trying again. Two other...
Loki (patting Yoda on the back): Does this help?
Mimer: Thanks, Loki.
Yoda: Yes, that helped, thanks. Harrumph. Wrong tube.
Loki: You are both welcome.
Yoda: So. There are at least two other solutions.
Mimer: That is correct.
Implement nat_fold_right in terms of nat_parafold_right:
let nat_fold_right_gen zero_case succ_case n =
...nat_parafold_right...
Implement nat_parafold_right in terms of nat_fold_right:
let nat_parafold_right_gen zero_case succ_case n =
...nat_fold_right...
Note: There are at least two solutions.
As pointed out in the section about primitive iteration at work and the section about primitive recursion at work, applying nat_fold_right to z, s, and, say, 3 gives rise to the following nested application:
s (s (s z))
where s is applied 3 times, whereas applying nat_parafold_right to z, s, and, say, 3 gives rise to the following nested application:
s 2 (s 1 (s 0 z))
In this nested application, s denotes a curried function. Suppose we uncurry this function. This nested application would then read:
s (2, s (1, s (0, z)))
which fits the pattern of nat_fold_right, in that applying nat_fold_right to (0, z), a suitable uncurried successor-case function, and 3 gives rise to this nested application.
Brynja: Wow.
Alfrothul: Right. Curry and uncurry, eh.
Harald: So the successor-case function is uncurried.
Alfrothul: Right.
Harald: So it is applied to a pair...
Alfrothul: ...and returns another pair, yes.
Brynja (practical): So that’s one solution.
The Practical OCaml programmer: Yes.
Brynja: But what about the other solution?
Mimer: One thing at a time.
Loki: This uncurried solution, however, does two things at a time since it operates on a pair, no?
Mimer: That is true. But the other solution doesn’t use a pair, so...
Brynja: It doesn’t use a pair?
Alfrothul: Wait. Could we use a pair to solve Exercise 09?
Harald: So nat_parafold_right and nat_fold_right only differ in their second argument.
Alfrothul: Yes. One is also passed an index, and not the other.
Harald: Kind of like String.mapi and String.map.
Alfrothul: Right. And this index is pretty useful if we want to rotate the characters to a string, circularly.
Harald: You mean as in:
let test_rotate_left_1 candidate =
let b0 = (candidate "" = "")
and b1 = (candidate "a" = "a")
and b2 = (candidate "ab" = "ba")
and b3 = (candidate "abc" = "bca")
and b5 = (candidate "abcde" = "bcdea")
in b0 && b1 && b2 && b3 && b5;;
Alfrothul: Yup. We want a string where all the characters that were at index i+1 are now at index i, except the first, which was at index 0 and now occurs last in the string. So:
let rotate_left_1a s =
let last_index = String.length s - 1
in String.mapi (fun i c ->
if i = last_index
then String.get s 0
else String.get s (i + 1))
s;;
Harald: Nice. We could factor the call to String.get s, though, look:
let rotate_left_1b s =
let last_index = String.length s - 1
in String.mapi (fun i c ->
String.get s (if i = last_index
then 0
else i + 1))
s;;
Brynja: Isn’t it a case for adding modulo the length of the string?
Harald: Uh-oh.
Alfrothul: Actually yes! Adding modulo the length of the string is just the ticket to rotate the string with one character to the left. Suppose this list has length 3:
# (0 + 1) mod 3;;
- : int = 1
# (0 + 2) mod 3;;
- : int = 2
# (0 + 3) mod 3;;
- : int = 0
#
Harald: Exercise 01 from Week 05 keeps coming back to haunt us, doesn’t it.
Brynja: Doesn’t it now:
let rotate_left_1c s =
let n = String.length s
in String.mapi (fun i c ->
String.get s ((i + 1) mod n))
s;;
Alfrothul: As for rotating a string with one character to the right, we can just subtract 1 instead of adding 1:
let test_rotate_right_1 candidate =
let b0 = (candidate "" = "")
and b1 = (candidate "a" = "a")
and b2 = (candidate "ab" = "ba")
and b3 = (candidate "abc" = "cab")
and b5 = (candidate "abcde" = "eabcd")
in b0 && b1 && b2 && b3 && b5;;
Harald: But won’t this subtraction give a negative index for 0? Let me check:
# (0 - 1) mod 3;;
- : int = -1
#
Alfrothul: Ah, we should not subtract, we should add the length of the string minus one, and due to the rounding effect of modulo, we would obtain a proper decrement.
Harald: Pray show.
Alfrothul: Of course. Say the length of the string is 4. Then adding 3 to either 0, 1, 2, or 3 will do the right thing:
# (1 + 3) mod 4;;
- : int = 0
# (2 + 3) mod 4;;
- : int = 1
# (3 + 3) mod 4;;
- : int = 2
# (0 + 3) mod 4;;
- : int = 3
#
Harald: I see – 1 is mapped to 0, 2 to 1, 3 to 2, and 0 to 3, as we wanted:
let rotate_right_1 s =
let n = String.length s
in let last_index = n - 1
in String.mapi (fun i c ->
String.get s ((i + last_index) mod n))
s;;
Vigfus: Just checking:
# test_rotate_left_1 rotate_left_1c;;
- : bool = true
# test_rotate_right_1 rotate_right_1;;
- : bool = true
#
Generalize these two rotating functions with an extra parameter (a non-negative integer) so that
In other words, the extra parameter specifies the number of characters the string should be rotated with.
As a generalization of Exercise 12, implement a rotating function such that applying it to a string and an integer rotates this string to the right if the integer is positive and to the left if the integer is negative.
Adjusted some names [19 Mar 2022]
Renamed sum to be sigma in Exercise 07 and simplified Exercise 07.f [11 Mar 2022]
Moved Exercise 03 from the previous chapter, thanks to Cathy Choo [04 Mar 2022]
Used last_index in the definition of rotate_right_1, for naming consistency [26 Feb 2022]
Created [19 Feb 2022]