afl-material: slides/slides02.tex@6cb517754d8a (annotated)

7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
258 1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	2	\usepackage{../slides}
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	3	\usepackage{../graphics}
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	4	\usepackage{../langs}
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	5	\usepackage{../data}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
258 1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	7	\hfuzz=220pt
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	8
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	9	\lstset{language=Scala,
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	10	style=mystyle,
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	11	numbersep=0pt,
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	12	numbers=none,
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	13	xleftmargin=0mm}
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	14
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	15	\pgfplotsset{compat=1.11}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	16
258 1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	17	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	18
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	% beamer stuff
258 1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	20	\renewcommand{\slidecaption}{AFL 02, King's College London}
1e4da6d2490c updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	21
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\begin{document}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	26	\begin{frame}[t]
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	\frametitle{%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	\begin{tabular}{@ {}c@ {}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	\\[-3mm]
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	\LARGE Automata and \\[-2mm]
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	31	\LARGE Formal Languages (2)\\[3mm]
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	\end{tabular}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	33
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	34	\normalsize
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	\begin{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	\begin{tabular}{ll}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	Email: & christian.urban at kcl.ac.uk\\
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	38	Office: & S1.27 (1st floor Strand Building)\\
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	39	Slides: & KEATS
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	\end{tabular}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	\end{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	42
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	43	\end{frame}
24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	44	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	47	\begin{frame}[c]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	48	\frametitle{\begin{tabular}{@ {}c@ {}}An Efficient Regular\\[-1mm]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	49	Expression Matcher\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	50
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	51	\footnotesize
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	52	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	53	\begin{tabular}{@{}cc@{}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	54	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	55	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	56	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	57	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	58	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	59	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	60	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	61	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	62	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	63	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	64	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	65	width=4.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	66	height=4.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	67	legend entries={Python,Ruby},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	68	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	69	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	70	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	71	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	72	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	73	\addplot[brown,mark=pentagon*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	74	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	75	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	76	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	77	&
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	78	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	79	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	80	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	81	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	82	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	83	xtick={0,3000,...,12000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	84	xmax=12000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	85	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	86	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	87	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	88	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	89	width=5.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	90	height=4.5cm
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	91	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	92	\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	93	\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	94	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	95	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	96	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	97	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	98
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	99
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	100	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	101	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	102
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	103
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	104	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	105	\begin{frame}[c]
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	106	\frametitle{Languages, Strings}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	107
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	108	\begin{itemize}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	109	\item \alert{\bf Strings} are lists of characters, for example
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	110	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	111	\bl{$[]$},\;\bl{$abc$} \hspace{2cm}(Pattern match: \bl{$c\!::\!s$})
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	112	\end{center}\bigskip
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	113
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	114
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	115	\item A \alert{\bf language} is a set of strings, for example\medskip
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	116	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	117	\bl{$\{[], hello, \textit{foobar}, a, abc\}$}
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	118	\end{center}\bigskip
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	119
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	120	\item \alert{\bf Concatenation} of strings and sets
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	121
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	122	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	123	\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	124	\bl{$\textit{foo}\;@\;bar$} & \bl{$=$} & \bl{$\textit{foobar}$}\medskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	125	\bl{$A\;@\;B$} & \bl{$\dn$} & \bl{$\{ s_1\,@\,s_2 \;\mid\; s_1 \in A \wedge s_2 \in B\}$}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	126	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	127	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	128
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	129	%\item The \alert{\bf meaning} of a regular expression is a set of
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	130	% strings, or language.
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	131	\end{itemize}
24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	132
24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	133	\end{frame}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	134	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	135
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	136
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	137	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	138	\begin{frame}[t]
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	140
15 f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	141	Their inductive definition:
f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	142
f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	143
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	144	\begin{textblock}{6}(2,7.5)
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	\begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	146	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	147	& \bl{$\mid$} & \bl{$\epsilon$} & empty string / \pcode{""} / $[]$\\
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	148	& \bl{$\mid$} & \bl{$c$} & character\\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	149	& \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	150	& \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	151	& \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	\end{tabular}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	\end{textblock}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	154
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	155
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	156	\only<2->{\footnotesize
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	157	\begin{textblock}{9}(2,0.5)
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	158	\begin{bubble}[9.8cm]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	159	\lstinputlisting{../progs/app01.scala}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	160	\end{bubble}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	161	\end{textblock}}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	162
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	163	\end{frame}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	164	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	165
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	166
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	167	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	168	\begin{frame}[c]
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	169	\frametitle{\begin{tabular}{c}The Meaning of a\\[-2mm] Regular Expression\end{tabular}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	170
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	171	\begin{textblock}{15}(1,4)
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	172	\begin{tabular}{@ {}rcl}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	173	\bl{$L(\varnothing)$} & \bl{$\dn$} & \bl{$\varnothing$}\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	174	\bl{$L(\epsilon)$} & \bl{$\dn$} & \bl{$\{$[]$\}$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	175	\bl{$L(c)$} & \bl{$\dn$} & \bl{$\{[c]\}$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	176	\bl{$L(r_1 + r_2)$} & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	177	\bl{$L(r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$L(r_1) \,@\, L(r_2)$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	178	\bl{$L(r^*)$} & \bl{$\dn$} & \bl{$\bigcup_{n \ge 0} L(r)^n$}\\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	\end{tabular}\bigskip
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	180
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	181	\only<2->{
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	182	\hspace{5mm}\textcolor{blue}{$L(r)^0 \;\dn\; \{[]\}$}\\
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	183	\textcolor{blue}{$L(r)^{n+1} \;\dn\; L(r) \,@\, L(r)^n$}}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	184	\end{textblock}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	185
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	186	\only<1->{
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	187	\begin{textblock}{6}(9,12)\small
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	188	\bl{$L$} is a function from regular expressions to sets of strings\\
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	189	\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	190	\end{textblock}}
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	191
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	192	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	194
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	195	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	196	\begin{frame}[c]
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	197
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	198	\large
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	199	\begin{center}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	200	What is \bl{$L(a^*)$}?
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	201	\end{center}
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	202
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	203	\end{frame}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	204	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	205
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	206	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	207	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	208	\frametitle{\begin{tabular}{c}Concrete Equivalences\end{tabular}}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	209
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	210	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	211	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	212	$(a + b) + c$ & $\equiv$ & $a + (b + c)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	213	$a + a$ & $\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	214	$a + b$ & $\equiv$ & $b + a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	215	$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	216	$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	217	$a \cdot a$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	218	$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	219	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	220	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	221
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	222	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	223	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	224
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	225	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	226	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	227	\frametitle{\begin{tabular}{c}Corner Cases\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	228
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	229	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	230	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	231	$a \cdot \varnothing$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	232	$a + \epsilon$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	233	$\epsilon$ & $\equiv$ & $\varnothing^*$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	234	$\epsilon^*$ & $\equiv$ & $\epsilon$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	235	$\varnothing^*$ & $\not\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	236	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	237	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	238
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	239	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	240	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	241
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	242	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	243	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	244	\frametitle{\begin{tabular}{c}Simplification Rules\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	245
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	246	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	247	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	248	$r + \varnothing$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	249	$\varnothing + r$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	250	$r \cdot \epsilon$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	251	$\epsilon \cdot r$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	252	$r \cdot \varnothing$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	253	$\varnothing \cdot r$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	254	$r + r$ & $\equiv$ & $r$
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	255	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	256	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	257
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	258	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	259	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	260
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	261	\newcommand{\YES}{\textcolor{gray}{yes}}
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	262	\newcommand{\NO}{\textcolor{gray}{no}}
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	263	\newcommand{\FORALLR}{\textcolor{gray}{$\forall$ r.}}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	264
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	265	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	\begin{frame}[c]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	267	\frametitle{\begin{tabular}{c}The Specification\\[-1mm] for Matching\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	268
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	269	\large
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	270	A regular expression \bl{$r$} matches a string \bl{$s$}\\ if and only if
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	271
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	273	\bl{$s \in L(r)$}\\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	\end{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	275
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	276	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	277	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	278
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	279	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	280	\mode<presentation>{
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	281	\begin{frame}[c]
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	282	\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	283
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	284	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	285	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	286	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	287	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	288	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	289	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	290	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	291	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	292	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	293	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	294	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	295	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	296	width=9cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	297	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	298	legend entries={Python,Ruby},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	299	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	300	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	301	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	302	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	303	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	304	\addplot[brown,mark=pentagon*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	305	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	306	\end{axis}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	307	\end{tikzpicture}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	308	\end{center}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	309
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	310	\end{frame}}
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	311	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	312
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	313	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	314	\mode<presentation>{
118 6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	315	\begin{frame}[c]
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	316	\frametitle{\begin{tabular}{c}Evil Regular Expressions\end{tabular}}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	317
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	318	\begin{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	319	\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	320	\item Evil regular expressions\medskip
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	321	\begin{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	322	\item \bl{$(a?\{n\}) \cdot a\{n\}$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	323	\item \bl{$(a^+)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	324	\item \bl{$([a$\,-\,$z]^+)^*$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	325	\item \bl{$(a + a \cdot a)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	326	\item \bl{$(a + a?)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	327	\end{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	328	\end{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	329
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	330	\end{frame}}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	331	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	332
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	333	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	334	\mode<presentation>{
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	335	\begin{frame}[t]
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	336	\frametitle{\begin{tabular}{c}A Matching Algorithm\end{tabular}}
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	337
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	338
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	339	\ldots{}whether a regular expression can match the empty string:
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	340	\begin{center}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	341	\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	342	\bl{$nullable(\varnothing)$} & \bl{$\dn$} & \bl{$f\!\/alse$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	343	\bl{$nullable(\epsilon)$} & \bl{$\dn$} & \bl{$true$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	344	\bl{$nullable (c)$} & \bl{$\dn$} & \bl{$f\!alse$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	345	\bl{$nullable (r_1 + r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	346	\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	347	\bl{$nullable (r^*)$} & \bl{$\dn$} & \bl{$true$} \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	348	\end{tabular}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	349	\end{center}
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	350
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	351	\end{frame}}
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	352	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	353
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	354
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	355	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	356	\mode<presentation>{
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	357	\begin{frame}[c]
15 f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	358	\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	359
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	360	\large
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	361	If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	362	expression that matches \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	363
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	364	\small
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	365	\bl{$der\,c\,r$} gives the answer
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	\end{frame}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	367	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	368
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	369	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	370	\mode<presentation>{
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	371	\begin{frame}[c]
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	372	\frametitle{\begin{tabular}{c}The Derivative of a Rexp (2)\end{tabular}}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	373
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	374	\begin{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	375	\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	376	\bl{$der\, c\, (\varnothing)$} & \bl{$\dn$} & \bl{$\varnothing$} & \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	377	\bl{$der\, c\, (\epsilon)$} & \bl{$\dn$} & \bl{$\varnothing$} & \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	378	\bl{$der\, c\, (d)$} & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	379	\bl{$der\, c\, (r_1 + r_2)$} & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	380	\bl{$der\, c\, (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{if $nullable (r_1)$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	381	& & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	382	& & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	383	\bl{$der\, c\, (r^)$} & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^)$} &\medskip\\\pause
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	384
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	385	\bl{$\textit{ders}\, []\, r$} & \bl{$\dn$} & \bl{$r$} & \\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	386	\bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	387	\end{tabular}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	388	\end{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	389
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	390	\end{frame}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	392
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	393	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	394	\mode<presentation>{
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	395	\begin{frame}[c]
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	396	\frametitle{\begin{tabular}{c}Examples\end{tabular}}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	397
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	398	Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	399
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	400	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	401	\begin{tabular}{l}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	402	\bl{$der\,a\,r =?$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	403	\bl{$der\,b\,r =?$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	404	\bl{$der\,c\,r =?$}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	405	\end{tabular}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	406	\end{center}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	407
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	408
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	409	\end{frame}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	410	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	411
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	412	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	413	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	414	\begin{frame}[t]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	415	\frametitle{The Algorithm}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	416
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	417	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	418	\begin{tabular}{@{}rll@{}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	419	Input: & \bl{$r_1$}, \bl{$abc$}\medskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	420	Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = der\,a\,r_1)$}\smallskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	421	Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = der\,b\,r_2)$}\smallskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	422	Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = der\,b\,r_3)$}\smallskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	423	Step 4: & the string is exhausted; test & (\bl{$nullable(r_4)$})\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	424	& whether \bl{$r_4$} can recognise\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	425	& the empty string\smallskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	426	Output: & result of the test\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	427	& $\Rightarrow true \,\text{or}\, \textit{false}$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	428	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	429	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	430
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	431
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	432	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	433	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	434
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	435	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	436	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	437	\begin{frame}[c]
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	438	\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	439
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	440	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	441	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	442	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	443	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	444	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	445	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	446	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	447	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	448	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	449	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	450	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	451	width=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	452	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	453	legend entries={Python,Ruby,Scala V1},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	454	legend pos=outer north east,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	455	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	456	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	457	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	458	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	459	\addplot[brown,mark=pentagon*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	460	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	461	\addplot[red,mark=triangle*,mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	462	table {re1.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	463	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	464	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	465	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	466
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	467	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	468	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	469
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	470	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	471	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	472	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	473	\frametitle{\begin{tabular}{c}A Problem\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	474
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	475	We represented the ``n-times'' \bl{$a\{n\}$} as a sequence regular expression:
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	476
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	477	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	478	\begin{tabular}{rl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	479	1: & \bl{$a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	480	2: & \bl{$a\cdot a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	481	3: & \bl{$a\cdot a\cdot a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	482	& \ldots\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	483	13: & \bl{$a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	484	& \ldots\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	485	20:
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	486	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	487	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	488
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	489	This problem is aggravated with \bl{$a?$} being represented as \bl{$\epsilon + a$}.
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	490	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	491	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	492
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	493	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	494	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	495	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	496	\frametitle{\begin{tabular}{c}Solving the Problem\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	497
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	498	What happens if we extend our regular expressions
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	499
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	500	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	501	\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	502	\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	503	& \bl{$\mid$} & \bl{$r\{n\}$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	504	& \bl{$\mid$} & \bl{$r?$}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	505	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	506	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	507
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	508	What is their meaning? What are the cases for \bl{$nullable$} and \bl{$der$}?
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	509	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	510	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	511
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	512
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	513	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	514	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	515	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	516	\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	517
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	518	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	519	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	520	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	521	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	522	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	523	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	524	xtick={0,200,...,1000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	525	xmax=1000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	526	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	527	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	528	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	529	width=9.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	530	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	531	legend entries={Python,Ruby,Scala V1,Scala V2},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	532	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	533	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	534	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	535	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	536	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	537	\addplot[brown,mark=pentagon*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	538	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	539	\addplot[red,mark=triangle*,mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	540	table {re1.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	541	\addplot[green,mark=square*,mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	542	table {re2b.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	543	\end{axis}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	544	\end{tikzpicture}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	545	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	546
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	547	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	548	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	549
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	550
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	551	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	552	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	553	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	554	\frametitle{\begin{tabular}{c}Examples\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	555
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	556	Recall the example of \bl{$r \dn ((a \cdot b) + b)^*$} with
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	557
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	558	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	559	\begin{tabular}{l}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	560	\bl{$der\,a\,r = ((\epsilon \cdot b) + \varnothing) \cdot r$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	561	\bl{$der\,b\,r = ((\varnothing \cdot b) + \epsilon)\cdot r$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	562	\bl{$der\,c\,r = ((\varnothing \cdot b) + \varnothing)\cdot r$}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	563	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	564	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	565
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	566	What are these regular expressions equivalent to?
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	567
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	568	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	569	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	570
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	571
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	572
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	573	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	574	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	575	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	576	\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	577
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	578	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	579	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	580	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	581	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	582	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	583	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	584	xtick={0,3000,...,12000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	585	xmax=12000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	586	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	587	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	588	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	589	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	590	width=9cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	591	height=7cm
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	592	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	593	\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	594	\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	595	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	596	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	597	\end{center}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	598
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	599	\end{frame}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	600	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	601
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	602	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	603	\mode<presentation>{
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	604	\begin{frame}[t]
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	605	\frametitle{\begin{tabular}{c}Proofs about Rexps\end{tabular}}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	606
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	607	Remember their inductive definition:\\[5cm]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	608
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	609	\begin{textblock}{6}(5,5)
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	610	\begin{tabular}{@ {}rrl}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	611	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	612	& \bl{$\mid$} & \bl{$\epsilon$} \\
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	613	& \bl{$\mid$} & \bl{$c$} \\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	614	& \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	615	& \bl{$\mid$} & \bl{$r_1 + r_2$} \\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	616	& \bl{$\mid$} & \bl{$r^*$} \\
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	617	\end{tabular}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	618	\end{textblock}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	619
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	620	If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	621
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	622	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	623	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	624
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	625	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	626	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	627	\begin{frame}[c]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	628	\frametitle{\begin{tabular}{c}Proofs about Rexp (2)\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	629
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	630	\begin{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	631	\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	632	\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	633	holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	634	\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	635	holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	636	\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	637	holds for \bl{$r$}.
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	638	\end{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	639
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	640	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	641	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	642
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	643	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	644	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	645	\begin{frame}[c]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	646	\frametitle{\begin{tabular}{c}Proofs about Rexp (3)\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	647
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	648	Assume \bl{$P(r)$} is the property:
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	649
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	650	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	651	\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	652	\end{center}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	653
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	654	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	655	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	656
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	657	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	658	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	659	\begin{frame}[c]
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	660	\frametitle{\begin{tabular}{c}Proofs about Rexp (4)\end{tabular}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	661
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	662
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	663	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	664	\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	665	$rev(\varnothing)$ & $\dn$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	666	$rev(\epsilon)$ & $\dn$ & $\epsilon$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	667	$rev(c)$ & $\dn$ & $c$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	668	$rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	669	$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	670	$rev(r^)$ & $\dn$ & $rev(r)^$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	671	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	672	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	673
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	674
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	675	We can prove
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	676
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	677	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	678	\bl{$L(rev(r)) = \{s^{-1} \;\|\; s \in L(r)\}$}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	679	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	680
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	681	by induction on \bl{$r$}.
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	682
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	683	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	684	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	685
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	686	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	687	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	688	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	689	\frametitle{\begin{tabular}{c}Proofs about Rexp (5)\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	690
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	691	Let \bl{$Der\,c\,A$} be the set defined as
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	692
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	693	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	694	\bl{$Der\,c\,A \dn \{ s \;\|\; c\!::\!s \in A\}$ }
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	695	\end{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	696
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	697	We can prove
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	698
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	699	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	700	\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	701	\end{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	702
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	703	by induction on \bl{$r$}.
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	704
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	705	\end{frame}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	706	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	707
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	708
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	709	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	710	\mode<presentation>{
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	711	\begin{frame}[c]
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	712	\frametitle{\begin{tabular}{c}Proofs about Strings\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	713
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	714	If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	715
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	716	\begin{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	717	\item \bl{$P$} holds for the empty string, and\medskip
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	718	\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	719	already holds for \bl{$s$}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	720	\end{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	721	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	722	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	723
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	724	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	725	\mode<presentation>{
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	726	\begin{frame}[c]
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	727	\frametitle{\begin{tabular}{c}Proofs about Strings (2)\end{tabular}}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	728
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	729	We can finally prove
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	730
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	731	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	732	\bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$}
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	733	\end{center}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	734
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	735
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	736	\end{frame}}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	737	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	738
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	739	\end{document}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	740
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	741	%%% Local Variables:
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	742	%%% mode: latex
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	743	%%% TeX-master: t
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	744	%%% End:
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	745

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 17 Apr 2015 04:56:30 +0100 (2015-04-17)
changeset 324	6cb517754d8a
parent 263	92e6985018ae
child 325	794c599cee53
permissions	-rw-r--r--