Regular Languages Included in Deterministic Context-Free Languages

This file proves that every regular language over a finite alphabet is deterministic context-free.

Main results

• is_DCF_of_is_RG — every regular language is deterministic context-free
• RG_subclass_DCF — RG ⊆ DCF

def DPDA_of_DFA {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) : DPDA σ T Unit

DPDA that simulates a DFA by ignoring its stack.

Equations

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

theorem DPDA_of_DFA_reaches {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (w : List T) : PDA.Reaches { state := q, input := w, stack := [()] } { state := M.evalFrom q w, input := [], stack := [()] }

theorem DPDA_of_DFA_reaches_unique {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (w : List T) (q' : σ) (γ : List Unit) (h : PDA.Reaches { state := q, input := w, stack := [()] } { state := q', input := [], stack := γ }) : q' = M.evalFrom q w ∧ γ = [()]

theorem DPDA_of_DFA_accepts {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) : (DPDA_of_DFA M).acceptsByFinalState = M.accepts

The DPDA of a DFA accepts the same language as the DFA.

theorem is_DCF_of_is_RG {T : Type} [Fintype T] {L : Language T} (h : is_RG L) : is_DCF L

Every right-regular language over a finite alphabet is a DCF.

theorem RG_subclass_DCF {T : Type} [Fintype T] : RG ⊆ DCF