Accepting-run soundness for Aho's machine

The forward derivation invariant and the final theorem from accepting machine runs to grammar generation.

Forward derivation invariant and accepting-run soundness

def IndexedGrammar.Aho.ControlDenotation.ForwardInvariant {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (c : Config g) : Prop

The consumed input prefix followed by the execution-ordered remaining form is derivable from the grammar start symbol.

Equations

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

theorem IndexedGrammar.Aho.ControlDenotation.initial_forwardInvariant {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : ForwardInvariant g input (initialConfig g)

theorem IndexedGrammar.Aho.ControlDenotation.compositeStep_preserves_represents {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {c c' : Config g} {form : List g.ISym} (hstep : CompositeStep g input c c') (hrep : Config.Represents c form) : ∃ (form' : List g.ISym), Config.Represents c' form' ∧ StepEffect g input c c' form form'

theorem IndexedGrammar.Aho.ControlDenotation.compositeStep_preserves_forwardInvariant {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {c c' : Config g} (hstep : CompositeStep g input c c') (hinv : ForwardInvariant g input c) : ForwardInvariant g input c'

theorem IndexedGrammar.Aho.ControlDenotation.reachable_forwardInvariant {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) {c : Config g} (hreach : Relation.ReflTransGen (CompositeStep g input) (initialConfig g) c) : ForwardInvariant g input c

theorem IndexedGrammar.Aho.ControlDenotation.finalConfig_represents_only_nil {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (n : ℕ) {form : List g.ISym} (hrep : Config.Represents (finalConfig g n) form) : form = []

theorem IndexedGrammar.Aho.ControlDenotation.ahoMachine_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (hreach : Relation.ReflTransGen (CompositeStep g input) (initialConfig g) (finalConfig g input.length)) : g.Generates input

Every accepting run of the composite machine spells a genuine indexed-grammar derivation.