|
1 \documentclass[dvipsnames,14pt,t]{beamer} |
|
2 \usepackage{../slides} |
|
3 \usepackage{../langs} |
|
4 \usepackage{../data} |
|
5 \usepackage{../graphics} |
|
6 \usepackage{soul} |
|
7 |
|
8 |
|
9 % beamer stuff |
|
10 \renewcommand{\slidecaption}{AFL, King's College London} |
|
11 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
12 |
|
13 |
|
14 \begin{document} |
|
15 |
|
16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
17 \begin{frame}[t] |
|
18 \frametitle{% |
|
19 \begin{tabular}{@ {}c@ {}} |
|
20 \\[-3mm] |
|
21 \LARGE Automata and \\[-2mm] |
|
22 \LARGE Formal Languages\\[3mm] |
|
23 \end{tabular}} |
|
24 |
|
25 \normalsize |
|
26 \begin{center} |
|
27 \begin{tabular}{ll} |
|
28 Email: & christian.urban at kcl.ac.uk\\ |
|
29 Office: & S1.27 (1st floor Strand Building)\\ |
|
30 Slides: & KEATS (also home work is there)\\ |
|
31 \end{tabular} |
|
32 \end{center} |
|
33 |
|
34 \end{frame} |
|
35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
36 |
|
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
38 \begin{frame}[t] |
|
39 \frametitle{2nd CW} |
|
40 |
|
41 Remember we showed that\\ |
|
42 |
|
43 \begin{center} |
|
44 \bl{$der\;c\;(r^+) = (der\;c\;r)\cdot r^*$} |
|
45 \end{center}\bigskip\pause |
|
46 |
|
47 |
|
48 Does the same hold for \bl{$r^{\{n\}}$} with \bl{$n > 0$} |
|
49 |
|
50 \begin{center} |
|
51 \bl{$der\;c\;(r^{\{n\}}) = (der\;c\;r)\cdot r^{\{n-1\}}$} ? |
|
52 \end{center} |
|
53 \end{frame} |
|
54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
55 |
|
56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
57 \begin{frame}[t] |
|
58 \frametitle{2nd CW} |
|
59 |
|
60 \begin{itemize} |
|
61 \item \bl{$der$} |
|
62 |
|
63 \begin{center} |
|
64 \bl{$der\;c\;(r^{\{n\}}) \dn |
|
65 \begin{cases} |
|
66 \varnothing & \text{\textcolor{black}{if}}\; n = 0\\ |
|
67 der\;c\;(r\cdot r^{\{n-1\}}) & \text{\textcolor{black}{o'wise}} |
|
68 \end{cases}$} |
|
69 \end{center} |
|
70 |
|
71 \item \bl{$mkeps$} |
|
72 |
|
73 \begin{center} |
|
74 \bl{$mkeps(r^{\{n\}}) \dn |
|
75 [\underbrace{mkeps(r),\ldots,mkeps(r)}_{n\;times}]$} ? |
|
76 \end{center} |
|
77 |
|
78 \item \bl{$inj$} |
|
79 |
|
80 \begin{center} |
|
81 \begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l} |
|
82 \bl{$inj\;r^{\{n\}}\;c\;(v_1, [vs])$} & \bl{$\dn$} & |
|
83 \bl{$[inj\;r\;c\;v_1::vs]$}\\ |
|
84 \bl{$inj\;r^{\{n\}}\;c\;Left(v_1, [vs])$} & \bl{$\dn$} & |
|
85 \bl{$[inj\;r\;c\;v_1::vs]$}\\ |
|
86 \bl{$inj\;r^{\{n\}}\;c\;Right([v::vs])$} & \bl{$\dn$} & |
|
87 \bl{$[mkeps(r)::inj\;r\;c\;v::vs]$}\\ |
|
88 \end{tabular} |
|
89 \end{center} |
|
90 |
|
91 \end{itemize} |
|
92 |
|
93 \end{frame} |
|
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
95 |
|
96 |
|
97 |
|
98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
99 \begin{frame}[c] |
|
100 \frametitle{Compilers in Boeings 777} |
|
101 |
|
102 They want to achieve triple redundancy in hardware |
|
103 faults.\bigskip |
|
104 |
|
105 They compile 1 Ada program to |
|
106 |
|
107 \begin{itemize} |
|
108 \item Intel 80486 |
|
109 \item Motorola 68040 (old Macintosh's) |
|
110 \item AMD 29050 (RISC chips used often in laser printers) |
|
111 \end{itemize} |
|
112 |
|
113 \end{frame} |
|
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
115 |
|
116 |
|
117 |
|
118 |
|
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
120 \begin{frame}[t] |
|
121 \frametitle{Proofs about Rexps} |
|
122 |
|
123 Remember their inductive definition: |
|
124 |
|
125 \begin{center} |
|
126 \begin{tabular}{@ {}rrl} |
|
127 \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\ |
|
128 & \bl{$\mid$} & \bl{$\epsilon$} \\ |
|
129 & \bl{$\mid$} & \bl{$c$} \\ |
|
130 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\ |
|
131 & \bl{$\mid$} & \bl{$r_1 + r_2$} \\ |
|
132 & \bl{$\mid$} & \bl{$r^*$} \\ |
|
133 \end{tabular} |
|
134 \end{center} |
|
135 |
|
136 If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots |
|
137 |
|
138 \end{frame} |
|
139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
140 |
|
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
142 \begin{frame}[c] |
|
143 \frametitle{Proofs about Rexp (2)} |
|
144 |
|
145 \begin{itemize} |
|
146 \item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip |
|
147 \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already |
|
148 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
149 \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already |
|
150 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
151 \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already |
|
152 holds for \bl{$r$}. |
|
153 \end{itemize} |
|
154 |
|
155 \end{frame} |
|
156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
157 |
|
158 |
|
159 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
160 \begin{frame}[c] |
|
161 |
|
162 \bl{\begin{center} |
|
163 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
164 $zeroable(\varnothing)$ & $\dn$ & \textit{true}\\ |
|
165 $zeroable(\epsilon)$ & $\dn$ & \textit{false}\\ |
|
166 $zeroable (c)$ & $\dn$ & \textit{false}\\ |
|
167 $zeroable (r_1 + r_2)$ & $\dn$ & $zeroable(r_1) \wedge zeroable(r_2)$ \\ |
|
168 $zeroable (r_1 \cdot r_2)$ & $\dn$ & $zeroable(r_1) \vee zeroable(r_2)$ \\ |
|
169 $zeroable (r^*)$ & $\dn$ & \textit{false}\\ |
|
170 \end{tabular} |
|
171 \end{center}} |
|
172 |
|
173 \begin{center} |
|
174 \bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$} |
|
175 \end{center} |
|
176 |
|
177 \end{frame} |
|
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
179 |
|
180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
181 \begin{frame}[c] |
|
182 \frametitle{Correctness of the Matcher} |
|
183 |
|
184 \begin{itemize} |
|
185 \item We want to prove\medskip |
|
186 \begin{center} |
|
187 \bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$} |
|
188 \end{center}\bigskip |
|
189 |
|
190 where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$} |
|
191 \bigskip\pause |
|
192 |
|
193 \item We can do this, if we know\medskip |
|
194 \begin{center} |
|
195 \bl{$L(der\;c\;r) = Der\;c\;(L(r))$} |
|
196 \end{center} |
|
197 \end{itemize} |
|
198 \end{frame} |
|
199 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
200 |
|
201 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
202 \begin{frame}[c] |
|
203 \frametitle{Induction over Strings} |
|
204 |
|
205 \begin{itemize} |
|
206 \item case \bl{$[]$}:\bigskip |
|
207 |
|
208 We need to prove |
|
209 |
|
210 \begin{center} |
|
211 \bl{$\forall r.\;\;nullable(ders\;[]\;r) \;\Leftrightarrow\; [] \in L(r)$} |
|
212 \end{center}\bigskip |
|
213 |
|
214 \begin{center} |
|
215 \bl{$nullable(ders\;[]\;r) \;\dn\; nullable\;r \;\Leftrightarrow\ldots$} |
|
216 \end{center} |
|
217 \end{itemize} |
|
218 \end{frame} |
|
219 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
220 |
|
221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
222 \begin{frame}[c] |
|
223 \frametitle{Induction over Strings} |
|
224 |
|
225 \begin{itemize} |
|
226 \item case \bl{$c::s$}\bigskip |
|
227 |
|
228 We need to prove |
|
229 |
|
230 \begin{center} |
|
231 \bl{$\forall r.\;\;nullable(ders\;(c::s)\;r) \;\Leftrightarrow\; (c::s) \in L(r)$} |
|
232 \end{center} |
|
233 |
|
234 We have by IH |
|
235 |
|
236 \begin{center} |
|
237 \bl{$\forall r.\;\;nullable(ders\;s\;r) \;\Leftrightarrow\; s \in L(r)$} |
|
238 \end{center}\bigskip |
|
239 |
|
240 \begin{center} |
|
241 \bl{$ders\;(c::s)\;r \dn ders\;s\;(der\;c\;r)$} |
|
242 \end{center} |
|
243 \end{itemize} |
|
244 \end{frame} |
|
245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
246 |
|
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
248 \begin{frame}[c] |
|
249 \frametitle{Induction over Regexps} |
|
250 |
|
251 \begin{itemize} |
|
252 \item The proof hinges on the fact that we can prove\bigskip |
|
253 |
|
254 \begin{center} |
|
255 \Large\bl{$L(der\;c\;r) = Der\;c\;(L(r))$} |
|
256 \end{center} |
|
257 \end{itemize} |
|
258 |
|
259 \end{frame} |
|
260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
261 |
|
262 |
|
263 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
264 \begin{frame}[c] |
|
265 \frametitle{Some Lemmas} |
|
266 |
|
267 \begin{itemize} |
|
268 \item \bl{$Der\;c\;(A\cup B) = |
|
269 (Der\;c\;A)\cup(Der\;c\;B)$}\bigskip |
|
270 \item If \bl{$[] \in A$} then |
|
271 \begin{center} |
|
272 \bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$} |
|
273 \end{center}\bigskip |
|
274 \item If \bl{$[] \not\in A$} then |
|
275 \begin{center} |
|
276 \bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$} |
|
277 \end{center}\bigskip |
|
278 \item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\ |
|
279 \small\mbox{}\hfill (interesting case)\\ |
|
280 \end{itemize} |
|
281 |
|
282 \end{frame} |
|
283 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
284 |
|
285 |
|
286 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
287 \begin{frame}[c] |
|
288 \frametitle{Why?} |
|
289 |
|
290 Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold? |
|
291 \bigskip |
|
292 |
|
293 |
|
294 \begin{center} |
|
295 \begin{tabular}{lcl} |
|
296 \bl{$Der\;c\;(A^*)$} & \bl{$=$} & \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\ |
|
297 & \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\ |
|
298 & \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\ |
|
299 & \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\ |
|
300 \end{tabular} |
|
301 \end{center}\bigskip\bigskip |
|
302 |
|
303 \small |
|
304 using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\ |
|
305 \mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$} |
|
306 \end{frame} |
|
307 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
308 |
|
309 |
|
310 |
|
311 \end{document} |
|
312 |
|
313 %%% Local Variables: |
|
314 %%% mode: latex |
|
315 %%% TeX-master: t |
|
316 %%% End: |
|
317 |