Chapter 6 Recursive Data Types194
Definition. Base case: The LBThl;leafihasunique labels.
Constructor case: IfBandCare LBT’s with unique labels, no label ofBis a
labelCand vice-versa, andlis not a label ofBorC, thenhl;B;Cihasunique
labels.
IfBis an LBT, letnBbe the number of distinct internal-labels appearing inB
andfBbe the number of distinct leaflabels ofB. Prove by structural induction
that
fBDnBC 1 (6.25)
for all LBT’sBwith unique labels. This equation can obviously fail if labels are
not unique, so your proof had better use uniqueness of labels at some point; be sure
to indicate where.
Exam Problems
Problem 6.10.
The Arithmetic Trig Functions (Atrig’s) are the set of functions of one real variable
defined recursively as follows:
Base cases:
The identity function, id.x/WWDxis anAtrig, any constant function is anAtrig, the sine function is anAtrig,Constructor cases:
Iff;gareAtrig’s, then so are1.fCg2.fg- the compositionfıg.
Prove by structural induction on this definition that iff.x/is anAtrig, then so is
f^0 WWDdf=dx.
Problem 6.11.