Source heads along active characteristic spines

The visible prefix alone does not determine an arbitrary active occurrence: an epsilon edge may leave the terminal prefix unchanged. What is unique is the source of two introducing edges for the same active list child. The parent spines retained by Introduces are the history needed to state that property without losing the partial derivation tree.

inductive DPDA_to_LR.ActiveParentKind : Type

The three kinds of characteristic nonterminal which expose a stack head. The tag is essential: a single-symbol return and a nonempty-list split may have the same operational state and top-of-stack while representing different edges of the characteristic derivation tree.

• start : ActiveParentKind
• single : ActiveParentKind
• list : ActiveParentKind

def DPDA_to_LR.activeDescriptor {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Nonterminal M → Option (ActiveParentKind × State M × StackSymbol M)

Parent kind, state, and exposed stack symbol of a characteristic nonterminal. Empty-list nodes have no exposed source symbol. The grammar root denotes the boot configuration of the normalized empty-stack PDA.

Equations

• DPDA_to_LR.activeDescriptor M PDA_to_CFG.N.start = some (DPDA_to_LR.ActiveParentKind.start, (DPDA_to_LR.emptyStackPDA M).initial_state, (DPDA_to_LR.emptyStackPDA M).start_symbol)
• DPDA_to_LR.activeDescriptor M (PDA_to_CFG.N.single q Z a) = some (DPDA_to_LR.ActiveParentKind.single, q, Z)
• DPDA_to_LR.activeDescriptor M (PDA_to_CFG.N.list q (Z :: tail) a) = some (DPDA_to_LR.ActiveParentKind.list, q, Z)
• DPDA_to_LR.activeDescriptor M (PDA_to_CFG.N.list a [] a_1) = none

def DPDA_to_LR.activeSource {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Nonterminal M → Option (State M × StackSymbol M)

The untagged operational source is occasionally convenient when the parent form is already known.

Equations

• DPDA_to_LR.activeSource M PDA_to_CFG.N.start = some ((DPDA_to_LR.emptyStackPDA M).initial_state, (DPDA_to_LR.emptyStackPDA M).start_symbol)
• DPDA_to_LR.activeSource M (PDA_to_CFG.N.single q Z a) = some (q, Z)
• DPDA_to_LR.activeSource M (PDA_to_CFG.N.list q (Z :: tail) a) = some (q, Z)
• DPDA_to_LR.activeSource M (PDA_to_CFG.N.list a [] a_1) = none

theorem DPDA_to_LR.ActiveSpine.start_eq_nil {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {suffix : List T} (h : ActiveSpine M p PDA_to_CFG.N.start suffix) : p = [] ∧ suffix = []

The start symbol occurs only at the root of an active spine.

def DPDA_to_LR.ActiveHeadUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

History-sensitive head uniqueness required by the reverse-edge argument. The common list child and one symbol of its following input determine the kind and source configuration head of its two possible parent edges.

Equations

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

def DPDA_to_LR.IsEpsilonRule {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (rule : Nonterminal M × List (symbol T (Nonterminal M))) : Prop

A normalized characteristic rule generated by an epsilon transition.

Equations

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

def DPDA_to_LR.EpsilonIntroducingHeadsUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

The exact epsilon-bearing residual of active-head uniqueness. All pairs without an epsilon edge reduce to stable read heads or to syntactic cancellation; the useful-epsilon-cycle argument proves this remaining part.

Equations

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