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