DPDA Totalization for Deterministic Context-Free Languages

This module is the public import point for the totalization construction used by unconditional complement closure of deterministic context-free languages.

The implementation is split into:

• Definition: language-level deciding presentations;
• EpsilonPhase: semantic epsilon-only DPDA phases;
• Saturation: finite P-automata saturation for epsilon lookahead;
• RegularAnalysis: packaged regular epsilon analyses;
• StackSummary: finite stack-summary annotations;
• AnnotatedStack: annotated totalizer stack symbols and lookahead queries;
• Construction: the analyzed totalized DPDA and its correctness;
• Presentation: the language-level totalization theorem.

The headline result, assembled here from those pieces, is DPDA.exists_equivalent_total: every DPDA has an equivalent total DPDA.

theorem DPDA.exists_equivalent_total {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : ∃ (Q' : Type) (S' : Type) (x : Fintype Q') (x_1 : Fintype S') (M' : DPDA Q' T S'), M'.IsTotal ∧ M'.acceptsByFinalState = M.acceptsByFinalState

DPDA totalization. Every DPDA has an equivalent total DPDA: a DPDA that decides every input (DPDA.IsTotal) and recognizes the same language by final-state acceptance.

The witness is the analyzed totalizer of a regular epsilon analysis, which every finite DPDA admits (DPDA.hasRegularEpsilonAnalysis); totalizer_decides gives totality and totalizer_acceptsByFinalState_eq_original gives language equality.