A Formal Definition of a Pushdown Automaton

As with every other model of computation we study in the theory of computing, we need to come up with a formal definition of a pushdown automaton. There are about as many different definitions for a PDA as there are different textbooks. All of the various definitions are equivalent (unless someone has made a mistake).

Definition: Pushdown Automaton

A pushdown automaton is a mathematical object, M = (Q. Σ, Γ, δ, $q_0$, F), where

• Q is a finite set of states,
• Σ is a finite set of input symbols (also known as the input alphabet)
• Γ is a finite set of pushdown symbols (also known as the stack alphabet)
• δ is a transition function, δ: Q × Σ_ε × Γ_e → $2^Q$× Γ_ε, where Σ_ε = Σ ∪ {ε}, and Γ_ε = Γ ∪ { ε }
• $q_0$ ∈ Q is the designated start state
• F ⊆ Q is a set of accept states □