Forward traces of zero-visible leftmost descent

A zero-visible grammar tail alternates cost-free structural changes with epsilon transitions of the normalized empty-stack PDA. The grammar target state is irrelevant to the physical cut, but the boundary between the displayed stack and the hidden zipper context is essential. The positions below retain exactly that boundary.

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

Physical position of a zero-visible leftmost descent. Grammar return targets are omitted; displayed stack and hidden context remain separate.

• root {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} : LeftmostEpsilonPosition M
• single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (state : State M) (top : StackSymbol M) (context : List (StackSymbol M)) : LeftmostEpsilonPosition M
• list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (state : State M) (displayed context : List (StackSymbol M)) : LeftmostEpsilonPosition M

def DPDA_to_LR.LeftmostEpsilonPosition.conf {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (input : List T) : LeftmostEpsilonPosition M → (emptyStackPDA M).conf

The concrete PDA configuration represented by a position on a chosen unconsumed input tail.

Equations

• One or more equations did not get rendered due to their size.
• DPDA_to_LR.LeftmostEpsilonPosition.conf M input (DPDA_to_LR.LeftmostEpsilonPosition.single q Z context) = { state := q, input := input, stack := Z :: context }
• DPDA_to_LR.LeftmostEpsilonPosition.conf M input (DPDA_to_LR.LeftmostEpsilonPosition.list q gamma context) = { state := q, input := input, stack := gamma ++ context }

def DPDA_to_LR.leftmostEpsilonPositionOf {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (A : Nonterminal M) (context : List (StackSymbol M)) : LeftmostEpsilonPosition M

Forget the target-state index of a characteristic nonterminal while retaining its physical displayed-stack boundary.

Equations

• DPDA_to_LR.leftmostEpsilonPositionOf M PDA_to_CFG.N.start context = DPDA_to_LR.LeftmostEpsilonPosition.root
• DPDA_to_LR.leftmostEpsilonPositionOf M (PDA_to_CFG.N.single q Z a) context = DPDA_to_LR.LeftmostEpsilonPosition.single q Z context
• DPDA_to_LR.leftmostEpsilonPositionOf M (PDA_to_CFG.N.list q gamma a) context = DPDA_to_LR.LeftmostEpsilonPosition.list q gamma context

theorem DPDA_to_LR.leftmostEpsilonPositionOf_conf {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (A : Nonterminal M) (context : List (StackSymbol M)) (input : List T) : LeftmostEpsilonPosition.conf M input (leftmostEpsilonPositionOf M A context) = { state := spineCutState M A, input := input, stack := spineCutStack M A context }

Forgetting the grammar target preserves the exact concrete cut.

inductive DPDA_to_LR.LeftmostEpsilonStep {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : LeftmostEpsilonPosition M → LeftmostEpsilonPosition M → Prop

One forward zero-visible event. start and split only change the grammar view of a physical cut; epsilon is one actual PDA step.

• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} : LeftmostEpsilonStep M LeftmostEpsilonPosition.root (LeftmostEpsilonPosition.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] [])
• split {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q : State M} {Z : StackSymbol M} {gamma context : List (StackSymbol M)} : LeftmostEpsilonStep M (LeftmostEpsilonPosition.list q (Z :: gamma) context) (LeftmostEpsilonPosition.single q Z (gamma ++ context))
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q next : State M} {Z : StackSymbol M} {replacement context : List (StackSymbol M)} (transition : (next, replacement) ∈ (emptyStackPDA M).transition_fun' q Z) : LeftmostEpsilonStep M (LeftmostEpsilonPosition.single q Z context) (LeftmostEpsilonPosition.list next replacement context)

inductive DPDA_to_LR.LeftmostEpsilonTrace {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : LeftmostEpsilonPosition M → LeftmostEpsilonPosition M → Prop

Forward reflexive-transitive closure, oriented so induction exposes the first structural event.

• refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (position : LeftmostEpsilonPosition M) : LeftmostEpsilonTrace M position position
• head {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {start middle finish : LeftmostEpsilonPosition M} (first : LeftmostEpsilonStep M start middle) (rest : LeftmostEpsilonTrace M middle finish) : LeftmostEpsilonTrace M start finish

theorem DPDA_to_LR.LeftmostEpsilonTrace.snoc {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start middle finish : LeftmostEpsilonPosition M} (trace : LeftmostEpsilonTrace M start middle) (last : LeftmostEpsilonStep M middle finish) : LeftmostEpsilonTrace M start finish

Append one structural event to a forward trace.

theorem DPDA_to_LR.ZeroVisibleTail.leftmostEpsilonTrace {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {anchor current : Nonterminal M} {anchorSuffix currentSuffix : List T} {anchorContext currentContext : List (StackSymbol M)} (h : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) : LeftmostEpsilonTrace M (leftmostEpsilonPositionOf M anchor anchorContext) (leftmostEpsilonPositionOf M current currentContext)

A zero-visible tail forgets to a forward leftmost trace.

theorem DPDA_to_LR.LeftmostEpsilonStep.reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start finish : LeftmostEpsilonPosition M} (step : LeftmostEpsilonStep M start finish) (input : List T) : PDA.Reaches (LeftmostEpsilonPosition.conf M input start) (LeftmostEpsilonPosition.conf M input finish)

Every structural event is ordinary reachability on any fixed input tail. The two grammar-only events are literal equality of physical cuts.

theorem DPDA_to_LR.LeftmostEpsilonTrace.reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start finish : LeftmostEpsilonPosition M} (trace : LeftmostEpsilonTrace M start finish) (input : List T) : PDA.Reaches (LeftmostEpsilonPosition.conf M input start) (LeftmostEpsilonPosition.conf M input finish)

Operational realization of a complete forward trace.

def DPDA_to_LR.LeftmostEpsilonPosition.state' {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : LeftmostEpsilonPosition M → State M

Control state carried by a leftmost epsilon position.

Equations

• DPDA_to_LR.LeftmostEpsilonPosition.state' M DPDA_to_LR.LeftmostEpsilonPosition.root = (DPDA_to_LR.emptyStackPDA M).initial_state
• DPDA_to_LR.LeftmostEpsilonPosition.state' M (DPDA_to_LR.LeftmostEpsilonPosition.single q Z context) = q
• DPDA_to_LR.LeftmostEpsilonPosition.state' M (DPDA_to_LR.LeftmostEpsilonPosition.list q gamma context) = q

def DPDA_to_LR.LeftmostEpsilonPosition.upper {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : LeftmostEpsilonPosition M → List (StackSymbol M)

Stack prefix displayed by a leftmost epsilon position.

Equations

• DPDA_to_LR.LeftmostEpsilonPosition.upper M DPDA_to_LR.LeftmostEpsilonPosition.root = [(DPDA_to_LR.emptyStackPDA M).start_symbol]
• DPDA_to_LR.LeftmostEpsilonPosition.upper M (DPDA_to_LR.LeftmostEpsilonPosition.single q Z context) = [Z]
• DPDA_to_LR.LeftmostEpsilonPosition.upper M (DPDA_to_LR.LeftmostEpsilonPosition.list q gamma context) = gamma

def DPDA_to_LR.LeftmostEpsilonPosition.context' {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : LeftmostEpsilonPosition M → List (StackSymbol M)

Hidden stack context carried below a leftmost epsilon position.

Equations

• DPDA_to_LR.LeftmostEpsilonPosition.context' M DPDA_to_LR.LeftmostEpsilonPosition.root = []
• DPDA_to_LR.LeftmostEpsilonPosition.context' M (DPDA_to_LR.LeftmostEpsilonPosition.single q Z context) = context
• DPDA_to_LR.LeftmostEpsilonPosition.context' M (DPDA_to_LR.LeftmostEpsilonPosition.list q gamma context) = context

theorem DPDA_to_LR.LeftmostEpsilonPosition.conf_nil_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (position : LeftmostEpsilonPosition M) : conf M [] position = { state := state' M position, input := [], stack := upper M position ++ context' M position }

At empty input a position is its displayed prefix followed by its hidden context.

theorem DPDA_to_LR.retainedFrameRun_trans {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n m : ℕ} {a b c : P.conf} (h₁ : P.RetainedFrameRun frame n a b) (h₂ : P.RetainedFrameRun frame m b c) : P.RetainedFrameRun frame (n + m) a c

Concatenate two runs which retain the same stack frame.

theorem DPDA_to_LR.LeftmostEpsilonStep.retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start finish : LeftmostEpsilonPosition M} (step : LeftmostEpsilonStep M start finish) {frame added : List (StackSymbol M)} (hcontext : LeftmostEpsilonPosition.context' M start = added ++ frame) : ∃ (n : ℕ) (added' : List (StackSymbol M)), LeftmostEpsilonPosition.context' M finish = added' ++ frame ∧ (emptyStackPDA M).RetainedFrameRun frame n (LeftmostEpsilonPosition.conf M [] start) (LeftmostEpsilonPosition.conf M [] finish)

Every structural step preserves any selected suffix of the hidden context. The returned prefix records what was added above that suffix.

theorem DPDA_to_LR.LeftmostEpsilonTrace.retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start finish : LeftmostEpsilonPosition M} (trace : LeftmostEpsilonTrace M start finish) {frame added : List (StackSymbol M)} (hcontext : LeftmostEpsilonPosition.context' M start = added ++ frame) : ∃ (n : ℕ) (added' : List (StackSymbol M)), LeftmostEpsilonPosition.context' M finish = added' ++ frame ∧ (emptyStackPDA M).RetainedFrameRun frame n (LeftmostEpsilonPosition.conf M [] start) (LeftmostEpsilonPosition.conf M [] finish)

A whole leftmost epsilon trace preserves any selected suffix of the starting hidden context.

theorem DPDA_to_LR.LeftmostEpsilonTrace.fromSingle_exists_retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : State M} {Z : StackSymbol M} {context : List (StackSymbol M)} {finish : LeftmostEpsilonPosition M} (trace : LeftmostEpsilonTrace M (LeftmostEpsilonPosition.single q Z context) finish) : ∃ (n : ℕ) (added : List (StackSymbol M)), LeftmostEpsilonPosition.context' M finish = added ++ context ∧ (emptyStackPDA M).RetainedFrameRun context n (LeftmostEpsilonPosition.conf M [] (LeftmostEpsilonPosition.single q Z context)) (LeftmostEpsilonPosition.conf M [] finish)

A trace beginning at a single-stack-symbol position retains its entire hidden context.

theorem DPDA_to_LR.leftmostEpsilonTrace_productive_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start finish₁ finish₂ : LeftmostEpsilonPosition M} {final₁ final₂ : State M} {suffix₁ suffix₂ whole₁ whole₂ : List T} (trace₁ : LeftmostEpsilonTrace M start finish₁) (trace₂ : LeftmostEpsilonTrace M start finish₂) (global₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₁, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₁ start)) (global₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₂, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₂ start)) (useful₁ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₁ finish₁) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₂ finish₂) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : LeftmostEpsilonTrace M finish₁ finish₂ ∨ LeftmostEpsilonTrace M finish₂ finish₁

Two productive forward zero-visible traces from one structural position are prefix-comparable. The endpoints and the untouched input tails may differ; one-symbol lookahead and global usefulness synchronize every actual epsilon transition, while start and split align definitionally.

theorem DPDA_to_LR.leftmostEpsilonTrace_empty_state_unique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start : LeftmostEpsilonPosition M} {q₁ q₂ final₁ final₂ : State M} {context₁ context₂ : List (StackSymbol M)} {suffix₁ suffix₂ whole₁ whole₂ : List T} (trace₁ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.list q₁ [] context₁)) (trace₂ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.list q₂ [] context₂)) (global₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₁, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₁ start)) (global₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₂, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₂ start)) (useful₁ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₁ (LeftmostEpsilonPosition.list q₁ [] context₁)) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₂ (LeftmostEpsilonPosition.list q₂ [] context₂)) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂

Productive zero-visible traces from the same structural position and with the same one-symbol lookahead have the same empty-list return state.

The theorem is stronger than equal-count synchronization: the two traces may contain different numbers of epsilon transitions. Forward structural induction rules this out before the displayed stack first becomes empty.

theorem DPDA_to_LR.leftmostEpsilonTrace_converging_epsilon_heads_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {start : LeftmostEpsilonPosition M} {q₁ q₂ next final₁ final₂ : State M} {Z₁ Z₂ : StackSymbol M} {gamma context₁ context₂ : List (StackSymbol M)} {suffix₁ suffix₂ whole₁ whole₂ : List T} (trace₁ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.single q₁ Z₁ context₁)) (trace₂ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.single q₂ Z₂ context₂)) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (global₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₁, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₁ start)) (global₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₂, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₂ start)) (useful₁ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₁ (LeftmostEpsilonPosition.list next gamma context₁)) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₂ (LeftmostEpsilonPosition.list next gamma context₂)) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Two productive leftmost epsilon traces which converge through epsilon transitions to the same displayed list child have equal source state and exposed stack symbol.

The traces may have different hidden stack contexts and different unconsumed input tails. It is enough that their tails have the same one-symbol lookahead and that each child cut has an empty-stack continuation.