Langlib

Langlib.Grammars.LR.Equivalence.DPDAToLR.ActiveSpine

Active derivation spines of the characteristic grammar #

Focused records the operational meaning of an active characteristic nonterminal, but intentionally hides the partial derivation tree which led to that occurrence. Handle-collision arguments need that tree path: in particular, an empty-list occurrence has forgotten the return state of its parent unless the introducing edge is retained.

ActiveSpine is the minimal such path. Every descent remembers the parent active occurrence, the exact retained rule, the position of the child in its right-hand side, and the terminal completion of the part to the child's right. Its indices are exactly the visible prehandle prefix and terminal suffix.

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

The root-to-active-node path in a partial rightmost derivation tree.

Instances For
    source
    theorem DPDA_to_LR.ActiveSpine.derivesRightmost {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 : List T} (h : ActiveSpine M p A s) :
    (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)

    A stored spine reconstructs its visible reachable prehandle.

    source
    theorem DPDA_to_LR.activeSpine_of_derivesRightmostIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {n : ℕ} {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s : List T} (h : (characteristicGrammar M).DerivesRightmostIn n [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) :
    ActiveSpine M p A s

    Counted completeness of the active-spine representation.

    source
    theorem DPDA_to_LR.activeSpine_of_derivesRightmost {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 : List T} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) :
    ActiveSpine M p A s

    Every reachable characteristic prehandle has a canonical active-node ancestry spine (up to proof irrelevance).

    source
    theorem DPDA_to_LR.activeSpine_iff_derivesRightmost {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 : List T} :
    ActiveSpine M p A s ↔ (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)

    Reachability and existence of an active derivation spine are equivalent.

    Normalized final edges #

    source
    inductive DPDA_to_LR.ActiveEdge {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 (symbol T (Nonterminal M)) → Nonterminal M → List T → Prop

    One characteristic rule edge on the active tree spine, normalized to its semantic rule shape. The indices record both the parent and child visible prehandles.

    Instances For