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