The goal of this lecture note is to review structural induction and structural recursion over Peano numbers and to illustrate them with a series of examples.
Back in Week 02, in the chapter about characterizing languages with grammars, we saw that making a grammar self-referential makes it possible to finitely describe arbitrarily large data. Here, natural numbers are described with such a self-referential grammar:
n ::= 0 | succ n
In words, a natural number is either zero or it is the successor of another natural number, a grammar due to Giuseppe Peano. This grammar is sound and complete:
Sound: The result of using the two constructors 0 and succ always gives the representation of a natural number.
Complete: Any natural number can be represented using these two constructors.
The principle of mathematical induction exploits this sound and complete grammar by indexing a property with a Peano number. It states that
(1, base case) if this property holds for 0 and
(2, induction step) for any natural number i', if this property holds for i', then it holds for succ i',
then this property holds for any natural number.
This principle is stated as an inference rule, with the assumptions (1) and (2) as premises and the consequent as conclusion:
P(O) for any natural number i', P(i') => P(succ i')
MATHEMATICAL_INDUCTION ------------------------------------------------------
for any natural number n, P(n)
Mimer (with a straight face): There is a thin line between assumptions and conclusion.
Loki (ditto): A dashed line, you mean?
Mimer: Ah. Hum. No. The dashed line is an artifact of the ASCII layout. Here is the real thing:
| MATHEMATICAL_INDUCTION | P(O) | for any natural number i', P(i') => P(succ i') | |
| for any natural number n, P(n) | |||
Mimer: Better?
Loki: Yup.
Halcyon (whispering to Bong-sun): I think Mimer was making a pun.
Bong-sun (whispering back): I think so too.
Mimer: Ahem. Be that as it may, in the induction step, P(i') is the induction hypothesis. And to sum up, a self-referential grammar makes it possible to finitely describe arbitrarily large data. Such a grammar gives rise to a principle of structural induction – structural because it follows the grammatical structure of the data.
The programming counterpart of structural induction is structural recursion: A structurally recursive program makes it possible to finitely describe how to process arbitrarily large data when these data were constructed inductively. Here is the skeleton of such a structurally recursive program for Peano numbers:
let ... n =
let () = assert (n >= 0) in
let rec p i =
if i = 0
then ...
else let i' = pred i
in let ih = p i'
in ...ih...
in p n;;
In this skeleton,
In practice, the name visit is used instead of p – though any other name would do too.
And without syntactic sugar, this structurally recursive skeleton reads:
let ... n =
let () = assert (n >= 0) in
let rec p = fun i ->
if i = 0
then ...
else let i' = pred i
in let ih = p i'
in ...ih...
in p n;;
So when an instance of this recursive skeleton is used to declare a function foo (giving it the name foo) in the global environment Gv, applying foo, e.g., to 3 (represented as 3) reduces to evaluating:
let () = assert (n >= 0) in
let rec p = fun i ->
if i = 0
then ...
else let i' = pred i
in let ih = p i'
in ...ih...
in p n;;
in an extension of Gv where n denotes 3, i.e., in (n = 3, Gv). The definiens of the outer let-expression (i.e., the assertion) is evaluated in this extended environment, and since 3 is non-negative, the result is (). Evaluating the outer let-expression then reduces to evaluating the local let-rec expression in the same extended environment since this outer let-extended declares no names. Evaluating this let-rec expression reduces to evaluating p n in an extension of (n = 3, Gv) where p denotes a recursive function. Evaluating this application reduces to applying the recursive function denoted by p to 3. Applying this recursive function to 3 reduces to evaluating:
if i = 0
then ...
else let i' = pred i
in let ih = p i'
in ...ih...
in an environment where i denotes 3 and p denotes the recursive function.
Let us revisit OCaml function that, given a non-negative integer, doubles it up. We start with a unit-test function, which we first test:
let test_twice candidate =
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 2)
and b2 = (candidate 2 = 4)
and b3 = (candidate 3 = 6)
and b4 = (let n = Random.int 10000
in candidate n = 2 * n)
(* etc. *)
in b0 && b1 && b2 && b3 && b4;;
let () = assert (test_twice (fun n -> 2 * n) = true);;
Here is an inductive specification of how to double up a natural number:
In effect, each occurrence of succ (...) in the input is mapped homomorphically to succ (succ (...)), and the occurrence of 0 is mapped to 0.
Let us fill the structurally recursive skeleton with the pertinent information, i.e., the name twice, what should be returned in the base case (i.e., 0), and what should be returned in the induction step (i.e., the successor of the successor of the result of the recursive call):
let twice 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 (succ ih)
in visit n;;
A traced version of this implementation makes it possible to visualize a call to twice, the initial call to visit, and its subsequent recursive calls and returns:
# traced_twice 3;;
twice 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 0
visit 1 <- 2
visit 2 <- 4
visit 3 <- 6
twice 3 <- 6
- : int = 6
#
In this scenario, the given non-negative integer is 3, which was inductively constructed as succ (succ (succ 0)). So visit recursively peels off each of these successors until it reaches 0, at which point it returns 0, as per the base case. And then, as per the induction step, it adds 2 to each intermediate result, and the result is 6, which is the doubled version of 3.
Pablito: But...
Mimer: Yes, Pablito?
Pablito: How does the program processor know where to successively return the intermediate results?
Mimer: Good point, Pablito. The same question arise for evaluating, e.g., succ (succ (succ 0)), no?
Pablito: Not really, because each call to succ is distinct, whereas for a recursive function, it’s the same recursive call.
Mimer: That is because thanks to the rec keyword, the implementation of twice is finite. Without it, it would be arbitrarily large. Let me sketch this implementation so that its growth is visible:
let twice n0 =
let () = assert (n0 >= 0) in
if n0 = 0
then 0
else let n1 = pred n0
in let ih = ...
in succ (succ ih);;
let twice n0 =
let () = assert (n0 >= 0) in
if n0 = 0
then 0
else let n1 = pred n0
in let ih = if n1 = 0
then 0
else let n2 = pred n1
in let ih = ...
in succ (succ ih)
in succ (succ ih);;
let twice n0 =
let () = assert (n0 >= 0) in
if n0 = 0
then 0
else let n1 = pred n0
in let ih = if n1 = 0
then 0
else let n2 = pred n1
in let ih = if n2 = 0
then 0
else let n3 = pred n2
in let ih = ...
in succ (succ ih)
in succ (succ ih)
in succ (succ ih);;
let twice n0 =
let () = assert (n0 >= 0) in
if n0 = 0
then 0
else let n1 = pred n0
in let ih = if n1 = 0
then 0
else let n2 = pred n1
in let ih = if n2 = 0
then 0
else let n3 = pred n2
in let ih = if n3 = 0
then 0
else let n4 = pred n3
in let ih = ...
in succ (succ ih)
in succ (succ ih)
in succ (succ ih)
in succ (succ ih);;
Mimer: See? There is no recursive function here to account for a given integer that is arbitrarily large – there is an arbitrarily large program instead.
Alfrothul: Pablito’s question still stands: we have a finite recursive program, not an arbitrarily large one, and each recursive call yields an intermediate result. I can see that running a sufficiently large program and running the recursive program will carry out the same tests, the same decrements, and the same double increments in the same order, but how does the program processor know where to return the intermediate results when running the recursive program?
Mimer: The program processor runs the recursive program by simulating the arbitrarily large program, making it grow on demand, as it were. And if the program processor needs to remember where to return an intermediate result, well, it gives it a name and subsequently it uses this name.
Loki: You mean the program processor uses the computer memory to remember things?
Mimer: That’s kind of simplistic, and un-Aristotelian too, since we are describing OCaml in a computer-agnostic way.
Bob Harper: Right. You are describing what recursion is without explaining it in terms of how it is implemented. I approve that.
Mimer (surprised): Thank you. And Prof. Harper, thanks for passing by! Huh, mind autographing my copy of your foundational book about programming languages?
Bob Harper (graciously): By all means.
Mimer: Thank you. But back to you, Pablito and Alfrothul. As illustrated below, each recursive call implements an instance of the induction step, so all the program processor does is keeping track of these instances, and how it does that is as irrelevant as how it treats if-expressions and let-expressions. Not that this “how” is uninteresting: implementing program processors – be them parsers, interpreters, compilers, or partial evaluators – provides wonderful first-hand insights about computing, but that is not what we are doing here. So let’s try to not dance faster than the music, shall we?
The following box represents the base case – evaluating visit 0 yields 0:
+--------------+
| visit 0 -> |
| visit 0 <- 0 |
+--------------+
Given the following box to represent the induction hypothesis – evaluating visit i' yields ih:
+----------------+
| visit i' -> |
| visit i' <- ih |
+----------------+
the following new box represents an induction step – if evaluating visit i' yields ih then evaluating visit (succ i') yields succ (succ ih):
+-----------------------------------+
| visit (succ i') -> |
| +----------------+ |
| | visit i' -> | |
| | visit i' <- ih | |
| +----------------+ |
| visit (succ i') <- succ (succ ih) |
+-----------------------------------+
So overall, the trace induced by evaluating twice 3 is structured like an onion:
twice 3 ->
+------------------------------------------------+
| visit 3 -> |
| +--------------------------------------------+ |
| | visit 2 -> | |
| | +----------------------------------------+ | |
| | | visit 1 -> | | |
| | | +--------------+ | | |
| | | | visit 0 -> | | | |
| | | | visit 0 <- 0 | | | |
| | | +--------------+ | | |
| | | visit 1 <- 2 (* i.e., succ (succ 0) *) | | |
| | +----------------------------------------+ | |
| | visit 2 <- 4 (* i.e., succ (succ 2) *) | |
| +--------------------------------------------+ |
| visit 3 <- 6 (* i.e., succ (succ 4) *) |
+------------------------------------------------+
twice 3 <- 6
Let us analyze this onion inside out:
A recursive computation constructs the boxes outside in (the calls) and completes them inside out (the returns) once it has reached the base case.
The same story holds for the even predicate over natural numbers, which is specified inductively as follows:
In effect, each occurrence of succ (...) in the input is mapped homomorphically to not (...), and the occurrence of 0 is mapped to true.
Let us fill the structurally recursive skeleton with the pertinent information, i.e., the name evenp, what should be returned in the base case (i.e., true), and what should be returned in the induction step (i.e., the negation of the result of the recursive call):
let evenp n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then true
else let i' = pred i
in let ih = visit i'
in not ih
in visit n;;
A traced version of this implementation makes it possible to visualize a call to evenp, the initial call to visit, and its subsequent recursive calls and returns:
# traced_evenp 3;;
evenp 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- true
visit 1 <- false
visit 2 <- true
visit 3 <- false
evenp 3 <- false
- : bool = false
#
In this scenario, the given non-negative integer is 3, which was inductively constructed as succ (succ (succ 0)). So visit recursively peels off each of these successors until it reaches 0, at which point it returns true, as per the base case. And then, as per the induction step, it negates each intermediate result, and the result is false, reflecting that 3 is not even.
The following box represents the base case – evaluating visit 0 yields true:
+-----------------+
| visit 0 -> |
| visit 0 <- true |
+-----------------+
Given the following box to represent the induction hypothesis – evaluating visit i' yields ih:
+----------------+
| visit i' -> |
| visit i' <- ih |
+----------------+
the following new box represents an induction step – if evaluating visit i' yields ih then evaluating visit (succ i') yields not ih:
+---------------------------+
| visit (succ i') -> |
| +----------------+ |
| | visit i' -> | |
| | visit i' <- ih | |
| +----------------+ |
| visit (succ i') <- not ih |
+---------------------------+
So overall, the trace induced by evaluating evenp 3 is structured like an onion:
evenp 3 ->
+-----------------------------------------------+
| visit 3 -> |
| +-------------------------------------------+ |
| | visit 2 -> | |
| | +---------------------------------------+ | |
| | | visit 1 -> | | |
| | | +-----------------+ | | |
| | | | visit 0 -> | | | |
| | | | visit 0 <- true | | | |
| | | +-----------------+ | | |
| | | visit 1 <- false (* i.e., not true *) | | |
| | +---------------------------------------+ | |
| | visit 2 <- true (* i.e., not false *) | |
| +-------------------------------------------+ |
| visit 3 <- false (* i.e., not true *) |
+-----------------------------------------------+
evenp 3 <- false
Let us analyze this onion inside out:
A recursive computation constructs the boxes outside in (the calls) and completes them inside out (the returns) once it has reached the base case.
The elephant: It’s the same onion, right?Mimer: Yup.
The same story holds for the Factorial function, which is specified inductively as follows:
In effect, each ith occurrence of succ (...) in the input is mapped homomorphically to i * ..., where i represents i, and the occurrence of 0 is mapped to 1. (In succ (succ 0), the first occurrence of succ is the inner one (succ 0 represents 1) and the second occurrence of succ is the outer one (succ (succ 0) represents 2).
Let us fill the structurally recursive skeleton with the pertinent information, i.e., the name fac, what should be returned in the base case (i.e., 1), and what should be returned in the induction step (i.e., the product of the integer denoted by i and the result of the recursive call):
let fac 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;;
A traced version of this implementation makes it possible to visualize a call to fac, the initial call to visit, and its subsequent recursive calls and returns:
# traced_fac 3;;
fac 3 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- 1
visit 1 <- 1
visit 2 <- 2
visit 3 <- 6
fac 3 <- 6
- : int = 6
#
In this scenario, the given non-negative integer is 3, which was inductively constructed as succ (succ (succ 0)). So visit recursively peels off each of these successors until it reaches 0, at which point it returns 1, as per the base case. And then, as per the induction step, it multiplies each intermediate result by the argument of visit, and the result is 6, which is the Factorial number of 3.
The following box represents the base case – evaluating visit 0 yields 1:
+--------------+
| visit 0 -> |
| visit 0 <- 1 |
+--------------+
Given the following box to represent the induction hypothesis – evaluating visit i' yields ih:
+----------------+
| visit i' -> |
| visit i' <- ih |
+----------------+
the following new box represents an induction step – if evaluating visit i' yields ih then evaluating visit (succ i') yields succ i' * ih:
+---------------------------------+
| visit (succ i') -> |
| +----------------+ |
| | visit i' -> | |
| | visit i' <- ih | |
| +----------------+ |
| visit (succ i') <- succ i' * ih |
+---------------------------------+
So overall, the trace induced by evaluating fac 3 is structured like an onion:
fac 3 ->
+----------------------------------------+
| visit 3 -> |
| +------------------------------------+ |
| | visit 2 -> | |
| | +--------------------------------+ | |
| | | visit 1 -> | | |
| | | +--------------+ | | |
| | | | visit 0 -> | | | |
| | | | visit 0 <- 1 | | | |
| | | +--------------+ | | |
| | | visit 1 <- 1 (* i.e., 1 * 1 *) | | |
| | +--------------------------------+ | |
| | visit 2 <- 2 (* i.e., 2 * 1 *) | |
| +------------------------------------+ |
| visit 3 <- 6 (* i.e., 3 * 2 *) |
+----------------------------------------+
fac 3 <- 6
Let us analyze this onion inside out:
A recursive computation constructs the boxes outside in (the calls) and completes them inside out (the returns) once it has reached the base case.
Pablito: It’s the same onion, right?The elephant: Yup.
Implement an OCaml function named string_minchar that, given a nonempty string, yields its smallest character.
Pablito: Let’s start with a unit-test function:
let test_string_minchar candidate =
let b0 = (candidate "0" = '0')
and b1 = (candidate "01" = '0')
and b2 = (candidate "10" = '0')
and b3 = (candidate "012" = '0')
and b4 = (candidate "102" = '0')
and b5 = (candidate "120" = '0')
in b0 && b1 && b2 && b3 && b4 && b5;;
Dana: Thanks, Pablito.
Anton: Since string_minchar expects a nonempty string, we can take care of that at the outset:
let string_minchar_v0 s =
let () = assert (s <> "") in
...
Alfrothul: Wait. Clearly we are going to specify string_minchar by induction on its length, so we might as well compute this length at the outset:
let string_minchar_v1 s =
let n = String.length s
in let () = assert (n > 0) in
...
Anton: Fair enough. In the induction step, we are going to use OCaml’s min function:
# min;;
- : 'a -> 'a -> 'a = <fun>
# min 'a' 'b';;
- : char = 'a'
#
Alfrothul: Yup. And the induction is on the length of the given string, i.e., on successive prefixes of this string: the prefix of length 0, and then of length 1, etc.
Anton: Yup:
let string_minchar_v1 s =
let n = String.length s
in let () = assert (n > 0) in
let rec visit i =
if i = 0
then ...
else let i' = pred i
in let ih = visit i'
in min (String.get s i') ih
in visit n;;
Alfrothul: Now about the base case...
Anton: Well, the string is nonempty, and so its length cannot be 0. Harrumph.
Alfrothul: By extension, we could put the neutral element of min, as illustrated in Exercise 12 last week.
Anton: Right, we also talked about that in our romp about polynomials.
Pablito: So what is the neutral element of min?
Alfrothul: Let’s name it e (represented as e). For any x (represented as x), evaluating min x e and evaluating min e x should yield x. So e needs to be the largest element. Ugh.
Dana (mildly): We are comparing characters here.
Alfrothul: Ah, right. And since there are 256 characters in OCaml, there is a largest one.
Halcyon (suavely): The largest character is '\255'.
Dana: Thanks, Halcyon. Here we go:
Anton: Okeedokee:
let string_minchar_v1 s =
let n = String.length s
in let () = assert (n > 0) in
let rec visit i =
if i = 0
then '\255'
else let i' = pred i
in let ih = visit i'
in min (String.get s i') ih
in visit n;;
Pablito: Let me check, let me check:
# test_string_minchar string_minchar_v1;;
- : bool = true
#
Alfrothul <clickety clickety clickety click>: OK, let’s visualize the computation with a trace:
# traced_string_minchar_v1 "xyzcbaa";;
string_minchar_v1 "xyzcbaa" ->
visit 7 ->
visit 6 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- '\255'
visit 1 <- 'x'
visit 2 <- 'x'
visit 3 <- 'x'
visit 4 <- 'c'
visit 5 <- 'b'
visit 6 <- 'a'
visit 7 <- 'a'
string_minchar_v1 "xyzcbaa" <- 'a'
- : char = 'a'
#
Dana: Right. The trace shows how in the base case, the largest representable character is returned, and then the least of 'x' and this largest character, and then the least of 'x' and the result, and then the least of 'x' and the result, and then the least of 'c' and the result, and then the least of 'b' and the result, and then the least of 'a' and the result, and then the least of 'a' and the result, as the string is indexed from 0 to 6, since its length is 7.
The onion: It’s the same elephant, right?The elephant: I was going to say that.The onion: You’re welcome.The elephant: Well, almost that.The onion: You’re welcome.The elephant: Ugh, a talking onion.The onion: You’re welcome.The elephant: Ah, right, more layers.The onion: You’re welcome.
Implement an OCaml function named string_maxchar that, given a nonempty string, yields its largest character.
Implement an OCaml function named string_minmaxchar that, given a nonempty string, yields its smallest character and its largest character.
Replaced the occurrence of != with <> since we are considering structural equality [10 Mar 2023]
Added the accompanying .ml file after the live-coding session in class [17 Feb 2023]
Expanded the narrative of the section about structural recursion [17 Feb 2023]
Split the first section into two (Structural induction and Structural recursion) and sandwiched the express interlude inbetween [16 Feb 2023]
Added Exercise 01, Exercise 02, and Exercise 03 [13 Feb 2023]
Created [18 Sep 2022]