Finite Automata Strictly Included in Deterministic Pushdown Automata

The proof is entirely at the automata level. Inclusion is the explicit stack-ignoring simulation DPDA_of_DFA (preceded by subset determinization for NFAs). Strictness is witnessed by the explicit DPDA dpda_anbn, whose language {aⁿbⁿ} is not accepted by any DFA. Injective input relabelling transports that witness from Bool to every finite alphabet containing at least two symbols.

Main results

• DFA_strict_subclass_DPDA — DFA.Class ⊂ DPDA.Class on every nontrivial finite alphabet.
• NFA_strict_subclass_DPDA — NFA.Class ⊂ DPDA.Class under the same assumptions.
• _of_embedding and _of_card variants state the exact alphabet requirement.

theorem map_anbn_is_DPDA {T : Type} [Fintype T] (e : Bool ↪ T) : is_DPDA ((Language.map ⇑e) anbn)

Relabelling the explicit {aⁿbⁿ} DPDA along an alphabet embedding gives a DPDA for the relabelled language.

theorem DFA_strict_subclass_DPDA_of_embedding {T : Type} [Fintype T] (e : Bool ↪ T) : DFA.Class ⊂ DPDA.Class

DFA languages are strictly contained in DPDA languages whenever Bool embeds in the alphabet.

theorem DFA_strict_subclass_DPDA_of_card {T : Type} [Fintype T] (hT : 2 ≤ Fintype.card T) : DFA.Class ⊂ DPDA.Class

DFA languages are strictly contained in DPDA languages over every finite alphabet with at least two symbols.

theorem DFA_strict_subclass_DPDA {T : Type} [Fintype T] [Nontrivial T] : DFA.Class ⊂ DPDA.Class

DFA languages are strictly contained in DPDA languages over every nontrivial finite alphabet.

theorem NFA_strict_subclass_DPDA_of_embedding {T : Type} [Fintype T] (e : Bool ↪ T) : NFA.Class ⊂ DPDA.Class

NFA languages are strictly contained in DPDA languages whenever Bool embeds in the alphabet. Nonmembership of the witness is shown by explicitly determinizing any hypothetical accepting NFA.

theorem NFA_strict_subclass_DPDA_of_card {T : Type} [Fintype T] (hT : 2 ≤ Fintype.card T) : NFA.Class ⊂ DPDA.Class

NFA languages are strictly contained in DPDA languages over every finite alphabet with at least two symbols.

theorem NFA_strict_subclass_DPDA {T : Type} [Fintype T] [Nontrivial T] : NFA.Class ⊂ DPDA.Class

NFA languages are strictly contained in DPDA languages over every nontrivial finite alphabet.