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