Aho machine transitions

Zipper configurations, finite composite certificates, and the mathematical transition relation.

Zipper configurations and finite composite certificates

structure IndexedGrammar.Aho.WorkCursor {T : Type} (g : IndexedGrammar T) : Type

A work word with its hatted (active) symbol exposed.

• left : List (WorkSym g)
• focus : WorkSym g
• right : List (WorkSym g)

structure IndexedGrammar.Aho.WorkSlot {T : Type} (g : IndexedGrammar T) : Type

One logical work square, including the unique active-head marker.

• active : Bool
• symbol : WorkSym g

noncomputable instance IndexedGrammar.Aho.WorkSlot.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (WorkSlot g)

Equations

• IndexedGrammar.Aho.WorkSlot.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.WorkSlot g)

noncomputable instance IndexedGrammar.Aho.WorkSlot.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] : Fintype (WorkSlot g)

Equations

• IndexedGrammar.Aho.WorkSlot.instFintype = Fintype.ofInjective (fun (s : IndexedGrammar.Aho.WorkSlot g) => (s.active, s.symbol)) ⋯

def IndexedGrammar.Aho.WorkCursor.word {T : Type} {g : IndexedGrammar T} (c : WorkCursor g) : List (WorkSym g)

Forget the work head.

Equations

• c.word = c.left ++ c.focus :: c.right

def IndexedGrammar.Aho.WorkCursor.slots {T : Type} {g : IndexedGrammar T} (c : WorkCursor g) : List (WorkSlot g)

Encode the work cursor without losing its active position.

Equations

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

@[simp]

theorem IndexedGrammar.Aho.WorkCursor.slots_length {T : Type} {g : IndexedGrammar T} (c : WorkCursor g) : c.slots.length = c.word.length

@[simp]

theorem IndexedGrammar.Aho.WorkCursor.slots_symbols {T : Type} {g : IndexedGrammar T} (c : WorkCursor g) : List.map WorkSlot.symbol c.slots = c.word

theorem IndexedGrammar.Aho.WorkCursor.slots_injective {T : Type} {g : IndexedGrammar T} : Function.Injective slots

The marked slot word retains the whole cursor, not merely its underlying work word.

@[simp]

theorem IndexedGrammar.Aho.WorkCursor.word_length {T : Type} {g : IndexedGrammar T} (c : WorkCursor g) : c.word.length = c.left.length + 1 + c.right.length

structure IndexedGrammar.Aho.Config {T : Type} (g : IndexedGrammar T) : Type

A composite configuration: inputPos input symbols have already been compared, and work is the marked work-tape zipper.

• inputPos : ℕ
• work : WorkCursor g

def IndexedGrammar.Aho.initialConfig {T : Type} (g : IndexedGrammar T) : Config g

The initial composite configuration on every input.

Equations

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

def IndexedGrammar.Aho.finalConfig {T : Type} (g : IndexedGrammar T) (n : ℕ) : Config g

The final composite configuration after all n input symbols have been compared.

Equations

• IndexedGrammar.Aho.finalConfig g n = { inputPos := n, work := { left := [IndexedGrammar.Aho.WorkSym.dollar], focus := IndexedGrammar.Aho.WorkSym.hash, right := [] } }

inductive IndexedGrammar.Aho.CompositeCert {T : Type} (g : IndexedGrammar T) : Type

Finite evidence selecting one of Aho's composite moves. All fields range over types fixed by the grammar, so this is a finite certificate alphabet.

• plainBinary {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.nt → CompositeCert g
• plainTerminal {T : Type} {g : IndexedGrammar T} : g.nt → T → CompositeCert g
• plainPushSkip {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.flag → CompositeCert g
• plainPushUse {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.flag → CompositeCert g
• liveBinaryBoth {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.nt → CompositeCert g
• liveBinaryLeft {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.nt → CompositeCert g
• liveBinaryRight {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.nt → CompositeCert g
• livePushFresh {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.flag → CompositeCert g
• livePushCompress {T : Type} {g : IndexedGrammar T} : g.nt → g.nt → g.flag → CFlag g → IndexMark → CompositeCert g
• popPlain {T : Type} {g : IndexedGrammar T} : CFlag g → IndexMark → g.nt → g.nt → CompositeCert g
• popLive {T : Type} {g : IndexedGrammar T} : CFlag g → IndexMark → g.nt → g.nt → CompositeCert g
• matchTerminal {T : Type} {g : IndexedGrammar T} : T → CompositeCert g
• eraseIndex {T : Type} {g : IndexedGrammar T} : CFlag g → IndexMark → CompositeCert g
• returnFrame {T : Type} {g : IndexedGrammar T} : CompositeCert g

noncomputable instance IndexedGrammar.Aho.CompositeCert.instDecidableEq {T : Type} {g : IndexedGrammar T} : DecidableEq (CompositeCert g)

Equations

• IndexedGrammar.Aho.CompositeCert.instDecidableEq = Classical.decEq (IndexedGrammar.Aho.CompositeCert g)

noncomputable instance IndexedGrammar.Aho.CompositeCert.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] [Fintype g.flag] : Fintype (CompositeCert g)

Equations

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

noncomputable def IndexedGrammar.Aho.CertStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : CompositeCert g → Config g → Config g → Prop

Semantics of one finite composite certificate on a fixed input word.

The clauses are Aho's moves 1--6, split into their nondeterministic subcases. The paper's active hat is represented by WorkCursor.focus; consequently every equality below also fixes the new work-head position.

Equations

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

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

One composite move is a move selected by some finite certificate.

Equations

• IndexedGrammar.Aho.CompositeStep g input c c' = ∃ (cert : IndexedGrammar.Aho.CompositeCert g), IndexedGrammar.Aho.CertStep g input cert c c'

theorem IndexedGrammar.Aho.compositeStep_iff_exists_cert {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (c c' : Config g) : CompositeStep g input c c' ↔ ∃ (cert : CompositeCert g), CertStep g input cert c c'