Langlib

Langlib.Grammars.LR.Equivalence.DPDAToLR.VisibleAnchorSemantics

Semantics and alignment of visible spine anchors #

This file is the small, ancestry-preserving interface between normalized spines and paired synchronization. It exposes the exact operational cut of a visible anchor, classifies zero-visible tails according to whether they contain a genuine epsilon transition, and aligns the last visible event of two anchors with the same prefix.

source
theorem DPDA_to_LR.VisibleSpineAnchor.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 : VisibleSpineAnchor M p A suffix preWord context) :
FocusedExact M A preWord suffix context

Exact-context zipper semantics of a visible anchor.

source
theorem DPDA_to_LR.VisibleSpineAnchor.prefixPath {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) :
PDA.Reaches { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := spineCutState M A, input := [], stack := spineCutStack M A context }

The concrete cut of a visible anchor is reached after exactly its completed visible-prefix word.

source
theorem DPDA_to_LR.VisibleSpineAnchor.listContinuation {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} (h : VisibleSpineAnchor M p (PDA_to_CFG.N.list q gamma target) suffix preWord context) :
∃ (final : State M), PDA.Reaches { state := target, input := suffix, stack := context } { state := final, input := [], stack := [] }

A list-valued visible anchor retains an accepting continuation beginning at exactly its indexed outer context.

source
theorem DPDA_to_LR.VisibleSpineAnchor.listSemantics {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} (h : VisibleSpineAnchor M p (PDA_to_CFG.N.list q gamma target) suffix preWord context) :
∃ (final : State M), PDA.Reaches { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := gamma ++ context } ∧ PDA.Reaches { state := target, input := suffix, stack := context } { state := final, input := [], stack := [] }

Combined exact prefix and continuation semantics for a list anchor.

Stable physical source cuts before a read #

source
theorem DPDA_to_LR.concreteSingle_read_source_cuts_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ target₁ target₂ next₁ next₂ : State M} {a : T} {Z₁ Z₂ : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q₁ Z₁ target₁) suffix₁ preWord context₁) (parent₂ : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q₂ Z₂ target₂) suffix₂ preWord context₂) (read₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q₁ a Z₁) (read₂ : (next₂, gamma₂) ∈ (emptyStackPDA M).transition_fun q₂ a Z₂) :
{ state := q₁, input := [], stack := Z₁ :: context₁ } = { state := q₂, input := [], stack := Z₂ :: context₂ }

Two concrete single parents at the same visible/completed prefix which can both read the same next terminal represent the same complete physical source cut, including their saved outer stack contexts.

Epsilon-free and epsilon-bearing zero tails #

source
inductive DPDA_to_LR.EpsilonFreeZeroVisibleTail {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 zero-visible tail built without an epsilon constructor.

Instances For
    source
    inductive DPDA_to_LR.EpsilonBearingZeroVisibleTail {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 zero-visible tail whose retained history contains an epsilon constructor.

    Instances For
      source
      theorem DPDA_to_LR.EpsilonFreeZeroVisibleTail.cut_eq {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 : EpsilonFreeZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) :
      { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } = { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

      An epsilon-free zero tail only changes the grammar view of its physical cut.

      source
      theorem DPDA_to_LR.EpsilonBearingZeroVisibleTail.transGen_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 : EpsilonBearingZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) :
      Relation.TransGen PDA.Reaches₁ { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

      The epsilon step in an epsilon-bearing tail makes its exact cut path nonempty.

      source
      theorem DPDA_to_LR.ZeroVisibleTail.epsilonFree_or_epsilonBearing {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) :
      EpsilonFreeZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext ∨ EpsilonBearingZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext

      Structural classification of a zero-visible tail by the presence of an epsilon constructor.

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

      Operational form of the zero-tail dichotomy: either its endpoints are literally the same physical cut, or a nonempty PDA path connects them.

      source
      theorem DPDA_to_LR.ZeroVisibleTail.single_eq_splitLeft {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 suffix : List T} {anchorContext context : List (StackSymbol M)} {q middle : State M} {Z : StackSymbol M} (hanchor : VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext) (h : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.single q Z middle) suffix context) :
      ∃ (gamma : List (StackSymbol M)) (target : State M) (parentSuffix : List T) (outerContext : List (StackSymbol M)) (z : List T), ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q (Z :: gamma) target) parentSuffix outerContext ∧ ↑(Z :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M) ∧ (PDA_to_CFG.N.list q (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)]) ∈ (characteristicGrammar M).rules ∧ (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)] (List.map symbol.terminal z) ∧ suffix = z ++ parentSuffix ∧ context = gamma ++ outerContext

      A zero-visible tail from a visible anchor can reach a single node only by a final split-left constructor.

      source
      theorem DPDA_to_LR.ZeroVisibleTail.emptyList_eq_or_splitEpsilon {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 suffix : List T} {anchorContext context : List (StackSymbol M)} {q : State M} (hanchor : VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext) (h : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q [] q) suffix context) :
      anchor = PDA_to_CFG.N.list q [] q ∧ anchorSuffix = suffix ∧ anchorContext = context ∨ ∃ (source : State M) (Z : StackSymbol M) (gamma : List (StackSymbol M)) (target : State M) (parentSuffix : List T) (outerContext : List (StackSymbol M)) (z : List T), ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list source (Z :: gamma) target) parentSuffix outerContext ∧ ↑(Z :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M) ∧ (PDA_to_CFG.N.list source (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single source Z q), symbol.nonterminal (PDA_to_CFG.N.list q gamma target)]) ∈ (characteristicGrammar M).rules ∧ (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list q gamma target)] (List.map symbol.terminal z) ∧ (q, []) ∈ (emptyStackPDA M).transition_fun' source Z ∧ (PDA_to_CFG.N.single source Z q, [symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules ∧ suffix = z ++ parentSuffix ∧ context = gamma ++ outerContext

      A zero-visible tail from a visible anchor to an empty-list node is either already at that anchor, or ends in the exact split-left/epsilon pair which performs the empty return.

      Pure alignment of the last visible event #

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

      Two visible anchors with the same visible prefix have the same kind of last visible event. Read/read pairs share their predecessor prefix and last terminal. Split-right/split-right pairs share their predecessor prefix and the complete displayed single marker; their hidden replacement tails, targets, contexts, and left completions remain explicit and may differ.

      Instances For
        source
        theorem DPDA_to_LR.pairedVisibleAnchors_of_same_prefix {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p₁ p₂ : List (symbol T (Nonterminal M))} {w₁ w₂ : List T} {A₁ A₂ : Nonterminal M} {suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} (h₁ : VisibleSpineAnchor M p₁ A₁ suffix₁ w₁ context₁) (h₂ : VisibleSpineAnchor M p₂ A₂ suffix₂ w₂ context₂) (hp : p₁ = p₂) (hw : w₁ = w₂) :
        PairedVisibleAnchors M p₁ w₁ A₁ suffix₁ context₁ A₂ suffix₂ context₂

        Equal visible prefixes align the final visible events of two anchors.