Functional Automata

Tobias Nipkow 🌐

March 30, 2004

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.

License

BSD License

Topics

Session Functional-Automata

Depends on

Used by

Cite

× 
@article{Functional-Automata-AFP,
  author  = {Tobias Nipkow},
  title   = {Functional Automata},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2004},
  note    = {\url{https://isa-afp.org/entries/Functional-Automata.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: