6.2. Strings of Matched Brackets 179
Now,
[] [ ]D[ ] [ ] 2 RecMatch (lettingsD;tD[ ])
[ [ ] ]D[ [ ] ] 2 RecMatch (lettingsD[ ];tD)
[ [ ] ] [ ] 2 RecMatch (lettingsD[ ];tD[ ])are also strings in RecMatch by repeated applications of the constructor case; and
so on.
It’s pretty obvious that in order for brackets to match, there had better be an equal
number of left and right ones. For further practice, let’s carefully prove this from
the recursive definitions.
Lemma.Every string in RecMatch has an equal number of left and right brackets.
Proof. The proof is by structural induction with induction hypothesis
P.s/WWD#[.s/D#].s/:Base case:P./holds because
#[./D 0 D#]./by the base case of Definition 6.1.5 of #c./.
Constructor case: By structural induction hypothesis, we assumeP.s/andP.t/
and must showP.[s]t/:
#[.[s]t/D#[.[/C#[.s/C#[.]/C#[.t/ (Lemma 6.1.6)
D 1 C#[.s/C 0 C#[.t/ (def #[./)
D 1 C#].s/C 0 C#].t/ (byP.s/andP.t/)
D 0 C#].s/C 1 C#].t/
D#].[/C#].s/C#].]/C#].t/ (def #]./)
D#].[s]t/ (Lemma 6.1.6)This completes the proof of the constructor case. We conclude by structural induc-
tion thatP.s/holds for alls 2 RecMatch.
Warning:When a recursive definition of a data type allows the same element
to be constructed in more than one way, the definition is said to beambiguous.
We were careful to choose anunambiguous definition of RecMatch to ensure that
functions defined recursively on its definition would always be well-defined. Re-
cursively defining a function on an ambiguous data type definition usually will not
work. To illustrate the problem, here’s another definition of the matched strings.