LanglibProductive nonempty list positions #
A leftmost zero-visible trace remembers the boundary between the stack text displayed by a characteristic list nonterminal and its hidden zipper context. This module records the corresponding uniqueness fact for a nonempty list head. It is deliberately boundary-sensitive: equality of the underlying PDA stack would not suffice for the recursive split-right synchronization proof.
theorem
DPDA_to_LR.leftmostEpsilonTrace_nonempty_list_position_unique
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{start : LeftmostEpsilonPosition M}
{q final₁ final₂ : State M}
{Z : StackSymbol M}
{gamma₁ gamma₂ context₁ context₂ : List (StackSymbol M)}
{suffix₁ suffix₂ whole₁ whole₂ : List T}
(trace₁ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.list q (Z :: gamma₁) context₁))
(trace₂ : LeftmostEpsilonTrace M start (LeftmostEpsilonPosition.list q (Z :: gamma₂) context₂))
(global₁ :
PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₁, stack := [(emptyStackPDA M).start_symbol] }
(LeftmostEpsilonPosition.conf M suffix₁ start))
(global₂ :
PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₂, stack := [(emptyStackPDA M).start_symbol] }
(LeftmostEpsilonPosition.conf M suffix₂ start))
(useful₁ :
PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₁ (LeftmostEpsilonPosition.list q (Z :: gamma₁) context₁))
{ state := final₁, input := [], stack := [] })
(useful₂ :
PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₂ (LeftmostEpsilonPosition.list q (Z :: gamma₂) context₂))
{ state := final₂, input := [], stack := [] })
(hlook : List.take 1 suffix₁ = List.take 1 suffix₂)
:
LeftmostEpsilonPosition.list q (Z :: gamma₁) context₁ = LeftmostEpsilonPosition.list q (Z :: gamma₂) context₂
Two productive zero-visible traces from a common structural position to nonempty list positions with the same control state and exposed top symbol have equal exact positions, including the displayed/context boundary.
theorem
DPDA_to_LR.splitRight_positions_eq_of_parent_anchor_position_eq
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{base : List (symbol T (Nonterminal M))}
{beforeWord leftWord : List T}
{parentAnchor₁ parentAnchor₂ : Nonterminal M}
{parentAnchorSuffix₁ parentAnchorSuffix₂ : List T}
{parentAnchorContext₁ parentAnchorContext₂ : List (StackSymbol M)}
{parentSuffix₁ parentSuffix₂ future₁ future₂ : List T}
{parentContext₁ parentContext₂ : List (StackSymbol M)}
{source middle target₁ target₂ final₁ final₂ : State M}
{top : StackSymbol M}
{gamma₁ gamma₂ : List (StackSymbol M)}
(anchor₁ : VisibleSpineAnchor M base parentAnchor₁ parentAnchorSuffix₁ beforeWord parentAnchorContext₁)
(anchor₂ : VisibleSpineAnchor M base parentAnchor₂ parentAnchorSuffix₂ beforeWord parentAnchorContext₂)
(tail₁ :
ZeroVisibleTail M base beforeWord parentAnchor₁ parentAnchorSuffix₁ parentAnchorContext₁
(PDA_to_CFG.N.list source (top :: gamma₁) target₁) parentSuffix₁ parentContext₁)
(tail₂ :
ZeroVisibleTail M base beforeWord parentAnchor₂ parentAnchorSuffix₂ parentAnchorContext₂
(PDA_to_CFG.N.list source (top :: gamma₂) target₂) parentSuffix₂ parentContext₂)
(parentPosition :
leftmostEpsilonPositionOf M parentAnchor₁ parentAnchorContext₁ = leftmostEpsilonPositionOf M parentAnchor₂ parentAnchorContext₂)
(completion :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top middle)]
(List.map symbol.terminal leftWord))
(useful₁ :
PDA.Reaches { state := middle, input := future₁, stack := gamma₁ ++ parentContext₁ }
{ state := final₁, input := [], stack := [] })
(useful₂ :
PDA.Reaches { state := middle, input := future₂, stack := gamma₂ ++ parentContext₂ }
{ state := final₂, input := [], stack := [] })
(hlook : List.take 1 future₁ = List.take 1 future₂)
:
LeftmostEpsilonPosition.list middle gamma₁ parentContext₁ = LeftmostEpsilonPosition.list middle gamma₂ parentContext₂
Split-right children with a common selected word inherit exact-position synchronization from the last-visible anchors of their two parent spines.
The common single source top middle consumes the same word on both sides.
Consequently each productive child future extends to a productive parent
future on leftWord ++ future. Boundary-sensitive synchronization of the
two parent zero-visible tails then identifies both displayed parent stacks
and both hidden contexts, which immediately identifies the split-right
children.
theorem
DPDA_to_LR.nullableSplitRight_positions_eq_of_parent_anchor_position_eq
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{base : List (symbol T (Nonterminal M))}
{beforeWord : List T}
{parentAnchor₁ parentAnchor₂ : Nonterminal M}
{parentAnchorSuffix₁ parentAnchorSuffix₂ : List T}
{parentAnchorContext₁ parentAnchorContext₂ : List (StackSymbol M)}
{parentSuffix₁ parentSuffix₂ future₁ future₂ : List T}
{parentContext₁ parentContext₂ : List (StackSymbol M)}
{source middle target₁ target₂ final₁ final₂ : State M}
{top : StackSymbol M}
{gamma₁ gamma₂ : List (StackSymbol M)}
(anchor₁ : VisibleSpineAnchor M base parentAnchor₁ parentAnchorSuffix₁ beforeWord parentAnchorContext₁)
(anchor₂ : VisibleSpineAnchor M base parentAnchor₂ parentAnchorSuffix₂ beforeWord parentAnchorContext₂)
(tail₁ :
ZeroVisibleTail M base beforeWord parentAnchor₁ parentAnchorSuffix₁ parentAnchorContext₁
(PDA_to_CFG.N.list source (top :: gamma₁) target₁) parentSuffix₁ parentContext₁)
(tail₂ :
ZeroVisibleTail M base beforeWord parentAnchor₂ parentAnchorSuffix₂ parentAnchorContext₂
(PDA_to_CFG.N.list source (top :: gamma₂) target₂) parentSuffix₂ parentContext₂)
(parentPosition :
leftmostEpsilonPositionOf M parentAnchor₁ parentAnchorContext₁ = leftmostEpsilonPositionOf M parentAnchor₂ parentAnchorContext₂)
(emptyCompletion :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top middle)]
(List.map symbol.terminal []))
(useful₁ :
PDA.Reaches { state := middle, input := future₁, stack := gamma₁ ++ parentContext₁ }
{ state := final₁, input := [], stack := [] })
(useful₂ :
PDA.Reaches { state := middle, input := future₂, stack := gamma₂ ++ parentContext₂ }
{ state := final₂, input := [], stack := [] })
(hlook : List.take 1 future₁ = List.take 1 future₂)
:
LeftmostEpsilonPosition.list middle gamma₁ parentContext₁ = LeftmostEpsilonPosition.list middle gamma₂ parentContext₂
Nullable specialization of
splitRight_positions_eq_of_parent_anchor_position_eq.
inductive
DPDA_to_LR.ProductiveNonnullablePairedSplitResidual
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
:
The irreducible branch left after recursively peeling nullable paired
split-right markers. At least one selected single source top middle
completion consumes a nonempty terminal word. Both concrete parent spines,
their exact split rules, and the productive child futures are retained for
the terminal-extension argument.
- mk {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {base : List (symbol T (Nonterminal M))} {completedWord beforeWord₁ leftWord₁ beforeWord₂ leftWord₂ suffix₁ suffix₂ future₁ future₂ : List T} {context₁ context₂ : List (StackSymbol M)} {source middle target₁ target₂ final₁ final₂ : State M} {top : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₁) target₁) suffix₁ beforeWord₁ context₁) (length₁ : ↑(top :: gamma₁).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₁ : (PDA_to_CFG.N.list source (top :: gamma₁) target₁, [symbol.nonterminal (PDA_to_CFG.N.single source top middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma₁ target₁)]) ∈ (characteristicGrammar M).rules) (left₁ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top middle)] (List.map symbol.terminal leftWord₁)) (parent₂ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₂) target₂) suffix₂ beforeWord₂ context₂) (length₂ : ↑(top :: gamma₂).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₂ : (PDA_to_CFG.N.list source (top :: gamma₂) target₂, [symbol.nonterminal (PDA_to_CFG.N.single source top middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma₂ target₂)]) ∈ (characteristicGrammar M).rules) (left₂ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top middle)] (List.map symbol.terminal leftWord₂)) (word₁ : completedWord = beforeWord₁ ++ leftWord₁) (word₂ : completedWord = beforeWord₂ ++ leftWord₂) (nonnullable : leftWord₁ ≠ [] ∨ leftWord₂ ≠ []) (useful₁ : PDA.Reaches { state := middle, input := future₁, stack := gamma₁ ++ context₁ } { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches { state := middle, input := future₂, stack := gamma₂ ++ context₂ } { state := final₂, input := [], stack := [] }) (lookahead : List.take 1 future₁ = List.take 1 future₂) : ProductiveNonnullablePairedSplitResidual M
Instances For
@[irreducible]
theorem
DPDA_to_LR.productivePairedVisibleAnchor_positions_eq_or_nonnullable
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{preWord : List T}
{A₁ A₂ : Nonterminal M}
{suffix₁ suffix₂ : List T}
{context₁ context₂ : List (StackSymbol M)}
{future₁ future₂ : List T}
{final₁ final₂ : State M}
(paired : PairedVisibleAnchors M p preWord A₁ suffix₁ context₁ A₂ suffix₂ context₂)
(useful₁ :
PDA.Reaches { state := spineCutState M A₁, input := future₁, stack := spineCutStack M A₁ context₁ }
{ state := final₁, input := [], stack := [] })
(useful₂ :
PDA.Reaches { state := spineCutState M A₂, input := future₂, stack := spineCutStack M A₂ context₂ }
{ state := final₂, input := [], stack := [] })
(hlook : List.take 1 future₁ = List.take 1 future₂)
:
leftmostEpsilonPositionOf M A₁ context₁ = leftmostEpsilonPositionOf M A₂ context₂ ∨ ProductiveNonnullablePairedSplitResidual M
Productive paired visible anchors synchronize exactly after recursively
peeling split-right markers whose selected single completes on ε.
The only branch not discharged by this shorter-frontier recursion is the
explicit nonnullable split residual above.