6.1: Recursive Definitions and Structural Induction

We’ll start off illustrating recursive definitions and proofs using the example of character strings. Normally we’d take strings of characters for granted, but it’s informative to treat them as a recursive data type. In particular, strings are a nice first example because you will see recursive definitions of things that are easy to understand or that you already know, so you can focus on how the definitions work without having to figure out what they are for.

Definitions of recursive data types have two parts:

• Base case(s) specifying that some known mathematical elements are in the data type, and
• Constructor case(s) that specify how to construct new data elements from previously constructed elements or from base elements.

The definition of strings over a given character set, \(A\), follows this pattern:

Definition \(\PageIndex{1}\)

Let \(A\) be a nonempty set called an alphabet, whose elements are referred to as characters, letters, or symbols. The recursive data type, \(A^*\), of strings over alphabet, \(A\), are defined as follows:

• Base case: the empty string, \(\lambda\), is in \(A^*\).
• Constructor case: If \(a \in A\) and \(s \in A^*\), then the pair \(\langle a, s \rangle \in A^*\).

So \(\{0, 1\}^*\) are the binary strings.

The usual way to treat binary strings is as sequences of 0’s and 1’s. For example, we have identified the length-4 binary string 1011 as a sequence of bits, the 4-tuple (1, 0, 1, 1). But according to the recursive Definition 6.1.1, this string would be represented by nested pairs, namely

\[\nonumber \langle 1, \langle 0, \langle 1, \langle 1, \lambda \rangle \rangle \rangle \rangle.\]

These nested pairs are definitely cumbersome and may also seem bizarre, but they actually reflect the way that such lists of characters would be represented in programming languages like Scheme or Python, where \(\langle a, s \rangle\) would correspond to cons \((a, s)\).

Notice that we haven’t said exactly how the empty string is represented. It really doesn’t matter, as long as we can recognize the empty string and not confuse it with any nonempty string.

Continuing the recursive approach, let’s define the length of a string.

Definition \(\PageIndex{2}\)

The length, \(|s|\), of a string, \(s\), is defined recursively based on the definition of \(s \in A^*\):

Base case: \(| \lambda | ::= 0.\)

Constructor case: \(| \langle a, s \rangle| ::= 1 + |s|.\)

This definition of length follows a standard pattern: functions on recursive data types can be defined recursively using the same cases as the data type definition. Specifically, to define a function, \(f\), on a recursive data type, define the value of \(f\) for the base cases of the data type definition, then define the value of \(f\) in each constructor case in terms of the values of \(f\) on the component data items.

Let’s do another example: the concatenation \(s \cdot t\) of the strings \(s\) and \(t\) is the string consisting of the letters of \(s\) followed by the letters of \(t\). This is a perfectly clear mathematical definition of concatenation (except maybe for what to do with the empty string), and in terms of Scheme/Python lists, \(s \cdot t\) would be the list append (s, t). Here’s a recursive definition of concatenation.

Definition \(\PageIndex{3}\)

The concatenation \(s \cdot t\) of the strings \(s, t \in A^*\) is defined recursively based on the definition of \(s \in A^*\).

Base case:

\[\nonumber \lambda \cdot t ::= t.\]

Constructor case:

\[\nonumber \langle a, s \rangle \cdot t ::= \langle a, s \cdot t \rangle.\]

Structural Induction

Structural induction is a method for proving that all the elements of a recursively defined data type have some property. A structural induction proof has two parts corresponding to the recursive definition:

• Prove that each base case element has the property.
• Prove that each constructor case element has the property, when the constructor is applied to elements that have the property.

For example, we can verify the familiar fact that the length of the concatenation of two strings is the sum of their lengths using structural induction:

Theorem \(\PageIndex{4}\)

For all \(s, t \in A^*\),

\[\nonumber |s \cdot t| = |s| + |t|.\]

Proof

By structural induction on the definition of \(s \in A^*\). The induction hypothesis is

\[\nonumber P(s) ::= \forall t \in A^*. |s \cdot t| = |s| + |t|.\]

Base case (\(s = \lambda\)):

\[\begin{aligned}
|s \cdot t| &=|\lambda \cdot t| &  \\
&=|t| & (\text { def } \cdot, \text { base case}) \\
&=0+|t| &  \\
&=|s|+|t| &  \text { (def length, base case) }
\end{aligned}\]

Constructor case: Suppose \(s ::= \langle a, r \rangle\) and assume the induction hypothesis, \(P(r)\). We must show that \(P(s)\) holds:

\[\begin{aligned} |s \cdot t| &=|\langle a, r \rangle \cdot t| & \\ &=|\langle a, r \cdot t \rangle| & (\text {concat def, constructor case}) \\ &=1+|r \cdot t| & (\text {length def, constructor case})\\ &=|1 + (|r| + |t|) & (\text {since } P(r) \text{ holds})\\ &=(1+|r|)+|t| & \\ &= |\langle a, r \rangle| + |t| & & \text{(length def, constructor case)} \\ &= |s| + |t|. \end{aligned}\]

This proves that \(P(s)\) holds as required, completing the constructor case. By structural induction we conclude that \(P(s)\) holds for all strings \(s \in A^*\). \(\quad \blacksquare\)

This proof illustrates the general principle:

The Principle of Structural Induction.

Let \(P\) be a predicate on a recursively defined data type \(R\). If

• \(P(b)\) is true for each base case element, \(b \in R\), and
• for all two-argument constructors, \(\textbf{c}\),

\[\nonumber |P(r) \text{ AND } P(s)| \text{ IMPLIES } P(\textbf{c}(r, s))\]

for all \(r, s \in R\),

and likewise for all constructors taking other numbers of arguments, then

\[\nonumber P(r) \text{ is true for all } r \in R.\]

One More Thing

The number, \(\#_c (s)\), of occurrences of the character \(c \in A\) in the string \(s\) has a simple recursive definition based on the definition of \(s \in A^*:\)

Definition \(\PageIndex{5}\)

Base case: \(\#_{c} (\lambda) ::= 0\).

Constructor case:

\[\nonumber \#_{c}(\langle a, s\rangle)::=\Big\{\begin{array}{ll}
\#_{c}(s) & \text { if } a \neq c \\
1+\#_{c}(s) & \text { if } a=c
\end{array}\]

We'll need the following lemma in the next section:

\[\nonumber \#_{c}(s \cdot t)=\#_{c}(s)+\#_{c}(t)\]

The easy proof by structural induction is an exercise (Problem 6.7).