(*<*)+
−
theory Slides1+
−
imports "LaTeXsugar"+
−
begin+
−
+
−
notation (latex output)+
−
  set ("_") and+
−
  Cons  ("_::/_" [66,65] 65) +
−
+
−
(*>*)+
−
+
−
+
−
text_raw {*+
−
  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
  \mode<presentation>{+
−
  \begin{frame}+
−
  \frametitle{%+
−
  \begin{tabular}{@ {}c@ {}}+
−
  \Large A Formalisation of the\\[-5mm] +
−
  \Large Myhill-Nerode Theorem\\[-5mm] +
−
  \Large based on Regular Expressions\\[-3mm] +
−
  \large \onslide<2>{or, Regular Languages Done Right}\\+
−
  \end{tabular}}+
−
  +
−
  \begin{center}+
−
  Christian Urban+
−
  \end{center}+
−
 +
−
+
−
  \begin{center}+
−
  joint work with Chunhan Wu and Xingyuan Zhang from the PLA+
−
  University of Science and Technology in Nanjing+
−
  \end{center}+
−
+
−
  \end{frame}}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     +
−
+
−
*}+
−
+
−
text_raw {*+
−
  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
  \mode<presentation>{+
−
  \begin{frame}[c]+
−
  \frametitle{In Textbooks\ldots}+
−
+
−
  \begin{itemize}+
−
  \item A \alert{regular language} is one where there is DFA that +
−
  recognises it.\pause+
−
  \item Pumping lemma, closure properties of regular languages (closed +
−
  under ``negation'') etc are all described and proved in terms of DFAs\pause+
−
+
−
  \item similarly the Myhill-Nerode theorem, which gives necessary and sufficient+
−
  conditions for a language being regular (also describes a minimal DFA for a language)+
−
+
−
  \end{itemize}+
−
+
−
  \end{frame}}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     +
−
+
−
*}+
−
+
−
+
−
text_raw {*+
−
  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
  \mode<presentation>{+
−
  \begin{frame}[c]+
−
  \frametitle{Really Bad News!}+
−
+
−
  This is bad news for formalisations in theorem provers. DFAs might+
−
  be represented as+
−
+
−
  \begin{itemize}+
−
  \item graphs+
−
  \item matrices+
−
  \item partial functions+
−
  \end{itemize}+
−
+
−
  All constructions are difficult to reason about.\bigskip\bigskip +
−
  \pause+
−
+
−
  \small+
−
  Constable et al needed (on and off) 18 months for a 3-person team +
−
  to formalise automata theory in Nuprl including Myhill-Nerode. There is +
−
  only very little other formalised work on regular languages I know of+
−
  in Coq, Isabelle and HOL.+
−
+
−
+
−
  +
−
  \end{frame}}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     +
−
+
−
*}+
−
+
−
text_raw {*+
−
  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
  \mode<presentation>{+
−
  \begin{frame}[c]+
−
  \frametitle{Regular Expressions}+
−
+
−
  \ldots are a simple datatype defined as:+
−
+
−
  \only<1>{+
−
  \begin{center}\color{blue}+
−
  \begin{tabular}{rcl}+
−
  rexp & $::=$ & NULL\\+
−
               & $\mid$ & EMPTY\\+
−
               & $\mid$ & CHR c\\+
−
               & $\mid$ & ALT rexp rexp\\+
−
               & $\mid$ & SEQ rexp rexp\\+
−
               & $\mid$ & STAR rexp+
−
  \end{tabular}+
−
  \end{center}}+
−
  \only<2->{+
−
  \begin{center}+
−
  \begin{tabular}{rcl}+
−
  \smath{r} & \smath{::=}  & \smath{\varepsilon} \\+
−
            & \smath{\mid} & \smath{[]}\\+
−
            & \smath{\mid} & \smath{c}\\+
−
            & \smath{\mid} & \smath{r_1 + r_2}\\+
−
            & \smath{\mid} & \smath{r_1 ; r_2}\\+
−
            & \smath{\mid} & \smath{r^\star}+
−
  \end{tabular}+
−
  \end{center}}+
−
+
−
  \end{frame}}+
−
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     +
−
+
−
*}+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−