773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1 |
1
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
2 |
00:00:06,350 --> 00:00:10,305
|
774
|
3 |
Welcome come back. I
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
can hear you saying,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
5 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
6 |
2
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
7 |
00:00:10,305 --> 00:00:12,000
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
8 |
yes, you tried it out on
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
9 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
3
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
00:00:12,000 --> 00:00:14,760
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
one example and you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
were much better.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
4
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
00:00:14,760 --> 00:00:17,415
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
But how about on other examples?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
5
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
00:00:17,415 --> 00:00:21,265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
Specifically, we had two
|
774
|
22 |
evil regular expressions.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
23 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
6
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
00:00:21,265 --> 00:00:23,480
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
How about the other case?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
27 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
28 |
7
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
00:00:23,480 --> 00:00:27,480
|
774
|
30 |
Well, let's have a look at
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
that other case in this video.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
32 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
33 |
8
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
00:00:29,140 --> 00:00:32,705
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
So I'm back here
|
774
|
36 |
in this re2.sc file.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
9
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
00:00:32,705 --> 00:00:35,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
And here's this test
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
41 |
case which run quite
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
42 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
43 |
10
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
44 |
00:00:35,180 --> 00:00:39,665
|
774
|
45 |
nicely for strings between 0 and 1000.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
46 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
47 |
11
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
48 |
00:00:39,665 --> 00:00:42,725
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
49 |
Here is the other test case.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
12
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
00:00:42,725 --> 00:00:44,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
I still run it only
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
55 |
13
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
00:00:44,090 --> 00:00:48,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
for relatively small
|
774
|
58 |
strings between 0 and 20.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
60 |
14
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
61 |
00:00:48,470 --> 00:00:50,240
|
774
|
62 |
And let's see what it says.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
64 |
15
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
65 |
00:00:50,240 --> 00:00:51,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
66 |
So I'm running the test in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
67 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
68 |
16
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
69 |
00:00:51,800 --> 00:00:57,320
|
774
|
70 |
the Amoonite REPL and it
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
71 |
doesn't look too bad.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
73 |
17
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
74 |
00:00:57,320 --> 00:01:01,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
75 |
But this might be because
|
774
|
76 |
20 is not generous enough.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
78 |
18
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
00:01:01,160 --> 00:01:03,620
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
80 |
So let's try it with 30.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
81 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
82 |
19
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
00:01:03,620 --> 00:01:06,530
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
Let's run this test again.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
85 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
20
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
00:01:06,530 --> 00:01:11,075
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
And 20 is quite okay.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
89 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
90 |
21
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
00:01:11,075 --> 00:01:15,965
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
92 |
22, okay, that's now
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
almost ten times as much.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
94 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
95 |
22
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
00:01:15,965 --> 00:01:18,995
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
And then the next
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
one would be 24.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
99 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
23
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
00:01:18,995 --> 00:01:23,615
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
And we're waiting and waiting.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
103 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
104 |
24
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
00:01:23,615 --> 00:01:26,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
And we are waiting.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
108 |
25
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
109 |
00:01:26,410 --> 00:01:29,300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
Actually, it isn't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
calculated at all.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
113 |
26
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
00:01:29,300 --> 00:01:31,399
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
It run out of memory.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
117 |
27
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
00:01:31,399 --> 00:01:33,905
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
So here is something going on,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
120 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
121 |
28
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
122 |
00:01:33,905 --> 00:01:37,640
|
774
|
123 |
which is definitely bad and we
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
124 |
have to have a look at that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
125 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
126 |
29
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
127 |
00:01:37,640 --> 00:01:40,640
|
774
|
128 |
It's always
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
129 |
instructive with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
130 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
131 |
30
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
132 |
00:01:40,640 --> 00:01:43,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
133 |
this algorithm to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
134 |
look at the sizes of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
135 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
136 |
31
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
137 |
00:01:43,460 --> 00:01:45,695
|
774
|
138 |
the regular expressions
|
|
139 |
we calculate.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
140 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
141 |
32
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
142 |
00:01:45,695 --> 00:01:49,625
|
774
|
143 |
The EVIL2 is this
|
|
144 |
a star, star b.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
145 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
146 |
33
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
147 |
00:01:49,625 --> 00:01:51,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
148 |
So there's nothing we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
149 |
can compress there.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
150 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
151 |
34
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
152 |
00:01:51,800 --> 00:01:55,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
153 |
It has just stars and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
154 |
sequences and nothing else.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
155 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
156 |
35
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
157 |
00:01:55,490 --> 00:01:58,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
158 |
And so it's not that we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
159 |
can play the same trick
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
160 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
161 |
36
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
162 |
00:01:58,430 --> 00:02:01,805
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
163 |
of trying to introduce
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
164 |
an explicit constructor.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
165 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
166 |
37
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
167 |
00:02:01,805 --> 00:02:04,190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
168 |
But now let's have a
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
169 |
look at the derivatives.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
170 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
171 |
38
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
172 |
00:02:04,190 --> 00:02:05,600
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
173 |
As you can see here.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
174 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
175 |
39
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
176 |
00:02:05,600 --> 00:02:08,420
|
774
|
177 |
If I take this EVIL2 regular
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
178 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
179 |
40
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
180 |
00:02:08,420 --> 00:02:09,935
|
774
|
181 |
expression and then build
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
182 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
183 |
41
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
184 |
00:02:09,935 --> 00:02:12,470
|
774
|
185 |
longer and
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
186 |
longer derivatives,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
187 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
188 |
42
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
189 |
00:02:12,470 --> 00:02:14,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
190 |
you can see this grows.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
191 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
192 |
43
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
193 |
00:02:14,090 --> 00:02:16,055
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
194 |
And as you see in this line,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
195 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
196 |
44
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
197 |
00:02:16,055 --> 00:02:17,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
198 |
if I'm trying to take
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
199 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
200 |
45
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
201 |
00:02:17,270 --> 00:02:20,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
202 |
the derivative of a
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
203 |
quite large string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
204 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
205 |
46
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
206 |
00:02:20,180 --> 00:02:21,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
207 |
it is quite quick.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
208 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
209 |
47
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
210 |
00:02:21,680 --> 00:02:26,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
211 |
But the size of the
|
774
|
212 |
regular expression,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
213 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
214 |
48
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
215 |
00:02:26,870 --> 00:02:28,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
216 |
the number of nodes,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
217 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
218 |
49
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
219 |
00:02:28,310 --> 00:02:30,815
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
220 |
is also like nearly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
221 |
eight millions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
222 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
223 |
50
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
224 |
00:02:30,815 --> 00:02:33,845
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
225 |
And so even if that calculates
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
226 |
relatively quickly,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
227 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
228 |
51
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
229 |
00:02:33,845 --> 00:02:37,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
230 |
that is the reason why at 24,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
231 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
232 |
52
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
233 |
00:02:37,865 --> 00:02:39,560
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
234 |
it just runs out of memory.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
235 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
236 |
53
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
237 |
00:02:39,560 --> 00:02:42,785
|
774
|
238 |
This regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
239 |
just grew too much.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
240 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
241 |
54
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
242 |
00:02:42,785 --> 00:02:46,520
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
243 |
So we somehow need
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
244 |
to still compress
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
245 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
246 |
55
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
247 |
00:02:46,520 --> 00:02:49,655
|
774
|
248 |
this regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
249 |
and make it not
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
250 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
251 |
56
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
252 |
00:02:49,655 --> 00:02:52,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
253 |
grow so much when we
|
774
|
254 |
build the derivative.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
255 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
256 |
57
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
257 |
00:02:52,700 --> 00:02:54,020
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
258 |
So we have to look at
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
259 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
260 |
58
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
261 |
00:02:54,020 --> 00:02:57,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
262 |
where does that grow
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
263 |
actually come from.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
264 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
265 |
59
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
266 |
00:02:57,050 --> 00:03:00,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
267 |
Let's look at the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
268 |
derivative operation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
269 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
270 |
60
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
271 |
00:03:00,170 --> 00:03:01,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
272 |
again in more detail.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
273 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
274 |
61
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
275 |
00:03:01,895 --> 00:03:03,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
276 |
When we introduced
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
277 |
it, we looked at
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
278 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
279 |
62
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
280 |
00:03:03,740 --> 00:03:06,560
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
281 |
this example of a
|
774
|
282 |
regulat expression r,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
283 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
284 |
63
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
285 |
00:03:06,560 --> 00:03:11,465
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
286 |
which is a star of some
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
287 |
alternative and some sequence.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
288 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
289 |
64
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
290 |
00:03:11,465 --> 00:03:13,130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
291 |
And we can build now
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
292 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
293 |
65
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
294 |
00:03:13,130 --> 00:03:15,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
295 |
the derivative of this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
296 |
r according to a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
297 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
298 |
66
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
299 |
00:03:15,800 --> 00:03:18,965
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
300 |
b, and c and see
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
301 |
what it calculates.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
302 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
303 |
67
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
304 |
00:03:18,965 --> 00:03:21,935
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
305 |
And you see in case of a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
306 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
307 |
68
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
308 |
00:03:21,935 --> 00:03:26,570
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
309 |
it's like one times b plus
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
310 |
0 and then followed by r,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
311 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
312 |
69
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
313 |
00:03:26,570 --> 00:03:29,015
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
314 |
which is this whole
|
774
|
315 |
regular expression again.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
316 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
317 |
70
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
318 |
00:03:29,015 --> 00:03:30,935
|
774
|
319 |
So you can also see
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
320 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
321 |
71
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
322 |
00:03:30,935 --> 00:03:34,745
|
774
|
323 |
the derivative operation
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
324 |
introduces a lot of junk.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
325 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
326 |
72
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
327 |
00:03:34,745 --> 00:03:38,165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
328 |
This plus 0 isn't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
329 |
really necessary.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
330 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
331 |
73
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
332 |
00:03:38,165 --> 00:03:42,455
|
774
|
333 |
And this times 1 could
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
334 |
be also thrown away.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
335 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
336 |
74
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
337 |
00:03:42,455 --> 00:03:43,685
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
338 |
So in the first case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
339 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
340 |
75
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
341 |
00:03:43,685 --> 00:03:48,110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
342 |
actually we could just have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
343 |
one times b is b plus 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
344 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
345 |
76
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
346 |
00:03:48,110 --> 00:03:49,580
|
774
|
347 |
it still b,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
348 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
349 |
77
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
350 |
00:03:49,580 --> 00:03:54,905
|
774
|
351 |
so it would be b followed by
|
|
352 |
r. And in this second case,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
353 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
354 |
78
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
355 |
00:03:54,905 --> 00:03:57,515
|
774
|
356 |
0 times b, that will be just 0.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
357 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
358 |
79
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
359 |
00:03:57,515 --> 00:03:59,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
360 |
Then 0 plus one is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
361 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
362 |
80
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
363 |
00:03:59,270 --> 00:04:05,330
|
774
|
364 |
1 ... times r would be just
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
365 |
r. And in the last case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
366 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
367 |
81
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
368 |
00:04:05,330 --> 00:04:12,155
|
774
|
369 |
0 times b would be 0. 0 plus
|
|
370 |
0 is 0. 0 times r would be 0.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
371 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
372 |
82
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
373 |
00:04:12,155 --> 00:04:17,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
374 |
Okay? So we could throw out
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
375 |
all these useless zeros and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
376 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
377 |
83
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
378 |
00:04:17,540 --> 00:04:20,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
379 |
ones because actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
380 |
we have to throw
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
381 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
382 |
84
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
383 |
00:04:20,960 --> 00:04:24,845
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
384 |
them out because over time
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
385 |
they just accumulate.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
386 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
387 |
85
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
388 |
00:04:24,845 --> 00:04:27,035
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
389 |
And then we build
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
390 |
the next derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
391 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
392 |
86
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
393 |
00:04:27,035 --> 00:04:31,130
|
774
|
394 |
And the 0s wouldn't go away by
|
|
395 |
building a new derivative.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
396 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
397 |
87
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
398 |
00:04:31,130 --> 00:04:34,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
399 |
So we need to somehow
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
400 |
a mechanism to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
401 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
402 |
88
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
403 |
00:04:34,310 --> 00:04:39,120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
404 |
delete the junk from
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
405 |
these derivatives.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
406 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
407 |
89
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
408 |
00:04:39,280 --> 00:04:41,900
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
409 |
But how to delete junk?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
410 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
411 |
90
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
412 |
00:04:41,900 --> 00:04:43,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
413 |
We already know we have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
414 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
415 |
91
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
416 |
00:04:43,370 --> 00:04:47,825
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
417 |
the simplification rules
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
418 |
which say like if r plus 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
419 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
420 |
92
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
421 |
00:04:47,825 --> 00:04:53,000
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
422 |
I can just replace by
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
423 |
r and the other ones.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
424 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
425 |
93
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
426 |
00:04:53,000 --> 00:04:55,760
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
427 |
And so what I now
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
428 |
need to do is in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
429 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
430 |
94
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
431 |
00:04:55,760 --> 00:04:58,715
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
432 |
my algorithm when I
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
433 |
built the derivative,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
434 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
435 |
95
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
436 |
00:04:58,715 --> 00:05:01,415
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
437 |
this might have
|
774
|
438 |
introduced some junk.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
439 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
440 |
96
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
441 |
00:05:01,415 --> 00:05:02,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
442 |
And I now have to have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
443 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
444 |
97
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
445 |
00:05:02,960 --> 00:05:06,590
|
774
|
446 |
essentially an additional function
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
447 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
448 |
98
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
449 |
00:05:06,590 --> 00:05:08,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
450 |
which deletes this junk again.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
451 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
452 |
99
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
453 |
00:05:08,945 --> 00:05:10,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
454 |
And in doing so,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
455 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
456 |
100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
457 |
00:05:10,490 --> 00:05:13,340
|
774
|
458 |
keeps the regular expression,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
459 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
460 |
101
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
461 |
00:05:13,340 --> 00:05:16,730
|
774
|
462 |
relatively small, because that
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
463 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
464 |
102
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
465 |
00:05:16,730 --> 00:05:19,535
|
774
|
466 |
is the Achilles' heel
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
467 |
of this algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
468 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
469 |
103
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
470 |
00:05:19,535 --> 00:05:22,565
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
471 |
If this regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
472 |
grows too much,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
473 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
474 |
104
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
475 |
00:05:22,565 --> 00:05:25,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
476 |
then all these functions
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
477 |
will slow down.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
478 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
479 |
105
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
480 |
00:05:25,070 --> 00:05:26,360
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
481 |
So the purpose of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
482 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
483 |
106
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
484 |
00:05:26,360 --> 00:05:30,455
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
485 |
the simplification function
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
486 |
is to after the derivative,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
487 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
488 |
107
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
489 |
00:05:30,455 --> 00:05:33,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
490 |
compress again this
|
774
|
491 |
regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
492 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
493 |
108
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
494 |
00:05:33,080 --> 00:05:35,570
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
495 |
and then do the next derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
496 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
497 |
109
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
498 |
00:05:35,570 --> 00:05:39,815
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
499 |
So if we introduce that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
500 |
additional functions simp,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
501 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
502 |
110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
503 |
00:05:39,815 --> 00:05:42,440
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
504 |
which essentially
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
505 |
just goes through
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
506 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
507 |
111
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
508 |
00:05:42,440 --> 00:05:46,040
|
774
|
509 |
this regular expression and
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
510 |
deletes all this junk,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
511 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
512 |
112
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
513 |
00:05:46,040 --> 00:05:50,045
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
514 |
then we should be in a
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
515 |
much better position.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
516 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
517 |
113
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
518 |
00:05:50,045 --> 00:05:52,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
519 |
As you can see on this slide,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
520 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
521 |
114
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
522 |
00:05:52,490 --> 00:05:54,440
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
523 |
the simplification
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
524 |
function can actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
525 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
526 |
115
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
527 |
00:05:54,440 --> 00:05:56,855
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
528 |
be implemented very easily.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
529 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
530 |
116
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
531 |
00:05:56,855 --> 00:05:59,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
532 |
However, there are few
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
533 |
interesting points.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
534 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
535 |
117
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
536 |
00:05:59,750 --> 00:06:02,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
537 |
First of all, there
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
538 |
are only two cases.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
539 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
540 |
118
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
541 |
00:06:02,720 --> 00:06:05,060
|
774
|
542 |
We only simplify when we have
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
543 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
544 |
119
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
545 |
00:06:05,060 --> 00:06:08,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
546 |
an alternative or a sequence.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
547 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
548 |
120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
549 |
00:06:08,255 --> 00:06:12,859
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
550 |
So for example, we will
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
551 |
never simplify under star.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
552 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
553 |
121
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
554 |
00:06:12,859 --> 00:06:15,950
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
555 |
If you look at the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
556 |
derivative operation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
557 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
558 |
122
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
559 |
00:06:15,950 --> 00:06:17,825
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
560 |
and you scratch your
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
561 |
head a little bit,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
562 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
563 |
123
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
564 |
00:06:17,825 --> 00:06:20,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
565 |
we'll find out why
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
566 |
is that the case.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
567 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
568 |
124
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
569 |
00:06:20,180 --> 00:06:22,145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
570 |
It's essentially a waste of time.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
571 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
572 |
125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
573 |
00:06:22,145 --> 00:06:25,505
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
574 |
So you would not
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
575 |
simplify under star.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
576 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
577 |
126
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
578 |
00:06:25,505 --> 00:06:27,650
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
579 |
You only simplify if you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
580 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
581 |
127
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
582 |
00:06:27,650 --> 00:06:30,530
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
583 |
an alternative and the sequence.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
584 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
585 |
128
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
586 |
00:06:30,530 --> 00:06:34,880
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
587 |
Now, however, there
|
774
|
588 |
is one small point
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
589 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
590 |
129
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
591 |
00:06:34,880 --> 00:06:39,785
|
774
|
592 |
you have to be aware of.
|
|
593 |
These simplification rules
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
594 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
595 |
130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
596 |
00:06:39,785 --> 00:06:42,740
|
774
|
597 |
they need to be essentially
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
598 |
applied backwards.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
599 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
600 |
131
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
601 |
00:06:42,740 --> 00:06:45,650
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
602 |
So I have to first essentially
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
603 |
go to the leaves of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
604 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
605 |
132
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
606 |
00:06:45,650 --> 00:06:49,085
|
774
|
607 |
this regular expression and
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
608 |
then have to find out,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
609 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
610 |
133
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
611 |
00:06:49,085 --> 00:06:51,170
|
774
|
612 |
can I apply the simplification?
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
613 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
614 |
134
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
615 |
00:06:51,170 --> 00:06:52,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
616 |
And then if yes,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
617 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
618 |
135
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
619 |
00:06:52,670 --> 00:06:55,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
620 |
I apply the simplification
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
621 |
and I look at the next step,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
622 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
623 |
136
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
624 |
00:06:55,430 --> 00:06:57,815
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
625 |
can I now simplify
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
626 |
something more?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
627 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
628 |
137
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
629 |
00:06:57,815 --> 00:06:59,390
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
630 |
The reason is how
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
631 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
632 |
138
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
633 |
00:06:59,390 --> 00:07:03,125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
634 |
the simplification
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
635 |
rules are formulated.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
636 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
637 |
139
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
638 |
00:07:03,125 --> 00:07:05,300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
639 |
They might fire in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
640 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
641 |
140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
642 |
00:07:05,300 --> 00:07:08,765
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
643 |
a higher level if something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
644 |
simplifies below.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
645 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
646 |
141
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
647 |
00:07:08,765 --> 00:07:14,315
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
648 |
So we have to essentially
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
649 |
simplify from the inside out.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
650 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
651 |
142
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
652 |
00:07:14,315 --> 00:07:16,850
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
653 |
And in this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
654 |
simplification function,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
655 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
656 |
143
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
657 |
00:07:16,850 --> 00:07:20,885
|
774
|
658 |
what that means we're
|
|
659 |
matching this regular expression.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
660 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
661 |
144
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
662 |
00:07:20,885 --> 00:07:23,120
|
774
|
663 |
We test whether it's
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
664 |
an alternative or
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
665 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
666 |
145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
667 |
00:07:23,120 --> 00:07:26,345
|
774
|
668 |
a sequence. Only then we
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
669 |
actually go into action.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
670 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
671 |
146
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
672 |
00:07:26,345 --> 00:07:28,385
|
774
|
673 |
Once we know
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
674 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
675 |
147
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
676 |
00:07:28,385 --> 00:07:30,530
|
774
|
677 |
in case of an alternative,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
678 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
679 |
148
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
680 |
00:07:30,530 --> 00:07:32,120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
681 |
what are the two components?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
682 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
683 |
149
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
684 |
00:07:32,120 --> 00:07:35,765
|
774
|
685 |
We first, simplify each component,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
686 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
687 |
150
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
688 |
00:07:35,765 --> 00:07:39,095
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
689 |
okay, and then we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
690 |
get a result back.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
691 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
692 |
151
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
693 |
00:07:39,095 --> 00:07:41,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
694 |
And we check whether
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
695 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
696 |
152
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
697 |
00:07:41,180 --> 00:07:45,679
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
698 |
this simplification of
|
774
|
699 |
r1 resulted into a 0.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
700 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
701 |
153
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
702 |
00:07:45,679 --> 00:07:47,884
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
703 |
Then because it's an alternative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
704 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
705 |
154
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
706 |
00:07:47,884 --> 00:07:49,190
|
774
|
707 |
then I can just replace it
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
708 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
709 |
155
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
710 |
00:07:49,190 --> 00:07:53,375
|
774
|
711 |
by r2s, which a simplified
|
|
712 |
version of r2.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
713 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
714 |
156
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
715 |
00:07:53,375 --> 00:07:58,820
|
774
|
716 |
If it came back r2s
|
|
717 |
is actually 0,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
718 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
719 |
157
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
720 |
00:07:58,820 --> 00:08:00,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
721 |
then I can replace it by
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
722 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
723 |
158
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
724 |
00:08:00,410 --> 00:08:03,785
|
774
|
725 |
the simplified version of a r1.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
726 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
727 |
159
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
728 |
00:08:03,785 --> 00:08:07,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
729 |
If I simplify both
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
730 |
alternatives and it
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
731 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
732 |
160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
733 |
00:08:07,460 --> 00:08:11,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
734 |
happens that the simplified
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
735 |
versions are the same,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
736 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
737 |
161
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
738 |
00:08:11,180 --> 00:08:15,170
|
774
|
739 |
then I can throw away
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
740 |
one of the alternatives.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
741 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
742 |
162
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
743 |
00:08:15,170 --> 00:08:18,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
744 |
Otherwise, I just have to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
745 |
keep the alternatives,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
746 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
747 |
163
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
748 |
00:08:18,080 --> 00:08:21,155
|
774
|
749 |
but the simplified components.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
750 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
751 |
164
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
752 |
00:08:21,155 --> 00:08:23,915
|
774
|
753 |
In the sequence case it is
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
754 |
pretty much the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
755 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
756 |
165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
757 |
00:08:23,915 --> 00:08:27,950
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
758 |
I first have to check what
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
759 |
does it simplify underneath.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
760 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
761 |
166
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
762 |
00:08:27,950 --> 00:08:31,385
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
763 |
So I call first simplify
|
774
|
764 |
and then have a look...
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
765 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
766 |
167
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
767 |
00:08:31,385 --> 00:08:33,020
|
774
|
768 |
Does it matches 0 one of
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
769 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
770 |
168
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
771 |
00:08:33,020 --> 00:08:36,035
|
774
|
772 |
the simplifications,
|
|
773 |
then I just return 0.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
774 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
775 |
169
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
776 |
00:08:36,035 --> 00:08:38,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
777 |
Or if the other component is 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
778 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
779 |
170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
780 |
00:08:38,330 --> 00:08:40,535
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
781 |
I can also return a 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
782 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
783 |
171
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
784 |
00:08:40,535 --> 00:08:43,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
785 |
If it's one, then I keep
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
786 |
the other component.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
787 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
788 |
172
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
789 |
00:08:43,310 --> 00:08:45,920
|
774
|
790 |
And if the rs2 is one,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
791 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
792 |
173
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
793 |
00:08:45,920 --> 00:08:47,615
|
774
|
794 |
and I keep the first component.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
795 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
796 |
174
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
797 |
00:08:47,615 --> 00:08:50,359
|
774
|
798 |
And otherwise it's
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
799 |
still the sequence.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
800 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
801 |
175
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
802 |
00:08:50,359 --> 00:08:53,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
803 |
And in all the other cases I
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
804 |
don't have to do anything.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
805 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
806 |
176
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
807 |
00:08:53,540 --> 00:08:55,700
|
774
|
808 |
If it's just a plain
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
809 |
0. I leave it in.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
810 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
811 |
177
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
812 |
00:08:55,700 --> 00:08:57,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
813 |
If it's a plain
|
774
|
814 |
1, I leave it in.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
815 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
816 |
178
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
817 |
00:08:57,860 --> 00:09:00,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
818 |
And if something is under a star,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
819 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
820 |
179
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
821 |
00:09:00,170 --> 00:09:02,840
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
822 |
I don't open up this
|
774
|
823 |
star and simplify it.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
824 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
825 |
180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
826 |
00:09:02,840 --> 00:09:06,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
827 |
I just apply that to be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
828 |
as quick as possible.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
829 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
830 |
181
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
831 |
00:09:06,680 --> 00:09:10,280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
832 |
Let's see whether this has
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
833 |
any effect on our code.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
834 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
835 |
182
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
836 |
00:09:10,280 --> 00:09:12,980
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
837 |
So I'm now in the
|
774
|
838 |
file re3.sc,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
839 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
840 |
183
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
841 |
00:09:12,980 --> 00:09:17,405
|
774
|
842 |
and it's the same as re2.sc.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
843 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
844 |
184
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
845 |
00:09:17,405 --> 00:09:20,885
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
846 |
It still has this
|
774
|
847 |
explicit and n-times case,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
848 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
849 |
185
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
850 |
00:09:20,885 --> 00:09:24,665
|
774
|
851 |
nullable and derivative are
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
852 |
still the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
853 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
854 |
186
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
855 |
00:09:24,665 --> 00:09:28,610
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
856 |
Except now we have this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
857 |
simplification function as well.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
858 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
859 |
187
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
860 |
00:09:28,610 --> 00:09:29,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
861 |
And when we apply
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
862 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
863 |
188
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
864 |
00:09:29,960 --> 00:09:33,725
|
774
|
865 |
the derivative and after
|
|
866 |
we apply the derivative,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
867 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
868 |
189
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
869 |
00:09:33,725 --> 00:09:35,870
|
774
|
870 |
we simplify it to throw away
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
871 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
872 |
190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
873 |
00:09:35,870 --> 00:09:39,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
874 |
all the junk this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
875 |
derivative introduced.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
876 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
877 |
191
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
878 |
00:09:39,050 --> 00:09:41,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
879 |
Otherwise everything
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
880 |
stays the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
881 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
882 |
192
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
883 |
00:09:41,510 --> 00:09:43,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
884 |
You still have this expansion
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
885 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
886 |
193
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
887 |
00:09:43,580 --> 00:09:45,515
|
774
|
888 |
of the optional regular expression.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
889 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
890 |
194
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
891 |
00:09:45,515 --> 00:09:49,670
|
774
|
892 |
Here are our two EVIL regular
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
893 |
expressions we use as a test.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
894 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
895 |
195
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
896 |
00:09:49,670 --> 00:09:52,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
897 |
And here's now this test case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
898 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
899 |
196
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
900 |
00:09:52,460 --> 00:09:55,835
|
774
|
901 |
the first one and we're
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
902 |
actually now trying it
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
903 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
904 |
197
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
905 |
00:09:55,835 --> 00:10:00,515
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
906 |
out for strings between
|
774
|
907 |
0 and 9000 a's.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
908 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
909 |
198
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
910 |
00:10:00,515 --> 00:10:08,285
|
774
|
911 |
So let's see. So also the
|
|
912 |
simplification makes
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
913 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
914 |
199
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
915 |
00:10:08,285 --> 00:10:10,655
|
774
|
916 |
actually this case faster.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
917 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
918 |
200
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
919 |
00:10:10,655 --> 00:10:16,260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
920 |
So we can now run strings
|
774
|
921 |
up to 9000.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
922 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
923 |
201
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
924 |
00:10:16,260 --> 00:10:19,360
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
925 |
And we don't actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
926 |
sweat about this at all.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
927 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
928 |
202
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
929 |
00:10:19,360 --> 00:10:24,745
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
930 |
For I have to say my laptop
|
774
|
931 |
is now starting to run its fan.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
932 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
933 |
203
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
934 |
00:10:24,745 --> 00:10:28,525
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
935 |
And also, because the times
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
936 |
are relatively small,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
937 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
938 |
204
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
939 |
00:10:28,525 --> 00:10:30,610
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
940 |
I'm actually running
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
941 |
each test three
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
942 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
943 |
205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
944 |
00:10:30,610 --> 00:10:32,785
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
945 |
times and then take the average,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
946 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
947 |
206
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
948 |
00:10:32,785 --> 00:10:34,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
949 |
which I didn't do before,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
950 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
951 |
207
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
952 |
00:10:34,720 --> 00:10:37,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
953 |
just to be a tiny bit
|
774
|
954 |
more accurate.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
955 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
956 |
208
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
957 |
00:10:37,720 --> 00:10:42,025
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
958 |
So three seconds for a
|
774
|
959 |
string of 9000 a's.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
960 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
961 |
209
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
962 |
00:10:42,025 --> 00:10:44,980
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
963 |
And now the more
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
964 |
interesting question is,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
965 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
966 |
210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
967 |
00:10:44,980 --> 00:10:46,240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
968 |
for the second case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
969 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
970 |
211
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
971 |
00:10:46,240 --> 00:10:48,625
|
774
|
972 |
this a star, star, b.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
973 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
974 |
212
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
975 |
00:10:48,625 --> 00:10:51,250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
976 |
And you can already see
|
774
|
977 |
on these numbers...
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
978 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
979 |
213
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
980 |
00:10:51,250 --> 00:10:53,260
|
774
|
981 |
we are really ambitious.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
982 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
983 |
214
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
984 |
00:10:53,260 --> 00:10:57,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
985 |
And let's see how our
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
986 |
program is coping with that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
987 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
988 |
215
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
989 |
00:11:02,610 --> 00:11:07,780
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
990 |
Again. No sweat, at
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
991 |
least not on my part.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
992 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
993 |
216
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
994 |
00:11:07,780 --> 00:11:10,480
|
774
|
995 |
The laptop has to
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
996 |
calculate quite a bit.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
997 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
998 |
217
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
999 |
00:11:10,480 --> 00:11:12,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1000 |
But this is now a string of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1001 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1002 |
218
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1003 |
00:11:12,940 --> 00:11:16,539
|
774
|
1004 |
3 million a's and
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1005 |
it needs a second.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1006 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1007 |
219
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1008 |
00:11:16,539 --> 00:11:20,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1009 |
And let's see how far we get.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1010 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1011 |
220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1012 |
00:11:20,680 --> 00:11:25,280
|
774
|
1013 |
4 million a's around two seconds.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1014 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1015 |
221
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1016 |
00:11:27,030 --> 00:11:29,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1017 |
So say it again,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1018 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1019 |
222
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1020 |
00:11:29,050 --> 00:11:31,690
|
774
|
1021 |
I'm actually slowing it down
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1022 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1023 |
223
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1024 |
00:11:31,690 --> 00:11:34,150
|
774
|
1025 |
here artificially with running the test
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1026 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1027 |
224
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1028 |
00:11:34,150 --> 00:11:36,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1029 |
three times and then
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1030 |
take the average.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1031 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1032 |
225
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1033 |
00:11:36,895 --> 00:11:42,749
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1034 |
But it seems to be something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1035 |
less than five seconds.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1036 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1037 |
226
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1038 |
00:11:42,749 --> 00:11:48,185
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1039 |
And remember that is a
|
774
|
1040 |
string of 6 million a's.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1041 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1042 |
227
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1043 |
00:11:48,185 --> 00:11:51,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1044 |
Let's just have a
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1045 |
look at the graphs.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1046 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1047 |
228
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1048 |
00:11:51,170 --> 00:11:56,105
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1049 |
So the simplification also
|
774
|
1050 |
made our first case faster.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1051 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1052 |
229
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1053 |
00:11:56,105 --> 00:11:58,880
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1054 |
So earlier without
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1055 |
simplification,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1056 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1057 |
230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1058 |
00:11:58,880 --> 00:12:00,710
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1059 |
where we just have
|
774
|
1060 |
this explicit
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1061 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1062 |
231
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1063 |
00:12:00,710 --> 00:12:03,050
|
774
|
1064 |
n-times. That is this graph.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1065 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1066 |
232
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1067 |
00:12:03,050 --> 00:12:05,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1068 |
And now we can go up to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1069 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1070 |
233
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1071 |
00:12:05,210 --> 00:12:09,620
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1072 |
10 thousand and be still
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1073 |
under five seconds.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1074 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1075 |
234
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1076 |
00:12:09,620 --> 00:12:12,300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1077 |
So that is good news.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1078 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1079 |
235
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1080 |
00:12:13,270 --> 00:12:16,745
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1081 |
In the other example, remember,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1082 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1083 |
236
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1084 |
00:12:16,745 --> 00:12:19,220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1085 |
the existing regular
|
774
|
1086 |
expression matchers in
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1087 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1088 |
237
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1089 |
00:12:19,220 --> 00:12:22,880
|
774
|
1090 |
Java 8, Python,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1091 |
and JavaScript.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1092 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1093 |
238
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1094 |
00:12:22,880 --> 00:12:26,030
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1095 |
And thanks to the
|
774
|
1096 |
student we also
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1097 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1098 |
239
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1099 |
00:12:26,030 --> 00:12:27,935
|
774
|
1100 |
have a graph for Swift.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1101 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1102 |
240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1103 |
00:12:27,935 --> 00:12:29,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1104 |
They're pretty atrocious.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1105 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1106 |
241
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1107 |
00:12:29,750 --> 00:12:33,320
|
774
|
1108 |
They need like for 30 a's,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1109 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1110 |
242
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1111 |
00:12:33,320 --> 00:12:37,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1112 |
something like on the
|
774
|
1113 |
magnitude of 30 seconds.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1114 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1115 |
243
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1116 |
00:12:37,490 --> 00:12:39,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1117 |
As I said already,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1118 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1119 |
244
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1120 |
00:12:39,740 --> 00:12:42,665
|
774
|
1121 |
Java 9 is slightly better.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1122 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1123 |
245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1124 |
00:12:42,665 --> 00:12:44,870
|
774
|
1125 |
Java 9 and above,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1126 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1127 |
246
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1128 |
00:12:44,870 --> 00:12:46,220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1129 |
if you try that example,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1130 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1131 |
247
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1132 |
00:12:46,220 --> 00:12:48,665
|
774
|
1133 |
the same example in Java 9,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1134 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1135 |
248
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1136 |
00:12:48,665 --> 00:12:51,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1137 |
you would be able to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1138 |
process something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1139 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1140 |
249
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1141 |
00:12:51,230 --> 00:12:54,215
|
774
|
1142 |
like 40 thousand a's
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1143 |
in half a minute.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1144 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1145 |
250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1146 |
00:12:54,215 --> 00:12:57,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1147 |
I have to admit I'm not
|
774
|
1148 |
100% sure what they
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1149 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1150 |
251
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1151 |
00:12:57,740 --> 00:13:03,575
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1152 |
did to improve the
|
774
|
1153 |
performance between Java 8 and 9.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1154 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1155 |
252
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1156 |
00:13:03,575 --> 00:13:05,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1157 |
I know they did something on
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1158 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1159 |
253
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1160 |
00:13:05,510 --> 00:13:07,790
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1161 |
their regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1162 |
matching engine,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1163 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1164 |
254
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1165 |
00:13:07,790 --> 00:13:09,770
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1166 |
but I haven't really looked
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1167 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1168 |
255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1169 |
00:13:09,770 --> 00:13:12,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1170 |
at what precisely they've done.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1171 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1172 |
256
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1173 |
00:13:12,230 --> 00:13:17,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1174 |
But that's still not
|
774
|
1175 |
really a competition for us.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1176 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1177 |
257
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1178 |
00:13:17,945 --> 00:13:20,915
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1179 |
So our third version,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1180 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1181 |
258
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1182 |
00:13:20,915 --> 00:13:24,335
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1183 |
in this example, a star, star b.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1184 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1185 |
259
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1186 |
00:13:24,335 --> 00:13:28,445
|
774
|
1187 |
We said for something like
|
|
1188 |
6 million a's we need 15 secs.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1189 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1190 |
260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1191 |
00:13:28,445 --> 00:13:31,760
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1192 |
And again, I think these
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1193 |
are slightly older times,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1194 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1195 |
261
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1196 |
00:13:31,760 --> 00:13:33,770
|
774
|
1197 |
so here it needs 20 seconds.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1198 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1199 |
262
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1200 |
00:13:33,770 --> 00:13:37,250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1201 |
I think we had something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1202 |
like below five seconds.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1203 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1204 |
263
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1205 |
00:13:37,250 --> 00:13:40,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1206 |
But again, you can see
|
774
|
1207 |
the trends. We run.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1208 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1209 |
264
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1210 |
00:13:40,865 --> 00:13:42,590
|
774
|
1211 |
circles around them.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1212 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1213 |
265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1214 |
00:13:42,590 --> 00:13:46,530
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1215 |
And that's quite nice.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1216 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1217 |
266
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1218 |
00:13:46,570 --> 00:13:49,774
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1219 |
So what's good about
|
774
|
1220 |
this algorithm
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1221 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1222 |
267
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1223 |
00:13:49,774 --> 00:13:51,605
|
774
|
1224 |
by Brzozowski?
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1225 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1226 |
268
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1227 |
00:13:51,605 --> 00:13:54,500
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1228 |
Well, first, it extends
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1229 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1230 |
269
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1231 |
00:13:54,500 --> 00:13:57,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1232 |
actually to quite a number
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1233 |
of regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1234 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1235 |
270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1236 |
00:13:57,800 --> 00:13:59,900
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1237 |
So we saw in this example
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1238 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1239 |
271
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1240 |
00:13:59,900 --> 00:14:03,950
|
774
|
1241 |
the n-times regular expression.
|
|
1242 |
Is a little bit of work, but
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1243 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1244 |
272
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1245 |
00:14:03,950 --> 00:14:05,405
|
774
|
1246 |
we could extend that.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1247 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1248 |
273
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1249 |
00:14:05,405 --> 00:14:08,480
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1250 |
It also extends to the
|
774
|
1251 |
not regular expression,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1252 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1253 |
274
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1254 |
00:14:08,480 --> 00:14:10,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1255 |
which I explain on
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1256 |
the next slide.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1257 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1258 |
275
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1259 |
00:14:10,820 --> 00:14:15,290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1260 |
It's very easy to implement
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1261 |
in a functional language.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1262 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1263 |
276
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1264 |
00:14:15,290 --> 00:14:16,610
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1265 |
If you don't buy
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1266 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1267 |
277
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1268 |
00:14:16,610 --> 00:14:20,675
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1269 |
all that functional
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1270 |
programming language stuff,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1271 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1272 |
278
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1273 |
00:14:20,675 --> 00:14:22,955
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1274 |
you still have to agree.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1275 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1276 |
279
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1277 |
00:14:22,955 --> 00:14:25,715
|
774
|
1278 |
It's quite beautiful in Scala.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1279 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1280 |
280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1281 |
00:14:25,715 --> 00:14:28,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1282 |
And you could also
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1283 |
easily implemented
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1284 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1285 |
281
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1286 |
00:14:28,160 --> 00:14:31,760
|
774
|
1287 |
in the C language or in Python.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1288 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1289 |
282
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1290 |
00:14:31,760 --> 00:14:34,250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1291 |
There's really no
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1292 |
problem with that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1293 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1294 |
283
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1295 |
00:14:34,250 --> 00:14:38,390
|
774
|
1296 |
The algorithm is actually
|
|
1297 |
quite old already.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1298 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1299 |
284
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1300 |
00:14:38,390 --> 00:14:44,899
|
774
|
1301 |
Brzozowski wrote it down in
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1302 |
1964 and his PhD thesis.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1303 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1304 |
285
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1305 |
00:14:44,899 --> 00:14:49,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1306 |
Somehow it was forgotten during
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1307 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1308 |
286
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1309 |
00:14:49,460 --> 00:14:54,095
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1310 |
the next decades and only
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1311 |
recently has been rediscovered.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1312 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1313 |
287
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1314 |
00:14:54,095 --> 00:14:57,065
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1315 |
At the moment, we are
|
774
|
1316 |
only solved the problem
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1317 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1318 |
288
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1319 |
00:14:57,065 --> 00:15:02,240
|
774
|
1320 |
of given a regular expression,
|
|
1321 |
givven a string, does
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1322 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1323 |
289
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1324 |
00:15:02,240 --> 00:15:05,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1325 |
the regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1326 |
match the string yes or no.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1327 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1328 |
290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1329 |
00:15:05,550 --> 00:15:08,740
|
774
|
1330 |
We want to of course, use
|
|
1331 |
it as part of our lexer.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1332 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1333 |
291
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1334 |
00:15:08,740 --> 00:15:12,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1335 |
And there we have to do
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1336 |
something more complicated.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1337 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1338 |
292
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1339 |
00:15:12,370 --> 00:15:15,384
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1340 |
We have to essentially
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1341 |
generate tokens.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1342 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1343 |
293
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1344 |
00:15:15,384 --> 00:15:18,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1345 |
And this will still take
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1346 |
a little bit of work.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1347 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1348 |
294
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1349 |
00:15:18,670 --> 00:15:22,045
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1350 |
And that's actually relatively
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1351 |
recent work by somebody
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1352 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1353 |
295
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1354 |
00:15:22,045 --> 00:15:26,110
|
774
|
1355 |
called Sulzmann and
|
|
1356 |
the co-worker called Lu.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1357 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1358 |
296
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1359 |
00:15:26,110 --> 00:15:30,880
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1360 |
And what I personally
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1361 |
also find very satisfying
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1362 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1363 |
297
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1364 |
00:15:30,880 --> 00:15:32,695
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1365 |
about this algorithm is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1366 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1367 |
298
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1368 |
00:15:32,695 --> 00:15:36,040
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1369 |
that we can actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1370 |
prove that it's correct.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1371 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1372 |
299
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1373 |
00:15:36,040 --> 00:15:37,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1374 |
You might remember I did
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1375 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1376 |
300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1377 |
00:15:37,735 --> 00:15:41,500
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1378 |
quite some interesting
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1379 |
transformations
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1380 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1381 |
301
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1382 |
00:15:41,500 --> 00:15:44,830
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1383 |
when I calculated the derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1384 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1385 |
302
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1386 |
00:15:44,830 --> 00:15:48,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1387 |
How can I be sure that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1388 |
this is all correct?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1389 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1390 |
303
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1391 |
00:15:48,270 --> 00:15:50,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1392 |
Actually, I can now go away and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1393 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1394 |
304
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1395 |
00:15:50,270 --> 00:15:52,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1396 |
prove the correctness
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1397 |
of this algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1398 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1399 |
305
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1400 |
00:15:52,865 --> 00:15:56,645
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1401 |
Does it really satisfy
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1402 |
the specification?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1403 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1404 |
306
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1405 |
00:15:56,645 --> 00:15:58,550
|
774
|
1406 |
Is it really true that if a string
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1407 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1408 |
307
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1409 |
00:15:58,550 --> 00:16:00,440
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1410 |
is in the language
|
774
|
1411 |
of a regular expression.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1412 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1413 |
308
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1414 |
00:16:00,440 --> 00:16:03,050
|
774
|
1415 |
Does that matter? I would say yes.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1416 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1417 |
309
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1418 |
00:16:03,050 --> 00:16:07,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1419 |
However, I leave that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1420 |
for another video.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1421 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1422 |
310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1423 |
00:16:07,070 --> 00:16:10,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1424 |
What I also like about
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1425 |
this algorithm that can be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1426 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1427 |
311
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1428 |
00:16:10,580 --> 00:16:13,775
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1429 |
actually extended to quite a
|
774
|
1430 |
number of regular expressions.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1431 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1432 |
312
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1433 |
00:16:13,775 --> 00:16:17,810
|
774
|
1434 |
So this is the NOT regular
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1435 |
expression that is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1436 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1437 |
313
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1438 |
00:16:17,810 --> 00:16:19,760
|
774
|
1439 |
supposed to match strings which
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1440 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1441 |
314
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1442 |
00:16:19,760 --> 00:16:22,235
|
774
|
1443 |
this regular expression cannot match.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1444 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1445 |
315
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1446 |
00:16:22,235 --> 00:16:24,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1447 |
So here's an example.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1448 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1449 |
316
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1450 |
00:16:24,245 --> 00:16:28,640
|
774
|
1451 |
If you're in the business of
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1452 |
trying to find out what
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1453 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1454 |
317
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1455 |
00:16:28,640 --> 00:16:33,530
|
774
|
1456 |
are comments in languages like
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1457 |
Java or C. Then you know,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1458 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1459 |
318
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1460 |
00:16:33,530 --> 00:16:35,060
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1461 |
they always start with a slash,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1462 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1463 |
319
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1464 |
00:16:35,060 --> 00:16:36,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1465 |
then comes a star,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1466 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1467 |
320
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1468 |
00:16:36,245 --> 00:16:38,240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1469 |
then comes an arbitrary string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1470 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1471 |
321
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1472 |
00:16:38,240 --> 00:16:41,195
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1473 |
And then they finish
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1474 |
with a slash and a star.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1475 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1476 |
322
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1477 |
00:16:41,195 --> 00:16:44,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1478 |
And how you want to specify
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1479 |
that is something like this.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1480 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1481 |
323
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1482 |
00:16:44,330 --> 00:16:45,530
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1483 |
You want to say, OK,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1484 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1485 |
324
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1486 |
00:16:45,530 --> 00:16:48,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1487 |
a comment starts with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1488 |
a slash and a star.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1489 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1490 |
325
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1491 |
00:16:48,245 --> 00:16:51,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1492 |
Then it comes any
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1493 |
string in between.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1494 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1495 |
326
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1496 |
00:16:51,410 --> 00:16:55,340
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1497 |
But this string
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1498 |
in-between cannot contain
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1499 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1500 |
327
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1501 |
00:16:55,340 --> 00:16:58,280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1502 |
any star and slash
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1503 |
because that would then
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1504 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1505 |
328
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1506 |
00:16:58,280 --> 00:17:01,415
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1507 |
indicate there's the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1508 |
end already there.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1509 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1510 |
329
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1511 |
00:17:01,415 --> 00:17:03,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1512 |
And then after you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1513 |
have such a string
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1514 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1515 |
330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1516 |
00:17:03,680 --> 00:17:06,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1517 |
which doesn't
|
774
|
1518 |
contain a star and a slash,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1519 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1520 |
331
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1521 |
00:17:06,410 --> 00:17:11,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1522 |
then at the end you want to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1523 |
match a star and a slash.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1524 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1525 |
332
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1526 |
00:17:11,180 --> 00:17:13,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1527 |
So for these kind of comments,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1528 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1529 |
333
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1530 |
00:17:13,460 --> 00:17:15,995
|
774
|
1531 |
this regular expression is
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1532 |
actually quite useful.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1533 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1534 |
334
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1535 |
00:17:15,995 --> 00:17:19,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1536 |
And if you ever seen
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1537 |
how to do the negation,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1538 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1539 |
335
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1540 |
00:17:19,430 --> 00:17:21,995
|
774
|
1541 |
for this kind of regular
|
|
1542 |
expression with automata,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1543 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1544 |
336
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1545 |
00:17:21,995 --> 00:17:24,710
|
774
|
1546 |
you will know that's
|
|
1547 |
a bit of a pain.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1548 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1549 |
337
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1550 |
00:17:24,710 --> 00:17:26,675
|
774
|
1551 |
But for the Brzozowski,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1552 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1553 |
338
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1554 |
00:17:26,675 --> 00:17:28,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1555 |
it's no pain at all.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1556 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1557 |
339
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1558 |
00:17:28,370 --> 00:17:30,710
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1559 |
The meaning of this
|
774
|
1560 |
regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1561 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1562 |
340
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1563 |
00:17:30,710 --> 00:17:32,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1564 |
would be something like that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1565 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1566 |
341
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1567 |
00:17:32,255 --> 00:17:35,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1568 |
If I have all the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1569 |
strings there are,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1570 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1571 |
342
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1572 |
00:17:35,540 --> 00:17:38,390
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1573 |
and I take away all the strings,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1574 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1575 |
343
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1576 |
00:17:38,390 --> 00:17:40,055
|
774
|
1577 |
this r can match.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1578 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1579 |
344
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1580 |
00:17:40,055 --> 00:17:42,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1581 |
The remaining strings are
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1582 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1583 |
345
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1584 |
00:17:42,080 --> 00:17:44,630
|
774
|
1585 |
what this regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1586 |
is supposed to match.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1587 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1588 |
346
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1589 |
00:17:44,630 --> 00:17:47,165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1590 |
So I can specify
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1591 |
what the meaning is.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1592 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1593 |
347
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1594 |
00:17:47,165 --> 00:17:49,760
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1595 |
And then it's also very easy to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1596 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1597 |
348
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1598 |
00:17:49,760 --> 00:17:52,174
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1599 |
say what is nullable
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1600 |
and derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1601 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1602 |
349
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1603 |
00:17:52,174 --> 00:17:54,140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1604 |
So for nullable, it would be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1605 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1606 |
350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1607 |
00:17:54,140 --> 00:17:56,570
|
774
|
1608 |
just a test whether r
|
|
1609 |
is nullable.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1610 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1611 |
351
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1612 |
00:17:56,570 --> 00:17:58,985
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1613 |
And I just take the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1614 |
negation of that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1615 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1616 |
352
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1617 |
00:17:58,985 --> 00:18:00,680
|
774
|
1618 |
And then I have to build
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1619 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1620 |
353
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1621 |
00:18:00,680 --> 00:18:03,620
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1622 |
the derivative of this
|
774
|
1623 |
NOT regular expression.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1624 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1625 |
354
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1626 |
00:18:03,620 --> 00:18:05,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1627 |
Then I just have to move
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1628 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1629 |
355
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1630 |
00:18:05,420 --> 00:18:07,325
|
774
|
1631 |
this ....
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1632 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1633 |
356
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1634 |
00:18:07,325 --> 00:18:10,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1635 |
derivative inside
|
774
|
1636 |
the regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1637 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1638 |
357
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1639 |
00:18:10,070 --> 00:18:12,575
|
774
|
1640 |
and keep the NOT on
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1641 |
the outermost level.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1642 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1643 |
358
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1644 |
00:18:12,575 --> 00:18:15,515
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1645 |
So there's again no
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1646 |
pain involved in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1647 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1648 |
359
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1649 |
00:18:15,515 --> 00:18:19,130
|
774
|
1650 |
adding this regular expression
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1651 |
to the algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1652 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1653 |
360
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1654 |
00:18:19,130 --> 00:18:22,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1655 |
We made it to the end of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1656 |
this video and we made
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1657 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1658 |
361
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1659 |
00:18:22,100 --> 00:18:24,739
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1660 |
it also to the end
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1661 |
of this algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1662 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1663 |
362
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1664 |
00:18:24,739 --> 00:18:27,620
|
774
|
1665 |
I can see to loose strands.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1666 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1667 |
363
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1668 |
00:18:27,620 --> 00:18:29,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1669 |
One is we implemented
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1670 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1671 |
364
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1672 |
00:18:29,420 --> 00:18:32,855
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1673 |
this algorithm for the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1674 |
basic regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1675 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1676 |
365
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1677 |
00:18:32,855 --> 00:18:38,705
|
774
|
1678 |
And we also added the
|
|
1679 |
n-times out of necessity.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1680 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1681 |
366
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1682 |
00:18:38,705 --> 00:18:41,120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1683 |
And I also showed
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1684 |
you how to implement
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1685 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1686 |
367
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1687 |
00:18:41,120 --> 00:18:44,840
|
774
|
1688 |
the NOT regular
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1689 |
expression on a slide.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1690 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1691 |
368
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1692 |
00:18:44,840 --> 00:18:48,995
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1693 |
But your task in the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1694 |
coursework actually is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1695 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1696 |
369
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1697 |
00:18:48,995 --> 00:18:52,970
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1698 |
to extend that to some of
|
774
|
1699 |
the extended regular expressions.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1700 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1701 |
370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1702 |
00:18:52,970 --> 00:18:57,260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1703 |
So especially these bounded
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1704 |
repetitions like from 0 to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1705 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1706 |
371
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1707 |
00:18:57,260 --> 00:19:01,550
|
774
|
1708 |
n-times or between n and m times.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1709 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1710 |
372
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1711 |
00:19:01,550 --> 00:19:04,325
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1712 |
And I think also
|
774
|
1713 |
plus and option.
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1714 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1715 |
373
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1716 |
00:19:04,325 --> 00:19:07,220
|
774
|
1717 |
The other loose strand is,
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1718 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1719 |
374
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1720 |
00:19:07,220 --> 00:19:09,200
|
774
|
1721 |
remember I did this wild
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1722 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1723 |
375
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1724 |
00:19:09,200 --> 00:19:11,645
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1725 |
calculations with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1726 |
regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1727 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1728 |
376
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1729 |
00:19:11,645 --> 00:19:13,205
|
774
|
1730 |
Why on earth
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1731 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1732 |
377
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1733 |
00:19:13,205 --> 00:19:14,480
|
774
|
1734 |
is that all correct?
|
773
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1735 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1736 |
378
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1737 |
00:19:14,480 --> 00:19:16,355
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1738 |
Why on earth should
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1739 |
this algorithm
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1740 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1741 |
379
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1742 |
00:19:16,355 --> 00:19:18,575
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1743 |
actually satisfy
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1744 |
our specification,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1745 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1746 |
380
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1747 |
00:19:18,575 --> 00:19:20,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1748 |
which we set out
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1749 |
at the beginning.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1750 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1751 |
381
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1752 |
00:19:20,450 --> 00:19:25,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1753 |
So that needs to be looked at
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1754 |
more closely. Bye for now.
|