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