Chapter 6 Recursive Data Types198
Sincex 2 Erasable and has positive length, there must be an erase,y 2 Erasable,
ofx. Sojyj Dn 1 0 , and sincey 2 Erasable, we may assume by induction
hypothesis thaty 2 RecMatch.
Now we argue by cases:
Case(yis the empty string):
(*) Prove thatx 2 RecMatch in this case.
Case(yD[s]tfor some stringss;t 2 RecMatch): Now we argue by subcases.
Subcase(xDpy):
(*) Prove thatx 2 RecMatch in this subcase.
Subcase(xis of the form[s^0 ]twheresis an erase ofs^0 ):
Sinces 2 RecMatch, it is erasable by part (b), which implies thats^02
Erasable. Butjs^0 j< jxj, so by induction hypothesis, we may assume that
s^02 RecMatch. This shows thatxis the result of the constructor step of
RecMatch, and thereforex 2 RecMatch.
Subcase(xis of the form[s]t^0 wheretis an erase oft^0 ):
(*) Prove thatx 2 RecMatch in this subcase.(*) Explain why the above cases are sufficient.
This completes the proof by strong induction onn, so we conclude thatP.n/holds
for alln 2 N. Thereforex 2 RecMatch for every stringx 2 Erasable. That is,
ErasableRecMatch. Combined with part (a), we conclude that
ErasableDRecMatch:Problem 6.15. (a)Prove that the set RecMatch, of matched strings of Definition 6.2.1
is closed under string concatenation. Namely, ifs;t 2 RecMatch, thenst 2
RecMatch.
(b)Prove AmbRecMatchRecMatch, where AmbRecMatch is the set of am-
biguous matched strings of Definition 6.2.2.
(c)Prove that RecMatchDAmbRecMatch.