Total Deterministic Pushdown Automata

This file isolates the notion of a total DPDA. A DPDA need not read all of its input: it can reject by getting stuck or diverge in an infinite chain of ε-moves. A total DPDA always reaches an empty-input configuration on every input and its reachable empty-input configurations agree on acceptance, so it decides every input.

This is the target normal form produced by the totalization construction in Langlib.Automata.DeterministicPushdown.Totalization and the hypothesis under which DPDA.complement recognizes the complement language (Langlib.Automata.DeterministicPushdown.ClosureProperties.Complement).

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

A DPDA is total if it decides every input:

1. Totality: for each word w, the DPDA can reach some configuration with empty input from the initial configuration.
2. Acceptance consistency: all reachable empty-input configurations for a given word w agree on whether the state is accepting or not.

Equations

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

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

A language represented by a total DPDA: a DPDA that decides every input (DPDA.IsTotal) and accepts the language by final state. This is the target normal form used by deterministic context-free complement closure.

Equations

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