Context-free languages are closed under intersection with regular languages

The intersection of a context-free language with a regular language is context-free ([BHPS61]). The construction is the triple product: the nonterminals of the product grammar are the nonterminals of G annotated with an entry and an exit state of the automaton M, and a rule of G yields one product rule for every way of threading the states of M through its right-hand side. A fresh start symbol rewrites to the start nonterminal of G between the start state and each accepting state of M.

Main definitions

• ContextFreeGrammar.Annotates: Annotates M p l out q says that the sentential form l of the product grammar is out with its nonterminals annotated so that the states of M thread from p to q.
• ContextFreeGrammar.product: the product of a grammar with a finite automaton.

Main results

• ContextFreeGrammar.product_language: the product generates the intersection.
• Language.IsContextFree.inter_isRegular: closure under intersection with a regular language, and its contrapositives Language.not_isContextFree_of_inter_regular_not and the proof schema Language.not_isContextFree_via_witness of [Shi85], which first pushes the language through a string homomorphism.

References

• [BHPS61]
• [HMU00]
• [Shi85]

@[reducible, inline]

abbrev ContextFreeGrammar.ProductNT {T : Type u_1} (G : ContextFreeGrammar T) (σ : Type) : Type

The nonterminals of the product grammar: a nonterminal of G between an entry and an exit state of the automaton, or the fresh start symbol none.

Equations

• G.ProductNT σ = Option (σ × G.NT × σ)

inductive ContextFreeGrammar.Annotates {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) : σ → List (Symbol T (G.ProductNT σ)) → List (Symbol T G.NT) → σ → Prop

Annotates M p l out q: the sentential form l of the product grammar is out with every nonterminal A replaced by some some (p', A, q'), the states threading from p to q: a terminal advances the automaton, and an annotated nonterminal jumps from its entry state to its exit state.

• nil {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} (p : σ) : Annotates M p [] [] p
• terminal {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} (a : T) {l : List (Symbol T (G.ProductNT σ))} {out : List (Symbol T G.NT)} (h : Annotates M (M.step p a) l out q) : Annotates M p (Symbol.terminal a :: l) (Symbol.terminal a :: out) q
• nonterminal {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p p' q : σ} (A : G.NT) {l : List (Symbol T (G.ProductNT σ))} {out : List (Symbol T G.NT)} (h : Annotates M p' l out q) : Annotates M p (Symbol.nonterminal (some (p, A, p')) :: l) (Symbol.nonterminal A :: out) q

theorem ContextFreeGrammar.Annotates.append {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q r : σ} {l₁ l₂ : List (Symbol T (G.ProductNT σ))} {out₁ out₂ : List (Symbol T G.NT)} (h₁ : Annotates M p l₁ out₁ q) (h₂ : Annotates M q l₂ out₂ r) : Annotates M p (l₁ ++ l₂) (out₁ ++ out₂) r

theorem ContextFreeGrammar.Annotates.split_out {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p r : σ} {l : List (Symbol T (G.ProductNT σ))} {out₁ out₂ : List (Symbol T G.NT)} (h : Annotates M p l (out₁ ++ out₂) r) : ∃ (l₁ : List (Symbol T (G.ProductNT σ))) (l₂ : List (Symbol T (G.ProductNT σ))) (q : σ), l = l₁ ++ l₂ ∧ Annotates M p l₁ out₁ q ∧ Annotates M q l₂ out₂ r

An annotation of a concatenation splits at the concatenation.

theorem ContextFreeGrammar.Annotates.split {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p r : σ} {l₁ l₂ : List (Symbol T (G.ProductNT σ))} {out : List (Symbol T G.NT)} (h : Annotates M p (l₁ ++ l₂) out r) : ∃ (out₁ : List (Symbol T G.NT)) (out₂ : List (Symbol T G.NT)) (q : σ), out = out₁ ++ out₂ ∧ Annotates M p l₁ out₁ q ∧ Annotates M q l₂ out₂ r

An annotation that is a concatenation annotates a concatenation.

theorem ContextFreeGrammar.Annotates.map_terminal {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} (p : σ) (w : List T) : Annotates M p (List.map Symbol.terminal w) (List.map Symbol.terminal w) (M.evalFrom p w)

theorem ContextFreeGrammar.Annotates.eq_of_map_terminal_right {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} {l : List (Symbol T (G.ProductNT σ))} {w : List T} (h : Annotates M p l (List.map Symbol.terminal w) q) : l = List.map Symbol.terminal w ∧ q = M.evalFrom p w

A word annotates only itself, and ends where the automaton ends.

theorem ContextFreeGrammar.Annotates.eq_of_map_terminal_left {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} {out : List (Symbol T G.NT)} {w : List T} (h : Annotates M p (List.map Symbol.terminal w) out q) : out = List.map Symbol.terminal w ∧ q = M.evalFrom p w

A word is annotated only by itself, and ends where the automaton ends.

theorem ContextFreeGrammar.Annotates.eq_of_singleton_right {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} {l : List (Symbol T (G.ProductNT σ))} {A : G.NT} (h : Annotates M p l [Symbol.nonterminal A] q) : l = [Symbol.nonterminal (some (p, A, q))]

theorem ContextFreeGrammar.Annotates.eq_of_singleton_left {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} {out : List (Symbol T G.NT)} {p₀ q₀ : σ} {A : G.NT} (h : Annotates M p [Symbol.nonterminal (some (p₀, A, q₀))] out q) : out = [Symbol.nonterminal A] ∧ p₀ = p ∧ q₀ = q

theorem ContextFreeGrammar.Annotates.none_notMem {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} {p q : σ} {l : List (Symbol T (G.ProductNT σ))} {out : List (Symbol T G.NT)} (h : Annotates M p l out q) : Symbol.nonterminal none ∉ l

noncomputable def ContextFreeGrammar.annotations {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] : σ → List (Symbol T G.NT) → Finset (σ × List (Symbol T (G.ProductNT σ)))

The annotations of out from state p, each with its exit state.

Equations

• One or more equations did not get rendered due to their size.
• ContextFreeGrammar.annotations M x✝ [] = {(x✝, [])}

theorem ContextFreeGrammar.mem_annotations {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] {p : σ} {out : List (Symbol T G.NT)} {x : σ × List (Symbol T (G.ProductNT σ))} : x ∈ annotations M p out ↔ Annotates M p x.2 out x.1

def ContextFreeGrammar.startRule {T : Type u_1} {σ : Type} (M : DFA T σ) (G : ContextFreeGrammar T) (q : σ) : ContextFreeRule T (G.ProductNT σ)

The start rule of the product for an accepting state q.

Equations

• ContextFreeGrammar.startRule M G q = { input := none, output := [Symbol.nonterminal (some (M.start, G.initial, q))] }

noncomputable def ContextFreeGrammar.productRules {T : Type u_1} {σ : Type} (M : DFA T σ) [Fintype σ] (G : ContextFreeGrammar T) : Finset (ContextFreeRule T (G.ProductNT σ))

The rules of the product: a start rule for each accepting state, and each rule of G in every annotation of its right-hand side.

Equations

• One or more equations did not get rendered due to their size.

theorem ContextFreeGrammar.mem_productRules {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] {r' : ContextFreeRule T (G.ProductNT σ)} : r' ∈ productRules M G ↔ (∃ q ∈ M.accept, r' = startRule M G q) ∨ ∃ r ∈ G.rules, ∃ (p : σ) (q : σ), r'.input = some (p, r.input, q) ∧ Annotates M p r'.output r.output q

theorem ContextFreeGrammar.startRule_mem_productRules {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] {q : σ} (hq : q ∈ M.accept) : startRule M G q ∈ productRules M G

theorem ContextFreeGrammar.mem_productRules_of_annotates {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] {r : ContextFreeRule T G.NT} (hr : r ∈ G.rules) {p q : σ} {l : List (Symbol T (G.ProductNT σ))} (h : Annotates M p l r.output q) : { input := some (p, r.input, q), output := l } ∈ productRules M G

noncomputable def ContextFreeGrammar.product {T : Type u_1} {σ : Type} [Fintype σ] (G : ContextFreeGrammar T) (M : DFA T σ) : ContextFreeGrammar T

The product of a grammar with a finite automaton: the nonterminals are annotated with entry and exit states, each rule of G appears in every annotation of its right-hand side, and the fresh start symbol rewrites to the start nonterminal of G between the start state and each accepting state.

Equations

• G.product M = { NT := G.ProductNT σ, initial := none, rules := ContextFreeGrammar.productRules M G }

@[simp]

theorem ContextFreeGrammar.product_initial {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} (M : DFA T σ) [Fintype σ] : (G.product M).initial = none

The product generates the intersection

theorem ContextFreeGrammar.Produces.of_product {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} [Fintype σ] {l' t' : List (Symbol T (G.ProductNT σ))} (step : (G.product M).Produces l' t') {p q : σ} {out : List (Symbol T G.NT)} (h : Annotates M p l' out q) : ∃ (out' : List (Symbol T G.NT)), G.Produces out out' ∧ Annotates M p t' out' q

A step of the product on an annotated form is a step of G on the form it annotates.

theorem ContextFreeGrammar.Derives.of_product {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} [Fintype σ] {l' t' : List (Symbol T (G.ProductNT σ))} (hd : (G.product M).Derives l' t') {p q : σ} {out : List (Symbol T G.NT)} (h : Annotates M p l' out q) : ∃ (out' : List (Symbol T G.NT)), G.Derives out out' ∧ Annotates M p t' out' q

A derivation of the product from an annotated form is a derivation of G from the form it annotates.

theorem ContextFreeGrammar.product_language_le {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} [Fintype σ] : (G.product M).language ≤ G.language ⊓ M.accepts

theorem ContextFreeGrammar.exists_annotates_of_derives {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} [Fintype σ] {out : List (Symbol T G.NT)} {w : List T} (hd : G.Derives out (List.map Symbol.terminal w)) (p : σ) : ∃ (l : List (Symbol T (G.ProductNT σ))), Annotates M p l out (M.evalFrom p w) ∧ (G.product M).Derives l (List.map Symbol.terminal w)

Every derivation of G of a word is the projection of a derivation of the product from an annotation of its start, for any entry state.

theorem ContextFreeGrammar.le_product_language {T : Type u_1} {σ : Type} {G : ContextFreeGrammar T} {M : DFA T σ} [Fintype σ] : G.language ⊓ M.accepts ≤ (G.product M).language

theorem ContextFreeGrammar.product_language {T : Type u_1} {σ : Type} [Fintype σ] (G : ContextFreeGrammar T) (M : DFA T σ) : (G.product M).language = G.language ⊓ M.accepts

Bar-Hillel: the product generates the intersection.

theorem Language.IsContextFree.inter_isRegular {α : Type u_1} {L R : Language α} (hL : L.IsContextFree) (hR : R.IsRegular) : (L ⊓ R).IsContextFree

Context-free languages are closed under intersection with regular languages.

theorem Language.not_isContextFree_of_inter_regular_not {α : Type u_1} {L R : Language α} (hR : R.IsRegular) (h : ¬(L ⊓ R).IsContextFree) : ¬L.IsContextFree

If L ∩ R is not context-free for a regular R, then L is not context-free.

theorem Language.not_isContextFree_via_witness {α : Type u_1} {β : Type u_2} (f : α → List β) (R : Language β) {L : Language α} (hR : R.IsRegular) (h : ¬((stringMap f) L ⊓ R).IsContextFree) : ¬L.IsContextFree

The proof schema of [Shi85]: if the image of L under a string homomorphism, intersected with a regular language, is not context-free, then L is not context-free.