slides/slides02.tex
changeset 1005 0ffb6e4de10a
parent 1002 9bb223540e34
equal deleted inserted replaced
1004:99e89ad35d76 1005:0ffb6e4de10a
    92 \small I try my best, but \ldots
    92 \small I try my best, but \ldots
    93 \end{tabular} 
    93 \end{tabular} 
    94 \end{center} 
    94 \end{center} 
    95 \mbox{}
    95 \mbox{}
    96 \end{frame}
    96 \end{frame}
       
    97 
       
    98 {
       
    99 \setbeamercolor{background canvas}{bg=cream}
       
   100 \begin{frame}<1-2>[c]
       
   101 \end{frame}
       
   102 }
       
   103 
       
   104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   105 \begin{frame}[t]
       
   106 
       
   107 \mbox{}\\[-20mm]\mbox{}
       
   108 
       
   109 \tt
       
   110 \begin{center}\large
       
   111 \code{"if x = 42 then x := x + 1 else x := x - 1"}
       
   112 \end{center}\small
       
   113 
       
   114 
       
   115 \begin{tabular}{@{}l}
       
   116 KEYWORD: \\
       
   117 \hspace{5mm}{if}, {then}, {else},\ldots\\ 
       
   118 WHITESPACE:\\
       
   119 \hspace{5mm}{" "}, {$\backslash$n}, {$\backslash$r}\\ 
       
   120 IDENTIFIER:\\
       
   121 \hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
       
   122 NUM:\\
       
   123 \hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
       
   124 NUMBER:\\
       
   125 \hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
       
   126 OP:\\
       
   127 \hspace{5mm}+, -, *, \%, <, =<,\ldots\\
       
   128 COMMENTS:\\
       
   129 \hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
       
   130 \end{tabular}
       
   131 
       
   132 \end{frame}
       
   133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
       
   134 
       
   135 {
       
   136 \setbeamercolor{background canvas}{bg=cream}
       
   137 \begin{frame}<1-4>[c]
       
   138 \end{frame}
       
   139 }
    97 
   140 
    98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    99 \begin{frame}[t]
   142 \begin{frame}[t]
   100   \frametitle{
   143   \frametitle{
   101     Let's Implement an Efficient\\[-2mm] 
   144     Let's Implement an Efficient\\[-2mm] 
   406 
   449 
   407 \end{frame}
   450 \end{frame}
   408 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   451 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   409 
   452 
   410 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   453 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   411 \begin{frame}[c]
   454 %\begin{frame}[c]
   412 
   455 %
   413 \bl{$r ::= \ZERO \,\;|\;\, \ONE \,\;|\;\, c \,\;|\;\, r_1 + r_2 \,\;|\;\, r_1 \cdot r_2 \,\;|\;\, r^{*} \,\;|\;\, r^{\{n\}}$}  
   456 %\bl{$r ::= \ZERO \,\;|\;\, \ONE \,\;|\;\, c \,\;|\;\, r_1 + r_2 \,\;|\;\, r_1 \cdot r_2 \,\;|\;\, r^{*} \,\;|\;\, r^{\{n\}}$}  
   414 
   457 %
   415 \end{frame}
   458 %\end{frame}
   416 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   459 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   417 
   460 
   418   
       
   419 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   420 \begin{frame}[c]
       
   421 
       
   422 \begin{center}
       
   423 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
       
   424 \bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
       
   425 \bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
       
   426 \bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
       
   427 \bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
       
   428 \bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
       
   429 \bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
       
   430 \bl{$nullable (r^{\{n\}})$}      & \bl{$\dn$} & \bl{if $n = 0$ then \textit{true} else $nullable(r)$}\\  
       
   431 \end{tabular}
       
   432 \end{center}
       
   433 
       
   434 \end{frame}
       
   435 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
       
   436 
       
   437 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   438 \begin{frame}[c]
       
   439 
       
   440 \begin{center}
       
   441 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
       
   442   \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
       
   443   \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
       
   444   \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
       
   445   \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
       
   446   \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
       
   447   & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
       
   448   & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
       
   449   \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$}\\
       
   450 
       
   451   \bl{$\der\, c\, (r^{\{n\}})$}  & \bl{$\dn$} & \bl{if $n = 0$ then $\ZERO$ else $(\der\,c\,r) \cdot r^{\{n-1\}}$}\\
       
   452                                                 
       
   453   \end{tabular}
       
   454 \end{center}
       
   455 
       
   456 \end{frame}
       
   457 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
       
   458 
   461 
   459 
   462 
   460 
   463 
   461 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   464 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   462 \begin{frame}[c]
   465 \begin{frame}[c]
  1301 \end{frame}
  1304 \end{frame}
  1302 
  1305 
  1303 \begin{frame}<1-10>[c]
  1306 \begin{frame}<1-10>[c]
  1304 \end{frame}
  1307 \end{frame}
  1305 
  1308 
  1306 
  1309   
  1307 
  1310 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1308 \end{document}
  1311 \begin{frame}[c]
       
  1312 
       
  1313 \begin{center}
       
  1314 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
       
  1315 \bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
       
  1316 \bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
       
  1317 \bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
       
  1318 \bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
       
  1319 \bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
       
  1320 \bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
       
  1321 \bl{$nullable (r^{\{n\}})$}      & \bl{$\dn$} & \bl{if $n = 0$ then \textit{true} else $nullable(r)$}\\  
       
  1322 \end{tabular}
       
  1323 \end{center}
       
  1324 
       
  1325 \end{frame}
       
  1326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
       
  1327 
       
  1328 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1329 \begin{frame}[c]
       
  1330 
       
  1331 \begin{center}
       
  1332 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
       
  1333   \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
       
  1334   \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
       
  1335   \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
       
  1336   \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
       
  1337   \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
       
  1338   & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
       
  1339   & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
       
  1340   \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$}\\
       
  1341 
       
  1342   \bl{$\der\, c\, (r^{\{n\}})$}  & \bl{$\dn$} & \bl{if $n = 0$ then $\ZERO$ else $(\der\,c\,r) \cdot r^{\{n-1\}}$}\\
       
  1343                                                 
       
  1344   \end{tabular}
       
  1345 \end{center}
       
  1346 
       
  1347 \end{frame}
       
  1348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
       
  1349 
       
  1350 
       
  1351 %%\end{document}
  1309 % below are slides for proving.
  1352 % below are slides for proving.
  1310 
  1353 
  1311 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1354 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1312 \begin{frame}[c]
  1355 \begin{frame}[c]
  1313 \frametitle{Proofs about Rexp (4)}
  1356 \frametitle{Proofs about Rexp (4)}