Indexed Languages Intersected with Regular Languages

For an indexed grammar in Aho normal form, annotate each nonterminal with the entry and exit states of a DFA. Binary rules thread an intermediate state, push/pop rules preserve both endpoints, and terminal rules realize one DFA transition. Parse certificates give a compact soundness and completeness proof.

structure IndexedDFA.nt (N σ : Type) : Type

An indexed nonterminal annotated with the DFA states immediately before and after the word generated by that nonterminal.

• start : σ
• core : N
• stop : σ

def IndexedDFA.instDecidableEqNt.decEq {N✝ σ✝ : Type} [DecidableEq N✝] [DecidableEq σ✝] (x✝ x✝¹ : nt N✝ σ✝) : Decidable (x✝ = x✝¹)

Equations

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

instance IndexedDFA.instDecidableEqNt {N✝ σ✝ : Type} [DecidableEq N✝] [DecidableEq σ✝] : DecidableEq (nt N✝ σ✝)

Equations

• IndexedDFA.instDecidableEqNt = IndexedDFA.instDecidableEqNt.decEq

instance IndexedDFA.nt.fintype {N σ : Type} [Fintype N] [Fintype σ] : Fintype (nt N σ)

Equations

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

def IndexedGrammar.dfaBinaryRule {T σ : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (p m q : σ) (B C : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag

Equations

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

def IndexedGrammar.dfaPopRule {T σ : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (p q : σ) (f : g.flag) (B : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag

Equations

• g.dfaPopRule r p q f B = { lhs := { start := p, core := r.lhs, stop := q }, consume := some f, rhs := [IRhsSymbol.nonterminal { start := p, core := B, stop := q } none] }

def IndexedGrammar.dfaPushRule {T σ : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (p q : σ) (f : g.flag) (B : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag

Equations

• g.dfaPushRule r p q f B = { lhs := { start := p, core := r.lhs, stop := q }, consume := none, rhs := [IRhsSymbol.nonterminal { start := p, core := B, stop := q } (some f)] }

def IndexedGrammar.dfaTerminalRule {T σ : Type} (g : IndexedGrammar T) (M : DFA T σ) (r : IRule T g.nt g.flag) (p : σ) (a : T) : IRule T (IndexedDFA.nt g.nt σ) g.flag

Equations

• g.dfaTerminalRule M r p a = { lhs := { start := p, core := r.lhs, stop := M.step p a }, consume := none, rhs := [IRhsSymbol.terminal a] }

def IndexedGrammar.dfaRulesFor {T σ : Type} [Fintype σ] (g : IndexedGrammar T) (M : DFA T σ) (r : IRule T g.nt g.flag) : List (IRule T (IndexedDFA.nt g.nt σ) g.flag)

All DFA-threaded copies of one indexed-normal-form rule. Malformed rules contribute no product rules.

Equations

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

def IndexedGrammar.dfaProduct {T σ : Type} [Fintype σ] (g : IndexedGrammar T) (M : DFA T σ) (p q : σ) : IndexedGrammar T

Product of a normal-form indexed grammar and a DFA, with fixed initial and final DFA states.

Equations

• g.dfaProduct M p q = { nt := IndexedDFA.nt g.nt σ, flag := g.flag, initial := { start := p, core := g.initial, stop := q }, rules := List.flatMap (g.dfaRulesFor M) g.rules }

theorem Indexed_of_Indexed_inter_regular {T : Type} [Fintype T] (L R : Language T) (hL : is_Indexed L) (hR : R.IsRegular) : is_Indexed (L ⊓ R)

An indexed language intersected with a regular language is indexed.

theorem Indexed_closedUnderIntersectionWithRegular {T : Type} [Fintype T] : ClosedUnderIntersectionWithRegular is_Indexed

Predicate-form closure theorem used by the closure table.