Computation zipper for characteristic rightmost derivations

An occurrence in a right-sentential form has two pieces of operational meaning. A terminal completion of the symbols to its left drives the empty-stack PDA from its initial configuration to the configuration encoded by the occurrence. A terminal completion of the symbols to its right drives the saved stack context from the occurrence's target state to empty stack. This is the formal partial-tree invariant used in Knuth's DPDA-to-LR proof.

inductive DPDA_to_LR.Focused {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Nonterminal M → List T → List T → Prop

Operational meaning of a focused characteristic nonterminal.

• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} : Focused M PDA_to_CFG.N.start [] []
• single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (q target : State M) (Z : StackSymbol M) (preWord postWord : List T) (context : List (StackSymbol M)) (final : State M) (prefixPath : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := Z :: context }) (continuation : PDA.Reaches { state := target, input := postWord, stack := context } { state := final, input := [], stack := [] }) : Focused M (PDA_to_CFG.N.single q Z target) preWord postWord
• list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (q target : State M) (gamma : List (StackSymbol M)) (preWord postWord : List T) (context : List (StackSymbol M)) (final : State M) (prefixPath : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := gamma ++ context }) (continuation : PDA.Reaches { state := target, input := postWord, stack := context } { state := final, input := [], stack := [] }) : Focused M (PDA_to_CFG.N.list q gamma target) preWord postWord

theorem DPDA_to_LR.focused_of_derivation {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {form p right : List (symbol T (Nonterminal M))} {A : Nonterminal M} {preWord postWord : List T} (hroot : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] form) (hshape : form = p ++ [symbol.nonterminal A] ++ right) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) (hright : (characteristicGrammar M).DerivesRightmost right (List.map symbol.terminal postWord)) : Focused M A preWord postWord

The computation-zipper invariant for an arbitrary focused occurrence. The strings on both sides may be scheduled to terminals independently; their terminal yields are exactly the input consumed before the focus and the input handled by its saved continuation.

theorem DPDA_to_LR.focused_of_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} {suffix preWord : List T} (hroot : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal A] ++ List.map symbol.terminal suffix)) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : Focused M A preWord suffix

Prehandle-specialized form of the computation zipper.