| 
1344
 | 
     1  | 
<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
  | 
| 
 | 
     2  | 
<BODY>
  | 
| 
 | 
     3  | 
  | 
| 
1345
 | 
     4  | 
<H1>A Simplified Scanner Generator</H1>
  | 
| 
1344
 | 
     5  | 
  | 
| 
 | 
     6  | 
This is half of a simplified functional scanner generator. The overall design
  | 
| 
 | 
     7  | 
is like this:
  | 
| 
 | 
     8  | 
<PRE>
  | 
| 
 | 
     9  | 
         regular expression
  | 
| 
 | 
    10  | 
                  |
  | 
| 
 | 
    11  | 
                  v
  | 
| 
 | 
    12  | 
             -----------
  | 
| 
 | 
    13  | 
             | mk_auto |
  | 
| 
 | 
    14  | 
             -----------
  | 
| 
 | 
    15  | 
                  |
  | 
| 
 | 
    16  | 
        deterministic automaton
  | 
| 
 | 
    17  | 
                  |
  | 
| 
 | 
    18  | 
                  v
  | 
| 
 | 
    19  | 
           ----------------
  | 
| 
 | 
    20  | 
string --> | auto_chopper | --> chopped up string
  | 
| 
 | 
    21  | 
           ----------------
  | 
| 
 | 
    22  | 
</PRE>
  | 
| 
 | 
    23  | 
A chopped up string is a pair of
  | 
| 
 | 
    24  | 
<UL>
  | 
| 
 | 
    25  | 
<LI>a prefix of the input string, chopped up into words of the language,
  | 
| 
 | 
    26  | 
<LI>together with the remaining suffix.
  | 
| 
 | 
    27  | 
</UL>
  | 
| 
 | 
    28  | 
For example, if the language consists just of the word <KBD>ab</KBD>, the
  | 
| 
 | 
    29  | 
input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
  | 
| 
 | 
    30  | 
<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
  | 
| 
 | 
    31  | 
<P>
  | 
| 
 | 
    32  | 
  | 
| 
 | 
    33  | 
The auto_chopper is implemented in theory AutoChopper. The top part of the
  | 
| 
 | 
    34  | 
diagram, i.e. the translation of regular expressions into deterministic
  | 
| 
 | 
    35  | 
finite automata is still missing.  <P>
  | 
| 
 | 
    36  | 
  | 
| 
1345
 | 
    37  | 
<H2>M.Sc./Diplom/Fopra Project</H2>
  | 
| 
 | 
    38  | 
  | 
| 
 | 
    39  | 
Task: formalize the translation of regular expressions into deterministic
  | 
| 
 | 
    40  | 
finite automata. We are looking for a theoretically inclined student who
  | 
| 
 | 
    41  | 
likes automata theory and is not afraid of logic and proofs.  Sounds
  | 
| 
 | 
    42  | 
interesting? Then contact <A
  | 
| 
 | 
    43  | 
HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
  | 
| 
 | 
    44  | 
HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
  | 
| 
 | 
    45  | 
This project is also suitable as a joint "Fopra" for two students.
  | 
| 
 | 
    46  | 
  | 
| 
1344
 | 
    47  | 
</BODY>
  | 
| 
 | 
    48  | 
</HTML>
  |