The goal of this lecture note is to tackle the summatorial function (Exercise 15), the sum function (Exercise 16), and the summation operator (Exercise 17) in Week 06.
Anton: Well, the summatorial function is a piece of cake. It is the additive counterpart of the factorial function:
let test_summatorial candidate =
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 0 + 1)
and b2 = (candidate 2 = 0 + 1 + 2)
and b3 = (candidate 3 = 0 + 1 + 2 + 3)
in b0 && b1 && b2 && b3;;
Alfrothul: Right. And also: nice vertical alignment, Anton. While we are at it, we might as well single out the base case in this unit-test function and add a random instance of the induction step:
let test_summatorial candidate =
let bc = (candidate 0 = 0) (* base case *)
and b1 = (candidate 1 = 0 + 1)
and b2 = (candidate 2 = 0 + 1 + 2)
and b3 = (candidate 3 = 0 + 1 + 2 + 3)
and is = (let i' = Random.int 10 (* random instance of the induction step *)
in candidate (succ i') = candidate i' + succ i')
in bc && b1 && b2 && b3 && is;;
Pablito: For the record, let’s test it using Gauss’s formula:
# test_summatorial (fun n -> n * (n + 1) / 2);;
- : bool = true
#
Anton: Thanks, Pablito. And now that the base case and the induction steps are spelled out, the recursive implementation pretty much writes itself:
let summatorial_rec n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in succ i' + ih
in visit n;;
Pablito: Checking:
# test_summatorial summatorial_rec;;
- : bool = true
#
Alfrothul: And since this implementation is structurally recursive and uses the induction variable, let’s go with nat_parafold_right:
let summatorial_right n =
nat_parafold_right
0
(fun i' ih ->
succ i' + ih)
n;;
Pablito: Checking:
# test_summatorial summatorial_right;;
- : bool = true
#
Bong-sun (in thoughts): The additive counterpart of the factorial function, Anton said. Let’s see:
let test_factorial candidate =
let bc = (candidate 0 = 1) (* base case *)
and is = (let i' = Random.int 10 (* random instance of the induction step *)
in candidate (succ i') = succ i' * candidate i')
in bc && is;;
Pablito: Right. We might as well add a couple more tests:
let test_factorial candidate =
let bc = (candidate 0 = 1) (* base case *)
and b1 = (candidate 1 = 1 * 1)
and b2 = (candidate 2 = 2 * 1 * 1)
and b3 = (candidate 3 = 3 * 2 * 1 * 1)
and is = (let i' = Random.int 10 (* random instance of the induction step *)
in candidate (succ i') = succ i' * candidate i')
in bc && b1 && b2 && b3 && is;;
Bong-sun: Thanks, Pablito. And nice vertical alignment too. Now for testing this unit-test function...
Pablito: How about using the multiplicative analogue of Gauss’s formula?
Bong-sun: The multiplicative analogue of Gauss’s formula?
Pablito: Well, you know, with a vertical alignment:
2 * summatorial 3
= 0 + 1 + 2 + 3 +
3 + 2 + 1 + 0
= 3 + 3 + 3 + 3
= 4 * 3
Bong-sun: Let’s see:
3 * 2 * 1 * 1 *
1 * 1 * 2 * 3
Pablito: Exactly:
4 * 3 * 2 * 1 * 1 *
1 * 1 * 2 * 3 * 4
Bong-sun: Hum, I’m not seeing this. Maybe with a logarithm?
Pablito: ...
Bong-sun: ...
Loki: Nice try, but no cigar.
Pablito (not discouraged): It was worth a try.
Mimer: It was.
Bong-sun: Anyhow, moving on with a recursive definition that is the multiplicative analogue of summatorial_rec:
let factorial_rec 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;;
Pablito: Checking:
# test_factorial factorial_rec;;
- : bool = true
#
Bong-sun: And since this implementation is structurally recursive and uses the induction variable, we also go with nat_parafold_right:
let factorial_right n =
nat_parafold_right
1
(fun i' ih ->
succ i' * ih)
n;;
Pablito: Checking:
# test_factorial factorial_right;;
- : bool = true
#
Bong-sun: So yes, the multiplicative counterpart of the summatorial function. Thanks, Anton.
Anton: You’re welcome. Now one thing I have never been happy with, Exercise 01 of Week 05 notwithstanding, is this occurrence of succ in the definition of summatorial_rec. Also, this business about 0 being a natural number has never sat right with me. Here is a definition that makes sense to me:
let summatorial_rec_that_makes_sense n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in i' + ih
in visit (n + 1);;
Loki: Way to go, Anton!
Pablito (prudently): Checking:
# test_summatorial summatorial_rec_that_makes_sense;;
- : bool = true
#
Anton: See? Initially, visit is applied to n + 1 since it will add the n first natural numbers. We just add 1 to account for 0, since 0 is not a natural number. The definition is still structurally recursive, look:
let summatorial_right_that_makes_sense n =
nat_parafold_right
0
(fun i' ih ->
i' + ih)
(n + 1);;
Pablito: Checking:
# test_summatorial summatorial_right_that_makes_sense;;
- : bool = true
#
Bong-sun (reflectively): The argument should work for the factorial function, then?
Anton: It should, since it’s the right thing.
Bong-sun: Let’s see:
let factorial_right_that_makes_sense n =
nat_parafold_right
1
(fun i' ih ->
i' * ih)
(n + 1);;
Bong-sun: OK?
Anton: OK.
Pablito: Checking:
# test_factorial factorial_right_that_makes_sense;;
- : bool = false
#
Anton: Harrumph. Just a sec:
let factorial_rec_that_makes_sense 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 + 1);;
Pablito: Checking:
# test_factorial factorial_rec_that_makes_sense;;
- : bool = false
#
Anton: Wait. <clickety clickety clickety click>:
# traced_factorial_rec_that_makes_sense 5;;
factorial_rec_that_makes_sense 5 ->
visit 6 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 1
visit 1 <- 0
visit 2 <- 0
visit 3 <- 0
visit 4 <- 0
visit 5 <- 0
visit 6 <- 0
- : int = 0
#
Anton: Harrumph. The result of calling visit with 0 is multiplied by 0. Darn my socks. Sorry you all. My mistake, and I need to learn from it. Let me go back to Exercise 01 of Week 05 and make more sense out of it.
Mimer (encouragingly): That’s the spirit, Anton!
Anton exits.
Alfrothul: He’ll be back.
Dana: Shall we move on to the sum function?
Halcyon: Let’s.
Bong-sun: Let’s see. In the section about specifying and implementing a sum function, we were told:
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.
Pablito (bravely): Well, let’s start with a unit-test function:
let test_sum candidate f =
let b0 = (candidate f 0 = 0)
and b1 = (candidate f 1 = 0 + f 0)
and b2 = (candidate f 2 = 0 + f 0 + f 1)
and b3 = (candidate f 3 = 0 + f 0 + f 1 + f 2)
and b4 = (candidate f 4 = 0 + f 0 + f 1 + f 2 + f 3)
in b0 && b1 && b2 && b3 && b4;;
Dana: So b0 is the base case.
Pablito: Right. Let me rename it and add a random instance of the induction step:
let test_sum candidate f =
let bc = (candidate f 0 = 0) (* base case *)
and b1 = (candidate f 1 = 0 + f 0)
and b2 = (candidate f 2 = 0 + f 0 + f 1)
and b3 = (candidate f 3 = 0 + f 0 + f 1 + f 2)
and b4 = (candidate f 4 = 0 + f 0 + f 1 + f 2 + f 3)
and is = (let i' = Random.int 10 (* random instance of the induction step *)
in candidate f (succ i') = candidate f i' + f i')
in bc && b1 && b2 && b3 && b4 && is;;
Alfrothul: Thanks, Pablito. And now that the base case and the induction steps are spelled out, the recursive implementation pretty much writes itself:
let sum_rec f n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in ih + f i'
in visit n;;
Pablito: Checking:
# test_sum sum_rec (fun n -> n);;
- : bool = true
# test_sum sum_rec succ;;
- : bool = true
# test_sum sum_rec pred;;
- : bool = true
# test_sum sum_rec (fun n -> 2 * n);;
- : bool = true
# test_sum sum_rec (fun n -> 2 * n + 1);;
- : bool = true
#
Pablito: Yup.
Bong-sun: And since this implementation is structurally recursive and uses the induction variable, we also go with nat_parafold_right:
let sum_right f n =
nat_parafold_right
0
(fun i' ih ->
ih + f i')
n;;
Pablito: Checking:
# test_sum sum_right (fun n -> n);;
- : bool = true
# test_sum sum_right succ;;
- : bool = true
# test_sum sum_right pred;;
- : bool = true
# test_sum sum_right (fun n -> 2 * n);;
- : bool = true
# test_sum sum_right (fun n -> 2 * n + 1);;
- : bool = true
#
Bong-sun: Okeedokee. Now for expressing the summatorial function as an instance of the sum function...
Pablito: Actually we just tested that:
let summatorial_as_an_instance_of_sum n =
sum_rec succ n;;
Bong-sun: Still, let’s check:
# test_summatorial summatorial_as_an_instance_of_sum;;
- : bool = true
#
Halcyon: Yay!
Bong-sun: Let’s see. In the section about specifying and implementing a capital sigma function, we were told:
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.)
Dana: Hum.
Bong-sun: Right. Say that j is 0. We can then see that the summation operator is applying f to the k + 1 first natural numbers, not to the k first ones.
Dana: Right. It would be simpler if k was the number of natural numbers that follows j.
Bong-sun: We need a stepping stone.
Dana: We do. Fourth Wall?
The fourth wall: Yes?
Dana: May we have a stepping stone here?
The fourth wall: Of course.
Dana: Thanks, Fourth Wall.
The fourth wall: At your service.
Bong-sun: Great! Let’s first start from 0:
let test_capital_sigma' candidate f =
let b0 = (candidate f 0 0 = 0)
and b1 = (candidate f 0 1 = 0 + f 0)
and b2 = (candidate f 0 2 = 0 + f 0 + f 1)
and b3 = (candidate f 0 3 = 0 + f 0 + f 1 + f 2)
and b4 = (candidate f 0 4 = 0 + f 0 + f 1 + f 2 + f 3)
in b0 && b1 && b2 && b3 && b4;;
Dana: And then let’s start from another number:
let test_capital_sigma' candidate f =
let b0 = (candidate f 0 0 = 0)
and b1 = (candidate f 0 1 = 0 + f 0)
and b2 = (candidate f 0 2 = 0 + f 0 + f 1)
and b3 = (candidate f 0 3 = 0 + f 0 + f 1 + f 2)
and b4 = (candidate f 0 4 = 0 + f 0 + f 1 + f 2 + f 3)
and b5 = (candidate f 5 0 = 0)
and b6 = (candidate f 5 1 = 0 + f 5)
and b7 = (candidate f 5 2 = 0 + f 5 + f 6)
and b8 = (candidate f 5 3 = 0 + f 5 + f 6 + f 7)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Dana (mumbling to himself): Now to make that clear:
let test_capital_sigma' candidate f =
let b0 = (candidate f 0 0 = 0)
and b1 = (candidate f 0 1 = 0 + f 0)
and b2 = (candidate f 0 2 = 0 + f 0 + f 1)
and b3 = (candidate f 0 3 = 0 + f 0 + f 1 + f 2)
and b4 = (candidate f 0 4 = 0 + f 0 + f 1 + f 2 + f 3)
and b5 = (candidate f 5 0 = 0)
and b6 = (candidate f 5 1 = 0 + f (5 + 0))
and b7 = (candidate f 5 2 = 0 + f (5 + 0) + f (5 + 1))
and b8 = (candidate f 5 3 = 0 + f (5 + 0) + f (5 + 1) + f (5 + 2))
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Bong-sun: Right, that’s clearer. Let me restate the first half of the tests as well:
let test_capital_sigma' candidate f =
let b0 = (candidate f 0 0 = 0)
and b1 = (candidate f 0 1 = 0 + f (0 + 0))
and b2 = (candidate f 0 2 = 0 + f (0 + 0) + f (0 + 1))
and b3 = (candidate f 0 3 = 0 + f (0 + 0) + f (0 + 1) + f (0 + 2))
and b4 = (candidate f 0 4 = 0 + f (0 + 0) + f (0 + 1) + f (0 + 2) + f (0 + 3))
and b5 = (candidate f 5 0 = 0)
and b6 = (candidate f 5 1 = 0 + f (5 + 0))
and b7 = (candidate f 5 2 = 0 + f (5 + 0) + f (5 + 1))
and b8 = (candidate f 5 3 = 0 + f (5 + 0) + f (5 + 1) + f (5 + 2))
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Dana: OK. So capital_sigma' is defined by induction on its third parameter.
Alfrothul: How about adding a random instance of the induction step in test_capital_sigma'?
Dana: Good idea.
Alfrothul: Let me add two:
let test_capital_sigma' candidate f =
let b0 = (candidate f 0 0 = 0) (* instance of the base case when j = 0 *)
and b1 = (candidate f 0 1 = 0 + f (0 + 0))
and b2 = (candidate f 0 2 = 0 + f (0 + 0) + f (0 + 1))
and b3 = (candidate f 0 3 = 0 + f (0 + 0) + f (0 + 1) + f (0 + 2))
and b4 = (candidate f 0 4 = 0 + f (0 + 0) + f (0 + 1) + f (0 + 2) + f (0 + 3))
and is0 = (let i' = Random.int 10 (* random instance of the induction step when j = 0 *)
in candidate f 0 (succ i') = candidate f 0 i' + f (0 + i'))
and b5 = (candidate f 5 0 = 0) (* instance of the base case when j = 5 *)
and b6 = (candidate f 5 1 = 0 + f (5 + 0))
and b7 = (candidate f 5 2 = 0 + f (5 + 0) + f (5 + 1))
and b8 = (candidate f 5 3 = 0 + f (5 + 0) + f (5 + 1) + f (5 + 2))
and is5 = (let i' = Random.int 10 (* random instance of the induction step when j = 5 *)
in candidate f 5 (succ i') = candidate f 5 i' + f (5 + i'))
in b0 && b1 && b2 && b3 && b4 && is0 && b5 && b6 && b7 && b8 && is5;;
Bong-sun: Thanks, Alfrothul. Let’s see. I think we are good to go:
let capital_sigma'_rec f j n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in ih + f (j + i')
in visit n;;
Pablito: Checking:
# test_capital_sigma' capital_sigma'_rec (fun n -> n);;
- : bool = true
# test_capital_sigma' capital_sigma'_rec succ;;
- : bool = true
# test_capital_sigma' capital_sigma'_rec (fun n -> 100 * n);;
- : bool = true
#
Dana: Thanks, Pablito. And since this implementation is structurally recursive and uses the induction variable, nat_parafold_right, here we go:
let capital_sigma'_right f j n =
nat_parafold_right
0
(fun i' ih ->
ih + f (j + i'))
n;;
Pablito: Checking:
# test_capital_sigma' capital_sigma'_right (fun n -> n);;
- : bool = true
# test_capital_sigma' capital_sigma'_right succ;;
- : bool = true
# test_capital_sigma' capital_sigma'_right (fun n -> 100 * n);;
- : bool = true
#
Bong-sun: Thanks, Pablito. So, sum as an instance of capital_sigma':
let sum_as_an_instance_of_capital_sigma' f n =
capital_sigma'_rec f 0 n;;
Pablito: Checking:
# test_sum sum_as_an_instance_of_capital_sigma' (fun n -> n);;
- : bool = true
# test_sum sum_as_an_instance_of_capital_sigma' succ;;
- : bool = true
# test_sum sum_as_an_instance_of_capital_sigma' (fun n -> 100 * n);;
- : bool = true
#
Dana: Thanks, Pablito. And summmatorial as an instance of capital_sigma':
let summatorial_as_an_instance_of_capital_sigma' n =
capital_sigma'_rec (fun i -> i) 0 (succ n);;
Pablito: Checking:
# test_sumatorial summmatorial_as_an_instance_of_capital_sigma';;
- : bool = true
#
Dana: Thanks, Pablito. I think we are done with this stepping stone.
The fourth wall: Looks like.
Bong-sun: Dibs on the unit-test function:
let test'_capital_sigma candidate f =
let b0 = (candidate f 0 0 = 0 + f 0)
and b1 = (candidate f 0 1 = 0 + f 0 + f 1)
and b2 = (candidate f 0 2 = 0 + f 0 + f 1 + f 2)
and b3 = (candidate f 0 3 = 0 + f 0 + f 1 + f 2 + f 3)
and b4 = (candidate f 0 4 = 0 + f 0 + f 1 + f 2 + f 3 + f 4)
and b5 = (candidate f 5 5 = 0 + f 5)
and b6 = (candidate f 5 6 = 0 + f 5 + f 6)
and b7 = (candidate f 5 7 = 0 + f 5 + f 6 + f 7)
and b8 = (candidate f 5 8 = 0 + f 5 + f 6 + f 7 + f 8)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Dana: So, I guess:
let capital_sigma f j k =
if j <= k
then capital_sigma'_rec f j (k - j + 1)
else 0;;
Pablito: Checking:
# test'_capital_sigma capital_sigma (fun n -> n);;
- : bool = true
# test'_capital_sigma capital_sigma succ;;
- : bool = true
# test'_capital_sigma capital_sigma (fun n -> 100 * n);;
- : bool = true
#
Anton (who is back): Well, the tests in the unit-test function could just start with f j which is the base case here, look:
let test_capital_sigma candidate f =
let b0 = (candidate f 0 0 = f 0)
and b1 = (candidate f 0 1 = f 0 + f 1)
and b2 = (candidate f 0 2 = f 0 + f 1 + f 2)
and b3 = (candidate f 0 3 = f 0 + f 1 + f 2 + f 3)
and b4 = (candidate f 0 4 = f 0 + f 1 + f 2 + f 3 + f 4)
and b5 = (candidate f 5 5 = f 5)
and b6 = (candidate f 5 6 = f 5 + f 6)
and b7 = (candidate f 5 7 = f 5 + f 6 + f 7)
and b8 = (candidate f 5 8 = f 5 + f 6 + f 7 + f 8)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Pablito: Checking:
# test_capital_sigma capital_sigma (fun n -> n);;
- : bool = true
# test_capital_sigma capital_sigma succ;;
- : bool = true
# test_capital_sigma capital_sigma (fun n -> 100 * n);;
- : bool = true
#
Anton (mumbling to himself): Lemmesee:
let refined_test_capital_sigma candidate f =
let b0 = (candidate f 0 0 = f 0)
and b1 = (candidate f 0 1 = f 0 + f 1)
and b2 = (candidate f 0 2 = f 0 + f 1 + f 2)
and b3 = (candidate f 0 3 = f 0 + f 1 + f 2 + f 3)
and b4 = (candidate f 0 4 = f 0 + f 1 + f 2 + f 3 + f 4)
and b5 = (candidate f 5 5 = f (5 + 0))
and b6 = (candidate f 5 6 = f (5 + 0) + f (5 + 1))
and b7 = (candidate f 5 7 = f (5 + 0) + f (5 + 1) + f (5 + 2))
and b8 = (candidate f 5 8 = f (5 + 0) + f (5 + 1) + f (5 + 2) + f (5 + 3))
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8;;
Pablito: Yes?
Anton: Aha:
let capital_sigma_rec f j k =
if j <= k
then let rec visit i =
if i = 0
then f j
else let i' = pred i
in let ih = visit i'
in ih + f (j + succ i')
in visit (k - j)
else 0;;
Alfrothul: Aha indeed – visit is defined recursively on the difference between the two indices. Welcome back, Anton.
Pablito: Huh, checking:
# refined_test_capital_sigma capital_sigma_rec (fun n -> n);;
- : bool = true
# refined_test_capital_sigma capital_sigma_rec succ;;
- : bool = true
# refined_test_capital_sigma capital_sigma_rec (fun n -> 100 * n);;
- : bool = true
#
Anton: And now we can define the summatorial function as a straight instance of capital_sigma, look:
let summatorial_as_an_instance_of_capital_sigma n =
capital_sigma_rec (fun i -> i) 0 n;;
Pablito: Checking:
# test_summatorial summatorial_as_an_instance_of_capital_sigma;;
- : bool = true
#
Alfrothul: And since this implementation is structurally recursive:
let capital_sigma_right f j k =
if j <= k
then nat_parafold_right
(f j)
(fun i' ih ->
ih + f (j + succ i'))
(k - j)
else 0;;
Pablito: Checking:
# test_capital_sigma capital_sigma_right (fun n -> n);;
- : bool = true
# test_capital_sigma capital_sigma_right succ;;
- : bool = true
# test_capital_sigma capital_sigma_right (fun n -> 100 * n);;
- : bool = true
#
Anton: I think we are done here.
Mimer: Yup.
Anton (tiptoeing back): Lemmesee – the multiplication operator and the neutral element for multiplication:
let capital_pi_right f j k =
if j <= k
then nat_parafold_right
(f j)
(fun i' ih ->
ih * f (j + succ i'))
(k - j)
else 1;;
Anton: And now:
let factorial_seriously_right n =
capital_pi_right succ 0 (pred n);;
Anton (muttering to himself): Checking:
# test_factorial factorial_seriously_right;;
- : bool = true
#
Anton: OK.