| 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:05,810 --> 00:00:11,039
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |      3 | Okay, so we have strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |      4 | The empty string and string "abc".
 | 
| 
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:11,039 --> 00:00:13,200
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |      8 | And we can take the head
 | 
| 
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:13,200 --> 00:00:15,615
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     12 | of a string and the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     13 | tail of the string,
 | 
| 
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:15,615 --> 00:00:18,480
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     17 | since we regard them as
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     18 | lists of characters.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     19 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     20 | 5
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     21 | 00:00:18,480 --> 00:00:22,230
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     22 | We also introduced the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     23 | notion of a language.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     24 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     25 | 6
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     26 | 00:00:22,230 --> 00:00:25,305
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     27 | A language is just
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     28 | a set of strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     29 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     30 | 7
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     31 | 00:00:25,305 --> 00:00:26,700
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     32 | So here's a language.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     33 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     34 | 8
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     35 | 00:00:26,700 --> 00:00:28,275
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     36 | It contains the empty string,
 | 
| 
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:28,275 --> 00:00:30,360
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     40 | the string hello, string foobar,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     41 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     42 | 10
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     43 | 00:00:30,360 --> 00:00:31,965
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     44 | the string, which is
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     45 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     46 | 11
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     47 | 00:00:31,965 --> 00:00:34,874
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     48 | just a character a and
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     49 | the string abc.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     50 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     51 | 12
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     52 | 00:00:34,874 --> 00:00:37,800
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     53 | There will be also other
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     54 | languages, which for example,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     55 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     56 | 13
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     57 | 00:00:37,800 --> 00:00:39,780
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     58 | contain infinitely many strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     59 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     60 | 14
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     61 | 00:00:39,780 --> 00:00:42,190
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     62 | Actually that will
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     63 | happen quite often.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     64 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     65 | 15
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     66 | 00:00:42,190 --> 00:00:45,560
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     67 | Now, you've seen this operation
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     68 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     69 | 16
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     70 | 00:00:45,560 --> 00:00:47,660
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     71 | of concatenation of two strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     72 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     73 | 17
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     74 | 00:00:47,660 --> 00:00:50,840
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     75 | So if you have the string
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     76 | foo and a string bar,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     77 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     78 | 18
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     79 | 00:00:50,840 --> 00:00:53,255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     80 | we can just put them
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     81 | next to each other.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     82 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     83 | 19
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     84 | 00:00:53,255 --> 00:00:57,725
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     85 | We will now extend that
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     86 | notion also told languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     87 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     88 | 20
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     89 | 00:00:57,725 --> 00:01:02,270
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     90 | So assume you have a
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     91 | language A and a language B.
 | 
| 
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:02,270 --> 00:01:05,825
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     95 | That means we take every
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     96 | string from the language
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     97 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     98 | 22
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |     99 | 00:01:05,825 --> 00:01:11,195
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    100 | A and concatenate it with every
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    101 | string of the language B.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    102 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    103 | 23
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    104 | 00:01:11,195 --> 00:01:13,160
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    105 | Here's an example.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    106 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    107 | 24
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    108 | 00:01:13,160 --> 00:01:14,750
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    109 | If you have the language A
 | 
| 
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:14,750 --> 00:01:17,030
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    113 | containing foo and bar as strings,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    114 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    115 | 26
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    116 | 00:01:17,030 --> 00:01:20,585
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    117 | and the language B containing
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    118 | a and b as strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    119 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    120 | 27
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    121 | 00:01:20,585 --> 00:01:23,000
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    122 | Then concatenating
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    123 | these two languages
 | 
| 
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:23,000 --> 00:01:27,110
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    127 | means I take foo with this a and b,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    128 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    129 | 29
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    130 | 00:01:27,110 --> 00:01:28,625
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    131 | giving fooa and foob,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    132 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    133 | 30
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    134 | 00:01:28,625 --> 00:01:30,905
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    135 | and I take bar and
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    136 | concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    137 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    138 | 31
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    139 | 00:01:30,905 --> 00:01:34,160
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    140 | a and b, giving bara and barb.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    141 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    142 | 32
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    143 | 00:01:34,160 --> 00:01:36,185
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    144 | So the pointer is we're
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    145 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    146 | 33
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    147 | 00:01:36,185 --> 00:01:39,110
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    148 | overloading this notion
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    149 | of concatenating
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    150 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    151 | 34
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    152 | 00:01:39,110 --> 00:01:45,020
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    153 | two strings also to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    154 | concatenating two languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    155 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    156 | 35
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    157 | 00:01:45,020 --> 00:01:48,890
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    158 | Okay, here are two corner
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    159 | cases of this definition.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    160 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    161 | 36
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    162 | 00:01:48,890 --> 00:01:51,395
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    163 | What happens if I
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    164 | have any language,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    165 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    166 | 37
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    167 | 00:01:51,395 --> 00:01:54,470
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    168 | say A, and I concatenate it with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    169 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    170 | 38
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    171 | 00:01:54,470 --> 00:01:58,640
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    172 | the language which contains
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    173 | only the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    174 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    175 | 39
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    176 | 00:01:58,640 --> 00:02:02,270
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    177 | And secondly, if I
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    178 | have any language,
 | 
| 
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:02,270 --> 00:02:04,220
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    182 | say again A, and I
 | 
| 
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:04,220 --> 00:02:05,870
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    186 | concatenate it with the language
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    187 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    188 | 42
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    189 | 00:02:05,870 --> 00:02:08,345
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    190 | which doesn't contain any string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    191 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    192 | 43
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    193 | 00:02:08,345 --> 00:02:11,720
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    194 | How would these two
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    195 | cases be defined?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    196 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    197 | 44
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    198 | 00:02:11,720 --> 00:02:16,055
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    199 | Remember, this language here
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    200 | contains a single element,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    201 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    202 | 45
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    203 | 00:02:16,055 --> 00:02:17,645
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    204 | namely the empty string,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    205 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    206 | 46
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    207 | 00:02:17,645 --> 00:02:20,210
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    208 | while this language 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    209 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    210 | 47
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    211 | 00:02:20,210 --> 00:02:23,585
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    212 | does not contain any
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    213 | string. It is empty.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    214 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    215 | 48
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    216 | 00:02:23,585 --> 00:02:26,930
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    217 | So these are two
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    218 | different languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    219 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    220 | 49
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    221 | 00:02:26,930 --> 00:02:29,960
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    222 | Think about how this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    223 | would be defined.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    224 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    225 | 50
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    226 | 00:02:29,960 --> 00:02:33,455
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    227 | So what's the point of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    228 | all these definitions?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    229 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    230 | 51
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    231 | 00:02:33,455 --> 00:02:36,110
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    232 | Well, we want to make precise
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    233 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    234 | 52
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    235 | 00:02:36,110 --> 00:02:38,735
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    236 | what is the meaning of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    237 | a regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    238 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    239 | 53
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    240 | 00:02:38,735 --> 00:02:41,510
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    241 | For this, we use
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    242 | this function L. It
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    243 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    244 | 54
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    245 | 00:02:41,510 --> 00:02:44,180
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    246 | will take a regular expression as
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    247 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    248 | 55
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    249 | 00:02:44,180 --> 00:02:47,150
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    250 | argument and generates a
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    251 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    252 | 56
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    253 | 00:02:47,150 --> 00:02:49,970
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    254 | set of strings or a language.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    255 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    256 | 57
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    257 | 00:02:49,970 --> 00:02:52,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    258 | And it's supposed to be the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    259 | language which contains
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    260 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    261 | 58
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    262 | 00:02:52,670 --> 00:02:56,330
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    263 | all the strings this regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    264 | expression can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    265 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    266 | 59
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    267 | 00:02:56,330 --> 00:02:58,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    268 | So remember the 0
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    269 | regular expression,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    270 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    271 | 60
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    272 | 00:02:58,670 --> 00:03:01,115
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    273 | it's not supposed to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    274 | match any string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    275 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    276 | 61
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    277 | 00:03:01,115 --> 00:03:05,105
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    278 | So we give it the empty
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    279 | language or empty set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    280 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    281 | 62
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    282 | 00:03:05,105 --> 00:03:06,740
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    283 | This regular expression,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    284 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    285 | 63
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    286 | 00:03:06,740 --> 00:03:09,380
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    287 | the one regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    288 | is supposed to match
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    289 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    290 | 64
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    291 | 00:03:09,380 --> 00:03:13,445
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    292 | exactly one string,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    293 | namely the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    294 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    295 | 65
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    296 | 00:03:13,445 --> 00:03:15,710
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    297 | the regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    298 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    299 | 66
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    300 | 00:03:15,710 --> 00:03:18,875
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    301 | recognizing just the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    302 | character c, in this case.
 | 
| 
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:18,875 --> 00:03:22,820
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    306 | Well, that will be the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    307 | language which contains
 | 
| 
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:22,820 --> 00:03:28,175
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    311 | the string only containing
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    312 | the single character c. 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    313 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    314 | 69
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    315 | 00:03:28,175 --> 00:03:31,295
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    316 | Now, what is this regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    317 | expression supposed to match?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    318 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    319 | 70
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    320 | 00:03:31,295 --> 00:03:34,835
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    321 | Well, a string is matched
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    322 | by this regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    323 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    324 | 71
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    325 | 00:03:34,835 --> 00:03:37,355
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    326 | if it is matched by
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    327 | the first component, r1,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    328 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    329 | 72
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    330 | 00:03:37,355 --> 00:03:40,970
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    331 | or by the second component, r2.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    332 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    333 | 73
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    334 | 00:03:40,970 --> 00:03:43,190
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    335 | That's why this plus
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    336 | is the alternative.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    337 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    338 | 74
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    339 | 00:03:43,190 --> 00:03:45,605
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    340 | So which are the strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    341 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    342 | 75
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    343 | 00:03:45,605 --> 00:03:48,320
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    344 | this regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    345 | can match? Well,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    346 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    347 | 76
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    348 | 00:03:48,320 --> 00:03:51,275
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    349 | all the strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    350 | r1 one can match,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    351 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    352 | 77
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    353 | 00:03:51,275 --> 00:03:54,170
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    354 | given by L(r1) union...
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    355 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    356 | 78
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    357 | 00:03:54,170 --> 00:03:57,380
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    358 | all the strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    359 | R2 can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    360 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    361 | 79
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    362 | 00:03:57,380 --> 00:04:01,325
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    363 | And we use here the union
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    364 | because this alternative,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    365 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    366 | 80
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    367 | 00:04:01,325 --> 00:04:05,945
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    368 | even if it says this string
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    369 | is matched by r1 or by r2.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    370 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    371 | 81
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    372 | 00:04:05,945 --> 00:04:08,465
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    373 | The meaning of this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    374 | reg expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    375 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    376 | 82
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    377 | 00:04:08,465 --> 00:04:11,209
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    378 | is the union of both languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    379 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    380 | 83
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    381 | 00:04:11,209 --> 00:04:14,315
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    382 | Now the sequence case.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    383 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    384 | 84
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    385 | 00:04:14,315 --> 00:04:17,960
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    386 | This means a string is
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    387 | matched by this regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    388 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    389 | 85
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    390 | 00:04:17,960 --> 00:04:20,510
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    391 | if the first part of this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    392 | string is matched by r1
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    393 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    394 | 86
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    395 | 00:04:20,510 --> 00:04:24,935
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    396 | and the second part of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    397 | the string is matched by r2.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    398 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    399 | 87
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    400 | 00:04:24,935 --> 00:04:28,490
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    401 | Now we have to say, which
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    402 | are all the strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    403 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    404 | 88
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    405 | 00:04:28,490 --> 00:04:31,645
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    406 | this regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    407 | can match. Well, it's
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    408 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    409 | 89
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    410 | 00:04:31,645 --> 00:04:34,495
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    411 | all the strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    412 | r1 can match,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    413 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    414 | 90
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    415 | 00:04:34,495 --> 00:04:39,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    416 | concatenated with all the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    417 | strings r2 can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    418 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    419 | 91
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    420 | 00:04:39,205 --> 00:04:42,895
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    421 | So for this, we have to use
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    422 | this concatenation operation.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    423 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    424 | 92
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    425 | 00:04:42,895 --> 00:04:47,440
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    426 | So if r1 can match a string
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    427 | and r2 can match a string,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    428 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    429 | 93
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    430 | 00:04:47,440 --> 00:04:51,220
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    431 | then in the meaning will be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    432 | the concatenation of that.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    433 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    434 | 94
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    435 | 00:04:51,220 --> 00:04:53,170
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    436 | So with this function L
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    437 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    438 | 95
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    439 | 00:04:53,170 --> 00:04:56,995
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    440 | we can make precise
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    441 | what are the strings,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    442 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    443 | 96
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    444 | 00:04:56,995 --> 00:05:00,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    445 | *all* the strings a regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    446 | expression can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    447 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    448 | 97
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    449 | 00:05:00,205 --> 00:05:04,689
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    450 | The only case we haven't
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    451 | specified yet is the r*.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    452 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    453 | 98
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    454 | 00:05:04,689 --> 00:05:07,750
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    455 | For this, we need
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    456 | another operation
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    457 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    458 | 99
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    459 | 00:05:07,750 --> 00:05:12,470
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    460 | on languages or sets of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    461 | strings, which we do next.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    462 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    463 | 100
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    464 | 00:05:12,490 --> 00:05:17,285
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    465 | We introduce a power
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    466 | operation for languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    467 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    468 | 101
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    469 | 00:05:17,285 --> 00:05:19,100
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    470 | The power operation or
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    471 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    472 | 102
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    473 | 00:05:19,100 --> 00:05:22,835
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    474 | the nth power is
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    475 | defined recursively.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    476 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    477 | 103
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    478 | 00:05:22,835 --> 00:05:26,615
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    479 | So the A to the power of 0
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    480 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    481 | 104
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    482 | 00:05:26,615 --> 00:05:31,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    483 | would be defined as the set
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    484 | containing the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    485 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    486 | 105
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    487 | 00:05:31,205 --> 00:05:36,200
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    488 | And A to the power of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    489 | n + 1 would be A
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    490 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    491 | 106
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    492 | 00:05:36,200 --> 00:05:38,705
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    493 | concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    494 | A to the power of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    495 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    496 | 107
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    497 | 00:05:38,705 --> 00:05:42,160
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    498 | n. Here are a few examples.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    499 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    500 | 108
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    501 | 00:05:42,160 --> 00:05:45,380
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    502 | A to the power of four
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    503 | would be essentially
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    504 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    505 | 109
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    506 | 00:05:45,380 --> 00:05:47,660
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    507 | A concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    508 | A concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    509 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    510 | 110
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    511 | 00:05:47,660 --> 00:05:49,640
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    512 | A concatenated with A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    513 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    514 | 111
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    515 | 00:05:49,640 --> 00:05:51,650
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    516 | and also concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    517 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    518 | 112
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    519 | 00:05:51,650 --> 00:05:55,580
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    520 | the language which
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    521 | contains the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    522 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    523 | 113
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    524 | 00:05:55,580 --> 00:05:57,275
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    525 | Because that's how we define
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    526 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    527 | 114
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    528 | 00:05:57,275 --> 00:05:59,975
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    529 | the base case, A
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    530 | to the power of 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    531 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    532 | 115
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    533 | 00:05:59,975 --> 00:06:03,410
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    534 | And A to the power
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    535 | one would be just A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    536 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    537 | 116
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    538 | 00:06:03,410 --> 00:06:05,330
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    539 | again followed by that one,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    540 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    541 | 117
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    542 | 00:06:05,330 --> 00:06:07,790
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    543 | but this would be just A.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    544 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    545 | 118
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    546 | 00:06:07,790 --> 00:06:10,385
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    547 | And A to the power 0
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    548 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    549 | 119
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    550 | 00:06:10,385 --> 00:06:14,270
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    551 | is this language which
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    552 | contains the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    553 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    554 | 120
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    555 | 00:06:14,270 --> 00:06:16,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    556 | With this power operation,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    557 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    558 | 121
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    559 | 00:06:16,670 --> 00:06:19,505
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    560 | I can also fill in this case.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    561 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    562 | 122
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    563 | 00:06:19,505 --> 00:06:23,210
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    564 | Remember this r* operation
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    565 | is supposed to match
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    566 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    567 | 123
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    568 | 00:06:23,210 --> 00:06:27,680
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    569 | a string with either
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    570 | 0 or more copies of r.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    571 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    572 | 124
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    573 | 00:06:27,680 --> 00:06:31,940
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    574 | So the meaning of this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    575 | regular expression would be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    576 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    577 | 125
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    578 | 00:06:31,940 --> 00:06:37,475
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    579 | now the Union of all the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    580 | powers greater or equal than 0,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    581 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    582 | 126
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    583 | 00:06:37,475 --> 00:06:40,835
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    584 | of the language that r can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    585 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    586 | 127
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    587 | 00:06:40,835 --> 00:06:44,945
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    588 | And we take now at the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    589 | union of all these powers,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    590 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    591 | 128
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    592 | 00:06:44,945 --> 00:06:47,150
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    593 | that means essentially what
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    594 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    595 | 129
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    596 | 00:06:47,150 --> 00:06:48,530
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    597 | can the regular expression match
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    598 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    599 | 130
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    600 | 00:06:48,530 --> 00:06:51,440
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    601 | if I take L of r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    602 | to the 0th power,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    603 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    604 | 131
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    605 | 00:06:51,440 --> 00:06:53,030
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    606 | what can I match with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    607 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    608 | 132
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    609 | 00:06:53,030 --> 00:06:57,305
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    610 | the first power, the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    611 | second power, and so on.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    612 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    613 | 133
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    614 | 00:06:57,305 --> 00:07:00,544
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    615 | And I take the union
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    616 | of all these powers.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    617 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    618 | 134
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    619 | 00:07:00,544 --> 00:07:03,830
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    620 | That's the definition
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    621 | of which strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    622 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    623 | 135
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    624 | 00:07:03,830 --> 00:07:05,510
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    625 | this regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    626 | is supposed to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    627 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    628 | 136
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    629 | 00:07:05,510 --> 00:07:08,510
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    630 | match. The meaning of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    631 | this regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    632 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    633 | 137
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    634 | 00:07:08,510 --> 00:07:11,300
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    635 | This is such an
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    636 | important definition,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    637 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    638 | 138
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    639 | 00:07:11,300 --> 00:07:13,250
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    640 | that there's actually
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    641 | a name for it.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    642 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    643 | 139
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    644 | 00:07:13,250 --> 00:07:15,020
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    645 | It's called the Kleene star.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    646 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    647 | 140
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    648 | 00:07:15,020 --> 00:07:16,400
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    649 | And it's written like this.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    650 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    651 | 141
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    652 | 00:07:16,400 --> 00:07:18,335
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    653 | If I have a language A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    654 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    655 | 142
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    656 | 00:07:18,335 --> 00:07:21,785
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    657 | I can build the star
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    658 | of this language
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    659 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    660 | 143
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    661 | 00:07:21,785 --> 00:07:26,255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    662 | by union up all the powers
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    663 | greater or equal than 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    664 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    665 | 144
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    666 | 00:07:26,255 --> 00:07:28,580
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    667 | The A-star of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    668 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    669 | 145
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    670 | 00:07:28,580 --> 00:07:31,580
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    671 | a language would expand
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    672 | to a to the power 0,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    673 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    674 | 146
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    675 | 00:07:31,580 --> 00:07:33,770
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    676 | union A to the power of one,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    677 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    678 | 147
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    679 | 00:07:33,770 --> 00:07:36,665
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    680 | A to the power of two, and so on.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    681 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    682 | 148
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    683 | 00:07:36,665 --> 00:07:39,230
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    684 | And it would
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    685 | essentially mean, well,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    686 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    687 | 149
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    688 | 00:07:39,230 --> 00:07:43,460
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    689 | it's the language which contains
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    690 | the empty string because
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    691 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    692 | 150
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    693 | 00:07:43,460 --> 00:07:48,290
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    694 | of the A to the 0, one copy of A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    695 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    696 | 151
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    697 | 00:07:48,290 --> 00:07:51,020
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    698 | two concatenated copies of A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    699 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    700 | 152
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    701 | 00:07:51,020 --> 00:07:55,070
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    702 | three concatenated
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    703 | copies of A, and so on.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    704 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    705 | 153
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    706 | 00:07:55,070 --> 00:07:59,060
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    707 | So that's what this A-star
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    708 | is defined as.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    709 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    710 | 154
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    711 | 00:07:59,060 --> 00:08:03,725
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    712 | Essentially as the Union
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    713 | of all the powers.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    714 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    715 | 155
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    716 | 00:08:03,725 --> 00:08:05,990
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    717 | And it's essentially
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    718 | each power is how many
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    719 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    720 | 156
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    721 | 00:08:05,990 --> 00:08:08,750
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    722 | times I have to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    723 | concatenate this language A.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    724 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    725 | 157
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    726 | 00:08:08,750 --> 00:08:13,549
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    727 | And note that this language
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    728 | A-star will always contain
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    729 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    730 | 158
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    731 | 00:08:13,549 --> 00:08:21,240
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    732 | the empty string because that
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    733 | is how the A^0 is defined.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    734 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    735 | 159
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    736 | 00:08:21,310 --> 00:08:23,540
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    737 | So in this definition,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    738 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    739 | 160
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    740 | 00:08:23,540 --> 00:08:25,969
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    741 | I could have also written star
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    742 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    743 | 161
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    744 | 00:08:25,969 --> 00:08:29,180
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    745 | here because the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    746 | meaning of this r*,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    747 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    748 | 162
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    749 | 00:08:29,180 --> 00:08:34,055
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    750 | regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    751 | is the Kleene star of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    752 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    753 | 163
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    754 | 00:08:34,055 --> 00:08:37,130
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    755 | the language of r.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    756 | Remember that's
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    757 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    758 | 164
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    759 | 00:08:37,130 --> 00:08:41,525
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    760 | the union of all powers
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    761 | greater or equal than 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    762 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    763 | 165
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    764 | 00:08:41,525 --> 00:08:43,640
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    765 | It's behind.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    766 | I hope you don't get
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    767 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    768 | 166
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    769 | 00:08:43,640 --> 00:08:45,800
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    770 | confused by the use of the stars.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    771 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    772 | 167
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    773 | 00:08:45,800 --> 00:08:48,845
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    774 | This star is for
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    775 | the regular expressions.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    776 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    777 | 168
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    778 | 00:08:48,845 --> 00:08:52,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    779 | That star is for languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    780 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    781 | 169
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    782 | 00:08:52,205 --> 00:08:54,274
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    783 | They are two
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    784 | different operations.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    785 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    786 | 170
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    787 | 00:08:54,274 --> 00:08:56,555
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    788 | They don't even
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    789 | have the same type.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    790 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    791 | 171
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    792 | 00:08:56,555 --> 00:08:58,954
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    793 | Here might be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    794 | something interesting.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    795 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    796 | 172
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    797 | 00:08:58,954 --> 00:09:00,560
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    798 | Remember I asked you to think
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    799 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    800 | 173
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    801 | 00:09:00,560 --> 00:09:03,035
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    802 | about these two corner cases.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    803 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    804 | 174
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    805 | 00:09:03,035 --> 00:09:04,730
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    806 | I hope you have done so,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    807 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    808 | 175
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    809 | 00:09:04,730 --> 00:09:07,070
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    810 | but let's also have look
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    811 | at this together.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    812 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    813 | 176
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    814 | 00:09:07,070 --> 00:09:09,785
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    815 | According to the definition
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    816 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    817 | 177
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    818 | 00:09:09,785 --> 00:09:11,930
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    819 | for this append of languages,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    820 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    821 | 178
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    822 | 00:09:11,930 --> 00:09:13,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    823 | I have to take every string in
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    824 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    825 | 179
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    826 | 00:09:13,670 --> 00:09:16,130
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    827 | this set and have
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    828 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    829 | 180
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    830 | 00:09:16,130 --> 00:09:18,695
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    831 | two concatenated with
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    832 | every string in that set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    833 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    834 | 181
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    835 | 00:09:18,695 --> 00:09:22,115
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    836 | So this set contains only
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    837 | the empty string as element.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    838 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    839 | 182
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    840 | 00:09:22,115 --> 00:09:24,820
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    841 | So if I concatenate anything in
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    842 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    843 | 183
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    844 | 00:09:24,820 --> 00:09:27,745
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    845 | there with the empty string,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    846 | that will be left untouched.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    847 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    848 | 184
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    849 | 00:09:27,745 --> 00:09:31,855
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    850 | So this one will be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    851 | actually A.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    852 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    853 | 185
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    854 | 00:09:31,855 --> 00:09:34,600
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    855 | This one I have to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    856 | take every string in
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    857 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    858 | 186
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    859 | 00:09:34,600 --> 00:09:36,190
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    860 | this language and I have to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    861 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    862 | 187
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    863 | 00:09:36,190 --> 00:09:39,115
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    864 | concatenate with every
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    865 | string in that language.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    866 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    867 | 188
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    868 | 00:09:39,115 --> 00:09:41,110
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    869 | But here isn't any string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    870 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    871 | 189
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    872 | 00:09:41,110 --> 00:09:43,300
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    873 | So I can't concatenate that.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    874 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    875 | 190
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    876 | 00:09:43,300 --> 00:09:46,900
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    877 | That will be actually
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    878 | the empty set (not empty string).
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    879 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    880 | 191
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    881 | 00:09:46,900 --> 00:09:49,570
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    882 | So now let's have
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    883 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    884 | 192
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    885 | 00:09:49,570 --> 00:09:51,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    886 | a look at regular expressions.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    887 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    888 | 193
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    889 | 00:09:51,670 --> 00:09:53,230
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    890 | That was with languages.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    891 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    892 | 194
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    893 | 00:09:53,230 --> 00:09:56,035
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    894 | But let's have a look at
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    895 | regular expressions now.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    896 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    897 | 195
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    898 | 00:09:56,035 --> 00:09:58,660
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    899 | What would be the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    900 | meaning, for example,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    901 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    902 | 196
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    903 | 00:09:58,660 --> 00:10:01,945
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    904 | of r followed by 1?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    905 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    906 | 197
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    907 | 00:10:01,945 --> 00:10:04,149
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    908 | That is a regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    909 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    910 | 198
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    911 | 00:10:04,149 --> 00:10:06,255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    912 | And it essentially says:
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    913 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    914 | 199
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    915 | 00:10:06,255 --> 00:10:07,850
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    916 | this regular expression matches
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    917 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    918 | 200
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    919 | 00:10:07,850 --> 00:10:10,685
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    920 | some strings and this matches
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    921 | the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    922 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    923 | 201
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    924 | 00:10:10,685 --> 00:10:13,730
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    925 | So if you find out
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    926 | what the meaning is,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    927 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    928 | 202
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    929 | 00:10:13,730 --> 00:10:16,955
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    930 | we would apply this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    931 | L-function to it.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    932 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    933 | 203
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    934 | 00:10:16,955 --> 00:10:19,430
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    935 | And if we now look
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    936 | up the definition,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    937 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    938 | 204
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    939 | 00:10:19,430 --> 00:10:27,360
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    940 | that would be L of r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    941 | appended L of 1.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    942 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    943 | 205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    944 | 00:10:27,850 --> 00:10:32,255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    945 | If you look up what
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    946 | this is defined,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    947 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    948 | 206
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    949 | 00:10:32,255 --> 00:10:41,640
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    950 | then this would be L of r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    951 | appended with this language.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    952 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    953 | 207
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    954 | 00:10:41,950 --> 00:10:46,325
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    955 | And if you now look up
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    956 | our definition earlier,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    957 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    958 | 208
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    959 | 00:10:46,325 --> 00:10:50,455
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    960 | that will be just L of r.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    961 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    962 | 209
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    963 | 00:10:50,455 --> 00:10:52,690
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    964 | What that essentially
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    965 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    966 | 210
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    967 | 00:10:52,690 --> 00:10:55,765
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    968 | means is if you have
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    969 | this regular expression,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    970 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    971 | 211
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    972 | 00:10:55,765 --> 00:10:58,885
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    973 | this will match
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    974 | exactly those strings
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    975 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    976 | 212
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    977 | 00:10:58,885 --> 00:11:01,000
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    978 | which this regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    979 | expression can match.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    980 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    981 | 213
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    982 | 00:11:01,000 --> 00:11:04,794
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    983 | And that pretty much
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    984 | coincides with our intuition.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    985 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    986 | 214
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    987 | 00:11:04,794 --> 00:11:05,950
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    988 | This is supposed to match
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    989 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    990 | 215
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    991 | 00:11:05,950 --> 00:11:08,410
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    992 | the empty string at
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    993 | the end of the string,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    994 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    995 | 216
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    996 | 00:11:08,410 --> 00:11:11,005
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    997 | so it doesn't really
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    998 | make any difference.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |    999 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1000 | 217
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1001 | 00:11:11,005 --> 00:11:13,480
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1002 | And the meaning
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1003 | really tells us that.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1004 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1005 | 218
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1006 | 00:11:13,480 --> 00:11:15,880
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1007 | But here's the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1008 | interesting thing.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1009 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1010 | 219
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1011 | 00:11:15,880 --> 00:11:17,979
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1012 | When you were in school,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1013 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1014 | 220
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1015 | 00:11:17,979 --> 00:11:23,124
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1016 | how would you think
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1017 | about this expression?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1018 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1019 | 221
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1020 | 00:11:23,124 --> 00:11:29,515
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1021 | Well, r times 1
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1022 | equals just our, okay?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1023 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1024 | 222
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1025 | 00:11:29,515 --> 00:11:33,634
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1026 | Furthermore, if you had r times 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1027 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1028 | 223
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1029 | 00:11:33,634 --> 00:11:35,045
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1030 | What would that be equal?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1031 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1032 | 224
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1033 | 00:11:35,045 --> 00:11:37,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1034 | Well, it would be 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1035 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1036 | 225
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1037 | 00:11:37,205 --> 00:11:39,650
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1038 | Ok, let's have
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1039 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1040 | 226
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1041 | 00:11:39,650 --> 00:11:42,605
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1042 | a look how that works out
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1043 | with regular expressions.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1044 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1045 | 227
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1046 | 00:11:42,605 --> 00:11:46,355
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1047 | So if you take r followed by 0,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1048 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1049 | 228
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1050 | 00:11:46,355 --> 00:11:48,260
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1051 | remember this is
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1052 | the regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1053 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1054 | 229
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1055 | 00:11:48,260 --> 00:11:49,895
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1056 | that cannot match anything.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1057 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1058 | 230
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1059 | 00:11:49,895 --> 00:11:52,415
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1060 | By unfolding the definition,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1061 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1062 | 231
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1063 | 00:11:52,415 --> 00:11:59,104
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1064 | I would get L of r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1065 | appended with L of 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1066 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1067 | 232
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1068 | 00:11:59,104 --> 00:12:01,775
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1069 | This is of course defined as L of r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1070 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1071 | 233
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1072 | 00:12:01,775 --> 00:12:05,915
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1073 | appended with the empty set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1074 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1075 | 234
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1076 | 00:12:05,915 --> 00:12:10,760
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1077 | And this would, according
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1078 | to the definition earlier,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1079 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1080 | 235
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1081 | 00:12:10,760 --> 00:12:13,830
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1082 | well just the empty set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1083 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1084 | 236
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1085 | 00:12:14,160 --> 00:12:20,260
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1086 | And this would be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1087 | of course L of 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1088 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1089 | 237
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1090 | 00:12:20,260 --> 00:12:24,580
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1091 | So it seems like these laws,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1092 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1093 | 238
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1094 | 00:12:24,580 --> 00:12:27,175
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1095 | at least for the times,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1096 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1097 | 239
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1098 | 00:12:27,175 --> 00:12:29,785
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1099 | seem to be valid from math,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1100 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1101 | 240
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1102 | 00:12:29,785 --> 00:12:31,420
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1103 | are also valid with regular expressions,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1104 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1105 | 241
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1106 | 00:12:31,420 --> 00:12:33,370
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1107 | if we look at their meaning.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1108 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1109 | 242
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1110 | 00:12:33,370 --> 00:12:36,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1111 | These laws on natural numbers
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1112 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1113 | 243
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1114 | 00:12:36,670 --> 00:12:40,105
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1115 | and regular expressions and
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1116 | their close correspondance
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1117 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1118 | 244
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1119 | 00:12:40,105 --> 00:12:42,460
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1120 | probably explain why I use 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1121 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1122 | 245
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1123 | 00:12:42,460 --> 00:12:46,975
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1124 | a times for the sequence
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1125 | regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1126 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1127 | 246
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1128 | 00:12:46,975 --> 00:12:51,040
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1129 | So r followed by the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1130 | regular expression 1,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1131 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1132 | 247
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1133 | 00:12:51,040 --> 00:12:54,505
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1134 | will have the same meaning
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1135 | as that regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1136 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1137 | 248
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1138 | 00:12:54,505 --> 00:12:59,120
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1139 | And r followed by the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1140 | 0 regular expression
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1141 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1142 | 249
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1143 | 00:12:59,120 --> 00:13:01,295
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1144 | will have this meaning.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1145 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1146 | 250
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1147 | 00:13:01,295 --> 00:13:03,590
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1148 | You might now think, but I also
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1149 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1150 | 251
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1151 | 00:13:03,590 --> 00:13:06,605
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1152 | wrote the alternative with a plus.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1153 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1154 | 252
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1155 | 00:13:06,605 --> 00:13:10,370
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1156 | Does a similar law
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1157 | holds for plus?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1158 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1159 | 253
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1160 | 00:13:10,370 --> 00:13:15,965
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1161 | Of course, if I take r
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1162 | plus 0 on natural numbers,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1163 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1164 | 254
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1165 | 00:13:15,965 --> 00:13:20,060
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1166 | that would be just r. Does
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1167 | hold for regular expressions?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1168 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1169 | 255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1170 | 00:13:20,060 --> 00:13:22,085
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1171 | Yes, indeed it holds.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1172 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1173 | 256
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1174 | 00:13:22,085 --> 00:13:26,735
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1175 | If I have this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1176 | regular expression and
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1177 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1178 | 257
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1179 | 00:13:26,735 --> 00:13:33,245
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1180 | unfold the definition that
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1181 | would be L(r) union L(0).
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1182 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1183 | 258
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1184 | 00:13:33,245 --> 00:13:38,060
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1185 | This would be equal
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1186 | to L(r) union...
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1187 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1188 | 259
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1189 | 00:13:38,060 --> 00:13:41,150
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1190 | What is this? Well, that's
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1191 | just the empty set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1192 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1193 | 260
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1194 | 00:13:41,150 --> 00:13:43,760
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1195 | And if I union something
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1196 | with the empty set,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1197 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1198 | 261
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1199 | 00:13:43,760 --> 00:13:47,180
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1200 | then this will be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1201 | just of L(r). So yes,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1202 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1203 | 262
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1204 | 00:13:47,180 --> 00:13:50,120
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1205 | indeed, plus is also very much
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1206 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1207 | 263
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1208 | 00:13:50,120 --> 00:13:54,184
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1209 | inspired by the laws
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1210 | on natural numbers.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1211 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1212 | 264
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1213 | 00:13:54,184 --> 00:13:57,065
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1214 | There exists other notations too,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1215 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1216 | 265
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1217 | 00:13:57,065 --> 00:14:01,310
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1218 | but I prefer this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1219 | using the plus for
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1220 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1221 | 266
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1222 | 00:14:01,310 --> 00:14:03,844
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1223 | the alternatives and the times
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1224 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1225 | 267
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1226 | 00:14:03,844 --> 00:14:05,765
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1227 | for the sequence expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1228 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1229 | 268
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1230 | 00:14:05,765 --> 00:14:07,460
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1231 | It's also the reason why I call
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1232 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1233 | 269
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1234 | 00:14:07,460 --> 00:14:10,325
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1235 | this regular expression for
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1236 | the empty string 1.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1237 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1238 | 270
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1239 | 00:14:10,325 --> 00:14:14,915
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1240 | And for matching
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1241 | nothing at all 0.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1242 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1243 | 271
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1244 | 00:14:14,915 --> 00:14:18,665
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1245 | This correspondence to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1246 | natural numbers doesn't quite
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1247 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1248 | 272
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1249 | 00:14:18,665 --> 00:14:22,055
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1250 | extend to the star
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1251 | regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1252 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1253 | 273
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1254 | 00:14:22,055 --> 00:14:25,055
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1255 | But there's still a
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1256 | connection. There too.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1257 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1258 | 274
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1259 | 00:14:25,055 --> 00:14:26,510
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1260 | Can you remember how
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1261 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1262 | 275
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1263 | 00:14:26,510 --> 00:14:29,345
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1264 | the power operation on
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1265 | languages was defined?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1266 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1267 | 276
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1268 | 00:14:29,345 --> 00:14:31,370
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1269 | The 0 case was defined
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1270 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1271 | 277
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1272 | 00:14:31,370 --> 00:14:34,520
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1273 | as the set containing
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1274 | the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1275 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1276 | 278
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1277 | 00:14:34,520 --> 00:14:37,039
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1278 | Why is that? It looks
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1279 | a bit arbitrary.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1280 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1281 | 279
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1282 | 00:14:37,039 --> 00:14:41,150
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1283 | Why is it not the empty set
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1284 | or why is it not defined as A?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1285 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1286 | 280
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1287 | 00:14:41,150 --> 00:14:43,745
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1288 | Why is defined in this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1289 | particular way?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1290 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1291 | 281
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1292 | 00:14:43,745 --> 00:14:46,880
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1293 | Well, can you remember how
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1294 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1295 | 282
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1296 | 00:14:46,880 --> 00:14:48,950
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1297 | the power operation r to the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1298 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1299 | 283
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1300 | 00:14:48,950 --> 00:14:51,440
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1301 | 0 is defined on natural numbers?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1302 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1303 | 284
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1304 | 00:14:51,440 --> 00:14:53,930
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1305 | Yes, that's defined as 1.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1306 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1307 | 285
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1308 | 00:14:53,930 --> 00:14:57,125
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1309 | Does that also apply to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1310 | regular expressions?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1311 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1312 | 286
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1313 | 00:14:57,125 --> 00:15:00,725
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1314 | Well, if we take the meaning
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1315 | of a regular expression,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1316 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1317 | 287
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1318 | 00:15:00,725 --> 00:15:04,730
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1319 | let's say r, and raise
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1320 | it to the 0th power,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1321 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1322 | 288
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1323 | 00:15:04,730 --> 00:15:07,685
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1324 | then this will be, of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1325 | course, by definition,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1326 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1327 | 289
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1328 | 00:15:07,685 --> 00:15:12,245
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1329 | be defined as the set 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1330 | containing the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1331 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1332 | 290
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1333 | 00:15:12,245 --> 00:15:17,160
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1334 | And that is of course
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1335 | equal to L(1).
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1336 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1337 | 291
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1338 | 00:15:17,830 --> 00:15:20,570
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1339 | Again, you can see that
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1340 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1341 | 292
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1342 | 00:15:20,570 --> 00:15:23,300
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1343 | this law on natural numbers also
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1344 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1345 | 293
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1346 | 00:15:23,300 --> 00:15:29,000
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1347 | holds on the laws of regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1348 | expressions - on heir meaning.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1349 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1350 | 294
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1351 | 00:15:29,000 --> 00:15:32,810
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1352 | What I find really beautiful
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1353 | here is that of course,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1354 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1355 | 295
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1356 | 00:15:32,810 --> 00:15:36,244
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1357 | the meaning is defined on
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1358 | sets, sets of strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1359 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1360 | 296
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1361 | 00:15:36,244 --> 00:15:38,975
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1362 | This of course, on natural numbers.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1363 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1364 | 297
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1365 | 00:15:38,975 --> 00:15:41,060
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1366 | You can probably
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1367 | see now where I'm
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1368 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1369 | 298
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1370 | 00:15:41,060 --> 00:15:43,085
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1371 | coming from with my notation.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1372 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1373 | 299
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1374 | 00:15:43,085 --> 00:15:46,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1375 | That is actually a slight
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1376 | problem in this field,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1377 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1378 | 300
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1379 | 00:15:46,205 --> 00:15:48,590
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1380 | since it's so old.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1381 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1382 | 301
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1383 | 00:15:48,590 --> 00:15:52,205
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1384 | Pretty much everybody
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1385 | introduced their own notation.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1386 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1387 | 302
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1388 | 00:15:52,205 --> 00:15:53,870
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1389 | And you now have heaps of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1390 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1391 | 303
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1392 | 00:15:53,870 --> 00:15:55,550
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1393 | different notations
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1394 | for the same thing.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1395 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1396 | 304
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1397 | 00:15:55,550 --> 00:15:57,379
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1398 | Okay, that is slightly
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1399 | exaggerating.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1400 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1401 | 305
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1402 | 00:15:57,379 --> 00:16:00,830
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1403 | And also the notation
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1404 | I used for times and
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1405 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1406 | 306
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1407 | 00:16:00,830 --> 00:16:04,295
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1408 | plus and 0 and 1s...definitely
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1409 | I'm not the only one.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1410 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1411 | 307
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1412 | 00:16:04,295 --> 00:16:05,435
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1413 | There are many people
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1414 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1415 | 308
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1416 | 00:16:05,435 --> 00:16:07,625
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1417 | who have used this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1418 | notation as well.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1419 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1420 | 309
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1421 | 00:16:07,625 --> 00:16:10,190
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1422 | It's just, it's not universal.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1423 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1424 | 310
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1425 | 00:16:10,190 --> 00:16:12,290
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1426 | Well, here's a question now.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1427 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1428 | 311
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1429 | 00:16:12,290 --> 00:16:15,635
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1430 | Why did we go through this
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1431 | kerfuffle in the first place?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1432 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1433 | 312
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1434 | 00:16:15,635 --> 00:16:19,370
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1435 | Why did we introduce these
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1436 | operations on languages?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1437 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1438 | 313
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1439 | 00:16:19,370 --> 00:16:21,260
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1440 | And why did we introduce
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1441 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1442 | 314
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1443 | 00:16:21,260 --> 00:16:23,255
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1444 | the meaning of a
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1445 | regular expression?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1446 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1447 | 315
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1448 | 00:16:23,255 --> 00:16:26,300
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1449 | Well, remember at the beginning,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1450 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1451 | 316
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1452 | 00:16:26,300 --> 00:16:28,265
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1453 | we wanted to specify
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1454 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1455 | 317
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1456 | 00:16:28,265 --> 00:16:31,880
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1457 | what problem our algorithms
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1458 | actually supposed to solve.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1459 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1460 | 318
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1461 | 00:16:31,880 --> 00:16:35,960
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1462 | And we want to make that
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1463 | very precise so that we can
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1464 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1465 | 319
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1466 | 00:16:35,960 --> 00:16:38,555
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1467 | be sure that our implementation
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1468 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1469 | 320
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1470 | 00:16:38,555 --> 00:16:40,295
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1471 | really solves the problem.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1472 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1473 | 321
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1474 | 00:16:40,295 --> 00:16:41,540
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1475 | And that's what you can do now.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1476 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1477 | 322
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1478 | 00:16:41,540 --> 00:16:45,605
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1479 | We can say a regular
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1480 | expression, r say,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1481 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1482 | 323
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1483 | 00:16:45,605 --> 00:16:50,015
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1484 | is matching a string
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1485 | s if and only if
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1486 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1487 | 324
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1488 | 00:16:50,015 --> 00:16:55,474
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1489 | the string s is in the language
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1490 | of the regular expression.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1491 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1492 | 325
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1493 | 00:16:55,474 --> 00:17:00,770
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1494 | So that is the problem our
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1495 | matcher is supposed to solve.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1496 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1497 | 326
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1498 | 00:17:00,770 --> 00:17:03,320
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1499 | And it's supposed to
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1500 | solve that a bit faster
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1501 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1502 | 327
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1503 | 00:17:03,320 --> 00:17:06,860
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1504 | than in Python, Ruby and Java.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1505 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1506 | 328
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1507 | 00:17:06,860 --> 00:17:09,585
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1508 | And unfortunately we cannot use
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1509 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1510 | 329
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1511 | 00:17:09,585 --> 00:17:12,260
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1512 | the definition of L
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1513 | directly for that.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1514 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1515 | 330
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1516 | 00:17:12,260 --> 00:17:15,815
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1517 | Because remember, in
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1518 | the case of the star,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1519 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1520 | 331
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1521 | 00:17:15,815 --> 00:17:17,690
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1522 | sometimes the meaning of
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1523 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1524 | 332
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1525 | 00:17:17,690 --> 00:17:18,830
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1526 | a regular expression is actually
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1527 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1528 | 333
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1529 | 00:17:18,830 --> 00:17:20,925
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1530 | an infinite set of strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1531 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1532 | 334
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1533 | 00:17:20,925 --> 00:17:23,575
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1534 | And it's a tiny bit difficult
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1535 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1536 | 335
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1537 | 00:17:23,575 --> 00:17:27,040
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1538 | to decide whether a string
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1539 | is an infinite set.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1540 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1541 | 336
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1542 | 00:17:27,040 --> 00:17:30,790
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1543 | So we have to do something
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1544 | more clever in our algorithm.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1545 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1546 | 337
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1547 | 00:17:30,790 --> 00:17:33,535
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1548 | But that's for next week.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1549 | So see you next week. Bye.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1550 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1551 | 338
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1552 | 00:17:38,535 --> 00:17:41,680
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1553 | Okay, just to troll you.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1554 | Here's one more slide.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1555 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1556 | 339
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1557 | 00:17:41,680 --> 00:17:45,850
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1558 | So when you go over the
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1559 | handouts and the videos,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1560 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1561 | 340
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1562 | 00:17:45,850 --> 00:17:47,875
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1563 | think about this example.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1564 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1565 | 341
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1566 | 00:17:47,875 --> 00:17:49,840
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1567 | Imagine you have a language A,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1568 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1569 | 342
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1570 | 00:17:49,840 --> 00:17:51,970
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1571 | which contains four strings.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1572 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1573 | 343
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1574 | 00:17:51,970 --> 00:17:53,725
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1575 | First string is just the character a,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1576 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1577 | 344
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1578 | 00:17:53,725 --> 00:17:57,445
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1579 | second string is just
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1580 | the character b, and so on.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1581 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1582 | 345
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1583 | 00:17:57,445 --> 00:18:02,335
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1584 | How many strings are there
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1585 | in A to the power four.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1586 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1587 | 346
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1588 | 00:18:02,335 --> 00:18:05,210
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1589 | Okay, that should be
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1590 | relatively simple.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1591 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1592 | 347
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1593 | 00:18:05,210 --> 00:18:07,310
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1594 | If not, just try it out by
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1595 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1596 | 348
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1597 | 00:18:07,310 --> 00:18:11,165
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1598 | implementing it in Scala and see
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1599 | how many strings there are.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1600 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1601 | 349
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1602 | 00:18:11,165 --> 00:18:13,850
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1603 | But now the more
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1604 | interesting question,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1605 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1606 | 350
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1607 | 00:18:13,850 --> 00:18:16,670
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1608 | imagine the same language,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1609 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1610 | 351
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1611 | 00:18:16,670 --> 00:18:19,400
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1612 | except that instead
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1613 | of the character d,
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1614 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1615 | 352
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1616 | 00:18:19,400 --> 00:18:22,250
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1617 | we have here, the empty string.
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1618 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1619 | 353
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1620 | 00:18:22,250 --> 00:18:26,630
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1621 | How many strings are in
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1622 | A to the power four?
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1623 | 
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1624 | 354
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1625 | 00:18:26,630 --> 00:18:31,320
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1626 | Okay, I'll let you think
 | 
| 
Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset |   1627 | about this. Bye now.
 |