LanglibSyntactic characteristic-rule collision cases #
These are the LR-core cases decided solely by the rigid characteristic rule shapes. They deliberately do not use the operational cut invariant needed for collisions between transition rules (or between two empty-list rules).
theorem
DPDA_to_LR.base_nonbase_post_impossible
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{plain pre : List (symbol T (Nonterminal M))}
{suffixPlain suffixList : List T}
{q target : State M}
{gamma : List (StackSymbol M)}
(hplain : ∀ X ∈ plain, ¬IsListSymbol M X)
(heq :
plain ++ List.map symbol.terminal suffixPlain = pre ++ [symbol.nonterminal (PDA_to_CFG.N.list q gamma target)] ++ List.map symbol.terminal suffixList)
:
A post-handle form with no list symbol cannot equal one whose rule
right side ends in a list symbol. This disposes of every base/nonbase pair.
theorem
DPDA_to_LR.split_split_collision
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p₁ p₂ : List (symbol T (Nonterminal M))}
{s₂ y : List T}
{q₁ q₂ middle₁ middle₂ target₁ target₂ : State M}
{Z₁ Z₂ : StackSymbol M}
{alpha₁ alpha₂ : List (StackSymbol M)}
(hp₁ : PendingPrefix M p₁)
(hp₂ : PendingPrefix M p₂)
(heq :
p₂ ++ [symbol.nonterminal (PDA_to_CFG.N.single q₂ Z₂ middle₂), symbol.nonterminal (PDA_to_CFG.N.list middle₂ alpha₂ target₂)] ++ List.map symbol.terminal s₂ = p₁ ++ [symbol.nonterminal (PDA_to_CFG.N.single q₁ Z₁ middle₁), symbol.nonterminal (PDA_to_CFG.N.list middle₁ alpha₁ target₁)] ++ List.map symbol.terminal y)
:
p₁ = p₂ ∧ (PDA_to_CFG.N.list q₁ (Z₁ :: alpha₁) target₁, [symbol.nonterminal (PDA_to_CFG.N.single q₁ Z₁ middle₁), symbol.nonterminal (PDA_to_CFG.N.list middle₁ alpha₁ target₁)]) = (PDA_to_CFG.N.list q₂ (Z₂ :: alpha₂) target₂, [symbol.nonterminal (PDA_to_CFG.N.single q₂ Z₂ middle₂), symbol.nonterminal (PDA_to_CFG.N.list middle₂ alpha₂ target₂)])
Two split rules with equal post-handle forms have the same handle position and are literally the same production.
theorem
DPDA_to_LR.read_split_post_impossible
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{pRead pSplit : List (symbol T (Nonterminal M))}
{sRead sSplit : List T}
{a : T}
{q middle next targetRead targetSplit : State M}
{Z : StackSymbol M}
{alpha beta : List (StackSymbol M)}
(hpRead : PendingPrefix M pRead)
(hpSplit : PendingPrefix M pSplit)
(heq :
pSplit ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle beta targetSplit)] ++ List.map symbol.terminal sSplit = pRead ++ [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next alpha targetRead)] ++ List.map symbol.terminal sRead)
:
A read-rule prefix and a split-rule prefix cannot be equal: after cancelling the final list marker, one ends in a terminal and the other in a nonterminal.
theorem
DPDA_to_LR.split_read_post_impossible
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{pRead pSplit : List (symbol T (Nonterminal M))}
{sRead sSplit : List T}
{a : T}
{q middle next targetRead targetSplit : State M}
{Z : StackSymbol M}
{alpha beta : List (StackSymbol M)}
(hpRead : PendingPrefix M pRead)
(hpSplit : PendingPrefix M pSplit)
(heq :
pRead ++ [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next alpha targetRead)] ++ List.map symbol.terminal sRead = pSplit ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle beta targetSplit)] ++ List.map symbol.terminal sSplit)
:
Symmetric orientation of read_split_post_impossible.
theorem
DPDA_to_LR.start_prehandle_eq_nil
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p : List (symbol T (Nonterminal M))}
{s : List T}
(h :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial]
(p ++ [symbol.nonterminal PDA_to_CFG.N.start] ++ List.map symbol.terminal s))
:
The untouched characteristic start occurrence fixes its entire prehandle: there is no prefix and no terminal suffix.
theorem
DPDA_to_LR.retained_start_target_eq_drain
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)}
(hr : r ∈ (characteristicGrammar M).rules)
{target : State M}
(hrule :
r = (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)]))
:
Every retained start rule targets the distinguished global drain state. Productivity supplies a complete empty-stack run, and global accepting runs cannot finish in a boot or simulation state.
theorem
DPDA_to_LR.retained_start_rules_unique
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{r₁ r₂ : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)}
(hr₁ : r₁ ∈ (characteristicGrammar M).rules)
(hr₂ : r₂ ∈ (characteristicGrammar M).rules)
{target₁ target₂ : State M}
(hshape₁ :
r₁ = (PDA_to_CFG.N.start, [symbol.nonterminal
(PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₁)]))
(hshape₂ :
r₂ = (PDA_to_CFG.N.start, [symbol.nonterminal
(PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₂)]))
:
In particular, the productive reduction retains at most one start production.
theorem
DPDA_to_LR.start_start_collision
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{p₁ p₂ : List (symbol T (Nonterminal M))}
{s₁ s₂ y : List T}
{target₁ target₂ : State M}
(hd₁ :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial]
(p₁ ++ [symbol.nonterminal PDA_to_CFG.N.start] ++ List.map symbol.terminal s₁))
(hd₂ :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial]
(p₂ ++ [symbol.nonterminal PDA_to_CFG.N.start] ++ List.map symbol.terminal s₂))
(heq :
p₂ ++ [symbol.nonterminal
(PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₂)] ++ List.map symbol.terminal s₂ = p₁ ++ [symbol.nonterminal
(PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₁)] ++ List.map symbol.terminal y)
:
p₁ = p₂ ∧ (PDA_to_CFG.N.start, [symbol.nonterminal
(PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₁)]) = (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target₂)])
Two reachable start rules with equal post-handle forms coincide.
theorem
DPDA_to_LR.start_nonempty_action_post_impossible
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{pStart pOther : List (symbol T (Nonterminal M))}
{sStart sOther : List T}
{X : symbol T (Nonterminal M)}
{qStart qOther targetStart targetOther : State M}
{gammaStart gammaOther : List (StackSymbol M)}
(hdStart :
(characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial]
(pStart ++ [symbol.nonterminal PDA_to_CFG.N.start] ++ List.map symbol.terminal sStart))
(hpOther : PendingPrefix M pOther)
(hX : ¬IsListSymbol M X)
(heq :
pOther ++ [X] ++ [symbol.nonterminal (PDA_to_CFG.N.list qOther gammaOther targetOther)] ++ List.map symbol.terminal sOther = pStart ++ [symbol.nonterminal (PDA_to_CFG.N.list qStart gammaStart targetStart)] ++ List.map symbol.terminal sStart)
:
A start-rule postform cannot coincide with a read or split postform: the start occurrence has empty prefix, whereas those rule right sides put one non-list symbol before their final list marker.