Deterministic Pushdown Automata (DPDAs)

This file introduces deterministic pushdown automata (DPDAs).

The embedding of DPDAs into nondeterministic PDAs lives in Langlib.Automata.DeterministicPushdown.Inclusion.Pushdown. The notion of a total DPDA (DPDA.IsTotal) lives in Langlib.Automata.DeterministicPushdown.Basics.Total. Complement-closure results live in Langlib.Automata.DeterministicPushdown.ClosureProperties.Complement.

structure DPDA (Q T S : Type) [Fintype Q] [Fintype T] [Fintype S] : Type

A Deterministic Pushdown Automaton (DPDA) over state type Q, input alphabet T, and stack alphabet S.

The key difference from a (nondeterministic) PDA is that the transition functions return Option values instead of Set values, enforcing at most one transition per configuration. The no_mixed field additionally requires that ε-transitions and input-reading transitions are mutually exclusive for each (state, stack-top) pair.

Determinism guarantee. Given a configuration (q, a :: w, Z :: γ):

• If M.epsilon_transition q Z = some (p, β), then the unique possible move is to go to (p, a :: w, β ++ γ) (the no_mixed condition ensures no input-reading transition is available).
• Otherwise, if M.transition q a Z = some (p, β), the unique possible move is (p, w, β ++ γ).
• If neither transition is defined, the machine is stuck (halts).

• initial_state : Q

  Initial state

• start_symbol : S

  Initial stack symbol

• final_states : Set Q

  Set of accepting (final) states

• transition : Q → T → S → Option (Q × List S)

  Transition on reading input symbol a with stack top Z. Returns some (p, β) where p is the new state and β replaces Z on the stack, or none if no transition is defined.

• epsilon_transition : Q → S → Option (Q × List S)

  ε-transition (no input consumed) with stack top Z. Returns some (p, β) where p is the new state and β replaces Z on the stack, or none if no transition is defined.

• no_mixed (q : Q) (Z : S) : self.epsilon_transition q Z ≠ none → ∀ (a : T), self.transition q a Z = none

  Determinism constraint: if an ε-transition is defined for (q, Z), then no input-reading transition is defined for (q, a, Z) for any input symbol a.

noncomputable def DPDA.toPDA {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PDA Q T S

Embed a DPDA into the nondeterministic PDA framework by converting each Option transition to the corresponding singleton or empty set.

Equations

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

def DPDA.acceptsByFinalState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Language T

Language accepted by a DPDA via final-state acceptance: a word w is accepted iff the DPDA, starting from its initial configuration, can reach a configuration with empty input and an accepting state (with any remaining stack contents).

Equations

• M.acceptsByFinalState = M.toPDA.acceptsByFinalState

def is_DPDA {T : Type} [Fintype T] (L : Language T) : Prop

A language over a finite terminal alphabet is accepted by some DPDA via final-state acceptance.

Equations

• is_DPDA L = ∃ (Q : Type) (S : Type) (x : Fintype Q) (x_1 : Fintype S) (M : DPDA Q T S), M.acceptsByFinalState = L

def DPDA.Class {T : Type} [Fintype T] : Set (Language T)

The class of DPDA-recognizable languages.

Equations

• DPDA.Class = setOf is_DPDA