Finite Automata Included in Deterministic Pushdown Automata

This file proves the inclusion directly on automata. A DFA is simulated by a DPDA whose stack alphabet is Unit: every input transition updates the finite control exactly as the DFA does and replaces the sole stack symbol by itself. An NFA is first determinized by the subset construction and then passed through the same simulation.

Main results

• DPDA_of_DFA — the stack-ignoring DPDA associated with a DFA.
• DPDA_of_DFA_accepts — the construction preserves the accepted language.
• DFA_subclass_DPDA — every DFA language is a DPDA language.
• NFA_subclass_DPDA — every NFA language is a DPDA language.

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

A DPDA that simulates a DFA while leaving its one-symbol stack unchanged.

Equations

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

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

The simulating DPDA can follow every DFA run without changing its stack.

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

Any accepting run of the simulating DPDA is the corresponding DFA run.

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

The stack-ignoring DPDA accepts exactly the language of its source DFA.

theorem is_DPDA_of_is_DFA {T : Type} [Fintype T] {L : Language T} (hL : is_DFA L) : is_DPDA L

Every language accepted by a DFA is accepted by a DPDA, via DPDA_of_DFA.

theorem DFA_subclass_DPDA {T : Type} [Fintype T] : DFA.Class ⊆ DPDA.Class

DFA-recognizable languages form a subclass of DPDA-recognizable languages.

theorem is_DPDA_of_is_NFA {T : Type} [Fintype T] {L : Language T} (hL : is_NFA L) : is_DPDA L

Every language accepted by an NFA is accepted by a DPDA. The construction first uses the finite subset construction and then DPDA_of_DFA.

theorem NFA_subclass_DPDA {T : Type} [Fintype T] : NFA.Class ⊆ DPDA.Class

NFA-recognizable languages form a subclass of DPDA-recognizable languages.