Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
<BODY>
<H1>A Simplified Scanner Generator</H1>
This is half of a simplified functional scanner generator. The overall design
is like this:
<PRE>
regular expression
|
v
-----------
| mk_auto |
-----------
|
deterministic automaton
|
v
----------------
string --> | auto_chopper | --> chopped up string
----------------
</PRE>
A chopped up string is a pair of
<UL>
<LI>a prefix of the input string, chopped up into words of the language,
<LI>together with the remaining suffix.
</UL>
For example, if the language consists just of the word <KBD>ab</KBD>, the
input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
<P>
The auto_chopper is implemented in theory AutoChopper. The top part of the
diagram, i.e. the translation of regular expressions into deterministic
finite automata is still missing. <P>
<H2>M.Sc./Diplom/Fopra Project</H2>
Task: formalize the translation of regular expressions into deterministic
finite automata. We are looking for a theoretically inclined student who
likes automata theory and is not afraid of logic and proofs. Sounds
interesting? Then contact <A
HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
This project is also suitable as a joint "Fopra" for two students.
</BODY>
</HTML>