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