First-final normalization for deterministic pushdown automata

This file equips a DPDA with one extra bit of finite control. The bit records whether an accepting state has already been left since the most recent input-reading transition. Input transitions clear the bit, while epsilon-transitions set it when their source state is accepting. Only an unmarked copy of an original accepting state is accepting.

Consequently the normalized machine recognizes exactly the same language, but no nonempty epsilon-only path can run from one accepting configuration to another. This is the acceptance normalization used in the classical DPDA-to-LR(1) characteristic-grammar construction.

noncomputable def DPDA.firstFinal {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : DPDA (Q × Bool) T S

Add a bit recording whether a final state has already been left during the current epsilon phase. Reading input starts a fresh phase.

Equations

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

def DPDA.firstFinalLift {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (seen : Bool) (c : M.toPDA.conf) : M.firstFinal.toPDA.conf

Lift an original configuration, choosing the value of the first-final bit.

Equations

• M.firstFinalLift seen c = { state := (c.state, seen), input := c.input, stack := c.stack }

def DPDA.firstFinalErase {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : M.firstFinal.toPDA.conf) : M.toPDA.conf

Forget the first-final bit in a normalized configuration.

Equations

• M.firstFinalErase c = { state := c.state.1, input := c.input, stack := c.stack }

@[simp]

theorem DPDA.firstFinalErase_lift {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (seen : Bool) (c : M.toPDA.conf) : M.firstFinalErase (M.firstFinalLift seen c) = c

@[simp]

theorem DPDA.firstFinalLift_initial {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (w : List T) : M.firstFinalLift false { state := M.initial_state, input := w, stack := [M.start_symbol] } = { state := M.firstFinal.initial_state, input := w, stack := [M.firstFinal.start_symbol] }

@[simp]

theorem DPDA.firstFinal_lift_mem_final_iff {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (seen : Bool) (c : M.toPDA.conf) : (M.firstFinalLift seen c).state ∈ M.firstFinal.final_states ↔ seen = false ∧ c.state ∈ M.final_states

One-step simulation

theorem DPDA.firstFinalErase_step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d : M.firstFinal.toPDA.conf} (h : PDA.Reaches₁ c d) : PDA.Reaches₁ (M.firstFinalErase c) (M.firstFinalErase d)

Every normalized step projects to the corresponding original step.

theorem DPDA.firstFinalLift_step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (seen : Bool) {c d : M.toPDA.conf} (h : PDA.Reaches₁ c d) : ∃ (seen' : Bool), PDA.Reaches₁ (M.firstFinalLift seen c) (M.firstFinalLift seen' d) ∧ (seen' = true ↔ c.input = d.input ∧ (seen = true ∨ c.state ∈ M.final_states))

Lift one original step. The returned equation records exactly when the new first-final bit is set: epsilon steps preserve/set it, while input steps clear it.

Multi-step simulation and the seen-final trace invariant

theorem DPDA.firstFinalErase_reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d : M.firstFinal.toPDA.conf} (h : PDA.Reaches c d) : PDA.Reaches (M.firstFinalErase c) (M.firstFinalErase d)

Every normalized run projects to an original run.

theorem DPDA.firstFinalLift_reaches_from_clear {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d : M.toPDA.conf} (h : PDA.Reaches c d) : ∃ (seen : Bool), PDA.Reaches (M.firstFinalLift false c) (M.firstFinalLift seen d) ∧ (seen = true → ∃ (e : M.toPDA.conf), PDA.Reaches (M.firstFinalLift false c) (M.firstFinalLift false e) ∧ e.input = d.input ∧ e.state ∈ M.final_states)

Lift an original run from a clear first-final bit. If the resulting bit is set, the lifted run has already visited an unmarked original final state with the same remaining input as the endpoint. In particular, no input transition has occurred since that visit.

Language preservation

theorem DPDA.firstFinal_acceptsByFinalState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.firstFinal.acceptsByFinalState = M.acceptsByFinalState

First-final normalization preserves final-state acceptance exactly.

No repeated final state in an epsilon phase

theorem DPDA.firstFinal_no_return_through_final {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : Q × Bool} {input output : List T} {γ δ γ' : List S} (hbefore : PDA.Reaches { state := q, input := input, stack := γ } { state := p, input := output, stack := δ }) (hfinal : p ∈ M.firstFinal.final_states) (hafter : Relation.TransGen PDA.Reaches₁ { state := p, input := output, stack := δ } { state := q, input := input, stack := γ' }) : False

A same-input computation cannot pass through a normalized final state and then return nontrivially to the state from which it started. Before the final state the first-final marker is either already set, contradicting finality, or it is clear; in the latter case leaving the final state sets it and the nonempty return cannot restore the original clear marker.

theorem DPDA.firstFinal_no_final_to_final_epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : Q × Bool} {input : List T} {γ δ : List S} (hq : q ∈ M.firstFinal.final_states) (hreach : Relation.TransGen PDA.Reaches₁ { state := q, input := input, stack := γ } { state := p, input := input, stack := δ }) : p ∉ M.firstFinal.final_states

No nonempty run starting in a normalized final configuration and consuming no input can end in another normalized final configuration. Stating the path with Relation.TransGen excludes the reflexive zero-step path.