So the computational content of mathematical induction is nat_fold_right, a generic function that abstracts 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 another generic function, 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;;
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_parafold_right essentially yields the result of evaluating:
succ_specific 2 (succ_specific 1 (succ_specific 0 zero_specific))
In words, given a non-negative integer n represented as n, evaluating nat_parafold_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, and each of the calls to succ_specific is also passed a decreasing index.
The type of nat_parafold_right is 'a -> (int -> 'a -> 'a) -> int -> 'a:
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!).
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))
where s is also applied 3 times. 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
# nat_parafold_right 0 (fun i ih -> 10 + ih) 3;;
- : int = 30
#
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
#
Letting baz denote fun i ih -> 10 + ih, the third interaction gives rise to evaluating baz 2 (baz 1 (baz 0 0)):
# (fun i ih -> 10 + ih) 2 ((fun i ih -> 10 + ih) 1 ((fun i ih -> 10 + ih) 0 0));;
- : int = 30
# let baz i ih = 10 + ih;;
val baz : 'a -> int -> int = <fun>
# baz 2 (baz 1 (baz 0 0));;
- : int = 30
#
Implement nat_fold_right as an instance of nat_parafold_right:
let nat_fold_right_gen zero_case succ_case n =
...nat_parafold_right...
Implement string_minchar (from Exercise 01 earlier this week) as an instance of nat_parafold_right.
Pablito: Here is the unit-test function we used to solve Exercise 01:
let test_string_minchar candidate =
let b0 = (candidate "0" = '0')
and b1 = (candidate "01" = '0')
and b2 = (candidate "10" = '0')
and b3 = (candidate "012" = '0')
and b4 = (candidate "102" = '0')
and b5 = (candidate "120" = '0')
in b0 && b1 && b2 && b3 && b4 && b5;;
Dana: Thanks, Pablito.
Bong-sun: May I give it a shot?
Dana: Of course.
Bong-sun: In Exercise 01, the solution was:
let string_minchar_v1 s =
let n = String.length s
in let () = assert (n > 0) in
let rec visit i =
if i = 0
then '\255'
else let i' = pred i
in let ih = visit i'
in min (String.get s i') ih
in visit n;;
Pablito: Right.
Bong-sun: So... In the base case, the result is '\255'.
Pablito: Correct.
Bong-sun: And in the induction step, evaluating the let-expression that declares ih reduces to evaluating min (String.get s i') ih.
Pablito: Yes.
Bong-sun: Well, that’s pretty much it then:
let string_minchar_v2 s =
let n = String.length s
in let () = assert (n > 0) in
nat_parafold_right
'\255'
(fun i' ih ->
min (String.get s i') ih)
n;;
Bong-sun: Isn’t it?
Pablito: Let me check:
# test_string_minchar string_minchar_v1;;
- : bool = true
#
Pablito: Yup.
Bong-sun: Hmm... Are you sure about that??
Pablito: Oops:
# test_string_minchar string_minchar_v2;;
- : bool = true
#
Bong-sun: Yup.
Dana: Thanks, guys.
Implement string_maxchar (from Exercise 02 earlier this week) as an instance of nat_parafold_right.
Implement string_minmaxchar (from Exercise 03 earlier this week) as an instance of nat_parafold_right.
Along the lines of the solution for Exercise 09, implement nat_of_digits (from Chapter Polynomials revisited) as an instance of nat_parafold_right.
Implement a predecessor function over non-negative integers as an instance of nat_parafold_right, using 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 as an instance of nat_fold_right and using 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 18 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 as an instance of 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 following sum function:
sum f n = f(0) + f(1) + f(2) + ... + f(n-1)
In words: applying sum to a function f and to a non-negative integer n yields the sum of applying f to the n first natural numbers.
For any given function f (denoted by f) mapping integers to integers, sum is specified inductively over its second argument as follows:
base case (i = 0): sum f 0 = 0, since 0 is the neutral element for addition
induction step (i = succ i’): given a number i’ (denoted by i') such that sum f i' yields the sum of applying f to the first i’ natural numbers, which is the induction hypothesis, adding sum f i' and f i' should yield the sum of applying f to the first i natural numbers, i.e., sum f (succ i'):
sum f (succ i') = sum f i' + f i'
So, refining the initial characterization above, we get the following inductive specification:
sum f 0 = 0
sum f (n + 1) = 0 + f(0) + f(1) + f(2) + ... + f(n) = sum f n + f n
where n denotes a non-negative integer.
This exercise is about the sum function specified just above:
sum f 0 = 0
sum f (n + 1) = 0 + f(0) + f(1) + f(2) + ... + f(n)
where f denotes a function of type int -> int and n denotes a non-negative integer.
The goal of this section is to implement the summation operator in mathematics:
capital_sigma f j k = f(j) + f(j + 1) + ... + f(k - 1) + f(k)
where f denotes a function of type int -> int and where j denotes an integer and k denotes a larger integer. (If the integer denoted by j is strictly larger than the integer denoted by k, the summation is either undefined or it is 0, one’s choice.)
Implement two OCaml functions of type string -> int that, given a string of digits, return the sum of these digits. So for example, applying either of these functions to "23" should yield 5.
The first implementation should be structurally recursive, and the second should not be recursive.
Implement an OCaml function of type string -> char that, given a string of 9 characters containing distinct digits in any order, returns the missing digit. So for example, applying this function to "123456789" or to "987654321" should yield '0'.
For simplicity, and beyond checking that the given string contains 9 characters, there is no need to test whether it is conformant, i.e., that it contains distinct digits.
Mutatis mutandis, the goal of this section is to implement the following product function:
product f n = f(0) * f(1) * f(2) * ... * f(n-1)
Specify product inductively, in the manner of the section about the sum function.
This exercise is about the product function specified in Exercise 20.
The goal of this section is to implement the product operator in mathematics:
capital_pi f j k = f(j) * f(j * 1) * ... * f(k - 1) * f(k)
where f denotes a function of type int -> int and where j denotes an integer and k denotes a larger integer. (If the integer denoted by j is strictly larger than the integer denoted by k, the summation is either undefined or it is 0, one’s choice.)
Implement two OCaml functions of type string -> int that, given a string of digits, return the product of these digits. So for example, applying either of these functions to "23" should yield 5.
The first implementation should be structurally recursive, and the second should not be recursive.
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, 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)
(* random 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 as an instance of 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.
Anton: We did?
Alfrothul: It was named foo in the section about primitive recursion at work.
Anton: I see.
Implement the factorial function as an instance of nat_fold_right.
Hint: Check out the interlude and then Exercise 31 in the chapter about Fibonacci numbers and consider implementing a facfac function.
Note: There are at least two other solutions.
Implement nat_parafold_right as an instance 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.
Dana: Wow.
Alfrothul: Right. Curry and uncurry, eh.
Anton: So the successor-case function is uncurried.
Alfrothul: Right.
Anton: So it is applied to a pair...
Alfrothul: ...and returns another pair, yes.
Dana (practical): So that’s one solution.
The Practical OCaml programmer: Yes.
Dana: 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...
Dana: It doesn’t use a pair?
Alfrothul: Wait. Could we use a pair to solve Exercise 25?
Anton: 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.
Anton: 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.
Anton: 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;;
Anton: 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;;
Dana: Isn’t it a case for adding modulo the length of the string?
Anton: 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
#
Anton: Exercise 01 from Week 05 keeps coming back to haunt us, doesn’t it.
Dana: 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;;
Anton: 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.
Anton: 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
#
Anton: 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;;
Pablito: 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 27, 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.
The goal of this exercise is to understand each of the following four OCaml functions:
let pf0 n =
nat_parafold_right 1 (fun i' ih -> i' * ih) n;;
let pf1 n =
nat_parafold_right 1 (fun i' ih -> (n - i') * ih) n;;
let pf2 s =
nat_parafold_right
0
(fun i' ih ->
nat_of_digit (String.get s i') * power 10 i' + ih)
(String.length s);;
let pf3 s =
let n = String.length s
in let last_index = n - 1
in nat_parafold_right
0
(fun i' ih ->
nat_of_digit (String.get s (last_index - i')) * power 10 i' + ih)
n;;
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 pf0_rec n =
...
let pf1_rec n =
...
let pf2_rec n =
...
let pf3_rec n =
...
Made it clearer in Exercise 19 that the digits in the given string can occur in any order [12 Mar 2023]
Stated that the instance of the induction step is random in test_fac [04 Mar 2023]
Created Exercise 29 [18 Feb 2023]
Adjusted the narrative of the solution for Exercise 09 [18 Feb 2023]
Added the accompanying .ml file after the live-coding session in class [17 Feb 2023]
Added Exercise 09 and its solution [17 Feb 2023]
Added a section about the product function and a bunch of exercises [17 Feb 2023]
Created [10 Jan 2023]