| author | Christian Urban <urbanc@in.tum.de> | 
| Thu, 29 Nov 2018 02:37:01 +0000 | |
| changeset 614 | 3ed8ac396863 | 
| parent 581 | 4782a4bfc888 | 
| child 660 | 7ef4d9a2676a | 
| permissions | -rw-r--r-- | 
| 33 | 1  | 
\documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
2  | 
\usepackage{../slides}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
3  | 
\usepackage{../graphics}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
145 
diff
changeset
 | 
4  | 
\usepackage{../langs}
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
145 
diff
changeset
 | 
5  | 
\usepackage{../data}
 | 
| 33 | 6  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
7  | 
\hfuzz=220pt  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
8  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
9  | 
\pgfplotsset{compat=1.11}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
10  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
11  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}  
 | 
| 33 | 12  | 
|
| 445 | 13  | 
\renewcommand{\slidecaption}{CFL 04, King's College London}
 | 
| 33 | 14  | 
|
15  | 
\begin{document}
 | 
|
16  | 
||
17  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
18  | 
\begin{frame}[t]
 | 
| 33 | 19  | 
\frametitle{%
 | 
20  | 
  \begin{tabular}{@ {}c@ {}}
 | 
|
21  | 
\\[-3mm]  | 
|
| 445 | 22  | 
\LARGE Compilers and \\[-2mm]  | 
| 33 | 23  | 
\LARGE Formal Languages (4)\\[3mm]  | 
24  | 
  \end{tabular}}
 | 
|
25  | 
||
26  | 
\normalsize  | 
|
27  | 
  \begin{center}
 | 
|
28  | 
  \begin{tabular}{ll}
 | 
|
29  | 
Email: & christian.urban at kcl.ac.uk\\  | 
|
| 578 | 30  | 
  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
 | 
31  | 
Slides: & KEATS (also homework is there)\\  | 
|
| 33 | 32  | 
  \end{tabular}
 | 
33  | 
  \end{center}
 | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
34  | 
\end{frame}
 | 
| 574 | 35  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
36  | 
||
37  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 578 | 38  | 
\begin{frame}[t]
 | 
39  | 
\frametitle{Survey: Thanks!}
 | 
|
40  | 
\small  | 
|
41  | 
||
42  | 
\hspace{9mm}{\it``\ldots Thanks a million! Thanks without end!''}
 | 
|
43  | 
||
44  | 
\begin{textblock}{3}(12,1.7)
 | 
|
45  | 
\includegraphics[scale=0.1]{../pics/stickman.jpg}
 | 
|
46  | 
\end{textblock}\pause
 | 
|
47  | 
||
48  | 
\begin{textblock}{6}(1,4.15)
 | 
|
49  | 
\begin{bubble}[6.7cm]
 | 
|
50  | 
\it ``Urban is a very talented lecturer: thorough, concise,  | 
|
51  | 
clear, and cares to make sure that we are learning!''  | 
|
52  | 
\end{bubble}
 | 
|
53  | 
\end{textblock}
 | 
|
54  | 
||
55  | 
\only<3>{
 | 
|
56  | 
\begin{textblock}{6}(0.6,8.5)
 | 
|
57  | 
\includegraphics[scale=0.2]{../pics/s1.png}
 | 
|
58  | 
\end{textblock}
 | 
|
59  | 
\begin{textblock}{6}(8,8.5)
 | 
|
60  | 
\includegraphics[scale=0.2]{../pics/s2.png}
 | 
|
61  | 
\end{textblock}}
 | 
|
62  | 
||
| 579 | 63  | 
\only<4->{
 | 
| 578 | 64  | 
\begin{textblock}{6}(0.6,8.5)
 | 
65  | 
\includegraphics[scale=0.2]{../pics/s3.png}
 | 
|
66  | 
\end{textblock}
 | 
|
67  | 
\begin{textblock}{6}(8,8.5)
 | 
|
68  | 
\includegraphics[scale=0.2]{../pics/s4.png}
 | 
|
| 579 | 69  | 
\end{textblock}}
 | 
70  | 
||
71  | 
\only<5>{
 | 
|
72  | 
\begin{textblock}{6}(1.5,14.5)  
 | 
|
73  | 
room too hot, 3h lecture  | 
|
| 578 | 74  | 
\end{textblock}}  
 | 
75  | 
||
76  | 
% \begin{itemize}
 | 
|
77  | 
% \item {\bf My Voice} ``lecturer speaks in a low voice and 
 | 
|
78  | 
% is hard to hear him'' ``please use mic'' ``please use mic  | 
|
79  | 
% \& lecture recording''  | 
|
80  | 
% \item {\bf Pace} ``faster pace'' ``a bit quick for me 
 | 
|
81  | 
% personally''  | 
|
82  | 
% \item {\bf Recording} ``please use recording class''
 | 
|
83  | 
% \item {\bf Module Name} ``misleading''
 | 
|
84  | 
% \item {\bf Examples} ``more examples''
 | 
|
85  | 
% \item {\bf Assessment} ``really appreciate extension of 
 | 
|
86  | 
% first coursework''  | 
|
87  | 
% \end{itemize}
 | 
|
88  | 
||
89  | 
\end{frame}
 | 
|
90  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
91  | 
||
92  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 574 | 93  | 
\begin{frame}[c]
 | 
94  | 
||
| 578 | 95  | 
\begin{center}
 | 
96  | 
\begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
|
97  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
|
98  | 
  \only<-7>{\node[state, initial] (q0) at ( 0,1) {$\mbox{Q}_0$};}
 | 
|
99  | 
  \only<8->{\node[state, initial,accepting] (q0) at ( 0,1) {$\mbox{Q}_0$};}                           
 | 
|
100  | 
  \only<-7>{\node[state] (q1) at ( 1,1) {$\mbox{Q}_1$};}
 | 
|
101  | 
  \only<8->{\node[state,accepting] (q1) at ( 1,1) {$\mbox{Q}_1$};}
 | 
|
102  | 
  \node[state] (q2) at ( 2,1) {$\mbox{Q}_2$};
 | 
|
103  | 
  \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
|
104  | 
                  (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
|
105  | 
                  (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
|
106  | 
                  (q1) edge node[above] {\alert{$a$}} (q2)
 | 
|
107  | 
                  (q2) edge [loop right] node {\alert{$a$}} ()
 | 
|
108  | 
                  (q0) edge [loop below] node {\alert{$b$}} ()
 | 
|
109  | 
;  | 
|
110  | 
\end{tikzpicture}
 | 
|
111  | 
\end{center}\bigskip
 | 
|
| 574 | 112  | 
|
| 578 | 113  | 
\begin{center}
 | 
114  | 
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 | 
|
115  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$\ONE + \mbox{Q}_0\,b + \mbox{Q}_1\,b +  \mbox{Q}_2\,b$}\\
 | 
|
116  | 
\bl{$\mbox{Q}_1$} & \bl{$=$} & \bl{$\mbox{Q}_0\,a$}\\
 | 
|
117  | 
\bl{$\mbox{Q}_2$} & \bl{$=$} & \bl{$\mbox{Q}_1\,a + \mbox{Q}_2\,a$}\\
 | 
|
118  | 
\end{tabular}
 | 
|
119  | 
\end{center}
 | 
|
120  | 
||
121  | 
||
122  | 
Arden's Lemma:  | 
|
123  | 
\begin{center}
 | 
|
124  | 
If \bl{$q = q\,r + s$}\; then\; \bl{$q = s\, r^*$}
 | 
|
125  | 
\end{center}
 | 
|
126  | 
||
127  | 
\only<2-6>{\small
 | 
|
128  | 
\begin{textblock}{6}(1,0.8)
 | 
|
129  | 
\begin{bubble}[6.7cm]
 | 
|
130  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
| 579 | 131  | 
\multicolumn{3}{@{}l}{substitute \bl{$\mbox{Q}_1$} into \bl{$\mbox{Q}_0$} \& \bl{$\mbox{Q}_2$}:}\\    
 | 
| 578 | 132  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$\ONE + \mbox{Q}_0\,b + \mbox{Q}_0\,a\,b +  \mbox{Q}_2\,b$}\\
 | 
133  | 
\bl{$\mbox{Q}_2$} & \bl{$=$} & \bl{$\mbox{Q}_0\,a\,a + \mbox{Q}_2\,a$}
 | 
|
134  | 
\end{tabular}
 | 
|
135  | 
\end{bubble}
 | 
|
136  | 
\end{textblock}}
 | 
|
137  | 
||
138  | 
\only<3-6>{\small
 | 
|
139  | 
\begin{textblock}{6}(2,4.15)
 | 
|
140  | 
\begin{bubble}[6.7cm]
 | 
|
141  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
142  | 
\multicolumn{3}{@{}l}{simplifying \bl{$\mbox{Q}_0$}:}\\    
 | 
|
143  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$\ONE + \mbox{Q}_0\,(b + a\,b) + \mbox{Q}_2\,b$}\\
 | 
|
144  | 
\bl{$\mbox{Q}_2$} & \bl{$=$} & \bl{$\mbox{Q}_0\,a\,a + \mbox{Q}_2\,a$}
 | 
|
145  | 
\end{tabular}
 | 
|
146  | 
\end{bubble}
 | 
|
147  | 
\end{textblock}}
 | 
|
| 574 | 148  | 
|
| 578 | 149  | 
\only<4-6>{\small
 | 
150  | 
\begin{textblock}{6}(3,7.55)
 | 
|
151  | 
\begin{bubble}[6.7cm]
 | 
|
152  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
153  | 
  \multicolumn{3}{@{}l}{Arden for \bl{$\mbox{Q}_2$}:}\\    
 | 
|
154  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$\ONE + \mbox{Q}_0\,(b + a\,b) + \mbox{Q}_2\,b$}\\
 | 
|
155  | 
\bl{$\mbox{Q}_2$} & \bl{$=$} & \bl{$\mbox{Q}_0\,a\,a\,(a^*)$}
 | 
|
156  | 
\end{tabular}
 | 
|
157  | 
\end{bubble}
 | 
|
158  | 
\end{textblock}}
 | 
|
159  | 
||
160  | 
\only<5-6>{\small
 | 
|
161  | 
\begin{textblock}{6}(4,10.9)
 | 
|
162  | 
\begin{bubble}[7.5cm]
 | 
|
163  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
164  | 
  \multicolumn{3}{@{}l}{Substitute \bl{$\mbox{Q}_2$} and simplify:}\\    
 | 
|
165  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$\ONE + \mbox{Q}_0\,(b + a\,b + a\,a\,(a^*)\,b)$}\\
 | 
|
166  | 
\end{tabular}
 | 
|
167  | 
\end{bubble}
 | 
|
168  | 
\end{textblock}}
 | 
|
169  | 
||
170  | 
\only<6>{\small
 | 
|
171  | 
\begin{textblock}{6}(5,13.4)
 | 
|
172  | 
\begin{bubble}[7.5cm]
 | 
|
173  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
174  | 
  \multicolumn{3}{@{}l}{Arden again for \bl{$\mbox{Q}_0$}:}\\    
 | 
|
175  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$(b + a\,b + a\,a\,(a^*)\,b)^*$}\\
 | 
|
176  | 
\end{tabular}
 | 
|
177  | 
\end{bubble}
 | 
|
178  | 
\end{textblock}}
 | 
|
179  | 
||
180  | 
||
181  | 
\only<7->{\small
 | 
|
182  | 
\begin{textblock}{6}(6,11.5)
 | 
|
183  | 
\begin{bubble}[6.7cm]
 | 
|
184  | 
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 | 
|
185  | 
\multicolumn{3}{@{}l}{Finally:}\\    
 | 
|
186  | 
\bl{$\mbox{Q}_0$} & \bl{$=$} & \bl{$(b + a\,b + a\,a\,(a^*)\,b)^*$}\\
 | 
|
187  | 
\bl{$\mbox{Q}_1$} & \bl{$=$} & \bl{$(b + a\,b + a\,a\,(a^*)\,b)^*\,a$}\\
 | 
|
188  | 
\bl{$\mbox{Q}_2$} & \bl{$=$} & \bl{$(b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a^*)$}\\
 | 
|
189  | 
\end{tabular}
 | 
|
190  | 
\end{bubble}
 | 
|
191  | 
\end{textblock}}
 | 
|
192  | 
||
| 574 | 193  | 
\end{frame}
 | 
194  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
195  | 
||
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
196  | 
|
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
197  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
144
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
198  | 
\begin{frame}[c]
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
199  | 
\frametitle{Regexps and Automata}
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
200  | 
|
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
201  | 
\begin{center}
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
202  | 
\begin{tikzpicture}
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
203  | 
\node (rexp)  {\bl{\bf Regexps}};
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
204  | 
\node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
205  | 
\node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
206  | 
\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
207  | 
\path[->,red, line width=2mm] (rexp) edge node [above=4mm, black]  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
208  | 
     {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
209  | 
\path[->,red, line width=2mm] (nfa) edge node [above=4mm, black]  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
210  | 
     {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
211  | 
\path[->, red, line width=2mm] (dfa) edge node [below=5mm, black] {minimisation} (mdfa);
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
212  | 
%%\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
213  | 
\path[->, red, line width=2mm] (dfa) edge [bend left=45] node [below, black] {\begin{tabular}{l}Brzozowski's\\ method\end{tabular}} (rexp);
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
214  | 
|
| 
144
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
215  | 
\end{tikzpicture}\\
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
216  | 
\end{center}
 | 
| 
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
217  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
218  | 
\end{frame}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
219  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
220  | 
|
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
221  | 
|
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
222  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
223  | 
\begin{frame}[t]
 | 
| 445 | 224  | 
\frametitle{\bl{$a^{?\{n\}} \cdot a^{\{n\}}$}}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
225  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
226  | 
\begin{tikzpicture}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
227  | 
\begin{axis}[xlabel={\pcode{a}s},ylabel={time in secs},
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
228  | 
enlargelimits=false,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
229  | 
    xtick={0,5,...,30},
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
230  | 
xmax=30,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
231  | 
ymax=35,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
232  | 
    ytick={0,5,...,30},
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
233  | 
scaled ticks=false,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
234  | 
axis lines=left,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
235  | 
width=10cm,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
236  | 
height=7cm,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
237  | 
    legend entries={Python,Ruby,my NFA},  
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
238  | 
legend pos=north west,  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
239  | 
legend cell align=left]  | 
| 445 | 240  | 
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
 | 
241  | 
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
 | 
|
| 578 | 242  | 
\addplot[red,mark=triangle*, mark options={fill=white}] table {nfasearch.data};	 
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
243  | 
\end{axis}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
244  | 
\end{tikzpicture}
 | 
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
245  | 
|
| 579 | 246  | 
The punchline is that many existing libraries do depth-first search  | 
247  | 
in NFAs (backtracking).  | 
|
| 578 | 248  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
249  | 
\end{frame}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
250  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
251  | 
|
| 520 | 252  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
253  | 
% \begin{frame}[c]
 | 
|
254  | 
% \frametitle{DFA to Rexp}
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
255  | 
|
| 520 | 256  | 
% \begin{center}
 | 
257  | 
% \begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
|
258  | 
%                     every state/.style={minimum size=0pt,
 | 
|
259  | 
% draw=blue!50,very thick,fill=blue!20},]  | 
|
260  | 
%   \node[state, initial]        (q0) at ( 0,1) {$q_0$};
 | 
|
261  | 
%   \node[state]                    (q1) at ( 1,1) {$q_1$};
 | 
|
262  | 
%   \node[state, accepting] (q2) at ( 2,1) {$q_2$};
 | 
|
263  | 
%   \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
|
264  | 
%             (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
|
265  | 
%             (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
|
266  | 
%             (q1) edge node[above] {\alert{$a$}} (q2)
 | 
|
267  | 
%             (q2) edge [loop right] node {\alert{$a$}} ()
 | 
|
268  | 
%             (q0) edge [loop below] node {\alert{$b$}} ();
 | 
|
269  | 
% \end{tikzpicture}
 | 
|
270  | 
% \end{center}\bigskip
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
271  | 
|
| 520 | 272  | 
% \begin{center}
 | 
273  | 
% \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@{\hspace{7mm}}l}
 | 
|
274  | 
% \bl{$q_0$} & \bl{$=$} & \bl{$\ONE + q_0\,b + q_1\,b +  q_2\,b$} & (start state)\\
 | 
|
275  | 
% \bl{$q_1$} & \bl{$=$} & \bl{$q_0\,a$}\\
 | 
|
276  | 
% \bl{$q_2$} & \bl{$=$} & \bl{$q_1\,a + q_2\,a$}\\
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
277  | 
|
| 520 | 278  | 
% \end{tabular}
 | 
279  | 
% \end{center}
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
280  | 
|
| 520 | 281  | 
% Arden's Lemma:  | 
282  | 
% \begin{center}
 | 
|
283  | 
% If \bl{$q = q\,r + s$}\; then\; \bl{$q = s\, r^*$}
 | 
|
284  | 
% \end{center}
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
285  | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
286  | 
|
| 520 | 287  | 
% \end{frame}
 | 
288  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
289  | 
|
| 520 | 290  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
291  | 
% \begin{frame}[c]
 | 
|
292  | 
% \frametitle{DFA Minimisation}
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
293  | 
|
| 520 | 294  | 
% \begin{enumerate}
 | 
295  | 
% \item Take all pairs \bl{$(q, p)$} with \bl{$q \not= p$}
 | 
|
296  | 
% \item Mark all pairs that accepting and non-accepting states  | 
|
297  | 
% \item For  all unmarked pairs \bl{$(q, p)$} and all characters \bl{$c$} test whether
 | 
|
298  | 
% \begin{center}
 | 
|
299  | 
% \bl{$(\delta(q, c), \delta(p,c))$}
 | 
|
300  | 
% \end{center} 
 | 
|
301  | 
% are marked. If yes, then also mark \bl{$(q, p)$}.
 | 
|
302  | 
% \item Repeat last step until no change.  | 
|
303  | 
% \item All unmarked pairs can be merged.  | 
|
304  | 
% \end{enumerate}
 | 
|
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
305  | 
|
| 520 | 306  | 
% \end{frame}
 | 
307  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
308  | 
|
| 520 | 309  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
310  | 
% \begin{frame}[c]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
311  | 
|
| 520 | 312  | 
% \begin{center}
 | 
313  | 
% \begin{tabular}{@{\hspace{-8mm}}cc@{}}
 | 
|
314  | 
% \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
|
315  | 
%                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
|
316  | 
% \node[state,initial]  (q_0)  {$q_0$};
 | 
|
317  | 
% \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
|
318  | 
% \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
|
319  | 
% \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
|
320  | 
% \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
|
321  | 
% \path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
|
322  | 
% \path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
|
323  | 
% \path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
|
324  | 
% \path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
|
325  | 
% \path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
|
326  | 
% \path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
|
327  | 
% \path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
|
328  | 
% \path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
|
329  | 
% \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
|
330  | 
% \end{tikzpicture}
 | 
|
331  | 
% &  | 
|
332  | 
% \raisebox{9mm}{\begin{tikzpicture}[scale=0.6,line width=0.8mm]
 | 
|
333  | 
% \draw (0,0) -- (4,0);  | 
|
334  | 
% \draw (0,1) -- (4,1);  | 
|
335  | 
% \draw (0,2) -- (3,2);  | 
|
336  | 
% \draw (0,3) -- (2,3);  | 
|
337  | 
% \draw (0,4) -- (1,4);  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
338  | 
|
| 520 | 339  | 
% \draw (0,0) -- (0, 4);  | 
340  | 
% \draw (1,0) -- (1, 4);  | 
|
341  | 
% \draw (2,0) -- (2, 3);  | 
|
342  | 
% \draw (3,0) -- (3, 2);  | 
|
343  | 
% \draw (4,0) -- (4, 1);  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
344  | 
|
| 520 | 345  | 
% \draw (0.5,-0.5) node {$q_0$}; 
 | 
346  | 
% \draw (1.5,-0.5) node {$q_1$}; 
 | 
|
347  | 
% \draw (2.5,-0.5) node {$q_2$}; 
 | 
|
348  | 
% \draw (3.5,-0.5) node {$q_3$};
 | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
349  | 
|
| 520 | 350  | 
% \draw (-0.5, 3.5) node {$q_1$}; 
 | 
351  | 
% \draw (-0.5, 2.5) node {$q_2$}; 
 | 
|
352  | 
% \draw (-0.5, 1.5) node {$q_3$}; 
 | 
|
353  | 
% \draw (-0.5, 0.5) node {$q_4$}; 
 | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
354  | 
|
| 520 | 355  | 
% \draw (0.5,0.5) node {\large$\star$}; 
 | 
356  | 
% \draw (1.5,0.5) node {\large$\star$}; 
 | 
|
357  | 
% \draw (2.5,0.5) node {\large$\star$}; 
 | 
|
358  | 
% \draw (3.5,0.5) node {\large$\star$};
 | 
|
359  | 
% \draw (0.5,1.5) node {\large$\star$}; 
 | 
|
360  | 
% \draw (2.5,1.5) node {\large$\star$}; 
 | 
|
361  | 
% \draw (0.5,3.5) node {\large$\star$}; 
 | 
|
362  | 
% \draw (1.5,2.5) node {\large$\star$}; 
 | 
|
363  | 
% \end{tikzpicture}}
 | 
|
364  | 
% \end{tabular}
 | 
|
365  | 
% \end{center}
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
366  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
367  | 
|
| 520 | 368  | 
% \mbox{}\\[-20mm]\mbox{}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
369  | 
|
| 520 | 370  | 
% \begin{center}
 | 
371  | 
% \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
|
372  | 
%                              every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
|
373  | 
% \node[state,initial]  (q_02)  {$q_{0, 2}$};
 | 
|
374  | 
% \node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
 | 
|
375  | 
% \node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};
 | 
|
376  | 
% \path[->] (q_02) edge [bend left] node [above]  {\alert{$a$}} (q_13);
 | 
|
377  | 
% \path[->] (q_13) edge [bend left] node [below]  {\alert{$b$}} (q_02);
 | 
|
378  | 
% \path[->] (q_02) edge [loop below] node  {\alert{$b$}} ();
 | 
|
379  | 
% \path[->] (q_13) edge node [above]  {\alert{$a$}} (q_4);
 | 
|
380  | 
% \path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
|
381  | 
% \end{tikzpicture}\\
 | 
|
382  | 
% minimal automaton  | 
|
383  | 
% \end{center}
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
384  | 
|
| 520 | 385  | 
% \end{frame}
 | 
386  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
387  | 
|
| 
144
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
388  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
389  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
390  | 
\frametitle{Regular Languages}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
391  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
392  | 
Two equivalent definitions:\bigskip  | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
393  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
394  | 
\begin{quote}\rm A language is \alert{regular} iff there exists a
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
395  | 
regular expression that recognises all its strings.  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
396  | 
\end{quote}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
397  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
398  | 
\begin{quote}\rm A language is \alert{regular} iff there exists an
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
399  | 
automaton that recognises all its strings.  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
400  | 
\end{quote}\bigskip\bigskip
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
401  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
402  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
403  | 
\small  | 
| 445 | 404  | 
for example \bl{$a^nb^n$} is not regular
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
405  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
406  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
407  | 
|
| 578 | 408  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
409  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
410  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
411  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
412  | 
\frametitle{Negation}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
413  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
414  | 
Regular languages are closed under negation:\bigskip  | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
415  | 
|
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
416  | 
\begin{center}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
417  | 
\begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
418  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
419  | 
draw=blue!50,very thick,fill=blue!20}]  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
420  | 
  \only<1>{\node[state,initial] (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
421  | 
  \only<2>{\node[state,initial,accepting] (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
422  | 
  \only<1>{\node[state] (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
423  | 
  \only<2>{\node[state,accepting] (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
424  | 
  \only<1>{\node[state, accepting] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
425  | 
  \only<2>{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
426  | 
  \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
427  | 
            (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
428  | 
            (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
429  | 
            (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
430  | 
            (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
431  | 
            (q0) edge [loop below] node {\alert{$b$}} ();
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
432  | 
\end{tikzpicture}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
433  | 
\end{center}\bigskip\bigskip
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
434  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
435  | 
But requires that the automaton is \alert{completed}!
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
436  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
437  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
438  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
439  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
440  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
441  | 
\begin{frame}[c]
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
442  | 
\frametitle{The Goal of this Course}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
443  | 
\mbox{}\\[-26mm]\mbox{}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
444  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
445  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
446  | 
  \begin{tikzpicture}[scale=1,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
447  | 
                      node/.style={
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
448  | 
rectangle,rounded corners=3mm,  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
449  | 
very thick,draw=black!50,  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
450  | 
minimum height=18mm, minimum width=20mm,  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
451  | 
top color=white,bottom color=black!20}]  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
452  | 
|
| 578 | 453  | 
  \node at (3.05, 1.8) {\Large\bf Write a compiler};
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
454  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
455  | 
  \node (0) at (-2.3,0) {}; 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
456  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
457  | 
  \node (A) at (0,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
458  | 
  \node [below right] at (A.north west) {lexer};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
459  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
460  | 
  \node (B) at (3,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
461  | 
\node [below right=1mm] at (B.north west)  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
462  | 
    {\mbox{}\hspace{-1mm}parser};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
463  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
464  | 
  \node (C) at (6,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
465  | 
\node [below right] at (C.north west)  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
466  | 
    {\mbox{}\hspace{-1mm}code gen};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
467  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
468  | 
  \node (1) at (8.4,0) {}; 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
469  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
470  | 
\draw [->,line width=4mm] (0) -- (A);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
471  | 
\draw [->,line width=4mm] (A) -- (B);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
472  | 
\draw [->,line width=4mm] (B) -- (C);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
473  | 
\draw [->,line width=4mm] (C) -- (1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
474  | 
  \end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
475  | 
  \end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
476  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
477  | 
Today a lexer.  | 
| 579 | 478  | 
|
479  | 
\only<2>{
 | 
|
480  | 
\begin{textblock}{1}(6,9.8)
 | 
|
481  | 
\begin{tabular}{c}
 | 
|
482  | 
\includegraphics[scale=0.13]{../pics/rosetta.jpg}\\[-2mm]
 | 
|
483  | 
\footnotesize lexing $\Rightarrow$ recognising words (Stone of Rosetta)  | 
|
484  | 
\end{tabular}
 | 
|
485  | 
\end{textblock}}
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
486  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
487  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
488  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
489  | 
\begin{frame}[c]
 | 
| 578 | 490  | 
\frametitle{Regular Expressions}
 | 
491  | 
||
492  | 
In programming languages they are often used to recognise:\medskip  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
493  | 
|
| 578 | 494  | 
\begin{itemize}
 | 
495  | 
\item symbols, digits  | 
|
496  | 
\item identifiers  | 
|
497  | 
\item numbers (non-leading zeros)  | 
|
498  | 
\item keywords  | 
|
499  | 
\item comments  | 
|
500  | 
\end{itemize}\bigskip
 | 
|
501  | 
||
502  | 
\mbox{}\hfill\bl{\url{http://www.regexper.com}}
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
503  | 
\end{frame}
 | 
| 578 | 504  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
505  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
506  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
507  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
508  | 
\begin{frame}[c]
 | 
| 521 | 509  | 
\frametitle{Lexing: Test Case}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
510  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
511  | 
\mbox{\lstinputlisting[language=While]{../progs/fib.while}}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
512  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
513  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
514  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
515  | 
|
| 578 | 516  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
517  | 
%\begin{frame}[c]
 | 
|
518  | 
%\frametitle{?? Test Case}
 | 
|
519  | 
%  | 
|
520  | 
%\mbox{\lstinputlisting[language=While]{../progs/collatz.while}}
 | 
|
521  | 
%  | 
|
522  | 
%\end{frame}
 | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
523  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
524  | 
|
| 35 | 525  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
526  | 
\begin{frame}[t]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
527  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
528  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
529  | 
\begin{center}\large
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
530  | 
\code{"if true then then 42 else +"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
531  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
532  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
533  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
534  | 
\begin{tabular}{@{}l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
535  | 
KEYWORD: \\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
536  | 
\hspace{5mm}{if}, {then}, {else},\\ 
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
537  | 
WHITESPACE:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
538  | 
\hspace{5mm}{" "}, {$\backslash$n},\\ 
 | 
| 521 | 539  | 
IDENTIFIER:\\  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
540  | 
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
541  | 
NUM:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
542  | 
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
543  | 
OP:\\  | 
| 521 | 544  | 
\hspace{5mm}+, -, *, \%, <, <=\\
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
545  | 
COMMENT:\\  | 
| 
277
 
8eb3261294ba
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
274 
diff
changeset
 | 
546  | 
\hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
547  | 
\end{tabular}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
548  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
549  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
550  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
551  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
552  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
553  | 
\begin{frame}[t]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
554  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
555  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
556  | 
\begin{center}\large
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
557  | 
\code{"if true then then 42 else +"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
558  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
559  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
560  | 
\only<1>{
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
561  | 
\small\begin{tabular}{l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
562  | 
KEYWORD(if),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
563  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
564  | 
IDENT(true),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
565  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
566  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
567  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
568  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
569  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
570  | 
NUM(42),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
571  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
572  | 
KEYWORD(else),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
573  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
574  | 
OP(+)  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
575  | 
\end{tabular}}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
576  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
577  | 
\only<2>{
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
578  | 
\small\begin{tabular}{l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
579  | 
KEYWORD(if),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
580  | 
IDENT(true),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
581  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
582  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
583  | 
NUM(42),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
584  | 
KEYWORD(else),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
585  | 
OP(+)  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
586  | 
\end{tabular}}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
587  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
588  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
589  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
590  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
591  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
592  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
593  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
594  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
595  | 
There is one small problem with the tokenizer. How should we  | 
| 578 | 596  | 
tokenize\ldots?  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
597  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
598  | 
\begin{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
599  | 
\large\code{"x-3"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
600  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
601  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
602  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
603  | 
\begin{tabular}{@{}l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
604  | 
ID: \ldots\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
605  | 
OP:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
606  | 
\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
607  | 
NUM:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
608  | 
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {''0''}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
609  | 
NUMBER:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
610  | 
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
611  | 
\end{tabular}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
612  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
613  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
614  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
615  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
616  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
617  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
618  | 
The same problem with\medskip  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
619  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
620  | 
\[  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
621  | 
\bl{(ab + a) \cdot (c + bc)}
 | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
622  | 
\]\medskip  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
623  | 
|
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
624  | 
and the string $\bl{abc}$.\pause\pause\bigskip
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
625  | 
|
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
626  | 
Or, keywords are \pcode{if} and identifiers are 
 | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
627  | 
letters followed by ``letters + numbers + \_''$^*$  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
628  | 
|
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
629  | 
\[  | 
| 578 | 630  | 
\bl{if}\qquad\bl{iffoo}
 | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
631  | 
\]  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
632  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
633  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
634  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
635  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
636  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
637  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
638  | 
\frametitle{POSIX: Two Rules}
 | 
| 33 | 639  | 
|
| 38 | 640  | 
\begin{itemize}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
641  | 
\item Longest match rule (``maximal munch rule''): The  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
642  | 
longest initial substring matched by any regular expression is taken  | 
| 
278
 
c7890e677e06
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
277 
diff
changeset
 | 
643  | 
as the next token.\bigskip  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
644  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
645  | 
\item Rule priority:  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
646  | 
For a particular longest initial substring, the first regular  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
647  | 
expression that can match determines the token.  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
648  | 
\end{itemize}\bigskip\bigskip\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
649  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
650  | 
\small  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
651  | 
\hfill most posix matchers are buggy\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
652  | 
\footnotesize  | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
653  | 
\hfill  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
654  | 
\url{http://www.haskell.org/haskellwiki/Regex_Posix}
 | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
655  | 
\smallskip\pause  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
656  | 
|
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
657  | 
\hfill \small traditional lexers are fast, but hairy  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
658  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
659  | 
%\url{http://www.technologyreview.com/tr10/?year=2011}  
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
660  | 
%finite deterministic automata/ nondeterministic automaton  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
661  | 
%\item problem with infix operations, for example i-12  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
662  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
663  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
664  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
665  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
666  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
667  | 
\begin{frame}[c]
 | 
| 581 | 668  | 
\frametitle{Sulzmann \& Lu Matcher}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
669  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
670  | 
We want to match the string \bl{$abc$} using \bl{$r_1$}:
 | 
| 38 | 671  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
672  | 
\begin{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
673  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
674  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
675  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
676  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
677  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
678  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
679  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
680  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
 | 
| 521 | 681  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable?$}}};\pause
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
682  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
683  | 
\draw[->,line width=1mm] (r4) -- (v4);\pause  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
684  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
685  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
686  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
687  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
688  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
689  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
690  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
691  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
692  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
693  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
694  | 
\end{tikzpicture}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
695  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
696  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
697  | 
\end{frame}
 | 
| 33 | 698  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
699  | 
||
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
700  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
701  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
702  | 
\frametitle{Regexes and Values}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
703  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
704  | 
Regular expressions and their corresponding values:  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
705  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
706  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
707  | 
\begin{columns}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
708  | 
\begin{column}{3cm}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
709  | 
\begin{tabular}{@{}rrl@{}}
 | 
| 445 | 710  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
 | 
711  | 
           & \bl{$\mid$} & \bl{$\ONE$}   \\
 | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
712  | 
           & \bl{$\mid$} & \bl{$c$}          \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
713  | 
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
714  | 
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
715  | 
\\  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
716  | 
           & \bl{$\mid$} & \bl{$r^*$}         \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
717  | 
\\  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
718  | 
  \end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
719  | 
\end{column}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
720  | 
\begin{column}{3cm}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
721  | 
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
722  | 
  \bl{$v$} & \bl{$::=$}  & \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
723  | 
           &             & \bl{$Empty$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
724  | 
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
 | 
| 
279
 
f406c6677b8c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
278 
diff
changeset
 | 
725  | 
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
726  | 
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
727  | 
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
 | 
| 578 | 728  | 
           & \bl{$\mid$} & \bl{$Stars\,[]$}      \\
 | 
729  | 
           & \bl{$\mid$} & \bl{$Stars\,[v_1,\ldots\,v_n]$} \\
 | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
730  | 
  \end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
731  | 
\end{column}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
732  | 
\end{columns}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
733  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
734  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
735  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
736  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
737  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
738  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
739  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
740  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
741  | 
{\small\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
742  | 
xleftmargin=-5mm] {../progs/app01.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
743  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
744  | 
{\small\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
745  | 
xleftmargin=-5mm] {../progs/app02.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
746  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
747  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
748  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
749  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
750  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
751  | 
\frametitle{Mkeps}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
752  | 
|
| 
280
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
753  | 
Finding a (posix) value for recognising the empty string:  | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
754  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
755  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
756  | 
\begin{tabular}{lcl}
 | 
| 521 | 757  | 
  \bl{$mkeps\,(\ONE)$}  & \bl{$\dn$}  & \bl{$Empty$}\\
 | 
758  | 
  \bl{$mkeps\,(r_1 + r_2)$} & \bl{$\dn$}  & \bl{if $nullable(r_1)$}  \\
 | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
759  | 
                          &             & \bl{then $Left(mkeps(r_1))$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
760  | 
                          &             & \bl{else $Right(mkeps(r_2))$}\\
 | 
| 521 | 761  | 
  \bl{$mkeps\,(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),mkeps(r_2))$}\\
 | 
| 578 | 762  | 
  \bl{$mkeps\,(r^*)$}      & \bl{$\dn$} & \bl{$Stars\,[]$}  \\
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
763  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
764  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
765  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
766  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
767  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
768  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
769  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
770  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
771  | 
\frametitle{Inject}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
772  | 
|
| 521 | 773  | 
Injecting (``Adding'') a character to a value\\[-12mm]\mbox{}
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
774  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
775  | 
\begin{center}
 | 
| 578 | 776  | 
\begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
 | 
777  | 
  \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
 | 
|
778  | 
  \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
 | 
|
779  | 
  \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
 | 
|
780  | 
  \bl{$inj\,(r_1 \cdot r_2)\,c\,(Seq(v_1,v_2))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
 | 
|
781  | 
  \bl{$inj\,(r_1 \cdot r_2)\,c\,(Left(Seq(v_1,v_2)))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
 | 
|
782  | 
  \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\
 | 
|
| 579 | 783  | 
  \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}\\
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
784  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
785  | 
\end{center}\bigskip
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
786  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
787  | 
\footnotesize  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
788  | 
\bl{$inj$}: 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 3rd arg $\mapsto$ a value 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
789  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
790  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
791  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
792  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
793  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
794  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
795  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
796  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
797  | 
\begin{textblock}{10}(3,5)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
798  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
799  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
800  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
801  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
802  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
803  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
804  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
805  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
806  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
807  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
808  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
809  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
810  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
811  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
812  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
813  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
814  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
815  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
816  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
817  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
818  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
819  | 
\end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
820  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
821  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
822  | 
\only<2->{
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
823  | 
\begin{textblock}{6}(1,0.8)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
824  | 
\begin{bubble}[6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
825  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
826  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
827  | 
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
 | 
| 445 | 828  | 
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
 | 
829  | 
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
 | 
|
830  | 
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
831  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
832  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
833  | 
\end{textblock}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
834  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
835  | 
\only<2->{
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
836  | 
\begin{textblock}{6}(5,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
837  | 
\begin{bubble}[7.6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
838  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
839  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
840  | 
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
841  | 
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
842  | 
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
843  | 
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
844  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
845  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
846  | 
\end{textblock}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
847  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
848  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
849  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
850  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
851  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
852  | 
\frametitle{Flatten}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
853  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
854  | 
Obtaining the string underlying a value:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
855  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
856  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
857  | 
\begin{tabular}{lcl}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
858  | 
  \bl{$|Empty|$}     & \bl{$\dn$} & \bl{$[]$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
859  | 
  \bl{$|Char(c)|$}   & \bl{$\dn$} & \bl{$[c]$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
860  | 
  \bl{$|Left(v)|$}   & \bl{$\dn$} & \bl{$|v|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
861  | 
  \bl{$|Right(v)|$}  & \bl{$\dn$} & \bl{$|v|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
862  | 
  \bl{$|Seq(v_1,v_2)|$}& \bl{$\dn$} & \bl{$|v_1| \,@\, |v_2|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
863  | 
  \bl{$|[v_1,\ldots ,v_n]|$} & \bl{$\dn$} & \bl{$|v_1| \,@\ldots @\, |v_n|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
864  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
865  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
866  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
867  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
868  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
869  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
870  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
871  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
872  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
873  | 
\begin{textblock}{10}(3,5)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
874  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
875  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
876  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
877  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
878  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
879  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
880  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
881  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
882  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
883  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
884  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
885  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
886  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
887  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
888  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
889  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
890  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
891  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
892  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
893  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
894  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
895  | 
\end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
896  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
897  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
898  | 
\begin{textblock}{6}(1,0.8)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
899  | 
\begin{bubble}[6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
900  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
901  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
902  | 
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
 | 
| 445 | 903  | 
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
 | 
904  | 
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
 | 
|
905  | 
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
906  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
907  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
908  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
909  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
910  | 
\begin{textblock}{6}(1,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
911  | 
\begin{bubble}[7.6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
912  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
913  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
914  | 
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
915  | 
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
916  | 
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
917  | 
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
918  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
919  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
920  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
921  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
922  | 
\begin{textblock}{6}(12,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
923  | 
\begin{bubble}[2cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
924  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
925  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
926  | 
\bl{$|v_1|$}: & \bl{$abc$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
927  | 
\bl{$|v_2|$}: & \bl{$bc$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
928  | 
\bl{$|v_3|$}: & \bl{$c$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
929  | 
\bl{$|v_4|$}: & \bl{$[]$}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
930  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
931  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
932  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
933  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
934  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
935  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
936  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
937  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
938  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
939  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
940  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
941  | 
\frametitle{Lexing}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
942  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
943  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
944  | 
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
945  | 
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
946  | 
  \bl{$lex\,r\,c::s$} & \bl{$\dn$}  & \bl{$inj\,r\,c\,lex(der(c,r), s)$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
947  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
948  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
949  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
950  | 
\footnotesize  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
951  | 
\bl{$lex$}: returns a value
 | 
| 
280
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
952  | 
|
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
953  | 
\begin{center}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
954  | 
\begin{tikzpicture}[scale=2,node distance=1.0cm,every node/.style={minimum size=6mm}]
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
955  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
956  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
957  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
958  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
959  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
960  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
961  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
962  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
963  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
964  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
965  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
966  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
967  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
968  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
969  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
970  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
971  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
972  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
973  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
974  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
975  | 
\end{tikzpicture}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
976  | 
\end{center}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
977  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
978  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
979  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
980  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
981  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
982  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
983  | 
\frametitle{Records}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
984  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
985  | 
\begin{itemize}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
986  | 
\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
987  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
988  | 
\item \bl{$nullable(x:r) \dn nullable(r)$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
989  | 
\item \bl{$der\,c\,(x:r) \dn (x:der\,c\,r)$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
990  | 
\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
991  | 
\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
992  | 
\end{itemize}\bigskip\bigskip\pause
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
993  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
994  | 
\small  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
995  | 
for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
996  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
997  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
998  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
999  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1000  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1001  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1002  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1003  | 
\begin{itemize}
 | 
| 445 | 1004  | 
\item A regular expression for email addresses  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1005  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1006  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1007  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1008  | 
(name: \bl{$[a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+$})\bl{$\cdot @\cdot$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1009  | 
\qquad(domain: \bl{$[a\mbox{-}z0\mbox{-}9\,.-]^+$}) \bl{$\cdot .\cdot$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1010  | 
\qquad\qquad(top\_level: \bl{$[a\mbox{-}z\,.]^{\{2,6\}}$})
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1011  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1012  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1013  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1014  | 
\bl{\[
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1015  | 
\texttt{christian.urban@kcl.ac.uk}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1016  | 
\]}  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1017  | 
|
| 445 | 1018  | 
\item the result environment:  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1019  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1020  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1021  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1022  | 
\bl{$[(name:\texttt{christian.urban}),$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1023  | 
\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1024  | 
\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1025  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1026  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1027  | 
\end{itemize}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1028  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1029  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1030  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1031  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1032  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1033  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1034  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1035  | 
\frametitle{While Tokens}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1036  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1037  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1038  | 
\begin{tabular}{rcl}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1039  | 
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1040  | 
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1041  | 
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1042  | 
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1043  | 
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1044  | 
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1045  | 
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1046  | 
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1047  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1048  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1049  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1050  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1051  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
1052  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1053  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1054  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1055  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1056  | 
\begin{frame}[c]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1057  | 
\frametitle{Simplification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1058  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1059  | 
\begin{itemize}
 | 
| 522 | 1060  | 
\item If we simplify after the derivative, then we are building the  | 
| 578 | 1061  | 
value for the simplified regular expression, but \alert{\textbf{not}} for the original
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1062  | 
regular expression.  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1063  | 
\end{itemize}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1064  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1065  | 
\begin{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1066  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1067  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1068  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1069  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1070  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1071  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1072  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1073  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1074  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1075  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1076  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1077  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1078  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1079  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1080  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1081  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1082  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1083  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1084  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1085  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1086  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1087  | 
\end{tikzpicture}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1088  | 
\end{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1089  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1090  | 
\small  | 
| 445 | 1091  | 
\hspace{4.5cm}\bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1092  | 
$\mapsto$  | 
| 445 | 1093  | 
\bl{$\ONE$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1094  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1095  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1096  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1097  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1098  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1099  | 
\begin{frame}[c]
 | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1100  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1101  | 
Normally we would have  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1102  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1103  | 
  \begin{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1104  | 
  \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1105  | 
  \end{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1106  | 
|
| 
452
 
0b707b614dac
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
451 
diff
changeset
 | 
1107  | 
and answer how this regular expression matches the empty string  | 
| 578 | 1108  | 
with the value  | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1109  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1110  | 
  \begin{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1111  | 
  \bl{$Right(Right(Empty))$}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1112  | 
  \end{center}\bigskip
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1113  | 
|
| 578 | 1114  | 
  But now we simplify this to \bl{$\ONE$} and would produce \bl{$Empty$} (see \textit{mkeps}).
 | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1115  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1116  | 
\end{frame}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1117  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1118  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1119  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
1120  | 
\begin{frame}[c]
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1121  | 
\frametitle{Rectification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1122  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1123  | 
\def\arraystretch{1.05}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1124  | 
\begin{center}
 | 
| 445 | 1125  | 
\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l@{\hspace{8mm}}l}
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1126  | 
& & & \hspace{5mm}rectification \\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1127  | 
& & & \hspace{5mm}functions:\\
 | 
| 445 | 1128  | 
\bl{$r \cdot \ZERO$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
 | 
1129  | 
\bl{$\ZERO \cdot r$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
 | 
|
1130  | 
\bl{$r \cdot \ONE$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,v, f_2\,Empty)$}\\ 
 | 
|
1131  | 
\bl{$\ONE \cdot r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,Empty, f_2\,v)$}\\ 
 | 
|
1132  | 
\bl{$r + \ZERO$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}\\ 
 | 
|
1133  | 
\bl{$\ZERO + r$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Right(f_2\,v)$}\\
 | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1134  | 
\bl{$r + r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1135  | 
\end{tabular}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1136  | 
\end{center}\medskip\pause
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1137  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1138  | 
\small  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1139  | 
old \bl{$simp$} returns a rexp;\\
 | 
| 445 | 1140  | 
new \bl{$simp$} returns a rexp and a rectification~function.
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1141  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1142  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1143  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1144  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1145  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1146  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1147  | 
\frametitle{Rectification}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1148  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1149  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1150  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1151  | 
\bl{$simp(r)$}:\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1152  | 
\quad case \bl{$r = r_1 + r_2$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1153  | 
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1154  | 
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
 | 
| 445 | 1155  | 
\qquad case \bl{$r_{1s} = \ZERO$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1156  | 
       return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
 | 
| 445 | 1157  | 
\qquad case \bl{$r_{2s} = \ZERO$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1158  | 
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1159  | 
\qquad case \bl{$r_{1s} = r_{2s}$}:
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1160  | 
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1161  | 
\qquad otherwise:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1162  | 
       return \bl{$(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1163  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1164  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1165  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1166  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1167  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1168  | 
\begin{tabular}{l@{\hspace{1mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1169  | 
\bl{$f_{alt}(f_1, f_2) \dn$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1170  | 
\qquad \bl{$\lambda v.\,$} case \bl{$v = Left(v')$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1171  | 
      & return \bl{$Left(f_1(v'))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1172  | 
\qquad \phantom{$\lambda v.\,$} case \bl{$v = Right(v')$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1173  | 
      & return \bl{$Right(f_2(v'))$}\\      
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1174  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1175  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1176  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1177  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1178  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1179  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1180  | 
|
| 445 | 1181  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1182  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1183  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1184  | 
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1185  | 
xleftmargin=-5mm] {../progs/app05.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1186  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1187  | 
\end{frame}
 | 
| 445 | 1188  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1189  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1190  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1191  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1192  | 
\frametitle{Rectification}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1193  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1194  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1195  | 
\begin{tabular}{@{\hspace{-3mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1196  | 
\bl{$simp(r)$}:\ldots\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1197  | 
\quad case \bl{$r = r_1 \cdot r_2$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1198  | 
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1199  | 
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
 | 
| 445 | 1200  | 
\qquad case \bl{$r_{1s} = \ZERO$}: 
 | 
1201  | 
       return \bl{$(\ZERO, f_{error})$}\\
 | 
|
1202  | 
\qquad case \bl{$r_{2s} = \ZERO$}: 
 | 
|
1203  | 
       return \bl{$(\ZERO, f_{error})$}\\
 | 
|
1204  | 
\qquad case \bl{$r_{1s} = \ONE$}: 
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1205  | 
return \bl{$(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$}\\
 | 
| 445 | 1206  | 
\qquad case \bl{$r_{2s} = \ONE$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1207  | 
return \bl{$(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1208  | 
\qquad otherwise:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1209  | 
       return \bl{$(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1210  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1211  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1212  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1213  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1214  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1215  | 
\begin{tabular}{l@{\hspace{1mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1216  | 
\bl{$f_{seq}(f_1, f_2) \dn$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1217  | 
\qquad \bl{$\lambda v.\,$ case $v = Seq(v_1, v_2)$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1218  | 
      & return \bl{$Seq(f_1(v_1), f_2(v_2))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1219  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1220  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1221  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1222  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1223  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1224  | 
|
| 451 | 1225  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1226  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1227  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1228  | 
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1229  | 
xleftmargin=-5mm] {../progs/app06.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1230  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1231  | 
\end{frame}
 | 
| 451 | 1232  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1233  | 
||
1234  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1235  | 
\begin{frame}[t]
 | 
|
1236  | 
\frametitle{Rectification Example}
 | 
|
1237  | 
||
1238  | 
\begin{center}
 | 
|
1239  | 
\bl{$\only<1>{(b \cdot c)}%
 | 
|
1240  | 
     \only<2-3>{(\underline{b \cdot c})}%
 | 
|
1241  | 
     \only<1-3>{+}% 
 | 
|
1242  | 
     \only<1>{(\ZERO + \ONE)}%
 | 
|
1243  | 
     \only<2-3>{(\underline{\ZERO + \ONE})}$}%
 | 
|
1244  | 
\only<4->{%
 | 
|
1245  | 
\bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
 | 
|
1246  | 
}  | 
|
1247  | 
$\mapsto$  | 
|
1248  | 
\bl{$(b \cdot c) + \ONE$}
 | 
|
1249  | 
\end{center}\bigskip
 | 
|
1250  | 
||
1251  | 
\onslide<3->{%
 | 
|
1252  | 
\begin{center}
 | 
|
1253  | 
\begin{tabular}{lcl}
 | 
|
1254  | 
\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
 | 
|
1255  | 
\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
 | 
|
1256  | 
\end{tabular}
 | 
|
1257  | 
\end{center}}
 | 
|
1258  | 
||
1259  | 
\only<4>{%
 | 
|
1260  | 
\begin{center}
 | 
|
1261  | 
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
1262  | 
\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
 | 
|
1263  | 
\quad \bl{$\lambda v.\,$} 
 | 
|
1264  | 
        case \bl{$v = Left(v')$}: 
 | 
|
1265  | 
      & return \bl{$Left(f_{s1}(v'))$}\\
 | 
|
1266  | 
\quad \phantom{$\lambda v.\,$} 
 | 
|
1267  | 
        case \bl{$v = Right(v')$}: 
 | 
|
1268  | 
      & return \bl{$Right(f_{s2}(v'))$}\\ 
 | 
|
1269  | 
\end{tabular}
 | 
|
1270  | 
\end{center}}%
 | 
|
1271  | 
\only<5->{%
 | 
|
1272  | 
\begin{center}
 | 
|
1273  | 
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
1274  | 
\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
 | 
|
1275  | 
\quad \bl{$\lambda v.\,$} 
 | 
|
1276  | 
        case \bl{$v = Left(v')$}: 
 | 
|
1277  | 
      & return \bl{$Left(v')$}\\
 | 
|
1278  | 
\quad \phantom{$\lambda v.\,$} 
 | 
|
1279  | 
        case \bl{$v = Right(v')$}: 
 | 
|
1280  | 
      & return \bl{$Right(Right(v'))$}\\ 
 | 
|
1281  | 
\end{tabular}
 | 
|
1282  | 
\end{center}}%
 | 
|
1283  | 
||
1284  | 
\only<6->{%
 | 
|
1285  | 
\begin{center}
 | 
|
1286  | 
\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
 | 
|
1287  | 
\bl{$\textit{mkeps}$} simplified case: &
 | 
|
1288  | 
\bl{$\textit{Right}(\textit{Empty})$}\\
 | 
|
1289  | 
rectified case: &  | 
|
1290  | 
\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
 | 
|
1291  | 
\end{tabular}
 | 
|
1292  | 
\end{center}}%
 | 
|
1293  | 
||
1294  | 
\end{frame}
 | 
|
1295  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1296  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1297  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1298  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1299  | 
\begin{frame}[c]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1300  | 
\frametitle{Lexing with Simplification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1301  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1302  | 
\begin{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1303  | 
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1304  | 
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1305  | 
  \bl{$lex\,r\,c::s$} & \bl{$\dn$}  & \bl{let $(r', frect) = simp(der(c, r))$}\smallskip\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1306  | 
                      & & \bl{$inj\,r\,c\,(frect(lex(r', s)))$}\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1307  | 
\end{tabular}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1308  | 
\end{center}\bigskip
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1309  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1310  | 
\begin{center}\small
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1311  | 
\begin{tikzpicture}[node distance=1.1cm,every node/.style={minimum size=7mm}]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1312  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1313  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1314  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1315  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1316  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1317  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1318  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1319  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1320  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1321  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1322  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1323  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1324  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1325  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1326  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1327  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1328  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1329  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1330  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1331  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1332  | 
\end{tikzpicture}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1333  | 
\end{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1334  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1335  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1336  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1337  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1338  | 
|
| 451 | 1339  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1340  | 
\begin{frame}[c]
 | 
|
1341  | 
\frametitle{Environments}
 | 
|
1342  | 
||
1343  | 
Obtaining the ``recorded'' parts of a value:  | 
|
1344  | 
||
1345  | 
\begin{center}
 | 
|
1346  | 
\begin{tabular}{lcl}
 | 
|
1347  | 
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1348  | 
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1349  | 
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1350  | 
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1351  | 
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
 | 
|
| 578 | 1352  | 
  \bl{$env(Stars\,[v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
 | 
| 451 | 1353  | 
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
 | 
1354  | 
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
 | 
|
1355  | 
\end{tabular}
 | 
|
1356  | 
\end{center}
 | 
|
1357  | 
||
1358  | 
\end{frame}
 | 
|
1359  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1360  | 
||
1361  | 
||
1362  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1363  | 
\begin{frame}[c]
 | 
|
1364  | 
\frametitle{While Tokens}
 | 
|
1365  | 
||
1366  | 
\begin{center}
 | 
|
1367  | 
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
 | 
|
1368  | 
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
 | 
|
1369  | 
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
 | 
|
1370  | 
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
 | 
|
1371  | 
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
 | 
|
1372  | 
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
 | 
|
1373  | 
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
 | 
|
1374  | 
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
 | 
|
1375  | 
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
 | 
|
1376  | 
\end{tabular}
 | 
|
1377  | 
\end{center}
 | 
|
1378  | 
||
1379  | 
\end{frame}
 | 
|
1380  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1381  | 
||
1382  | 
||
1383  | 
||
1384  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1385  | 
\begin{frame}[t]
 | 
|
1386  | 
||
1387  | 
\consolas  | 
|
1388  | 
\begin{center}
 | 
|
1389  | 
\code{"if true then then 42 else +"}
 | 
|
1390  | 
\end{center}
 | 
|
1391  | 
||
1392  | 
\only<1>{
 | 
|
1393  | 
\small\begin{tabular}{l}
 | 
|
1394  | 
KEYWORD(if),\\  | 
|
1395  | 
WHITESPACE,\\  | 
|
1396  | 
IDENT(true),\\  | 
|
1397  | 
WHITESPACE,\\  | 
|
1398  | 
KEYWORD(then),\\  | 
|
1399  | 
WHITESPACE,\\  | 
|
1400  | 
KEYWORD(then),\\  | 
|
1401  | 
WHITESPACE,\\  | 
|
1402  | 
NUM(42),\\  | 
|
1403  | 
WHITESPACE,\\  | 
|
1404  | 
KEYWORD(else),\\  | 
|
1405  | 
WHITESPACE,\\  | 
|
1406  | 
OP(+)  | 
|
1407  | 
\end{tabular}}
 | 
|
1408  | 
||
1409  | 
\only<2>{
 | 
|
1410  | 
\small\begin{tabular}{l}
 | 
|
1411  | 
KEYWORD(if),\\  | 
|
1412  | 
IDENT(true),\\  | 
|
1413  | 
KEYWORD(then),\\  | 
|
1414  | 
KEYWORD(then),\\  | 
|
1415  | 
NUM(42),\\  | 
|
1416  | 
KEYWORD(else),\\  | 
|
1417  | 
OP(+)  | 
|
1418  | 
\end{tabular}}
 | 
|
1419  | 
||
1420  | 
\end{frame}
 | 
|
1421  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1422  | 
||
1423  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1424  | 
\begin{frame}[c]
 | 
|
| 521 | 1425  | 
\frametitle{Lexer: Two Rules}
 | 
| 451 | 1426  | 
|
1427  | 
\begin{itemize}
 | 
|
1428  | 
\item Longest match rule (``maximal munch rule''): The  | 
|
1429  | 
longest initial substring matched by any regular expression is taken  | 
|
1430  | 
as next token.\bigskip  | 
|
1431  | 
||
1432  | 
\item Rule priority:  | 
|
1433  | 
For a particular longest initial substring, the first regular  | 
|
1434  | 
expression that can match determines the token.  | 
|
1435  | 
||
1436  | 
\end{itemize}
 | 
|
1437  | 
||
1438  | 
%\url{http://www.technologyreview.com/tr10/?year=2011}
 | 
|
1439  | 
||
1440  | 
%finite deterministic automata/ nondeterministic automaton  | 
|
1441  | 
||
1442  | 
%\item problem with infix operations, for example i-12  | 
|
1443  | 
||
1444  | 
||
1445  | 
\end{frame}
 | 
|
1446  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1447  | 
||
1448  | 
||
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1449  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1450  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1451  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1452  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1453  | 
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
 | 
| 578 | 1454  | 
\bl{$zeroable(\ZERO)$}      & \bl{$\dn$} & \bl{$true$}\\
 | 
1455  | 
\bl{$zeroable(\ONE)$}         & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
|
| 445 | 1456  | 
\bl{$zeroable(c)$}                & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
1457  | 
\bl{$zeroable(r_1 + r_2)$}        & \bl{$\dn$} & \bl{$zeroable(r_1) \wedge zeroable(r_2)$}\\ 
 | 
|
1458  | 
\bl{$zeroable(r_1 \cdot r_2)$}    & \bl{$\dn$} & \bl{$zeroable(r_1) \vee zeroable(r_2)$}\\
 | 
|
1459  | 
\bl{$zeroable(r^*)$}              & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1460  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1461  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1462  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1463  | 
\begin{center}
 | 
| 445 | 1464  | 
\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1465  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1466  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1467  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1468  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1469  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1470  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1471  | 
|
| 33 | 1472  | 
\end{document}
 | 
1473  | 
||
1474  | 
%%% Local Variables:  | 
|
1475  | 
%%% mode: latex  | 
|
1476  | 
%%% TeX-master: t  | 
|
1477  | 
%%% End:  | 
|
1478  |