Operational interpretation of active characteristic spines

ActiveSpine remembers the partial-tree ancestry of a rightmost-reachable nonterminal. For the LR argument we also need to know how a chosen terminal completion of the visible prefix is divided among the edges of that ancestry. OperationalSpine records precisely that extra information. In particular, it retains an operational Focused cut at every ancestor rather than only at the final active node.

inductive DPDA_to_LR.OperationalSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → Nonterminal M → List T → List T → Prop

An active derivation spine equipped with a concrete terminal completion of every prefix on the root-to-active path.

• root {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} : OperationalSpine M [] (characteristicGrammar M).initial [] []
• descend {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p₀ alpha beta : List (symbol T (Nonterminal M))} {parent child : Nonterminal M} {t z preWord leftWord : List T} {r : Nonterminal M × List (symbol T (Nonterminal M))} (parentSpine : OperationalSpine M p₀ parent t preWord) (hr : r ∈ (characteristicGrammar M).rules) (hlhs : r.1 = parent) (hrhs : r.2 = alpha ++ [symbol.nonterminal child] ++ beta) (halpha : (characteristicGrammar M).DerivesRightmost alpha (List.map symbol.terminal leftWord)) (hbeta : (characteristicGrammar M).DerivesRightmost beta (List.map symbol.terminal z)) : OperationalSpine M (p₀ ++ alpha) child (z ++ t) (preWord ++ leftWord)

theorem DPDA_to_LR.OperationalSpine.activeSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s preWord : List T} (h : OperationalSpine M p A s preWord) : ActiveSpine M p A s

Forgetting terminal-completion data recovers the underlying ancestry.

theorem DPDA_to_LR.OperationalSpine.prefixDerives {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s preWord : List T} (h : OperationalSpine M p A s preWord) : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)

The last index really is a terminal rightmost completion of the visible prefix.

theorem DPDA_to_LR.OperationalSpine.focused {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s preWord : List T} (h : OperationalSpine M p A s preWord) : Focused M A preWord s

The operational meaning of the final active occurrence, with the exact prefix word accumulated by the spine.

theorem DPDA_to_LR.operationalSpine_of_activeSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s preWord : List T} (hspine : ActiveSpine M p A s) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : OperationalSpine M p A s preWord

Equip an ancestry spine with any concrete terminal completion of its visible prefix. The append-splitting theorem makes every edge yield explicit.

theorem DPDA_to_LR.operationalSpine_of_prehandle {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s preWord : List T} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : OperationalSpine M p A s preWord

Direct operational interpretation of a reachable prehandle and a chosen terminal completion of its prefix.