766
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:09,990 --> 00:00:13,465
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
3 |
Welcome back to this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
week's lecture.
|
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:13,465 --> 00:00:16,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
8 |
The task this week is to actually
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
9 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
3
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
00:00:16,450 --> 00:00:20,320
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
implement a regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
expression matcher.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
4
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
00:00:20,320 --> 00:00:22,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
And we want to be a bit
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
5
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
00:00:22,510 --> 00:00:25,315
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
faster than the regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
22 |
expression matcher
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
23 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
6
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
00:00:25,315 --> 00:00:29,380
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
in Python, Ruby,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
27 |
Javascript, and Java.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
28 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
7
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
30 |
00:00:29,380 --> 00:00:31,960
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
Remember this regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
32 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
33 |
8
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
00:00:31,960 --> 00:00:35,785
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
and strings which are
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
36 |
just a number of a's,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
9
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
00:00:35,785 --> 00:00:39,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
these regular expression matchers
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
41 |
where abysmally slow.
|
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:39,670 --> 00:00:43,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
45 |
They could only match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
46 |
approximately 30 a's in
|
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:43,170 --> 00:00:45,665
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
something like half a minute.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
12
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
00:00:45,665 --> 00:00:49,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
What we like to do with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
55 |
our regular expression matcher.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
13
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
58 |
00:00:49,460 --> 00:00:51,890
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
We will try a few times,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
60 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
61 |
14
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
62 |
00:00:51,890 --> 00:00:55,505
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
but our second trial will already
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
64 |
be much, much better.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
65 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
66 |
15
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
67 |
00:00:55,505 --> 00:00:58,400
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
68 |
It will probably
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
69 |
match around maybe
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
70 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
71 |
16
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
00:00:58,400 --> 00:01:02,030
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
73 |
thousand a's in something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
74 |
in half a minute.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
75 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
76 |
17
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
00:01:02,030 --> 00:01:03,920
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
78 |
But our third version in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
80 |
18
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
81 |
00:01:03,920 --> 00:01:06,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
82 |
comparison will be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
blindingly fast.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
85 |
19
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
00:01:06,230 --> 00:01:08,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
And we'll be able to match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
89 |
20
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
90 |
00:01:08,180 --> 00:01:10,145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
strings of length 10,000 a's
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
92 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
21
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
94 |
00:01:10,145 --> 00:01:12,230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
95 |
and will not require
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
22
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
00:01:12,230 --> 00:01:14,975
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
99 |
more than five seconds.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
So let's go ahead with that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
23
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
103 |
00:01:14,975 --> 00:01:18,095
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
104 |
We will first implement
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
24
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
00:01:18,095 --> 00:01:19,880
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
108 |
our regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
109 |
matcher only
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
25
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
00:01:19,880 --> 00:01:22,069
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
113 |
for the basic
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
26
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
117 |
00:01:22,069 --> 00:01:25,430
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
So we will have only six
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
cases to think about.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
120 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
121 |
27
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
122 |
00:01:25,430 --> 00:01:27,620
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
123 |
This will simplify matters at first.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
124 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
125 |
28
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
126 |
00:01:27,620 --> 00:01:30,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
127 |
Later we can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
128 |
think about how to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
129 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
130 |
29
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
131 |
00:01:30,350 --> 00:01:34,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
132 |
extend that to the extended
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
133 |
regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
134 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
135 |
30
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
136 |
00:01:34,100 --> 00:01:37,625
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
137 |
Unfortunately, before we can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
138 |
start our implementation,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
139 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
140 |
31
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
141 |
00:01:37,625 --> 00:01:39,290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
142 |
we have to discuss
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
143 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
144 |
32
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
145 |
00:01:39,290 --> 00:01:42,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
146 |
when two regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
147 |
expressions are equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
148 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
149 |
33
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
150 |
00:01:42,470 --> 00:01:46,595
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
151 |
And we use here this notation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
152 |
of the triple equals.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
153 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
154 |
34
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
155 |
00:01:46,595 --> 00:01:48,215
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
156 |
We say a regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
157 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
158 |
35
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
159 |
00:01:48,215 --> 00:01:50,180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
160 |
r1 and r2 are
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
161 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
162 |
36
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
163 |
00:01:50,180 --> 00:01:56,059
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
164 |
equivalent if and only
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
165 |
if the language of r1 is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
166 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
167 |
37
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
168 |
00:01:56,059 --> 00:01:59,360
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
169 |
equal to the language of r2.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
170 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
171 |
38
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
172 |
00:01:59,360 --> 00:02:02,915
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
173 |
Sounds complicated,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
174 |
but essentially means
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
175 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
176 |
39
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
177 |
00:02:02,915 --> 00:02:04,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
178 |
if the two regular expressions can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
179 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
180 |
40
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
181 |
00:02:04,700 --> 00:02:06,950
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
182 |
match exactly the same strings,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
183 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
184 |
41
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
185 |
00:02:06,950 --> 00:02:09,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
186 |
then we want to regard
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
187 |
them as equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
188 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
189 |
42
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
190 |
00:02:09,800 --> 00:02:14,300
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
191 |
This equivalence justifies
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
192 |
why we can be sloppy
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
193 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
194 |
43
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
195 |
00:02:14,300 --> 00:02:16,040
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
196 |
with parentheses.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
197 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
198 |
44
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
199 |
00:02:16,040 --> 00:02:23,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
200 |
For example, if we have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
201 |
(r1 + r2) + r3,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
202 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
203 |
45
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
204 |
00:02:23,870 --> 00:02:32,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
205 |
then this will be equivalent
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
206 |
to r1 + (r2 + r3).
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
207 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
208 |
46
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
209 |
00:02:32,270 --> 00:02:34,910
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
210 |
Remember, regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
211 |
expressions are trees,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
212 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
213 |
47
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
214 |
00:02:34,910 --> 00:02:37,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
215 |
so these are two different
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
216 |
regular expressions,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
217 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
218 |
48
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
219 |
00:02:37,940 --> 00:02:41,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
220 |
but they can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
221 |
the same strings.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
222 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
223 |
49
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
224 |
00:02:41,540 --> 00:02:45,695
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
225 |
Because, well, if we take
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
226 |
here the meaning of that,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
227 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
228 |
50
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
229 |
00:02:45,695 --> 00:02:54,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
230 |
that would be just L(r1 + r2 + r3),
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
231 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
232 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
233 |
51
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
234 |
00:02:54,350 --> 00:03:04,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
235 |
which is equal to L(r1 + r2) u L(r3).
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
236 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
237 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
238 |
52
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
239 |
00:03:04,100 --> 00:03:10,595
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
240 |
And that is equal to of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
241 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
242 |
53
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
243 |
00:03:10,595 --> 00:03:15,710
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
244 |
L(r1) u L(r2) u L(r3).
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
245 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
246 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
247 |
54
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
248 |
00:03:15,710 --> 00:03:17,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
249 |
And if you do the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
250 |
same calculation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
251 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
252 |
55
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
253 |
00:03:17,930 --> 00:03:19,445
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
254 |
for that regular expression,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
255 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
256 |
56
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
257 |
00:03:19,445 --> 00:03:22,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
258 |
you will find out the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
259 |
two sets are the same.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
260 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
261 |
57
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
262 |
00:03:22,940 --> 00:03:26,195
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
263 |
So both regular expressions
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
264 |
can match the same strings.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
265 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
266 |
58
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
267 |
00:03:26,195 --> 00:03:28,805
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
268 |
So even if they're different
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
269 |
regular expressions,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
270 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
271 |
59
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
272 |
00:03:28,805 --> 00:03:31,220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
273 |
we can regard them as eqivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
274 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
275 |
60
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
276 |
00:03:31,220 --> 00:03:33,290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
277 |
And so that's why we can forget
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
278 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
279 |
61
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
280 |
00:03:33,290 --> 00:03:35,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
281 |
about writing these parentheses.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
282 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
283 |
62
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
284 |
00:03:35,270 --> 00:03:40,205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
285 |
Let's have a look
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
286 |
at some more examples.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
287 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
288 |
63
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
289 |
00:03:40,205 --> 00:03:41,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
290 |
So the first one here,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
291 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
292 |
64
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
293 |
00:03:41,870 --> 00:03:43,205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
294 |
that is now clear.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
295 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
296 |
65
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
297 |
00:03:43,205 --> 00:03:45,200
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
298 |
We did this calculation already
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
299 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
300 |
66
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
301 |
00:03:45,200 --> 00:03:47,480
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
302 |
for arbitrary regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
303 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
304 |
67
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
305 |
00:03:47,480 --> 00:03:49,520
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
306 |
Here it is for
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
307 |
concrete ones a, b and c.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
308 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
309 |
68
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
310 |
00:03:49,520 --> 00:03:52,690
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
311 |
Here on the left-hand side,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
312 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
313 |
69
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
314 |
00:03:52,690 --> 00:03:54,895
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
315 |
the regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
316 |
has the same meaning
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
317 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
318 |
70
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
319 |
00:03:54,895 --> 00:03:56,620
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
320 |
as on the right-hand side.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
321 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
322 |
71
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
323 |
00:03:56,620 --> 00:03:58,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
324 |
So they are equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
325 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
326 |
72
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
327 |
00:03:58,420 --> 00:04:01,375
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
328 |
We can ignore the parentheses.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
329 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
330 |
73
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
331 |
00:04:01,375 --> 00:04:03,220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
332 |
If I have a choice,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
333 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
334 |
74
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
335 |
00:04:03,220 --> 00:04:06,610
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
336 |
but the choice is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
337 |
the same a or a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
338 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
339 |
75
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
340 |
00:04:06,610 --> 00:04:09,265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
341 |
then this is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
342 |
equivalent to just a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
343 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
344 |
76
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
345 |
00:04:09,265 --> 00:04:13,075
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
346 |
So the same choice doesn't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
347 |
introduce anything more.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
348 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
349 |
77
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
350 |
00:04:13,075 --> 00:04:15,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
351 |
In the next case, if I have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
352 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
353 |
78
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
354 |
00:04:15,370 --> 00:04:19,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
355 |
a regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
356 |
which can match a or b,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
357 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
358 |
79
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
359 |
00:04:19,450 --> 00:04:23,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
360 |
that can match the same
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
361 |
strings as b or a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
362 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
363 |
80
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
364 |
00:04:23,860 --> 00:04:27,325
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
365 |
So you have a kind of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
366 |
commutativity for the plus,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
367 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
368 |
81
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
369 |
00:04:27,325 --> 00:04:29,485
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
370 |
which is like on natural numbers.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
371 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
372 |
82
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
373 |
00:04:29,485 --> 00:04:32,880
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
374 |
But you would not have a
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
375 |
communitivity for the sequence:
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
376 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
377 |
83
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
378 |
00:04:32,880 --> 00:04:37,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
379 |
if you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
380 |
first a and then b,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
381 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
382 |
84
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
383 |
00:04:37,070 --> 00:04:40,850
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
384 |
that's not the same as
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
385 |
matching first b and then a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
386 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
387 |
85
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
388 |
00:04:40,850 --> 00:04:42,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
389 |
So for the sequence ...
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
390 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
391 |
86
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
392 |
00:04:42,800 --> 00:04:44,615
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
393 |
they are not equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
394 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
395 |
87
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
396 |
00:04:44,615 --> 00:04:49,475
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
397 |
However, for the sequence I
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
398 |
can, like for the plus, ignore
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
399 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
400 |
88
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
401 |
00:04:49,475 --> 00:04:51,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
402 |
prarentheses.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
403 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
404 |
89
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
405 |
00:04:51,245 --> 00:04:55,070
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
406 |
If I have the parentheses
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
407 |
and this way,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
408 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
409 |
90
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
410 |
00:04:55,070 --> 00:04:57,785
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
411 |
or I have it in this way.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
412 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
413 |
91
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
414 |
00:04:57,785 --> 00:05:00,605
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
415 |
These are two different
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
416 |
regular expressions,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
417 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
418 |
92
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
419 |
00:05:00,605 --> 00:05:02,120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
420 |
but they have the same meaning.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
421 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
422 |
93
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
423 |
00:05:02,120 --> 00:05:03,815
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
424 |
So they are equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
425 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
426 |
94
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
427 |
00:05:03,815 --> 00:05:05,780
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
428 |
And so I can leave out parentheses
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
429 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
430 |
95
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
431 |
00:05:05,780 --> 00:05:09,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
432 |
for times as well.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
433 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
434 |
96
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
435 |
00:05:09,170 --> 00:05:12,185
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
436 |
The next one is a slightly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
437 |
more interesting one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
438 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
439 |
97
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
440 |
00:05:12,185 --> 00:05:15,020
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
441 |
If I have a regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
442 |
expression which can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
443 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
444 |
98
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
445 |
00:05:15,020 --> 00:05:19,655
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
446 |
c first followed by (a + b),
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
447 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
448 |
99
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
449 |
00:05:19,655 --> 00:05:25,355
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
450 |
then this is the same as
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
451 |
first c followed by a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
452 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
453 |
100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
454 |
00:05:25,355 --> 00:05:28,640
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
455 |
or c followed by b.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
456 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
457 |
101
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
458 |
00:05:28,640 --> 00:05:31,265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
459 |
So that's the kind of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
460 |
distributivity law
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
461 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
462 |
102
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
463 |
00:05:31,265 --> 00:05:33,545
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
464 |
on regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
465 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
466 |
103
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
467 |
00:05:33,545 --> 00:05:36,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
468 |
But they're also regular expressions
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
469 |
which are not equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
470 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
471 |
104
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
472 |
00:05:36,350 --> 00:05:38,990
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
473 |
If I have the regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
474 |
expression which can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
475 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
476 |
105
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
477 |
00:05:38,990 --> 00:05:42,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
478 |
match the string containing
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
479 |
exactly two a's.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
480 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
481 |
106
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
482 |
00:05:42,800 --> 00:05:44,240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
483 |
That is not equivalent
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
484 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
485 |
107
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
486 |
00:05:44,240 --> 00:05:46,730
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
487 |
to the regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
488 |
expression which can just match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
489 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
490 |
108
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
491 |
00:05:46,730 --> 00:05:49,250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
492 |
a single a. And similarly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
493 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
494 |
109
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
495 |
00:05:49,250 --> 00:05:51,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
496 |
in this case, if I can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
497 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
498 |
110
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
499 |
00:05:51,680 --> 00:05:56,075
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
500 |
a or the string b followed by c,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
501 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
502 |
111
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
503 |
00:05:56,075 --> 00:05:59,825
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
504 |
that is not the same as a or b,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
505 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
506 |
112
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
507 |
00:05:59,825 --> 00:06:02,000
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
508 |
followed by a or c.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
509 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
510 |
113
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
511 |
00:06:02,000 --> 00:06:05,990
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
512 |
I'll let you think about
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
513 |
why is that not equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
514 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
515 |
114
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
516 |
00:06:05,990 --> 00:06:08,060
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
517 |
Essentially you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
518 |
have to find out what's
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
519 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
520 |
115
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
521 |
00:06:08,060 --> 00:06:10,475
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
522 |
the meaning of both
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
523 |
regular expressions.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
524 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
525 |
116
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
526 |
00:06:10,475 --> 00:06:14,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
527 |
And are they the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
528 |
same sets or not?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
529 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
530 |
117
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
531 |
00:06:14,090 --> 00:06:17,435
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
532 |
There are again some
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
533 |
interesting corner cases.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
534 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
535 |
118
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
536 |
00:06:17,435 --> 00:06:20,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
537 |
If I have a regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
538 |
that can match a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
539 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
540 |
119
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
541 |
00:06:20,540 --> 00:06:23,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
542 |
but followed by the regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
543 |
expression which cannot match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
544 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
545 |
120
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
546 |
00:06:23,450 --> 00:06:25,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
547 |
anything, that is not equivalent
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
548 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
549 |
121
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
550 |
00:06:25,670 --> 00:06:29,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
551 |
to the regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
552 |
expression which can match a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
553 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
554 |
122
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
555 |
00:06:29,255 --> 00:06:31,340
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
556 |
Again here you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
557 |
to do the calculation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
558 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
559 |
123
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
560 |
00:06:31,340 --> 00:06:32,915
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
561 |
to convince you of that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
562 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
563 |
124
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
564 |
00:06:32,915 --> 00:06:35,840
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
565 |
Similarly, if I have a regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
566 |
expression which can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
567 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
568 |
125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
569 |
00:06:35,840 --> 00:06:38,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
570 |
match a or the empty string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
571 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
572 |
126
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
573 |
00:06:38,750 --> 00:06:40,640
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
574 |
this is not equivalent to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
575 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
576 |
127
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
577 |
00:06:40,640 --> 00:06:43,355
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
578 |
the regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
579 |
which can just match a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
580 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
581 |
128
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
582 |
00:06:43,355 --> 00:06:46,925
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
583 |
Here are some interesting
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
584 |
ones with zeros and ones.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
585 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
586 |
129
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
587 |
00:06:46,925 --> 00:06:48,860
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
588 |
So if I have the regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
589 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
590 |
130
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
591 |
00:06:48,860 --> 00:06:50,975
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
592 |
that can match the empty string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
593 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
594 |
131
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
595 |
00:06:50,975 --> 00:06:53,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
596 |
this will be actually equivalent to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
597 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
598 |
132
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
599 |
00:06:53,540 --> 00:06:56,435
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
600 |
the regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
601 |
which can match nothing,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
602 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
603 |
133
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
604 |
00:06:56,435 --> 00:06:59,405
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
605 |
but star of that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
606 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
607 |
134
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
608 |
00:06:59,405 --> 00:07:01,970
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
609 |
Remember the star
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
610 |
always introduces,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
611 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
612 |
135
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
613 |
00:07:01,970 --> 00:07:04,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
614 |
no matter what, the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
615 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
616 |
136
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
617 |
00:07:04,370 --> 00:07:06,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
618 |
So this regular expression can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
619 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
620 |
137
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
621 |
00:07:06,170 --> 00:07:08,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
622 |
the empty string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
623 |
just like the 1.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
624 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
625 |
138
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
626 |
00:07:08,930 --> 00:07:12,125
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
627 |
So these two expressions
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
628 |
are not the same,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
629 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
630 |
139
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
631 |
00:07:12,125 --> 00:07:14,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
632 |
but they are equivalent.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
633 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
634 |
140
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
635 |
00:07:14,210 --> 00:07:16,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
636 |
And it doesn't matter
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
637 |
whether you take
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
638 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
639 |
141
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
640 |
00:07:16,700 --> 00:07:20,090
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
641 |
the empty string to the star,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
642 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
643 |
142
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
644 |
00:07:20,090 --> 00:07:23,855
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
645 |
because if I can match 0 or
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
646 |
more times the empty string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
647 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
648 |
143
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
649 |
00:07:23,855 --> 00:07:27,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
650 |
that will be equivalent to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
651 |
just the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
652 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
653 |
144
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
654 |
00:07:27,520 --> 00:07:32,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
655 |
Slightly similar to the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
656 |
third case is this one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
657 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
658 |
145
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
659 |
00:07:32,510 --> 00:07:35,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
660 |
Zero star is not equivalent to 0
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
661 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
662 |
146
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
663 |
00:07:35,720 --> 00:07:40,025
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
664 |
because that can match
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
665 |
exactly the empty string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
666 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
667 |
147
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
668 |
00:07:40,025 --> 00:07:42,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
669 |
This cannot match anything.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
670 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
671 |
148
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
672 |
00:07:42,740 --> 00:07:44,839
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
673 |
While the previous
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
674 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
675 |
149
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
676 |
00:07:44,839 --> 00:07:47,540
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
677 |
equivalences are all very
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
678 |
instructive to look at,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
679 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
680 |
150
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
681 |
00:07:47,540 --> 00:07:49,910
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
682 |
these are the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
683 |
equivalences we need
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
684 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
685 |
151
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
686 |
00:07:49,910 --> 00:07:52,685
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
687 |
in our regular expression matchers.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
688 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
689 |
152
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
690 |
00:07:52,685 --> 00:07:54,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
691 |
And they are defined for
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
692 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
693 |
153
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
694 |
00:07:54,350 --> 00:07:58,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
695 |
all regular expressions r.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
696 |
So r plus 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
697 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
698 |
154
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
699 |
00:07:58,160 --> 00:08:00,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
700 |
no matter what r looks
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
701 |
like is equivalent
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
702 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
703 |
155
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
704 |
00:08:00,470 --> 00:08:02,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
705 |
to just r. Similarly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
706 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
707 |
156
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
708 |
00:08:02,945 --> 00:08:05,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
709 |
0 plus r is also
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
710 |
equivalent to r.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
711 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
712 |
157
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
713 |
00:08:05,930 --> 00:08:08,525
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
714 |
The order of this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
715 |
choice doesn't matter;
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
716 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
717 |
158
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
718 |
00:08:08,525 --> 00:08:11,495
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
719 |
r followed by 1,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
720 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
721 |
159
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
722 |
00:08:11,495 --> 00:08:14,030
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
723 |
that's the sequence
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
724 |
regular expression, is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
725 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
726 |
160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
727 |
00:08:14,030 --> 00:08:16,760
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
728 |
equivalent to r. The
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
729 |
sam, r followed by
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
730 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
731 |
161
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
732 |
00:08:16,760 --> 00:08:19,010
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
733 |
r is equivalent to r.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
734 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
735 |
162
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
736 |
00:08:19,010 --> 00:08:20,990
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
737 |
And r followed by
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
738 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
739 |
163
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
740 |
00:08:20,990 --> 00:08:23,390
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
741 |
the regular expression which
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
742 |
cannot match anything,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
743 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
744 |
164
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
745 |
00:08:23,390 --> 00:08:27,455
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
746 |
is equivalent to just 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
747 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
748 |
165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
749 |
00:08:27,455 --> 00:08:30,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
750 |
And 0 followed by r is also equivalent to 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
751 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
752 |
166
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
753 |
00:08:30,740 --> 00:08:33,615
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
754 |
And if you have the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
755 |
choice of r plus r,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
756 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
757 |
167
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
758 |
00:08:33,615 --> 00:08:37,210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
759 |
that is also
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
760 |
equivalent to just r.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
761 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
762 |
168
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
763 |
00:08:37,210 --> 00:08:40,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
764 |
What we're going to do
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
765 |
with these equivalences is
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
766 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
767 |
169
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
768 |
00:08:40,270 --> 00:08:42,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
769 |
that we regard them as
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
770 |
simplification rules.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
771 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
772 |
170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
773 |
00:08:42,820 --> 00:08:43,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
774 |
So whenever we see
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
775 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
776 |
171
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
777 |
00:08:43,930 --> 00:08:46,465
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
778 |
this regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
779 |
in our algorithm,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
780 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
781 |
172
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
782 |
00:08:46,465 --> 00:08:48,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
783 |
we will replace it by
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
784 |
the right-hand side.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
785 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
786 |
173
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
787 |
00:08:48,580 --> 00:08:51,715
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
788 |
So we will orient
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
789 |
these equivalences.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
790 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
791 |
174
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
792 |
00:08:51,715 --> 00:08:53,650
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
793 |
If we see, this regular expression,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
794 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
795 |
175
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
796 |
00:08:53,650 --> 00:08:55,225
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
797 |
we will replace it by that one.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
798 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
799 |
176
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
800 |
00:08:55,225 --> 00:08:58,945
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
801 |
And it will not matter
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
802 |
because the left-hand sides
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
803 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
804 |
177
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
805 |
00:08:58,945 --> 00:09:01,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
806 |
can match exactly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
807 |
the same strings
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
808 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
809 |
178
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
810 |
00:09:01,255 --> 00:09:03,475
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
811 |
as the right-hand sides.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
812 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
813 |
179
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
814 |
00:09:03,475 --> 00:09:06,370
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
815 |
Here two quick examples.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
816 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
817 |
180
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
818 |
00:09:06,370 --> 00:09:08,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
819 |
The first one, let's
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
820 |
assume you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
821 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
822 |
181
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
823 |
00:09:08,680 --> 00:09:10,270
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
824 |
a regular expression r and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
825 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
826 |
182
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
827 |
00:09:10,270 --> 00:09:11,905
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
828 |
there is something
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
829 |
in front of it.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
830 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
831 |
183
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
832 |
00:09:11,905 --> 00:09:13,720
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
833 |
This "something in front of it"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
834 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
835 |
184
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
836 |
00:09:13,720 --> 00:09:15,870
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
837 |
can be simplified as follows.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
838 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
839 |
185
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
840 |
00:09:15,870 --> 00:09:20,000
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
841 |
This 1 times b
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
842 |
can be simplified to b.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
843 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
844 |
186
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
845 |
00:09:20,000 --> 00:09:23,555
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
846 |
Then this b plus 0 can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
847 |
be simplified to b.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
848 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
849 |
187
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
850 |
00:09:23,555 --> 00:09:25,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
851 |
And assuming that nothing can
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
852 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
853 |
188
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
854 |
00:09:25,490 --> 00:09:27,470
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
855 |
be simplified inside this r,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
856 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
857 |
189
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
858 |
00:09:27,470 --> 00:09:28,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
859 |
then this would be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
860 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
861 |
190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
862 |
00:09:28,700 --> 00:09:33,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
863 |
the simplified version
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
864 |
of this regular expression.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
865 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
866 |
191
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
867 |
00:09:33,050 --> 00:09:34,820
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
868 |
And because the simplification
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
869 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
870 |
192
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
871 |
00:09:34,820 --> 00:09:36,965
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
872 |
rules preserve what can be matched,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
873 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
874 |
193
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
875 |
00:09:36,965 --> 00:09:39,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
876 |
we can be sure that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
877 |
this regular expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
878 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
879 |
194
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
880 |
00:09:39,080 --> 00:09:41,255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
881 |
can match exactly the strings
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
882 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
883 |
195
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
884 |
00:09:41,255 --> 00:09:43,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
885 |
this regular expression can match.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
886 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
887 |
196
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
888 |
00:09:43,940 --> 00:09:45,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
889 |
Here is the other example.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
890 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
891 |
197
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
892 |
00:09:45,740 --> 00:09:49,550
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
893 |
This has just a tiny change
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
894 |
that this becomes here as 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
895 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
896 |
198
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
897 |
00:09:49,550 --> 00:09:54,485
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
898 |
Then 0 times b can be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
899 |
replaced by just 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
900 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
901 |
199
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
902 |
00:09:54,485 --> 00:09:56,705
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
903 |
Then they are actually two
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
904 |
rules which could apply
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
905 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
906 |
200
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
907 |
00:09:56,705 --> 00:09:59,014
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
908 |
either that we have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
909 |
the same choice
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
910 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
911 |
201
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
912 |
00:09:59,014 --> 00:10:01,160
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
913 |
or we can just say something plus
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
914 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
915 |
202
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
916 |
00:10:01,160 --> 00:10:04,100
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
917 |
0 will always go to something.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
918 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
919 |
203
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
920 |
00:10:04,100 --> 00:10:06,245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
921 |
So we can simplify it to that.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
922 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
923 |
204
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
924 |
00:10:06,245 --> 00:10:08,510
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
925 |
And then we have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
926 |
0 times r again,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
927 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
928 |
205
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
929 |
00:10:08,510 --> 00:10:10,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
930 |
and that can be simplified to 0.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
931 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
932 |
206
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
933 |
00:10:10,460 --> 00:10:12,080
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
934 |
So actually what we find out with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
935 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
936 |
207
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
937 |
00:10:12,080 --> 00:10:14,645
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
938 |
this calculation is that
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
939 |
this regular expression,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
940 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
941 |
208
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
942 |
00:10:14,645 --> 00:10:16,835
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
943 |
even if it looks
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
944 |
quite complicated,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
945 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
946 |
209
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
947 |
00:10:16,835 --> 00:10:19,295
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
948 |
actually doesn't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
949 |
match any string.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
950 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
951 |
210
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
952 |
00:10:19,295 --> 00:10:21,290
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
953 |
Because it matches exactly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
954 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
955 |
211
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
956 |
00:10:21,290 --> 00:10:23,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
957 |
those string this regular
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
958 |
expression can match.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
959 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
960 |
212
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
961 |
00:10:23,420 --> 00:10:26,285
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
962 |
And this reg expression
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
963 |
cannot match any.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
964 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
965 |
213
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
966 |
00:10:26,285 --> 00:10:29,930
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
967 |
We need one more
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
968 |
operation on languages.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
969 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
970 |
214
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
971 |
00:10:29,930 --> 00:10:31,700
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
972 |
I call this operation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
973 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
974 |
215
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
975 |
00:10:31,700 --> 00:10:35,165
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
976 |
the semantic derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
977 |
of a language.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
978 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
979 |
216
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
980 |
00:10:35,165 --> 00:10:37,775
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
981 |
This operation takes
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
982 |
two arguments.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
983 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
984 |
217
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
985 |
00:10:37,775 --> 00:10:40,670
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
986 |
It takes a character
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
987 |
which we take
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
988 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
989 |
218
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
990 |
00:10:40,670 --> 00:10:43,925
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
991 |
the semantic derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
992 |
according to,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
993 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
994 |
219
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
995 |
00:10:43,925 --> 00:10:45,980
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
996 |
and it takes a language.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
997 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
998 |
220
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
999 |
00:10:45,980 --> 00:10:49,579
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1000 |
And what it does is it
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1001 |
looks into this language
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1002 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1003 |
221
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1004 |
00:10:49,579 --> 00:10:51,365
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1005 |
and looks for all the strings
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1006 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1007 |
222
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1008 |
00:10:51,365 --> 00:10:53,735
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1009 |
that start with this character,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1010 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1011 |
223
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1012 |
00:10:53,735 --> 00:10:56,405
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1013 |
let's say c, and then
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1014 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1015 |
224
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1016 |
00:10:56,405 --> 00:11:00,920
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1017 |
just strips off that c.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1018 |
So here's an example.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1019 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1020 |
225
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1021 |
00:11:00,920 --> 00:11:02,975
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1022 |
Suppose you have a language A,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1023 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1024 |
226
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1025 |
00:11:02,975 --> 00:11:04,460
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1026 |
with the strings
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1027 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1028 |
227
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1029 |
00:11:04,460 --> 00:11:06,965
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1030 |
foo, bar and frak.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1031 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1032 |
228
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1033 |
00:11:06,965 --> 00:11:10,835
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1034 |
And you take the semantic
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1035 |
derivative according to f,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1036 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1037 |
229
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1038 |
00:11:10,835 --> 00:11:14,450
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1039 |
then we discard all the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1040 |
strings which do not
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1041 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1042 |
230
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1043 |
00:11:14,450 --> 00:11:18,320
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1044 |
start with an f. So
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1045 |
bar will be discarded.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1046 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1047 |
231
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1048 |
00:11:18,320 --> 00:11:22,850
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1049 |
Foo and frac start with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1050 |
an f. So we keep them
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1051 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1052 |
232
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1053 |
00:11:22,850 --> 00:11:25,265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1054 |
but we strip off the first f.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1055 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1056 |
233
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1057 |
00:11:25,265 --> 00:11:29,045
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1058 |
So here we have only oo and rak.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1059 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1060 |
234
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1061 |
00:11:29,045 --> 00:11:31,609
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1062 |
If you take the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1063 |
semantic derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1064 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1065 |
235
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1066 |
00:11:31,609 --> 00:11:33,830
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1067 |
of that language according to b,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1068 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1069 |
236
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1070 |
00:11:33,830 --> 00:11:37,190
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1071 |
then we will discard foo and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1072 |
frak because they don't
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1073 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1074 |
237
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1075 |
00:11:37,190 --> 00:11:40,940
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1076 |
start with b, and just keep bar.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1077 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1078 |
238
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1079 |
00:11:40,940 --> 00:11:44,585
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1080 |
But again, we have to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1081 |
strip off this first b.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1082 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1083 |
239
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1084 |
00:11:44,585 --> 00:11:49,305
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1085 |
And if you take the semantic
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1086 |
derivative according to a,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1087 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1088 |
240
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1089 |
00:11:49,305 --> 00:11:52,585
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1090 |
then none of these
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1091 |
strings start with a.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1092 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1093 |
241
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1094 |
00:11:52,585 --> 00:11:56,800
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1095 |
So this will be defined
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1096 |
as just the empty set.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1097 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1098 |
242
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1099 |
00:11:56,800 --> 00:11:59,695
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1100 |
You can slightly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1101 |
generalized this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1102 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1103 |
243
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1104 |
00:11:59,695 --> 00:12:02,560
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1105 |
semantic derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1106 |
to also strings.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1107 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1108 |
244
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1109 |
00:12:02,560 --> 00:12:05,170
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1110 |
So imagine you have
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1111 |
a language A and you
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1112 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1113 |
245
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1114 |
00:12:05,170 --> 00:12:08,274
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1115 |
build the semantic derivative
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1116 |
according to a string s.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1117 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1118 |
246
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1119 |
00:12:08,274 --> 00:12:10,990
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1120 |
Then you look in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1121 |
this language and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1122 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1123 |
247
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1124 |
00:12:10,990 --> 00:12:13,420
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1125 |
you look for all the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1126 |
strings that start with
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1127 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1128 |
248
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1129 |
00:12:13,420 --> 00:12:19,555
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1130 |
this s. But you strip
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1131 |
off that s. Ok?
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1132 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1133 |
249
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1134 |
00:12:19,555 --> 00:12:23,830
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1135 |
So if you have a string
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1136 |
starting with the s,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1137 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1138 |
250
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1139 |
00:12:23,830 --> 00:12:26,065
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1140 |
then you keep that string,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1141 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1142 |
251
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1143 |
00:12:26,065 --> 00:12:27,490
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1144 |
but you keep only the rest...
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1145 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1146 |
252
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1147 |
00:12:27,490 --> 00:12:28,810
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1148 |
what's coming after this s.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1149 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1150 |
253
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1151 |
00:12:28,810 --> 00:12:32,010
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1152 |
That is here indicated
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1153 |
with this s'.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1154 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1155 |
254
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1156 |
00:12:32,010 --> 00:12:35,330
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1157 |
I also have this convention,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1158 |
this personal convention
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1159 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1160 |
255
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1161 |
00:12:35,330 --> 00:12:40,055
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1162 |
I have to say, that everything
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1163 |
which works on lists,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1164 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1165 |
256
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1166 |
00:12:40,055 --> 00:12:42,185
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1167 |
remember strings are
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1168 |
lists of characters.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1169 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1170 |
257
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1171 |
00:12:42,185 --> 00:12:46,655
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1172 |
I just put there an 's'. So
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1173 |
here's the one for characters.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1174 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1175 |
258
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1176 |
00:12:46,655 --> 00:12:48,680
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1177 |
I just call it Der with a capital
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1178 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1179 |
259
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1180 |
00:12:48,680 --> 00:12:51,740
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1181 |
D. And I call that Ders,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1182 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1183 |
260
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1184 |
00:12:51,740 --> 00:12:54,350
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1185 |
because that works over strings.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1186 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1187 |
261
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1188 |
00:12:54,350 --> 00:12:55,865
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1189 |
And you can see how it would
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1190 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1191 |
262
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1192 |
00:12:55,865 --> 00:12:59,750
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1193 |
be defined if you only take this
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1194 |
as a primitive operation.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1195 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1196 |
263
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1197 |
00:12:59,750 --> 00:13:01,340
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1198 |
We would just need to iterate
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1199 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1200 |
264
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1201 |
00:13:01,340 --> 00:13:04,050
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1202 |
that essentially for this Ders.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1203 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1204 |
265
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1205 |
00:13:04,060 --> 00:13:07,970
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1206 |
Ok, we now have all
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1207 |
the theory in place.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1208 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1209 |
266
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1210 |
00:13:07,970 --> 00:13:11,345
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1211 |
And we can finally start
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1212 |
implementing our algorithm.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1213 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1214 |
267
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1215 |
00:13:11,345 --> 00:13:14,580
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1216 |
That's when we'll do
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1217 |
in the next video.
|