Psst: The paper, Inductive Graphs and Functional Graph Algorithms, I shared near the end of this post illustrates why inductive specification is so useful to functional programming.
Another way to write an inductive specification is by using a bottomup definition.
For e.g. the set S
from here can be defined using a bottomup inductive specification as follows:
S
is the smallest set contained in ℕ
that satisfies the following properties:

0 ∊ S
, and  If
n ∊ S
thenn + 5 ∊ S
.
We have to say that "S
is the smallest" to ensure that S
is uniquely defined.
We can use this definition to generate natural numbers that are in S
. By definition, 0 ∊ S
and by condition 2 it follows that 0 + 5 = 5 ∊ S
. By repeatedly applying condition 2 we can see that all multiples of 5 are in S
.
Why bother?
For the same reasons as before.
Also, bottomup definitions in particular can be used to generate the values of the set.
As another example, here's a bottomup inductive specification for the set, L
, of all lists of natural numbers:

[] ∊ L
,  If
n ∊ ℕ
andl ∊ L
thenn :: l ∊ L
,  Nothing else is in
L
.
N.B. Condition 3 is another way of saying that L
is the smallest such set.
What's neat about this is that from a bottomup definition we can use an algebraic data type to represent the values of the set.
type List a
= Empty  condition 1
 Cons a (List a)  condition 2
 condition 3 is implicit
Then, many functions on lists can be succinctly given by recursive function definitions.
In Inductive Graphs and Functional Graph Algorithms, Martin Erwig views graphs as inductively defined data types and then proceeds to show how the graphs can be implemented efficiently and how graph algorithms can be succinctly given by recursive function definitions.
Challenge
Write a bottomup inductive specification for the set S = {2n + 3m + 1  n, m ∊ ℕ}
.
N.B. This post is based on my EoPL notes for Chapter 1.
Discussion (0)