Editing Nondeterministic finite automaton (section)

==Formal definition==
For a more elementary introduction of the formal definition, see [[automata theory]].

===Automaton===
An ''NFA'' is represented formally by a 5-[[tuple]],
<math>(Q, \Sigma, \delta, q_0, F)</math>, consisting of
* a finite [[Set (mathematics)|set]] of [[State (computer science)|states]] <math>Q</math>,
* a finite set of input symbols called the [[Alphabet (computer science)|alphabet]] <math>\Sigma</math>,
* a transition [[function (mathematics)|function]] <math>\delta</math> : <math>Q\times \Sigma  \rightarrow \mathcal{P}(Q)</math>,
* an initial (or start) state <math>q_0 \in Q</math>, and
* a set of accepting (or final) states <math>F \subseteq Q</math>.

Here, <math>\mathcal{P}(Q)</math> denotes the [[power set]] of <math>Q</math>.

===Recognized language===
Given an NFA <math>M = (Q, \Sigma, \delta, q_0, F)</math>, its recognized language is denoted by <math>L(M)</math>, and is defined as the set of all strings over the alphabet <math>\Sigma</math> that are accepted by <math>M</math>.

Loosely corresponding to the [[#Informal introduction|above]] informal explanations, there are several equivalent formal definitions of a string <math>w = a_1 a_2 ... a_n</math> being accepted by <math>M</math>:
*<math>w</math> is accepted if a sequence of states, <math>r_0, r_1, ..., r_n</math>, exists in <math>Q</math> such that:
*# <math>r_0 = q_0</math>
*# <math>r_{i+1} \in \delta (r_i, a_{i+1})</math>, for <math>i = 0, \ldots, n-1</math>
*# <math>r_n \in F</math>.
:In words, the first condition says that the machine starts in the start state <math>q_0</math>. The second condition says that given each character of string <math>w</math>, the machine will transition from state to state according to the transition function <math>\delta</math>. The last condition says that the machine accepts <math>w</math> if the last input of <math>w</math> causes the machine to halt in one of the accepting states. In order for <math>w</math> to be accepted by <math>M</math>, it is not required that every state sequence ends in an accepting state, it is sufficient if one does. Otherwise, ''i.e.'' if it is impossible at all to get from <math>q_0</math> to a state from <math>F</math> by following <math>w</math>, it is said that the automaton ''rejects'' the string. The set of strings <math>M</math> accepts is the [[Formal language|language]] ''recognized'' by <math>M</math> and this language is denoted by <math>L(M)</math>.<ref name="Aho.Hopcroft.Ullman.1974"/>{{rp|320}}<!---using "deduction" relation "\vdash"--->{{sfn|Sipser|1997|p=54}}

*Alternatively, <math>w</math> is accepted if <math>\delta^*(q_0, w) \cap F \not = \emptyset</math>, where <math>\delta^*: Q \times \Sigma^* \rightarrow \mathcal{P}(Q)</math> is defined [[recursion (computer science)|recursively]] by:
*# <math>\delta^*(r, \epsilon) = \{r\}</math> where <math>\epsilon</math> is the empty string, and
*# <math>\delta^*(r, xa)= \bigcup_{r' \in \delta^*(r, x)} \delta(r', a)</math> for all <math>x \in \Sigma^*, a \in \Sigma</math>.
:In words, <math>\delta^*(r, x)</math> is the set of all states reachable from state <math>r</math> by consuming the string <math>x</math>. The string <math>w</math> is accepted if some accepting state in <math>F</math> can be reached from the start state <math>q_0</math> by consuming <math>w</math>.{{sfn|Hopcroft|Ullman|1979|p=21}}{{sfn|Hopcroft|Motwani|Ullman|2006|p=59}}

===Initial state===
The above automaton definition uses a ''single initial state'', which is not necessary. Sometimes, NFAs are defined with a set of initial states. There is an easy construction that translates an NFA with multiple initial states to an NFA with a single initial state, which provides a convenient notation.