Pushdown automata and context-free grammars

DefinitionTransitions of the grammar-simulating pushdown automaton#✓fully proved

Let \(g\) be a context-free grammar over an alphabet \(T\). To the single state, an input option (a letter of \(T\), or none for an \(\varepsilon\)-transition) and a popped symbol of \(g\) (a terminal or a nonterminal), this assigns a finite set of pairs of the state and a list of symbols of \(g\) to push. Popping a nonterminal \(A\) with no input gives, for each production of \(g\) with left-hand side \(A\), the pair pushing its right-hand side. Popping a terminal \(b\) while reading the letter \(a\) gives the single pair pushing nothing if \(a = b\), and the empty set otherwise. Popping a nonterminal while reading a letter, or a terminal with no input, gives the empty set.

noncomputable def cfgStep (g : ContextFreeGrammar T) :
    Unit → Option T → Symbol T g.NT → Finset (Unit × List (Symbol T g.NT))
  | _, none, .nonterminal A =>
      (g.rules.filter fun r => r.input = A).image fun r => ((), r.output)
  | _, some a, .terminal b => if a = b then {((), [])} else ∅
  | _, some _, .nonterminal _ => ∅
  | _, none, .terminal _ => ∅
Used by 4
Used byThe pushdown automaton simulating a context-free grammar · The grammar-simulating pushdown automaton accepts the grammar's language · The grammar-simulating pushdown automaton is finitely supported · Context-free languages are exactly the languages of finite pushdown automata

DefinitionThe pushdown automaton simulating a context-free grammar#✓fully proved

For a context-free grammar \(g\) over an alphabet \(T\), this is the pushdown automaton with input alphabet \(T\), a single state, the terminals and nonterminals of \(g\) as stack alphabet, and the initial nonterminal of \(g\) as initial stack symbol. Popping a nonterminal \(A\) on an \(\varepsilon\)-transition, it may push the right-hand side of any production of \(g\) with left-hand side \(A\) (whose first symbol becomes the new top); popping a terminal \(a\) while reading the input letter \(a\), it pushes nothing. It has no other transitions.

noncomputable def cfgPDA (g : ContextFreeGrammar T) :
    PDA T Unit (Symbol T g.NT) where
  step := cfgStep g
  start := ()
  startStack := .nonterminal g.initial
Uses 2 · Used by 5
Statement usesPushdown automaton · Transitions of the grammar-simulating pushdown automaton
Used byThe grammar-simulating pushdown automaton accepts the grammar's language · The grammar-simulating pushdown automaton is finitely supported · Context-free languages are accepted by finitely supported pushdown automata · Context-free languages are accepted by pushdown automata · Context-free languages are exactly the languages of finite pushdown automata

TheoremThe grammar-simulating pushdown automaton accepts the grammar's language#✓fully proved

For every context-free grammar \(g\) over an alphabet \(T\), the language accepted by empty stack by the one-state pushdown automaton simulating \(g\) equals the language generated by \(g\).

theorem ContextFreeGrammar.cfgPDA_accepts (g : ContextFreeGrammar T) :
    (cfgPDA g).accepts = g.language
Uses 12 · Used by 3
Statement usesLanguage accepted by a pushdown automaton · The pushdown automaton simulating a context-free grammar
Proof usesPushdown automaton · Pushdown automaton configuration · Multi-step computation of a pushdown automaton · Computations extend by unread input and stack bottom · One step of a pushdown automaton · Initial configuration of a pushdown automaton · Yield of a sentential form · Splitting a yield over a concatenation · Transitions of the grammar-simulating pushdown automaton · Language membership through yields
Used byContext-free languages are accepted by finitely supported pushdown automata · Context-free languages are accepted by pushdown automata · Context-free languages are exactly the languages of finite pushdown automata

TheoremContext-free languages are accepted by pushdown automata#✓fully proved

For every context-free language \(L\) over an alphabet \(T\) there are a context-free grammar \(g\) over \(T\) and a pushdown automaton with input alphabet \(T\), a single state, and the terminals and nonterminals of \(g\) as stack alphabet, whose language accepted by empty stack is \(L\).

theorem IsContextFree.exists_pda_accepts {L : Language T} (hL : L.IsContextFree) :
    ∃ (g : ContextFreeGrammar T) (M : PDA T Unit (Symbol T g.NT)), M.accepts = L
Uses 4
Statement usesPushdown automaton · Language accepted by a pushdown automaton
Proof usesThe grammar-simulating pushdown automaton accepts the grammar's language · The pushdown automaton simulating a context-free grammar

TheoremThe grammar-simulating pushdown automaton is finitely supported#✓fully proved

For every context-free grammar \(g\) over an alphabet \(T\), the one-state pushdown automaton simulating \(g\) is finitely supported.

The finite sets witnessing this are the set containing the single state, the set of stack symbols consisting of the initial nonterminal of \(g\) and all symbols occurring in right-hand sides of productions of \(g\), and the set of terminals occurring in right-hand sides of productions of \(g\).

theorem ContextFreeGrammar.cfgPDA_finitelySupported (g : ContextFreeGrammar T) :
    (cfgPDA g).FinitelySupported
Uses 4 · Used by 1
Statement usesFinitely supported pushdown automata · The pushdown automaton simulating a context-free grammar
Proof usesPushdown automaton · Transitions of the grammar-simulating pushdown automaton
Used byContext-free languages are accepted by finitely supported pushdown automata

TheoremContext-free languages are accepted by finitely supported pushdown automata#✓fully proved

For every context-free language \(L\) over an alphabet \(T\) there are a context-free grammar \(g\) over \(T\) and a finitely supported pushdown automaton with input alphabet \(T\), a single state, and the terminals and nonterminals of \(g\) as stack alphabet, whose language accepted by empty stack is \(L\).

theorem IsContextFree.exists_finitely_supported_pda_accepts {L : Language T}
    (hL : L.IsContextFree) :
    ∃ (g : ContextFreeGrammar T) (M : PDA T Unit (Symbol T g.NT)),
      M.FinitelySupported ∧ M.accepts = L
Uses 6
Statement usesPushdown automaton · Finitely supported pushdown automata · Language accepted by a pushdown automaton
Proof usesThe grammar-simulating pushdown automaton accepts the grammar's language · The grammar-simulating pushdown automaton is finitely supported · The pushdown automaton simulating a context-free grammar

DefinitionChain of triple nonterminals#✓fully proved

Write \((p, \gamma, q)\) for the nonterminal symbol given by states \(p, q\) and a stack symbol \(\gamma\) (the nonterminals of the triple grammar are these triples and one extra initial nonterminal). The chain form of a list \(\gamma_1 \cdots \gamma_k\) of stack symbols along a nonempty list \(s_0, s_1, \dots, s_m\) of states is the word \((s_0, \gamma_1, s_1)(s_1, \gamma_2, s_2) \cdots (s_{j-1}, \gamma_j, s_j)\) with \(j = \min(k, m)\): consecutive states bracket each stack symbol. Along the empty list of states the chain form is the empty word. In the intended use \(m = k\), so every stack symbol is bracketed.

def chainForm : List Γ → List σ → List (Symbol T (Option (σ × Γ × σ)))
  | [], _ => []
  | _ :: _, [] => []
  | _ :: _, _ :: [] => []
  | γ :: γs, p :: q :: ss =>
    Symbol.nonterminal (some (p, γ, q)) :: chainForm γs (q :: ss)
Used by 3
Used byChain forms consist of nonterminals · The triple grammar generates the accepted language · Production of the triple grammar for a transition

TheoremChain forms consist of nonterminals#✓fully proved

For every list of stack symbols and every list of states, every symbol of their chain form is a nonterminal.

theorem nonterminal_of_mem_chainForm {s : Symbol T (Option (σ × Γ × σ))}
    {γs : List Γ} {ss : List σ} (hs : s ∈ chainForm γs ss) :
    ∃ A, s = Symbol.nonterminal A
Uses 1 · Used by 1
Statement usesChain of triple nonterminals
Used byThe triple grammar generates the accepted language

DefinitionLists of states of a given length#✓fully proved

For a finite set \(\sigma\) of states and a natural number \(n\), this is the finite set of all lists of length \(n\) with entries in \(\sigma\). It is built recursively: for \(n = 0\) it contains only the empty list, and for \(n + 1\) it consists of the lists obtained by putting a state \(p \in \sigma\) in front of a list from the set for \(n\).

noncomputable def stateLists : ℕ → Finset (List σ)
  | 0 => {[]}
  | n + 1 => (Finset.univ ×ˢ stateLists n).image fun x => x.1 :: x.2
Used by 4
Used byProductions of the triple grammar · Start productions of the triple grammar · Transition productions of the triple grammar · Triple grammar of a pushdown automaton

DefinitionTerminal word of an optional input letter#✓fully proved

As a word of grammar symbols (terminals and triple nonterminals), an input that is a letter \(a\) contributes the one-symbol word consisting of the terminal \(a\), and the empty input \(\varepsilon\) contributes the empty word.

def optTerms (opt : Option T) : List (Symbol T (Option (σ × Γ × σ))) :=
  opt.toList.map Symbol.terminal
Used by 2
Used byThe triple grammar generates the accepted language · Production of the triple grammar for a transition

DefinitionProduction of the triple grammar for a transition#✓fully proved

Let \(p\) and \(r\) be states, \(\gamma\) a stack symbol, \(a\) an optional input letter, \(\varepsilon_1 \cdots \varepsilon_k\) a list of stack symbols and \(s_1, \dots, s_m\) a list of states. Write \(s_0 = r\) and let \(q = s_m\) be the last state of the list \(s_0, s_1, \dots, s_m\) (so \(q = r\) when \(m = 0\)). The production has left-hand side the nonterminal \((p, \gamma, q)\), and its right-hand side is the letter \(a\) (nothing if \(a\) is absent) followed by the nonterminals \((s_{i-1}, \varepsilon_i, s_i)\) for \(i = 1, \dots, \min(k, m)\) in order.

It encodes a transition that in state \(p\), reading \(a\) (or no letter), pops \(\gamma\), moves to state \(r\) and pushes \(\varepsilon_1 \cdots \varepsilon_k\); the triple grammar uses it with \(m = k\).

def stepRule (p : σ) (γ : Γ) (opt : Option T) (r : σ) (εs : List Γ)
    (ss : List σ) : ContextFreeRule T (Option (σ × Γ × σ)) :=
  ⟨some (p, γ, (r :: ss).getLast (List.cons_ne_nil r ss)),
    optTerms opt ++ chainForm εs (r :: ss)⟩
Uses 2 · Used by 5
Statement usesChain of triple nonterminals · Terminal word of an optional input letter
Used byProductions of the triple grammar · Start productions of the triple grammar · Transition productions of the triple grammar · Triple grammar of a pushdown automaton · The triple grammar generates the accepted language

DefinitionTriple grammar of a pushdown automaton#✓fully proved

Let \(M\) be a pushdown automaton over the alphabet \(T\) with a finite set \(\sigma\) of states, a finite stack alphabet \(\Gamma\), start state \(q_0\) and initial stack symbol \(Z_0\), and let \(T_0\) be a finite set of letters. The triple grammar of \(M\) and \(T_0\) is the context-free grammar over \(T\) whose nonterminals are an initial nonterminal \(S\) and the triples \((p, \gamma, q)\) with \(p, q \in \sigma\) and \(\gamma \in \Gamma\). Its productions are the start productions \(S \to (q_0, Z_0, q)\) for every state \(q\), and the transition productions: for every state \(p\), stack symbol \(\gamma\), input \(a\) that is \(\varepsilon\) or a letter of \(T_0\), transition of \(M\) from \(p\) on \(a\) popping \(\gamma\) that moves to a state \(r\) and pushes \(\gamma_1 \cdots \gamma_k\), and all states \(s_1, \dots, s_k\), writing \(s_0 = r\), the production

\[(p, \gamma, s_k) \to a\,(s_0, \gamma_1, s_1)(s_1, \gamma_2, s_2) \cdots (s_{k-1}, \gamma_k, s_k)\]

where \(a\) is omitted when it is \(\varepsilon\) (for \(k = 0\) this is \((p, \gamma, r) \to a\)).

The nonterminal \((p, \gamma, q)\) is meant to derive the words that take \(M\) from state \(p\) with stack \(\gamma\) to state \(q\) with empty stack; transitions on letters outside \(T_0\) are not used.

noncomputable def pdaGrammar (M : PDA T σ Γ) (T₀ : Finset T) :
    ContextFreeGrammar T where
  NT := Option (σ × Γ × σ)
  initial := none
  rules :=
    (Finset.univ.image fun q =>
        (⟨none, [Symbol.nonterminal (some (M.start, M.startStack, q))]⟩ :
          ContextFreeRule T (Option (σ × Γ × σ)))) ∪
      (Finset.univ.biUnion fun p => Finset.univ.biUnion fun γ =>
        (insert none (T₀.image some)).biUnion fun opt =>
          (M.step p opt γ).biUnion fun y =>
            (stateLists y.2.length).image fun ss =>
              stepRule p γ opt y.1 y.2 ss)
Uses 3 · Used by 5
Statement usesPushdown automaton · Lists of states of a given length · Production of the triple grammar for a transition
Used byProductions of the triple grammar · Finite pushdown automata accept context-free languages · Start productions of the triple grammar · Transition productions of the triple grammar · The triple grammar generates the accepted language

TheoremStart productions of the triple grammar#✓fully proved

Let \(M\) be a pushdown automaton with a finite set of states, a finite stack alphabet, start state \(q_0\) and initial stack symbol \(Z_0\), and let \(T_0\) be a finite set of input letters. For every state \(q\), the triple grammar of \(M\) and \(T_0\) contains the production \(S \to (q_0, Z_0, q)\), where \(S\) is its initial nonterminal.

theorem mem_rules_start {q : σ} :
    (⟨none, [Symbol.nonterminal (some (M.start, M.startStack, q))]⟩ :
        ContextFreeRule T (Option (σ × Γ × σ))) ∈
      (pdaGrammar M T₀).rules
Uses 4 · Used by 1
Statement usesPushdown automaton · Triple grammar of a pushdown automaton
Proof usesLists of states of a given length · Production of the triple grammar for a transition
Used byThe triple grammar generates the accepted language

TheoremTransition productions of the triple grammar#✓fully proved

Let \(M\) be a pushdown automaton with a finite set of states and a finite stack alphabet, and let \(T_0\) be a finite set of input letters. Let \(a\) be either \(\varepsilon\) or a letter in \(T_0\), and suppose that \(M\) has a transition from state \(p\) on \(a\) popping the stack symbol \(\gamma\) that moves to state \(r\) and pushes \(\gamma_1 \cdots \gamma_k\). Then for all states \(s_1, \dots, s_k\), writing \(s_0 = r\), the triple grammar of \(M\) and \(T_0\) contains the production

\[(p, \gamma, s_k) \to a\,(s_0, \gamma_1, s_1)(s_1, \gamma_2, s_2) \cdots (s_{k-1}, \gamma_k, s_k)\]

where \(a\) is omitted when it is \(\varepsilon\).

theorem mem_rules_step {p : σ} {γ : Γ} {opt : Option T} {r : σ}
    {εs : List Γ} {ss : List σ}
    (hopt : opt = none ∨ ∃ a ∈ T₀, opt = some a)
    (hstep : (r, εs) ∈ M.step p opt γ) (hss : ss.length = εs.length) :
    stepRule p γ opt r εs ss ∈ (pdaGrammar M T₀).rules
Uses 4 · Used by 1
Statement usesPushdown automaton · Triple grammar of a pushdown automaton · Production of the triple grammar for a transition
Proof usesLists of states of a given length
Used byThe triple grammar generates the accepted language

TheoremProductions of the triple grammar#✓fully proved

Let \(M\) be a pushdown automaton with a finite set of states, a finite stack alphabet, start state \(q_0\) and initial stack symbol \(Z_0\), and let \(T_0\) be a finite set of input letters. Every production of the triple grammar of \(M\) and \(T_0\) is of one of two kinds. Either it is a start production \(S \to (q_0, Z_0, q)\) for some state \(q\), where \(S\) is the initial nonterminal; or there are states \(p\) and \(r\), a stack symbol \(\gamma\), an input \(a\) that is a letter or \(\varepsilon\), a transition of \(M\) from \(p\) on \(a\) popping \(\gamma\) that moves to \(r\) and pushes \(\gamma_1 \cdots \gamma_k\), and states \(s_1, \dots, s_k\) such that, writing \(s_0 = r\), the production is

\[(p, \gamma, s_k) \to a\,(s_0, \gamma_1, s_1)(s_1, \gamma_2, s_2) \cdots (s_{k-1}, \gamma_k, s_k)\]

where \(a\) is omitted when it is \(\varepsilon\) (for \(k = 0\) the production is \((p, \gamma, r) \to a\)).

theorem cases_of_mem_rules {r : ContextFreeRule T (Option (σ × Γ × σ))}
    (hr : r ∈ (pdaGrammar M T₀).rules) :
    (∃ q : σ, r = ⟨none,
      [Symbol.nonterminal (some (M.start, M.startStack, q))]⟩) ∨
    (∃ (p : σ) (γ : Γ) (opt : Option T) (r₀ : σ) (εs : List Γ) (ss : List σ),
      (r₀, εs) ∈ M.step p opt γ ∧ ss.length = εs.length ∧
        r = stepRule p γ opt r₀ εs ss)
Uses 4 · Used by 1
Statement usesPushdown automaton · Triple grammar of a pushdown automaton · Production of the triple grammar for a transition
Proof usesLists of states of a given length
Used byThe triple grammar generates the accepted language

TheoremThe triple grammar generates the accepted language#✓fully proved

Let \(M\) be a pushdown automaton with a finite set of states and a finite stack alphabet, and let \(T_0\) be a finite set of input letters such that \(M\) has no transition, from any state and popping any stack symbol, that consumes a letter outside \(T_0\). Then the language generated by the triple grammar of \(M\) and \(T_0\) equals the language accepted by \(M\) by empty stack.

theorem PDA.pdaGrammar_language
    (hT : ∀ (p : σ) (a : T) (γ : Γ), a ∉ T₀ → M.step p (some a) γ = ∅) :
    (pdaGrammar M T₀).language = M.accepts
Uses 20 · Used by 1
Statement usesPushdown automaton · Language accepted by a pushdown automaton · Triple grammar of a pushdown automaton
Proof usesPushdown automaton configuration · Multi-step computation of a pushdown automaton · Computations extend by unread input and stack bottom · One step of a pushdown automaton · Initial configuration of a pushdown automaton · Yield of a sentential form · Concatenation of yields · Splitting a yield over a concatenation · Productions of the triple grammar · Chain of triple nonterminals · Language membership through yields · Start productions of the triple grammar · Transition productions of the triple grammar · Chain forms consist of nonterminals · Terminal word of an optional input letter · Production of the triple grammar for a transition · Yield through one production
Used byFinite pushdown automata accept context-free languages

TheoremFinite pushdown automata accept context-free languages#✓fully proved

Let \(M\) be a pushdown automaton with a finite set of states and a finite stack alphabet, and suppose that there is a finite set \(T_0\) of input letters such that \(M\) has no transition, from any state and popping any stack symbol, that consumes a letter outside \(T_0\). Then the language accepted by \(M\) by empty stack is context-free.

theorem PDA.isContextFree_accepts [Finite σ] [Finite Γ]
    (hT : ∀ (p : σ) (a : T) (γ : Γ), a ∉ T₀ → M.step p (some a) γ = ∅) :
    M.accepts.IsContextFree
Uses 4 · Used by 2
Statement usesPushdown automaton · Language accepted by a pushdown automaton
Proof usesThe triple grammar generates the accepted language · Triple grammar of a pushdown automaton
Used byDeterministic context-free languages are context-free · Context-free languages are exactly the languages of finite pushdown automata

TheoremContext-free languages are exactly the languages of finite pushdown automata#✓fully proved

A language \(L\) over an alphabet \(T\) is context-free if and only if there are a pushdown automaton \(M\) over \(T\) with a finite set of states and a finite stack alphabet, and a finite set \(T_0\) of input letters such that \(M\) has no transition, from any state and popping any stack symbol, that consumes a letter outside \(T_0\), for which the language accepted by \(M\) by empty stack is \(L\).

Here the alphabet, the states and the stack alphabet are types in the lowest universe.

theorem isContextFree_iff_exists_pda_accepts {T : Type} {L : Language T} :
    L.IsContextFree ↔ ∃ (σ Γ : Type) (_ : Fintype σ) (_ : Fintype Γ)
      (M : PDA T σ Γ),
      (∃ T₀ : Finset T, ∀ (p : σ) (a : T) (γ : Γ), a ∉ T₀ →
        M.step p (some a) γ = ∅) ∧ M.accepts = L
Uses 10
Statement usesPushdown automaton · Language accepted by a pushdown automaton
Proof usesClosed sets of stack symbols · Restricting the stack alphabet preserves the accepted language · Transitions of the restricted pushdown automaton · Restricting the stack alphabet of a pushdown automaton · The grammar-simulating pushdown automaton accepts the grammar's language · Finite pushdown automata accept context-free languages · The pushdown automaton simulating a context-free grammar · Transitions of the grammar-simulating pushdown automaton
18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.