Useful cycles in deterministic pushdown computations

A nonempty cycle in a deterministic computation cannot occur before a configuration from which no step is possible. The characteristic-grammar proof uses this elementary fact after two competing active spines have been projected to the same normalized-DPDA computation.

theorem DPDA.toPDA_no_cycle_before_stuck {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d : M.toPDA.conf} (hcycle : Relation.TransGen PDA.Reaches₁ c c) (hreach : PDA.Reaches c d) (hstuck : ∀ (e : M.toPDA.conf), ¬PDA.Reaches₁ d e) : False

A deterministic run which contains a nonempty cycle cannot later reach a configuration with no outgoing transition.

theorem DPDA.toPDA_no_cycle_before_empty_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c : M.toPDA.conf} {q : Q} (hcycle : Relation.TransGen PDA.Reaches₁ c c) (hreach : PDA.Reaches c { state := q, input := [], stack := [] }) : False

In particular, a nonempty deterministic cycle cannot have a continuation to an empty-stack configuration.

theorem DPDA.toPDA_predecessor_eq_of_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c₁ c₂ next : M.toPDA.conf} {final : Q} (hcomparable : PDA.Reaches c₁ c₂ ∨ PDA.Reaches c₂ c₁) (hstep₁ : PDA.Reaches₁ c₁ next) (hstep₂ : PDA.Reaches₁ c₂ next) (huseful : PDA.Reaches next { state := final, input := [], stack := [] }) : c₁ = c₂

Two comparable configurations on a useful deterministic run cannot have distinct one-step edges which merge immediately. Otherwise the longer prefix, followed by its edge to the common successor, forms a nonempty cycle before the successor's empty-stack continuation.

theorem DPDA.toPDA_no_useful_stack_growth {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q final : Q} {base extra context : List S} {input : List T} (hgrowth : PDA.Reaches { state := q, input := [], stack := base } { state := q, input := [], stack := base ++ extra }) (hextra : extra ≠ []) (huseful : PDA.Reaches { state := q, input := input, stack := base ++ extra ++ context } { state := final, input := [], stack := [] }) : False

A deterministic pushdown computation cannot usefully repeat a stack growth segment. The segment starts and ends with the same state and exposed stack prefix, inserting a nonempty block immediately below that prefix. By stack locality it can be repeated arbitrarily often; determinism would then place an arbitrarily long growth run before a fixed finite empty-stack continuation.

theorem DPDA.firstFinal_toPDA_no_stack_growth_before_final {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : Q × Bool} {base extra context targetStack : List S} {input output : List T} (hgrowth : PDA.Reaches { state := q, input := [], stack := base } { state := q, input := [], stack := base ++ extra }) (hextra : extra ≠ []) (hreach : PDA.Reaches { state := q, input := input, stack := base ++ extra ++ context } { state := p, input := output, stack := targetStack }) (hfinal : p ∈ M.firstFinal.final_states) : False

First-final normalization also rules out a repeatable stack-growth segment before a normalized final state, even if the stack has not yet been drained. A sufficiently long repetition contains the finite path to that final state as a prefix. The first-final marker then either was already set, or is set on leaving the final state, and in either case cannot return to the unchanged source state of the repeated segment.