Alfrothul: Decimal integers As We Know Them are a shorthand for polymomials. For example:
12345 = 1 * 10^4 + 2 * 10^3 + 3 * 10^2 + 4 * 10^1 + 5 * 10^0
= (((1 * 10 + 2) * 10 + 3) * 10 + 4) * 10 + 5
Anton: Indeed. The first right-hand side is an ordinary polynomial, and the second the polynomial in Horner form.
Alfrothul: This Horner form suggests a way to convert a nonempty string of digits into the corresponding non-negative integer in base 10, by induction on the length of this string.
Halcyon: How about we name this function nat_of_digits?
Anton: That would be logical.
Pablito (diligent): Here is a unit-test function for the implementation:
let test_nat_of_digits candidate =
let b1 = (candidate "9" = 9)
and b2 = (candidate "89" = 89)
and b3 = (candidate "789" = 789)
and b4 = (candidate "6789" = 6789)
and br = (let n = Random.int 10000
in candidate (string_of_int n) = n)
in b1 && b2 && b3 && b4 && br;;
Pablito: The last test exploits the fact that nat_of_digits is a left inverse of string_of_int for non-negative integers.
Alfrothul: Thanks, Pablito, that’s pretty good!
Test test_nat_of_digits.
Alfrothul: We will also need a function to map a digit character into an integer:
let nat_of_digit c =
let () = assert ('0' <= c && c <= '9') in
int_of_char c - int_of_char '0';;
Explain nat_of_digit in your own words.
Anton: Well, we first need to check that the given string is nonempty:
let nat_of_digits s =
let n = String.length s
in let () = assert (n > 0) in
...
Dana: Not necessarily.
Anton: What’s that now? Oh, sorry – I mean what do you mean here?
Dana: In the induction step, we are going to make an addition, right?
Anton: Right.
Dana: That’s when the string is nonempty. So how about aligning the case for the empty string with this addition?
Alfrothul: Ah, right, you mean we can use the neutral element of addition if the string is empty.
Dana: Yup. If the string is empty, we can return 0 by extension.
Anton: Let me take an analogy. Say that we are to sum the first n successive natural numbers. If n is 0, we can return 0 by extension because 0 is the neutral element of addition.
Dana: Right. And ditto if we are to multiply the first n consecutive natural numbers. If n is 0, we can return 1 by extension because 1 is the neutral element of multiplication.
Pablito: You mean like in the factorial function.
Dana: I mean like in the factorial function.
Alfrothul: Let me extend test_nat_of_digits with that case...
Dana: Thanks.
Anton: OK. So we don’t first need to check whether the given string is nonempty:
let nat_of_digits s =
let n = String.length s
in ...
Alfrothul: And then we need to define a recursive function over the length of the given string:
let nat_of_digits s =
let n = String.length s
in let rec visit i =
if i = 0
then ...
else let i' = pred i
in let ih = visit i'
in ... ih ...
in visit ...;;
Anton: And initially, we should apply this recursive function to the length of the string:
let nat_of_digits s =
let n = String.length s
in let rec visit i =
if i = 0
then ...
else let i' = pred i
in let ih = visit i'
in ... ih ...
in visit n;;
Alfrothul: OK. Base case... Let’s see. We need to get the corresponding character in the string...
Anton: ...and convert it into an integer.
Halcyon: Er, guys – there is no character in the empty string.
Dana: Right. And that’s where we align this base case with the operation in the induction step.
Guess what.
The fourth wall: Are they talking to us?The fifth wall: Not sure.
Alfrothul: Thanks, guys.
Anton: Nice solution for the base case.
Dana: So, the induction step?
Anton: Well, we still need to get the corresponding character in the string...
Alfrothul: ...and convert it into an integer too.
Anton: And then we should add it, according to the Horner form.
Alfrothul: Pretty sure a multiplication by 10 is involved too.
Anton: Let me scribble something.
The fourth wall: Oh, the ignominy.
Alfrothul: On the wall?
Anton (mumbling to himself): Well:
12345 = (((1 * 10 + 2) * 10 + 3) * 10 + 4) * 10 + 5,
1234 = ((1 * 10 + 2) * 10 + 3) * 10 + 4,
123 = (1 * 10 + 2) * 10 + 3,
12 = 1 * 10 + 2,
1 = 1
so lemmesee:
# let s = "1" in nat_of_digit (String.get s 0);;
- : int = 1
# let s = "12" in (nat_of_digit (String.get s 0) * 10) + nat_of_digit (String.get s 1);;
- : int = 12
# let s = "123" in ((nat_of_digit (String.get s 0) * 10) + nat_of_digit (String.get s 1)) * 10 + nat_of_digit (String.get s 2);;
- : int = 123
# let s = "1234" in (((nat_of_digit (String.get s 0) * 10) + nat_of_digit (String.get s 1)) * 10 + nat_of_digit (String.get s 2)) * 10 + nat_of_digit (String.get s 3);;
- : int = 1234
# let s = "12345" in ((((nat_of_digit (String.get s 0) * 10) + nat_of_digit (String.get s 1)) * 10 + nat_of_digit (String.get s 2)) * 10 + nat_of_digit (String.get s 3)) * 10 + nat_of_digit (String.get s 4);;
- : int = 12345
#
Pablito: What was that?
Anton: Let me name the intermediate results:
# let s = "12345"
in let ih = let ih = let ih = let ih = let ih = 0
in ih * 10 + nat_of_digit (String.get s 0)
in ih * 10 + nat_of_digit (String.get s 1)
in ih * 10 + nat_of_digit (String.get s 2)
in ih * 10 + nat_of_digit (String.get s 3)
in ih * 10 + nat_of_digit (String.get s 4);;
- : int = 12345
#
Halcyon (cleverly): Well, the writing was on the wall.
Guess again. (You had been warned.)
Alfrothul: All right! And now for the unit tests:
let () = assert (test_nat_of_digits nat_of_digits = true);;
Anton: I can’t wait to load the file.
Pablito: Woa, woa, woa.
Dana (kindly): That was too fast?
Pablito: Er, yes?
Dana: How about we render the computation as a theater play?
Pablito (grateful): Yes, let’s.
Halcyon: Can I play too?
Dana: Yes, please. But we need a two more actors.
The fourth wall: May I be of assistance?
Dana: Wonderful, yes, thanks.
Bong-sun: I am game too.
Dana: Thanks, Bong-sun.
Pablito: So?
Dana: OK. I play nat_of_digits which is applied to "369". Bong-sun, you play visit when it is initially applied to 3, Pablito, you play visit when it is recursively applied to 2, Halcyon, you play visit when it is recursively applied to 1, and Fourth Wall, you play visit when it is recursively applied to 0. Remember to indent to convey the nesting of the calls. OK?
Everybody agrees, and Dana gets started.
Dana: Hello. I am nat_of_string and I am applied to "369". Let me compute its length – OK, it’s 3 since this string contains 3 characters, and I name it n. Let’s continue the computation.
Halcyon: And if n denotes 0?
Pablito: Then the string would contain 0 characters, it would be the empty string, and Exercise 16 (implementing the base case) took care of that.
Halcyon: OK. Just for completeness, what if n denotes a negative integer?
The fourth wall: I think we are safe here, since no strings with a negative length exist in this Euclidean space.
Dana: Right, thanks. So n denotes 3, and I get ready to call visit with 3.
Pablito: Yes, I remember Exercise 01.d this week.
Dana: Good. So, evaluating nat_of_digits "369" reduces to evaluating the let-expression that names the length of "369", which reduces to evaluating visit n, where n denotes 3. So Bong-sun, I call you with 3 as actual parameter, which is going to be the last thing I do.
Bong-sun: Hello. I am visit and I am applied to 3. 3 is not 0, and so we are in the induction step. Let me name the predecessor of 3, i.e., 2, as i'. And let me recursively call visit with i', i.e., 2, as actual parameter. So Pablito, I call you with 2 as actual parameter.
Pablito: Hello. I am visit and I am applied to 2. 2 is not 0, and so we are in the induction step. Let me name the predecessor of 2, i.e., 1, as i'. And let me recursively call visit with i', i.e., 1, as actual parameter. So Halcyon, I call you with 1 as actual parameter.
Halcyon: Hello. I am visit and I am applied to 1. 1 is not 0, and so we are in the induction step. Let me name the predecessor of 1, i.e., 0, as i'. And let me recursively call visit with i', i.e., 0, as actual parameter. So Fourth Wall, I call you with 0 as actual parameter.
The fourth wall: Hello. I am visit and I am applied to 0. 0 is 0, and so we are in the base case. I return 0 to Halcyon.Halcyon: Thank you, Fourth Wall, for 0. As per the Horner form, let me multiply it by 10 – there we go, 0. I called Fourth Wall with 0, so let me get the character at index 0 in "369", i.e., '3'. Since this character is a digit, I can call nat_of_digit to convert this digit into an integer, namely 3, which I add to 0. And then I return 3 to Pablito.
Pablito: Thank you, Halcyon, for 3. As per the Horner form, let me multiply it by 10 – there we go, 30. I called Halcyon with 1 so let me get the character at index 1 in "369", i.e., '6'. Since this character is a digit, I can call nat_of_digit to convert this digit into an integer, namely 6, which I add to 30. And then I return 36 to Bong-sun.
Bong-sun: Thank you, Pablito, for 36. As per the Horner form, let me multiply it by 10 – there we go, 360. I called Pablito with 2 so let me get the character at index 2 in "369", i.e., '9'. Since this character is a digit, I can call nat_of_digit to convert this digit into an integer, namely 9, which I add to 360. And then I return 369 to Dana.
Dana: Thank you, Bong-sun, for 369, which is the result. And thank you all for participating!
The fourth wall: Always here if you need to bounce an idea off someone.
Dana: Thank you most kindly.
She turns to Pablito, who looks contemplative.
Dana: Are things clearer now, Pablito?
Pablito: I think so, thanks. Can we play again with "x86" as an argument for nat_of_digits?
Dana: Sure thing. I still play nat_of_digits who is applied to "x86". Bong-sun, you still play visit when it is initially applied to 3, Halcyon, you play visit when it is recursively applied to 2, Pablito, you play visit when it is recursively applied to 1, and Fourth Wall, you still play visit when it is recursively applied to 0. And you all indent to convey the nesting of the calls. OK?
Everybody agrees, and Dana gets started.
Dana: Hello. I am nat_of_string and I am applied to "x86". Let me compute its length – OK, it’s 3 since this string contains 3 characters, and I name it n. So, evaluating nat_of_digits "x86" reduces to evaluating the let-expression that names the length of "x86", which reduces to evaluating visit n, where n denotes 3. So Bong-sun, I call you with 3 as actual parameter, which is going to be the last thing I do.
Bong-sun: Hello. I am visit and I am applied to 3. 3 is not 0, and so we are in the induction step. Let me name the predecessor of 3, i.e., 2, as i'. And let me recursively call visit with i', i.e., 2, as actual parameter. So Halcyon, I call you with 2 as actual parameter.
Halcyon: Hello. I am visit and I am applied to 2. 2 is not 0, and so we are in the induction step. Let me name the predecessor of 2, i.e., 1, as i'. And let me recursively call visit with i', i.e., 1 as actual parameter. So Pablito, I call you with 1 as actual parameter.
Pablito: Hello. I am visit and I am applied to 1. 1 is not 0, and so we are in the induction step. Let me name the predecessor of 1, i.e., 0, as i'. And let me recursively call visit with i', i.e., 0 as actual parameter. So Fourth Wall, I call you with 0 as actual parameter.
The fourth wall: Hello. I am visit and I am applied to 0. 0 is 0, and so we are in the base case. I return 0 to Pablito.Pablito: Thank you, Fourth Wall, for 0. As per the Horner form, let me multiply it by 10 – there we go, 0. I called Fourth Wall with 0, so let me get the character at index 0 in "x86", i.e., 'x'. Since this character is not a digit, the assertion in nat_of_digit fails and the whole computation stops.
Dana: OK Pablito?
Pablito: Yup.
The fourth wall: Maybe we could check at the outset that the given string only contains digits? Then there would be no recursive calls at all if a given string contains something else than a digit, and all the recursive calls would complete if the given string only contains digits.
Dana: And we would check that how?
Pablito: With String.map?
What do you think? Yes, exactly.
Anton: So we only convert a string to a non-negative integer if it contains digits?
Alfrothul: Yup. It’s kind of like a statically typed program, which is only executed if it is both syntactically correct and type correct.
The fourth wall: BTW, thanks, guys.
Dana: Er, sure. But why?
The fourth wall: For talking, well, to a wall.
Dana: You do talk back.
The fourth wall: Yes, there is that.
Dana: OK. So we can implement nat_of_digits by following the Horner form:
12345 = (((1 * 10 + 2) * 10 + 3) * 10 + 4) * 10 + 5
Alfrothul: But we could also implement it by following the standard form:
12345 = 1 * 10^4 + 2 * 10^3 + 3 * 10^2 + 4 * 10^1 + 5 * 10^0
Dana: This example is messy. Let me swap the order of the digits:
43210 = 4 * 10^4 + 3 * 10^3 + 2 * 10^2 + 1 * 10^1 + 0 * 10^0
Alfrothul: It’s still messy – for "43210", the coefficient for 10^4 is at index 0, the coefficient for 10^3 is at index 1, the coefficient for 10^2 is at index 2, the coefficient for 10^1 is at index 3, and the coefficient for 10^0 is at index 4.
Dana: ‘fraid you’re right:
3210 = 3 * 10^3 + 2 * 10^2 + 1 * 10^1 + 0 * 10^0
210 = 2 * 10^2 + 1 * 10^1 + 0 * 10^0
10 = 1 * 10^1 + 0 * 10^0
0 = 0 * 10^0
Alfrothul: Unfortunately. For "210", the coefficient for 10^2 is at index 0, the coefficient for 10^1 is at index 1, and the coefficient for 10^0 is at index 2.
Dana: On the other hand, if we subtract these successive indices from the last possible index, the enumeration is aligned, look. For "210", the last possible index – let me name it “li” – is 2.
Alfrothul: Yes, the length of the string minus 1, I remember Exercise 01.d.
Dana: So for "210", the coefficient for 10^2 is at index li-2, the coefficient for 10^1 is at index li-1, and the coefficient for 10^0 is at index li-0. Look:
let nat_of_digits_B s =
let n = String.length s
in let last_index = pred n
in let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in nat_of_digit (String.get s (last_index - i')) * power 10 i' + ih
in visit n;;
Alfrothul: And vice-versa, actually. For "210", the coefficient for 10^(li-2) is at index 2, the coefficient for 10^(li-1) is at index 1, and the coefficient for 10^(li-0) is at index 0. Look:
let nat_of_digits_A s =
let n = String.length s
in let last_index = pred n
in let rec visit i =
if i = 0
then 0
else let i' = pred i
in let ih = visit i'
in nat_of_digit (String.get s i') * power 10 (last_index - i') + ih
in visit n;;
Pablito (diligent): Lemme check:
# test_nat_of_digits nat_of_digits_B;;
- : bool = true
# test_nat_of_digits nat_of_digits_A;;
- : bool = true
#
Compare the number of multiplications in nat_of_digits and in either nat_of_digits_B or nat_of_digits_A and power.
Dana: Isn’t it funny how i decreases through the recursive calls in the factorial function?
Alfrothul: Well, that’s the point of structural recursion, and anyway we need it to decrease in order to compute the resulting factorial number. That said, we could use its complement, which increases, like in the definition of nat_of_digits_B.
Dana: Right. So that instead of computing, e.g.:
5 * (4 * (3 * (2 * (1 * 1))))
we would compute:
1 * (2 * (3 * (4 * (5 * 1))))
instead.
Alfrothul: Not that the result is going to be different, since multiplication is associative and commutative. But still, let’s try:
let fac_alt 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 (n - i') * ih
in visit n;;
Dana: Let’s check:
# test_fac fac_alt;;
- : bool = true
#
Alfrothul <clickety clickety clickety click>: OK, let’s visualize the computation with a trace:
# traced_fac_alt 5;;
fac_alt 5 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 1
visit 1 <- 5
visit 2 <- 20
visit 3 <- 60
visit 4 <- 120
visit 5 <- 120
fac_alt 5 <- 120
- : int = 120
#
Alfrothul: The numbers that are successfully returned don’t say much.
Dana: In contrast, the numbers returned in the original factorial function are the successive factorial numbers:
# traced_fac 5;;
fac 5 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 1
visit 1 <- 1
visit 2 <- 2
visit 3 <- 6
visit 4 <- 24
visit 5 <- 120
fac 5 <- 120
- : int = 120
#
Mimer: Yes. These successive factorial numbers are the rising factorial numbers of 5, and the others are the falling factorial numbers of 5: 5, 4 * 5, 3 * 4 * 5, 2 * 3 * 4 * 5, and 1 * 2 * 3 * 4 * 5.
Alfrothul: Thanks, Mimer.
Dana (facetiously): Why don’t we verify that this property holds?
Alfrothul: Er, sure, but how?
Dana: With an assertion. But let me first make sure about something:
# 5 = fac 5 / fac 4;;
- : bool = true
# 4 * 5 = fac 5 / fac 3;;
- : bool = true
# 3 * 4 * 5 = fac 5 / fac 2;;
- : bool = true
# 2 * 3 * 4 * 5 = fac 5 / fac 1;;
- : bool = true
# 1 * 2 * 3 * 4 * 5 = fac 5 / fac 0;;
- : bool = true
#
Dana: OK. Here we go:
let fac_alt_with_an_assertion n =
let () = assert (n >= 0) in
let fac_n = fac n
in let rec visit i =
if i = 0
then 1
else let i' = pred i
in let ih = visit i'
in let () = assert (ih = fac_n / fac (n - i')) in
(n - i') * ih
in visit n;;
Dana: See? If the assertion doesn’t hold, the execution will stop. And also, fac n is computed only once, thanks to the let-expression.
Alfrothul (prudent): Let’s check:
# test_fac fac_alt_with_an_assertion;;
- : bool = true
#
Bong-sun: Wow!
Implement a function dot_product that satisfies the following specification:
dot_product f g 0 = 0
dot_product f g (n + 1) = f 0 * g 0 + f 1 * g 1 + ... + f (n - 1) * g (n - 1) + f n * g n
Implement a function convolution that satisfies the following specification:
convolution f g 0 = 0
convolution f g (n + 1) = f 0 * g n + f 1 * g (n - 1) + ... + f (n - 1) * g 1 + f n * g 0
Re-implement nat_of_digits_B as an instance of convolution.
Included Na Bong-sun to render the computation as a theater play [13 Feb 2023]
Added Exercise 20.c [13 Feb 2023]
Added Section The rise and fall of Factorial numbers and Exercise 20 [12 Feb 2023]
Added the aftermath and Exercise 19 [12 Feb 2023]
Added Anton’s scribblings before Exercise 17 (implementing the induction step) [10 Feb 2023]
Polished the narrative [23 Jan 2023]
Created [10 Jan 2023]