Predictive first moves of the characteristic PDA

The final-state-to-empty-stack PDA is nondeterministic only at a normalized final state, where it may either continue simulating the DPDA or enter its stack-draining state. For a computation segment with a fixed target state, one symbol of input lookahead makes the first productive move unique. The normalizer's no-repeated-final theorem rules out the sole epsilon/epsilon ambiguity at end of input.

@[reducible, inline]

abbrev DPDA_to_LR.EState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

Equations

• DPDA_to_LR.EState M = (Q × Bool ⊕ Fin 2)

@[reducible, inline]

abbrev DPDA_to_LR.EStack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

Equations

• DPDA_to_LR.EStack M = Option S

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

A transition signature records whether the move consumes the leading input symbol, together with its next control state and replacement stack.

• consumes : Bool
• nextState : EState M
• replacement : List (EStack M)

inductive DPDA_to_LR.HasFirstMove {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : EState M) (Z : EStack M) : List T → FirstMoveSignature M → Prop

A first-move signature is enabled at (q,input,Z).

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q : EState M} {Z : EStack M} (a : T) (tail : List T) (p : EState M) (alpha : List (EStack M)) (h : (p, alpha) ∈ (emptyStackPDA M).transition_fun q a Z) : HasFirstMove M q Z (a :: tail) { consumes := true, nextState := p, replacement := alpha }
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q : EState M} {Z : EStack M} (input : List T) (p : EState M) (alpha : List (EStack M)) (h : (p, alpha) ∈ (emptyStackPDA M).transition_fun' q Z) : HasFirstMove M q Z input { consumes := false, nextState := p, replacement := alpha }

def DPDA_to_LR.inputAfter {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (sig : FirstMoveSignature M) (input : List T) : List T

Remaining input after a move with the given signature.

Equations

• DPDA_to_LR.inputAfter M sig input = if sig.consumes = true then List.drop 1 input else input

def DPDA_to_LR.ProductiveFirstMove {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : EState M) (Z : EStack M) (input : List T) (target : EState M) (sig : FirstMoveSignature M) : Prop

An enabled first move is productive for a fixed characteristic-nonterminal target when its successor can net-pop the replacement stack and finish in that target state.

Equations

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

Drain and simulation path facts

theorem DPDA_to_LR.drain_reaches_input_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {input : List T} {stack : List (EStack M)} {c : (emptyStackPDA M).conf} (h : PDA.Reaches { state := Sum.inr 1, input := input, stack := stack } c) : c.input = input

Once the FS→ES construction enters its drain state, it never changes the remaining input.

theorem DPDA_to_LR.simulation_reaches_drain_witness {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : Q × Bool} {stack : List S} {drainStack : List (EStack M)} (h : PDA.Reaches { state := Sum.inl q, input := [], stack := List.map some stack } { state := Sum.inr 1, input := [], stack := drainStack }) : ∃ (p : Q × Bool) (delta : List S), p ∈ M.firstFinal.final_states ∧ PDA.Reaches { state := q, input := [], stack := stack } { state := p, input := [], stack := delta }

While the FS→ES machine remains in simulation states with a stack made of some symbols, its path projects to the normalized DPDA. If it reaches the drain state, some normalized final configuration was reached first.