The goal of this lecture note is to articulate the inductive specification of a computation over natural numbers and how to program the corresponding recursive functions in OCaml.
Warning
Caveat: succ denotes a predeclared function in OCaml, it is not a data constructor for integers.
(Reminder: succ and pred respectively denote increment and decrement functions, i.e., functions that respectively add 1 and subtract 1 to their argument.)
The concept of grammar in linguistics can be exported to specifying not just programming languages, but any kind of data. For example, here is yet again the grammar of natural numbers (Peano numbers):
<natural-number> ::= 0
| succ <natural-number>
An onion by any other name...—Juliet
This grammar is sound in that using the two constructors 0 and succ, we can construct natural numbers. And it is complete in that any natural number can be expressed as a combination of 0 and succ.
To wit:
# succ;;
- : int -> int = <fun>
# succ 0;;
- : int = 1
# succ 1;;
- : int = 2
# succ (succ 0);;
- : int = 2
#
This self-referential way of specifying data inductively has a computational counterpart: a way of processing data recursively that lets us define a self-referential, i.e., recursive, OCaml function. In the induction step, the function calls itself. Its name is then part of its definition, and it is declared with the keyword rec.
The corresponding typing rule reads as follows:
| REC | (f : t1 -> t2), G |- fun x1 -> e2 : t1 -> t2 | (f : t1 -> t2), G |- e0 : t0 | |
| G |- let rec f = fun x1 -> e2 in e0 : t0 | |||
In words: in any type environment G, the expression let rec f = fun x1 -> e2 in e0 has type t0 whenever, in an extension of this environment where f has type t1 -> t2, (1) fun x1 -> e2 has type t1 -> t2 and (2) e0 has type t0.
Removing the rec would make the REC rule devolve into an instance of the LET rule where the definiens is a function abstraction:
| LET | G |- fun x1 -> e2 : t1 -> t2 | (f : t1 -> t2), G |- e0 : t0 | |
| G |- let rec f = fun x1 -> e2 in e0 : t0 | |||
In the LET rule, f is only lexically visible in e0. In the REC rule, f is also lexically visible in fun x1 -> x2.
Expanding the left premise of the REC rule illustrates how e2 is processed in an environment where f is bound:
(x1 : t1), (f : t1 -> t2), G |- e2 : t2
FUN --------------------------------------------
(f : t1 -> t2), G |- fun x1 -> e2 : t1 -> t2
When let rec f = fun x1 -> e2 in e0 is evaluated, the definiens (i.e., fun x1 -> e2) is first evaluated in an extension of the current environment where f denotes the result of evaluating fun x1 -> e2 in this extended environment. The body e0 is then evaluated in this extended environment, yielding a value v0 if this evaluation completes. The result of evaluating the let rec expression is v0. The binding of f is local to the let rec expression, and vanishes once this expression is evaluated.
N.B.: Forgetting to write rec, when declaring a function, means that the occurrence of the name in the body of the function will refer to an earlier occurrence of this name in the environment, if there was one.
Likewise, recursive functions can be declared at the toplevel:
In practice, the long-handed declaration:
let rec foo = fun x -> ...
is shortened to:
let rec foo x = ...
The goal of this section is to specify the multiplication of a natural number by 2 by mathematical induction, and to then implement this computation with a recursive function.
First thing first, let us write a unit-test function:
let test_twice t =
let b0 = (t 0 = 0)
and b1 = (t 1 = 2)
and b2 = (t 2 = 4)
and b3 = (t 3 = 6)
and b4 = (let n = Random.int 10000
in t n = 2 * n)
(* etc. *)
in b0 && b1 && b2 && b3 && b4;;
For the sake of sanity, let us test this unit-test function:
# test_twice (fun n -> 2 * n);;
- : bool = true
# test_twice (fun n -> n + n);;
- : bool = true
#
For the sake of lucidity, let us write a fake twice function that passes the unit test:
# test_twice (fun n -> if n < 10000 then 2 * n else ~-1);;
- : bool = true
#
Now for the idea. By the completeness of Peano numbers, the number n can be represented by applying succ n times to 0. If we were to duplicate each occurrence of succ in n, we would double n:
# (succ 0, succ (succ 0));;
- : int * int = (1, 2)
# (succ (succ 0), succ (succ (succ (succ 0))));;
- : int * int = (2, 4)
#
Hence the inductive specification of how to double up a natural number:
(The intuition behind this inductive specification is that 2 * n = succ (succ (succ (succ (... (succ (succ (0)))...)))), where succ is iteratively applied 2 * n times to 0, as per Exercise 0 in the lecture note about strings.)
Let us express this inductive specification as the declaration of a recursive function:
let rec twice_v0 n =
if n = 0
then ...
else let n' = pred n
in let ih = twice_v0 n'
in ...;;
In this implementation, we distinguish the base case and the induction step with an if-expression testing whether the given number is 0 or not. If it is, we put in the consequent what is specified in the base case:
let rec twice_v0 n =
if n = 0
then 0
else let n' = pred n
in let ih = twice_v0 n'
in ...;;
If the given number n is not 0, this means that it is the successor of another number, n', which we compute. We then implement the induction hypothesis with a recursive call over n', and then complete the alternative with what is specified in the induction step:
let rec twice_v0 n =
if n = 0
then 0
else let n' = pred n
in let ih = twice_v0 n'
in succ (succ ih);;
This implementation passes the unit test:
# test_twice twice_v0;;
- : bool = true
#
It also is vulnerable to being applied to a negative integer (which would make it diverge), so we should shield it by asserting that its given integer lies above 0:
let twice_v1 n_given =
let () = assert (0 <= n_given) in
let rec visit n =
if n = 0
then 0
else let n' = pred n
in let ih = visit n'
in succ (succ ih)
in visit n_given;;
This shielded implementation passes the unit test:
# test_twice twice_v1;;
- : bool = true
#
Because this recursive implementation mirrors the corresponding inductive specification, it is said to be structurally recursive.
That twice_v1 has type int -> int is proved by constructing the following proof tree (using the obvious typing rule LESSER_OR_EQUAL):
INT ----------------------------------------------------------------------- LOOKUP_FOUND -----------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- 0 : int (n_given : int), (succ : int -> int), (pred : int -> int), G |- n_given : int
LESSER_OR_EQUAL ---------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- 0 <= n_given : bool
ASSERT --------------------------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- assert (0 <= n_given) : unit XXX
LET ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- let () = assert (0 <= n_given) in let rec visit n = if n = 0 then 0 else let n' = pred n in let ih = visit n' in succ (succ ih) in visit n_given : int
FUN ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(succ : int -> int), (pred : int -> int), G |- fun n_given -> let () = assert (0 <= n_given) in let rec visit n = if n = 0 then 0 else let n' = pred n in let ih = visit n' in succ (succ ih) in visit n_given : int -> int
where the tree XXX reads as follows:
LOOKUP_FOUND -----------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- n_given : int
LOOKUP_FOUND -------------------------------------------------------------------------------------------------------- LOOKUP_NOT_FOUND ---------------------------------------------------------------------------------------------------
(visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G |- visit : int -> int (visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G |- n_given : int
APP --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
YYY (visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G |- visit n_given : int
REC ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n_given : int), (succ : int -> int), (pred : int -> int), G |- let rec visit n = if n = 0 then 0 else let n' = pred n in let ih = visit n' in succ (succ ih) in visit n_given : int
where the tree YYY reads as follows, writing ... to stand for (n : int), (visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G:
... |- n = 0 : bool ... |- 0 : int ... |- let n' = pred n in let ih = visit n' in succ (succ ih) : int
IF ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(n : int), (visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G |- if n = 0 then 0 else let n' = pred n in let ih = visit n' in succ (succ ih) : int
FUN ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
(visit : int -> int), (n_given : int), (succ : int -> int), (pred : int -> int), G |- fun n -> if n = 0 then 0 else let n' = pred n in let ih = visit n' in succ (succ ih) : int -> int
where constructing the proof trees rooted in the premises of the instance of IF is routine.
To visualize the computation, let us instrument the implementation with tracing information. The idea is that every call to visit emits a trace, and that so does every return:
let indent i =
String.make (2 * i) ' ';;
let traced_twice_v1 n_given =
let () = Printf.printf "twice_v1 %s ->\n" (show_int n_given) in
let () = assert (0 <= n_given) in
let rec visit n i =
let () = Printf.printf "%svisit %s ->\n" (indent i) (show_int n) in
let result = if n = 0
then 0
else let n' = pred n
in let ih = visit n' (i + 1)
in succ (succ ih)
in let () = Printf.printf "%svisit %s <- %s\n" (indent i) (show_int n) (show_int result) in
result
in let result = visit n_given 1
in let () = Printf.printf "twice_v1 %s <- %s\n" (show_int n_given) (show_int result) in
result;;
Specifically,
In addition,
To wit:
# traced_twice_v1 0;;
twice_v1 0 ->
visit 0 ->
visit 0 <- 0
twice_v1 0 <- 0
- : int = 0
# traced_twice_v1 1;;
twice_v1 1 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
twice_v1 1 <- 2
- : int = 2
# traced_twice_v1 2;;
twice_v1 2 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
twice_v1 2 <- 4
- : int = 4
# traced_twice_v1 3;;
twice_v1 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
visit 3 <- 6
twice_v1 3 <- 6
- : int = 6
# traced_twice_v1 4;;
twice_v1 4 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
visit 3 <- 6
visit 4 <- 8
twice_v1 4 <- 8
- : int = 8
# traced_twice_v1 5;;
twice_v1 5 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
visit 3 <- 6
visit 4 <- 8
visit 5 <- 10
twice_v1 5 <- 10
- : int = 10
#
The implementation of the traced version of twice_v1 starts with:
let traced_twice_v1 n_given =
let () = Printf.printf "twice_v1 %s ->\n" (show_int n_given) in
let () = assert (0 <= n_given) in
...
Would it be equivalent to first test whether the given argument is non-negative? That is to say:
let traced_twice_v1 n_given =
let () = assert (0 <= n_given) in
let () = Printf.printf "twice_v1 %s ->\n" (show_int n_given) in
...
In the induction step, the let-expressions are said to be linear, in that the variable they declare is used exactly once. Furthermore this variable is used immediately. Therefore these let-expressions are only cosmetic and we can unfold them, i.e., substitute their definiens for the variable they declare. Let us proceed step by step:
unfolding the declaration of n':
let twice_v2 n_given =
let () = assert (0 <= n_given) in
let rec visit n =
if n = 0
then 0
else let ih = visit (pred n)
in succ (succ ih)
in visit n_given;;
We have substituted the definiens pred n for the variable n'.
unfolding the declaration of ih:
let twice_v3 n_given =
let () = assert (0 <= n_given) in
let rec visit n =
if n = 0
then 0
else succ (succ (visit (pred n)))
in visit n_given;;
We have substituted the definiens visit (pred n) for the variable ih.
Both simplified implementations pass the unit test:
# test_twice twice_v2;;
- : bool = true
# test_twice twice_v3;;
- : bool = true
#
Due to the dramatic spillage of an excessively caffeinated beverage all over your keyboard, you realize with dismay that the + key has stopped working. For some unspecified reason, you however are in urgent need to perform a series of additions of natural numbers in OCaml. Fortunately, OCaml features the predefined function succ that maps an integer to its successor:
# succ ~-1;;
- : int = 0
# succ 0;;
- : int = 1
# succ 1;;
- : int = 2
#
You therefore man up and resolve to program your own addition function, based on the following inductive specification. Given an integer y,
(The intuition behind this inductive specification is that x + y = succ (succ (succ (... (succ y)...))), where 1 is iteratively added x times to y, as per Exercise 0 in the lecture note about strings.)
To this end,
write a unit-test function:
let test_add a =
...
define a structurally recursive function that embodies the inductive specification above (and that uses succ):
let add_v0 x_given y_given =
...
Does your recursive function pass your unit test?
can you shield your definition so that it handles being applied to a negative integer as its first argument?
ever the helpful ones, Harald and Alfrothul proposed the following definition:
let add_v1 x y =
x - (0 - y);;
Does this proposed definition pass your unit test?
add is specified over natural numbers, i.e., non-negative integers, so let’s try a few:
let test_add a =
(* an instance of the base case: *)
let b0 = (let y = Random.int 2000
in a 0 y = y)
(* an instance of the induction step: *)
and b1 = (let y = Random.int 2000
and x' = Random.int 1000
in a (succ x') y = succ (a x' y))
(* a few handpicked numbers: *)
and b2 = (a 0 100 = 100)
and b3 = (a 1 100 = 101)
and b4 = (a 2 100 = 102)
(* using a witness implementation of the addition function *)
and b5 = (let x = Random.int 1000
and y = Random.int 2000
in a x y = x + y) (* so much for the dramatic spillage *)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5;;
For the sake of sanity, let us test this unit-test function, copy-pasting the + character since the + key doesn’t work:
# test_add (+);;
- : bool = true
#
For the sake of lucidity, let us write a fake addition function that passes the unit test:
# test_add (fun x y -> if x < 1000 then x + y else ~-1);;
- : bool = true
#
since add is specified over natural numbers, we might as well shield it. Here is its skeleton:
let add_v0 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then ...
else let x' = pred x
in let ih = visit x'
in ... ih ...
in visit x_given;;
Rationale:
Now all we need is to fill the blanks:
in the base case, the result is y_given, and
in the induction step, the result is obtained by applying succ to the result of the recursive call:
let add_v0 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then y_given
else let x' = pred x
in let ih = visit x'
in succ ih
in visit x_given;;
This shielded implementation is structurally recursive and it passes our unit test:
# test_add add_v0;;
- : bool = true
#
Not only that, but since it is structurally recursive, code coverage is ensured since the unit-test function tests both the base case and the induction step.
our definition is already shielded.
yes, Harald and Alfrothul’s definition passes our unit test:
# test_add add_v1;;
- : bool = true
#
This definition is mathematically correct because subtracting a negative number is the same as adding the corresponding positive number.
To visualize the recursive computation implemented in add_v0, let us instrument this implementation with tracing information:
let traced_add_v0 x_given y_given =
let () = Printf.printf "add_v0 %s %s ->\n" (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then y_given
else let x' = pred x
in let ih = visit x' (i + 1)
in succ ih
in let () = Printf.printf "%svisit %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x_given 1
in let () = Printf.printf "add_v0 %s %s <- %s\n" (show_int x_given) (show_int y_given) (show_int result) in
result;;
Specifically,
In addition,
To wit:
# traced_add_v0 0 10;;
add_v0 0 10 ->
visit 0 ->
visit 0 <- 10
add_v0 0 10 <- 10
- : int = 10
# traced_add_v0 1 10;;
add_v0 1 10 ->
visit 1 ->
visit 0 ->
visit 0 <- 10
visit 1 <- 11
add_v0 1 10 <- 11
- : int = 11
# traced_add_v0 2 10;;
add_v0 2 10 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 10
visit 1 <- 11
visit 2 <- 12
add_v0 2 10 <- 12
- : int = 12
# traced_add_v0 3 10;;
add_v0 3 10 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 10
visit 1 <- 11
visit 2 <- 12
visit 3 <- 13
add_v0 3 10 <- 13
- : int = 13
#
In the induction step, the let-expressions that declare n' and ih, in the definition of visit, are cosmetic and so we can unfold them:
let add_v2 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then y_given
else succ (visit (pred x))
in visit x_given;;
This simplified implementation is still structurally recursive and it passes the unit test:
# test_add add_v2;;
- : bool = true
#
Vigfus: The exercise was about adding two natural numbers, right?
Mimer: Yes it was.
Vigfus: And since OCaml does not have natural numbers, but only integers, we have put an assertion to check that the function is not applied to a negative integer, right?
Mimer: Right.
Vigfus: Then why is the implementation only checking that the first argument is non-negative and not the second?
Mimer: Good point, Vigfus. Do you think it matters?
Vigfus: I guess it doesn’t.
This exercise is a followup to Exercise 6.
The internal damage in your keyboard is spreading, and now the * key too has stopped working. Again, for some unspecified reason, you are in urgent need to perform a series of multiplications of natural numbers and integers in OCaml. So again you man up and resolve to program your own multiplication function, based on the following inductive specification. Given an integer y,
(The intuition behind this inductive specification is that x * y = y + (... (y + (y + (y + (0))))...), where y is iteratively added to the left x times to 0, as per Exercise 0 in the lecture note about strings.)
This inductive specification is aligned with the other inductive specifications so far (i.e., for computing a Factorial number, for doubling up a natural number, and for adding two natural numbers), but for the sake of variation, and since addition is commutative, let us consider the following alternative inductive specification. Given an integer y,
(The intuition behind this inductive specification is that x * y = (...((((0) + y) + y) + y) ...) + y, where y is iteratively added to the right x times to 0.)
To this end,
write a unit-test function:
let test_mul m =
...
define a structurally recursive function that embodies the inductive specification above (and that uses add_v0 or add_v1):
let mul_v0 x_given y_given =
...
Does your recursive function pass your unit test?
ever the helpful ones, Harald and Alfrothul proposed the following definition:
let mul_v1 x y =
x / (1 / y);;
Does this proposed function pass your unit test?
mul is specified over natural numbers, i.e., non-negative integers, so let’s try a few:
let test_mul m =
(* an instance of the base case: *)
let b0 = (let y = Random.int 1000
in m 0 y = 0)
(* an instance of the induction step: *)
and b1 = (let y = Random.int 1000
and x' = Random.int 99
in m (succ x') y = (m x' y) + y)
(* a few handpicked numbers: *)
and b2 = (m 0 100 = 0)
and b3 = (m 1 100 = 100)
and b4 = (m 2 100 = 200)
(* using a witness implementation of the multiplication function *)
and b5 = (let x = Random.int 100
and y = Random.int 1000
in m x y = x * y) (* so much for the dramatic spillage *)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5;;
For the sake of sanity, let us test this unit-test function:
# test_mul ( * );;
- : bool = true
#
For the sake of lucidity, let us write a fake multiplication function that passes the unit test:
# test_mul (fun x y -> if x < 200 then x * y else ~-1);;
- : bool = true
#
since mul is specified over natural numbers, we might as well shield it. Here is its skeleton:
let mul_v0 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then ...
else let x' = pred x
in let ih = visit x'
in ...
in visit x_given;;
Rationale:
Now all we need is to fill the blanks:
in the base case, the result is 0, and
in the induction step, the result is obtained by applying add_v0 to the result of the recursive call and to y_given:
let mul_v0 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then 0
else let x' = pred x
in let ih = visit x'
in add_v0 ih y_given
in visit x_given;;
This shielded implementation is structurally recursive and it passes our unit test:
# test_mul mul_v0;;
- : bool = true
#
Also, since it is structurally recursive, code coverage is ensured since the unit-test function tests both the base case and the induction step.
our definition is already shielded.
no, Harald and Alfrothul’s definition does not pass our unit test:
# test_mul mul_v1;;
Exception: Division_by_zero.
#
This definition only works when the second argument is 1 because / computes the quotient function.
To visualize the computation, let us instrument the implementation with tracing information. The idea is that every call to visit emits a trace, and that so does every return:
let traced_mul_v0 x_given y_given =
let () = Printf.printf "mul_v0 %s %s ->\n" (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then 0
else let x' = pred x
in let ih = visit x' (i + 1)
in ih + y_given
in let () = Printf.printf "%svisit %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x_given 1
in let () = Printf.printf "mul_v0 %s %s <- %s\n" (show_int x_given) (show_int y_given) (show_int result) in
result;;
Specifically,
In addition,
To wit:
# traced_mul_v0 0 10;;
mul_v0 0 10 ->
visit 0 ->
visit 0 <- 0
mul_v0 0 10 <- 0
- : int = 0
# traced_mul_v0 1 10;;
mul_v0 1 10 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 10
mul_v0 1 10 <- 10
- : int = 10
# traced_mul_v0 2 10;;
mul_v0 2 10 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 10
visit 2 <- 20
mul_v0 2 10 <- 20
- : int = 20
# traced_mul_v0 3 10;;
mul_v0 3 10 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 10
visit 2 <- 20
visit 3 <- 30
mul_v0 3 10 <- 30
- : int = 30
#
In the induction step, the let-expressions that declare n' and ih, in the definition of visit, are cosmetic and so we can unfold them:
let mul_v2 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then 0
else add_v0 (visit (pred x)) y_given
in visit x_given;;
This simplified implementation is still structurally recursive and it passes the unit test:
# test_mul mul_v2;;
- : bool = true
#
Harald: Did you notice how the traced version of mul_v0 is using + instead of add_v0, in the induction step?
Alfrothul: True. And I didn’t notice. But it shouldn’t make any difference, should it?
Harald: Well, I don’t know. Suppose that it uses traced_add_v0.
Alfrothul: Oh, right – we could then see how each induction step in the multiplication function triggers an addition:
let traced_mul_v0' x_given y_given =
let () = Printf.printf "mul_v0' %s %s ->\n" (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then 0
else let x' = pred x
in let ih = visit x' (i + 1)
in traced_add_v0 ih y_given
in let () = Printf.printf "%svisit %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x 1
in let () = Printf.printf "mul_v0 %s %s <- %s\n" (show_int x_given) (show_int y_given) (show_int result) in
result;;
Harald: Let’s see:
# traced_mul_v0' 2 3;;
mul_v0' 2 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
add_v0 0 3 ->
visit 0 ->
visit 0 <- 3
add_v0 0 3 <- 3
visit 1 <- 3
add_v0 3 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 3
visit 1 <- 4
visit 2 <- 5
visit 3 <- 6
add_v0 3 3 <- 6
visit 2 <- 6
mul_v0 2 3 <- 6
- : int = 6
#
Alfrothul: That seems broken.
Harald: Yes, the indentation is off, for example.
Alfrothul: Right – because traced_add_v0 assumes it is called at the toplevel, but it isn’t.
Harald: Also, it is confusing that both traced_mul_v0 and traced_add_v0 use visit as a trace.
Alfrothul: So we should define another version of traced_add_v0 that is parameterized by the current number of nested calls.
Brynja (interjecting): Ditto for traced_mul_v0' in case it is not called at the toplevel.
Harald: And we should make traced_mul_v0 and traced_add_v0 use distinct instances of visit as a trace:
let traced_add_v0' x_given y_given i_given =
let () = Printf.printf "%sadd_v0 %s %s ->\n" (indent i_given) (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit_add_v0 %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then y_given
else let x' = pred x
in let ih = visit x' (i + 1)
in succ ih
in let () = Printf.printf "%svisit_add_v0 %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x_given (i_given + 1)
in let () = Printf.printf "%sadd_v0 %s %s <- %s\n" (indent i_given) (show_int x_given) (show_int y_given) (show_int result) in
result;;
let traced_mul_v0' x_given y_given i_given =
let () = Printf.printf "%smul_v0 %s %s ->\n" (indent i_given) (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit_mul_v0 %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then 0
else let x' = pred x
in let ih = visit x' (i + 1)
in traced_add_v0' ih y_given (i + 1)
in let () = Printf.printf "%svisit_mul_v0 %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x_given (i_given + 1)
in let () = Printf.printf "%smul_v0 %s %s <- %s\n" (indent i_given) (show_int x_given) (show_int y_given) (show_int result) in
result;;
Alfrothul: Let’s see:
# traced_mul_v0' 2 3;;
- : int -> int = <fun>
#
Harald: Huh?
Alfrothul: My bad. As Brynja pointed out, we need to tell traced_mul_v0' that it starts with zero nested calls:
# traced_mul_v0' 4 2 0;;
mul_v0 4 2 ->
visit_mul_v0 4 ->
visit_mul_v0 3 ->
visit_mul_v0 2 ->
visit_mul_v0 1 ->
visit_mul_v0 0 ->
visit_mul_v0 0 <- 0
add_v0 0 2 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 2
add_v0 0 2 <- 2
visit_mul_v0 1 <- 2
add_v0 2 2 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 2
visit_add_v0 1 <- 3
visit_add_v0 2 <- 4
add_v0 2 2 <- 4
visit_mul_v0 2 <- 4
add_v0 4 2 ->
visit_add_v0 4 ->
visit_add_v0 3 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 2
visit_add_v0 1 <- 3
visit_add_v0 2 <- 4
visit_add_v0 3 <- 5
visit_add_v0 4 <- 6
add_v0 4 2 <- 6
visit_mul_v0 3 <- 6
add_v0 6 2 ->
visit_add_v0 6 ->
visit_add_v0 5 ->
visit_add_v0 4 ->
visit_add_v0 3 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 2
visit_add_v0 1 <- 3
visit_add_v0 2 <- 4
visit_add_v0 3 <- 5
visit_add_v0 4 <- 6
visit_add_v0 5 <- 7
visit_add_v0 6 <- 8
add_v0 6 2 <- 8
visit_mul_v0 4 <- 8
mul_v0 4 2 <- 8
- : int = 8
#
Harald: Wow.
Alfrothul: Actually, more like “Yay” – the trace clearly shows the series of additions triggered by recursive calls in the multiplication function.
Vigfus: Er... Doesn’t this series grows as the computation proceeds?
Alfrothul: Beg pardon?
Harald: Well spotted, Vigfus – visit_mul_v0 successively returns 0, and then 2, and then 4, etc., and each time, it triggers a call to add_v0 with this number and the multiplicand.
Vigfus: The multiplicand?
Harald: Well, you know, as the French say, culture is like marmalade: the less you have of it, the more you spread it.
Alfrothul: Like, “marmalade” is “confiture” in French, which rhymes with “culture”.
Vigfus (clickety-clickety-click): I see. The first argument of the multiplication function is the multiplier and the second the multiplicand.
Harald: Right. In infix form, the left operand is the multiplier and the right one the multiplicand.
Vigfus: Still, the first argument of add_v0 is growing, and so the bigger the multiplier, the more additions, no?
Brynja (jumping in): Good point, Vigfus. Multiplying x and y entails x additions, just as adding a and b entails a calls to succ. So multiplying x and y entails 0 + y + 2 * y + 3 * y + ... + (x - 1) * y calls to succ.
Alfrothul: In other words, factoring y on the right, (0 + 1 + 2 + 3 + ... + (x - 1)) * y calls to succ.
Harald: Or again (Gauss to the rescue), ((x - 1) * x / 2) * y calls to succ.
Brynja: In short, a number of calls to succ that is proportional to the product of the square of x and of y.
Harald: Which is not too good.
Alfrothul: Which is why we should rather use the built-in addition function instead of add_v0, I guess. Surely it is implemented more efficiently.
Harald: By that token, we should simply use the built-in multiplication function instead of mul_v0, and then what would we learn?
Vigfus: Maybe we should just swap the arguments of add_v0?
Harald (o_o): Swap the arguments of add_v0.
Vigfus: Well, yes, in the definition of the traced multiplication function:
let traced_mul_v0'' x_given y_given i_given =
let () = Printf.printf "%smul_v0 %s %s ->\n" (indent i_given) (show_int x_given) (show_int y_given) in
let () = assert (x_given >= 0) in
let rec visit x i =
let () = Printf.printf "%svisit_mul_v0 %s ->\n" (indent i) (show_int x) in
let result = if x = 0
then 0
else let x' = pred x
in let ih = visit x' (i + 1)
in traced_add_v0' y_given ih (i + 1) (* <--- here *)
in let () = Printf.printf "%svisit_mul_v0 %s <- %s\n" (indent i) (show_int x) (show_int result) in
result
in let result = visit x_given (i_given + 1)
in let () = Printf.printf "%smul_v0 %s %s <- %s\n" (indent i_given) (show_int x_given) (show_int y_given) (show_int result) in
result;;
After all, addition is commutative.
Vigfus (to Mimer): And now it matters that the multiplicand is non-negative.
Alfrothul (pragmatic): Let me see:
# traced_mul_v0'' 5 2 0;;
mul_v0 5 2 ->
visit_mul_v0 5 ->
visit_mul_v0 4 ->
visit_mul_v0 3 ->
visit_mul_v0 2 ->
visit_mul_v0 1 ->
visit_mul_v0 0 ->
visit_mul_v0 0 <- 0
add_v0 2 0 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 0
visit_add_v0 1 <- 1
visit_add_v0 2 <- 2
add_v0 2 0 <- 2
visit_mul_v0 1 <- 2
add_v0 2 2 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 2
visit_add_v0 1 <- 3
visit_add_v0 2 <- 4
add_v0 2 2 <- 4
visit_mul_v0 2 <- 4
add_v0 2 4 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 4
visit_add_v0 1 <- 5
visit_add_v0 2 <- 6
add_v0 2 4 <- 6
visit_mul_v0 3 <- 6
add_v0 2 6 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 6
visit_add_v0 1 <- 7
visit_add_v0 2 <- 8
add_v0 2 6 <- 8
visit_mul_v0 4 <- 8
add_v0 2 8 ->
visit_add_v0 2 ->
visit_add_v0 1 ->
visit_add_v0 0 ->
visit_add_v0 0 <- 8
visit_add_v0 1 <- 9
visit_add_v0 2 <- 10
add_v0 2 8 <- 10
visit_mul_v0 5 <- 10
mul_v0 5 2 <- 10
- : int = 10
#
Vigfus: See? Now the first argument of add_v0 doesn’t grow.
Brynja: Well done, Vigfus. Now multiplying x and y entails 0 + y + y + y + ... + y, i.e., (x - 1) * y calls to succ.
Vigfus: So, a number of calls to succ that is proportional to x * y instead of to x * x * y. That seems more natural since we are computing the product of x and y.
Harald: So all in all, we should write:
let mul_v3 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then 0
else add_v0 y_given (visit (pred x))
in visit x_given;;
Alfrothul: Or we could just use the built-in addition function:
let mul_v4 x_given y_given =
let () = assert (x_given >= 0)
in let rec visit x =
if x = 0
then 0
else visit (pred x) + y_given
in visit x_given;;
And then whether we write visit (pred x) + y or y + visit (pred x) doesn’t matter.
Vigfus: All these definitions pass the unit test, but running the one for mul_v2 is perceptibly slower:
# test_mul mul_v4;;
- : bool = true
# test_mul mul_v3;;
- : bool = true
# test_mul mul_v2;;
- : bool = true
#
Loki: Plus, we can now call each of traced_mul_v0'' and traced_add_v0' with a negative indentation. That could come handy.
The power function exponentiates its first argument (an integer) with its second (a non-negative integer):
let test_power p =
(* a few handpicked numbers: *)
let b0 = (p 2 0 = 1)
and b1 = (p 2 1 = 2)
and b2 = (p 2 2 = 4)
and b3 = (p 2 3 = 8)
and b4 = (p 2 4 = 16)
and b5 = (p 2 5 = 32)
and b6 = (p 10 2 = 100)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
It is inductively specified as follows. Given an integer x,
(The intuition behind this inductive specification is that x^n = x * (x * (...(x * 1)...)), where x is iteratively multiplied n times, starting with 1, as per Exercise 0 in the lecture note about strings.)
Questions:
Expand and test test_power with an instance of the base case and an instance of the induction step, as in Section Using random numbers to test the factorial function.
You might be tempted to use OCaml’s predefined exponentiation function over floats (**) (together with the conversion functions int_of_float and float_of_int) as a witness implementation, but then beware of its approximations, for they can make unit tests fail unduly) – in other words, using (**) is not necessarily a good idea.
Define a structurally recursive function that embodies the inductive specification above (and that uses mul_v0, mul_v2, or mul_v3):
let power_v0 x n =
...
Does your recursive function pass your unit test? Does your unit-test function provide code coverage?
Can you shield your definition so that it handles being applied to a negative integer as its second argument?
It would be great if you could instrument your implementation with tracing information.
For efficiency, you should use the native multiplication, not your implementation of it, especially if it uses your implementation of addition. Why is that? Can you quantify the computational steps taken by your implementation?
The goal of this section is to write a predicate (i.e., a function that returns a Boolean) computing whether a given natural number is even. Let us start with a unit-test function:
let test_evenp candidate =
(* a few handpicked numbers: *)
let b0 = (candidate 0 = true)
and b1 = (candidate 1 = false)
and b2 = (candidate 2 = true)
and b3 = (candidate 3 = false)
and b4 = (candidate 4 = true)
and b5 = (candidate 5 = false)
and b6 = (candidate 1000 = true)
and b7 = (candidate 1001 = false)
(* testing the completeness of the even predicate: *)
and b8 = (let n = Random.int 1000
in candidate (2 * n) = true)
and b9 = (let n = Random.int 1000
in candidate (2 * n + 1) = false)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 && b9;;
For the sake of sanity, let us test this unit-test function:
# test_evenp (fun n -> n mod 2 = 0);;
- : bool = true
#
For the sake of lucidity, let us write a fake predicate that passes the unit test:
# test_evenp (fun n -> if n < 2001 then n mod 2 = 0 else false);;
- : bool = true
#
Now for the idea. The successor of an even number is odd, i.e., not even, and the successor of an odd number is even. In other words, the evenness of the successor of a number is the negation of the evenness of this number.
Hence the inductive specification of how to test whether a natural number is even:
The unit-test function already contains an instance of the base case, but let us expand it with an instance of the induction step:
let test_evenp candidate =
(* a few handpicked numbers: *)
let b1 = (candidate 1 = false)
and b2 = (candidate 2 = true)
and b3 = (candidate 3 = false)
and b4 = (candidate 4 = true)
and b5 = (candidate 5 = false)
and b6 = (candidate 1000 = true)
and b7 = (candidate 1001 = false)
(* testing the completeness of the even predicate: *)
and b8 = (let n = Random.int 1000
in candidate (2 * n) = true)
and b9 = (let n = Random.int 1000
in candidate (2 * n + 1) = false)
(* an instance of the base case: *)
and bc = (candidate 0 = true)
(* an instance of the induction step: *)
and is = (let n' = Random.int 1000
in candidate (succ n') = not (candidate n'))
(* etc. *)
in b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 && b9 && bc && is;;
Let us express this inductive specification as the declaration of a recursive function:
let evenp_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;;
In the base case, visit should yields true and in the induction step, visit (succ n') should yield the negation of the induction hypothesis:
let evenp_v0 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then true
else let n' = pred n
in let ih = visit n'
in not ih
in visit n_given;;
This implementation is structurally recursive and it passes the unit test, which provides code coverage since it tests both the base case and the induction step:
# test_evenp evenp_v0;;
- : bool = true
#
In the induction step, the let-expressions that declare n' and ih, in the definition of visit, are cosmetic and so we can unfold them:
let evenp_v1 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then true
else not (visit (pred n))
in visit n_given;;
This simplified implementation is still structurally recursive and it passes the unit test:
# test_evenp evenp_v1;;
- : bool = true
#
The accompanying resource file contains a traced version of evenp_v0:
# traced_evenp_v0 5;;
even_v0 5 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- true
visit 1 <- false
visit 2 <- true
visit 3 <- false
visit 4 <- true
visit 5 <- false
even_v0 5 <- false
- : bool = false
# traced_evenp_v0 4;;
even_v0 4 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- true
visit 1 <- false
visit 2 <- true
visit 3 <- false
visit 4 <- true
even_v0 4 <- true
- : bool = true
#
The goal of this section is to write a predicate computing whether a given natural number is odd.
Along the lines of the previous section, specify, implement, and test the oddp predicate.
OCaml provides language support to declare global recursive functions:
Vigfus (falling asleep): Weird stuff, this multiplier and this multiplicand. I wonder if a similar weird stuff happens for addition. Could be funny...
And then the Lord said: go forth, you multipliers and multiplicands, and multiply. And the throng of animals, big and small, scampered away to do just that, except two tiny ones who stayed there, looking up at Him in dismay.
The Lord (kindly): Yes?
The two tiny animals (in dismay): But we can’t multiply – we’re adders.
So the Lord took his mighty axe and chopped down a tree (material cause: wood, and efficient cause: the Lord himself), swiftly assembled a contraption (formal cause), and presented it to them along with its final cause:
The Lord: Here is a table of logs. Now go forth and multiply.
Added a traced version of evenp_v0 in the accompanying resource file [26 Feb 2020]
Clarified the statement of Exercise 7 [17 Feb 2020]
Used more systematically the _given convention as well as pred, and added the food for thought as well as Loki’s closing remark in the aftermath [16 Feb 2020]
Adjusted the tracing to make it more consistent and added the intuition in the solutions for Exercise 6 and Exercise 7 [15 Feb 2020]
Created [14 Feb 2020]