1 (*<*)

     2 theory Slides1

     3 imports "LaTeXsugar"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    15   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    16   \mode<presentation>{

    17   \begin{frame}

    18   \frametitle{%

    19   \begin{tabular}{@ {}c@ {}}

    20   \Large A Formalisation of the\\[-5mm] 

    21   \Large Myhill-Nerode Theorem\\[-5mm] 

    22   \Large based on Regular Expressions\\[-3mm] 

    23   \large \onslide<2>{or, Regular Languages Done Right}\\

    24   \end{tabular}}

    25   

    26   \begin{center}

    27   Christian Urban

    28   \end{center}

    29  

    30 

    31   \begin{center}

    32   joint work with Chunhan Wu and Xingyuan Zhang from the PLA

    33   University of Science and Technology in Nanjing

    34   \end{center}

    35 

    36   \end{frame}}

    37   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    38 

    39 *}

    40 

    41 text_raw {*

    42   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    43   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    44   \mode<presentation>{

    45   \begin{frame}[c]

    46   \frametitle{In Textbooks\ldots}

    47 

    48   \begin{itemize}

    49   \item A \alert{regular language} is one where there is DFA that 

    50   recognises it.\pause

    51   \item Pumping lemma, closure properties of regular languages (closed 

    52   under ``negation'') etc are all described and proved in terms of DFAs\pause

    53 

    54   \item similarly the Myhill-Nerode theorem, which gives necessary and sufficient

    55   conditions for a language being regular (also describes a minimal DFA for a language)

    56 

    57   \end{itemize}

    58 

    59   \end{frame}}

    60   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    61 

    62 *}

    63 

    64 

    65 text_raw {*

    66   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    67   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    68   \mode<presentation>{

    69   \begin{frame}[c]

    70   \frametitle{Really Bad News!}

    71 

    72   This is bad news for formalisations in theorem provers. DFAs might

    73   be represented as

    74 

    75   \begin{itemize}

    76   \item graphs

    77   \item matrices

    78   \item partial functions

    79   \end{itemize}

    80 

    81   All constructions are difficult to reason about.\bigskip\bigskip 

    82   \pause

    83 

    84   \small

    85   Constable et al needed (on and off) 18 months for a 3-person team 

    86   to formalise automata theory in Nuprl including Myhill-Nerode. There is 

    87   only very little other formalised work on regular languages I know of

    88   in Coq, Isabelle and HOL.

    89 

    90 

    91   

    92   \end{frame}}

    93   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    94 

    95 *}

    96 

    97 text_raw {*

    98   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   100   \mode<presentation>{

   101   \begin{frame}[c]

   102   \frametitle{Regular Expressions}

   103 

   104   \ldots are a simple datatype defined as:

   105 

   106   \only<1>{

   107   \begin{center}\color{blue}

   108   \begin{tabular}{rcl}

   109   rexp & $::=$ & NULL\\

   110                & $\mid$ & EMPTY\\

   111                & $\mid$ & CHR c\\

   112                & $\mid$ & ALT rexp rexp\\

   113                & $\mid$ & SEQ rexp rexp\\

   114                & $\mid$ & STAR rexp

   115   \end{tabular}

   116   \end{center}}

   117   \only<2->{

   118   \begin{center}

   119   \begin{tabular}{rcl}

   120   \smath{r} & \smath{::=}  & \smath{\varepsilon} \\

   121             & \smath{\mid} & \smath{[]}\\

   122             & \smath{\mid} & \smath{c}\\

   123             & \smath{\mid} & \smath{r_1 + r_2}\\

   124             & \smath{\mid} & \smath{r_1 ; r_2}\\

   125             & \smath{\mid} & \smath{r^\star}

   126   \end{tabular}

   127   \end{center}}

   128 

   129   \end{frame}}

   130   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   131 

   132 *}

   133 

   134 

   135 (*<*)

   136 end

   137 (*>*)