251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
\documentclass{article}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
\usepackage{../style}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
\usepackage{../langs}
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
4 |
\usepackage{../graphics}
|
251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
\begin{document}
|
520
|
8 |
\fnote{\copyright{} Christian Urban, King's College London, 2014, 2015, 2016, 2017}
|
251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
\section*{Handout 4 (Sulzmann \& Lu Algorithm)}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
So far our algorithm based on derivatives was only able to say
|
422
|
13 |
yes or no depending on whether a string was matched by a regular
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
expression or not. Often a more interesting question is to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
find out \emph{how} a regular expression matched a string?
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
Answering this question will also help us with the problem we
|
319
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
are after, namely tokenising an input string.
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
|
422
|
19 |
The algorithm we will be looking at in this lecture was designed by Sulzmann
|
|
20 |
\& Lu in a rather recent research paper (from 2014). A link to it is
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
provided on KEATS, in case you are interested.\footnote{In my
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
humble opinion this is an interesting instance of the research
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
literature: it contains a very neat idea, but its presentation
|
422
|
24 |
is rather sloppy. In earlier versions of this paper, a King's
|
|
25 |
undergraduate student and I found several rather annoying typos in the
|
|
26 |
examples and definitions.} My PhD student Fahad Ausaf and I even more recently
|
|
27 |
wrote a paper where we build on their result: we provided a
|
|
28 |
mathematical proof that their algorithm is really correct---the proof
|
|
29 |
Sulzmann \& Lu had originally given contained major flaws. Such correctness
|
|
30 |
proofs are important: Kuklewicz maintains a unit-test library
|
520
|
31 |
for the kind of algorithms we are interested in here and he showed
|
422
|
32 |
that many implementations in the ``wild'' are buggy, that is not
|
|
33 |
satisfy his unit tests:
|
|
34 |
|
|
35 |
\begin{center}
|
|
36 |
\url{http://www.haskell.org/haskellwiki/Regex_Posix}
|
|
37 |
\end{center}
|
|
38 |
|
|
39 |
|
|
40 |
In order to give an answer for
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
\emph{how} a regular expression matches a string, Sulzmann and
|
417
|
42 |
Lu use \emph{values}. A value will be the output of the
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
algorithm whenever the regular expression matches the string.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
If the string does not match the string, an error will be
|
417
|
45 |
raised.
|
|
46 |
The definition for values is given below. They are shown
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
together with the regular expressions $r$ to which
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
they correspond:
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
\begin{tabular}{cc}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
\begin{tabular}{@{}rrl@{}}
|
319
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
\multicolumn{3}{c}{regular expressions}\medskip\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
$r$ & $::=$ & $\ZERO$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
& $\mid$ & $\ONE$ \\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
& $\mid$ & $c$ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
& $\mid$ & $r_1 \cdot r_2$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
& $\mid$ & $r_1 + r_2$ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
& $\mid$ & $r^*$ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
|
319
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
\multicolumn{3}{c}{values}\medskip\\
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
$v$ & $::=$ & \\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
& & $Empty$ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
& $\mid$ & $Char(c)$ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
& $\mid$ & $Seq(v_1,v_2)$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
& $\mid$ & $\Left(v)$ \\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
& $\mid$ & $Right(v)$ \\
|
422
|
71 |
& $\mid$ & $Stars\,[v_1,\ldots\,v_n]$ \\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
|
417
|
76 |
\noindent There is no value for the
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
$\ZERO$ regular expression, since it does not match any
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
string. Otherwise there is exactly one value corresponding to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
each regular expression with the exception of $r_1 + r_2$
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
where there are two values, namely $\Left(v)$ and $Right(v)$
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
corresponding to the two alternatives. Note that $r^*$ is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
associated with a list of values, one for each copy of $r$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
that was needed to match the string. This means we might also
|
520
|
84 |
return the empty list $Stars []$, if no copy was needed
|
|
85 |
for $r^*$. For sequence, there is exactly one value, composed
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
of two component values ($v_1$ and $v_2$).
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
|
422
|
88 |
My implementation of regular expressions and values in Scala is
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
shown below. I have in my implementation the convention that
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
regular expressions are written entirely with upper-case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
letters, while values just start with a single upper-case
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
character and the rest are lower-case letters.
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
|
490
|
94 |
{\small\lstinputlisting[language=Scala,numbers=none,linebackgroundcolor=
|
|
95 |
{\ifodd\value{lstnumber}\color{capri!3}\fi}]
|
352
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
{../progs/app01.scala}}
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
|
490
|
99 |
{\small\lstinputlisting[language=Scala,numbers=none,linebackgroundcolor=
|
|
100 |
{\ifodd\value{lstnumber}\color{capri!3}\fi}]
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
{../progs/app02.scala}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
Graphically the algorithm by Sulzmann \& Lu can be illustrated
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
by the picture in Figure~\ref{Sulz} where the path from the
|
422
|
106 |
left to the right involving $\textit{der}/\textit{nullable}$ is the first phase
|
|
107 |
of the algorithm and $\textit{mkeps}/\textit{inj}$, the path from right to left,
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
the second phase. This picture shows the steps required when a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
regular expression, say $r_1$, matches the string $abc$. We
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
first build the three derivatives (according to $a$, $b$ and
|
422
|
111 |
$c$). We then use $\textit{nullable}$ to find out whether the resulting
|
296
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
regular expression can match the empty string. If yes, we call
|
422
|
113 |
the function $\textit{mkeps}$. The $\textit{mkeps}$ function calculates a value for how a regular
|
|
114 |
expression has matched the empty string. Its definition
|
|
115 |
is as follows:
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
\begin{figure}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
\begin{tikzpicture}[scale=2,node distance=1.2cm,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
every node/.style={minimum size=7mm}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
\node (r1) {$r_1$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
\node (r2) [right=of r1]{$r_2$};
|
422
|
123 |
\draw[->,line width=1mm](r1)--(r2) node[above,midway] {$\textit{der}\,a$};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
\node (r3) [right=of r2]{$r_3$};
|
422
|
125 |
\draw[->,line width=1mm](r2)--(r3) node[above,midway] {$\textit{der}\,b$};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
\node (r4) [right=of r3]{$r_4$};
|
422
|
127 |
\draw[->,line width=1mm](r3)--(r4) node[above,midway] {$\textit{der}\,c$};
|
|
128 |
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{$\textit{nullable}$}};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
\node (v4) [below=of r4]{$v_4$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
\draw[->,line width=1mm](r4) -- (v4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
\node (v3) [left=of v4] {$v_3$};
|
422
|
132 |
\draw[->,line width=1mm](v4)--(v3) node[below,midway] {$\textit{inj}\,c$};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
\node (v2) [left=of v3]{$v_2$};
|
422
|
134 |
\draw[->,line width=1mm](v3)--(v2) node[below,midway] {$\textit{inj}\,b$};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
\node (v1) [left=of v2] {$v_1$};
|
422
|
136 |
\draw[->,line width=1mm](v2)--(v1) node[below,midway] {$\textit{inj}\,a$};
|
|
137 |
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{$\textit{mkeps}$}};
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
\caption{The two phases of the algorithm by Sulzmann \& Lu.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
\label{Sulz}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
\end{figure}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
|
422
|
144 |
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
\begin{tabular}{lcl}
|
422
|
148 |
$\textit{mkeps}(\ONE)$ & $\dn$ & $Empty$\\
|
|
149 |
$\textit{mkeps}(r_1 + r_2)$ & $\dn$ & if $\textit{nullable}(r_1)$ \\
|
|
150 |
& & then $\Left(\textit{mkeps}(r_1))$\\
|
|
151 |
& & else $Right(\textit{mkeps}(r_2))$\\
|
|
152 |
$\textit{mkeps}(r_1 \cdot r_2)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{mkeps}(r_2))$\\
|
|
153 |
$\textit{mkeps}(r^*)$ & $\dn$ & $Stars\,[]$ \\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
|
596
|
157 |
\noindent There are no cases for $\ZERO$ and $c$, since
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
these regular expression cannot match the empty string. Note
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
also that in case of alternatives we give preference to the
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
regular expression on the left-hand side. This will become
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
important later on.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
The second phase of the algorithm is organised so that it will
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
calculate a value for how the derivative regular expression
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
has matched a string. For this we need a function that
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
reverses this ``chopping off'' for values which we did in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
first phase for derivatives. The corresponding function is
|
422
|
168 |
called $\textit{inj}$ (short for injection). This function takes three
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
arguments: the first one is a regular expression for which we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
want to calculate the value, the second is the character we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
want to inject and the third argument is the value where we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
will inject the character into. The result of this function is a
|
422
|
173 |
new value. The definition of $\textit{inj}$ is as follows:
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
|
422
|
177 |
$\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\
|
|
178 |
$\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
|
|
179 |
$\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
|
|
180 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
|
|
181 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
|
|
182 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
|
|
183 |
$\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars(\textit{inj}\,r\,c\,v\,::\,vs)$\\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
\noindent This definition is by recursion on the regular
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
expression and by analysing the shape of the values. Therefore
|
422
|
189 |
there are three cases for sequence regular
|
|
190 |
expressions (for all possible shapes of the value we can encounter). The last
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
clause for the star regular expression returns a list where
|
422
|
192 |
the first element is $\textit{inj}\,r\,c\,v$ and the other elements are
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
$vs$. That means $\_\,::\,\_$ should be read as list cons.
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
To understand what is going on, it might be best to do some
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
example calculations and compare them with Figure~\ref{Sulz}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
For this note that we have not yet dealt with the need of
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
simplifying regular expressions (this will be a topic on its
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
own later). Suppose the regular expression is $a \cdot (b
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
\cdot c)$ and the input string is $abc$. The derivatives from
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
the first phase are as follows:
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
\begin{tabular}{ll}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
$r_1$: & $a \cdot (b \cdot c)$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
$r_2$: & $\ONE \cdot (b \cdot c)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
$r_3$: & $(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
$r_4$: & $(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$\\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
\noindent According to the simple algorithm, we would test
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
whether $r_4$ is nullable, which in this case it indeed is.
|
422
|
214 |
This means we can use the function $\textit{mkeps}$ to calculate a
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
value for how $r_4$ was able to match the empty string.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
Remember that this function gives preference for alternatives
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
on the left-hand side. However there is only $\ONE$ on the
|
422
|
218 |
very right-hand side of $r_4$ (underlined)
|
|
219 |
|
|
220 |
\begin{center}
|
|
221 |
$r_4$:\;$(\ZERO \cdot (b \cdot c)) +
|
|
222 |
((\ZERO \cdot c) + \underline{\ONE})$\\
|
|
223 |
\end{center}
|
|
224 |
|
|
225 |
\noindent
|
|
226 |
that matches the empty string.
|
|
227 |
Therefore $\textit{mkeps}$ returns the value
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
$v_4:\;Right(Right(Empty))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
\noindent If there had been a $\ONE$ on the left, then
|
422
|
234 |
$\textit{mkeps}$ would have returned something of the form
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
$\Left(\ldots)$. The point is that from this value we can
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
directly read off which part of $r_4$ matched the empty
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
string: take the right-alternative first, and then the
|
422
|
238 |
right-alternative again.
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
Next we have to ``inject'' the last character, that is $c$ in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
the running example, into this value $v_4$ in order to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
242 |
calculate how $r_3$ could have matched the string $c$.
|
596
|
243 |
For this we call injection with $\textit{inj}(r_3, c, v_4)$.
|
422
|
244 |
According to the definition of $\textit{inj}$ we obtain
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
245 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
246 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
$v_3:\;Right(Seq(Empty, Char(c)))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
249 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
250 |
\noindent This is the correct result, because $r_3$ needs
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
to use the right-hand alternative, and then $\ONE$ needs
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
to match the empty string and $c$ needs to match $c$.
|
596
|
253 |
Next we need to inject back the letter $b$ into $v_3$.
|
|
254 |
For this we call injection with $\textit{inj}(r_2, b, v_3)$.
|
|
255 |
This gives
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
$v_2:\;Seq(Empty, Seq(Char(b), Char(c)))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
\noindent which is again the correct result for how $r_2$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
matched the string $bc$. Finally we need to inject back the
|
596
|
263 |
letter $a$ into $v_2$ giving the final result.
|
|
264 |
For this we call injection with $\textit{inj}(r_1, a, v_2)$
|
|
265 |
and obtain
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
$v_1:\;Seq(Char(a), Seq(Char(b), Char(c)))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
|
596
|
271 |
\noindent This value corresponds to how the regular expression $r_1$,
|
|
272 |
namely $a \cdot (b \cdot c)$, matched the string $abc$.
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
There are a few auxiliary functions that are of interest
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
when analysing this algorithm. One is called \emph{flatten},
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
276 |
written $|\_|$, which extracts the string ``underlying'' a
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
value. It is defined recursively as
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
279 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
280 |
\begin{tabular}{lcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
281 |
$|Empty|$ & $\dn$ & $[]$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
282 |
$|Char(c)|$ & $\dn$ & $[c]$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
$|\Left(v)|$ & $\dn$ & $|v|$\\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
$|Right(v)|$ & $\dn$ & $|v|$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
$|Seq(v_1,v_2)|$& $\dn$ & $|v_1| \,@\, |v_2|$\\
|
422
|
286 |
$|Stars\,[v_1,\ldots ,v_n]|$ & $\dn$ & $|v_1| \,@\ldots @\, |v_n|$\\
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
\noindent Using flatten we can see what are the strings behind
|
422
|
291 |
the values calculated by $\textit{mkeps}$ and $\textit{inj}$. In our running
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
example:
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
\begin{tabular}{ll}
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
$|v_4|$: & $[]$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
$|v_3|$: & $c$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
298 |
$|v_2|$: & $bc$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
299 |
$|v_1|$: & $abc$
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
|
422
|
303 |
\noindent This indicates that $\textit{inj}$ indeed is injecting, or
|
|
304 |
adding, back a character into the value.
|
350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
305 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
There is a problem, however, with the described algorithm
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
307 |
so far: it is very slow. We need to include the simplification
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
308 |
from Lecture 2. This is what we shall do next.
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
310 |
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
\subsubsection*{Simplification}
|
282
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
312 |
|
283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
Generally the matching algorithms based on derivatives do
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
314 |
poorly unless the regular expressions are simplified after
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
each derivative step. But this is a bit more involved in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
algorithm of Sulzmann \& Lu. So what follows might require you
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
317 |
to read several times before it makes sense and also might
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
require that you do some example calculations yourself. As a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
first example consider the last derivation step in our earlier
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
example:
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
|
422
|
322 |
\begin{equation}\label{regexfour}
|
|
323 |
r_4 = \textit{der}\,c\,r_3 =
|
|
324 |
(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)
|
|
325 |
\end{equation}
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
\noindent Simplifying this regular expression would just give
|
422
|
328 |
us $\ONE$. Running $\textit{mkeps}$ with this $\ONE$ as
|
|
329 |
input, however, would give us with the value $Empty$ instead of
|
|
330 |
|
|
331 |
\[Right(Right(Empty))\]
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
|
422
|
333 |
\noindent
|
|
334 |
that was obtained without the simplification. The problem is we need
|
|
335 |
to recreate this more complicated value, rather than just return
|
|
336 |
$Empty$. This will require what I call \emph{rectification functions}.
|
|
337 |
They need to be calculated whenever a regular expression gets
|
|
338 |
simplified.
|
|
339 |
|
|
340 |
Rectification functions take a value as argument and return a
|
|
341 |
(rectified) value. In the example above the argument would be $Empty$
|
|
342 |
and the output $Right(Right(Empty))$. Before we define these
|
|
343 |
rectification functions in general, let us first take a look again at
|
|
344 |
our simplification rules:
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
346 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
$r \cdot \ZERO$ & $\mapsto$ & $\ZERO$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
$\ZERO \cdot r$ & $\mapsto$ & $\ZERO$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
$r \cdot \ONE$ & $\mapsto$ & $r$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
$\ONE \cdot r$ & $\mapsto$ & $r$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
$r + \ZERO$ & $\mapsto$ & $r$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
$\ZERO + r$ & $\mapsto$ & $r$\\
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
$r + r$ & $\mapsto$ & $r$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
|
422
|
358 |
\noindent Applying them to $r_4$ in \eqref{regexfour} will require several nested
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
simplifications in order end up with just $\ONE$. However,
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
it is possible to apply them in a depth-first, or inside-out,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
manner in order to calculate this simplified regular
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
expression.
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
The rectification we can implement by letting simp return not
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
just a (simplified) regular expression, but also a
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
rectification function. Let us consider the alternative case,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
367 |
$r_1 + r_2$, first. By going depth-first, we first simplify
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
the component regular expressions $r_1$ and $r_2.$ This will
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
return simplified versions, say $r_{1s}$ and $r_{2s}$, of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
component regular expressions (if they can be simplified) but
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
also two rectification functions $f_{1s}$ and $f_{2s}$. We
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
need to assemble them in order to obtain a rectified value for
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
$r_1 + r_2$. In case $r_{1s}$ simplified to $\ZERO$, we
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
continue the derivative calculation with $r_{2s}$. The
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
Sulzmann \& Lu algorithm would return a corresponding value,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
say $v_{2s}$. But now this value needs to be ``rectified'' to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
the value
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
$Right(v_{2s})$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
\noindent The reason is that we look for the value that tells
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
us how $r_1 + r_2$ could have matched the string, not just
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
$r_2$ or $r_{2s}$. Unfortunately, this is still not the right
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
value in general because there might be some simplifications
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
that happened inside $r_2$ and for which the simplification
|
520
|
388 |
function returned also a rectification function $f_{2s}$. So in
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
fact we need to apply this one too which gives
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
$Right(f_{2s}(v_{2s}))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
\noindent This is now the correct, or rectified, value. Since
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
the simplification will be done in the first phase of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
397 |
algorithm, but the rectification needs to be done to the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
values in the second phase, it is advantageous to calculate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
the rectification as a function, remember this function and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
then apply the value to this function during the second phase.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
So if we want to implement the rectification as function, we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
402 |
would need to return
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
404 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
$\lambda v.\,Right(f_{2s}(v))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
\noindent which is the lambda-calculus notation for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
409 |
a function that expects a value $v$ and returns everything
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
410 |
after the dot where $v$ is replaced by whatever value is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
given.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
Let us package this idea with rectification functions
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
into a single function (still only considering the alternative
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
415 |
case):
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
416 |
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
\begin{center}
|
422
|
418 |
\begin{tabular}{ll}
|
|
419 |
$_1$ & $simp(r)$:\\
|
|
420 |
$_2$ & \quad case $r = r_1 + r_2$\\
|
|
421 |
$_3$ & \qquad let $(r_{1s}, f_{1s}) = simp(r_1)$\\
|
|
422 |
$_4$ & \qquad \phantom{let} $(r_{2s}, f_{2s}) = simp(r_2)$\smallskip\\
|
|
423 |
$_5$ & \qquad case $r_{1s} = \ZERO$:
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
424 |
return $(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$\\
|
422
|
425 |
$_6$ & \qquad case $r_{2s} = \ZERO$:
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
426 |
return $(r_{1s}, \lambda v. \,\Left(f_{1s}(v)))$\\
|
422
|
427 |
$_7$ & \qquad case $r_{1s} = r_{2s}$:
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
428 |
return $(r_{1s}, \lambda v. \,\Left(f_{1s}(v)))$\\
|
422
|
429 |
$_8$ & \qquad otherwise:
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
430 |
return $(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
431 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
432 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
433 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
434 |
\noindent We first recursively call the simplification with
|
422
|
435 |
$r_1$ and $r_2$ (Lines 3 and 4). This gives simplified regular expressions,
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
436 |
$r_{1s}$ and $r_{2s}$, as well as two rectification functions
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
437 |
$f_{1s}$ and $f_{2s}$. We next need to test whether the
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
438 |
simplified regular expressions are $\ZERO$ so as to make
|
422
|
439 |
further simplifications. In case $r_{1s}$ is $\ZERO$ (Line 5),
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
440 |
then we can return $r_{2s}$ (the other alternative). However
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
441 |
for this we need to build a corresponding rectification
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
442 |
function, which as said above is
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
443 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
444 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
445 |
$\lambda v.\,Right(f_{2s}(v))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
446 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
447 |
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
448 |
\noindent The case where $r_{2s} = \ZERO$ is similar:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
449 |
We return $r_{1s}$ and rectify with $\Left(\_)$ and the
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
450 |
other calculated rectification function $f_{1s}$. This gives
|
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
451 |
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
452 |
\begin{center}
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
453 |
$\lambda v.\,\Left(f_{1s}(v))$
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
454 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
455 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
456 |
\noindent The next case where $r_{1s} = r_{2s}$ can be treated
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
457 |
like the one where $r_{2s} = \ZERO$. We return $r_{1s}$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
458 |
and rectify with $\Left(\_)$ and so on.
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
459 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
460 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
461 |
The otherwise-case is slightly more complicated. In this case
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
462 |
neither $r_{1s}$ nor $r_{2s}$ are $\ZERO$ and also
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
463 |
$r_{1s} \not= r_{2s}$, which means no further simplification
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
464 |
can be applied. Accordingly, we return $r_{1s} + r_{2s}$ as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
465 |
the simplified regular expression. In principle we also do not
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
466 |
have to do any rectification, because no simplification was
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
467 |
done in this case. But this is actually not true: There might
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
468 |
have been simplifications inside $r_{1s}$ and $r_{2s}$. We
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
469 |
therefore need to take into account the calculated
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
470 |
rectification functions $f_{1s}$ and $f_{2s}$. We can do this
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
471 |
by defining a rectification function $f_{alt}$ which takes two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
472 |
rectification functions as arguments and applies them
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
473 |
according to whether the value is of the form $\Left(\_)$ or
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
474 |
$Right(\_)$:
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
475 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
476 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
477 |
\begin{tabular}{l@{\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
478 |
$f_{alt}(f_1, f_2) \dn$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
479 |
\qquad $\lambda v.\,$ case $v = \Left(v')$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
480 |
& return $\Left(f_1(v'))$\\
|
285
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
481 |
\qquad \phantom{$\lambda v.\,$} case $v = Right(v')$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
482 |
& return $Right(f_2(v'))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
483 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
484 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
485 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
486 |
The other interesting case with simplification is the sequence
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
487 |
case. In this case the main simplification function is as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
488 |
follows
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
489 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
490 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
491 |
\begin{tabular}{l}
|
422
|
492 |
$simp(r)$:\hspace{5cm} (continued)\\
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
493 |
\quad case $r = r_1 \cdot r_2$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
494 |
\qquad let $(r_{1s}, f_{1s}) = simp(r_1)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
495 |
\qquad \phantom{let} $(r_{2s}, f_{2s}) = simp(r_2)$\smallskip\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
496 |
\qquad case $r_{1s} = \ZERO$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
497 |
return $(\ZERO, f_{error})$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
498 |
\qquad case $r_{2s} = \ZERO$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
499 |
return $(\ZERO, f_{error})$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
500 |
\qquad case $r_{1s} = \ONE$:
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
501 |
return $(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
502 |
\qquad case $r_{2s} = \ONE$:
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
503 |
return $(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
504 |
\qquad otherwise:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
505 |
return $(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
506 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
507 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
508 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
509 |
\noindent whereby in the last line $f_{seq}$ is again pushing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
510 |
the two rectification functions into the two components of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
511 |
Seq-value:
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
512 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
513 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
514 |
\begin{tabular}{l@{\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
515 |
$f_{seq}(f_1, f_2) \dn$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
516 |
\qquad $\lambda v.\,$ case $v = Seq(v_1, v_2)$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
517 |
& return $Seq(f_1(v_1), f_2(v_2))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
518 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
519 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
520 |
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
521 |
\noindent Note that in the case of $r_{1s} = \ZERO$
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
522 |
(similarly $r_{2s}$) we use the function $f_{error}$ for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
523 |
rectification. If you think carefully, then you will realise
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
524 |
that this function will actually never been called. This is
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
525 |
because a sequence with $\ZERO$ will never recognise any
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
526 |
string and therefore the second phase of the algorithm would
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
527 |
never been called. The simplification function still expects
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
528 |
us to give a function. So in my own implementation I just
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
529 |
returned a function that raises an error. In the case
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
530 |
where $r_{1s} = \ONE$ (similarly $r_{2s}$) we have
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
531 |
to create a sequence where the first component is a rectified
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
532 |
version of $Empty$. Therefore we call $f_{1s}$ with $Empty$.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
533 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
534 |
Since we only simplify regular expressions of the form $r_1 +
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
535 |
r_2$ and $r_1 \cdot r_2$ we do not have to do anything else
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
536 |
in the remaining cases. The rectification function will
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
537 |
be just the identity, which in lambda-calculus terms is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
538 |
just
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
539 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
540 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
541 |
$\lambda v.\,v$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
542 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
543 |
|
422
|
544 |
\noindent This completes the high-level version of the simplification
|
|
545 |
function, which is shown again in Figure~\ref{simp}. The Scala code
|
444
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
546 |
for the simplification function is in Figure~\ref{simprect}.
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
547 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
548 |
\begin{figure}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
549 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
550 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
551 |
$simp(r)$:\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
552 |
\quad case $r = r_1 + r_2$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
553 |
\qquad let $(r_{1s}, f_{1s}) = simp(r_1)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
554 |
\qquad \phantom{let} $(r_{2s}, f_{2s}) = simp(r_2)$\smallskip\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
555 |
\qquad case $r_{1s} = \ZERO$:
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
556 |
return $(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
557 |
\qquad case $r_{2s} = \ZERO$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
558 |
return $(r_{1s}, \lambda v. \,\Left(f_{1s}(v)))$\\
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
559 |
\qquad case $r_{1s} = r_{2s}$:
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
560 |
return $(r_{1s}, \lambda v. \,\Left(f_{1s}(v)))$\\
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
561 |
\qquad otherwise:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
562 |
return $(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
563 |
\medskip\\
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
564 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
565 |
\quad case $r = r_1 \cdot r_2$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
566 |
\qquad let $(r_{1s}, f_{1s}) = simp(r_1)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
567 |
\qquad \phantom{let} $(r_{2s}, f_{2s}) = simp(r_2)$\smallskip\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
568 |
\qquad case $r_{1s} = \ZERO$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
569 |
return $(\ZERO, f_{error})$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
570 |
\qquad case $r_{2s} = \ZERO$:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
571 |
return $(\ZERO, f_{error})$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
572 |
\qquad case $r_{1s} = \ONE$:
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
573 |
return $(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
574 |
\qquad case $r_{2s} = \ONE$:
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
575 |
return $(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
576 |
\qquad otherwise:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
577 |
return $(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
578 |
\medskip\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
579 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
580 |
\quad otherwise:\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
581 |
\qquad return $(r, \lambda v.\,v)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
582 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
583 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
584 |
\caption{The simplification function that returns a simplified
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
585 |
regular expression and a rectification function.\label{simp}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
586 |
\end{figure}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
587 |
|
422
|
588 |
\begin{figure}[p]
|
492
|
589 |
\small
|
490
|
590 |
\lstinputlisting[numbers=left,linebackgroundcolor=
|
|
591 |
{\ifodd\value{lstnumber}\color{capri!3}\fi}]{../progs/app61.scala}
|
422
|
592 |
|
|
593 |
\caption{The Scala code for the simplification function. The
|
520
|
594 |
first part defines some auxiliary functions for the rectification.
|
422
|
595 |
The second part give the simplification function.
|
|
596 |
\label{simprect}}
|
|
597 |
\end{figure}
|
|
598 |
|
|
599 |
|
|
600 |
We are now in the position to define a \emph{lexing function} as follows:
|
|
601 |
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
602 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
603 |
\begin{tabular}{lcl}
|
422
|
604 |
$lex\,r\,[]$ & $\dn$ & if $\textit{nullable}(r)$ then $\textit{mkeps}(r)$\\
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
605 |
& & else $error$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
606 |
$lex\,r\,c\!::\!s$ & $\dn$ & let
|
422
|
607 |
$(r_{simp}, f_{rect}) = simp(\textit{der}(c, r))$\\
|
|
608 |
& & $\textit{inj}\,r\,c\,f_{rect}(lex\,r_{simp}\,s)$
|
287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
609 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
610 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
611 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
612 |
\noindent This corresponds to the $matches$ function we have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
613 |
seen in earlier lectures. In the first clause we are given an
|
520
|
614 |
empty string, $[]$, and need to test whether the regular
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
615 |
expression is $nullable$. If yes, we can proceed normally and
|
422
|
616 |
just return the value calculated by $\textit{mkeps}$. The second clause
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
617 |
is for strings where the first character is $c$, say, and the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
618 |
rest of the string is $s$. We first build the derivative of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
619 |
$r$ with respect to $c$; simplify the resulting regular
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
620 |
expression. We continue lexing with the simplified regular
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
621 |
expression and the string $s$. Whatever will be returned as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
622 |
value, we sill need to rectify using the $f_{rect}$ from the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
623 |
simplification and finally inject $c$ back into the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
624 |
(rectified) value.
|
286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
625 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
626 |
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
627 |
\subsubsection*{Records}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
628 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
629 |
Remember we wanted to tokenize input strings, that means
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
630 |
splitting strings into their ``word'' components. Furthermore
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
631 |
we want to classify each token as being a keyword or
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
632 |
identifier and so on. For this one more feature will be
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
633 |
required, which I call a \emph{record} regular expression.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
634 |
While values encode how a regular expression matches a string,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
635 |
records can be used to ``focus'' on some particular parts of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
636 |
the regular expression and ``forget'' about others.
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
637 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
638 |
Let us look at an example. Suppose you have the regular
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
639 |
expression $a\cdot b + a\cdot c$. Clearly this regular expression can only
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
640 |
recognise two strings. But suppose you are not interested
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
641 |
whether it can recognise $ab$ or $ac$, but rather if it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
642 |
matched, then what was the last character of the matched
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
643 |
string\ldots either $b$ or $c$. You can do this by annotating
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
644 |
the regular expression with a record, written in general
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
645 |
$(x:r)$, where $x$ is just an identifier (in my implementation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
646 |
a plain string) and $r$ is a regular expression. A record will
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
647 |
be regarded as a regular expression. The extended definition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
648 |
in Scala therefore looks as follows:
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
649 |
|
490
|
650 |
{\small\lstinputlisting[language=Scala, numbers=none,linebackgroundcolor=
|
|
651 |
{\ifodd\value{lstnumber}\color{capri!3}\fi}]
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
652 |
{../progs/app03.scala}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
653 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
654 |
\noindent Since we regard records as regular expressions we
|
422
|
655 |
need to extend the functions $\textit{nullable}$ and $\textit{der}$. Similarly
|
|
656 |
$\textit{mkeps}$ and $\textit{inj}$ need to be extended. This means we also need
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
657 |
to extend the definition of values, which in Scala looks as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
658 |
follows:
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
659 |
|
490
|
660 |
{\small\lstinputlisting[language=Scala, numbers=none,linebackgroundcolor=
|
|
661 |
{\ifodd\value{lstnumber}\color{capri!3}\fi}]
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
662 |
{../progs/app04.scala}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
663 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
664 |
\noindent Let us now look at the purpose of records more
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
665 |
closely and let us return to our question whether the string
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
666 |
terminated in a $b$ or $c$. We can do this as follows: we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
667 |
annotate the regular expression $ab + ac$ with a record
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
668 |
as follows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
669 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
670 |
\begin{center}
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
671 |
$a\cdot (x:b) + a\cdot (x:c)$
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
672 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
673 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
674 |
\noindent This regular expression can still only recognise
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
675 |
the strings $ab$ and $ac$, but we can now use a function
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
676 |
that takes a value and returns all records. I call this
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
677 |
function \emph{env} for environment\ldots it builds a list
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
678 |
of identifiers associated with a string. This function
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
679 |
can be defined as follows:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
680 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
681 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
682 |
\begin{tabular}{lcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
683 |
$env(Empty)$ & $\dn$ & $[]$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
684 |
$env(Char(c))$ & $\dn$ & $[]$\\
|
400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
685 |
$env(\Left(v))$ & $\dn$ & $env(v)$\\
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
686 |
$env(Right(v))$ & $\dn$ & $env(v)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
687 |
$env(Seq(v_1,v_2))$& $\dn$ & $env(v_1) \,@\, env(v_2)$\\
|
422
|
688 |
$env(Stars\,[v_1,\ldots ,v_n])$ & $\dn$ &
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
689 |
$env(v_1) \,@\ldots @\, env(v_n)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
690 |
$env(Rec(x:v))$ & $\dn$ & $(x:|v|) :: env(v)$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
691 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
692 |
\end{center}
|
251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
693 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
694 |
\noindent where in the last clause we use the flatten function
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
695 |
defined earlier. As can be seen, the function $env$ ``picks''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
696 |
out all underlying strings where a record is given. Since
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
697 |
there can be more than one, the environment will potentially
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
698 |
contain many ``records''. If we now postprocess the value
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
699 |
calculated by $lex$ extracting all records using $env$, we can
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
700 |
answer the question whether the last element in the string was
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
701 |
an $b$ or a $c$. Lets see this in action: if we use $a\cdot b
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
702 |
+ a\cdot c$ and $ac$ the calculated value will be
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
703 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
704 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
705 |
$Right(Seq(Char(a), Char(c)))$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
706 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
707 |
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
708 |
\noindent If we use instead $a\cdot (x:b) + a\cdot (x:c)$ and
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
709 |
use the $env$ function to extract the recording for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
710 |
$x$ we obtain
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
711 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
712 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
713 |
$[(x:c)]$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
714 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
715 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
716 |
\noindent If we had given the string $ab$ instead, then the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
717 |
record would have been $[(x:b)]$. The fun starts if we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
718 |
iterate this. Consider the regular expression
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
719 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
720 |
\begin{center}
|
326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
721 |
$(a\cdot (x:b) + a\cdot (y:c))^*$
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
722 |
\end{center}
|
251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
723 |
|
288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
724 |
\noindent and the string $ababacabacab$. This string is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
725 |
clearly matched by the regular expression, but we are only
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
726 |
interested in the sequence of $b$s and $c$s. Using $env$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
727 |
we obtain
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
728 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
729 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
730 |
$[(x:b), (x:b), (y:c), (x:b), (y:c), (x:b)]$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
731 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
732 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
733 |
\noindent While this feature might look silly, it is in fact
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
734 |
quite useful. For example if we want to match the name of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
735 |
an email we might use the regular expression
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
736 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
737 |
\[
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
738 |
(name: [a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+)\cdot @\cdot
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
739 |
(domain: [a\mbox{-}z0\mbox{-}9\,.-]^+)\cdot .\cdot
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
740 |
(top\_level: [a\mbox{-}z\,.]^{\{2,6\}})
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
741 |
\]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
742 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
743 |
\noindent Then if we match the email address
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
744 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
745 |
\[
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
746 |
\texttt{christian.urban@kcl.ac.uk}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
747 |
\]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
748 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
749 |
\noindent we can use the $env$ function and find out
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
750 |
what the name, domain and top-level part of the email
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
751 |
address are:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
752 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
753 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
754 |
$[(name:\texttt{christian.urban}),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
755 |
(domain:\texttt{kcl}),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
756 |
(top\_level:\texttt{ac.uk})]$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
757 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
758 |
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
759 |
Recall that we want to lex a little programming language,
|
357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
760 |
called the \emph{While}-language. A simple program in this
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
761 |
language is shown in Figure~\ref{while}. The main keywords in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
762 |
this language are \pcode{while}, \pcode{if}, \pcode{then} and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
763 |
\pcode{else}. As usual we have syntactic categories for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
764 |
identifiers, operators, numbers and so on. For this we would
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
765 |
need to design the corresponding regular expressions to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
766 |
recognise these syntactic categories. I let you do this design
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
767 |
task. Having these regular expressions at our disposal, we can
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
768 |
form the regular expression
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
769 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
770 |
\begin{figure}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
771 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
772 |
\mbox{\lstinputlisting[language=while]{../progs/fib.while}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
773 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
774 |
\caption{The Fibonacci program in the While-language.\label{while}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
775 |
\end{figure}
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
776 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
777 |
\begin{center}
|
357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
778 |
$\textit{WhileRegs} \;\dn\;
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
779 |
\left(\begin{array}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
780 |
(k, KeyWords)\; +\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
781 |
(i, Ids)\;+\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
782 |
(o, Ops)\;+ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
783 |
(n, Nums)\;+ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
784 |
(s, Semis)\;+ \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
785 |
(p, (LParens + RParens))\;+\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
786 |
(b, (Begin + End))\;+ \\
|
551
|
787 |
(w, WhiteSpaces)
|
394
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
788 |
\end{array}\right)^{\mbox{\LARGE{}*}}$
|
357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
789 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
790 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
791 |
\noindent and ask the algorithm by Sulzmann \& Lu to lex, say
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
792 |
the following string
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
793 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
794 |
\begin{center}\large
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
795 |
\code{"if true then then 42 else +"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
796 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
797 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
798 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
799 |
By using the records and extracting the environment, the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
800 |
result is the following list:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
801 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
802 |
\begin{center}\tt
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
803 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
804 |
KEYWORD(if),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
805 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
806 |
IDENT(true),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
807 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
808 |
KEYWORD(then),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
809 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
810 |
KEYWORD(then),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
811 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
812 |
NUM(42),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
813 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
814 |
KEYWORD(else),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
815 |
WHITESPACE,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
816 |
OP(+)
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
817 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
818 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
819 |
|
357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
820 |
\noindent Typically we are not interested in the whitespaces
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
821 |
and comments and would filter them out: this gives
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
822 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
823 |
\begin{center}\tt
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
824 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
825 |
KEYWORD(if),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
826 |
IDENT(true),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
827 |
KEYWORD(then),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
828 |
KEYWORD(then),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
829 |
NUM(42),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
830 |
KEYWORD(else),\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
831 |
OP(+)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
832 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
833 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
834 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
835 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
836 |
which will be the input for the next phase of our compiler.
|
356
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
837 |
|
251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
838 |
\end{document}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
839 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
840 |
%%% Local Variables:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
841 |
%%% mode: latex
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
842 |
%%% TeX-master: t
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
843 |
%%% End:
|