LanglibOperational runs for characteristic list introductions #
These factorizations expose the hidden stack context of read, epsilon, and split-right introduction edges after a chosen terminal completion of their visible prefix. They form the cycle-free prerequisite shared by spine synchronization and the final epsilon-head assembly.
def
DPDA_to_LR.ListIntroductionRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(preWord suffix : List T)
(source : State M)
(top : StackSymbol M)
(next : State M)
(gamma : List (StackSymbol M))
(target : State M)
:
Operational factorization of a non-start list introduction after a chosen terminal completion of its visible child prefix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
DPDA_to_LR.ListTransitionRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(preWord suffix : List T)
(source : State M)
(top : StackSymbol M)
(next : State M)
(gamma : List (StackSymbol M))
(target : State M)
:
Stronger factorization for an introduction generated by one actual PDA transition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
DPDA_to_LR.ListTransitionRun.introductionRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{preWord suffix : List T}
{source : State M}
{top : StackSymbol M}
{next : State M}
{gamma : List (StackSymbol M)}
{target : State M}
(h : ListTransitionRun M preWord suffix source top next gamma target)
:
ListIntroductionRun M preWord suffix source top next gamma target
Forgetting that the middle segment is one step gives the uniform introduction-run factorization.
def
DPDA_to_LR.ListSplitRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
(preWord suffix : List T)
(source : State M)
(top : StackSymbol M)
(next : State M)
(gamma : List (StackSymbol M))
(target : State M)
:
Split-right introductions preserve the stronger fact that the source tail is exactly the child stack followed by the saved outer context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
DPDA_to_LR.ListSplitRun.introductionRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{preWord suffix : List T}
{source : State M}
{top : StackSymbol M}
{next : State M}
{gamma : List (StackSymbol M)}
{target : State M}
(h : ListSplitRun M preWord suffix source top next gamma target)
:
ListIntroductionRun M preWord suffix source top next gamma target
Forgetting the split-specific source-tail equation gives a uniform run.
theorem
DPDA_to_LR.listIntroductionRun_read
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q target next : State M}
{a : T}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) suffix)
(htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun q a Z)
(hp : (characteristicGrammar M).DerivesRightmost (p ++ [symbol.terminal a]) (List.map symbol.terminal preWord))
:
ListIntroductionRun M preWord suffix q Z next gamma target
Exact factorization for a reading list introduction.
theorem
DPDA_to_LR.listTransitionRun_read
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q target next : State M}
{a : T}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) suffix)
(htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun q a Z)
(hp : (characteristicGrammar M).DerivesRightmost (p ++ [symbol.terminal a]) (List.map symbol.terminal preWord))
:
ListTransitionRun M preWord suffix q Z next gamma target
One-step specialization of listIntroductionRun_read.
theorem
DPDA_to_LR.listIntroductionRun_epsilon
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q target next : State M}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) suffix)
(htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z)
(hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord))
:
ListIntroductionRun M preWord suffix q Z next gamma target
Exact factorization for an epsilon list introduction.
theorem
DPDA_to_LR.listTransitionRun_epsilon
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q target next : State M}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) suffix)
(htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z)
(hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord))
:
ListTransitionRun M preWord suffix q Z next gamma target
One-step specialization of listIntroductionRun_epsilon.
theorem
DPDA_to_LR.listIntroductionRun_split
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q middle target : State M}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.list q (Z :: gamma) target) suffix)
(hp :
(characteristicGrammar M).DerivesRightmost (p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)])
(List.map symbol.terminal preWord))
:
ListIntroductionRun M preWord suffix q Z middle gamma target
Exact factorization for a split-right list introduction.
theorem
DPDA_to_LR.listSplitRun
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{suffix preWord : List T}
{q middle target : State M}
{Z : StackSymbol M}
{gamma : List (StackSymbol M)}
(hparent : ActiveSpine M p (PDA_to_CFG.N.list q (Z :: gamma) target) suffix)
(hp :
(characteristicGrammar M).DerivesRightmost (p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)])
(List.map symbol.terminal preWord))
:
ListSplitRun M preWord suffix q Z middle gamma target
Split-specific factorization retaining the exact hidden-context shape.