The goal of this lecture note is to document a simple way to introduce recursion, based on the inductive structure of Factorial numbers, by defining a factorial function that maps a natural number to the corresponding factorial number: 0 to 0!, 1 to 1!, 2 to 2!, etc.
let test_fac fac_candidate =
let b0 = (fac_candidate 0 = 1)
and b1 = (fac_candidate 1 = 1)
and b2 = (fac_candidate 2 = 2)
and b3 = (fac_candidate 3 = 6)
and b4 = (fac_candidate 4 = 24)
and b5 = (let n = Random.int 15
in fac_candidate (succ n)
= (succ n) * fac_candidate n)
in b0 && b1 && b2 && b3 && b4 && b5;;
The factorial numbers are defined as follows:
They are remarkable because each of them is defined in terms of the previous one:
In fact, this characterization works even for 1! if we define 0! to be 1:
Mimer: I am asked to compute 5!. Good, 5 is a natural number. Harald, can you give me a hand?
Harald: Sure thing. Let’s see. To compute 5!, I first need to compute 4!. Alfrothul, can you give me a hand?
Alfrothul: Sure thing. Let’s see. To compute 4!, I first need to compute 3!. Brynja, can you give me a hand?
Brynja: Sure thing. Let’s see. To compute 3!, I first need to compute 2!. Vigfus, can you give me a hand?
Vigfus: Sure thing. Let’s see. To compute 2!, I first need to compute 1!. Sigbjørn, can you give me a hand?
Sigbjørn: Sure thing. Let’s see. To compute 1!, I first need to compute 0!. Halcyon, can you give me a hand?
Halcyon: Sure thing. Let’s see. !0 is 1. There you are, Sigbjørn: 0! = 1Sigbjørn: Thanks, Halcyon. Let’s see. 1 * 1 is 1. There you are, Vigfus: 1! = 1
Vigfus: Thanks, Sigbjørn. Let’s see. 2 * 1 is 2. There you are, Brynja: 2! = 2
Brynja: Thanks, Vigfus. Let’s see. 3 * 2 is 6. There you are, Alfrothul: 3! = 6
Alfrothul: Thanks, Brynja. Let’s see. 4 * 6 is 24. There you are, Harald: 4! = 24
Harald: Thanks, Alfrothul. Let’s see. 5 * 24 is 120. There you are, Mimer: 5! = 120
Mimer: Thanks, Harald. Great teamwork, all of you!
Harald: Isn’t it funny how out interaction above can be rendered in OCaml as a series of definitions:
let fac_0 =
1;;
let fac_1 =
1 * fac_0;;
let fac_2 =
2 * fac_1;;
let fac_3 =
3 * fac_2;;
let fac_4 =
4 * fac_3;;
let fac_5 =
5 * fac_4;;
Alfrothul: True that.
Harald: Except for the first definition, all the other ones are strikingly similar: the index of each name is the multiplier, and the multiplicand is the previous factorial number.
Alfrothul: It is extremely tempting to parameterize this series of definitions with the index and conflate it into one single definition:
let fac n =
n * fac (pred n);;
Harald: Wow. You are defining fac in terms of itself.
Alfrothul: Yup. It’s a recursive definition. And to make it work, we just need to add rec to the definition, I peeked ahead to the next lecture note:
let rec fac n =
n * fac (pred n);;
Harald: I understand the principle of using recursion in OCaml before we have been explained how recursion works in OCaml, but wait. This can’t possibly work: sooner or later fac will be called with 0 and then it should stop. This implementation, however, doesn’t.
Alfrothul: Right. Let’s intercept this case with a conditional expression:
let rec fac n =
if n = 0
then 1
else n * fac (pred n);;
Harald: Hum. OCaml accepts this definition, and the unit tests are passed too:
# test_fac fac;;
- : bool = true
#
Brynja: But what if fac is called with a negative integer?
Harald: We could add an assertion:
let rec fac n =
let () = assert (n >= 0)
in if n = 0
then 1
else n * fac (pred n);;
Brynja: And verify that this assertion holds each time fac is called?
Alfrothul: Right. We should only do that at the outset, and only test once whether the given argument is not negative. Let me declare the recursive function locally, so that nobody else can call it:
let fac n_given =
let () = assert (n_given >= 0)
in let rec countdown n =
if n = 0
then 1
else n * countdown (pred n)
in countdown n_given;;
Harald: Well, the name countdown fits.
Mimer: And guess what – the accompanying resource file contains a traced version of fac. Look at it in action:
# traced_fac 5;;
fac 5 ->
countdown 5 ->
countdown 4 ->
countdown 3 ->
countdown 2 ->
countdown 1 ->
countdown 0 ->
countdown 0 <- 1
countdown 1 <- 1
countdown 2 <- 2
countdown 3 <- 6
countdown 4 <- 24
countdown 5 <- 120
fac 5 <- 120
- : int = 120
#
Brynja: This trace is rendering our earlier interaction, doesn’t it? You are fac, and each of the rest of us is an instance of countdown.
Mimer: Yup.
Fixed a hyperlink, thanks to Matthias Ephraim Goh Wei Zheng’s eagle eye [06 Mar 2020]
Polished the narrative and indented the teamwork [15 Feb 2020]
Fixed a typo in the definition of fac_5, thanks to Chau Nguyen’s eagle eye [14 Feb 2020]
Created [14 Feb 2020]