Hopcroft and Ullman say: a *finite automaton* over an
alphabet is a system where is
a finite nonempty set of *states*, is a finite *input
alphabet*, is a mapping of into ,
is the *initial state*, and is
the set of *final states*.

In Nuprl this definition is formalized nearly verbatim. The ``system'' is just an element of a product type. We use the notation Automata to denote the type of all automata with input alphabet and states . An automaton is a triple of transition, initial state and final states.

A automata

Automata == *A DA_act* (the first component of
)*A DA_init* (the
initial state, the second component)*A DA_fin* (the final states, the third component)*T DA_act_wf* Automata *T DA_init_wf* Automata *T DA_fin_wf* Automata

The first symbol on the line indicates either an abstraction, , or a theorem, .

Wed Jul 2 08:55:38 EDT 1997