So the computational content of mathematical induction is fold_right_nat, a generic function that embodies the programming pattern of structural recursion over natural numbers:
let fold_right_nat zero_case succ_case n_given =
(* fold_right_nat : '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 (* <-- succ_case takes one argument *)
in visit n_given;;
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 parafold_right_nat:
let parafold_right_nat zero_case succ_case n_given =
(* parafold_right_nat : 'a -> (int -> '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 n' ih (* <-- succ_case takes two arguments *)
in visit n_given;;
The goal of this lecture note is to investigate primitive recursion, starting with programming a function that maps the index of a Factorial number (say, n) to this Factorial number (i.e., n!).
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_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then ...
else let n' = pred n
in let ih = visit n'
in ...
in visit n_given;;
This implementation embodies the inductive specification above:
Concretely:
let fac_v0 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 1
else let n' = pred n
in let ih = visit n'
in (succ n') * ih
in visit n_given;;
let fac_v1 n_given =
let () = assert (n_given >= n_given) in
let rec visit n =
if n = 0
then 1
else let n' = pred n
in let ih = visit n'
in n * ih
in visit n_given;;
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 parafold_right_nat:
let fac_v2 n_given =
let () = assert (n_given >= 0) in
parafold_right_nat 1 (fun n' ih -> (succ n') * ih) n_given;;
This implementation passes the unit test:
# test_fac fac_v2;;
- : bool = true
#
Define the factorial function using fold_right_nat.
As a continuation of Exercise 14 in Week 03, implement two sumtorial 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 parafold_right_nat.
N.B.: You will need to start from scratch, i.e., with the inductive specification of the sumtorial function. (Hint: mimic the specification of the factorial function.)
The goal of this section is to implement the summation operator in mathematics:
sum f n = f(0) + f(1) + f(2) + ... + f(n-1) + f(n)
For any given function f mapping integers to integers, sum is specified inductively as follows:
Compose a unit-test function for sum, based on its inductive specification.
Implement this specification as a structurally recursive function expecting a function from int to int and a non-negative integer.
Verify that this function passes your unit test.
Express your implementation using either fold_right_nat or parafold_right_nat, your choice. Justify this choice, and verify that your new implementation passes your unit test.
Revisit the sumtorial function and express it using sum.
Revisit Exercise 15 in Week 03 and implement three OCaml functions that given a non-negative integer n, compute the sum of the n+1 first odd numbers. The first should be structurally recursive. The second should use either fold_right_nat or parafold_right_nat, your choice. And the third should operate in constant time.
Observing that for any non-negative integer n,
1 + F_0 + F_1 + F_2 + ... + F_n = F_(n+2)
(where F_0, F_1, F_2, etc. are Fibonacci numbers) verify that this identity holds and beef up your unit-test function for sum with it.
Define fold_right_nat in terms of parafold_right_nat:
let fold_right_nat zero_case succ_case n =
...parafold_right_nat...
Define parafold_right_nat in terms of fold_right_nat:
let parafold_right_nat zero_case succ_case n =
...fold_right_nat...
Harald: So parafold_right_nat and fold_right_nat 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 0 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 n' = n - 1
in String.mapi (fun i c ->
String.get s ((i + n') 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 7, 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.
Fixed a typo, thanks to Syed Muhammad Maaz’s eagle eye [14 Mar 2020]
Added the postlude, Exercise 7, and Exercise 8 [22 Feb 2020]
Adapted [21 Feb 2020]
Streamlined the unit-test functions [08 Jun 2019]
Created [23 Feb 2019]