382 |
382 |
383 |
383 |
384 text_raw {* |
384 text_raw {* |
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
386 \mode<presentation>{ |
386 \mode<presentation>{ |
|
387 \begin{frame}<1->[c] |
|
388 \frametitle{Lesson Learned} |
|
389 |
|
390 \begin{textblock}{11.5}(1.2,5) |
|
391 \begin{minipage}{10.5cm} |
|
392 \begin{block}{} |
|
393 Theorem provers can keep large proofs and definitions consistent and |
|
394 make them modifiable. |
|
395 \end{block} |
|
396 \end{minipage} |
|
397 \end{textblock} |
|
398 |
|
399 |
|
400 \end{frame}} |
|
401 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
402 *} |
|
403 |
|
404 text_raw {* |
|
405 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
406 \mode<presentation>{ |
|
407 \begin{frame} |
|
408 \frametitle{} |
|
409 |
|
410 \begin{textblock}{11.5}(0.8,2.3) |
|
411 \begin{minipage}{11.2cm} |
|
412 In most papers/books: |
|
413 \begin{block}{} |
|
414 \color{darkgray} |
|
415 ``\ldots this necessary hygienic discipline is somewhat swept under the carpet via |
|
416 the so-called `{\bf variable convention}' \ldots |
|
417 The {\color{black}{\bf belief}} that this is {\bf sound} came from the calculus |
|
418 with nameless binders in de Bruijn'' |
|
419 \end{block}\medskip |
|
420 \end{minipage} |
|
421 \end{textblock} |
|
422 |
|
423 \begin{textblock}{11.5}(0.8,10) |
|
424 \includegraphics[scale=0.25]{LambdaBook.jpg}\hspace{-3mm}\includegraphics[scale=0.3]{barendregt.jpg} |
|
425 \end{textblock} |
|
426 \end{frame}} |
|
427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
428 *} |
|
429 |
|
430 |
|
431 text_raw {* |
|
432 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
433 \mode<presentation>{ |
387 \begin{frame}<1->[t] |
434 \begin{frame}<1->[t] |
388 \frametitle{Regular Expressions} |
435 \frametitle{Regular Expressions} |
389 |
436 |
390 \begin{textblock}{6}(2,4) |
437 \begin{textblock}{6}(2,4) |
391 \begin{tabular}{@ {}rrl} |
438 \begin{tabular}{@ {}rrl} |
1212 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1213 *} |
1258 *} |
1214 |
1259 |
1215 |
1260 |
1216 |
1261 |
1217 text_raw {* |
1262 |
1218 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1263 text_raw {* |
1219 \mode<presentation>{ |
1264 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1220 \begin{frame}[c] |
1265 \mode<presentation>{ |
1221 \frametitle{\LARGE The Other Direction} |
1266 \begin{frame}[c] |
1222 |
1267 \frametitle{\LARGE Other Direction} |
|
1268 |
1223 One has to prove |
1269 One has to prove |
1224 |
1270 |
1225 \begin{center} |
1271 \begin{center} |
1226 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
1272 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} |
1227 \end{center} |
1273 \end{center} |
1228 |
1274 |
1229 by induction on \smath{r}. This is straightforward for \\the base cases:\small |
1275 by induction on \smath{r}. Not trivial, but after a bit |
1230 |
1276 of thinking, one can prove that if |
1231 \begin{center} |
1277 |
1232 \begin{tabular}{l@ {\hspace{1mm}}l} |
1278 \begin{center} |
1233 \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\ |
1279 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm} |
1234 \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\ |
|
1235 \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}} |
|
1236 \end{tabular} |
|
1237 \end{center} |
|
1238 |
|
1239 |
|
1240 \end{frame}} |
|
1241 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1242 *} |
|
1243 |
|
1244 |
|
1245 text_raw {* |
|
1246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1247 \mode<presentation>{ |
|
1248 \begin{frame}[t] |
|
1249 \frametitle{\LARGE The Other Direction} |
|
1250 |
|
1251 More complicated are the inductive cases:\\ one needs to prove that if |
|
1252 |
|
1253 \begin{center} |
|
1254 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm} |
|
1255 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})} |
1280 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})} |
1256 \end{center} |
1281 \end{center} |
1257 |
1282 |
1258 then |
1283 then |
1259 |
1284 |
1260 \begin{center} |
1285 \begin{center} |
1261 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})} |
1286 \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})} |
1262 \end{center} |
1287 \end{center} |
1263 |
1288 |
1264 \end{frame}} |
1289 |
1265 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1290 |
1266 *} |
1291 \end{frame}} |
1267 |
1292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1268 |
1293 *} |
1269 text_raw {* |
1294 |
1270 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1271 \mode<presentation>{ |
|
1272 \begin{frame}[t] |
|
1273 \frametitle{\LARGE Helper Lemma} |
|
1274 |
|
1275 \begin{center} |
|
1276 \begin{tabular}{p{10cm}} |
|
1277 %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective |
|
1278 %(on \smath{A}),\\ then \smath{\text{finite}\,A}. |
|
1279 Given two equivalence relations \smath{R_1} and \smath{R_2} with |
|
1280 \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ |
|
1281 Then\medskip\\ |
|
1282 \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)} |
|
1283 \end{tabular} |
|
1284 \end{center} |
|
1285 |
|
1286 \end{frame}} |
|
1287 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1288 *} |
|
1289 |
|
1290 text_raw {* |
|
1291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1292 \mode<presentation>{ |
|
1293 \begin{frame}[c] |
|
1294 \frametitle{\Large Derivatives and Left-Quotients} |
|
1295 \small |
|
1296 Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip |
|
1297 |
|
1298 |
|
1299 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
1300 \multicolumn{4}{@ {}l}{Left-Quotient:}\\ |
|
1301 \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\ |
|
1302 |
|
1303 \multicolumn{4}{@ {}l}{Derivative:}\\ |
|
1304 \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\ |
|
1305 \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\ |
|
1306 \bl{der c (d)} & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\ |
|
1307 \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ |
|
1308 \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\ |
|
1309 & & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ |
|
1310 \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\ |
|
1311 |
|
1312 \bl{ders [] r} & \bl{$=$} & \bl{r} & \\ |
|
1313 \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\ |
|
1314 \end{tabular}\pause |
|
1315 |
|
1316 \begin{center} |
|
1317 \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})} |
|
1318 \end{center} |
|
1319 |
|
1320 \end{frame}} |
|
1321 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1322 *} |
|
1323 |
|
1324 text_raw {* |
|
1325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1326 \mode<presentation>{ |
|
1327 \begin{frame}[c] |
|
1328 \frametitle{\LARGE Left-Quotients and MN-Rels} |
|
1329 |
|
1330 \begin{itemize} |
|
1331 \item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip |
|
1332 \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$} |
|
1333 \end{itemize}\bigskip |
|
1334 |
|
1335 \begin{center} |
|
1336 \smath{x \approx_A y \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A} |
|
1337 \end{center}\bigskip\pause\small |
|
1338 |
|
1339 which means |
|
1340 |
|
1341 \begin{center} |
|
1342 \smath{x \approx_{\mathbb{L}(r)} y \Longleftrightarrow |
|
1343 \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)} |
|
1344 \end{center}\pause |
|
1345 |
|
1346 \hspace{8.8mm}or |
|
1347 \smath{\;x \approx_{\mathbb{L}(r)} y \Longleftarrow |
|
1348 \text{ders}\;x\;r = \text{ders}\;y\;r} |
|
1349 |
|
1350 |
|
1351 |
|
1352 \end{frame}} |
|
1353 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1354 *} |
|
1355 |
|
1356 text_raw {* |
|
1357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1358 \mode<presentation>{ |
|
1359 \begin{frame}[c] |
|
1360 \frametitle{\LARGE Partial Derivatives} |
|
1361 |
|
1362 Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip |
|
1363 |
|
1364 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
1365 \bl{pder c ($\varnothing$)} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\ |
|
1366 \bl{pder c ([])} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\ |
|
1367 \bl{pder c (d)} & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\ |
|
1368 \bl{pder c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\ |
|
1369 \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\ |
|
1370 & & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\ |
|
1371 \bl{pder c (r$^*$)} & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\ |
|
1372 \end{tabular} |
|
1373 |
|
1374 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
|
1375 \bl{pders [] r} & \bl{$=$} & \bl{r} & \\ |
|
1376 \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\ |
|
1377 \end{tabular}\pause |
|
1378 |
|
1379 \begin{center} |
|
1380 \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))} |
|
1381 \end{center} |
|
1382 |
|
1383 \end{frame}} |
|
1384 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1385 *} |
|
1386 |
|
1387 text_raw {* |
|
1388 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1389 \mode<presentation>{ |
|
1390 \begin{frame}[t] |
|
1391 \frametitle{\LARGE Final Result} |
|
1392 |
|
1393 \mbox{}\\[7mm] |
|
1394 |
|
1395 \begin{itemize} |
|
1396 \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}} |
|
1397 {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} |
|
1398 refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause |
|
1399 \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause |
|
1400 \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed. |
|
1401 \end{itemize} |
|
1402 |
|
1403 \end{frame}} |
|
1404 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1405 *} |
|
1406 |
1295 |
1407 |
1296 |
1408 text_raw {* |
1297 text_raw {* |
1409 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1298 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1410 \mode<presentation>{ |
1299 \mode<presentation>{ |