769
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,020 --> 00:00:09,945
|
772
|
3 |
Welcome back. After
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
this disappointment
|
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:09,945 --> 00:00:14,115
|
772
|
8 |
and case of over-promising
|
|
9 |
and under-achieving,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
3
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
00:00:14,115 --> 00:00:17,295
|
772
|
13 |
let's have a look whether
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
we can recover from that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
4
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
00:00:17,295 --> 00:00:20,535
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
So here's one problem.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
5
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
00:00:20,535 --> 00:00:23,790
|
772
|
22 |
When we looked at this
|
|
23 |
n-times regular expression, we
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
6
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
00:00:23,790 --> 00:00:27,330
|
772
|
27 |
were not able to represent
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
28 |
that directly.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
30 |
7
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
00:00:27,330 --> 00:00:31,275
|
772
|
32 |
We had to represent it as a
|
|
33 |
sequence regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
8
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
36 |
00:00:31,275 --> 00:00:32,850
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
So we expanded it.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
9
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
00:00:32,850 --> 00:00:36,510
|
772
|
41 |
So times-one would be just a,
|
769
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:36,510 --> 00:00:40,595
|
772
|
45 |
times-two would
|
|
46 |
be a o a, and so on.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
47 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
48 |
11
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
49 |
00:00:40,595 --> 00:00:43,535
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
And so you can see if
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
you go already to 13,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
12
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
00:00:43,535 --> 00:00:47,960
|
772
|
55 |
n equals 13, the regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
expression becomes quite large.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
58 |
13
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
00:00:47,960 --> 00:00:52,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
60 |
And now the functions
|
772
|
61 |
nullable and also derivative,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
62 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
14
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
64 |
00:00:52,865 --> 00:00:56,360
|
772
|
65 |
they need to traverse
|
|
66 |
this regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
67 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
68 |
15
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
69 |
00:00:56,360 --> 00:00:59,060
|
772
|
70 |
Remember this tree, sometimes,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
71 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
16
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
73 |
00:00:59,060 --> 00:01:01,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
74 |
they have to traverse
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
75 |
that even several times.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
76 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
17
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
78 |
00:01:01,820 --> 00:01:04,535
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
So that will slow
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
80 |
down the algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
81 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
82 |
18
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
00:01:04,535 --> 00:01:08,150
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
And in particular, because
|
772
|
85 |
our first regular expression was
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
19
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
00:01:08,150 --> 00:01:11,840
|
772
|
89 |
actually not just a, but
|
|
90 |
a + 1. So we had
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
92 |
20
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
00:01:11,840 --> 00:01:14,330
|
772
|
94 |
in the case of 13,
|
|
95 |
we had a + 1, a + 1,...
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
21
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
00:01:14,330 --> 00:01:17,330
|
772
|
99 |
a + 1... 13 times.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
22
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
00:01:17,330 --> 00:01:20,150
|
772
|
103 |
And this regular
|
|
104 |
expression just grows
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
23
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
00:01:20,150 --> 00:01:25,475
|
772
|
108 |
with the number n. Just to
|
|
109 |
show you this also in code,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
24
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
00:01:25,475 --> 00:01:28,115
|
772
|
113 |
I'm in the file re1.sc,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
25
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
00:01:28,115 --> 00:01:30,920
|
772
|
117 |
and in the end I have a size function.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
26
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
120 |
00:01:30,920 --> 00:01:33,140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
121 |
The size function takes
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
122 |
a regular expression as
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
123 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
124 |
27
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
125 |
00:01:33,140 --> 00:01:36,215
|
772
|
126 |
argument and produces an integer.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
127 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
128 |
28
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
129 |
00:01:36,215 --> 00:01:39,980
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
130 |
And essentially it takes
|
772
|
131 |
this regular expression, seen as
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
132 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
133 |
29
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
134 |
00:01:39,980 --> 00:01:44,045
|
772
|
135 |
a tree and counts how many
|
|
136 |
nodes there are in this tree.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
137 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
138 |
30
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
139 |
00:01:44,045 --> 00:01:49,490
|
772
|
140 |
And so if I take this EVIL1
|
|
141 |
regular expression, this one,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
142 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
143 |
31
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
144 |
00:01:49,490 --> 00:01:52,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
145 |
and increase now this n. So you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
146 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
147 |
32
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
148 |
00:01:52,160 --> 00:01:54,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
149 |
can already see
|
772
|
150 |
for n = 1,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
151 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
152 |
33
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
153 |
00:01:54,680 --> 00:01:56,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
154 |
the size of this
|
772
|
155 |
record expression is 5
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
156 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
157 |
34
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
158 |
00:01:56,540 --> 00:01:59,615
|
772
|
159 |
and you see it
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
160 |
slowly increases.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
161 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
162 |
35
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
163 |
00:01:59,615 --> 00:02:02,150
|
772
|
164 |
And this 20, i.e. n = 20,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
165 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
166 |
36
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
167 |
00:02:02,150 --> 00:02:07,100
|
772
|
168 |
the size of this regular
|
|
169 |
expression is now already 119.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
170 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
171 |
37
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
172 |
00:02:07,100 --> 00:02:10,145
|
772
|
173 |
The interesting
|
|
174 |
line is this one.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
175 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
176 |
38
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
177 |
00:02:10,145 --> 00:02:13,295
|
772
|
178 |
Remember, when we
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
179 |
built the derivative,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
180 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
181 |
39
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
182 |
00:02:13,295 --> 00:02:17,150
|
772
|
183 |
very often parts of a regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
184 |
expression gets copied.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
185 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
186 |
40
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
187 |
00:02:17,150 --> 00:02:19,280
|
772
|
188 |
So if you have like EVIL1
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
189 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
190 |
41
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
191 |
00:02:19,280 --> 00:02:22,325
|
772
|
192 |
of 20, and you have 119 nodes,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
193 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
194 |
42
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
195 |
00:02:22,325 --> 00:02:25,475
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
196 |
now this will be often copied.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
197 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
198 |
43
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
199 |
00:02:25,475 --> 00:02:31,475
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
200 |
And we want to see what's the
|
772
|
201 |
resulting tree look like, i.e.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
202 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
203 |
44
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
204 |
00:02:31,475 --> 00:02:32,780
|
772
|
205 |
how many nodes does it have.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
206 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
207 |
45
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
208 |
00:02:32,780 --> 00:02:34,985
|
772
|
209 |
So I take here EVIL1 of 20
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
210 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
211 |
46
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
212 |
00:02:34,985 --> 00:02:38,405
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
213 |
and the derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
214 |
according to 20 a's.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
215 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
216 |
47
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
217 |
00:02:38,405 --> 00:02:41,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
218 |
And just have a look
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
219 |
what the size is.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
220 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
221 |
48
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
222 |
00:02:43,210 --> 00:02:45,680
|
772
|
223 |
Okay, that takes a while.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
224 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
225 |
49
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
226 |
00:02:45,680 --> 00:02:48,410
|
772
|
227 |
You see now this recular expression,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
228 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
229 |
50
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
230 |
00:02:48,410 --> 00:02:52,280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
231 |
the derivative has already
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
232 |
8 million plus nodes.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
233 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
234 |
51
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
235 |
00:02:52,280 --> 00:02:55,400
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
236 |
And now nullable and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
237 |
derivative have to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
238 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
239 |
52
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
240 |
00:02:55,400 --> 00:02:58,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
241 |
traverse these trees with
|
772
|
242 |
8 million plus nodes.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
243 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
244 |
53
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
245 |
00:02:58,430 --> 00:03:01,400
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
246 |
So it's no wonder
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
247 |
that this is slow.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
248 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
249 |
54
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
250 |
00:03:01,400 --> 00:03:03,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
251 |
The first thing we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
252 |
can try to mitigate
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
253 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
254 |
55
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
255 |
00:03:03,860 --> 00:03:06,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
256 |
this explosion problem is to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
257 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
258 |
56
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
259 |
00:03:06,350 --> 00:03:09,050
|
772
|
260 |
have an explicit
|
|
261 |
n-times regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
262 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
263 |
57
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
264 |
00:03:09,050 --> 00:03:11,600
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
265 |
So instead of expanding
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
266 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
267 |
58
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
268 |
00:03:11,600 --> 00:03:13,415
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
269 |
it to the sequence
|
772
|
270 |
regular expression,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
271 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
272 |
59
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
273 |
00:03:13,415 --> 00:03:17,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
274 |
let's just have a single
|
772
|
275 |
regular expression n-times,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
276 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
277 |
60
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
278 |
00:03:17,510 --> 00:03:20,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
279 |
which takes an expression and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
280 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
281 |
61
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
282 |
00:03:20,540 --> 00:03:24,470
|
772
|
283 |
a number, and keeps that
|
|
284 |
regular expression small.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
285 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
286 |
62
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
287 |
00:03:24,470 --> 00:03:27,095
|
772
|
288 |
I'm here in the file re2.sc,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
289 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
290 |
63
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
291 |
00:03:27,095 --> 00:03:29,090
|
772
|
292 |
which is also on KEATS.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
293 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
294 |
64
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
295 |
00:03:29,090 --> 00:03:32,570
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
296 |
And the only change I made
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
297 |
is I added explicitly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
298 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
299 |
65
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
300 |
00:03:32,570 --> 00:03:33,860
|
772
|
301 |
a regular expression for
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
302 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
303 |
66
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
304 |
00:03:33,860 --> 00:03:36,770
|
772
|
305 |
n-times. The optional
|
|
306 |
regular expression
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
307 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
308 |
67
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
309 |
00:03:36,770 --> 00:03:39,920
|
772
|
310 |
we leave out at the
|
|
311 |
moment because this a?
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
312 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
313 |
68
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
314 |
00:03:39,920 --> 00:03:41,975
|
772
|
315 |
is represented as
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
316 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
317 |
69
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
318 |
00:03:41,975 --> 00:03:44,645
|
772
|
319 |
a + 1 and doesn't
|
|
320 |
expand too much.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
321 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
322 |
70
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
323 |
00:03:44,645 --> 00:03:47,375
|
772
|
324 |
The real culprit
|
|
325 |
is this n-times.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
326 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
327 |
71
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
328 |
00:03:47,375 --> 00:03:51,095
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
329 |
And instead of expanding
|
772
|
330 |
it n-times, we just
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
331 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
332 |
72
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
333 |
00:03:51,095 --> 00:03:54,275
|
772
|
334 |
take here a regular expression
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
335 |
and a natural number,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
336 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
337 |
73
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
338 |
00:03:54,275 --> 00:03:56,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
339 |
which says how many times
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
340 |
it should be repeated.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
341 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
342 |
74
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
343 |
00:03:56,960 --> 00:03:59,165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
344 |
And in this week we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
345 |
can keep it small.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
346 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
347 |
75
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
348 |
00:03:59,165 --> 00:04:01,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
349 |
But by adding that
|
772
|
350 |
regular expression,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
351 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
352 |
76
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
353 |
00:04:01,370 --> 00:04:05,150
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
354 |
we now have to think about
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
355 |
cases for nullable and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
356 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
357 |
77
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
358 |
00:04:05,150 --> 00:04:07,340
|
772
|
359 |
derivative. So that we have
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
360 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
361 |
78
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
362 |
00:04:07,340 --> 00:04:10,205
|
772
|
363 |
to calculate next
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
364 |
what they look like.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
365 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
366 |
79
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
367 |
00:04:10,205 --> 00:04:14,060
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
368 |
We can actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
369 |
calculate what the rule
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
370 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
371 |
80
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
372 |
00:04:14,060 --> 00:04:17,525
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
373 |
for nullable should be from
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
374 |
how we defined it earlier.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
375 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
376 |
81
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
377 |
00:04:17,525 --> 00:04:19,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
378 |
Remember, if you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
379 |
a regular expression,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
380 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
381 |
82
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
382 |
00:04:19,580 --> 00:04:21,980
|
772
|
383 |
r and we take it
|
|
384 |
n-times of this r,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
385 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
386 |
83
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
387 |
00:04:21,980 --> 00:04:25,220
|
772
|
388 |
then in case if n = 0,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
389 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
390 |
84
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
391 |
00:04:25,220 --> 00:04:28,130
|
772
|
392 |
we definded that as the
|
|
393 |
1 regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
394 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
395 |
85
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
396 |
00:04:28,130 --> 00:04:30,380
|
772
|
397 |
If n = 1,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
398 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
399 |
86
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
400 |
00:04:30,380 --> 00:04:32,495
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
401 |
it will be just a
|
772
|
402 |
single copy of r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
403 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
404 |
87
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
405 |
00:04:32,495 --> 00:04:33,725
|
772
|
406 |
If n = 2,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
407 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
408 |
88
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
409 |
00:04:33,725 --> 00:04:35,270
|
772
|
410 |
it will be two copies in sequence.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
411 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
412 |
89
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
413 |
00:04:35,270 --> 00:04:39,260
|
772
|
414 |
If three, we have
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
415 |
three copies and so on.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
416 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
417 |
90
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
418 |
00:04:39,260 --> 00:04:41,390
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
419 |
Now we have to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
420 |
somehow characterize
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
421 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
422 |
91
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
423 |
00:04:41,390 --> 00:04:44,285
|
772
|
424 |
when are these cases all nullable.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
425 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
426 |
92
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
427 |
00:04:44,285 --> 00:04:47,810
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
428 |
Well, if n equals 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
429 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
430 |
93
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
431 |
00:04:47,810 --> 00:04:49,850
|
772
|
432 |
then this will be defined as 1.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
433 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
434 |
94
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
435 |
00:04:49,850 --> 00:04:52,100
|
772
|
436 |
So 1 can match
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
437 |
the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
438 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
439 |
95
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
440 |
00:04:52,100 --> 00:04:54,785
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
441 |
So that should be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
442 |
definitely true.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
443 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
444 |
96
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
445 |
00:04:54,785 --> 00:04:57,725
|
772
|
446 |
Okay, if n = 1,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
447 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
448 |
97
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
449 |
00:04:57,725 --> 00:05:00,470
|
772
|
450 |
when can this regular expression
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
451 |
match the empty string?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
452 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
453 |
98
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
454 |
00:05:00,470 --> 00:05:02,000
|
772
|
455 |
So when should this be nullable?
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
456 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
457 |
99
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
458 |
00:05:02,000 --> 00:05:07,535
|
772
|
459 |
Well, if nullable of r holds,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
460 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
461 |
100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
462 |
00:05:07,535 --> 00:05:09,860
|
772
|
463 |
If it can match
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
464 |
the empty string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
465 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
466 |
101
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
467 |
00:05:09,860 --> 00:05:12,110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
468 |
then we can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
469 |
the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
470 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
471 |
102
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
472 |
00:05:12,110 --> 00:05:14,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
473 |
When can this regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
474 |
match the empty string?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
475 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
476 |
103
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
477 |
00:05:14,870 --> 00:05:16,265
|
772
|
478 |
So these are now two copies of r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
479 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
480 |
104
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
481 |
00:05:16,265 --> 00:05:20,690
|
772
|
482 |
Well, both copies need
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
483 |
to match the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
484 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
485 |
105
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
486 |
00:05:20,690 --> 00:05:22,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
487 |
So again, we have to ask
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
488 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
489 |
106
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
490 |
00:05:22,820 --> 00:05:25,774
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
491 |
both of them need to be nullable.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
492 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
493 |
107
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
494 |
00:05:25,774 --> 00:05:28,520
|
772
|
495 |
Similarly, in the third case,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
496 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
497 |
108
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
498 |
00:05:28,520 --> 00:05:30,710
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
499 |
all three copies need to be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
500 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
501 |
109
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
502 |
00:05:30,710 --> 00:05:33,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
503 |
able to match the empty
|
772
|
504 |
string. When is that the case?
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
505 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
506 |
110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
507 |
00:05:33,230 --> 00:05:38,360
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
508 |
Well, if nullable of
|
772
|
509 |
r holds and so on.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
510 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
511 |
111
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
512 |
00:05:38,360 --> 00:05:48,754
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
513 |
So we can actually define that
|
772
|
514 |
if n = 0, then true,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
515 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
516 |
112
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
517 |
00:05:48,754 --> 00:05:56,045
|
772
|
518 |
else we have to ask whether
|
|
519 |
nullable of r holds.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
520 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
521 |
113
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
522 |
00:05:56,045 --> 00:05:58,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
523 |
So that will be the clause we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
524 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
525 |
114
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
526 |
00:05:58,550 --> 00:06:01,625
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
527 |
have to implement for
|
772
|
528 |
n-times and nullable.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
529 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
530 |
115
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
531 |
00:06:01,625 --> 00:06:04,280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
532 |
Deriving the definition for
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
533 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
534 |
116
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
535 |
00:06:04,280 --> 00:06:06,920
|
772
|
536 |
the derivative of the n-times
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
537 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
538 |
117
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
539 |
00:06:06,920 --> 00:06:10,175
|
772
|
540 |
regular expression
|
|
541 |
is not that easy.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
542 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
543 |
118
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
544 |
00:06:10,175 --> 00:06:12,755
|
772
|
545 |
We have to look again
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
546 |
how it was defined
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
547 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
548 |
119
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
549 |
00:06:12,755 --> 00:06:16,010
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
550 |
earlier and we somehow
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
551 |
have to spot a pattern.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
552 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
553 |
120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
554 |
00:06:16,010 --> 00:06:18,380
|
772
|
555 |
Otherwise, our
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
556 |
algorithm will be again
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
557 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
558 |
121
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
559 |
00:06:18,380 --> 00:06:20,975
|
772
|
560 |
quite slow if we don't
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
561 |
spot that pattern.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
562 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
563 |
122
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
564 |
00:06:20,975 --> 00:06:22,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
565 |
So let's have a look.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
566 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
567 |
123
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
568 |
00:06:22,550 --> 00:06:26,240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
569 |
So in the case that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
570 |
n is equal to 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
571 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
572 |
124
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
573 |
00:06:26,240 --> 00:06:29,885
|
772
|
574 |
then r n-times was
|
|
575 |
defined as just 1.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
576 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
577 |
125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
578 |
00:06:29,885 --> 00:06:32,030
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
579 |
What would be the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
580 |
derivative of one?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
581 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
582 |
126
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
583 |
00:06:32,030 --> 00:06:36,140
|
773
|
584 |
So the derivative of c of 1
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
585 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
586 |
127
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
587 |
00:06:36,140 --> 00:06:38,990
|
773
|
588 |
would be defined as 0.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
589 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
590 |
128
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
591 |
00:06:38,990 --> 00:06:41,465
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
592 |
Okay, fair enough.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
593 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
594 |
129
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
595 |
00:06:41,465 --> 00:06:44,960
|
773
|
596 |
If he have n = 1,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
597 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
598 |
130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
599 |
00:06:44,960 --> 00:06:48,125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
600 |
then we just have one copy
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
601 |
of this regular expression.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
602 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
603 |
131
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
604 |
00:06:48,125 --> 00:06:50,120
|
773
|
605 |
So there's not much else we can do.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
606 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
607 |
132
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
608 |
00:06:50,120 --> 00:06:53,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
609 |
We would have to calculate
|
773
|
610 |
the derivative of r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
611 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
612 |
133
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
613 |
00:06:53,735 --> 00:06:57,395
|
773
|
614 |
Now in the n = 2 case,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
615 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
616 |
134
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
617 |
00:06:57,395 --> 00:07:00,245
|
773
|
618 |
that would mean we
|
|
619 |
have two copies of r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
620 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
621 |
135
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
622 |
00:07:00,245 --> 00:07:03,425
|
773
|
623 |
And they would be a sequence.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
624 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
625 |
136
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
626 |
00:07:03,425 --> 00:07:07,775
|
773
|
627 |
How would be the derivative c of
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
628 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
629 |
137
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
630 |
00:07:07,775 --> 00:07:10,340
|
773
|
631 |
r followed by r be
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
632 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
633 |
138
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
634 |
00:07:10,340 --> 00:07:13,265
|
773
|
635 |
defined? Well we would
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
636 |
look up the definition.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
637 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
638 |
139
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
639 |
00:07:13,265 --> 00:07:15,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
640 |
And it would say that's
|
773
|
641 |
the complicated case,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
642 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
643 |
140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
644 |
00:07:15,470 --> 00:07:16,760
|
773
|
645 |
the sequence.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
646 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
647 |
141
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
648 |
00:07:16,760 --> 00:07:21,875
|
773
|
649 |
If nullable of r,
|
769
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:21,875 --> 00:07:25,250
|
773
|
653 |
then the more complicated case,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
654 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
655 |
143
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
656 |
00:07:25,250 --> 00:07:28,225
|
773
|
657 |
else, that's the easy
|
|
658 |
case, that would be
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
659 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
660 |
144
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
661 |
00:07:28,225 --> 00:07:32,660
|
773
|
662 |
derivative of c of r, followed
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
663 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
664 |
145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
665 |
00:07:32,660 --> 00:07:35,540
|
773
|
666 |
by r. And then I just have to copy
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
667 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
668 |
146
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
669 |
00:07:35,540 --> 00:07:40,775
|
773
|
670 |
that derivative of c
|
|
671 |
of r followed by r here.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
672 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
673 |
147
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
674 |
00:07:40,775 --> 00:07:43,130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
675 |
But in this case I have also
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
676 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
677 |
148
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
678 |
00:07:43,130 --> 00:07:51,145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
679 |
the alternative derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
680 |
of c of r. And from that,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
681 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
682 |
149
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
683 |
00:07:51,145 --> 00:07:55,030
|
773
|
684 |
it looks like we can't
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
685 |
do much better than
|
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:55,030 --> 00:07:58,390
|
773
|
689 |
that, unless we do
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
690 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
691 |
151
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
692 |
00:07:58,390 --> 00:08:02,560
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
693 |
a little bit of magic and the
|
773
|
694 |
magic has to do with this case.
|
769
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:08:02,560 --> 00:08:07,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
698 |
So let me look at this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
699 |
case a bit more closely.
|
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:08:07,420 --> 00:08:09,819
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
703 |
Let me go back to slides
|
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:08:09,819 --> 00:08:12,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
707 |
because actually the calculation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
708 |
might be a bit hairy.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
709 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
710 |
155
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
711 |
00:08:12,940 --> 00:08:16,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
712 |
So remember we are in this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
713 |
case where n equals two.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
714 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
715 |
156
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
716 |
00:08:16,945 --> 00:08:18,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
717 |
And this was defined as
|
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:08:18,550 --> 00:08:20,680
|
773
|
721 |
this sequence regular
|
|
722 |
expression r followed by r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
723 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
724 |
158
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
725 |
00:08:20,680 --> 00:08:23,080
|
773
|
726 |
And the question was,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
727 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
728 |
159
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
729 |
00:08:23,080 --> 00:08:26,365
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
730 |
can we somehow make sense
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
731 |
out of this derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
732 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
733 |
160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
734 |
00:08:26,365 --> 00:08:30,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
735 |
where we have to build the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
736 |
derivative of a sequence.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
737 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
738 |
161
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
739 |
00:08:30,370 --> 00:08:33,020
|
773
|
740 |
So if we just unfold the definition,
|
769
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:33,020 --> 00:08:36,050
|
773
|
744 |
we would ask if
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
745 |
the r is nullable,
|
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:36,050 --> 00:08:39,095
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
749 |
In this case, we return
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
750 |
this alternative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
751 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
752 |
164
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
753 |
00:08:39,095 --> 00:08:40,640
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
754 |
And if it's not nullable,
|
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:40,640 --> 00:08:44,135
|
773
|
758 |
it is just this
|
|
759 |
regular expression.
|
769
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:44,135 --> 00:08:49,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
763 |
Now my claim is that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
764 |
this whole if condition
|
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:49,550 --> 00:08:55,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
768 |
can be replaced by just this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
769 |
simple derivative here.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
770 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
771 |
168
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
772 |
00:08:55,895 --> 00:08:58,775
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
773 |
And if that claim is correct,
|
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:58,775 --> 00:09:01,520
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
777 |
there would be very nice
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
778 |
because in contrast to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
779 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
780 |
170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
781 |
00:09:01,520 --> 00:09:04,130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
782 |
this if condition where
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
783 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
784 |
171
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
785 |
00:09:04,130 --> 00:09:06,280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
786 |
we have to calculate
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
787 |
like nullable,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
788 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
789 |
172
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
790 |
00:09:06,280 --> 00:09:08,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
791 |
decide in which branch we are.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
792 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
793 |
173
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
794 |
00:09:08,330 --> 00:09:10,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
795 |
We don't have to
|
773
|
796 |
calculate nullable,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
797 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
798 |
174
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
799 |
00:09:10,580 --> 00:09:13,880
|
773
|
800 |
we can just replace
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
801 |
it by this expression.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
802 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
803 |
175
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
804 |
00:09:13,880 --> 00:09:16,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
805 |
So if we can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
806 |
substantiate that claim,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
807 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
808 |
176
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
809 |
00:09:16,670 --> 00:09:19,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
810 |
that will be definitely
|
773
|
811 |
good our algorithm.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
812 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
813 |
177
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
814 |
00:09:20,140 --> 00:09:22,775
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
815 |
And to substantiate that,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
816 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
817 |
178
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
818 |
00:09:22,775 --> 00:09:26,795
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
819 |
I will focus on this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
820 |
record expression here.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
821 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
822 |
179
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
823 |
00:09:26,795 --> 00:09:31,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
824 |
And notice that this record
|
773
|
825 |
expression will only be
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
826 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
827 |
180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
828 |
00:09:31,100 --> 00:09:35,780
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
829 |
called or only be generated
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
830 |
if r is nullable.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
831 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
832 |
181
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
833 |
00:09:35,780 --> 00:09:38,075
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
834 |
So in any other case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
835 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
836 |
182
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
837 |
00:09:38,075 --> 00:09:40,060
|
773
|
838 |
I will actually not go into
|
769
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:40,060 --> 00:09:43,850
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
842 |
that if branch and would
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
843 |
be in the other one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
844 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
845 |
184
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
846 |
00:09:43,850 --> 00:09:45,260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
847 |
So if we are in this if branch,
|
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:45,260 --> 00:09:47,705
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
851 |
we definitely know
|
773
|
852 |
that r is nullable.
|
769
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:47,705 --> 00:09:52,955
|
773
|
856 |
Okay, so here's
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
857 |
our regular expression.
|
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:52,955 --> 00:09:55,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
861 |
And we know it's nullable.
|
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:55,940 --> 00:09:57,920
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
865 |
So we have to somehow find
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
866 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
867 |
189
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
868 |
00:09:57,920 --> 00:10:00,380
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
869 |
an equivalent expression that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
870 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
871 |
190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
872 |
00:10:00,380 --> 00:10:04,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
873 |
is smaller or simpler
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
874 |
than that one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
875 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
876 |
191
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
877 |
00:10:04,100 --> 00:10:05,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
878 |
Let's see what we can do.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
879 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
880 |
192
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
881 |
00:10:05,945 --> 00:10:10,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
882 |
So the first thing
|
773
|
883 |
actually is we're multiplying
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
884 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
885 |
193
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
886 |
00:10:10,160 --> 00:10:16,595
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
887 |
this right hand side of the
|
773
|
888 |
alternative with times 1.
|
769
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:10:16,595 --> 00:10:19,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
892 |
We can do that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
893 |
because this does not
|
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:10:19,700 --> 00:10:23,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
897 |
change which strings this
|
773
|
898 |
regular expression can match.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
899 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
900 |
196
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
901 |
00:10:23,090 --> 00:10:25,685
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
902 |
Remember we even had it
|
773
|
903 |
as a simplification rule,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
904 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
905 |
197
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
906 |
00:10:25,685 --> 00:10:27,425
|
773
|
907 |
just in this case we
|
769
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:27,425 --> 00:10:29,705
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
911 |
don't apply it as a
|
773
|
912 |
simplification rule,
|
769
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:29,705 --> 00:10:31,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
916 |
actually make this
|
773
|
917 |
regular expression
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
918 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
919 |
200
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
920 |
00:10:31,310 --> 00:10:32,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
921 |
a bit more complicated.
|
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:32,720 --> 00:10:34,910
|
773
|
925 |
But times 1 doesn't make
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
926 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
927 |
202
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
928 |
00:10:34,910 --> 00:10:37,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
929 |
a difference because it
|
773
|
930 |
means at the end of a string,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
931 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
932 |
203
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
933 |
00:10:37,820 --> 00:10:40,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
934 |
we still want to match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
935 |
the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
936 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
937 |
204
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
938 |
00:10:40,070 --> 00:10:42,155
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
939 |
Okay, so that is possible.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
940 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
941 |
205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
942 |
00:10:42,155 --> 00:10:45,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
943 |
I can do that. Once
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
944 |
we have done that,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
945 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
946 |
206
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
947 |
00:10:45,740 --> 00:10:48,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
948 |
you will notice that this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
949 |
factor derivative of
|
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:48,410 --> 00:10:51,860
|
773
|
953 |
r are exactly the
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
954 |
same as that one.
|
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:51,860 --> 00:10:54,650
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
958 |
And in between is a plus.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
959 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
960 |
209
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
961 |
00:10:54,650 --> 00:10:57,440
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
962 |
So you probably remember the law
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
963 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
964 |
210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
965 |
00:10:57,440 --> 00:11:00,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
966 |
from school math
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
967 |
that I can pull out
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
968 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
969 |
211
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
970 |
00:11:00,170 --> 00:11:02,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
971 |
this factor derivative of c of r.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
972 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
973 |
212
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
974 |
00:11:02,735 --> 00:11:06,320
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
975 |
And I'm inside the parentheses
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
976 |
is left with that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
977 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
978 |
213
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
979 |
00:11:06,320 --> 00:11:09,245
|
773
|
980 |
So now I have r + 1.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
981 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
982 |
214
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
983 |
00:11:09,245 --> 00:11:13,055
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
984 |
Usually we cannot
|
773
|
985 |
simplify r + 1.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
986 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
987 |
215
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
988 |
00:11:13,055 --> 00:11:15,530
|
773
|
989 |
If it had been r + 0, then yes,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
990 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
991 |
216
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
992 |
00:11:15,530 --> 00:11:18,665
|
773
|
993 |
we could have got rid of the 0.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
994 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
995 |
217
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
996 |
00:11:18,665 --> 00:11:21,590
|
773
|
997 |
But this + 1 often
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
998 |
makes a difference,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
999 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1000 |
218
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1001 |
00:11:21,590 --> 00:11:22,970
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1002 |
but not in our case.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1003 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1004 |
219
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1005 |
00:11:22,970 --> 00:11:25,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1006 |
Remember, we know that
|
773
|
1007 |
this r is nullable,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1008 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1009 |
220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1010 |
00:11:25,940 --> 00:11:29,840
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1011 |
so on its own can already
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1012 |
match the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1013 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1014 |
221
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1015 |
00:11:29,840 --> 00:11:33,305
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1016 |
So we don't really need this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1017 |
alternative plus one there,
|
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:33,305 --> 00:11:35,300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1021 |
so we can just get rid of that.
|
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:35,300 --> 00:11:37,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1025 |
Okay, and so now we have
|
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:37,070 --> 00:11:40,535
|
773
|
1029 |
a much simpler equivalent
|
|
1030 |
regular expression.
|
769
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:40,535 --> 00:11:44,285
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1034 |
And this actually helps a
|
773
|
1035 |
lot for our if-condition.
|
769
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:44,285 --> 00:11:46,925
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1039 |
Look, this was the
|
773
|
1040 |
original if-condition
|
769
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:46,925 --> 00:11:50,270
|
773
|
1044 |
and this is the regular expression
|
|
1045 |
we just simplified.
|
769
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:50,270 --> 00:11:53,105
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1049 |
If we replace it with this one,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1050 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1051 |
229
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1052 |
00:11:53,105 --> 00:11:56,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1053 |
then we just end up with this.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1054 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1055 |
230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1056 |
00:11:56,090 --> 00:11:59,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1057 |
And now you will see that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1058 |
the if condition is actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1059 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1060 |
231
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1061 |
00:11:59,510 --> 00:12:02,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1062 |
pointless because you
|
773
|
1063 |
check if it's nullable,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1064 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1065 |
232
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1066 |
00:12:02,750 --> 00:12:05,060
|
773
|
1067 |
we return this regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1068 |
expression or it's
|
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,060 --> 00:12:08,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1072 |
not nullable and we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1073 |
return exactly the same.
|
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:08,210 --> 00:12:10,025
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1077 |
That doesn't make any difference.
|
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:10,025 --> 00:12:11,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1081 |
So we can just get rid of
|
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:11,750 --> 00:12:14,645
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1085 |
that one and can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1086 |
replace it by that.
|
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:14,645 --> 00:12:16,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1090 |
And you see, this is now
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1091 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1092 |
238
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1093 |
00:12:16,865 --> 00:12:20,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1094 |
a much simpler case than
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1095 |
what we had before.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1096 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1097 |
239
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1098 |
00:12:20,720 --> 00:12:24,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1099 |
So let's take stock
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1100 |
what we have so far.
|
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:24,170 --> 00:12:26,915
|
773
|
1104 |
So we know in the 0-case,
|
769
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:26,915 --> 00:12:30,920
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1108 |
the derivative needs
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1109 |
to be defined as 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1110 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1111 |
242
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1112 |
00:12:30,920 --> 00:12:33,095
|
773
|
1113 |
Because we define this
|
769
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:33,095 --> 00:12:36,785
|
773
|
1117 |
n-times as one,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1118 |
the derivative is 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1119 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1120 |
244
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1121 |
00:12:36,785 --> 00:12:39,889
|
773
|
1122 |
For just r, this will
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1123 |
be the derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1124 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1125 |
245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1126 |
00:12:39,889 --> 00:12:42,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1127 |
And we can't do any
|
773
|
1128 |
better than that.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1129 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1130 |
246
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1131 |
00:12:42,170 --> 00:12:45,620
|
773
|
1132 |
For r followed by r, as we
|
|
1133 |
just found out
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1134 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1135 |
247
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1136 |
00:12:45,620 --> 00:12:47,270
|
773
|
1137 |
actually it is quite simple
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1138 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1139 |
248
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1140 |
00:12:47,270 --> 00:12:51,410
|
773
|
1141 |
regular expression is equivalent
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1142 |
to the derivative.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1143 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1144 |
249
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1145 |
00:12:51,410 --> 00:12:53,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1146 |
Now, we have to continue with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1147 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1148 |
250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1149 |
00:12:53,870 --> 00:12:56,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1150 |
that case where n is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1151 |
equal to three and we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1152 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1153 |
251
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1154 |
00:12:56,090 --> 00:12:58,099
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1155 |
now have three copies
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1156 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1157 |
252
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1158 |
00:12:58,099 --> 00:13:02,390
|
773
|
1159 |
of this r. What should
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1160 |
be the derivative?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1161 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1162 |
253
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1163 |
00:13:02,390 --> 00:13:05,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1164 |
Well, if you look very carefully
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1165 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1166 |
254
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1167 |
00:13:05,330 --> 00:13:08,465
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1168 |
at this emerging pattern,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1169 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1170 |
255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1171 |
00:13:08,465 --> 00:13:12,410
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1172 |
I have to say then
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1173 |
what would be nice if,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1174 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1175 |
256
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1176 |
00:13:12,410 --> 00:13:16,400
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1177 |
if he could show that in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1178 |
the n equals three case,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1179 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1180 |
257
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1181 |
00:13:16,400 --> 00:13:18,275
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1182 |
we end up with this.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1183 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1184 |
258
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1185 |
00:13:18,275 --> 00:13:21,290
|
773
|
1186 |
Because then what we have is this.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1187 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1188 |
259
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1189 |
00:13:21,290 --> 00:13:25,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1190 |
We can define our
|
773
|
1191 |
nullable for n-times
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1192 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1193 |
260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1194 |
00:13:25,370 --> 00:13:31,025
|
773
|
1195 |
as if n = 0 then
|
|
1196 |
true, else nullable r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1197 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1198 |
261
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1199 |
00:13:31,025 --> 00:13:33,875
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1200 |
And for the derivative,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1201 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1202 |
262
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1203 |
00:13:33,875 --> 00:13:37,190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1204 |
we can save if n is equal to 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1205 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1206 |
263
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1207 |
00:13:37,190 --> 00:13:40,235
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1208 |
then we return the
|
773
|
1209 |
0 regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1210 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1211 |
264
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1212 |
00:13:40,235 --> 00:13:43,295
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1213 |
Otherwise, as you can see
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1214 |
from this pattern here,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1215 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1216 |
265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1217 |
00:13:43,295 --> 00:13:50,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1218 |
it would be derivative of
|
773
|
1219 |
c r followed by r{n-1}.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1220 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1221 |
266
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1222 |
00:13:50,735 --> 00:13:54,770
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1223 |
Okay? And the only
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1224 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1225 |
267
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1226 |
00:13:54,770 --> 00:13:56,330
|
773
|
1227 |
thing we have to make csure is that
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1228 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1229 |
268
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1230 |
00:13:56,330 --> 00:13:58,175
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1231 |
this pattern actually holds.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1232 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1233 |
269
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1234 |
00:13:58,175 --> 00:14:00,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1235 |
So that's, I will
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1236 |
show you next in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1237 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1238 |
270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1239 |
00:14:00,470 --> 00:14:03,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1240 |
the case for n equals three.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1241 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1242 |
271
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1243 |
00:14:03,735 --> 00:14:07,810
|
773
|
1244 |
If we have a regular expression r
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1245 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1246 |
272
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1247 |
00:14:07,810 --> 00:14:09,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1248 |
and it's followed
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1249 |
by r and another r,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1250 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1251 |
273
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1252 |
00:14:09,820 --> 00:14:11,275
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1253 |
three copies of it.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1254 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1255 |
274
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1256 |
00:14:11,275 --> 00:14:14,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1257 |
We can just unfold
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1258 |
again the definition.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1259 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1260 |
275
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1261 |
00:14:14,245 --> 00:14:16,930
|
773
|
1262 |
So we would ask if r is nullable,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1263 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1264 |
276
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1265 |
00:14:16,930 --> 00:14:19,765
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1266 |
then we have this if branch.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1267 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1268 |
277
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1269 |
00:14:19,765 --> 00:14:23,905
|
773
|
1270 |
And if r is not nullable,
|
|
1271 |
we have this else branch.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1272 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1273 |
278
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1274 |
00:14:23,905 --> 00:14:27,010
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1275 |
Okay? What can we do here?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1276 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1277 |
279
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1278 |
00:14:27,010 --> 00:14:30,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1279 |
Well, we notice that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1280 |
this one is just now
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1281 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1282 |
280
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1283 |
00:14:30,310 --> 00:14:34,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1284 |
the derivative of two
|
773
|
1285 |
r's, one after another.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1286 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1287 |
281
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1288 |
00:14:34,510 --> 00:14:37,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1289 |
But this we just
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1290 |
calculated a moment ago,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1291 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1292 |
282
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1293 |
00:14:37,330 --> 00:14:40,120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1294 |
so we can just
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1295 |
replace it by this.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1296 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1297 |
283
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1298 |
00:14:40,120 --> 00:14:43,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1299 |
Ok. That's what we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1300 |
calculated earlier.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1301 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1302 |
284
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1303 |
00:14:43,255 --> 00:14:46,665
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1304 |
But now you will see
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1305 |
again this factor,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1306 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1307 |
285
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1308 |
00:14:46,665 --> 00:14:48,695
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1309 |
and this factor is the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1310 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1311 |
286
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1312 |
00:14:48,695 --> 00:14:52,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1313 |
So I can pull that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1314 |
out to be like that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1315 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1316 |
287
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1317 |
00:14:52,700 --> 00:14:57,380
|
773
|
1318 |
And I have now r followed
|
|
1319 |
by r plus r.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1320 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1321 |
288
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1322 |
00:14:57,380 --> 00:14:59,030
|
773
|
1323 |
But now you probably
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1324 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1325 |
289
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1326 |
00:14:59,030 --> 00:15:00,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1327 |
remember how we did it earlier.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1328 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1329 |
290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1330 |
00:15:00,680 --> 00:15:03,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1331 |
We can now pull out one copy of
|
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:03,080 --> 00:15:06,020
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1335 |
this are to just get
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1336 |
something like this.
|
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:06,020 --> 00:15:08,765
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1340 |
We have to add one essentially,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1341 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1342 |
293
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1343 |
00:15:08,765 --> 00:15:11,615
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1344 |
but we now get r plus one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1345 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1346 |
294
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1347 |
00:15:11,615 --> 00:15:15,065
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1348 |
And this r here is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1349 |
now just pulled out.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1350 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1351 |
295
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1352 |
00:15:15,065 --> 00:15:18,995
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1353 |
Well, here again kicks
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1354 |
in this reasoning.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1355 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1356 |
296
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1357 |
00:15:18,995 --> 00:15:22,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1358 |
We go in this if branch
|
773
|
1359 |
only if r is nullable.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1360 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1361 |
297
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1362 |
00:15:22,700 --> 00:15:26,150
|
773
|
1363 |
So r on its own can already
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1364 |
match the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1365 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1366 |
298
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1367 |
00:15:26,150 --> 00:15:28,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1368 |
So I don't need
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1369 |
really this plus one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1370 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1371 |
299
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1372 |
00:15:28,895 --> 00:15:30,695
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1373 |
I can just get rid of it.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1374 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1375 |
300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1376 |
00:15:30,695 --> 00:15:33,140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1377 |
And so I now just have
|
773
|
1378 |
to rearrange the parentheses
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1379 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1380 |
301
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1381 |
00:15:33,140 --> 00:15:35,450
|
773
|
1382 |
which we said we can also do.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1383 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1384 |
302
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1385 |
00:15:35,450 --> 00:15:37,595
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1386 |
So we have something like that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1387 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1388 |
303
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1389 |
00:15:37,595 --> 00:15:39,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1390 |
And here again, the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1391 |
same reasoning,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1392 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1393 |
304
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1394 |
00:15:39,740 --> 00:15:41,975
|
773
|
1395 |
we have an if condition
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1396 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1397 |
305
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1398 |
00:15:41,975 --> 00:15:43,310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1399 |
where it doesn't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1400 |
really matter what
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1401 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1402 |
306
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1403 |
00:15:43,310 --> 00:15:44,405
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1404 |
we're going to return,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1405 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1406 |
307
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1407 |
00:15:44,405 --> 00:15:46,205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1408 |
it's in both branches the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1409 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1410 |
308
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1411 |
00:15:46,205 --> 00:15:48,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1412 |
So we can just
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1413 |
replace it by that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1414 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1415 |
309
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1416 |
00:15:48,470 --> 00:15:51,920
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1417 |
And yes, now we can be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1418 |
pretty sure they'll
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1419 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1420 |
310
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1421 |
00:15:51,920 --> 00:15:55,310
|
773
|
1422 |
work for all the n-times
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1423 |
regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1424 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1425 |
311
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1426 |
00:15:55,310 --> 00:15:57,860
|
773
|
1427 |
And I leave
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1428 |
the calculation for
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1429 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1430 |
312
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1431 |
00:15:57,860 --> 00:16:02,570
|
773
|
1432 |
maybe r to the four to you.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1433 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1434 |
313
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1435 |
00:16:02,570 --> 00:16:04,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1436 |
And the reason why I do it
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1437 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1438 |
314
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1439 |
00:16:04,490 --> 00:16:06,605
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1440 |
in such a detail,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1441 |
this calculation,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1442 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1443 |
315
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1444 |
00:16:06,605 --> 00:16:08,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1445 |
this is really meant
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1446 |
to help you with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1447 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1448 |
316
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1449 |
00:16:08,960 --> 00:16:13,200
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1450 |
the coursework which is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1451 |
coming up this week.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1452 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1453 |
317
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1454 |
00:16:13,210 --> 00:16:16,250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1455 |
I'm now back in our
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1456 |
implementation.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1457 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1458 |
318
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1459 |
00:16:16,250 --> 00:16:20,660
|
773
|
1460 |
In this re2.sc, we said we have
|
|
1461 |
this explicit constructor
|
769
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:20,660 --> 00:16:25,535
|
773
|
1465 |
for n-times. We can now fill
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1466 |
in the cases for nullable.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1467 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1468 |
320
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1469 |
00:16:25,535 --> 00:16:27,635
|
773
|
1470 |
So if we have r n-times,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1471 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1472 |
321
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1473 |
00:16:27,635 --> 00:16:30,995
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1474 |
if this n is equal to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1475 |
0, we return true.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1476 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1477 |
322
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1478 |
00:16:30,995 --> 00:16:34,190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1479 |
Otherwise we have to test
|
773
|
1480 |
whether r is nullable.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1481 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1482 |
323
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1483 |
00:16:34,190 --> 00:16:37,565
|
773
|
1484 |
And in the derivative case,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1485 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1486 |
324
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1487 |
00:16:37,565 --> 00:16:40,339
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1488 |
if this n is equal to 0,
|
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:40,339 --> 00:16:43,564
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1492 |
the return this 0
|
773
|
1493 |
regular expression.
|
769
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:43,564 --> 00:16:46,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1497 |
Otherwise we return the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1498 |
sequence of the derivative
|
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:46,700 --> 00:16:50,270
|
773
|
1502 |
of c of r followed by n times of r,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1503 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1504 |
328
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1505 |
00:16:50,270 --> 00:16:54,545
|
773
|
1506 |
but n minus one times, and
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1507 |
everything else stays the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1508 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1509 |
329
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1510 |
00:16:54,545 --> 00:16:56,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1511 |
Here's the function for strings,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1512 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1513 |
330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1514 |
00:16:56,510 --> 00:16:58,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1515 |
derivative function for strings.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1516 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1517 |
331
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1518 |
00:16:58,430 --> 00:17:01,595
|
773
|
1519 |
In the main matcher
|
|
1520 |
function is all the same.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1521 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1522 |
332
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1523 |
00:17:01,595 --> 00:17:04,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1524 |
We still require this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1525 |
definition because
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1526 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1527 |
333
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1528 |
00:17:04,820 --> 00:17:06,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1529 |
we haven't done anything about
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1530 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1531 |
334
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1532 |
00:17:06,050 --> 00:17:08,090
|
773
|
1533 |
the optional regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1534 |
expression yet.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1535 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1536 |
335
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1537 |
00:17:08,090 --> 00:17:10,670
|
773
|
1538 |
And we have now this
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1539 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1540 |
336
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1541 |
00:17:10,670 --> 00:17:13,250
|
773
|
1542 |
EVIL1 and EVIL2
|
|
1543 |
regular expression.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1544 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1545 |
337
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1546 |
00:17:13,250 --> 00:17:15,290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1547 |
And let's test it. And let's be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1548 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1549 |
338
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1550 |
00:17:15,290 --> 00:17:17,000
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1551 |
a bit more ambitious.
|
773
|
1552 |
We're testing it with
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1553 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1554 |
339
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1555 |
00:17:17,000 --> 00:17:20,315
|
773
|
1556 |
strings between 0 and 1000
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1557 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1558 |
340
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1559 |
00:17:20,315 --> 00:17:22,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1560 |
and let's see what the time say.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1561 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1562 |
341
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1563 |
00:17:22,580 --> 00:17:26,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1564 |
I'm testing this again
|
773
|
1565 |
inside the Ammonite REPL.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1566 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1567 |
342
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1568 |
00:17:26,210 --> 00:17:30,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1569 |
And you'll see it should
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1570 |
be now much quicker.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1571 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1572 |
343
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1573 |
00:17:30,610 --> 00:17:34,640
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1574 |
Okay, it might slow
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1575 |
down also around 600.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1576 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1577 |
344
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1578 |
00:17:34,640 --> 00:17:40,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1579 |
700 needs two seconds,
|
773
|
1580 |
three seconds for 800.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1581 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1582 |
345
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1583 |
00:17:40,490 --> 00:17:43,940
|
773
|
1584 |
Let's see what it
|
|
1585 |
needs for one thousand?
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1586 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1587 |
346
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1588 |
00:17:43,940 --> 00:17:47,435
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1589 |
But you have to remember
|
773
|
1590 |
Ruby and Python
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1591 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1592 |
347
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1593 |
00:17:47,435 --> 00:17:51,530
|
773
|
1594 |
needed half a
|
|
1595 |
minute for just 30 a's.
|
769
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:51,530 --> 00:17:54,485
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1599 |
We need a little bit
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1600 |
more than six seconds,
|
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:54,485 --> 00:17:57,110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1604 |
but we are processing a string of
|
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:57,110 --> 00:18:00,575
|
773
|
1608 |
1000 a's. So that success.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1609 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1610 |
351
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1611 |
00:18:00,575 --> 00:18:04,775
|
773
|
1612 |
This speed is also explained
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1613 |
if you look at the sizes.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1614 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1615 |
352
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1616 |
00:18:04,775 --> 00:18:08,975
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1617 |
Since we now have this explicit
|
773
|
1618 |
n-times constructor,
|
769
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:08,975 --> 00:18:11,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1622 |
it doesn't really matter
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1623 |
how big this n is.
|
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:11,930 --> 00:18:14,540
|
773
|
1627 |
This EVIL1 regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1628 |
expression will always be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1629 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1630 |
355
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1631 |
00:18:14,540 --> 00:18:17,195
|
773
|
1632 |
of this size seven, at
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1633 |
the beginning.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1634 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1635 |
356
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1636 |
00:18:17,195 --> 00:18:20,315
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1637 |
And you can also see if you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1638 |
now build the derivatives,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1639 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1640 |
357
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1641 |
00:18:20,315 --> 00:18:22,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1642 |
they still grow in size,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1643 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1644 |
358
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1645 |
00:18:22,550 --> 00:18:24,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1646 |
but much more moderately.
|
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:24,740 --> 00:18:28,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1650 |
And let's try out this
|
773
|
1651 |
example with 20 a's.
|
769
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:28,100 --> 00:18:31,685
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1655 |
So we build the derivative
|
773
|
1656 |
according to 20 character a's.
|
769
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:31,685 --> 00:18:33,890
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1660 |
In the earlier example,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1661 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1662 |
362
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1663 |
00:18:33,890 --> 00:18:35,780
|
773
|
1664 |
we ended up with a
|
|
1665 |
regular expression that
|
769
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:35,780 --> 00:18:37,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1669 |
had like 8 million plus nodes.
|
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:37,895 --> 00:18:39,830
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1673 |
And if we do this now,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1674 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1675 |
365
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1676 |
00:18:39,830 --> 00:18:43,205
|
773
|
1677 |
then we just have a regular
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1678 |
expression with 211 nodes.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1679 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1680 |
366
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1681 |
00:18:43,205 --> 00:18:44,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1682 |
And that is much smaller and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1683 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1684 |
367
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1685 |
00:18:44,750 --> 00:18:47,165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1686 |
all the calculations
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1687 |
would be much quicker.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1688 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1689 |
368
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1690 |
00:18:47,165 --> 00:18:49,550
|
773
|
1691 |
So yeah, the Brzozowski
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1692 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1693 |
369
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1694 |
00:18:49,550 --> 00:18:52,205
|
773
|
1695 |
algorithm
|
|
1696 |
and with this improvement,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1697 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1698 |
370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1699 |
00:18:52,205 --> 00:18:54,890
|
773
|
1700 |
we're now running
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1701 |
circles around Ruby and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1702 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1703 |
371
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1704 |
00:18:54,890 --> 00:18:58,445
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1705 |
Python because they're just
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1706 |
stuck here at the beginning.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1707 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1708 |
372
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1709 |
00:18:58,445 --> 00:19:00,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1710 |
Because they need already
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1711 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1712 |
373
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1713 |
00:19:00,230 --> 00:19:02,975
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1714 |
like half a minute
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1715 |
for just 30 a's.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1716 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1717 |
374
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1718 |
00:19:02,975 --> 00:19:05,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1719 |
We now can do something
|
773
|
1720 |
like thousand a's
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1721 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1722 |
375
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1723 |
00:19:05,930 --> 00:19:07,580
|
773
|
1724 |
in a reasonable time.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1725 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1726 |
376
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1727 |
00:19:07,580 --> 00:19:09,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1728 |
I think this must be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1729 |
timing I obtained with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1730 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1731 |
377
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1732 |
00:19:09,740 --> 00:19:12,635
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1733 |
my older laptop some time ago.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1734 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1735 |
378
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1736 |
00:19:12,635 --> 00:19:14,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1737 |
Because remember we
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1738 |
had something like
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1739 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1740 |
379
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1741 |
00:19:14,210 --> 00:19:16,670
|
773
|
1742 |
six seconds. Here it says 15.
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1743 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1744 |
380
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1745 |
00:19:16,670 --> 00:19:18,080
|
773
|
1746 |
You always have to take
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1747 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1748 |
381
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1749 |
00:19:18,080 --> 00:19:20,885
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1750 |
these times with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1751 |
the pinch of salt.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1752 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1753 |
382
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1754 |
00:19:20,885 --> 00:19:22,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1755 |
It's essentially only the trend,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1756 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1757 |
383
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1758 |
00:19:22,670 --> 00:19:25,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1759 |
but it's clear we are
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1760 |
much, much better.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1761 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1762 |
384
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1763 |
00:19:25,100 --> 00:19:27,065
|
773
|
1764 |
We have worked a lot,
|
769
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1765 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1766 |
385
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1767 |
00:19:27,065 --> 00:19:30,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1768 |
but we also got something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1769 |
for it in return.
|