DCF Closure Under Intersection with a Regular Language

This file proves that the intersection of a deterministic context-free language with a regular language is again deterministic context-free.

Strategy

Given a DPDA M over (Q, T, S) and a DFA D over (T, σ), we build a product DPDA over (Q × σ, T, S) that simulates both machines in parallel:

• On reading input symbol a with stack top Z: the DPDA component transitions via M.transition q a Z and the DFA component transitions via D.step s a.
• On an ε-transition with stack top Z: only the DPDA component moves (via M.epsilon_transition q Z); the DFA state stays the same.
• Acceptance: the product state (q, s) is accepting iff q ∈ M.final_states and s ∈ D.accept.

Main declarations

• DPDA.productDFA : the product DPDA×DFA construction
• DPDA.productDFA_correct : the product accepts M.acceptsByFinalState ⊓ D.accepts
• DCF_inter_regular : DCFLs are closed under intersection with regular languages

def DPDA.productDFA {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) : DPDA (Q × σ) T S

The product DPDA×DFA: runs a DPDA and a DFA in parallel.

Equations

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

theorem DPDA.productDFA_step_projects {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) {c₁ c₂ : (M.productDFA D).toPDA.conf} (h : PDA.Reaches₁ c₁ c₂) : PDA.Reaches₁ { state := c₁.state.1, input := c₁.input, stack := c₁.stack } { state := c₂.state.1, input := c₂.input, stack := c₂.stack }

theorem DPDA.productDFA_step_dfa {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) {c₁ c₂ : (M.productDFA D).toPDA.conf} (h : PDA.Reaches₁ c₁ c₂) : ∃ (consumed : List T), c₁.input = consumed ++ c₂.input ∧ c₂.state.2 = List.foldl D.step c₁.state.2 consumed

theorem DPDA.productDFA_step_lift {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) (q : Q) (s : σ) (w : List T) (γ : List S) (q' : Q) (w' : List T) (γ' : List S) (hstep : PDA.Reaches₁ { state := q, input := w, stack := γ } { state := q', input := w', stack := γ' }) : ∃ (s' : σ), PDA.Reaches₁ { state := (q, s), input := w, stack := γ } { state := (q', s'), input := w', stack := γ' }

theorem DPDA.productDFA_reaches_projects {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) (q : Q) (s : σ) (w : List T) (γ : List S) (q' : Q) (s' : σ) (w' : List T) (γ' : List S) (h : PDA.Reaches { state := (q, s), input := w, stack := γ } { state := (q', s'), input := w', stack := γ' }) : PDA.Reaches { state := q, input := w, stack := γ } { state := q', input := w', stack := γ' }

theorem DPDA.productDFA_reaches_dfa_state {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) (q : Q) (s : σ) (w : List T) (γ : List S) (q' : Q) (s' : σ) (w' : List T) (γ' : List S) (h : PDA.Reaches { state := (q, s), input := w, stack := γ } { state := (q', s'), input := w', stack := γ' }) : ∃ (consumed : List T), w = consumed ++ w' ∧ s' = List.foldl D.step s consumed

theorem DPDA.productDFA_reaches_lift {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) (q : Q) (s : σ) (w : List T) (γ : List S) (q' : Q) (w' : List T) (γ' : List S) (hreach : PDA.Reaches { state := q, input := w, stack := γ } { state := q', input := w', stack := γ' }) : ∃ (s' : σ), PDA.Reaches { state := (q, s), input := w, stack := γ } { state := (q', s'), input := w', stack := γ' }

theorem DPDA.productDFA_correct {Q T S σ : Type} [Fintype Q] [Fintype T] [Fintype S] [Fintype σ] (M : DPDA Q T S) (D : DFA T σ) : (M.productDFA D).acceptsByFinalState = M.acceptsByFinalState ⊓ D.accepts

theorem DCF_inter_regular {T : Type} [Fintype T] (L₁ L₂ : Language T) (h₁ : is_DCF L₁) (h₂ : L₂.IsRegular) : is_DCF (L₁ ⊓ L₂)

The class of deterministic context-free languages is closed under intersection with regular languages.

theorem DCF_closedUnderIntersectionWithRegular {T : Type} [Fintype T] : ClosedUnderIntersectionWithRegular is_DCF

The class of deterministic context-free languages is closed under intersection with regular languages.