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_given =
(* nat_fold_right : '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 nat_parafold_right:
let nat_parafold_right zero_case succ_case n_given =
(* nat_parafold_right : '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 >= 0) 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 nat_parafold_right:
let fac_v2 n_given =
let () = assert (n_given >= 0) in
nat_parafold_right 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 nat_fold_right.
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 nat_parafold_right.
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:
Implement nat_fold_right in terms of nat_parafold_right:
let nat_fold_right zero_case succ_case n =
...nat_parafold_right...
Implement nat_parafold_right in terms of nat_fold_right:
let nat_parafold_right zero_case succ_case n =
...nat_fold_right...
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 1 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 8, 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 in the definition of fac_v1, thanks to Aiman Imtiaz’s eagle eye [02 Apr 2021]
Split an exercise into 2 [21 Feb 2021]
Created [20 Feb 2021]