Regular Epsilon Analysis for DPDA Totalization

The totalizer needs finite, stack-regular lookahead for two semantic questions:

• Does the forced epsilon phase from (q, γ) reach a stable configuration?
• If the input is already exhausted at (q, γ), does the epsilon closure encounter an accepting state?

This file packages the finite analysis data. The remaining existence theorem is provided by the pushdown-system saturation construction: every finite DPDA has such an analysis.

structure DPDA.RegularEpsilonAnalysis {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type 1

A finite regular analysis of the epsilon-only behavior of a DPDA.

• StopState : Q → Type
• stopDecidableEq (q : Q) : DecidableEq (self.StopState q)
• stopFintype (q : Q) : Fintype (self.StopState q)
• stopDFA (q : Q) : DFA S (self.StopState q)
• stop_correct (q : Q) (γ : List S) : (self.stopDFA q).evalFrom (self.stopDFA q).start γ ∈ (self.stopDFA q).accept ↔ ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) c'
• AcceptState : Q → Type
• acceptDecidableEq (q : Q) : DecidableEq (self.AcceptState q)
• acceptFintype (q : Q) : Fintype (self.AcceptState q)
• acceptDFA (q : Q) : DFA S (self.AcceptState q)
• accept_correct (q : Q) (γ : List S) : (self.acceptDFA q).evalFrom (self.acceptDFA q).start γ ∈ (self.acceptDFA q).accept ↔ ∃ (q' : Q) (γ' : List S), M.EpsilonReaches (q, γ) (q', γ') ∧ q' ∈ M.final_states

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

The semantic epsilon-analysis existence theorem needed by the finite totalizer.

Equations

• M.HasRegularEpsilonAnalysis = Nonempty M.RegularEpsilonAnalysis

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

The saturation construction supplies the finite regular epsilon analysis used by the totalizer. For each control state q, the DFA state is the current set of P-automaton states reachable after reading the stack prefix.

Equations

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

theorem DPDA.hasRegularEpsilonAnalysis {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.HasRegularEpsilonAnalysis

Every finite DPDA has a regular epsilon analysis.