P-Automata for DPDA Epsilon Saturation

This file contains the finite automaton layer and saturation construction for DPDA epsilon phases. The saturated P-automaton relations recognize exactly the stack prefixes whose epsilon phase can reach either a stable configuration or a final control state.

@[reducible, inline]

abbrev DPDA.PAutState (Q : Type) : Type

States of a P-automaton: original control states plus one distinguished sink state used by target automata for arbitrary stack suffixes.

Equations

• DPDA.PAutState Q = (Q ⊕ Unit)

def DPDA.PAutState.control {Q : Type} (q : Q) : PAutState Q

Embed an original DPDA state as a P-automaton state.

Equations

• DPDA.PAutState.control q = Sum.inl q

def DPDA.PAutState.sink {Q : Type} : PAutState Q

Distinguished target/sink state.

Equations

• DPDA.PAutState.sink = Sum.inr ()

inductive DPDA.RelPath {Q S : Type} (R : PAutState Q → S → PAutState Q → Prop) : PAutState Q → List S → PAutState Q → Prop

A path through a stack-reading relation. Symbols are read top-to-bottom.

• nil {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} (p : PAutState Q) : RelPath R p [] p
• cons {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {p m r : PAutState Q} {Z : S} {γ : List S} : R p Z m → RelPath R m γ r → RelPath R p (Z :: γ) r

theorem DPDA.RelPath.append {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {p m r : PAutState Q} {γ δ : List S} (h₁ : RelPath R p γ m) (h₂ : RelPath R m δ r) : RelPath R p (γ ++ δ) r

theorem DPDA.RelPath.of_append_left {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {p r : PAutState Q} {γ δ : List S} (h : RelPath R p (γ ++ δ) r) : ∃ (m : PAutState Q), RelPath R p γ m ∧ RelPath R m δ r

theorem DPDA.RelPath.mono {Q S : Type} {R₁ R₂ : PAutState Q → S → PAutState Q → Prop} (hsub : ∀ {p : PAutState Q} {Z : S} {r : PAutState Q}, R₁ p Z r → R₂ p Z r) {p r : PAutState Q} {γ : List S} (h : RelPath R₁ p γ r) : RelPath R₂ p γ r

def DPDA.relNFA {Q S : Type} (R : PAutState Q → S → PAutState Q → Prop) (start : PAutState Q) (accept : Set (PAutState Q)) : NFA S (PAutState Q)

The NFA whose transitions are exactly a stack-reading relation.

Equations

• DPDA.relNFA R start accept = { step := fun (p : DPDA.PAutState Q) (Z : S) => {r : DPDA.PAutState Q | R p Z r}, start := {start}, accept := accept }

theorem DPDA.relPath_iff_nonempty_nfa_path {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {start : PAutState Q} {accept : Set (PAutState Q)} {p r : PAutState Q} {γ : List S} : RelPath R p γ r ↔ Nonempty ((relNFA R start accept).Path p r γ)

def DPDA.relDFA {Q S : Type} (R : PAutState Q → S → PAutState Q → Prop) (start : PAutState Q) (accept : Set (PAutState Q)) : DFA S (Set (PAutState Q))

The DFA obtained by subset construction from a stack-reading relation.

Equations

• DPDA.relDFA R start accept = (DPDA.relNFA R start accept).toDFA

theorem DPDA.relDFA_accepts_iff {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {start : PAutState Q} {accept : Set (PAutState Q)} {γ : List S} : γ ∈ (relDFA R start accept).accepts ↔ ∃ r ∈ accept, RelPath R start γ r

Correctness of the relation DFA: it accepts exactly the stacks labeling a path from start to an accepting P-automaton state.

theorem DPDA.relDFA_evalFrom_control_iff {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {q : Q} {accept : Set (PAutState Q)} {γ : List S} : (relDFA R (PAutState.control q) accept).evalFrom (relDFA R (PAutState.control q) accept).start γ ∈ (relDFA R (PAutState.control q) accept).accept ↔ ∃ r ∈ accept, RelPath R (PAutState.control q) γ r

The relation recognized from an original control state by the relation DFA.

def DPDA.EpsilonStepSaturated {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (R : PAutState Q → S → PAutState Q → Prop) : Prop

A relation is saturated for the epsilon rules of a DPDA if every pushdown epsilon step can be summarized by a single stack-reading transition.

Equations

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

def DPDA.epsilonSaturationRel {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (base : PAutState Q → S → PAutState Q → Prop) : PAutState Q → S → PAutState Q → Prop

Least saturated relation containing a base P-automaton relation.

Equations

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

theorem DPDA.base_subset_epsilonSaturationRel {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : PAutState Q → S → PAutState Q → Prop} {p : PAutState Q} {Z : S} {r : PAutState Q} : base p Z r → M.epsilonSaturationRel base p Z r

theorem DPDA.epsilonSaturationRel_saturated {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (base : PAutState Q → S → PAutState Q → Prop) : M.EpsilonStepSaturated (M.epsilonSaturationRel base)

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

Base target relation for stopping epsilon phases. A control state with no epsilon transition on the current top symbol is a target; the sink consumes the unexamined suffix.

Equations

• M.stopTargetBase (Sum.inl q) x✝ (Sum.inr PUnit.unit) = (M.epsilon_transition q x✝ = none)
• M.stopTargetBase (Sum.inr PUnit.unit) x✝ (Sum.inr PUnit.unit) = True
• M.stopTargetBase x✝² x✝¹ x✝ = False

def DPDA.stopTargetAccept {Q : Type} : Set (PAutState Q)

Empty stack is stable for every control state; after detecting a stable top, the sink accepts the remaining suffix.

Equations

• DPDA.stopTargetAccept = Set.univ

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

Saturated relation recognizing stacks from which the forced epsilon phase reaches a stable configuration.

Equations

• M.stopSaturationRel = M.epsilonSaturationRel M.stopTargetBase

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

Base target relation for epsilon reachability to a final state.

Equations

• M.finalTargetBase (Sum.inl q) x✝ (Sum.inr PUnit.unit) = (q ∈ M.final_states)
• M.finalTargetBase (Sum.inr PUnit.unit) x✝ (Sum.inr PUnit.unit) = True
• M.finalTargetBase x✝² x✝¹ x✝ = False

def DPDA.finalTargetAccept {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Set (PAutState Q)

Accepting P-automaton states for final-state epsilon reachability.

Equations

• M.finalTargetAccept (Sum.inl q) = (q ∈ M.final_states)
• M.finalTargetAccept (Sum.inr PUnit.unit) = True

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

Saturated relation recognizing stacks from which epsilon reachability can hit an original final state.

Equations

• M.finalSaturationRel = M.epsilonSaturationRel M.finalTargetBase

def DPDA.stopSaturationDFA {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) : DFA S (Set (PAutState Q))

Candidate DFA for the stop-lookahead language at control state q.

Equations

• M.stopSaturationDFA q = DPDA.relDFA M.stopSaturationRel (DPDA.PAutState.control q) DPDA.stopTargetAccept

def DPDA.finalSaturationDFA {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) : DFA S (Set (PAutState Q))

Candidate DFA for the epsilon-final-reachability language at control state q.

Equations

• M.finalSaturationDFA q = DPDA.relDFA M.finalSaturationRel (DPDA.PAutState.control q) M.finalTargetAccept

theorem DPDA.stopSaturationDFA_accepts_iff {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.stopSaturationDFA q).accepts ↔ ∃ (r : PAutState Q), RelPath M.stopSaturationRel (PAutState.control q) γ r

def DPDA.RelationPreservesTarget {Q S : Type} (R : PAutState Q → S → PAutState Q → Prop) (Target : PAutState Q → List S → Prop) : Prop

A relation preserves a target stack language if one transition consumes one stack symbol while preserving target membership for every suffix.

Equations

• DPDA.RelationPreservesTarget R Target = ∀ {p r : DPDA.PAutState Q} {Z : S}, R p Z r → ∀ (δ : List S), Target r δ → Target p (Z :: δ)

theorem DPDA.RelPath.preservesTarget {Q S : Type} {R : PAutState Q → S → PAutState Q → Prop} {Target : PAutState Q → List S → Prop} (hR : RelationPreservesTarget R Target) {p r : PAutState Q} {γ δ : List S} (hpath : RelPath R p γ r) (htarget : Target r δ) : Target p (γ ++ δ)

def DPDA.stopTarget {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PAutState Q → List S → Prop

Semantic target for stopping: controls represent genuine DPDA configurations; the sink means the target has already been reached and the rest of the stack is ignored.

Equations

• M.stopTarget (Sum.inl q) x✝ = ∃ (cstable : DPDA.EpsilonConf Q S), M.EpsilonStopsAt (q, x✝) cstable
• M.stopTarget (Sum.inr PUnit.unit) x✝ = True

theorem DPDA.stopTarget_nil {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (r : PAutState Q) : M.stopTarget r []

theorem DPDA.stopSaturationRel_preservesTarget {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : RelationPreservesTarget M.stopSaturationRel M.stopTarget

theorem DPDA.stopSaturationRel_path_sound {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p r : PAutState Q} {γ δ : List S} (hpath : RelPath M.stopSaturationRel p γ r) (htarget : M.stopTarget r δ) : M.stopTarget p (γ ++ δ)

theorem DPDA.stopSaturationDFA_sound {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.stopSaturationDFA q).accepts → ∃ (cstable : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) cstable

theorem DPDA.stopSaturationRel_sink_path {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (γ : List S) : RelPath M.stopSaturationRel PAutState.sink γ PAutState.sink

theorem DPDA.stopSaturationRel_path_of_stable {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : Q} {γ : List S} (hstable : M.EpsilonStable (q, γ)) : ∃ (r : PAutState Q), RelPath M.stopSaturationRel (PAutState.control q) γ r

theorem DPDA.stopSaturationRel_path_of_epsilonStopsAt {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : Q} {γ : List S} {cstable : EpsilonConf Q S} (hstops : M.EpsilonStopsAt (q, γ) cstable) : ∃ (r : PAutState Q), RelPath M.stopSaturationRel (PAutState.control q) γ r

theorem DPDA.stopSaturationDFA_complete {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : (∃ (cstable : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) cstable) → γ ∈ (M.stopSaturationDFA q).accepts

theorem DPDA.stopSaturationDFA_correct {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.stopSaturationDFA q).accepts ↔ ∃ (cstable : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) cstable

theorem DPDA.finalSaturationDFA_accepts_iff {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.finalSaturationDFA q).accepts ↔ ∃ r ∈ M.finalTargetAccept, RelPath M.finalSaturationRel (PAutState.control q) γ r

def DPDA.finalTarget {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PAutState Q → List S → Prop

Semantic target for final-state epsilon reachability.

Equations

• M.finalTarget (Sum.inl q) x✝ = ∃ (qf : Q) (γf : List S), M.EpsilonReaches (q, x✝) (qf, γf) ∧ qf ∈ M.final_states
• M.finalTarget (Sum.inr PUnit.unit) x✝ = True

theorem DPDA.finalTarget_nil_iff {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (r : PAutState Q) : M.finalTarget r [] ↔ r ∈ M.finalTargetAccept

theorem DPDA.finalSaturationRel_preservesTarget {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : RelationPreservesTarget M.finalSaturationRel M.finalTarget

theorem DPDA.finalSaturationRel_path_sound {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p r : PAutState Q} {γ δ : List S} (hpath : RelPath M.finalSaturationRel p γ r) (htarget : M.finalTarget r δ) : M.finalTarget p (γ ++ δ)

theorem DPDA.finalSaturationDFA_sound {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.finalSaturationDFA q).accepts → ∃ (qf : Q) (γf : List S), M.EpsilonReaches (q, γ) (qf, γf) ∧ qf ∈ M.final_states

theorem DPDA.finalSaturationRel_sink_path {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (γ : List S) : RelPath M.finalSaturationRel PAutState.sink γ PAutState.sink

theorem DPDA.finalSaturationRel_path_of_final {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : Q} {γ : List S} (hfinal : q ∈ M.final_states) : ∃ r ∈ M.finalTargetAccept, RelPath M.finalSaturationRel (PAutState.control q) γ r

theorem DPDA.finalSaturationRel_path_of_epsilonReaches_final {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q qf : Q} {γ γf : List S} (hreach : M.EpsilonReaches (q, γ) (qf, γf)) (hfinal : qf ∈ M.final_states) : ∃ r ∈ M.finalTargetAccept, RelPath M.finalSaturationRel (PAutState.control q) γ r

theorem DPDA.finalSaturationDFA_complete {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : (∃ (qf : Q) (γf : List S), M.EpsilonReaches (q, γ) (qf, γf) ∧ qf ∈ M.final_states) → γ ∈ (M.finalSaturationDFA q).accepts

theorem DPDA.finalSaturationDFA_correct {Q S T : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) (γ : List S) : γ ∈ (M.finalSaturationDFA q).accepts ↔ ∃ (qf : Q) (γf : List S), M.EpsilonReaches (q, γ) (qf, γf) ∧ qf ∈ M.final_states