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:

    The manifestation of poetry in external life is formal perfection. True sentiment grows within, and art must represent internal phenomena externally.
    Franz Grillparzer (1791–1872)

    Beauty, like all other qualities presented to human experience, is relative; and the definition of it becomes unmeaning and useless in proportion to its abstractness. To define beauty not in the most abstract, but in the most concrete terms possible, not to find a universal formula for it, but the formula which expresses most adequately this or that special manifestation of it, is the aim of the true student of aesthetics.
    Walter Pater (1839–1894)