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