Indexed Grammar Definitions

This file defines indexed grammars (Aho, 1968), their derivation relation, and the induced language predicate.

An indexed grammar extends context-free grammars by attaching a stack of flags (index symbols) to each nonterminal in a sentential form. Productions can push flags onto, or pop flags from, these stacks.

Main declarations

• IndexedGrammar — the grammar structure
• IndexedGrammar.SententialForm — sentential forms with stacked nonterminals
• IndexedGrammar.Transforms — one-step derivation
• IndexedGrammar.Derives — reflexive–transitive closure of Transforms
• IndexedGrammar.Language — the generated language

References

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

inductive IRhsSymbol (T N F : Type) : Type

A symbol on the right-hand side of an indexed production. A nonterminal can optionally have a flag pushed onto its inherited stack.

• terminal {T N F : Type} : T → IRhsSymbol T N F
• nonterminal {T N F : Type} : N → Option F → IRhsSymbol T N F

instance instDecidableEqIRhsSymbol {T✝ N✝ F✝ : Type} [DecidableEq T✝] [DecidableEq N✝] [DecidableEq F✝] : DecidableEq (IRhsSymbol T✝ N✝ F✝)

Equations

• instDecidableEqIRhsSymbol = instDecidableEqIRhsSymbol.decEq

def instDecidableEqIRhsSymbol.decEq {T✝ N✝ F✝ : Type} [DecidableEq T✝] [DecidableEq N✝] [DecidableEq F✝] (x✝ x✝¹ : IRhsSymbol T✝ N✝ F✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqIRhsSymbol.decEq (IRhsSymbol.terminal a) (IRhsSymbol.terminal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqIRhsSymbol.decEq (IRhsSymbol.terminal a) (IRhsSymbol.nonterminal a_1 a_2) = isFalse ⋯
• instDecidableEqIRhsSymbol.decEq (IRhsSymbol.nonterminal a a_1) (IRhsSymbol.terminal a_2) = isFalse ⋯
• instDecidableEqIRhsSymbol.decEq (IRhsSymbol.nonterminal a a_1) (IRhsSymbol.nonterminal b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

structure IRule (T N F : Type) : Type

A production rule of an indexed grammar.

• lhs : the nonterminal on the left-hand side.
• consume : if some f, the rule can only fire when f is on top of the nonterminal's stack, and pops it; if none, no flag is consumed.
• rhs : the right-hand side; each nonterminal inherits the (possibly modified) stack of the left-hand side, with an optional additional flag push.

• lhs : N
• consume : Option F
• rhs : List (IRhsSymbol T N F)

structure IndexedGrammar (T : Type) : Type 1

An indexed grammar that generates words over the alphabet T.

• nt : type of nonterminals
• flag : type of index symbols (flags)
• initial : the start nonterminal
• rules : the list of production rules

• nt : Type
• flag : Type
• initial : self.nt
• rules : List (IRule T self.nt self.flag)

inductive IndexedGrammar.ISym {T : Type} (g : IndexedGrammar T) : Type

A symbol in a sentential form of an indexed grammar: either a terminal or a nonterminal equipped with its current flag stack.

• terminal {T : Type} {g : IndexedGrammar T} : T → g.ISym
• indexed {T : Type} {g : IndexedGrammar T} : g.nt → List g.flag → g.ISym

def IndexedGrammar.expandRhs {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) : List g.ISym

Expand the right-hand side of a rule, distributing the given stack σ to every nonterminal (and pushing any specified flag on top).

Equations

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

def IndexedGrammar.Transforms {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

One step of indexed-grammar transformation.

Equations

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

def IndexedGrammar.Derives {T : Type} (g : IndexedGrammar T) : List g.ISym → List g.ISym → Prop

Any number of steps of indexed-grammar transformation.

Equations

• g.Derives = Relation.ReflTransGen g.Transforms

def IndexedGrammar.Generates {T : Type} (g : IndexedGrammar T) (w : List T) : Prop

A word (list of terminals) is generated by the grammar if it can be derived from the initial nonterminal (with empty stack).

Equations

• g.Generates w = g.Derives [IndexedGrammar.ISym.indexed g.initial []] (List.map IndexedGrammar.ISym.terminal w)

def IndexedGrammar.Language {T : Type} (g : IndexedGrammar T) : _root_.Language T

The language generated by the grammar.

Equations

• g.Language = setOf g.Generates

theorem IndexedGrammar.deri_self {T : Type} (g : IndexedGrammar T) (w : List g.ISym) : g.Derives w w

theorem IndexedGrammar.deri_of_tran {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : g.Derives w₁ w₂

theorem IndexedGrammar.deri_of_deri_deri {T : Type} {g : IndexedGrammar T} {w₁ w₂ w₃ : List g.ISym} (h₁ : g.Derives w₁ w₂) (h₂ : g.Derives w₂ w₃) : g.Derives w₁ w₃

theorem IndexedGrammar.deri_of_deri_tran {T : Type} {g : IndexedGrammar T} {w₁ w₂ w₃ : List g.ISym} (h₁ : g.Derives w₁ w₂) (h₂ : g.Transforms w₂ w₃) : g.Derives w₁ w₃

theorem IndexedGrammar.deri_of_tran_deri {T : Type} {g : IndexedGrammar T} {w₁ w₂ w₃ : List g.ISym} (h₁ : g.Transforms w₁ w₂) (h₂ : g.Derives w₂ w₃) : g.Derives w₁ w₃

theorem IndexedGrammar.deri_with_prefix {T : Type} {g : IndexedGrammar T} (p : List g.ISym) {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : g.Derives (p ++ w₁) (p ++ w₂)

theorem IndexedGrammar.deri_with_suffix {T : Type} {g : IndexedGrammar T} (s : List g.ISym) {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : g.Derives (w₁ ++ s) (w₂ ++ s)