Mathematics for Computer Science

Chapter 7 Recursive Data Types162

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:

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 7.1.5.

Base case: #c./WWD 0.

Constructor case:

#c.ha;si/WWD

(

#c.s/ ifa¤c;

1 C#c.s/ ifaDc: