1

00:00:06,260 --> 00:00:10,275

I come back, I know

the topic of proofs

2

00:00:10,275 --> 00:00:13,950

is usually not the most

favorite topics with students.

3

00:00:13,950 --> 00:00:17,220

But I'm really passionate

about proofs in

4

00:00:17,220 --> 00:00:19,320

this module because they really

5

00:00:19,320 --> 00:00:21,885

help you with understanding

what's going on.

6

00:00:21,885 --> 00:00:25,170

And very often they help

you with preventing errors.

7

00:00:25,170 --> 00:00:28,695

You seen me earlier doing

these calculations.

8

00:00:28,695 --> 00:00:30,210

And if I hadn't had

9

00:00:30,210 --> 00:00:33,330

the safety net of

knowing what I'm doing,

10

00:00:33,330 --> 00:00:35,130

I could have easily gone wrong.

11

00:00:35,130 --> 00:00:36,390

And that's actually a problem is

12

00:00:36,390 --> 00:00:38,935

existing wreck Expression

Matching engines.

13

00:00:38,935 --> 00:00:41,330

Sometimes in corner

cases as we seen,

14

00:00:41,330 --> 00:00:43,130

they produce slow results,

15

00:00:43,130 --> 00:00:45,455

which is actually not so bad.

16

00:00:45,455 --> 00:00:48,020

Much worse is that

we also know they

17

00:00:48,020 --> 00:00:50,570

sometimes produce

incorrect results.

18

00:00:50,570 --> 00:00:51,980

So for us here,

19

00:00:51,980 --> 00:00:53,390

the proofs will be

20

00:00:53,390 --> 00:00:55,100

essentially the safety nets

21

00:00:55,100 --> 00:00:58,295

of making sure that our

algorithms actually correct.

22

00:00:58,295 --> 00:01:00,095

And that's actually

the beauty of that.

23

00:01:00,095 --> 00:01:03,170

It doesn't happen very often

in real life that we can

24

00:01:03,170 --> 00:01:06,500

actually prove the

correctness of our algorithm.

25

00:01:06,500 --> 00:01:08,405

But we can do this here.

26

00:01:08,405 --> 00:01:11,000

So we will start

a bit slow first,

27

00:01:11,000 --> 00:01:14,330

I will show you how

properties are stated.

28

00:01:14,330 --> 00:01:17,255

And then along the way

we will see how proofs

29

00:01:17,255 --> 00:01:20,940

actually can be performed

and how they can help you.

30

00:01:20,980 --> 00:01:25,205

You can probably remember this

slide from the beginning.

31

00:01:25,205 --> 00:01:29,300

Now we would probably stayed

the same property that

32

00:01:29,300 --> 00:01:32,420

our algorithm matches

the specification

33

00:01:32,420 --> 00:01:33,695

of what that means.

34

00:01:33,695 --> 00:01:35,450

Maybe slightly more mathematical,

35

00:01:35,450 --> 00:01:37,130

we would write

something like this.

36

00:01:37,130 --> 00:01:39,545

If our Marcia is given as

37

00:01:39,545 --> 00:01:42,740

a string direct expression

R and says yes,

38

00:01:42,740 --> 00:01:45,110

then this string

really needs to be in

39

00:01:45,110 --> 00:01:48,350

the language of R. And

if the matcher says no,

40

00:01:48,350 --> 00:01:50,120

then this string cannot be in

41

00:01:50,120 --> 00:01:52,325

the language of r. And we spent

42

00:01:52,325 --> 00:01:54,590

quite some effort to make precise

43

00:01:54,590 --> 00:01:57,065

what the language is

of a wreck expression.

44

00:01:57,065 --> 00:01:59,090

And we spend some effort to

45

00:01:59,090 --> 00:02:01,505

make precise what

our algorithm is.

46

00:02:01,505 --> 00:02:02,840

So we could now take

47

00:02:02,840 --> 00:02:06,875

this property and we could

generate some test cases,

48

00:02:06,875 --> 00:02:09,410

and that is all fine and good.

49

00:02:09,410 --> 00:02:13,340

Testing is a very important

thing for our software.

50

00:02:13,340 --> 00:02:16,715

But we can only do

this testing so far.

51

00:02:16,715 --> 00:02:19,385

Remember in the homework,

52

00:02:19,385 --> 00:02:21,275

there was a single string,

53

00:02:21,275 --> 00:02:23,750

abcd, and there were

actually infinitely

54

00:02:23,750 --> 00:02:27,530

many wreck expressions which

can match only that string.

55

00:02:27,530 --> 00:02:30,470

So testing something for

infinitely many things,

56

00:02:30,470 --> 00:02:32,000

that's a bit hard.

57

00:02:32,000 --> 00:02:36,710

And Summa, as soon as we have

an expression with a star,

58

00:02:36,710 --> 00:02:39,289

this l function returns,

59

00:02:39,289 --> 00:02:41,360

in the general case

an infinite set.

60

00:02:41,360 --> 00:02:43,940

And testing whether a

string is an infinite set,

61

00:02:43,940 --> 00:02:45,500

that's also a bit hard.

62

00:02:45,500 --> 00:02:47,510

So testing can only do so much.

63

00:02:47,510 --> 00:02:49,820

We could generate some

wreck expressions

64

00:02:49,820 --> 00:02:51,560

and we can generate some strings.

65

00:02:51,560 --> 00:02:53,990

And we can test

whether that is true.

66

00:02:53,990 --> 00:02:57,470

So B would be still

in the quandary that

67

00:02:57,470 --> 00:03:00,950

maybe there's a corner

case which doesn't work.

68

00:03:00,950 --> 00:03:03,110

So what we want to

achieve instead

69

00:03:03,110 --> 00:03:05,615

is you want to really make sure

70

00:03:05,615 --> 00:03:07,325

that this algorithm works for

71

00:03:07,325 --> 00:03:10,850

all reg expression

and for all strings.

72

00:03:10,850 --> 00:03:16,400

And that ONE proving will

help us to establish.

73

00:03:16,400 --> 00:03:19,040

Testing cannot do that.

74

00:03:19,040 --> 00:03:22,310

Remember, metro

mainly consisted of

75

00:03:22,310 --> 00:03:25,444

these functions,

nullable and derivative.

76

00:03:25,444 --> 00:03:27,755

So if you want to prove

anything about Metro.

77

00:03:27,755 --> 00:03:30,200

Bet on, make sure that

we know what actually

78

00:03:30,200 --> 00:03:33,890

the specification of

nullable and derivative is.

79

00:03:33,890 --> 00:03:35,750

That's actually quite

instructive to also

80

00:03:35,750 --> 00:03:37,850

understand how they work.

81

00:03:37,850 --> 00:03:39,695

So let's do that next.

82

00:03:39,695 --> 00:03:41,975

The central property of nullable,

83

00:03:41,975 --> 00:03:43,445

Actually that's not so hard.

84

00:03:43,445 --> 00:03:48,740

It's just says a function or

a reg expression is nullable

85

00:03:48,740 --> 00:03:50,360

if and only if

86

00:03:50,360 --> 00:03:52,160

the empty string is in

87

00:03:52,160 --> 00:03:54,410

the language that was the

purpose of this novel,

88

00:03:54,410 --> 00:03:55,670

it takes work, expression and

89

00:03:55,670 --> 00:03:58,490

test whether can match

the empty string.

90

00:03:58,490 --> 00:04:01,010

Meaning this empty string needs

91

00:04:01,010 --> 00:04:03,230

to be in the language

of R. And again,

92

00:04:03,230 --> 00:04:04,385

we have this if an only,

93

00:04:04,385 --> 00:04:05,885

if this one says yes,

94

00:04:05,885 --> 00:04:08,465

then the empty string needs

to be in this language.

95

00:04:08,465 --> 00:04:10,385

And if this nullable says no,

96

00:04:10,385 --> 00:04:13,085

the empty string CoMP

unless language.

97

00:04:13,085 --> 00:04:15,290

So that's relatively easy.

98

00:04:15,290 --> 00:04:18,110

The next one might be also

very instructive to look

99

00:04:18,110 --> 00:04:22,775

at what's the property the

derivative should satisfy.

100

00:04:22,775 --> 00:04:26,329

And remember, the derivative

was a kind of operation.

101

00:04:26,329 --> 00:04:28,850

We taking a wrecker

expression and we're looking

102

00:04:28,850 --> 00:04:31,955

at all the strings this

reg expression can match,

103

00:04:31,955 --> 00:04:35,510

but which starts with

C. And then me somehow

104

00:04:35,510 --> 00:04:37,250

looking for reg expression

which can match

105

00:04:37,250 --> 00:04:39,335

the same string starting with C,

106

00:04:39,335 --> 00:04:42,440

except that this

c is chopped off.

107

00:04:42,440 --> 00:04:47,150

And that actually saves

what this property states.

108

00:04:47,150 --> 00:04:50,300

Take the, take a

break expression are,

109

00:04:50,300 --> 00:04:53,045

and build the derivative

according to see,

110

00:04:53,045 --> 00:04:56,150

okay, so this gives

us a reg expression,

111

00:04:56,150 --> 00:04:58,025

the derivative of that

112

00:04:58,025 --> 00:05:01,775

r. Now we take the

a language of that,

113

00:05:01,775 --> 00:05:06,620

are that supposed to be

the same set as if I take

114

00:05:06,620 --> 00:05:12,845

the language of R and then

build the semantic derivative.

115

00:05:12,845 --> 00:05:16,055