Inductive specification using a top-down definition

Inductive specification is a powerful method for specifying a set of values.

And, a top-down 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 top-down inductive specification as follows:

A natural number n is in S if and only if:

1. n = 0, or
2. 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:

1. Prove properties about the set of values or structures.
2. Write functions that manipulate them.

Top-down 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 (n-5)
  else
    False

Challenge

Write a top-down inductive specification for the set S = {2n + 3m + 1 | n, m ∊ ℕ}.

N.B. This post is based on my EoPL notes for Chapter 1.