afl-material: slides/slides03.tex@332fbe9c91ab (annotated)

25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	2	\usepackage{../slides}
332fbe9c91ab added slides 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: 143 diff changeset	4	\usepackage{../langs}
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	5	\usepackage{../data}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	7	\hfuzz=220pt
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	8
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	9	\pgfplotsset{compat=1.11}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	10
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	11	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	% beamer stuff
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	14	\renewcommand{\slidecaption}{AFL 03, King's College London}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	\begin{document}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	19	\begin{frame}[t]
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	\frametitle{%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	\begin{tabular}{@ {}c@ {}}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\\[-3mm]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\LARGE Automata and \\[-2mm]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\LARGE Formal Languages (3)\\[3mm]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\end{tabular}}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	\normalsize
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	\begin{center}
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	29	\begin{tabular}{lp{8cm}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	Email: & christian.urban at kcl.ac.uk\\
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	31	Office: & S1.27 (1st floor Strand Building)\\
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	32	Slides: & KEATS (also home work and coursework is there)\\
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	\end{tabular}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	\end{center}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	36	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	\begin{frame}[c]
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	41	\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	42
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	43	In programming languages they are often used to recognise:\medskip
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	\begin{itemize}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	46	\item symbols, digits
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	47	\item identifiers
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	48	\item numbers (non-leading zeros)
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	49	\item keywords
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	50	\item comments
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	51	\end{itemize}\bigskip
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	52
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	53	\mbox{}\hfill\bl{\url{http://www.regexper.com}}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	54	\end{frame}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	55	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	56
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	57
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	58	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	59	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	60	\frametitle{Last Week}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	61
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	62	Last week I showed you a regular expression matcher
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	63	which works provably correct in all cases (we did not
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	64	do the proving part though)
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	65
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	\begin{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	67	\bl{$matches\,r\,s$} \;\;if and only if \;\; \bl{$s \in L(r)$}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	68	\end{center}\bigskip\bigskip
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	69
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	70	\small
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	71	\textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	72
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	73	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	75
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	78	\frametitle{The Derivative of a Rexp}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	79
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	\begin{center}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	82	\bl{$der\, c\, (\varnothing)$} & \bl{$\dn$} & \bl{$\varnothing$} & \\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	83	\bl{$der\, c\, (\epsilon)$} & \bl{$\dn$} & \bl{$\varnothing$} & \\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	84	\bl{$der\, c\, (d)$} & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	85	\bl{$der\, c\, (r_1 + r_2)$} & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	86	\bl{$der\, c\, (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{if $nullable (r_1)$}\\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	87	& & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	88	& & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	89	\bl{$der\, c\, (r^)$} & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^)$} &\medskip\\
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	90
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	91	\bl{$\textit{ders}\, []\, r$} & \bl{$\dn$} & \bl{$r$} & \\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	92	\bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	\end{tabular}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	\end{center}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	95
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	96	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	98
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	\begin{frame}[c]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	101
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	102	To see what is going on, define
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	103
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	\begin{center}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	105	\bl{$Der\,c\,A \dn \{ s \;\|\; c\!::\!s \in A\}$ }
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	106	\end{center}\bigskip\bigskip
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	107
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	108	For \bl{$A = \{\textit{foo}, \textit{bar}, \textit{frak}\}$} then
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	109
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	\begin{center}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	111	\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	112	$Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	113	$Der\,b\,A$ & $=$ & $\{\textit{ar}\}$\\
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	114	$Der\,a\,A$ & $=$ & $\varnothing$\\
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	115	\end{tabular}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	\end{center}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	117
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	118	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	120
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	121
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	124	\frametitle{The Idea of the Algorithm}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	125
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	126	If we want to recognise the string \bl{$abc$} with regular expression \bl{$r$}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	then\medskip
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	128
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	\begin{enumerate}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	130	\item \bl{$Der\,a\,(L(r))$}\pause
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	131	\item \bl{$Der\,b\,(Der\,a\,(L(r)))$}\pause
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	132	\item \bl{$Der\,c\,(Der\,b\,(Der\,a\,(L(r))))$}\bigskip\pause
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	133	\item finally we test whether the empty string is in this set\pause\medskip
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	\end{enumerate}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	135
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	136	The matching algorithm works similarly, just over regular expressions instead of sets.
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	137	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	139
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	140
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	\begin{frame}[c]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	143
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	144	Input: string \bl{$abc$} and regular expression \bl{$r$}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	145
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	\begin{enumerate}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	147	\item \bl{$der\,a\,r$}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	148	\item \bl{$der\,b\,(der\,a\,r)$}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	149	\item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	150	\item finally check whether the last regular expression can match the empty string
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	\end{enumerate}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	152
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	153	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	155
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	\begin{frame}[c]
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	158
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	159	We proved already
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	160
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	161	\begin{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	162	\bl{$nullable(r)$} \;if and only if\; \bl{$[] \in L(r)$}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	163	\end{center}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	164
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	165	by induction on the regular expression.\bigskip\pause
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	166
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	167	\begin{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	168	{\huge\bf\alert{Any Questions?}}
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	169	\end{center}
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	170
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	171	\end{frame}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	172	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	173
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	174	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	175	\begin{frame}[c]
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	176
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	We need to prove
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	178
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	\begin{center}
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	180	\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	\end{center}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	182
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	by induction on the regular expression.
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	184	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	186
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	187
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	188	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	189	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	190	\frametitle{Proofs about Rexps}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	191
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	\begin{itemize}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	194	\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	195	holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	196	\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	197	holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	198	\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	199	holds for \bl{$r$}.
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	\end{itemize}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	201
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	202	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	204
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	\begin{frame}[c]
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	207	\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	208
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	209	\begin{itemize}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	\item \bl{$P$} holds for \bl{$0$} and
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	211	\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	212	holds for \bl{$n$}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	\end{itemize}\bigskip
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	214
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	215	\begin{itemize}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	216	\item \bl{$P$} holds for \bl{$[]$} and
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	holds for \bl{$s$}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	\end{itemize}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	220
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	221	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	223
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	224
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	225
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	228	\frametitle{Languages}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	229
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	230	A \alert{language} is a set of strings.\bigskip
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	231
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	232	A \alert{regular expression} specifies a language.\bigskip
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	233
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	234	A language is \alert{regular} iff there exists
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	235	a regular expression that recognises all its strings.\bigskip\bigskip\pause
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	236
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	237	\textcolor{gray}{not all languages are regular, e.g.~\bl{$a^nb^n$} is not}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	238	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	240
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	242	\begin{frame}[t]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	243	\frametitle{Regular Expressions}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	244
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	245	\begin{center}
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	246	\begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	247	\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	248	& \bl{$\mid$} & \bl{$\epsilon$} & empty string / "" / $[]$\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	249	& \bl{$\mid$} & \bl{$c$} & character\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	250	& \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	251	& \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	252	& \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	253	\end{tabular}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	254	\end{center}
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	255
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	256	How about ranges \bl{$[a\mbox{-}z]$}, \bl{$r^+$} and \bl{$\sim{}r$}? Do they increase the
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	257	set of languages we can recognise?
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	258
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	259	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	260	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	261
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	264	\frametitle{Negation of Regular Expr's}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	265
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	\begin{itemize}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	267	\item \bl{$\sim{}r$} \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	268	\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	269	\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	270	\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	271	\end{itemize}\bigskip\pause
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	272
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	273	Used often for recognising comments:
134 e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	274
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	275	\[
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	276	\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^)) \cdot \cdot /}
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	277	\]
e3a8cf96f570 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	278
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	279	\end{frame}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	280	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	281
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	282	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	283	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	284	\frametitle{Negation}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	285
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	286	Assume you have an alphabet consisting of the letters \bl{$a$}, \bl{$b$} and \bl{$c$} only.
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	287	Find a (basic!) regular expression that matches all strings \emph{\alert{except}}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	288	\bl{$ab$} and \bl{$ac$}!
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	289
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	290	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	291	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	292
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	293
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	294	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	295	%\mode<presentation>{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	296	%\begin{frame}[c]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	297	%\frametitle{\begin{tabular}{c}Regular Exp's for Lexing\end{tabular}}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	298	%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	299	%Lexing separates strings into ``words'' / components.
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	300	%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	301	%\begin{itemize}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	302	%\item Identifiers (non-empty strings of letters or digits, starting with a letter)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	303	%\item Numbers (non-empty sequences of digits omitting leading zeros)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	304	%\item Keywords (else, if, while, \ldots)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	305	%\item White space (a non-empty sequence of blanks, newlines and tabs)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	306	%\item Comments
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	307	%\end{itemize}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	308	%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	309	%\end{frame}}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	310	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	311
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	312	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	313	\begin{frame}[c]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	314	\frametitle{Automata}
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	315
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	316	A \alert{deterministic finite automaton} consists of:
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	317
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	\begin{itemize}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	319	\item a set of states
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	320	\item one of these states is the start state
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	321	\item some states are accepting states, and
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	322	\item there is transition function\medskip
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	323
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	\small
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	325	which takes a state as argument and a character and produces a
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	326	new state\smallskip\\
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	327	this function might not be everywhere defined
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	328	\end{itemize}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	329
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	330	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	331	\bl{$A(Q, q_0, F, \delta)$}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	332	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	333
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	334	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	335	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	336
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	337
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	338	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	339	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	340
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	341	\begin{center}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	342	\begin{tikzpicture}[>=stealth',very thick,auto,
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	343	every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	344	\node[state,initial] (q_0) {$q_0$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	345	\node[state] (q_1) [right=of q_0] {$q_1$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	346	\node[state] (q_2) [below right=of q_0] {$q_2$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	347	\node[state] (q_3) [right=of q_2] {$q_3$};
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	348	\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	349	\path[->] (q_0) edge node [above] {\alert{$a$}} (q_1);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	350	\path[->] (q_1) edge node [above] {\alert{$a$}} (q_4);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	351	\path[->] (q_4) edge [loop right] node {\alert{$a, b$}} ();
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	352	\path[->] (q_3) edge node [right] {\alert{$a$}} (q_4);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	353	\path[->] (q_2) edge node [above] {\alert{$a$}} (q_3);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	354	\path[->] (q_1) edge node [right] {\alert{$b$}} (q_2);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	355	\path[->] (q_0) edge node [above] {\alert{$b$}} (q_2);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	356	\path[->] (q_2) edge [loop left] node {\alert{$b$}} ();
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	357	\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below] {\alert{$b$}} (q_0);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	358	\end{tikzpicture}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	359	\end{center}\pause
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	360
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	361
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	362	\begin{itemize}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	363	\item the start state can be an accepting state
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	364	\item it is possible that there is no accepting state
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	365	\item all states might be accepting (but this does not necessarily mean all strings are accepted)
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	366	\end{itemize}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	367
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	368	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	369	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	370
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	371	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	372	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	373
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	374	\begin{center}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	375	\begin{tikzpicture}[>=stealth',very thick,auto,
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	376	every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	377	\node[state,initial] (q_0) {$q_0$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	378	\node[state] (q_1) [right=of q_0] {$q_1$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	379	\node[state] (q_2) [below right=of q_0] {$q_2$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	380	\node[state] (q_3) [right=of q_2] {$q_3$};
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	381	\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	382	\path[->] (q_0) edge node [above] {\alert{$a$}} (q_1);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	383	\path[->] (q_1) edge node [above] {\alert{$a$}} (q_4);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	384	\path[->] (q_4) edge [loop right] node {\alert{$a, b$}} ();
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	385	\path[->] (q_3) edge node [right] {\alert{$a$}} (q_4);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	386	\path[->] (q_2) edge node [above] {\alert{$a$}} (q_3);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	387	\path[->] (q_1) edge node [right] {\alert{$b$}} (q_2);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	388	\path[->] (q_0) edge node [above] {\alert{$b$}} (q_2);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	389	\path[->] (q_2) edge [loop left] node {\alert{$b$}} ();
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	390	\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below] {\alert{$b$}} (q_0);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	391	\end{tikzpicture}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	392	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	393
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	394	for this automaton \bl{$\delta$} is the function\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	395
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	396	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	397	\begin{tabular}{lll}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	398	\bl{$(q_0, a) \rightarrow q_1$} & \bl{$(q_1, a) \rightarrow q_4$} & \bl{$(q_4, a) \rightarrow q_4$}\\
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	399	\bl{$(q_0, b) \rightarrow q_2$} & \bl{$(q_1, b) \rightarrow q_2$} & \bl{$(q_4, b) \rightarrow q_4$}\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	400	\end{tabular}\ldots
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	401	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	402
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	403	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	404	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	405
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	406	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	407	\begin{frame}[t]
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	408	\frametitle{Accepting a String}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	409
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	410	Given
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	411
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	412	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	413	\bl{$A(Q, q_0, F, \delta)$}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	414	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	415
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	416	you can define
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	417
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	418	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	419	\begin{tabular}{l}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	420	\bl{$\hat{\delta}(q, []) \dn q$}\\
143 e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	421	\bl{$\hat{\delta}(q, c::s) \dn \hat{\delta}(\delta(q, c), s)$}\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	422	\end{tabular}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	423	\end{center}\pause
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	424
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	425	Whether a string \bl{$s$} is accepted by \bl{$A$}?
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	426
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	427	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	428	\hspace{5mm}\bl{$\hat{\delta}(q_0, s) \in F$}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	429	\end{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	430	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	431	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	432
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	433	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	434	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	435	\frametitle{\begin{tabular}{c}Non-Deterministic\\[-1mm] Finite Automata\end{tabular}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	436
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	437	A non-deterministic finite automaton consists again of:
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	438
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	439	\begin{itemize}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	440	\item a finite set of states
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	441	\item one of these states is the start state
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	442	\item some states are accepting states, and
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	443	\item there is transition \alert{relation}\medskip
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	444	\end{itemize}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	445
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	446
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	447	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	448	\begin{tabular}{c}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	449	\bl{$(q_1, a) \rightarrow q_2$}\\
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	450	\bl{$(q_1, a) \rightarrow q_3$}\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	451	\end{tabular}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	452	\hspace{10mm}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	453	\begin{tabular}{c}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	454	\bl{$(q_1, \epsilon) \rightarrow q_2$}\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	455	\end{tabular}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	456	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	457
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	458	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	459	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	460
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	461	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	462	\begin{frame}[c]
143 e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	463	\frametitle{Two NFA Examples}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	464
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	465	\begin{center}
143 e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	466	\begin{tabular}[t]{c@{\hspace{9mm}}c}
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	467	\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	468	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	469	\node[state,initial] (q_0) {$q_0$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	470	\node[state] (q_1) [above=of q_0] {$q_1$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	471	\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	472	\path[->] (q_0) edge node [left] {\alert{$\epsilon$}} (q_1);
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	473	\path[->] (q_0) edge node [left] {\alert{$\epsilon$}} (q_2);
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	474	\path[->] (q_0) edge [loop right] node {\alert{$a$}} ();
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	475	\path[->] (q_1) edge [loop above] node {\alert{$a$}} ();
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	476	\path[->] (q_2) edge [loop below] node {\alert{$b$}} ();
143 e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	477	\end{tikzpicture} &
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	478
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	479	\raisebox{20mm}{
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	480	\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	481	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	482	\node[state,initial] (r_1) {$r_1$};
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	483	\node[state] (r_2) [above=of r_1] {$r_2$};
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	484	\node[state, accepting] (r_3) [right=of r_1] {$r_3$};
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	485	\path[->] (r_1) edge node [below] {\alert{$b$}} (r_3);
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	486	\path[->] (r_2) edge [bend left] node [above] {\alert{$a$}} (r_3);
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	487	\path[->] (r_1) edge [bend left] node [left] {\alert{$\epsilon$}} (r_2);
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	488	\path[->] (r_2) edge [bend left] node [right] {\alert{$a$}} (r_1);
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	489	\end{tikzpicture}}
e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	490	\end{tabular}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	491	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	492
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	493	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	494	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	495
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	496	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	497	\begin{frame}[c]
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	498	\frametitle{Rexp to NFA}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	499
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	500	\begin{center}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	501	\begin{tabular}[t]{l@{\hspace{10mm}}l}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	502	\raisebox{1mm}{\bl{$\varnothing$}} &
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	503	\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	504	\node[state, initial] (q_0) {$\mbox{}$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	505	\end{tikzpicture}\\\\
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	506	\raisebox{1mm}{\bl{$\epsilon$}} &
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	507	\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	508	\node[state, initial, accepting] (q_0) {$\mbox{}$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	509	\end{tikzpicture}\\\\
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	510	\raisebox{2mm}{\bl{$c$}} &
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	511	\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	512	\node[state, initial] (q_0) {$\mbox{}$};
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	513	\node[state, accepting] (q_1) [right=of q_0] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	514	\path[->] (q_0) edge node [below] {\alert{$c$}} (q_1);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	515	\end{tikzpicture}\\\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	516	\end{tabular}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	517	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	518
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	519	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	520	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	521
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	522	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	523	\begin{frame}[t]
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	524	\frametitle{Case $r_1\cdot r_2$}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	525
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	526	\mbox{}\bigskip
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	527	\onslide<1>{By recursion we are given two automata:\bigskip}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	528
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	529	{\centering\begin{tikzpicture}[node distance=3mm,
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	530	>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	531	\node[state, initial] (q_0) {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	532	\node (r_1) [right=of q_0] {$\ldots$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	533	\only<1>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	534	\node[state, accepting] (t_1) [right=of r_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	535	\node[state, accepting] (t_2) [above=of t_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	536	\node[state, accepting] (t_3) [below=of t_1] {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	537	\only<2>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	538	\node[state] (t_1) [right=of r_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	539	\node[state] (t_2) [above=of t_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	540	\node[state] (t_3) [below=of t_1] {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	541	\only<1>{\node[state, initial] (a_0) [right=2.5cm of t_1] {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	542	\only<2>{\node[state] (a_0) [right=2.5cm of t_1] {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	543	\node (b_1) [right=of a_0] {$\ldots$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	544	\node[state, accepting] (c_1) [right=of b_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	545	\node[state, accepting] (c_2) [above=of c_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	546	\node[state, accepting] (c_3) [below=of c_1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	547	\only<2>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	548	\path[->] (t_1) edge node [above, pos=0.3] {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	549	\path[->] (t_2) edge node [above] {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	550	\path[->] (t_3) edge node [below] {\alert{$\epsilon$}} (a_0);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	551	}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	552	\begin{pgfonlayer}{background}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	553	\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (r_1) (t_1) (t_2) (t_3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	554	\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	555	\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	556	\only<1>{\node [yshift=2mm] at (1.north) {\bl{$r_1$}};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	557	\only<1>{\node [yshift=2mm] at (2.north) {\bl{$r_2$}};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	558	\only<2>{\node [yshift=2mm] at (3.north) {\bl{$r_1\cdot r_2$}};}
143 e3fd4c5995ef added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 139 diff changeset	559	\end{pgfonlayer}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	560	\end{tikzpicture}}\bigskip\bigskip
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	561
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	562	\small
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	563	We need to (1) change the accepting nodes of the first automaton into non-accepting nodes, and (2) connect them
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	564	via $\epsilon$-transitions to the starting state of the second automaton.
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	565
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	566	\end{frame}
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	567	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	568
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	569	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	570	\begin{frame}[t]
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	571	\frametitle{Case $r_1+ r_2$}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	572	\mbox{}\\[-10mm]
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	573
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	574	\onslide<1>{By recursion we are given two automata:\smallskip}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	575
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	576	\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	577	>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	578	\onslide<1>{\node at (0,0) (1) {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	579	\onslide<2>{\node at (0,0) [state, initial] (1) {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	580	\only<1>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	581	\node[state, initial] (2) [above right=16mm of 1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	582	\node[state, initial] (3) [below right=16mm of 1] {$\mbox{}$};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	583	\only<2>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	584	\node[state] (2) [above right=16mm of 1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	585	\node[state] (3) [below right=16mm of 1] {$\mbox{}$};}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	586
137 69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	587	\node (a) [right=of 2] {$\ldots$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	588	\node[state, accepting] (a1) [right=of a] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	589	\node[state, accepting] (a2) [above=of a1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	590	\node[state, accepting] (a3) [below=of a1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	591
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	592	\node (b) [right=of 3] {$\ldots$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	593	\node[state, accepting] (b1) [right=of b] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	594	\node[state, accepting] (b2) [above=of b1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	595	\node[state, accepting] (b3) [below=of b1] {$\mbox{}$};
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	596	\only<2>{
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	597	\path[->] (1) edge node [above] {\alert{$\epsilon$}} (2);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	598	\path[->] (1) edge node [below] {\alert{$\epsilon$}} (3);
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	599	}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	600	\begin{pgfonlayer}{background}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	601	\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	602	\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	603	\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	604	\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r_1$}};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	605	\only<1>{\node [yshift=3mm] at (2.north) {\bl{$r_2$}};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	606	\only<2>{\node [yshift=3mm] at (3.north) {\bl{$r_1+ r_2$}};}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	607	\end{pgfonlayer}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	608	\end{tikzpicture}
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	609
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	610	\small
69cec773736b added pictures Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	611	We (1) need to introduce a new starting state and (2) connect it to the original two starting states.
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	612	\end{frame}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	613	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	614
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	615	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	616	\mode<presentation>{
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	617	\begin{frame}[c]
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	618	\frametitle{Case $r^*$}
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	619
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	620	\onslide<1>{By recursion we are given an automaton for $r$:\smallskip}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	621
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	622	\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	623	>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	624	\onslide<1>{\node at (0,0) (1) {$\mbox{}$};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	625	\onslide<2->{\node at (0,0) [state, initial,accepting] (1) {$\mbox{}$};}
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	626	\only<1>{\node[state, initial] (2) [right=16mm of 1] {$\mbox{}$};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	627	\only<2->{\node[state] (2) [right=16mm of 1] {$\mbox{}$};}
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	628	\node (a) [right=of 2] {$\ldots$};
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	629	\only<1>{
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	630	\node[state, accepting] (a1) [right=of a] {$\mbox{}$};
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	631	\node[state, accepting] (a2) [above=of a1] {$\mbox{}$};
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	632	\node[state, accepting] (a3) [below=of a1] {$\mbox{}$};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	633	\only<2->{
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	634	\node[state] (a1) [right=of a] {$\mbox{}$};
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	635	\node[state] (a2) [above=of a1] {$\mbox{}$};
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	636	\node[state] (a3) [below=of a1] {$\mbox{}$};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	637	\only<2->{
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	638	\path[->] (1) edge node [above] {\alert{$\epsilon$}} (2);
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	639	\path[->] (a1) edge [bend left=45] node [above] {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	640	\path[->] (a2) edge [bend right] node [below] {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	641	\path[->] (a3) edge [bend left=45] node [below] {\alert{$\epsilon$}} (1);
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	642
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	643	}
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	644	\begin{pgfonlayer}{background}
b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	645	\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	646	\only<2->{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};}
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	647	\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r$}};}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	648	\only<2->{\node [yshift=3mm] at (2.north) {\bl{$r^*$}};}
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	649	\end{pgfonlayer}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	650	\end{tikzpicture}\bigskip
138 b98a0a49c432 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	651
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	652	\onslide<3->{
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	653	Why can't we just have an epsilon transition from the accepting states to the starting state?}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	654
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	655	\end{frame}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	656	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	657
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	658
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	659	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	660	\mode<presentation>{
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	661	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	662	\frametitle{\begin{tabular}{c}Subset Construction\end{tabular}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	663
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	664
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	665	\begin{textblock}{5}(1,1)
cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	666	\begin{center}
cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	667	\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	668	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
215 828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	669	\node[state,initial] (q_0) {$q_0$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	670	\node[state] (q_1) [above=of q_0] {$q_1$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	671	\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	672	\path[->] (q_0) edge node [left] {\alert{$\epsilon$}} (q_1);
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	673	\path[->] (q_0) edge node [left] {\alert{$\epsilon$}} (q_2);
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	674	\path[->] (q_0) edge [loop right] node {\alert{$a$}} ();
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	675	\path[->] (q_1) edge [loop above] node {\alert{$a$}} ();
828303e8e4af updated slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	676	\path[->] (q_2) edge [loop below] node {\alert{$b$}} ();
136 cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	677	\end{tikzpicture}
cc19e6cbcb68 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 135 diff changeset	678	\end{center}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	679	\end{textblock}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	680
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	681	\begin{textblock}{11}(6.5,4.5)
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	682	\begin{tabular}{r\|cl}
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	683	nodes \textcolor{white}{*} & $a$ & $b$\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	684	\hline
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	685	$\varnothing$ \textcolor{white}{*} & \onslide<2->{$\varnothing$} & \onslide<2->{$\varnothing$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	686	$\{0\}$ \textcolor{white}{*} & \onslide<3->{$\{0,1,2\}$} & \onslide<3->{$\{2\}$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	687	$\{1\}$ \textcolor{white}{*} & \onslide<3->{$\{1\}$} & \onslide<3->{$\varnothing$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	688	$\{2\}$ \onslide<5->{*} & \onslide<3->{$\varnothing$} & \onslide<3->{$\{2\}$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	689	$\{0,1\}$ \textcolor{white}{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	690	$\{0,2\}$ \onslide<5->{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	691	$\{1,2\}$ \onslide<5->{*} & \onslide<4->{$\{1\}$} & \onslide<4->{$\{2\}$}\\
6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	692	\onslide<5->{s:} $\{0,1,2\}$ \onslide<5->{*}& \onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	693	\end{tabular}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	694	\end{textblock}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	695
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	696
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	697	\end{frame}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	698	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	699
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	700	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	701	\begin{frame}[c]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	702	\frametitle{Regexps and Automata}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	703
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	704	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	705	\begin{tikzpicture}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	706	\node (rexp) {\bl{\bf Regexps}};
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	707	\node (nfa) [right=of rexp] {\bl{\bf NFAs}};
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	708	\node (dfa) [right=of nfa] {\bl{\bf DFAs}};
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	709	\onslide<3->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	710	\path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	711	\path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	712	\onslide<3->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	713	\onslide<2->{\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	714	\end{tikzpicture}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	715	\end{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	716
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	717	\end{frame}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	718	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	719
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	720
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	721	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	722	\mode<presentation>{
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	723	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	724	\frametitle{\begin{tabular}{c}Regular Languages\end{tabular}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	725
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	726	A language is \alert{regular} iff there exists
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	727	a regular expression that recognises all its strings.\bigskip\medskip
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	728
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	729	or {\bf equivalently}\bigskip\medskip
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	730
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	731	A language is \alert{regular} iff there exists
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	732	a deterministic finite automaton that recognises all its strings.\bigskip\medskip\pause
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	733
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	734	Why is every finite set of strings a regular language?
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	735	\end{frame}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	736	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	737
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	738	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	739	\mode<presentation>{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	740	\begin{frame}<2>[c]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	741	\frametitle{DFA to Rexp}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	742
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	743	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	744	\begin{tikzpicture}[scale=2,>=stealth',very thick,
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	745	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	746	\only<1>{\node[state, initial] (q0) at ( 0,1) {$q_0$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	747	\only<2->{\node[state, initial,accepting] (q0) at ( 0,1) {$q_0$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	748	\only<1>{\node[state] (q1) at ( 1,1) {$q_1$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	749	\only<2->{\node[state,accepting] (q1) at ( 1,1) {$q_1$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	750	\only<1>{\node[state, accepting] (q2) at ( 2,1) {$q_2$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	751	\only<2->{\node[state] (q2) at ( 2,1) {$q_2$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	752	\path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	753	(q1) edge[bend left] node[above] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	754	(q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	755	(q1) edge node[above] {\alert{$a$}} (q2)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	756	(q2) edge [loop right] node {\alert{$a$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	757	(q0) edge [loop below] node {\alert{$b$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	758	;
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	759	\end{tikzpicture}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	760	\end{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	761
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	762	\onslide<3>{How to get from a DFA to a regular expression?}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	763
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	764	\end{frame}}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	765	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	766
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	767
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	768	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	769	\mode<presentation>{
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	770	\begin{frame}[c]
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	771
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	772	\begin{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	773	\begin{tikzpicture}[scale=2,>=stealth',very thick,
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	774	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	775	\only<1->{\node[state, initial] (q0) at ( 0,1) {$q_0$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	776	\only<1->{\node[state] (q1) at ( 1,1) {$q_1$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	777	\only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	778	\path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	779	(q1) edge[bend left] node[above] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	780	(q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	781	(q1) edge node[above] {\alert{$a$}} (q2)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	782	(q2) edge [loop right] node {\alert{$a$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	783	(q0) edge [loop below] node {\alert{$b$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	784	;
139 6e7c3db9023d added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	785	\end{tikzpicture}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	786	\end{center}\pause\bigskip
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	787
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	788	\onslide<2->{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	789	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	790	\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	791	\bl{$q_0$} & \bl{$=$} & \bl{$2\, q_0 + 3 \,q_1 + 4\, q_2$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	792	\bl{$q_1$} & \bl{$=$} & \bl{$2 \,q_0 + 3\, q_1 + 1\, q_2$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	793	\bl{$q_2$} & \bl{$=$} & \bl{$1\, q_0 + 5\, q_1 + 2\, q_2$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	794
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	795	\end{tabular}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	796	\end{center}
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	797	}
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	798
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	799	\end{frame}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	800	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	801
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	802	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	803	\mode<presentation>{
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	804	\begin{frame}[c]
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	805
265 332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	806	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	807	\begin{tikzpicture}[scale=2,>=stealth',very thick,
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	808	every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	809	\only<1->{\node[state, initial] (q0) at ( 0,1) {$q_0$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	810	\only<1->{\node[state] (q1) at ( 1,1) {$q_1$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	811	\only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	812	\path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	813	(q1) edge[bend left] node[above] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	814	(q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	815	(q1) edge node[above] {\alert{$a$}} (q2)
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	816	(q2) edge [loop right] node {\alert{$a$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	817	(q0) edge [loop below] node {\alert{$b$}} ()
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	818	;
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	819	\end{tikzpicture}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	820	\end{center}\bigskip
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	821
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	822	\onslide<2->{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	823	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	824	\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	825	\bl{$q_0$} & \bl{$=$} & \bl{$\epsilon + q_0\,b + q_1\,b + q_2\,b$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	826	\bl{$q_1$} & \bl{$=$} & \bl{$q_0\,a$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	827	\bl{$q_2$} & \bl{$=$} & \bl{$q_1\,a + q_2\,a$}\\
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	828
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	829	\end{tabular}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	830	\end{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	831	}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	832
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	833	\onslide<3->{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	834	Arden's Lemma:
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	835	\begin{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	836	If \bl{$q = q\,r + s$}\; then\; \bl{$q = s\, r^*$}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	837	\end{center}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	838	}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	839
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	840	\end{frame}}
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	841	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	842
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	843
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	844
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	845	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	846	\mode<presentation>{
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	847	\begin{frame}[c]
332fbe9c91ab added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 215 diff changeset	848
135 72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	849	Given the function
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	850
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	851	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	852	\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	853	$rev(\varnothing)$ & $\dn$ & $\varnothing$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	854	$rev(\epsilon)$ & $\dn$ & $\epsilon$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	855	$rev(c)$ & $\dn$ & $c$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	856	$rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	857	$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	858	$rev(r^)$ & $\dn$ & $rev(r)^$\\
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	859	\end{tabular}}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	860	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	861
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	862
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	863	and the set
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	864
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	865	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	866	\bl{$Rev\,A \dn \{s^{-1} \;\|\; s \in A\}$}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	867	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	868
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	869	prove whether
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	870
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	871	\begin{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	872	\bl{$L(rev(r)) = Rev (L(r))$}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	873	\end{center}
72b686e1c974 added slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	874
133 09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	875	\end{frame}}
09efdf5cf07c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 93 diff changeset	876	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25 94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	877
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	878
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	879	\end{document}
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	880
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	881	%%% Local Variables:
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	882	%%% mode: latex
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	883	%%% TeX-master: t
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	884	%%% End:
94133a0e62ed tuned Christian Urban <urbanc@in.tum.de> parents: diff changeset	885

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 06 Oct 2014 00:46:18 +0100
changeset 265	332fbe9c91ab
parent 215	828303e8e4af
child 346	a98794b11ac4
permissions	-rw-r--r--