100:00:06,260 --> 00:00:10,275I come back, I knowthe topic of proofs200:00:10,275 --> 00:00:13,950is usually not the mostfavorite topics with students.300:00:13,950 --> 00:00:17,220But I'm really passionateabout proofs in400:00:17,220 --> 00:00:19,320this module because they really500:00:19,320 --> 00:00:21,885help you with understandingwhat's going on.600:00:21,885 --> 00:00:25,170And very often they helpyou with preventing errors.700:00:25,170 --> 00:00:28,695You seen me earlier doingthese calculations.800:00:28,695 --> 00:00:30,210And if I hadn't had900:00:30,210 --> 00:00:33,330the safety net ofknowing what I'm doing,1000:00:33,330 --> 00:00:35,130I could have easily gone wrong.1100:00:35,130 --> 00:00:36,390And that's actually a problem is1200:00:36,390 --> 00:00:38,935existing wreck ExpressionMatching engines.1300:00:38,935 --> 00:00:41,330Sometimes in cornercases as we seen,1400:00:41,330 --> 00:00:43,130they produce slow results,1500:00:43,130 --> 00:00:45,455which is actually not so bad.1600:00:45,455 --> 00:00:48,020Much worse is thatwe also know they1700:00:48,020 --> 00:00:50,570sometimes produceincorrect results.1800:00:50,570 --> 00:00:51,980So for us here,1900:00:51,980 --> 00:00:53,390the proofs will be2000:00:53,390 --> 00:00:55,100essentially the safety nets2100:00:55,100 --> 00:00:58,295of making sure that ouralgorithms actually correct.2200:00:58,295 --> 00:01:00,095And that's actuallythe beauty of that.2300:01:00,095 --> 00:01:03,170It doesn't happen very oftenin real life that we can2400:01:03,170 --> 00:01:06,500actually prove thecorrectness of our algorithm.2500:01:06,500 --> 00:01:08,405But we can do this here.2600:01:08,405 --> 00:01:11,000So we will starta bit slow first,2700:01:11,000 --> 00:01:14,330I will show you howproperties are stated.2800:01:14,330 --> 00:01:17,255And then along the waywe will see how proofs2900:01:17,255 --> 00:01:20,940actually can be performedand how they can help you.3000:01:20,980 --> 00:01:25,205You can probably remember thisslide from the beginning.3100:01:25,205 --> 00:01:29,300Now we would probably stayedthe same property that3200:01:29,300 --> 00:01:32,420our algorithm matchesthe specification3300:01:32,420 --> 00:01:33,695of what that means.3400:01:33,695 --> 00:01:35,450Maybe slightly more mathematical,3500:01:35,450 --> 00:01:37,130we would writesomething like this.3600:01:37,130 --> 00:01:39,545If our Marcia is given as3700:01:39,545 --> 00:01:42,740a string direct expressionR and says yes,3800:01:42,740 --> 00:01:45,110then this stringreally needs to be in3900:01:45,110 --> 00:01:48,350the language of R. Andif the matcher says no,4000:01:48,350 --> 00:01:50,120then this string cannot be in4100:01:50,120 --> 00:01:52,325the language of r. And we spent4200:01:52,325 --> 00:01:54,590quite some effort to make precise4300:01:54,590 --> 00:01:57,065what the language isof a wreck expression.4400:01:57,065 --> 00:01:59,090And we spend some effort to4500:01:59,090 --> 00:02:01,505make precise whatour algorithm is.4600:02:01,505 --> 00:02:02,840So we could now take4700:02:02,840 --> 00:02:06,875this property and we couldgenerate some test cases,4800:02:06,875 --> 00:02:09,410and that is all fine and good.4900:02:09,410 --> 00:02:13,340Testing is a very importantthing for our software.5000:02:13,340 --> 00:02:16,715But we can only dothis testing so far.5100:02:16,715 --> 00:02:19,385Remember in the homework,5200:02:19,385 --> 00:02:21,275there was a single string,5300:02:21,275 --> 00:02:23,750abcd, and there wereactually infinitely5400:02:23,750 --> 00:02:27,530many wreck expressions whichcan match only that string.5500:02:27,530 --> 00:02:30,470So testing something forinfinitely many things,5600:02:30,470 --> 00:02:32,000that's a bit hard.5700:02:32,000 --> 00:02:36,710And Summa, as soon as we havean expression with a star,5800:02:36,710 --> 00:02:39,289this l function returns,5900:02:39,289 --> 00:02:41,360in the general casean infinite set.6000:02:41,360 --> 00:02:43,940And testing whether astring is an infinite set,6100:02:43,940 --> 00:02:45,500that's also a bit hard.6200:02:45,500 --> 00:02:47,510So testing can only do so much.6300:02:47,510 --> 00:02:49,820We could generate somewreck expressions6400:02:49,820 --> 00:02:51,560and we can generate some strings.6500:02:51,560 --> 00:02:53,990And we can testwhether that is true.6600:02:53,990 --> 00:02:57,470So B would be stillin the quandary that6700:02:57,470 --> 00:03:00,950maybe there's a cornercase which doesn't work.6800:03:00,950 --> 00:03:03,110So what we want toachieve instead6900:03:03,110 --> 00:03:05,615is you want to really make sure7000:03:05,615 --> 00:03:07,325that this algorithm works for7100:03:07,325 --> 00:03:10,850all reg expressionand for all strings.7200:03:10,850 --> 00:03:16,400And that ONE proving willhelp us to establish.7300:03:16,400 --> 00:03:19,040Testing cannot do that.7400:03:19,040 --> 00:03:22,310Remember, metromainly consisted of7500:03:22,310 --> 00:03:25,444these functions,nullable and derivative.7600:03:25,444 --> 00:03:27,755So if you want to proveanything about Metro.7700:03:27,755 --> 00:03:30,200Bet on, make sure thatwe know what actually7800:03:30,200 --> 00:03:33,890the specification ofnullable and derivative is.7900:03:33,890 --> 00:03:35,750That's actually quiteinstructive to also8000:03:35,750 --> 00:03:37,850understand how they work.8100:03:37,850 --> 00:03:39,695So let's do that next.8200:03:39,695 --> 00:03:41,975The central property of nullable,8300:03:41,975 --> 00:03:43,445Actually that's not so hard.8400:03:43,445 --> 00:03:48,740It's just says a function ora reg expression is nullable8500:03:48,740 --> 00:03:50,360if and only if8600:03:50,360 --> 00:03:52,160the empty string is in8700:03:52,160 --> 00:03:54,410the language that was thepurpose of this novel,8800:03:54,410 --> 00:03:55,670it takes work, expression and8900:03:55,670 --> 00:03:58,490test whether can matchthe empty string.9000:03:58,490 --> 00:04:01,010Meaning this empty string needs9100:04:01,010 --> 00:04:03,230to be in the languageof R. And again,9200:04:03,230 --> 00:04:04,385we have this if an only,9300:04:04,385 --> 00:04:05,885if this one says yes,9400:04:05,885 --> 00:04:08,465then the empty string needsto be in this language.9500:04:08,465 --> 00:04:10,385And if this nullable says no,9600:04:10,385 --> 00:04:13,085the empty string CoMPunless language.9700:04:13,085 --> 00:04:15,290So that's relatively easy.9800:04:15,290 --> 00:04:18,110The next one might be alsovery instructive to look9900:04:18,110 --> 00:04:22,775at what's the property thederivative should satisfy.10000:04:22,775 --> 00:04:26,329And remember, the derivativewas a kind of operation.10100:04:26,329 --> 00:04:28,850We taking a wreckerexpression and we're looking10200:04:28,850 --> 00:04:31,955at all the strings thisreg expression can match,10300:04:31,955 --> 00:04:35,510but which starts withC. And then me somehow10400:04:35,510 --> 00:04:37,250looking for reg expressionwhich can match10500:04:37,250 --> 00:04:39,335the same string starting with C,10600:04:39,335 --> 00:04:42,440except that thisc is chopped off.10700:04:42,440 --> 00:04:47,150And that actually saveswhat this property states.10800:04:47,150 --> 00:04:50,300Take the, take abreak expression are,10900:04:50,300 --> 00:04:53,045and build the derivativeaccording to see,11000:04:53,045 --> 00:04:56,150okay, so this givesus a reg expression,11100:04:56,150 --> 00:04:58,025the derivative of that11200:04:58,025 --> 00:05:01,775r. Now we take thea language of that,11300:05:01,775 --> 00:05:06,620are that supposed to bethe same set as if I take11400:05:06,620 --> 00:05:12,845the language of R and thenbuild the semantic derivative.11500:05:12,845 --> 00:05:16,055Remember the semantic derivativewas doing exactly that.11600:05:16,055 --> 00:05:18,380It goes through allthe strings in this11700:05:18,380 --> 00:05:21,350that filters out everything which11800:05:21,350 --> 00:05:24,770doesn't start with C.So throws them away of11900:05:24,770 --> 00:05:26,510the remaining stringswhich start with12000:05:26,510 --> 00:05:28,670C. It chops off so that C,12100:05:28,670 --> 00:05:31,370So this will be exactly12200:05:31,370 --> 00:05:34,205what our derivativeis supposed to do.12300:05:34,205 --> 00:05:36,605And yes, if you canestablish that,12400:05:36,605 --> 00:05:38,450then the language of12500:05:38,450 --> 00:05:43,355this derivative operationwill produce the same sat.12600:05:43,355 --> 00:05:45,815This actually alsohow I'm going to12700:05:45,815 --> 00:05:49,760test in cases iconsyet at the beginning,12800:05:49,760 --> 00:05:52,910how your coursework is correct.12900:05:52,910 --> 00:05:55,625If you give me adefinition for derivative13000:05:55,625 --> 00:05:58,730of one of these boundedrecord expressions,13100:05:58,730 --> 00:06:01,085and I can't seewhether it's correct.13200:06:01,085 --> 00:06:03,380Then what it will dois I will just try to13300:06:03,380 --> 00:06:05,675establish that thisproperty holds.13400:06:05,675 --> 00:06:07,265And if I can establish that,13500:06:07,265 --> 00:06:08,870then you coursework is find.13600:06:08,870 --> 00:06:10,550And if I can't establish that,13700:06:10,550 --> 00:06:12,410then usually it shows13800:06:12,410 --> 00:06:14,360there is a counterexamplesomewhere.13900:06:14,360 --> 00:06:19,220Because this derivative,as you've seen desk times,14000:06:19,220 --> 00:06:21,725more than one solutionyou can give.14100:06:21,725 --> 00:06:23,915Some of them are moreefficient than others.14200:06:23,915 --> 00:06:25,685But in terms of correctness,14300:06:25,685 --> 00:06:30,680there are multiple solutionsfor the coursework.14400:06:30,680 --> 00:06:34,145And in the past I really hadto scratch my head and say,14500:06:34,145 --> 00:06:36,995Is that definitionreally correct?14600:06:36,995 --> 00:06:39,620And so what I did isI just went ahead and14700:06:39,620 --> 00:06:42,785tried to prove that orestablish this property.14800:06:42,785 --> 00:06:45,110The reason why we writing14900:06:45,110 --> 00:06:47,300these propertiesdown so precisely,15000:06:47,300 --> 00:06:49,880remember we know herewhat the derivative is,15100:06:49,880 --> 00:06:51,290we know what thelanguages we know15200:06:51,290 --> 00:06:53,495what this semantic derivative is.15300:06:53,495 --> 00:06:56,960This is usually when you aretrying to prove something.15400:06:56,960 --> 00:06:58,715And very important step.15500:06:58,715 --> 00:07:01,385If you know what you'reactually trying to prove,15600:07:01,385 --> 00:07:05,510then you have alreadydone half of the proof.15700:07:05,510 --> 00:07:08,300Remember, we want toestablish these properties15800:07:08,300 --> 00:07:10,460not just for some reg expression,15900:07:10,460 --> 00:07:13,940but for all wrecker expressionand for all characters.16000:07:13,940 --> 00:07:17,225So proving is the onlymethod to achieve that.16100:07:17,225 --> 00:07:18,590And I said at the beginning of16200:07:18,590 --> 00:07:21,170this video's proving is16300:07:21,170 --> 00:07:23,810not the most favoritesubject of students.16400:07:23,810 --> 00:07:25,730But I can promise you,16500:07:25,730 --> 00:07:29,630if you just follow a verysimple minded recipe,16600:07:29,630 --> 00:07:33,695that brings, you're alreadyvery far in these proofs.16700:07:33,695 --> 00:07:35,720Of course, there'salways some creativity16800:07:35,720 --> 00:07:37,070involved in these proofs.16900:07:37,070 --> 00:07:39,380But a simple-mindedrecipe you can17000:07:39,380 --> 00:07:42,620follow brings you're alreadyvery close to the end.17100:07:42,620 --> 00:07:46,610So let's have a look howthis recipe can be derived.17200:07:46,610 --> 00:07:48,740Establishing a property is for17300:07:48,740 --> 00:07:50,900all Rekha expression nearly17400:07:50,900 --> 00:07:55,805always requires an inductionover wreck expressions.17500:07:55,805 --> 00:07:57,350And so we have to look at what's17600:07:57,350 --> 00:07:59,150the recipe for doing inductions17700:07:59,150 --> 00:08:02,390over wreck expressionsand inductions.17800:08:02,390 --> 00:08:03,590You probably remember from17900:08:03,590 --> 00:08:07,100school time you did inductionover natural numbers.18000:08:07,100 --> 00:08:11,120You had to establish thatsome property holds for 0.18100:08:11,120 --> 00:08:13,775And you had to establish it18200:08:13,775 --> 00:08:14,960that if you assume that18300:08:14,960 --> 00:08:16,970the property holdsfor the N case,18400:08:16,970 --> 00:08:21,365it has to also hold forthe n plus one case.18500:08:21,365 --> 00:08:24,350And induction over wreckexpressions is very,18600:08:24,350 --> 00:08:26,810very similar to thiskind of induction.18700:08:26,810 --> 00:08:30,754Just that in case ofbreak expressions,18800:08:30,754 --> 00:08:33,200we have essentiallythree base cases.18900:08:33,200 --> 00:08:35,360So in our grandmaor we say it rec,19000:08:35,360 --> 00:08:38,705expressions are 01and characters.19100:08:38,705 --> 00:08:42,260And these will be the basecases in our induction.19200:08:42,260 --> 00:08:43,895So we have to establish19300:08:43,895 --> 00:08:46,475any property we wantto prove by induction,19400:08:46,475 --> 00:08:49,055you have to showthat it holds for 0,19500:08:49,055 --> 00:08:50,495it holds for one,19600:08:50,495 --> 00:08:52,505and it holds for the character.19700:08:52,505 --> 00:08:57,350So there's nothing else wecan assume in these cases.19800:08:57,350 --> 00:08:59,300We just have to provethat this property19900:08:59,300 --> 00:09:01,835holds in these three base cases.20000:09:01,835 --> 00:09:04,490It is very much thesame as if you proved20100:09:04,490 --> 00:09:06,050something over natural numbers20200:09:06,050 --> 00:09:08,270and you had to prove it for 0.20300:09:08,270 --> 00:09:10,880Now, the sequence case,20400:09:10,880 --> 00:09:12,755the alternative in a star.20500:09:12,755 --> 00:09:15,815These are the kindof inductive cases.20600:09:15,815 --> 00:09:17,750Remember in natural numbers,20700:09:17,750 --> 00:09:20,450you could assume thata property holds for20800:09:20,450 --> 00:09:24,770n and then you had toestablish it for n plus one.20900:09:24,770 --> 00:09:26,945This is here very simmer.21000:09:26,945 --> 00:09:29,000You can assume that21100:09:29,000 --> 00:09:30,920these properties hold for21200:09:30,920 --> 00:09:33,140the components ofthese reg expression.21300:09:33,140 --> 00:09:35,840So you can assume that itholds for this on one,21400:09:35,840 --> 00:09:38,960and you can assume thatit holds for this R2.21500:09:38,960 --> 00:09:41,090And your task is now to21600:09:41,090 --> 00:09:44,240establish this propertyalso for sequences.21700:09:44,240 --> 00:09:46,255The same for alternative soup.21800:09:46,255 --> 00:09:48,710Assume that it holdsalready for R1.21900:09:48,710 --> 00:09:51,005You can assume thatit holds for the R2.22000:09:51,005 --> 00:09:53,930You have to establish thatthis property holds also for22100:09:53,930 --> 00:09:58,460the entire alternative,the same four star.22200:09:58,460 --> 00:10:00,440So there you can assume it for r,22300:10:00,440 --> 00:10:02,330but you have to nowestablish it that22400:10:02,330 --> 00:10:04,760it also holds for r star.22500:10:04,760 --> 00:10:07,910Ok, that leads to thissimple-minded recipe22600:10:07,910 --> 00:10:09,560which you can always follow.22700:10:09,560 --> 00:10:10,970So first you have to know22800:10:10,970 --> 00:10:13,085what's the propertyyou want to show.22900:10:13,085 --> 00:10:16,790Luckily for you, that'salmost always given by me.23000:10:16,790 --> 00:10:19,100So there's nothingto think about it.23100:10:19,100 --> 00:10:22,100But then what you have todo in an induction proof,23200:10:22,100 --> 00:10:23,855you have to show thatthis property holds23300:10:23,855 --> 00:10:26,345for 041 and characters.23400:10:26,345 --> 00:10:28,790These are the basecases in the induction.23500:10:28,790 --> 00:10:31,280And then in the induction cases,23600:10:31,280 --> 00:10:32,555you just have to say, well,23700:10:32,555 --> 00:10:34,535I know that thisproperty holds for one,23800:10:34,535 --> 00:10:36,980I know that theproperty holds for R2.23900:10:36,980 --> 00:10:38,720What does it look like that24000:10:38,720 --> 00:10:40,895this property holdsfor the alternative,24100:10:40,895 --> 00:10:44,480for the sequenceand for the r-star,24200:10:44,480 --> 00:10:46,955that will then requiressome reasoning.24300:10:46,955 --> 00:10:48,230But if you know what you can24400:10:48,230 --> 00:10:50,359assume and what do youhave to establish?24500:10:50,359 --> 00:10:52,940Often can already see bought24600:10:52,940 --> 00:10:55,490needs to be proved andwhat's the argument like?24700:10:55,490 --> 00:10:58,325So let's try that andthen concrete example.24800:10:58,325 --> 00:11:01,265So how does approvework in real life?24900:11:01,265 --> 00:11:03,530And say that the beginningfirst you have to know25000:11:03,530 --> 00:11:05,630what's the propertyyou want to prove.25100:11:05,630 --> 00:11:10,280So in our case, the P of R is if25200:11:10,280 --> 00:11:14,900nullable of R holds if25300:11:14,900 --> 00:11:19,760and only if the empty stringis in the language of.25400:11:19,760 --> 00:11:23,690So we want to do an inductionof rec expressions.25500:11:23,690 --> 00:11:28,400So we better have Fan propertywhich depends on this25600:11:28,400 --> 00:11:31,130R. And so now in25700:11:31,130 --> 00:11:34,985each case I would start witha blank piece of paper.25800:11:34,985 --> 00:11:38,030And I would write on the top,25900:11:38,030 --> 00:11:40,190what are my assumptions?26000:11:40,190 --> 00:11:42,470And on the bottom, I would write26100:11:42,470 --> 00:11:45,485down what I need to prove.26200:11:45,485 --> 00:11:49,280And then I would tryto somehow navigate26300:11:49,280 --> 00:11:53,540my way from these assumptionsto what I want to prove,26400:11:53,540 --> 00:11:57,740to somehow infersmall steps so that I26500:11:57,740 --> 00:11:59,960can assure that what I'm trying26600:11:59,960 --> 00:12:02,780to prove holds formy assumptions.26700:12:02,780 --> 00:12:06,905Obviously. That dependson how hard that case is.26800:12:06,905 --> 00:12:08,930And if you look atour first case,26900:12:08,930 --> 00:12:10,835what we have to show is if to27000:12:10,835 --> 00:12:13,655prove that this P of 0 holds.27100:12:13,655 --> 00:12:15,410And actually no assumption in27200:12:15,410 --> 00:12:17,450this case because it'sone of the base cases.27300:12:17,450 --> 00:12:23,015So what I have to show is Ihave to show that nullable of27400:12:23,015 --> 00:12:29,5700 if and only if the emptystring is in L of 0.27500:12:29,570 --> 00:12:31,340Okay? And I have to27600:12:31,340 --> 00:12:34,190somehow show that thisimplementation of nullable in27700:12:34,190 --> 00:12:35,600this case produces27800:12:35,600 --> 00:12:39,185exactly the same answeras that specification.27900:12:39,185 --> 00:12:41,660Okay? So what is nullable of 0 is28000:12:41,660 --> 00:12:45,605defined where debt isjust false by definition.28100:12:45,605 --> 00:12:50,225And what is thislanguage of LCA defined?28200:12:50,225 --> 00:12:52,535Well, that is justthe empty string.28300:12:52,535 --> 00:12:55,010In the empty language.28400:12:55,010 --> 00:12:57,110Is the empty string andthe empty language,28500:12:57,110 --> 00:12:59,240no, that is false too.28600:12:59,240 --> 00:13:01,610So I have shown that28700:13:01,610 --> 00:13:03,890both of them producethe same result.28800:13:03,890 --> 00:13:08,765So I would already be donein the first base case.28900:13:08,765 --> 00:13:12,125The second base case is notso much more difficult.29000:13:12,125 --> 00:13:15,455We want to provethat P of one holds.29100:13:15,455 --> 00:13:21,680And that would sayif nullable of one,29200:13:21,680 --> 00:13:23,825if and only if29300:13:23,825 --> 00:13:27,665the empty string is inthe language of one.29400:13:27,665 --> 00:13:31,235Okay? I can again lookat what's that defined,29500:13:31,235 --> 00:13:33,275that is defined as true.29600:13:33,275 --> 00:13:35,450And what is this language to29700:13:35,450 --> 00:13:37,640find where that is defined as29800:13:37,640 --> 00:13:39,320the empty string in29900:13:39,320 --> 00:13:42,230the language containingthe empty string.30000:13:42,230 --> 00:13:44,150And is the empty string in30100:13:44,150 --> 00:13:46,055the language containingthe empty string?30200:13:46,055 --> 00:13:47,975Yes, that's true as well.30300:13:47,975 --> 00:13:50,735So again, I've shown thatthe actual implementation30400:13:50,735 --> 00:13:55,250produces the same resultas the specification.30500:13:55,250 --> 00:13:57,635I leave the character base case30600:13:57,635 --> 00:14:00,690for you to fill in the details.30700:14:01,150 --> 00:14:03,320More interesting are these30800:14:03,320 --> 00:14:05,300inductive cases asyou can imagine.30900:14:05,300 --> 00:14:08,360So let's try to proveit for the alternative.31000:14:08,360 --> 00:14:10,639So I want to show a property31100:14:10,639 --> 00:14:13,790for this record expression way.31200:14:13,790 --> 00:14:15,410What does our property save31300:14:15,410 --> 00:14:16,970for that reg expressionwhere we have to31400:14:16,970 --> 00:14:20,915say that nullable of31500:14:20,915 --> 00:14:25,490R1 plus R2 if and only if31600:14:25,490 --> 00:14:31,519the empty string is in thelanguage if R1 plus R2.31700:14:31,519 --> 00:14:35,090Ok? So I would now go ahead with31800:14:35,090 --> 00:14:39,695my plank piece of paper andI would write down on top.31900:14:39,695 --> 00:14:41,475Now what can I assume?32000:14:41,475 --> 00:14:45,170Well, I can assumethat P of R1 holds and32100:14:45,170 --> 00:14:49,175I can assume whatp of r two holds.32200:14:49,175 --> 00:14:50,750And let's just write that down.32300:14:50,750 --> 00:14:56,210We can say that nullable of R1 if32400:14:56,210 --> 00:14:58,655and only if the empty string32500:14:58,655 --> 00:15:02,000is in the language ofR1, I can assume that.32600:15:02,000 --> 00:15:03,500And I can assume32700:15:03,500 --> 00:15:10,355that none above our two ifand only if the empty string.32800:15:10,355 --> 00:15:14,675Or to Hawaii. What's now,32900:15:14,675 --> 00:15:15,830what do I want to prove?33000:15:15,830 --> 00:15:18,455Where I want toprove this property?33100:15:18,455 --> 00:15:21,935So let me write this hereagain on the bottom.33200:15:21,935 --> 00:15:30,935So p of R1 plus R2is narrow form of R133300:15:30,935 --> 00:15:34,595plus R2 if and only if33400:15:34,595 --> 00:15:40,610the empty string is in thelanguage of R1 plus R2.33500:15:40,610 --> 00:15:43,280Well, the first thing I can do is33600:15:43,280 --> 00:15:46,760I can infer what's thedefinition of that?33700:15:46,760 --> 00:15:51,920Where that wouldbe nullable of R133800:15:51,920 --> 00:15:57,530or nullable of our two.33900:15:57,530 --> 00:15:59,960That's how it was defined, okay?34000:15:59,960 --> 00:16:01,730And what can I do with this?34100:16:01,730 --> 00:16:04,700I can also look at how is34200:16:04,700 --> 00:16:08,510this language to findwhere that is defined as34300:16:08,510 --> 00:16:16,730the empty string in thelanguage of R1 union R2.34400:16:16,730 --> 00:16:19,910Okay? So what does that mean?34500:16:19,910 --> 00:16:23,585Well, Venice, the emptystring in a union.34600:16:23,585 --> 00:16:27,095Well, it has to bethe case that either34700:16:27,095 --> 00:16:31,190the empty stringis in L of R one,34800:16:31,190 --> 00:16:37,670all the empty stringis o. L of R two.34900:16:37,670 --> 00:16:43,715Ok, so that's, I justapplied all the definitions.35000:16:43,715 --> 00:16:47,930And now I have to look bettermy induction hypothesis.35100:16:47,930 --> 00:16:50,930These somehow help.35200:16:50,930 --> 00:16:55,820Well, I know nullableof R1 holds if35300:16:55,820 --> 00:17:00,815and only if the emptystring is in L of one.35400:17:00,815 --> 00:17:05,330So that is by the inductionhypothesis, a hypothesis.35500:17:05,330 --> 00:17:07,670And I also know by this,35600:17:07,670 --> 00:17:10,040that this holds only if35700:17:10,040 --> 00:17:17,465the empty string is in R2and there's an in-between.35800:17:17,465 --> 00:17:19,580Now you can see again,35900:17:19,580 --> 00:17:23,690this is what my specificationsay It must hold.36000:17:23,690 --> 00:17:25,640And this is essentially36100:17:25,640 --> 00:17:28,685what I could infer frommy implementation.36200:17:28,685 --> 00:17:30,140And they are the same.36300:17:30,140 --> 00:17:32,270So also this case,36400:17:32,270 --> 00:17:35,520I've shown my property holds.36500:17:35,740 --> 00:17:39,275Just for fun. Let's do thisalso for the sequence.36600:17:39,275 --> 00:17:43,835So we want to showP of 014 by two.36700:17:43,835 --> 00:17:51,050And that means I have toprove that nullable of R1 by36800:17:51,050 --> 00:17:54,095R2 if and only if36900:17:54,095 --> 00:18:00,440the empty string isone followed by two.37000:18:00,440 --> 00:18:04,880Ok? And in this caseI'm just writing37100:18:04,880 --> 00:18:09,695my inductionhypothesis on the top.37200:18:09,695 --> 00:18:11,060And that would be,37300:18:11,060 --> 00:18:13,460I know that p of r one holds.37400:18:13,460 --> 00:18:18,290So another ball of R one37500:18:18,290 --> 00:18:24,860if and only if the emptystring is in L one.37600:18:24,860 --> 00:18:29,525And the P of R to sayis that I know already37700:18:29,525 --> 00:18:36,815nullable of R2 if and onlyif the empty string then R2.37800:18:36,815 --> 00:18:39,230Okay? And I know some hard to37900:18:39,230 --> 00:18:42,285infer that underthese assumptions,38000:18:42,285 --> 00:18:45,970this property, likein the earlier case,38100:18:45,970 --> 00:18:48,070I just have a look how38200:18:48,070 --> 00:18:51,145everything is defined andsee if I can go from there.38300:18:51,145 --> 00:18:56,485So nullable of thesequence would be nullable38400:18:56,485 --> 00:19:04,555of R1 and nullable of R2.38500:19:04,555 --> 00:19:08,559Okay? By theinduction hypothesis,38600:19:08,559 --> 00:19:16,255I can now infer thatthe empty string is38700:19:16,255 --> 00:19:24,750in L one and the emptystring is in L two.38800:19:24,750 --> 00:19:28,175Ok? Not much as Ican do on this side.38900:19:28,175 --> 00:19:31,520But I can now tryto infer something39000:19:31,520 --> 00:19:33,110here because I know how39100:19:33,110 --> 00:19:35,735this L of thissequence is defined.39200:19:35,735 --> 00:19:39,665That says the emptystring has to be n l,39300:19:39,665 --> 00:19:45,110one append of L of R, two.39400:19:45,110 --> 00:19:48,365Ok? So they are not yet equal.39500:19:48,365 --> 00:19:50,150But now I have toessentially scratch39600:19:50,150 --> 00:19:52,430my head. What does that mean?39700:19:52,430 --> 00:19:54,965So this is the languageconcatenation,39800:19:54,965 --> 00:19:57,035Venice, the empty string.39900:19:57,035 --> 00:20:01,265In this concatenation ofthese two language as well.40000:20:01,265 --> 00:20:05,990It will be there ifL of our wormholes40100:20:05,990 --> 00:20:12,560and The empty stringof L R2 holds.40200:20:12,560 --> 00:20:14,600And so again, I have shown that40300:20:14,600 --> 00:20:17,780this is equivalent to that.40400:20:17,780 --> 00:20:20,480Which means that this must be40500:20:20,480 --> 00:20:24,540equal to that o holdsif and only if.40600:20:25,600 --> 00:20:28,940Finally, the star case,40700:20:28,940 --> 00:20:31,235p of r star.40800:20:31,235 --> 00:20:35,450Ok? So I know myinduction hypothesis,40900:20:35,450 --> 00:20:41,075let me write it again onthe top that P of R holds,41000:20:41,075 --> 00:20:46,835which means nullable of R if and41100:20:46,835 --> 00:20:53,060only if the emptystring is in L. Okay?41200:20:53,060 --> 00:20:58,580And I have to provethat nullable of41300:20:58,580 --> 00:21:08,930r star if and only if theempty string is n l of r star.41400:21:08,930 --> 00:21:15,020Ok? So again, I just followhow are things define?41500:21:15,020 --> 00:21:18,125So this is definedactually as true.41600:21:18,125 --> 00:21:21,365So a star's always nullable.41700:21:21,365 --> 00:21:23,090What is this defined where,41800:21:23,090 --> 00:21:26,225remember that wants to findusing the Kleene star.41900:21:26,225 --> 00:21:28,685So that is essentially L of42000:21:28,685 --> 00:21:33,680R. And then we had thisstar on languages.42100:21:33,680 --> 00:21:36,260And does the star on42200:21:36,260 --> 00:21:39,380languages always containthe empty string?42300:21:39,380 --> 00:21:42,980Yes, that is true as well.42400:21:42,980 --> 00:21:45,320And so again, I'veshown their clone.42500:21:45,320 --> 00:21:47,420And here you can see, even if I42600:21:47,420 --> 00:21:49,730have here in this casean induction hypothesis,42700:21:49,730 --> 00:21:51,860I actually didn't needthat in my reasoning.42800:21:51,860 --> 00:21:53,960Well, that might happen.42900:21:53,960 --> 00:21:56,840This might have been thefirst induction proof43000:21:56,840 --> 00:21:58,445for regular expressions for you.43100:21:58,445 --> 00:22:00,680But you've seen atWatson so difficult,43200:22:00,680 --> 00:22:02,480you just follow this recipe.43300:22:02,480 --> 00:22:04,280It told us we can43400:22:04,280 --> 00:22:06,725assume in each casewhat we have to prove.43500:22:06,725 --> 00:22:09,860And then we essentially justfollowed what are things to43600:22:09,860 --> 00:22:13,595find and try to inferwhether in each case,43700:22:13,595 --> 00:22:15,560both of them producethe same result,43800:22:15,560 --> 00:22:18,245the specification andthe implementation.43900:22:18,245 --> 00:22:20,300And the great thing about this,44000:22:20,300 --> 00:22:22,250if you've done all these cases,44100:22:22,250 --> 00:22:25,490we not just know that it holdsfor some reg expression,44200:22:25,490 --> 00:22:28,280but actually it holds forall wreck expressions be44300:22:28,280 --> 00:22:30,890couldn't achieve the sameresult by looking just44400:22:30,890 --> 00:22:33,710at testing becausewe would not be44500:22:33,710 --> 00:22:37,280able to test for allrecord expressions.44600:22:37,280 --> 00:22:39,560Ok, of course, there will be44700:22:39,560 --> 00:22:43,010also induction proofs whichare more complicated.44800:22:43,010 --> 00:22:46,170But let's leave thatfor another time.44900:22:49,210 --> 00:22:53,405You know, I always like totalk about the subject.45000:22:53,405 --> 00:22:55,700So here's one last thought.45100:22:55,700 --> 00:22:58,040You might think these proofs for45200:22:58,040 --> 00:22:59,930this little propertyabout nullable are45300:22:59,930 --> 00:23:04,295totally overkill andtotal waste of your time.45400:23:04,295 --> 00:23:07,310Please rest assured disproves45500:23:07,310 --> 00:23:10,160have saved me from somuch embarrassment.45600:23:10,160 --> 00:23:13,745You cannot imagine,once I have a proof,45700:23:13,745 --> 00:23:15,425I can sleep much better.45800:23:15,425 --> 00:23:16,820If I don't have a proof,45900:23:16,820 --> 00:23:19,560I don't believe what I'm doing.