Mathematics for Computer Science

Chapter 6 Recursive Data Types176

Constructor case: SupposesWWDha;riand assume the induction hypothesis,P.r/.
We must show thatP.s/holds:

js
tjDjha;ri
tj

Djha;r
tij (concat def, constructor case)

D 1 Cjr
tj (length def, constructor case)

D 1 C.jrjCjtj/ sinceP.r/holds

D.1Cjrj/Cjtj

Djha;rijCjtj (length def, constructor case)

DjsjCjtj:

This proves thatP.s/holds as required, completing the constructor case. By struc-
tural induction we conclude thatP.s/holds for all stringss 2 A. 

This proof illustrates the general principle:

The Principle of Structural Induction.

LetPbe a predicate on a recursively defined data typeR. If

 P.b/is true for each base case element,b 2 R, and

 for all two-argument constructors,c,

ŒP.r/ANDP.s/çIMPLIESP.c.r;s//

for allr;s 2 R,

and likewise for all constructors taking other numbers of arguments,

then

P.r/is true for allr 2 R:

6.1.2 One More Thing

The number, #c.s/, of occurrences of the characterc 2 Ain the stringshas a
simple recursive definition based on the definition ofs 2 A:

Definition 6.1.5.

Base case: #c./WWD 0.