Functional Automata

Title:	Functional Automata
Author:	Tobias Nipkow
Submission date:	2004-03-30
Abstract:	This theory defines deterministic and nondeterministic automata in a functional representation: the transition function/relation and the finality predicate are just functions. Hence the state space may be infinite. It is shown how to convert regular expressions into such automata. A scanner (generator) is implemented with the help of functional automata: the scanner chops the input up into longest recognized substrings. Finally we also show how to convert a certain subclass of functional automata (essentially the finite deterministic ones) into regular sets.
BibTeX:	@article{Functional-Automata-AFP, author = {Tobias Nipkow}, title = {Functional Automata}, journal = {Archive of Formal Proofs}, month = mar, year = 2004, note = {\url{http://isa-afp.org/entries/Functional-Automata.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Regular-Sets
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.