LanglibHypothesis-driven closure of the remaining epsilon-head cases #
This module keeps the three hard branches of epsilonIntroducingHeadsUnique
separate from NoEpsilonCycle. They all follow from the same
boundary-sensitive paired-anchor synchronization hypothesis used by the
empty-return classifier.
theorem
DPDA_to_LR.epsilonBearing_sameListPosition_false_of_useful
{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 future : List T}
{anchorContext comparisonContext currentContext : List (StackSymbol M)}
{q target final : State M}
{gamma : List (StackSymbol M)}
(tail :
ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q gamma target) suffix
currentContext)
(bearing :
EpsilonBearingZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q gamma target) suffix
currentContext)
(hposition :
leftmostEpsilonPositionOf M anchor anchorContext = leftmostEpsilonPositionOf M (PDA_to_CFG.N.list q gamma target) comparisonContext)
(useful :
PDA.Reaches { state := q, input := future, stack := gamma ++ currentContext }
{ state := final, input := [], stack := [] })
:
An epsilon-bearing tail which starts at the same boundary-sensitive position as its displayed list endpoint is a forbidden useful return to that list cut.
theorem
DPDA_to_LR.EpsilonSplitTailData.false_of_productivePositions
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(hpositions : ProductivePairedVisibleAnchorPositionsEqual M)
{childPrefix : List (symbol T (Nonterminal M))}
{next target : State M}
{gamma : List (StackSymbol M)}
{epsilonSuffix splitSuffix : List T}
(data : EpsilonSplitTailData M childPrefix next target gamma epsilonSuffix splitSuffix)
:
The paired-anchor position theorem eliminates the epsilon/split branch
after activeEpsilonSplit_tailData has exposed its common child and useful
futures.
theorem
DPDA_to_LR.activeEpsilonSplit_false_of_productivePositions
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(hpositions : ProductivePairedVisibleAnchorPositionsEqual M)
{childPrefix base : List (symbol T (Nonterminal M))}
{epsilonSuffix splitSuffix : List T}
{epsilonSource next target splitSource : State M}
{epsilonTop splitTop : StackSymbol M}
{gamma : List (StackSymbol M)}
(epsilonParent : ActiveSpine M childPrefix (PDA_to_CFG.N.single epsilonSource epsilonTop target) epsilonSuffix)
(epsilonTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' epsilonSource epsilonTop)
(epsilonRule :
(PDA_to_CFG.N.single epsilonSource epsilonTop target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(splitParent : ActiveSpine M base (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target) splitSuffix)
(splitLength : ↑(splitTop :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M))
(splitRule :
(PDA_to_CFG.N.list splitSource (splitTop :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next), symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(hprefix : childPrefix = base ++ [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next)])
(hlook : List.take 1 epsilonSuffix = List.take 1 splitSuffix)
:
Active epsilon/split introductions of one list child are impossible once productive paired anchors have equal boundary-sensitive positions.
theorem
DPDA_to_LR.activeSplitEpsilon_false_of_productivePositions
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(hpositions : ProductivePairedVisibleAnchorPositionsEqual M)
{childPrefix base : List (symbol T (Nonterminal M))}
{splitSuffix epsilonSuffix : List T}
{splitSource next target epsilonSource : State M}
{splitTop epsilonTop : StackSymbol M}
{gamma : List (StackSymbol M)}
(splitParent : ActiveSpine M base (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target) splitSuffix)
(splitLength : ↑(splitTop :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M))
(splitRule :
(PDA_to_CFG.N.list splitSource (splitTop :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next), symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(epsilonParent : ActiveSpine M childPrefix (PDA_to_CFG.N.single epsilonSource epsilonTop target) epsilonSuffix)
(epsilonTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' epsilonSource epsilonTop)
(epsilonRule :
(PDA_to_CFG.N.single epsilonSource epsilonTop target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(hprefix : base ++ [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next)] = childPrefix)
(hlook : List.take 1 splitSuffix = List.take 1 epsilonSuffix)
:
Symmetric callable form for the split/epsilon branch.
theorem
DPDA_to_LR.activeEpsilonEpsilon_heads_eq_of_productivePositions
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(hpositions : ProductivePairedVisibleAnchorPositionsEqual M)
{childPrefix : List (symbol T (Nonterminal M))}
{suffix₁ suffix₂ : List T}
{q₁ q₂ next target : State M}
{top₁ top₂ : StackSymbol M}
{gamma : List (StackSymbol M)}
(parent₁ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₁ top₁ target) suffix₁)
(transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ top₁)
(rule₁ :
(PDA_to_CFG.N.single q₁ top₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(parent₂ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₂ top₂ target) suffix₂)
(transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ top₂)
(rule₂ :
(PDA_to_CFG.N.single q₂ top₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules)
(hlook : List.take 1 suffix₁ = List.take 1 suffix₂)
:
Two active epsilon introductions of the same list child have equal source state and exposed stack symbol under the paired-position hypothesis.
theorem
DPDA_to_LR.epsilonIntroducingHeadsUnique_of_productivePositions
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(hpositions : ProductivePairedVisibleAnchorPositionsEqual M)
:
Productive paired-anchor position synchronization discharges every epsilon-bearing case of active introducing-head uniqueness.