6.1. Recursive Definitions and Structural Induction 175
Definition 6.1.3.Theconcatenationstof the stringss;t 2 Ais defined recur-
sively based on the definition ofs 2 A:
Base case:
tWWDt:
Constructor case:
ha;sitWWDha;sti:
6.1.1 Structural Induction
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 6.1.4.For alls;t 2 A,
jstjDjsjCjtj:Proof. By structural induction on the definition ofs 2 A. The induction hypoth-
esis is
P.s/WWD 8t 2 A:jstjDjsjCjtj:
Base case(sD):
jstjDjtj
Djtj (def, base case)
D 0 Cjtj
DjsjCjtj (def length, base case)