We use standard
formal language notation: \Gamma^{*} denotes the set of finite-length
strings over alphabet \Gamma and \varepsilon denotes the
empty string. A PDA is formally defined as a 7-tuple: M=(Q, \Sigma, \Gamma, \delta, q_{0}, Z, F) where • Q is a finite set of
states • \Sigma is a finite set which is called the
input alphabet • \Gamma is a finite set which is called the
stack alphabet • \delta is a finite subset of Q \times (\Sigma \cup \{\varepsilon\}) \times \Gamma \times Q \times \Gamma^*, the
transition relation • q_{0} \in Q is the
start state • Z \in \Gamma is the
initial stack symbol • F \subseteq Q is the set of
accepting states An element (p,a,A,q,\alpha) \in \delta is a transition of M. It has the intended meaning that M, in state p \in Q, on the input a \in \Sigma \cup \{\varepsilon\} and with A \in \Gamma as topmost stack symbol, may read a, change the state to q, pop A, replacing it by pushing \alpha \in \Gamma^*. The (\Sigma \cup \{\varepsilon\}) component of the transition relation is used to formalize that the PDA can either read a letter from the input, or proceed leaving the input untouched. In many texts the transition relation is replaced by an (equivalent) formalization, where • \delta is the
transition function, mapping Q \times (\Sigma \cup \{\varepsilon\}) \times \Gamma into finite subsets of Q \times \Gamma^* Here \delta(p, a, A) contains all possible actions in state p with A on the stack, while reading a on the input. One writes for example \delta(p, a, A) = \{(q, BA)\} precisely when (q, BA) \in \{(q, BA)\}, (q, BA) \in \delta(p, a, A), because ((p, a, A), \{(q, BA)\}) \in \delta. Note that
finite in this definition is essential.
Computations In order to formalize the semantics of the pushdown automaton, a description of the current situation is introduced. Any 3-tuple (p,w,\beta) \in Q \times \Sigma^* \times \Gamma^* is called an
instantaneous description (ID) of M, which includes the current state, the part of the input tape that has not been read, and the contents of the stack (top-most symbol written first). The transition relation \delta defines the step-relation \vdash_{M} of M on instantaneous descriptions. For instruction (p,a,A,q,\alpha) \in \delta there exists a step (p,ax,A\gamma) \vdash_{M} (q,x,\alpha\gamma), for every x\in\Sigma^* and every \gamma\in \Gamma^*. In general, pushdown automata are nondeterministic, meaning that in a given instantaneous description (p,w,\beta) there may be several possible steps. Any of these steps can be chosen in a computation. With the above definition, in each step a single symbol (top of the stack) is always popped, and replaced 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 q_{0} with the initial stack symbol Z on the stack, and a string w on the input tape—thus, with initial description (q_{0},w,Z). There are two modes of accepting. The pushdown automaton either accepts by final state, which means that after reading its input the automaton reaches an accepting state (in F), or else it accepts by empty stack (\varepsilon), which means that 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 • L(M) = \{ w\in\Sigma^* | (q_{0},w,Z) \vdash_M^* (f,\varepsilon,\gamma) with f \in F and \gamma \in \Gamma^* \} (final state) • N(M) = \{ w\in\Sigma^* | (q_{0},w,Z) \vdash_M^* (q,\varepsilon,\varepsilon) with q \in Q \} (empty stack) Here \vdash_M^* represents the
reflexive and
transitive closure of the step relation \vdash_M, meaning any number of consecutive steps (zero, one or more). For each single pushdown automaton, these two languages need 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 M one may construct a pushdown automaton M' such that L(M)=N(M'), and vice versa, for each pushdown automaton M one may construct a pushdown automaton M' such that N(M)=L(M') == Example ==