Aho's finite compression of index strings

This file contains the grammar-facing part of Aho's linear-space simulation of an indexed grammar. A stack-neutral derivation is saturated into the four normal-form rule shapes, and a possibly long string of flags is represented by the finite binary relation it induces on nonterminals when it is consumed.

The actual marked-derivation machine and its linear tape bound are deliberately kept separate. The declarations here only expose finite symbols and semantic lemmas that such a machine can use.

Reference

• A. V. Aho, "Indexed grammars -- an extension of context-free grammars", JACM 15(4), Section 5, 1968.

Concrete normal-form rule predicates

def IndexedGrammar.Aho.BinaryRule {T : Type} (g : IndexedGrammar T) (A B C : g.nt) : Prop

A concrete binary rule A -> B C.

Equations

• IndexedGrammar.Aho.BinaryRule g A B C = ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]

def IndexedGrammar.Aho.PopRule {T : Type} (g : IndexedGrammar T) (A : g.nt) (f : g.flag) (B : g.nt) : Prop

A concrete flag-pop rule A f -> B.

Equations

• IndexedGrammar.Aho.PopRule g A f B = ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none]

def IndexedGrammar.Aho.PushRule {T : Type} (g : IndexedGrammar T) (A B : g.nt) (f : g.flag) : Prop

A concrete flag-push rule A -> B f.

Equations

• IndexedGrammar.Aho.PushRule g A B f = ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.nonterminal B (some f)]

def IndexedGrammar.Aho.TerminalRule {T : Type} (g : IndexedGrammar T) (A : g.nt) (a : T) : Prop

A concrete terminal rule A -> a.

Equations

• IndexedGrammar.Aho.TerminalRule g A a = ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = [IRhsSymbol.terminal a]

Stack-neutral saturation

def IndexedGrammar.Aho.Neutral {T : Type} (g : IndexedGrammar T) (A B : g.nt) : Prop

Neutral g A B means that A can become B while starting and ending with an empty stack and without leaving any other sentential symbols behind. In normal form such a derivation can only consist of balanced flag pushes and pops; the semantic definition is more convenient for the saturation lemmas below.

Equations

• IndexedGrammar.Aho.Neutral g A B = g.Derives [IndexedGrammar.ISym.indexed A []] [IndexedGrammar.ISym.indexed B []]

theorem IndexedGrammar.Aho.Neutral.refl {T : Type} (g : IndexedGrammar T) (A : g.nt) : Neutral g A A

theorem IndexedGrammar.Aho.Neutral.trans {T : Type} {g : IndexedGrammar T} {A B C : g.nt} (hAB : Neutral g A B) (hBC : Neutral g B C) : Neutral g A C

theorem IndexedGrammar.Aho.Neutral.lift_suffix {T : Type} {g : IndexedGrammar T} {A B : g.nt} (h : Neutral g A B) (suffix : List g.flag) : g.Derives [ISym.indexed A suffix] [ISym.indexed B suffix]

A neutral derivation is parametric in an arbitrary inherited stack suffix.

Aho's augmented rule predicates

Rather than materializing an equivalent augmented grammar, we use its rules as finite semantic predicates. Ordinary terminal, binary, and push rules are precomposed with neutral closure. A pop edge is saturated on both sides: a neutral prefix may expose the concrete pop, and a neutral suffix may follow it. The prefix saturation is essential when a balanced push/pop segment lies between a productive event and the next inherited flag consumption.

def IndexedGrammar.Aho.AugTerminal {T : Type} (g : IndexedGrammar T) (A : g.nt) (a : T) : Prop

An augmented terminal edge: A =>* B -> a, with the first part stack-neutral.

Equations

• IndexedGrammar.Aho.AugTerminal g A a = ∃ (B : g.nt), IndexedGrammar.Aho.Neutral g A B ∧ IndexedGrammar.Aho.TerminalRule g B a

def IndexedGrammar.Aho.AugBinary {T : Type} (g : IndexedGrammar T) (A B C : g.nt) : Prop

An augmented binary edge: A =>* D -> B C, with the first part stack-neutral.

Equations

• IndexedGrammar.Aho.AugBinary g A B C = ∃ (D : g.nt), IndexedGrammar.Aho.Neutral g A D ∧ IndexedGrammar.Aho.BinaryRule g D B C

def IndexedGrammar.Aho.AugPush {T : Type} (g : IndexedGrammar T) (A B : g.nt) (f : g.flag) : Prop

An augmented push edge: A =>* C -> B f, with the first part stack-neutral.

Equations

• IndexedGrammar.Aho.AugPush g A B f = ∃ (C : g.nt), IndexedGrammar.Aho.Neutral g A C ∧ IndexedGrammar.Aho.PushRule g C B f

def IndexedGrammar.Aho.AugPop {T : Type} (g : IndexedGrammar T) (f : g.flag) (A B : g.nt) : Prop

The relation induced by consuming one augmented flag: take a neutral prefix, pop f, then take a neutral suffix. The flag argument comes first because AugPop g f is used as a binary relation.

Equations

• IndexedGrammar.Aho.AugPop g f A B = ∃ (D : g.nt) (C : g.nt), IndexedGrammar.Aho.Neutral g A D ∧ IndexedGrammar.Aho.PopRule g D f C ∧ IndexedGrammar.Aho.Neutral g C B

Ordinary rules embed into the augmented predicates

theorem IndexedGrammar.Aho.terminalRule_aug {T : Type} {g : IndexedGrammar T} {A : g.nt} {a : T} (h : TerminalRule g A a) : AugTerminal g A a

theorem IndexedGrammar.Aho.binaryRule_aug {T : Type} {g : IndexedGrammar T} {A B C : g.nt} (h : BinaryRule g A B C) : AugBinary g A B C

theorem IndexedGrammar.Aho.pushRule_aug {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : PushRule g A B f) : AugPush g A B f

theorem IndexedGrammar.Aho.popRule_aug {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : PopRule g A f B) : AugPop g f A B

One-rule semantic facts

theorem IndexedGrammar.Aho.binaryRule_transforms {T : Type} {g : IndexedGrammar T} {A B C : g.nt} (h : BinaryRule g A B C) (suffix : List g.flag) : g.Transforms [ISym.indexed A suffix] [ISym.indexed B suffix, ISym.indexed C suffix]

theorem IndexedGrammar.Aho.popRule_transforms {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : PopRule g A f B) (suffix : List g.flag) : g.Transforms [ISym.indexed A (f :: suffix)] [ISym.indexed B suffix]

theorem IndexedGrammar.Aho.pushRule_transforms {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : PushRule g A B f) (suffix : List g.flag) : g.Transforms [ISym.indexed A suffix] [ISym.indexed B (f :: suffix)]

theorem IndexedGrammar.Aho.terminalRule_transforms {T : Type} {g : IndexedGrammar T} {A : g.nt} {a : T} (h : TerminalRule g A a) (suffix : List g.flag) : g.Transforms [ISym.indexed A suffix] [ISym.terminal a]

Soundness of augmented edges

theorem IndexedGrammar.Aho.augTerminal_derives {T : Type} {g : IndexedGrammar T} {A : g.nt} {a : T} (h : AugTerminal g A a) (suffix : List g.flag) : g.Derives [ISym.indexed A suffix] [ISym.terminal a]

theorem IndexedGrammar.Aho.augBinary_derives {T : Type} {g : IndexedGrammar T} {A B C : g.nt} (h : AugBinary g A B C) (suffix : List g.flag) : g.Derives [ISym.indexed A suffix] [ISym.indexed B suffix, ISym.indexed C suffix]

theorem IndexedGrammar.Aho.augPush_derives {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : AugPush g A B f) (suffix : List g.flag) : g.Derives [ISym.indexed A suffix] [ISym.indexed B (f :: suffix)]

theorem IndexedGrammar.Aho.augPop_derives {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} (h : AugPop g f A B) (suffix : List g.flag) : g.Derives [ISym.indexed A (f :: suffix)] [ISym.indexed B suffix]

Finite compressed flags

@[reducible, inline]

abbrev IndexedGrammar.Aho.CFlag {T : Type} (g : IndexedGrammar T) : Type

A compressed flag is the Boolean adjacency matrix of the relation it induces on nonterminals. For a finite nonterminal type this is itself a finite type, independently of the number or length of concrete flag strings represented by it.

Equations

• IndexedGrammar.Aho.CFlag g = (g.nt → g.nt → Bool)

def IndexedGrammar.Aho.cflagZero {T : Type} (g : IndexedGrammar T) : CFlag g

The empty compressed relation.

Equations

• IndexedGrammar.Aho.cflagZero g x✝¹ x✝ = false

noncomputable def IndexedGrammar.Aho.cflagBase {T : Type} (g : IndexedGrammar T) (f : g.flag) : CFlag g

The compressed relation denoted by one concrete flag, including Aho's neutral post-saturation of a pop edge.

Equations

• IndexedGrammar.Aho.cflagBase g f A B = decide (IndexedGrammar.Aho.AugPop g f A B)

def IndexedGrammar.Aho.cflagComp {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (first second : CFlag g) : CFlag g

Relational composition of two compressed flags. If the concrete stack begins with the first flag and then the second, it is denoted by cflagComp first second.

Equations

• IndexedGrammar.Aho.cflagComp g first second A C = decide (∃ (B : g.nt), first A B = true ∧ second B C = true)

def IndexedGrammar.Aho.CFlag.Nonempty {T : Type} {g : IndexedGrammar T} (R : CFlag g) : Prop

A compressed relation has at least one usable edge.

Equations

• R.Nonempty = ∃ (A : g.nt) (B : g.nt), R A B = true

theorem IndexedGrammar.Aho.CFlag.ext {T : Type} {g : IndexedGrammar T} {R S : CFlag g} (h : ∀ (A B : g.nt), R A B = S A B) : R = S

Extensionality specialized to compressed flags.

theorem IndexedGrammar.Aho.CFlag.ext_iff {T : Type} {g : IndexedGrammar T} {R S : CFlag g} : R = S ↔ ∀ (A B : g.nt), R A B = S A B

@[simp]

theorem IndexedGrammar.Aho.cflagZero_apply {T : Type} {g : IndexedGrammar T} (A B : g.nt) : cflagZero g A B = false

@[simp]

theorem IndexedGrammar.Aho.cflagBase_apply {T : Type} {g : IndexedGrammar T} (f : g.flag) (A B : g.nt) : cflagBase g f A B = true ↔ AugPop g f A B

@[simp]

theorem IndexedGrammar.Aho.cflagComp_apply {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (first second : CFlag g) (A C : g.nt) : cflagComp g first second A C = true ↔ ∃ (B : g.nt), first A B = true ∧ second B C = true

theorem IndexedGrammar.Aho.cflagComp_assoc {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (R S U : CFlag g) : cflagComp g (cflagComp g R S) U = cflagComp g R (cflagComp g S U)

@[simp]

theorem IndexedGrammar.Aho.cflagComp_zero_left {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (R : CFlag g) : cflagComp g (cflagZero g) R = cflagZero g

@[simp]

theorem IndexedGrammar.Aho.cflagComp_zero_right {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (R : CFlag g) : cflagComp g R (cflagZero g) = cflagZero g

@[simp]

theorem IndexedGrammar.Aho.cflagZero_not_nonempty {T : Type} {g : IndexedGrammar T} : ¬(cflagZero g).Nonempty

theorem IndexedGrammar.Aho.CFlag.eq_zero_iff_not_nonempty {T : Type} {g : IndexedGrammar T} (R : CFlag g) : R = cflagZero g ↔ ¬R.Nonempty

theorem IndexedGrammar.Aho.cflagComp_nonempty_iff {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (R S : CFlag g) : (cflagComp g R S).Nonempty ↔ ∃ (A : g.nt) (B : g.nt) (C : g.nt), R A B = true ∧ S B C = true

theorem IndexedGrammar.Aho.cflagComp_nonempty_left {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {R S : CFlag g} (h : (cflagComp g R S).Nonempty) : R.Nonempty

theorem IndexedGrammar.Aho.cflagComp_nonempty_right {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {R S : CFlag g} (h : (cflagComp g R S).Nonempty) : S.Nonempty

theorem IndexedGrammar.Aho.cflagBase_edge_derives {T : Type} {g : IndexedGrammar T} {f : g.flag} {A B : g.nt} (h : cflagBase g f A B = true) (suffix : List g.flag) : g.Derives [ISym.indexed A (f :: suffix)] [ISym.indexed B suffix]

A base compressed edge is exactly an augmented one-flag pop edge.

inductive IndexedGrammar.Aho.CFlag.Denotes {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : List g.flag → CFlag g → Prop

Provenance for a compressed relation. Denotes g flags R records that R was built from the concrete, top-first flag string flags by Aho's base relation and relational composition. It is useful as a soundness invariant for a machine whose finite alphabet contains every Boolean relation, but whose reachable compressed symbols arise only through cflagBase and cflagComp.

• base {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (f : g.flag) : Denotes g [f] (cflagBase g f)
• comp {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {fs gs : List g.flag} {R S : CFlag g} (hR : Denotes g fs R) (hS : Denotes g gs S) : Denotes g (fs ++ gs) (cflagComp g R S)

theorem IndexedGrammar.Aho.CFlag.Denotes.edge_derives {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {R : CFlag g} (hden : Denotes g flags R) {A B : g.nt} (hedge : R A B = true) (suffix : List g.flag) : g.Derives [ISym.indexed A (flags ++ suffix)] [ISym.indexed B suffix]

Every edge of a denoted compressed relation is sound for consuming the represented concrete flag string above any inherited stack suffix.