afl-material: slides/slides05.tex@c22c8baff491 (annotated)

44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
270 4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	2	\usepackage{../slides}
4dbeaf43031d updated 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: 169 diff changeset	4	\usepackage{../langs}
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 169 diff changeset	5	\usepackage{../data}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
270 4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	7	\hfuzz=220pt
4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	8
4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	9	\pgfplotsset{compat=1.11}
4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	10
4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	11	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	% beamer stuff
270 4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	14	\renewcommand{\slidecaption}{AFL 05, King's College London}
4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	15
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	\begin{document}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
270 4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	20	\begin{frame}[t]
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	\frametitle{%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\begin{tabular}{@ {}c@ {}}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\\[-3mm]
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\LARGE Automata and \\[-2mm]
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\LARGE Formal Languages (5)\\[3mm]
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	\end{tabular}}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	\normalsize
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	\begin{center}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	\begin{tabular}{ll}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	Email: & christian.urban at kcl.ac.uk\\
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	32	Office: & S1.27 (1st floor Strand Building)\\
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	Slides: & KEATS (also home work is there)\\
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	\end{tabular}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	\end{center}
270 4dbeaf43031d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	36	\end{frame}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	37	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	40	\begin{frame}[c]
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	41	\frametitle{\begin{tabular}{c}Last Week\\ Regexes and Values\end{tabular}}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	42
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	43	Regular expressions and their corresponding values:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	44
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	45	\begin{center}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	46	\begin{columns}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	47	\begin{column}{3cm}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	48	\begin{tabular}{@{}rrl@{}}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	49	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	50	& \bl{$\mid$} & \bl{$\epsilon$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	51	& \bl{$\mid$} & \bl{$c$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	52	& \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	53	& \bl{$\mid$} & \bl{$r_1 + r_2$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	54	\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	55	& \bl{$\mid$} & \bl{$r^*$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	56	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	57	\end{column}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	58	\begin{column}{3cm}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	59	\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	60	\bl{$v$} & \bl{$::=$} & \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	61	& & \bl{$Empty$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	62	& \bl{$\mid$} & \bl{$Char(c)$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	63	& \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	64	& \bl{$\mid$} & \bl{$Left(v)$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	65	& \bl{$\mid$} & \bl{$Right(v)$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	66	& \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	67	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	68	\end{column}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	69	\end{columns}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	70	\end{center}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	71
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	72
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	73	\end{frame}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	74	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	75
4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	76
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	77
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	78	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
272 1446bc47a294 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 270 diff changeset	79	\begin{frame}[c]
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	80
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	81	\begin{textblock}{10}(3,5)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	82	\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	83	\node (r1) {\bl{$r_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	84	\node (r2) [right=of r1] {\bl{$r_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	85	\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	86	\node (r3) [right=of r2] {\bl{$r_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	87	\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	88	\node (r4) [right=of r3] {\bl{$r_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	89	\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	90	\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	91	\node (v4) [below=of r4] {\bl{$v_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	92	\draw[->,line width=1mm] (r4) -- (v4);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	93	\node (v3) [left=of v4] {\bl{$v_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	94	\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	95	\node (v2) [left=of v3] {\bl{$v_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	96	\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	97	\node (v1) [left=of v2] {\bl{$v_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	98	\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	99	\draw[->,line width=0.5mm] (r3) -- (v3);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	100	\draw[->,line width=0.5mm] (r2) -- (v2);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	101	\draw[->,line width=0.5mm] (r1) -- (v1);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	102	\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	103	\end{tikzpicture}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	104	\end{textblock}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	105
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	106	\only<2->{
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	107	\begin{textblock}{6}(1,0.8)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	108	\begin{bubble}[6cm]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	109	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	110	\begin{tabular}{ll}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	111	\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	112	\bl{$r_2$}: & \bl{$\epsilon \cdot (b \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	113	\bl{$r_3$}: & \bl{$(\varnothing \cdot (b \cdot c)) + (\epsilon \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	114	\bl{$r_4$}: & \bl{$(\varnothing \cdot (b \cdot c)) + ((\varnothing \cdot c) + \epsilon)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	115	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	116	\end{bubble}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	117	\end{textblock}}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	118
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	119	\only<2->{
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	120	\begin{textblock}{6}(5,11.4)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	121	\begin{bubble}[7.6cm]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	122	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	123	\begin{tabular}{ll}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	124	\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	125	\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	126	\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	127	\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	128	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	129	\end{bubble}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	130	\end{textblock}}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	131	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	132	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	133
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	134	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	135	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	136	\frametitle{Mkeps}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	137
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	138	Finding a (posix) value for recognising the empty string:
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	139
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	\begin{center}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	141	\begin{tabular}{lcl}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	142	\bl{$mkeps\,\epsilon$} & \bl{$\dn$} & \bl{$Empty$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	143	\bl{$mkeps\,r_1 + r_2$} & \bl{$\dn$} & \bl{if $nullable(r_1)$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	144	& & \bl{then $Left(mkeps(r_1))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	145	& & \bl{else $Right(mkeps(r_2))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	146	\bl{$mkeps\,r_1 \cdot r_2$} & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),mkeps(r_2))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	147	\bl{$mkeps\,r^*$} & \bl{$\dn$} & \bl{$[]$} \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	148	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	149	\end{center}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	150
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	151	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	152	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	153
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	154	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	155	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	156	\frametitle{Inject}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	157
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	158	Injecting (``Adding'') a character to a value\\
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	159
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	160	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	161	\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	162	\bl{$inj\,(c)\,c\,Empty$} & \bl{$\dn$} & \bl{$Char\,c$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	163	\bl{$inj\,(r_1 + r_2)\,c\,Left(v)$} & \bl{$\dn$} & \bl{$Left(inj\,r_1\,c\,v)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	164	\bl{$inj\,(r_1 + r_2)\,c\,Right(v)$} & \bl{$\dn$} & \bl{$Right(inj\,r_2\,c\,v)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	165	\bl{$inj\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$} & \bl{$\dn$} & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	166	\bl{$inj\,(r_1 \cdot r_2)\,c\,Left(Seq(v_1,v_2))$} & \bl{$\dn$} & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	167	\bl{$inj\,(r_1 \cdot r_2)\,c\,Right(v)$} & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	168	\bl{$inj\,(r^*)\,c\,Seq(v,vs)$} & \bl{$\dn$} & \bl{$inj\,r\,c\,v\,::\,vs$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	169	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	170	\end{center}\bigskip
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	171
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	172	\footnotesize
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	173	\bl{$inj$}: 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 3rd arg $\mapsto$ a value
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	174	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	175	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	176
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	177	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	178	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	179	\frametitle{Flatten}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	180
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	181	Obtaining the string underlying a value:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	182
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	183	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	184	\begin{tabular}{lcl}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	185	\bl{$\|Empty\|$} & \bl{$\dn$} & \bl{$[]$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	186	\bl{$\|Char(c)\|$} & \bl{$\dn$} & \bl{$[c]$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	187	\bl{$\|Left(v)\|$} & \bl{$\dn$} & \bl{$\|v\|$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	188	\bl{$\|Right(v)\|$} & \bl{$\dn$} & \bl{$\|v\|$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	189	\bl{$\|Seq(v_1,v_2)\|$}& \bl{$\dn$} & \bl{$\|v_1\| \,@\, \|v_2\|$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	190	\bl{$\|[v_1,\ldots ,v_n]\|$} & \bl{$\dn$} & \bl{$\|v_1\| \,@\ldots @\, \|v_n\|$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	191	\end{tabular}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	192	\end{center}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	193
272 1446bc47a294 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 270 diff changeset	194	\end{frame}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	196
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	197	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
272 1446bc47a294 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 270 diff changeset	198	\begin{frame}[c]
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	199
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	200	\begin{textblock}{10}(3,5)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	201	\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	202	\node (r1) {\bl{$r_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	203	\node (r2) [right=of r1] {\bl{$r_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	204	\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	205	\node (r3) [right=of r2] {\bl{$r_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	206	\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	207	\node (r4) [right=of r3] {\bl{$r_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	208	\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	209	\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	210	\node (v4) [below=of r4] {\bl{$v_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	211	\draw[->,line width=1mm] (r4) -- (v4);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	212	\node (v3) [left=of v4] {\bl{$v_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	213	\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	214	\node (v2) [left=of v3] {\bl{$v_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	215	\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	216	\node (v1) [left=of v2] {\bl{$v_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	217	\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	218	\draw[->,line width=0.5mm] (r3) -- (v3);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	219	\draw[->,line width=0.5mm] (r2) -- (v2);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	220	\draw[->,line width=0.5mm] (r1) -- (v1);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	221	\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	222	\end{tikzpicture}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	223	\end{textblock}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	224
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	225	\begin{textblock}{6}(1,0.8)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	226	\begin{bubble}[6cm]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	227	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	228	\begin{tabular}{ll}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	229	\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	230	\bl{$r_2$}: & \bl{$\epsilon \cdot (b \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	231	\bl{$r_3$}: & \bl{$(\varnothing \cdot (b \cdot c)) + (\epsilon \cdot c)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	232	\bl{$r_4$}: & \bl{$(\varnothing \cdot (b \cdot c)) + ((\varnothing \cdot c) + \epsilon)$}\\
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	233	\end{tabular}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	234	\end{bubble}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	235	\end{textblock}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	236
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	237	\begin{textblock}{6}(1,11.4)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	238	\begin{bubble}[7.6cm]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	239	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	240	\begin{tabular}{ll}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	241	\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	242	\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	243	\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	244	\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	245	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	246	\end{bubble}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	247	\end{textblock}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	248
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	249	\begin{textblock}{6}(12,11.4)
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	250	\begin{bubble}[2cm]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	251	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	252	\begin{tabular}{ll}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	253	\bl{$\|v_1\|$}: & \bl{$abc$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	254	\bl{$\|v_2\|$}: & \bl{$bc$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	255	\bl{$\|v_3\|$}: & \bl{$c$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	256	\bl{$\|v_4\|$}: & \bl{$[]$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	257	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	258	\end{bubble}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	259	\end{textblock}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	260
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	261
272 1446bc47a294 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 270 diff changeset	262	\end{frame}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	264
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	265	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	266	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	267	\frametitle{Simplification}
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	268
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	269	\begin{itemize}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	270	\item If we simplify after the derivative, then we are builing the
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	271	value for the simplified regular expression, but \emph{not} for the original
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	272	regular expression.
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	273	\end{itemize}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	274
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	275	\begin{center}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	276	\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	277	\node (r1) {\bl{$r_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	278	\node (r2) [right=of r1] {\bl{$r_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	279	\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	280	\node (r3) [right=of r2] {\bl{$r_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	281	\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	282	\node (r4) [right=of r3] {\bl{$r_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	283	\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	284	\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	285	\node (v4) [below=of r4] {\bl{$v_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	286	\draw[->,line width=1mm] (r4) -- (v4);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	287	\node (v3) [left=of v4] {\bl{$v_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	288	\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	289	\node (v2) [left=of v3] {\bl{$v_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	290	\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	291	\node (v1) [left=of v2] {\bl{$v_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	292	\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	293	\draw[->,line width=0.5mm] (r3) -- (v3);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	294	\draw[->,line width=0.5mm] (r2) -- (v2);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	295	\draw[->,line width=0.5mm] (r1) -- (v1);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	296	\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
147 4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	297	\end{tikzpicture}
4725bba8ef26 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	298	\end{center}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	299
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	300	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	301	\hspace{4.5cm}\bl{$(\varnothing \cdot (b \cdot c)) + ((\varnothing \cdot c) + \epsilon)$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	302	$\mapsto$
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	303	\bl{$\epsilon$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	304
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	305	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	306	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	307
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	308	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	309	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	310	\frametitle{Rectification}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	311
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	312	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	313	\begin{tabular}{l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	314	\bl{$simp(r)$}:\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	315	\quad case \bl{$r = r_1 + r_2$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	316	\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	317	\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	318	\qquad case \bl{$r_{1s} = \varnothing$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	319	return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	320	\qquad case \bl{$r_{2s} = \varnothing$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	321	return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	322	\qquad case \bl{$r_{1s} = r_{2s}$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	323	return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	324	\qquad otherwise:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	325	return \bl{$(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	326	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	327	\end{center}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	328
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	329	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	330	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	331	\begin{tabular}{l@{\hspace{1mm}}l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	332	\bl{$f_{alt}(f_1, f_2) \dn$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	333	\qquad \bl{$\lambda v.\,$} case \bl{$v = Left(v')$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	334	& return \bl{$Left(f_1(v'))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	335	\qquad \phantom{$\lambda v.\,$} case \bl{$v = Right(v')$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	336	& return \bl{$Right(f_2(v'))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	337	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	338	\end{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	339
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	340
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	341	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	342	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	343
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	344	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	345	\begin{frame}[c]
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	346	\frametitle{Rectification}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	347
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	348	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	349	\begin{tabular}{@{\hspace{-3mm}}l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	350	\bl{$simp(r)$}:\ldots\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	351	\quad case \bl{$r = r_1 \cdot r_2$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	352	\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	353	\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	354	\qquad case \bl{$r_{1s} = \varnothing$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	355	return \bl{$(\varnothing, f_{error})$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	356	\qquad case \bl{$r_{2s} = \varnothing$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	357	return \bl{$(\varnothing, f_{error})$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	358	\qquad case \bl{$r_{1s} = \epsilon$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	359	return \bl{$(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	360	\qquad case \bl{$r_{2s} = \epsilon$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	361	return \bl{$(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	362	\qquad otherwise:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	363	return \bl{$(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	364	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	365	\end{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	366
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	367	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	368	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	369	\begin{tabular}{l@{\hspace{1mm}}l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	370	\bl{$f_{seq}(f_1, f_2) \dn$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	371	\qquad \bl{$\lambda v.\,$ case $v = Seq(v_1, v_2)$}:
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	372	& return \bl{$Seq(f_1(v_1), f_2(v_2))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	373	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	374	\end{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	375	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	376	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	377
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	378	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	379	\begin{frame}[c]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	380	\frametitle{Lexing with Simplification}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	381
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	382	\begin{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	383	\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	384	\bl{$lex\,r\,[]$} & \bl{$\dn$} & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	385	\bl{$lex\,r\,c::s$} & \bl{$\dn$} & \bl{let $(r', frect) = simp(der(c, r))$}\smallskip\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	386	& & \bl{$inj\,r\,c\,(frect(lex(r', s)))$}\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	387	\end{tabular}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	388	\end{center}\bigskip
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	389
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	390	\begin{center}\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	391	\begin{tikzpicture}[node distance=1.1cm,every node/.style={minimum size=7mm}]
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	392	\node (r1) {\bl{$r_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	393	\node (r2) [right=of r1] {\bl{$r_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	394	\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	395	\node (r3) [right=of r2] {\bl{$r_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	396	\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	397	\node (r4) [right=of r3] {\bl{$r_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	398	\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	399	\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	400	\node (v4) [below=of r4] {\bl{$v_4$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	401	\draw[->,line width=1mm] (r4) -- (v4);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	402	\node (v3) [left=of v4] {\bl{$v_3$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	403	\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	404	\node (v2) [left=of v3] {\bl{$v_2$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	405	\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	406	\node (v1) [left=of v2] {\bl{$v_1$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	407	\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	408	\draw[->,line width=0.5mm] (r3) -- (v3);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	409	\draw[->,line width=0.5mm] (r2) -- (v2);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	410	\draw[->,line width=0.5mm] (r1) -- (v1);
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	411	\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	412	\end{tikzpicture}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	413	\end{center}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	414
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	415
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	416	\end{frame}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	417	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	418
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	419	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	\begin{frame}[c]
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	421	\frametitle{Records}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	422
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	423	\begin{itemize}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	424	\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	425
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	426	\item \bl{$nullable(x:r) \dn nullable(r)$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	427	\item \bl{$der\,c\,(x:r) \dn (x:der\,c\,r)$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	428	\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	429	\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	430	\end{itemize}\bigskip\bigskip\pause
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	431
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	432	\small
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	433	for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	434
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	435	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	436	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
46 a97a6de47c28 tuned Christian Urban <urbanc@in.tum.de> parents: 44 diff changeset	437
148 36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	438	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	439	\begin{frame}[c]
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	440	\frametitle{While Tokens}
150 a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	441
148 36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	442	\begin{center}
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	443	\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	444	\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	445	& & \phantom{(}\pcode{("i" : ID)} +\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	446	& & \phantom{(}\pcode{("o" : OP)} + \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	447	& & \phantom{(}\pcode{("n" : NUM)} + \\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	448	& & \phantom{(}\pcode{("s" : SEMI)} +\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	449	& & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	450	& & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	451	& & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	452	\end{tabular}
148 36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	453	\end{center}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	454
289 c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	455	\end{frame}
c22c8baff491 updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 272 diff changeset	456	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
148 36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	457
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	458	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	459	\mode<presentation>{
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	460	\begin{frame}[t]
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	461
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	462	\consolas
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	463	\begin{center}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	464	"if true then then 42 else +"
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	465	\end{center}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	466
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	467	\only<1>{
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	468	\small\begin{tabular}{l}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	469	KEYWORD(if),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	470	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	471	IDENT(true),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	472	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	473	KEYWORD(then),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	474	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	475	KEYWORD(then),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	476	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	477	NUM(42),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	478	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	479	KEYWORD(else),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	480	WHITESPACE,\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	481	OP(+)
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	482	\end{tabular}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	483
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	484	\only<2>{
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	485	\small\begin{tabular}{l}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	486	KEYWORD(if),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	487	IDENT(true),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	488	KEYWORD(then),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	489	KEYWORD(then),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	490	NUM(42),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	491	KEYWORD(else),\\
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	492	OP(+)
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	493	\end{tabular}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	494
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	495	\end{frame}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	496	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	497
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	498	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	499	\mode<presentation>{
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	500	\begin{frame}[c]
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	501
150 a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	502
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	503	There is one small problem with the tokenizer. How should we
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	504	tokenize:
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	505
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	506	\begin{center}
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	507	{\consolas "x - 3"}
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	508	\end{center}
149 b728c9dbf120 add Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	509
150 a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	510	\consolas
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	511	\begin{tabular}{@{}l}
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	512	OP:\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	513	\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	514	NUM:\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	515	\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {''0''}\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	516	NUMBER:\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	517	\hspace{5mm}NUM + (\texttt{"-"} $\cdot$ NUM)\\
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	518	\end{tabular}
149 b728c9dbf120 add Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	519
148 36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	520
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	521	\end{frame}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	522	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	523
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	524	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	525	\mode<presentation>{
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	526	\begin{frame}[c]
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	527	\frametitle{\begin{tabular}{c}Two Rules\end{tabular}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	528
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	529	\begin{itemize}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	530	\item Longest match rule (``maximal munch rule''): The
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	531	longest initial substring matched by any regular expression is taken
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	532	as next token.\bigskip
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	533
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	534	\item Rule priority:
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	535	For a particular longest initial substring, the first regular
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	536	expression that can match determines the token.
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	537
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	538	\end{itemize}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	539
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	540	%\url{http://www.technologyreview.com/tr10/?year=2011}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	541
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	542	%finite deterministic automata/ nondeterministic automaton
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	543
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	544	%\item problem with infix operations, for example i-12
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	545
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	546
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	547	\end{frame}}
36eb7bfb0e63 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 147 diff changeset	548	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
150 a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	549
a2d792ed768e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 149 diff changeset	550
44 3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	551	\end{document}
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	552
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	553	%%% Local Variables:
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	554	%%% mode: latex
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	555	%%% TeX-master: t
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	556	%%% End:
3840d09e4271 added Christian Urban <urbanc@in.tum.de> parents: diff changeset	557

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 20 Oct 2014 00:10:57 +0100
changeset 289	c22c8baff491
parent 272	1446bc47a294
child 290	3a2fa69ea675
permissions	-rw-r--r--