Mathematics for Computer Science

7.1. Recursive Definitions and Structural Induction 161

Definition 7.1.3.Theconcatenations
tof the stringss;t 2 Ais defined recur-
sively based on the definition ofs 2 A:

Base case:

tWWDt:

Constructor case:
ha;si
tWWDha;s
ti:

Structural inductionis 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 construc-

tor 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 7.1.4.For alls;t 2 A,

js
tjDjsjCjtj:

Proof. By structural induction on the definition ofs 2 A. The induction hypoth-
esis is
P.s/WWD 8t 2 A:js
tjDjsjCjtj:

Base case(sD):

js
tjDj
tj

Djtj (def
, base case)

D 0 Cjtj

DjsjCjtj (def length, base case)

Constructor case: SupposesWWDha;riand assume the induction hypothesis,P.r/.