Langlib

Langlib.Grammars.LR.Equivalence.DPDAToLR.ZeroVisibleSpine

Zero-visible tails of operational characteristic spines #

An OperationalSpine deliberately retains a grammar rule in its generic descend constructor. This file normalizes that rule to one of the five nonbase characteristic-rule shapes and, at the same time, records the hidden outer stack context of the active occurrence.

The normalized trace makes the important dichotomy syntactic. A read or a split-right descent appends one visible symbol to the prehandle. Start, epsilon, and split-left descents leave the prehandle unchanged. The latter three constructors form ZeroVisibleTail. Along such a tail, split-left is the only constructor that changes the hidden context, and it does so by prepending the saved replacement tail.

source
inductive DPDA_to_LR.ConcreteOperationalSpine {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 → List (StackSymbol M) → Prop

A normalized operational spine carrying the outer stack context of its active occurrence. At start the context index is a harmless [] convention; every other constructor has its literal zipper meaning.

Instances For
    source
    inductive DPDA_to_LR.FocusedExact {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) :
    Nonterminal M → List T → List T → List (StackSymbol M) → Prop

    Exact-context version of Focused. Unlike Focused, the outer context is an index, so consumers can relate it to the context carried by a concrete spine without recovering an unrelated existential witness.

    Instances For
      source
      theorem DPDA_to_LR.FocusedExact.focused {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {A : Nonterminal M} {preWord postWord : List T} {context : List (StackSymbol M)} (h : FocusedExact M A preWord postWord context) :
      Focused M A preWord postWord

      Forgetting the exact context index gives the ordinary zipper invariant.

      source
      theorem DPDA_to_LR.ConcreteOperationalSpine.focusedExact {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M p A suffix preWord context) :
      FocusedExact M A preWord suffix context

      The context index of a normalized concrete spine has its exact operational zipper meaning.

      source
      theorem DPDA_to_LR.ConcreteOperationalSpine.operationalSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M p A suffix preWord context) :
      OperationalSpine M p A suffix preWord

      Forgetting normalization and the hidden-context index recovers the original operational spine.

      source
      theorem DPDA_to_LR.concreteOperationalSpine_of_operationalSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} (h : OperationalSpine M p A suffix preWord) :
      ∃ (context : List (StackSymbol M)), ConcreteOperationalSpine M p A suffix preWord context

      Normalize every generic operational spine and recover its literal hidden outer context.

      source
      theorem DPDA_to_LR.concreteOperationalSpine_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} {suffix preWord : List T} (hspine : ActiveSpine M p A suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) :
      ∃ (context : List (StackSymbol M)), ConcreteOperationalSpine M p A suffix preWord context

      Direct normalization interface for an active spine and a chosen terminal completion of its visible prefix.

      source
      theorem DPDA_to_LR.concreteOperationalSpine_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} {suffix preWord : List T} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal suffix)) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) :
      ∃ (context : List (StackSymbol M)), ConcreteOperationalSpine M p A suffix preWord context

      Reachability-specialized normalization interface.

      source
      def DPDA_to_LR.spineCutState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) :
      Nonterminal M → State M

      State component of the operational cut represented by an active characteristic nonterminal.

      Equations
      Instances For
        source
        def DPDA_to_LR.spineCutStack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) :
        Nonterminal M → List (StackSymbol M) → List (StackSymbol M)

        Stack component of the operational cut. The root convention agrees with the initial configuration of emptyStackPDA.

        Equations
        Instances For
          source
          inductive DPDA_to_LR.ZeroVisibleTail {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 : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)) :
          Nonterminal M → List T → List (StackSymbol M) → Prop

          A suffix of a normalized spine containing no visible descent. Its only proper constructors are exactly start, epsilon, and split-left. The complete syntactic witnesses are retained, so downstream arguments can distinguish a literal epsilon transition from a context-only split.

          Instances For
            source
            theorem DPDA_to_LR.ZeroVisibleTail.context_eq_append {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) :
            ∃ (added : List (StackSymbol M)), currentContext = added ++ anchorContext

            Hidden contexts along a zero-visible tail are obtained only by prepending blocks to the anchor context.

            source
            theorem DPDA_to_LR.ZeroVisibleTail.reaches_cut {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) :
            PDA.Reaches { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

            The zero-visible tail is also a literal same-input PDA computation between its endpoint cuts. Start and split-left merely change the grammar view of the same physical configuration; epsilon contributes its one transition step.

            source
            inductive DPDA_to_LR.VisibleSpineAnchor {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 → List (StackSymbol M) → Prop

            The node immediately before a maximal zero-visible tail. It is either the root or the child of the last visible event (read or split-right).

            Instances For
              source
              theorem DPDA_to_LR.VisibleSpineAnchor.concreteOperationalSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} {context : List (StackSymbol M)} (h : VisibleSpineAnchor M p A suffix preWord context) :
              ConcreteOperationalSpine M p A suffix preWord context

              A visible anchor is itself a concrete normalized spine.

              source
              theorem DPDA_to_LR.ZeroVisibleTail.concreteOperationalSpine {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) (hanchor : ConcreteOperationalSpine M p anchor anchorSuffix preWord anchorContext) :
              ConcreteOperationalSpine M p current currentSuffix preWord currentContext

              Extending a concrete anchor by a zero-visible tail reconstructs a concrete spine at the endpoint.

              source
              theorem DPDA_to_LR.ConcreteOperationalSpine.zeroVisibleDecomposition {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M p A suffix preWord context) :
              ∃ (anchor : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)), VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext ∧ ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext A suffix context

              Every concrete spine factors at the last visible event into a visible anchor followed by a maximal tail of start/epsilon/split-left descents.