afl-material: slides/slides02.tex@2d112a7b29eb (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]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	48	\frametitle{\begin{tabular}{@ {}c@ {}}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	49	An Efficient Regular\\[-1mm]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	50	Expression Matcher\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	51
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	52	\footnotesize
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	53	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	54	\begin{tabular}{@{}cc@{}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	55	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	56	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	57	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	58	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	59	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	60	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	61	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	62	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	63	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	64	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	65	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	66	width=4.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	67	height=4.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	68	legend entries={Python,Ruby},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	69	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	70	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	71	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	72	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	73	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	74	\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	75	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	76	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	77	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	78	&
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	79	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	80	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	81	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	82	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	83	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	84	xtick={0,3000,...,12000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	85	xmax=12000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	86	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	87	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	88	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	89	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	90	width=5.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	91	height=4.5cm
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	92	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	93	\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	94	\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	95	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	96	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	97	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	98	\end{center}
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
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	101	\end{frame}
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	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	106	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	107	\frametitle{Languages}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	108
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	109	\begin{itemize}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	110
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	111	\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	112	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	113	\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	114	\end{center}\bigskip
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	115
332 4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	116	\item \alert{\bf Concatenation} of strings and languages
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	117
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	118	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	119	\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	120	\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	121	\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	122	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	123	\end{center}
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	124	\bigskip
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	125
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	126	\small
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	127	\item [] For example \bl{$A = \{foo, bar\}$}, \bl{$B = \{a, b\}$}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	128
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	129	\[
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	130	\bl{A \,@\, B = \{fooa, foob, bara, barb\}}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	131	\]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	132
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	133	\end{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	134
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	135	\end{frame}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	136	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	137
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	138	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	139	\begin{frame}[c]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	140	\frametitle{The Power Operation}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	141
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	142	\begin{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	143	\item The \alert{\bf Power} of a language:
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	144
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	145	\begin{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	146	\begin{tabular}{lcl}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	147	\bl{$A^0$} & \bl{$\dn$} & \bl{$\{[]\}$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	148	\bl{$A^{n+1}$} & \bl{$\dn$} & \bl{$A \,@\, A^n$}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	149	\end{tabular}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	150	\end{center}\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	151
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	152	\item[] For example
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	153
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	154	\begin{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	155	\begin{tabular}{l}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	156	\bl{$A^4 = A \,@\, A \,@\, A \,@\, A$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	157	\bl{$A^0 \dn \{[]\}$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	158	\end{tabular}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	159	\end{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	160
261 24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	161	\end{itemize}
24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 diff changeset	162
24531cfaa36a updated handouts Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 258 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
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	166	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	167	\begin{frame}[c]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	168	\frametitle{The Star Operation}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	169
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	170	\begin{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	171	\item The \alert{\bf Star} of a \underline{language}:
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	172	\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	173
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	174	\begin{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	175	\begin{tabular}{c}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	176	\bl{$A^* \dn \bigcup_{0\le n} A^n$}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	177	\end{tabular}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	178	\end{center}\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	179
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	180	\item[] This expands to
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	181
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	182	\[
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	183	\bl{A^0 \cup A^1 \cup A^2 \cup A^3 \cup A^4 \cup \ldots}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	184	\]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	185
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	186	\small
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	187	\[
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	188	\bl{\{[]\} \;\cup\; A \;\cup\; A\,@\,A \;\cup\;
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	189	A\,@\,A\,@\,A \;\cup\; A\,@\,A\,@\,A\,@\,A \cup \ldots}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	190	\]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	191
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	192	\end{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	193
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	194	\end{frame}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	195	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	196
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	197	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	198	\begin{frame}[c]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	199	\frametitle{Semantic Derivative}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	200
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	201	\begin{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	202	\item The \alert{\bf Semantic Derivative} of a
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	203	\underline{language}\\ wrt to a character \bl{$c$}:
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	204	\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	205
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	206	\begin{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	207	\bl{$Der\,c\,A \dn \{ s \;\|\; c\!::\!s \in A\}$ }
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	208	\end{center}\bigskip\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	209
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	210	For \bl{$A = \{\textit{foo}, \textit{bar}, \textit{frak}\}$} then
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	211
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	212	\begin{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	213	\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	214	$Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	215	$Der\,b\,A$ & $=$ & $\{\textit{ar}\}$\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	216	$Der\,a\,A$ & $=$ & $\varnothing$\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	217	\end{tabular}}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	218	\end{center}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	219
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	220	\end{itemize}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	221
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	222	\end{frame}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	223	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	224
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	225	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	226	\begin{frame}[t]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	227	\frametitle{Regular Expressions}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	228
15 f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	229	Their inductive definition:
f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	230
f5a6270adebc tuning Christian Urban <urbanc@in.tum.de> parents: 11 diff changeset	231
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	232	\begin{textblock}{6}(2,7.5)
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	233	\begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	234	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	235	& \bl{$\mid$} & \bl{$\epsilon$} & empty string / \pcode{""} / $[]$\\
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	236	& \bl{$\mid$} & \bl{$c$} & character\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	237	& \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	238	& \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	239	& \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	240	\end{tabular}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	\end{textblock}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	242
332 4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	243
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	244	\end{frame}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	245	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	246
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	247
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	248	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	249	\begin{frame}[c]
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	250	\frametitle{\begin{tabular}{c}The Meaning of a\\[-2mm] Regular Expression\end{tabular}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	251
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	252	\begin{textblock}{15}(1,4)
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	253	\begin{tabular}{@ {}rcl}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	254	\bl{$L(\varnothing)$} & \bl{$\dn$} & \bl{$\varnothing$}\\
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	255	\bl{$L(\epsilon)$} & \bl{$\dn$} & \bl{$\{[]\}$}\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	256	\bl{$L(c)$} & \bl{$\dn$} & \bl{$\{[c]\}$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	257	\bl{$L(r_1 + r_2)$} & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	258	\bl{$L(r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$L(r_1) \,@\, L(r_2)$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	259	\bl{$L(r^)$} & \bl{$\dn$} & \bl{$(L(r))^$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	260	\end{tabular}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	261	\end{textblock}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	262
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	263	\begin{textblock}{6}(9,12)\small
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	264	\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	265	\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	266	\end{textblock}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	267
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	268	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	270
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	271	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	272	\begin{frame}[c]
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	273
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	274	\large
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	275	\begin{center}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	276	What is \bl{$L(a^*)$}?
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	277	\end{center}
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	278
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	279	\end{frame}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	280	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	281
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	282	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332 4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	283	\begin{frame}[c]
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	284	\frametitle{\begin{tabular}{c}
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	285	When Are Two Regular\\[-1mm]
332 4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	286	Expressions Equivalent?\end{tabular}}
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	287	\large
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	288	\begin{center}
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	289	\bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	290	\end{center}
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	291
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	292	\end{frame}
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	293	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	294
4755ad4b457b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 325 diff changeset	295	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	296	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	297	\frametitle{\begin{tabular}{c}Concrete Equivalences\end{tabular}}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	298
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	299	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	300	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	301	$(a + b) + c$ & $\equiv$ & $a + (b + c)$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	302	$a + a$ & $\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	303	$a + b$ & $\equiv$ & $b + a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	304	$(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	305	$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	306	$a \cdot a$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	307	$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	308	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	309	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	310
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	311	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	312	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	313
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	314	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	315	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	316	\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	317
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	318	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	319	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	320	$a \cdot \varnothing$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	321	$a + \epsilon$ & $\not\equiv$ & $a$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	322	$\epsilon$ & $\equiv$ & $\varnothing^*$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	323	$\epsilon^*$ & $\equiv$ & $\epsilon$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	324	$\varnothing^*$ & $\not\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	325	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	326	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	327
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	328	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	329	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	330
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	331	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	332	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	333	\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	334
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	335	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	336	\bl{\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	337	$r + \varnothing$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	338	$\varnothing + r$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	339	$r \cdot \epsilon$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	340	$\epsilon \cdot r$ & $\equiv$ & $r$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	341	$r \cdot \varnothing$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	342	$\varnothing \cdot r$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	343	$r + r$ & $\equiv$ & $r$
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	344	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	345	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	346
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	347	\end{frame}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	348	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	349
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	350	%\newcommand{\YES}{\textcolor{gray}{yes}}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	351	%\newcommand{\NO}{\textcolor{gray}{no}}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	352	%\newcommand{\FORALLR}{\textcolor{gray}{$\forall$ r.}}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	353
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	354	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	355	\begin{frame}[c]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	356	\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	357
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	358	\large
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	359	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	360
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	361	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	362	\bl{$s \in L(r)$}\\
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	363	\end{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	364
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	365	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	370	\frametitle{\bl{$(a?\{n\}) \cdot a\{n\}$}}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	371
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	372	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	373	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	374	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	375	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	376	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	377	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	378	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	379	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	380	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	381	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	382	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	383	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	384	width=9cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	385	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	386	legend entries={Python,Ruby},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	387	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	388	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	389	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	390	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	391	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	392	\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	393	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	394	\end{axis}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	395	\end{tikzpicture}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	396	\end{center}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	397
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	398	\end{frame}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	399	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	400
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	401	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
118 6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	402	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	403	\frametitle{Evil Regular Expressions}
118 6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	404
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	405	\begin{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	406	\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	407	\item Evil regular expressions\medskip
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	408	\begin{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	409	\item \bl{$(a?\{n\}) \cdot a\{n\}$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	410	\item \bl{$(a^+)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	411	\item \bl{$([a$\,-\,$z]^+)^*$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	412	\item \bl{$(a + a \cdot a)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	413	\item \bl{$(a + a?)^+$}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	414	\end{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	415	\end{itemize}
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	416
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	417	\end{frame}
118 6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	418	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	419
6a5b59690f7d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 117 diff changeset	420	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	421	\begin{frame}[t]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	422	\frametitle{A Matching Algorithm}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	423
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	424
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	425	\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	426	\begin{center}
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	427	\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	428	\bl{$nullable(\varnothing)$} & \bl{$\dn$} & \bl{\textit{false}}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	429	\bl{$nullable(\epsilon)$} & \bl{$\dn$} & \bl{\textit{true}}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	430	\bl{$nullable (c)$} & \bl{$\dn$} & \bl{\textit{false}}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	431	\bl{$nullable (r_1 + r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	432	\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	433	\bl{$nullable (r^*)$} & \bl{$\dn$} & \bl{\textit{true}}\\
117 25999de692b2 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	434	\end{tabular}
16 32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	435	\end{center}
32d56fef14a7 tuned Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	436
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	437	\end{frame}
11 5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	438	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	439
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	440
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	441	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2 Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	442	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	443	\frametitle{The Derivative of a Rexp}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	444
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	445	\large
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	446	If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	447	expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	448
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	449	\small
325 794c599cee53 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	450	\bl{$der\,c\,r$} gives the answer, Brzozowski 1964
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	451	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	452	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	453
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	454	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	455	\mode<presentation>{
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	456	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	457	\frametitle{The Derivative of a Rexp}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	458
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	459	\begin{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	460	\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	461	\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	462	\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	463	\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	464	\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	465	\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	466	& & \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	467	& & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	468	\bl{$der\, c\, (r^)$} & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^)$} &\bigskip\\\pause
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	469
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	470	\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	471	\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	472	\end{tabular}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	473	\end{center}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	474
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	475	\end{frame}}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	476	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	477
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	478	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	479	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	480	\frametitle{Examples}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	481
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	482	Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	483
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	484	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	485	\begin{tabular}{l}
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	486	\bl{$der\,a\,r =\;?$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	487	\bl{$der\,b\,r =\;?$}\\
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	488	\bl{$der\,c\,r =\;?$}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	489	\end{tabular}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	490	\end{center}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	491
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	492	\end{frame}
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	493	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	494
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	495	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	496	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	497	\begin{frame}[t]
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	498	\frametitle{The Algorithm}
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}{@{}rll@{}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	502	Input: & \bl{$r_1$}, \bl{$abc$}\medskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	503	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	504	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	505	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	506	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	507	& whether \bl{$r_4$} can recognise\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	508	& the empty string\smallskip\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	509	Output: & result of the test\\
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	510	& $\Rightarrow \bl{\textit{true}} \,\text{or}\,
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	511	\bl{\textit{false}}$\\
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	512	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	513	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	514
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	515
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	516	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	517	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	518
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	519	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	520	\begin{frame}[c]
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	521	\frametitle{The Idea of the Algorithm}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	522
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	523	If we want to recognise the string \bl{$abc$} with regular
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	524	expression \bl{$r_1$} then\medskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	525
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	526	\begin{enumerate}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	527	\item \bl{$Der\,a\,(L(r_1))$}\pause
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	528	\item \bl{$Der\,b\,(Der\,a\,(L(r_1)))$}\pause
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	529	\item \bl{$Der\,c\,(Der\,b\,(Der\,a\,(L(r_1))))$}\bigskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	530	\item finally we test whether the empty string is in this set\medskip
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	531	\end{enumerate}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	532
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	533	The matching algorithm works similarly, just over regular expressions instead of sets.
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	534	\end{frame}
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	535	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	536
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	537
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	538	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	539	\begin{frame}[c]
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	540	\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	541
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	542	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	543	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	544	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	545	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	546	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	547	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	548	xtick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	549	xmax=30,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	550	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	551	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	552	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	553	width=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	554	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	555	legend entries={Python,Ruby,Scala V1},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	556	legend pos=outer north east,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	557	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	558	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	559	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	560	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	561	\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	562	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	563	\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	564	table {re1.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	565	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	566	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	567	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	568
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	569	\end{frame}
263 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	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	574	\frametitle{A Problem}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	575
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	576	We represented the ``n-times'' \bl{$a\{n\}$} as a
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	577	sequence regular expression:
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	578
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	579	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	580	\begin{tabular}{rl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	581	1: & \bl{$a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	582	2: & \bl{$a\cdot a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	583	3: & \bl{$a\cdot a\cdot a$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	584	& \ldots\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	585	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	586	& \ldots\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	587	20:
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	588	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	589	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	590
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	591	This problem is aggravated with \bl{$a?$} being represented
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	592	as \bl{$\epsilon + a$}.
2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	593	\end{frame}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	594	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	595
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	596	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	597	\begin{frame}[c]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	598	\frametitle{Solving the Problem}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	599
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	600	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	601
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	602	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	603	\begin{tabular}{rcl}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	604	\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	605	& \bl{$\mid$} & \bl{$r\{n\}$}\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	606	& \bl{$\mid$} & \bl{$r?$}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	607	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	608	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	609
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	610	What is their meaning? What are the cases for \bl{$nullable$} and \bl{$der$}?
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	611	\end{frame}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	612	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	613
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	614
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	615	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	616	\begin{frame}[t]
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	617	\frametitle{\bl{$(a?\{n\}) \cdot a\{n\}$}}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	618
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	619	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	620	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	621	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	622	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	623	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	624	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	625	xtick={0,200,...,1000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	626	xmax=1000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	627	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	628	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	629	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	630	width=9.5cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	631	height=7cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	632	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	633	legend pos=north west,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	634	legend cell align=left
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	635	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	636	\addplot[blue,mark=*, mark options={fill=white}]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	637	table {re-python.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	638	\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	639	table {re-ruby.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	640	\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	641	table {re1.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	642	\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	643	table {re2b.data};
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	644	\end{axis}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	645	\end{tikzpicture}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	646	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	647
335 2d112a7b29eb updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 332 diff changeset	648	\end{frame}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	649	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	650
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	651
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	652	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	653	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	654	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	655	\frametitle{\begin{tabular}{c}Examples\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	656
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	657	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	658
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	659	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	660	\begin{tabular}{l}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	661	\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	662	\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	663	\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	664	\end{tabular}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	665	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	666
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	667	What are these regular expressions equivalent to?
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	668
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	669	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	670	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	671
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	672
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	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	676	\begin{frame}[t]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	677	\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	678
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	679	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	680	\begin{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	681	\begin{axis}[
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	682	xlabel={\pcode{a}s},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	683	ylabel={time in secs},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	684	enlargelimits=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	685	xtick={0,3000,...,12000},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	686	xmax=12000,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	687	ymax=35,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	688	ytick={0,5,...,30},
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	689	scaled ticks=false,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	690	axis lines=left,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	691	width=9cm,
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	692	height=7cm
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	693	]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	694	\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	695	\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	696	\end{axis}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	697	\end{tikzpicture}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	698	\end{center}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	699
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	700	\end{frame}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	701	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	704	\mode<presentation>{
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	705	\begin{frame}[t]
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	706	\frametitle{\begin{tabular}{c}Proofs about Rexps\end{tabular}}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	707
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	708	Remember their inductive definition:\\[5cm]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	709
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	710	\begin{textblock}{6}(5,5)
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	711	\begin{tabular}{@ {}rrl}
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	712	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	713	& \bl{$\mid$} & \bl{$\epsilon$} \\
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	714	& \bl{$\mid$} & \bl{$c$} \\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	715	& \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	716	& \bl{$\mid$} & \bl{$r_1 + r_2$} \\
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	717	& \bl{$\mid$} & \bl{$r^*$} \\
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	718	\end{tabular}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	719	\end{textblock}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	720
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	721	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	722
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	723	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	724	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	725
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	726	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	727	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	728	\begin{frame}[c]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	729	\frametitle{\begin{tabular}{c}Proofs about Rexp (2)\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	730
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	731	\begin{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	732	\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	733	\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	734	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	735	\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	736	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	737	\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	738	holds for \bl{$r$}.
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	739	\end{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	740
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	741	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	742	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	743
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	744	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	745	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	746	\begin{frame}[c]
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	747	\frametitle{\begin{tabular}{c}Proofs about Rexp (3)\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	748
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	749	Assume \bl{$P(r)$} is the property:
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	750
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	751	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	752	\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	753	\end{center}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	754
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	755	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	756	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	757
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	758	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	759	\mode<presentation>{
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	760	\begin{frame}[c]
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	761	\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	762
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	763
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	764	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	765	\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	766	$rev(\varnothing)$ & $\dn$ & $\varnothing$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	767	$rev(\epsilon)$ & $\dn$ & $\epsilon$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	768	$rev(c)$ & $\dn$ & $c$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	769	$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	770	$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	771	$rev(r^)$ & $\dn$ & $rev(r)^$\\
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	772	\end{tabular}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	773	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	774
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	775
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	776	We can prove
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	777
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	778	\begin{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	779	\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	780	\end{center}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	781
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	782	by induction on \bl{$r$}.
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	783
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	784	\end{frame}}
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	785	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	786
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	787	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	788	\mode<presentation>{
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	789	\begin{frame}[c]
92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	790	\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	791
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	792	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	793
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	794	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	795	\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	796	\end{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	797
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	798	We can prove
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	799
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	800	\begin{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	801	\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	802	\end{center}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	803
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	804	by induction on \bl{$r$}.
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	805
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	806	\end{frame}}
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	807	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	808
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	809
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	810	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	811	\mode<presentation>{
a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	812	\begin{frame}[c]
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	813	\frametitle{\begin{tabular}{c}Proofs about Strings\end{tabular}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	814
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	815	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	816
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	817	\begin{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	818	\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	819	\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	820	already holds for \bl{$s$}
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	821	\end{itemize}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	822	\end{frame}}
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	823	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	824
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	825	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	826	\mode<presentation>{
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	827	\begin{frame}[c]
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	828	\frametitle{\begin{tabular}{c}Proofs about Strings (2)\end{tabular}}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	829
119 a6684e8961d0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 118 diff changeset	830	We can finally prove
19 f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	831
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	832	\begin{center}
263 92e6985018ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	833	\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	834	\end{center}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	835
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	836
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	837	\end{frame}}
f702fd716bd8 tuned Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	838	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
17 4d81b2dc8271 tuned Christian Urban <urbanc@in.tum.de> parents: 16 diff changeset	839
7 73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	840	\end{document}
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	841
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	842	%%% Local Variables:
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	843	%%% mode: latex
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	844	%%% TeX-master: t
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	845	%%% End:
73cf4406b773 updated Christian Urban <urbanc@in.tum.de> parents: diff changeset	846

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 01 Oct 2015 22:10:00 +0100
changeset 335	2d112a7b29eb
parent 332	4755ad4b457b
child 336	7c80b9b6f713
permissions	-rw-r--r--