Editing Pushdown automaton (section)

=== Computations ===
[[Image:Pushdown-step.svg|thumb|200px|a step of the pushdown automaton]]
In order to formalize the semantics of the pushdown automaton a description of the current situation is introduced. Any 3-tuple <math>(p,w,\beta) \in Q \times \Sigma^* \times \Gamma^*</math> is called an instantaneous description (ID) of <math>M</math>, which includes the current state, the part of the input tape that has not been read, and the contents of the stack (topmost symbol written first). The transition relation <math>\delta</math> defines the step-relation <math>\vdash_{M}</math> of <math>M</math> on instantaneous descriptions. For instruction <math>(p,a,A,q,\alpha) \in \delta</math> there exists a step <math>(p,ax,A\gamma) \vdash_{M} (q,x,\alpha\gamma)</math>, for every <math>x\in\Sigma^*</math> and every <math>\gamma\in \Gamma^*</math>.

In general pushdown automata are nondeterministic meaning that in a given instantaneous description <math>(p,w,\beta)</math> there may be several possible steps. Any of these steps can be chosen in a computation.
With the above definition in each step always a single symbol (top of the stack) is popped, replacing it with as many symbols as necessary. As a consequence no step is defined when the stack is empty.

Computations of the pushdown automaton are sequences of steps. The computation starts in the initial state <math>q_{0}</math> with the initial stack symbol <math>Z</math> on the stack, and a string <math>w</math> on the input tape, thus with initial description <math>(q_{0},w,Z)</math>. 
There are two modes of accepting. The pushdown automaton either accepts by final state, which means after reading its input the automaton reaches an accepting state (in <math>F</math>), or it accepts by empty stack (<math>\varepsilon</math>), which means after reading its input the automaton empties its stack. The first acceptance mode uses the internal memory (state), the second the external memory (stack).

Formally one defines
# <math>L(M) = \{ w\in\Sigma^* | (q_{0},w,Z) \vdash_M^* (f,\varepsilon,\gamma)</math> with <math>f \in F</math> and <math>\gamma \in \Gamma^* \}</math> (final state)
# <math>N(M) = \{ w\in\Sigma^* | (q_{0},w,Z) \vdash_M^* (q,\varepsilon,\varepsilon)</math> with <math>q \in Q \}</math> (empty stack)

Here <math>\vdash_M^*</math> represents the [[reflexive closure|reflexive]] and [[transitive closure]] of the step relation <math>\vdash_M</math> meaning any number of consecutive steps (zero, one or more).

For each single pushdown automaton these two languages need to have no relation: they may be equal but usually this is not the case. A specification of the automaton should also include the intended mode of acceptance. Taken over all pushdown automata both acceptance conditions define the same family of languages.

'''Theorem.''' For each pushdown automaton <math>M</math> one may construct a pushdown automaton <math>M'</math> such that <math>L(M)=N(M')</math>, and vice versa, for each pushdown automaton <math>M</math> one may construct a pushdown automaton <math>M'</math> such that <math>N(M)=L(M')</math>