theorem pda_language_isContextFree {α : Type u} {σ : Type u_1} {γ : Type u_2} (M : PDA α σ γ) : M.language.IsContextFree

If a PDA M recognizes a language, then the language is context-free. This is one direction of the equivalence of CFGs and PDAs (Theorem, Lecture 4).

theorem cfl_recognized_by_pda {α : Type u} (L : Language α) (hL : L.IsContextFree) : ∃ (σ : Type u) (γ : Type u) (M : PDA α σ γ), M.language = L

Every context-free language is recognized by some PDA. This is the converse direction of the equivalence of CFGs and PDAs (Theorem, Lecture 4): given a CFG g whose language is L, the constructed pushdown automaton CFGtoPDA.toPDA g recognizes L.

def PDA.product {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) : PDA α (σ₁ × σ₂) γ

Product construction of a PDA P and a DFA D. The resulting PDA has state set σ₁ × σ₂; it simulates P on its first component and the DFA D on its second component. For ε-transitions of P, the DFA state is left unchanged; for input transitions on a, the DFA component advances by D.step _ a. This is the standard construction used to show that the class of CFLs is closed under intersection with regular languages.

theorem PDA.product_step_proj₁ {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) {c₁ c₂ : Config} (hs : (P.product D).Step c₁ c₂) : P.Step (c₁.1.1, c₁.2.1, c₁.2.2) (c₂.1.1, c₂.2.1, c₂.2.2)

Projection lemma: a single step of the product PDA P.product D projects onto a single step of the original PDA P on the first component (state, input, stack).

theorem PDA.product_step_dfa_invariant {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) {c₁ c₂ : Config} (hs : (P.product D).Step c₁ c₂) : ∃ (a : Option α), c₁.2.1 = a.toList ++ c₂.2.1 ∧ c₂.1.2 = D.evalFrom c₁.1.2 a.toList

DFA invariant for one step of the product PDA: every step of P.product D corresponds to consuming some optional symbol a from the input and advancing the DFA component by D.evalFrom _ a.toList.

theorem PDA.product_reaches_proj₁ {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) {c₁ c₂ : Config} (hr : (P.product D).Reaches c₁ c₂) : P.Reaches (c₁.1.1, c₁.2.1, c₁.2.2) (c₂.1.1, c₂.2.1, c₂.2.2)

Reflexive–transitive version of product_step_proj₁: any computation of the product PDA P.product D projects to a computation of P on the first component.

theorem PDA.product_reaches_dfa_invariant {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) {c₁ c₂ : Config} (hr : (P.product D).Reaches c₁ c₂) : ∃ (consumed : List α), c₁.2.1 = consumed ++ c₂.2.1 ∧ c₂.1.2 = D.evalFrom c₁.1.2 consumed

DFA invariant for a full computation of the product PDA: any reachable configuration of P.product D corresponds to consuming a consumed prefix of the input, with the DFA component equal to D.evalFrom _ consumed.

theorem PDA.product_step_lift {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) (qd : σ₂) {c₁ c₂ : Config} (hs : P.Step c₁ c₂) : ∃ (a : Option α), c₁.2.1 = a.toList ++ c₂.2.1 ∧ (P.product D).Step ((c₁.1, qd), c₁.2.1, c₁.2.2) ((c₂.1, D.evalFrom qd a.toList), c₂.2.1, c₂.2.2)

Lifting lemma: any single step of the PDA P can be simulated by the product PDA P.product D starting from any DFA state qd, with the DFA component advancing along the symbol consumed in the step.

theorem PDA.product_reaches_of_pda_reaches {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) (qd : σ₂) {c₁ c₂ : Config} (hr : P.Reaches c₁ c₂) : ∃ (consumed : List α), c₁.2.1 = consumed ++ c₂.2.1 ∧ (P.product D).Reaches ((c₁.1, qd), c₁.2.1, c₁.2.2) ((c₂.1, D.evalFrom qd consumed), c₂.2.1, c₂.2.2)

Reflexive–transitive lifting of product_step_lift: any computation of P from c₁ to c₂ can be matched, starting from any DFA state qd, by a corresponding computation of P.product D where the DFA component evolves to D.evalFrom qd consumed.

theorem PDA.product_language {α : Type u} {σ₁ : Type u_1} {σ₂ : Type u_2} {γ : Type u_3} (P : PDA α σ₁ γ) (D : DFA α σ₂) : (P.product D).language = P.language ⊓ D.accepts

Language of the product PDA: L(P.product D) = L(P) ∩ L(D). This is the key step in proving that the class of context-free languages is closed under intersection with a regular language.

theorem cfl_inter_regular {T : Type u} {A B : Language T} (hA : A.IsContextFree) (hB : B.IsRegular) : (A ⊓ B).IsContextFree

Corollary 2 (Sipser, Lecture 5). If A is a context-free language and B is a regular language, then A ∩ B is context-free.

The proof takes a PDA P for A (via the equivalence of CFGs and PDAs) and a DFA D for B, forms the product PDA P.product D (which has language L(P) ∩ L(D) = A ∩ B), and converts that PDA back to a CFG.