Whole-tape denotation for Aho's close-crossing control stack

Stack visibility and execution order are deliberately separated. PhysicalRep scans the whole physical tape right-to-left, ignoring control delimiters. Exec follows active symbols and the $/¢ return discipline to emit the remaining sentential form in execution order. This handles later pops whose index-free scan crosses one or more ¢ markers.

Mark-insensitive alignment

def IndexedGrammar.Aho.ControlDenotation.normalizeIndexMark (d : IndexMark) : IndexMark

Equations

• IndexedGrammar.Aho.ControlDenotation.normalizeIndexMark d = if d.later = true then IndexedGrammar.Aho.IndexMark.laterPending else IndexedGrammar.Aho.IndexMark.firstPending

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeIndexMark_later (d : IndexMark) : (normalizeIndexMark d).later = d.later

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeIndexMark_markUsed (d : IndexMark) : normalizeIndexMark d.markUsed = normalizeIndexMark d

def IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym {T : Type} {g : IndexedGrammar T} : WorkSym g → WorkSym g

Equations

• IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym (IndexedGrammar.Aho.WorkSym.index R d) = IndexedGrammar.Aho.WorkSym.index R (IndexedGrammar.Aho.ControlDenotation.normalizeIndexMark d)
• IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym x✝ = x✝

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym_index {T : Type} {g : IndexedGrammar T} (R : CFlag g) (d : IndexMark) : normalizeWorkSym (WorkSym.index R d) = WorkSym.index R (normalizeIndexMark d)

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym_markUsed {T : Type} {g : IndexedGrammar T} (R : CFlag g) (d : IndexMark) : normalizeWorkSym (WorkSym.index R d.markUsed) = normalizeWorkSym (WorkSym.index R d)

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym_markProductivePrefix {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) : List.map normalizeWorkSym (markProductivePrefix alpha) = List.map normalizeWorkSym alpha

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.indexFree_map_normalizeWorkSym {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : IndexFree (List.map normalizeWorkSym xs) ↔ IndexFree xs

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.dollarFree_map_normalizeWorkSym {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : DollarFree (List.map normalizeWorkSym xs) ↔ DollarFree xs

@[simp]

theorem IndexedGrammar.Aho.ControlDenotation.normalizeWorkSym_ne_dollar_iff {T : Type} {g : IndexedGrammar T} (z : WorkSym g) : normalizeWorkSym z ≠ WorkSym.dollar ↔ z ≠ WorkSym.dollar

def IndexedGrammar.Aho.ControlDenotation.normalizeCursor {T : Type} {g : IndexedGrammar T} (cursor : WorkCursor g) : WorkCursor g

Equations

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

inductive IndexedGrammar.Aho.ControlDenotation.AnnSym {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : Type

Ghost work symbols. An index remembers its denoted concrete block and only its first/later class; the operational pending/used bit has no semantic content.

• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : T → AnnSym g
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : g.nt → List g.flag → AnnSym g
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : g.nt → List g.flag → AnnSym g
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (R : CFlag g) (continues : Bool) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) : AnnSym g
• dollar {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : AnnSym g
• close {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : AnnSym g
• hash {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : AnnSym g

def IndexedGrammar.Aho.ControlDenotation.AnnSym.erase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : AnnSym g → WorkSym g

Equations

• (IndexedGrammar.Aho.ControlDenotation.AnnSym.terminal a).erase = IndexedGrammar.Aho.WorkSym.terminal a
• (IndexedGrammar.Aho.ControlDenotation.AnnSym.plain A a).erase = IndexedGrammar.Aho.WorkSym.plain A
• (IndexedGrammar.Aho.ControlDenotation.AnnSym.live A a).erase = IndexedGrammar.Aho.WorkSym.live A
• (IndexedGrammar.Aho.ControlDenotation.AnnSym.index R false flags denotes).erase = IndexedGrammar.Aho.WorkSym.index R IndexedGrammar.Aho.IndexMark.firstPending
• (IndexedGrammar.Aho.ControlDenotation.AnnSym.index R true flags denotes).erase = IndexedGrammar.Aho.WorkSym.index R IndexedGrammar.Aho.IndexMark.laterPending
• IndexedGrammar.Aho.ControlDenotation.AnnSym.dollar.erase = IndexedGrammar.Aho.WorkSym.dollar
• IndexedGrammar.Aho.ControlDenotation.AnnSym.close.erase = IndexedGrammar.Aho.WorkSym.close
• IndexedGrammar.Aho.ControlDenotation.AnnSym.hash.erase = IndexedGrammar.Aho.WorkSym.hash

structure IndexedGrammar.Aho.ControlDenotation.AnnCursor {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : Type

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

def IndexedGrammar.Aho.ControlDenotation.AnnCursor.word {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (cursor : AnnCursor g) : List (AnnSym g)

Equations

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

def IndexedGrammar.Aho.ControlDenotation.AnnCursor.erase {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (cursor : AnnCursor g) : WorkCursor g

Equations

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

Physical stack assignment

inductive IndexedGrammar.Aho.ControlDenotation.PhysicalRep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : BlockDenotation.VisibleStack g → List (AnnSym g) → BlockDenotation.VisibleStack g → Prop

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (inherited : BlockDenotation.VisibleStack g) : PhysicalRep g inherited [] inherited
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (a : T) (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.terminal a :: xs) stack
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (A : g.nt) (actual : List g.flag) (decorates : BlockDenotation.Decorates stack actual) (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.plain A actual :: xs) stack
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (A : g.nt) (actual : List g.flag) (decorates : BlockDenotation.LiveDecorates stack actual) (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.live A actual :: xs) stack
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (R : CFlag g) (continues : Bool) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.index R continues flags denotes :: xs) ({ flags := flags, continues := continues } :: stack)
• dollar {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.dollar :: xs) stack
• close {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.close :: xs) stack
• hash {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited stack : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (tail : PhysicalRep g inherited xs stack) : PhysicalRep g inherited (AnnSym.hash :: xs) stack

theorem IndexedGrammar.Aho.ControlDenotation.physicalRep_append_iff {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (xs ys : List (AnnSym g)) {inherited before : BlockDenotation.VisibleStack g} : PhysicalRep g inherited (xs ++ ys) before ↔ ∃ (middle : BlockDenotation.VisibleStack g), PhysicalRep g inherited ys middle ∧ PhysicalRep g middle xs before

def IndexedGrammar.Aho.ControlDenotation.AnnIndexFree {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (xs : List (AnnSym g)) : Prop

Equations

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

theorem IndexedGrammar.Aho.ControlDenotation.PhysicalRep.stack_eq_of_indexFree {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {inherited before : BlockDenotation.VisibleStack g} {xs : List (AnnSym g)} (hfree : AnnIndexFree xs) (h : PhysicalRep g inherited xs before) : before = inherited

Shrinking execution-order interpreter

inductive IndexedGrammar.Aho.ControlDenotation.Exec {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : AnnCursor g → List g.ISym → Prop

Traverse active symbols in machine order. Every recursive cursor is shorter: an ordinary or index step deletes its focus, and a return step deletes one $/¢ pair.

• done {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : Exec g { left := [AnnSym.dollar], focus := AnnSym.hash, right := [] } []
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (AnnSym g)} {next : AnnSym g} {right : List (AnnSym g)} {form : List g.ISym} (a : T) (tail : Exec g { left := left, focus := next, right := right } form) : Exec g { left := left, focus := AnnSym.terminal a, right := next :: right } (ISym.terminal a :: form)
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (AnnSym g)} {next : AnnSym g} {right : List (AnnSym g)} {form : List g.ISym} (A : g.nt) (actual : List g.flag) (tail : Exec g { left := left, focus := next, right := right } form) : Exec g { left := left, focus := AnnSym.plain A actual, right := next :: right } (ISym.indexed A actual :: form)
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (AnnSym g)} {next : AnnSym g} {right : List (AnnSym g)} {form : List g.ISym} (A : g.nt) (actual : List g.flag) (tail : Exec g { left := left, focus := next, right := right } form) : Exec g { left := left, focus := AnnSym.live A actual, right := next :: right } (ISym.indexed A actual :: form)
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (AnnSym g)} {next : AnnSym g} {right : List (AnnSym g)} {form : List g.ISym} (R : CFlag g) (continues : Bool) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) (tail : Exec g { left := left, focus := next, right := right } form) : Exec g { left := left, focus := AnnSym.index R continues flags denotes, right := next :: right } form
• returnFrame {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha beta gamma : List (AnnSym g)} {Z : AnnSym g} {form : List g.ISym} (hfree : AnnSym.dollar ∉ beta) (tail : Exec g { left := alpha ++ [AnnSym.dollar], focus := Z, right := beta ++ gamma } form) : Exec g { left := alpha ++ [AnnSym.dollar, Z] ++ beta ++ [AnnSym.dollar], focus := AnnSym.close, right := gamma } form

Active-right stack semantics

Only symbols to the right of the active focus index that occurrence. A close does not stop the scan: this is exactly how a later pop reaches a lower block across completed inner frames. When a frame returns, ExecRep.returnFrame reactivates its saved left material and the right stack is recomputed in that new cursor, preventing an inner consumed block from leaking across older $ scopes.

inductive IndexedGrammar.Aho.ControlDenotation.RightRep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : List (WorkSym g) → BlockDenotation.VisibleStack g → Prop

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : RightRep g [] []
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (a : T) (tail : RightRep g xs stack) : RightRep g (WorkSym.terminal a :: xs) stack
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (A : g.nt) (tail : RightRep g xs stack) : RightRep g (WorkSym.plain A :: xs) stack
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (A : g.nt) (tail : RightRep g xs stack) : RightRep g (WorkSym.live A :: xs) stack
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (R : CFlag g) (d : IndexMark) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) (tail : RightRep g xs stack) : RightRep g (WorkSym.index R d :: xs) ({ flags := flags, continues := d.later } :: stack)
• close {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (tail : RightRep g xs stack) : RightRep g (WorkSym.close :: xs) stack
• hash {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (tail : RightRep g xs stack) : RightRep g (WorkSym.hash :: xs) stack

inductive IndexedGrammar.Aho.ControlDenotation.RightPrefix {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : List (WorkSym g) → BlockDenotation.VisibleStack g → BlockDenotation.VisibleStack g → Prop

A right-stack prefix transformer, used to split at a selected compressed token without inventing annotations for ordinary symbols.

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (stack : BlockDenotation.VisibleStack g) : RightPrefix g [] stack stack
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (a : T) (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.terminal a :: xs) before after
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (A : g.nt) (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.plain A :: xs) before after
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (A : g.nt) (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.live A :: xs) before after
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (R : CFlag g) (d : IndexMark) (flags : List g.flag) (denotes : CFlag.Denotes g flags R) (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.index R d :: xs) ({ flags := flags, continues := d.later } :: before) after
• close {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.close :: xs) before after
• hash {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (tail : RightPrefix g xs before after) : RightPrefix g (WorkSym.hash :: xs) before after

theorem IndexedGrammar.Aho.ControlDenotation.rightRep_append {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs ys : List (WorkSym g)} {stack : BlockDenotation.VisibleStack g} (h : RightRep g (xs ++ ys) stack) : ∃ (middle : BlockDenotation.VisibleStack g), RightRep g ys middle ∧ RightPrefix g xs stack middle

theorem IndexedGrammar.Aho.ControlDenotation.RightPrefix.stack_eq_of_indexFree {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (hfree : IndexFree xs) (h : RightPrefix g xs before after) : before = after

theorem IndexedGrammar.Aho.ControlDenotation.RightPrefix.dollarFree {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (h : RightPrefix g xs before after) : DollarFree xs

theorem IndexedGrammar.Aho.ControlDenotation.RightPrefix.toRightRep {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {xs ys : List (WorkSym g)} {before after : BlockDenotation.VisibleStack g} (hp : RightPrefix g xs before after) (hr : RightRep g ys after) : RightRep g (xs ++ ys) before

inductive IndexedGrammar.Aho.ControlDenotation.ExecRep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : WorkCursor g → List g.ISym → Prop

Execution traversal coupled to the concrete stack visible from every active focus.

• done {T : Type} {g : IndexedGrammar T} [Fintype g.nt] : ExecRep g { left := [WorkSym.dollar], focus := WorkSym.hash, right := [] } []
• terminal {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} (a : T) (tail : ExecRep g { left := left, focus := next, right := right } form) : ExecRep g { left := left, focus := WorkSym.terminal a, right := next :: right } (ISym.terminal a :: form)
• plain {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {stack : BlockDenotation.VisibleStack g} (A : g.nt) (actual : List g.flag) (rightRep : RightRep g (next :: right) stack) (decorates : BlockDenotation.Decorates stack actual) (tail : ExecRep g { left := left, focus := next, right := right } form) : ExecRep g { left := left, focus := WorkSym.plain A, right := next :: right } (ISym.indexed A actual :: form)
• live {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} {stack : BlockDenotation.VisibleStack g} (A : g.nt) (actual : List g.flag) (rightRep : RightRep g (next :: right) stack) (decorates : BlockDenotation.LiveDecorates stack actual) (tail : ExecRep g { left := left, focus := next, right := right } form) : ExecRep g { left := left, focus := WorkSym.live A, right := next :: right } (ISym.indexed A actual :: form)
• index {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {left : List (WorkSym g)} {next : WorkSym g} {right : List (WorkSym g)} {form : List g.ISym} (R : CFlag g) (d : IndexMark) (tail : ExecRep g { left := left, focus := next, right := right } form) : ExecRep g { left := left, focus := WorkSym.index R d, right := next :: right } form
• returnFrame {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {alpha beta gamma : List (WorkSym g)} {Z : WorkSym g} {form : List g.ISym} (hfree : DollarFree beta) (tail : ExecRep g { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } form) : ExecRep g { left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } form

def IndexedGrammar.Aho.ControlDenotation.WorkCursor.Represents {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (cursor : WorkCursor g) (form : List g.ISym) : Prop

Whole-tape, execution-ordered cursor denotation.

Equations

• IndexedGrammar.Aho.ControlDenotation.WorkCursor.Represents cursor form = IndexedGrammar.Aho.ControlDenotation.ExecRep g (IndexedGrammar.Aho.ControlDenotation.normalizeCursor cursor) form

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

Equations

• IndexedGrammar.Aho.ControlDenotation.Config.Represents c form = IndexedGrammar.Aho.ControlDenotation.WorkCursor.Represents c.work form

Boundary configurations

theorem IndexedGrammar.Aho.ControlDenotation.initialConfig_represents {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : Config.Represents (initialConfig g) [ISym.indexed g.initial []]

theorem IndexedGrammar.Aho.ControlDenotation.finalConfig_represents {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (n : ℕ) : Config.Represents (finalConfig g n) []