Chapter 6 Recursive Data Types180
Definition 6.2.2.Define the set, AmbRecMatchf];[grecursively as follows:
Base case: 2 AmbRecMatch,
Constructor cases: ifs;t 2 AmbRecMatch, then the strings[s]andstare
also in AmbRecMatch.
It’s pretty easy to see that the definition of AmbRecMatch is just another way
to define RecMatch, that is AmbRecMatchDRecMatch (see Problem 6.15). The
definition of AmbRecMatch is arguably easier to understand, but we didn’t use it
because it’s ambiguous, while the trickier definition of RecMatch is unambiguous.
Here’s why this matters. Let’s define the number of operations,f.s/, to construct
a matched stringsrecursively on the definition ofs 2 AmbRecMatch:
f./WWD0; (fbase case)
f.[s]/WWD 1 Cf.s/;
f.st/WWD 1 Cf.s/Cf.t/: (fconcat case)
This definition may seem ok, but it isn’t: f./winds up with two values, and
consequently:
0 Df./ (f base case))
Df./ (concat def, base case)
D 1 Cf./Cf./ (fconcat case);
D 1 C 0 C 0 D 1 (fbase case):
This is definitely not a situation we want to be in!
6.3 Recursive Functions on Nonnegative Integers
The nonnegative integers can be understood as a recursive data type.
Definition 6.3.1.The set,N, is a data type defined recursively as:
02 N.
Ifn 2 N, then thesuccessor,nC 1 , ofnis inN.
The point here is to make it clear that ordinary induction is simply the special
case of structural induction on the recursive Definition 6.3.1. This also justifies the
familiar recursive definitions of functions on the nonnegative integers.
