Rightmost frontiers of the DPDA characteristic grammar

Rightmost derivations in the characteristic grammar have a particularly rigid frontier. Every nonterminal strictly before the active (rightmost) nonterminal is a single nonterminal. The active nonterminal is either single or list; the untouched start symbol is handled separately. These facts let the DPDA-to-LR proof recover the productive first move represented by an arbitrary reachable prehandle.

def DPDA_to_LR.PendingPrefix {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) : Prop

Every nonterminal in a pending prefix is a characteristic single nonterminal. Terminals may occur anywhere in the prefix.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.PendingPrefix.nil {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PendingPrefix M []

theorem DPDA_to_LR.PendingPrefix.of_append_left {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p q : List (symbol T (Nonterminal M))} (h : PendingPrefix M (p ++ q)) : PendingPrefix M p

theorem DPDA_to_LR.PendingPrefix.append_terminals {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (h : PendingPrefix M p) (s : List T) : PendingPrefix M (p ++ List.map symbol.terminal s)

theorem DPDA_to_LR.PendingPrefix.append_single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (h : PendingPrefix M p) (q t : State M) (Z : StackSymbol M) : PendingPrefix M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z t)])

theorem DPDA_to_LR.PendingPrefix.lastView {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (h : PendingPrefix M p) : (∃ (w : List T), p = List.map symbol.terminal w) ∨ ∃ (p₀ : List (symbol T (Nonterminal M))) (q : State M) (t : State M) (Z : StackSymbol M) (s : List T), PendingPrefix M p₀ ∧ p = p₀ ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z t)] ++ List.map symbol.terminal s

Looking from the right, a pending prefix is either entirely terminal or ends in a single nonterminal followed only by terminals.

A convenient nonterminal projection

def DPDA_to_LR.CharacteristicFrontier {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (v : List (symbol T (Nonterminal M))) : Prop

The complete shape invariant for a rightmost-reachable characteristic sentential form.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.CharacteristicFrontier.pendingPrefix_of_prehandle {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {v p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s : List T} (hv : CharacteristicFrontier M v) (hshape : v = p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s) : PendingPrefix M p

Every prefix before a displayed rightmost nonterminal in a frontier is pending.

theorem DPDA_to_LR.derivesRightmost_characteristic_frontier {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {v : List (symbol T (Nonterminal M))} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] v) : CharacteristicFrontier M v

Every rightmost-reachable sentential form of the reduced characteristic grammar has the frontier shape above.

theorem DPDA_to_LR.characteristic_prehandle_classification {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s : List T} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) : PendingPrefix M p ∧ (A = PDA_to_CFG.N.start ∧ p = [] ∧ s = [] ∨ (∃ (q : State M) (t : State M) (Z : StackSymbol M), A = PDA_to_CFG.N.single q Z t) ∨ ∃ (q : State M) (t : State M) (alpha : List (StackSymbol M)), A = PDA_to_CFG.N.list q alpha t)

Classification of an arbitrary reachable characteristic prehandle. The untouched start case is explicit; otherwise the active nonterminal is either a single or a list, and in every case its prefix is pending.

theorem DPDA_to_LR.pendingPrefix_of_characteristic_prehandle {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {s : List T} (h : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal s)) : PendingPrefix M p

Prefix-only form of characteristic_prehandle_classification.