Inductive specification using a bottom-up definition

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 bottom-up definition.

For e.g. the set S from here can be defined using a bottom-up inductive specification as follows:

S is the smallest set contained in ℕ that satisfies the following properties:

1. 0 ∊ S, and
2. If n ∊ S then n + 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, bottom-up definitions in particular can be used to generate the values of the set.

As another example, here's a bottom-up inductive specification for the set, L, of all lists of natural numbers:

1. [] ∊ L,
2. If n ∊ ℕ and l ∊ L then n :: l ∊ L,
3. 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 bottom-up 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 bottom-up inductive specification for the set S = {2n + 3m + 1 | n, m ∊ ℕ}.

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