(*<*)
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
(*>*)