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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Functional-Automata-2009-04-29.tar.gz Isabelle 2008: afp-Functional-Automata-2008-06-10.tar.gz Isabelle 2007: afp-Functional-Automata-2007-11-27.tar.gz Isabelle 2005: afp-Functional-Automata-2005-10-14.tar.gz Isabelle 2004: afp-Functional-Automata-2004-05-21.tar.gz Isabelle 2003: afp-Functional-Automata-2004-03-30.tar.gz