Pushdown Automaton - Formal Definition

Formal Definition

We use standard formal language notation: denotes the set of strings over alphabet and denotes the empty string.

A PDA is formally defined as a 7-tuple:

where

  • is a finite set of states
  • is a finite set which is called the input alphabet
  • is a finite set which is called the stack alphabet
  • is a finite subset of, the transition relation.
  • is the start state
  • is the initial stack symbol
  • is the set of accepting states

An element is a transition of . It has the intended meaning that, in state, with on the input and with as topmost stack symbol, may read, change the state to, pop, replacing it by pushing . The 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

  • is the transition function, mapping into finite subsets of .

Here contains all possible actions in state with on the stack, while reading on the input. One writes for the function precisely when for the relation. 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 is called an instantaneous description (ID) of, 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 defines the step-relation of on instantaneous descriptions. For instruction there exists a step, for every and every .

In general pushdown automata are nondeterministic meaning that in a given instantaneous description 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 with the initial stack symbol on the stack, and a string on the input tape, thus with initial description . 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 ), or it accepts by empty stack, 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

  1. with and (final state)
  2. with (empty stack)

Here represents the reflexive and transitive closure of the step relation 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 one may construct a pushdown automaton such that, and vice versa, for each pushdown automaton one may construct a pushdown automaton such that

Read more about this topic:  Pushdown Automaton

Famous quotes containing the words formal and/or definition:

    True variety is in that plenitude of real and unexpected elements, in the branch charged with blue flowers thrusting itself, against all expectations, from the springtime hedge which seems already too full, while the purely formal imitation of variety ... is but void and uniformity, that is, that which is most opposed to variety....
    Marcel Proust (1871–1922)

    Perhaps the best definition of progress would be the continuing efforts of men and women to narrow the gap between the convenience of the powers that be and the unwritten charter.
    Nadine Gordimer (b. 1923)