Myhill.thy
changeset 68 dceb84acdee8
parent 64 b69d4e04e64a
child 69 ecf6c61a4541
equal deleted inserted replaced
67:7478be786f87 68:dceb84acdee8
    33 get stuck: whenever a string is recognized as not belonging to the language, the augmented automaton
    33 get stuck: whenever a string is recognized as not belonging to the language, the augmented automaton
    34 is transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, 
    34 is transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, 
    35 in which case, the string is rejected by situation \ref{case_end_reject} above.
    35 in which case, the string is rejected by situation \ref{case_end_reject} above.
    36 
    36 
    37 Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}
    37 Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}
    38 corresponds to the state reached by processing @{text "x"} with the augmented automaton. 
    38 corresponds to the state reached by processing @{text "x"} with the augmented automaton. Since  
       
    39 @{text "\<approx>Lang `` {x}"} is defined for every @{text "x"}, it corresponds to the fact that 
       
    40 the processing of @{text "x"} will never get stuck.
       
    41 
       
    42 The most acquainted way to define a regular language @{text "Lang"} is by giving an automaton which
       
    43 recorgizes every string in @{text "Lang"}. Fig.\ref{fig_origin_auto} gives such a automaton, which 
       
    44 can be viewed as a way of assigning status to strings: for any given string @{text "x"}:
       
    45 
       
    46 
    39 
    47 
    40 \begin{figure}[h!]
    48 \begin{figure}[h!]
    41 \centering
    49 \centering
    42 \subfigure[Original automaton]{\label{fig_origin_auto}
    50 \subfigure[Original automaton]{\label{fig_origin_auto}
    43 \begin{minipage}{0.4\textwidth}
    51 \begin{minipage}{0.4\textwidth}