Inductive specification using a topdown definition
Dwayne Crooks ・2 min read
Inductive specification is a powerful method for specifying a set of values.
And, a topdown definition is one way to write an inductive specification.
For e.g.
Given the set consisting of multiples of 5, i.e. S = { 5n  n ∊ ℕ }
we can define S
alternatively using a topdown inductive specification as follows:
A natural number n
is in S
if and only if:

n = 0
, or 
n  5 ∊ S
.
We can use this definition to determine what natural numbers are in S
. 0 ∊ S
by condition 1. 5 ∊ S
since 5  5 = 0 ∊ S
by condition 2. 10 ∊ S
since 10  5 = 5 ∊ S
by condition 2. And so on.
What about 3? Is 3 in S
?
We know that 3 ≠ 0
, so condition 1 is not satisfied. Furthermore, 3  5 = 2
, which is not a natural number and so is not a member of S
. Therefore, condition 2 is not satisfied. Since 3 satisfies neither condition, 3 ∉ S
.
Can you see why 8 is not a member of S
?
Can you see why only the multiples of 5 are members of S
?
Why bother?
Many discrete structures in Computer Science, lists, binary trees, lambda calculus expressions, regular expressions and much more, can be defined using an inductive specification.
Inductive specifications allow us to:
 Prove properties about the set of values or structures.
 Write functions that manipulate them.
Topdown definitions in particular can be used to test for inclusion in the set of values.
For e.g. the above specification for S
can be used to write the following predicate:
inS : Int > Bool
inS =
if n == 0 then
True
else if n >= 5 then
inS (n5)
else
False
Challenge
Write a topdown inductive specification for the set S = {2n + 3m + 1  n, m ∊ ℕ}
.
N.B. This post is based on my EoPL notes for Chapter 1.