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

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 ⋯

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

Equations

• instDecidableEqIRhsSymbol = instDecidableEqIRhsSymbol.decEq

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)

Uniform stack-suffix extension

def IndexedGrammar.ISym.appendStackSuffix {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) : g.ISym → g.ISym

Equations

• IndexedGrammar.ISym.appendStackSuffix suffix (IndexedGrammar.ISym.terminal a) = IndexedGrammar.ISym.terminal a
• IndexedGrammar.ISym.appendStackSuffix suffix (IndexedGrammar.ISym.indexed A σ) = IndexedGrammar.ISym.indexed A (σ ++ suffix)

def IndexedGrammar.appendStackSuffixes {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (w : List g.ISym) : List g.ISym

Equations

• IndexedGrammar.appendStackSuffixes suffix w = List.map (IndexedGrammar.ISym.appendStackSuffix suffix) w

@[simp]

theorem IndexedGrammar.ISym.appendStackSuffix_terminal {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (a : T) : appendStackSuffix suffix (terminal a) = terminal a

@[simp]

theorem IndexedGrammar.ISym.appendStackSuffix_indexed {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (A : g.nt) (σ : List g.flag) : appendStackSuffix suffix (indexed A σ) = indexed A (σ ++ suffix)

@[simp]

theorem IndexedGrammar.appendStackSuffixes_nil {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) : appendStackSuffixes suffix [] = []

@[simp]

theorem IndexedGrammar.appendStackSuffixes_cons {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (s : g.ISym) (w : List g.ISym) : appendStackSuffixes suffix (s :: w) = ISym.appendStackSuffix suffix s :: appendStackSuffixes suffix w

@[simp]

theorem IndexedGrammar.appendStackSuffixes_append {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (u v : List g.ISym) : appendStackSuffixes suffix (u ++ v) = appendStackSuffixes suffix u ++ appendStackSuffixes suffix v

@[simp]

theorem IndexedGrammar.appendStackSuffixes_length {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (w : List g.ISym) : (appendStackSuffixes suffix w).length = w.length

@[simp]

theorem IndexedGrammar.appendStackSuffixes_map_terminal {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (w : List T) : appendStackSuffixes suffix (List.map (fun (a : T) => ISym.terminal a) w) = List.map (fun (a : T) => ISym.terminal a) w

@[simp]

theorem IndexedGrammar.appendStackSuffixes_expandRhs {T : Type} {g : IndexedGrammar T} (suffix : List g.flag) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) : appendStackSuffixes suffix (g.expandRhs rhs σ) = g.expandRhs rhs (σ ++ suffix)

theorem IndexedGrammar.transforms_appendStackSuffixes {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) (suffix : List g.flag) : g.Transforms (appendStackSuffixes suffix w₁) (appendStackSuffixes suffix w₂)

theorem IndexedGrammar.derives_appendStackSuffixes {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) (suffix : List g.flag) : g.Derives (appendStackSuffixes suffix w₁) (appendStackSuffixes suffix w₂)

theorem IndexedGrammar.derives_appendStackSuffix_indexed {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List g.ISym} (h : g.Derives [ISym.indexed A σ] w) (suffix : List g.flag) : g.Derives [ISym.indexed A (σ ++ suffix)] (appendStackSuffixes suffix w)

theorem IndexedGrammar.derives_appendStackSuffix_to_terminals {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (h : g.Derives [ISym.indexed A σ] (List.map ISym.terminal w)) (suffix : List g.flag) : g.Derives [ISym.indexed A (σ ++ suffix)] (List.map ISym.terminal w)

def IndexedGrammar.NoEpsilon' {T : Type} (g : IndexedGrammar T) : Prop

A grammar has no ε-productions.

Equations

• g.NoEpsilon' = ∀ r ∈ g.rules, r.rhs ≠ []

theorem IndexedGrammar.transforms_length_le_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : w₁.length ≤ w₂.length

theorem IndexedGrammar.derives_length_le_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : w₁.length ≤ w₂.length

theorem IndexedGrammar.not_generates_nil_of_noEpsilon {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : ¬g.Generates []

def IndexedGrammar.TerminalsIsolated {T : Type} (g : IndexedGrammar T) : Prop

A grammar has terminals isolated: each rule's RHS either is a single terminal, or consists entirely of nonterminals (with optional flag annotations).

Equations

• g.TerminalsIsolated = ∀ r ∈ g.rules, (∃ (a : T), r.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r.rhs, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

def IndexedGrammar.StartNotOnRhs' {T : Type} (g : IndexedGrammar T) : Prop

The start symbol does not appear on the right-hand side of any rule.

Equations

• g.StartNotOnRhs' = ∀ r ∈ g.rules, ∀ s ∈ r.rhs, match s with | IRhsSymbol.nonterminal n a => n ≠ g.initial | IRhsSymbol.terminal a => True

def IndexedGrammar.IRule.FlagsSeparated {T N F : Type} (r : IRule T N F) : Prop

A rule has separated flag operations.

Equations

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

def IndexedGrammar.FlagsSeparated {T : Type} (g : IndexedGrammar T) : Prop

All rules in the grammar have separated flag operations.

Equations

• g.FlagsSeparated = ∀ r ∈ g.rules, IndexedGrammar.IRule.FlagsSeparated r

def IndexedGrammar.IRule.IsNF {T N F : Type} [DecidableEq N] (r : IRule T N F) (s : N) : Prop

A production rule is in normal form with respect to a start symbol s.

Equations

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

def IndexedGrammar.IsNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] : Prop

An indexed grammar is in normal form if every production rule is in normal form with respect to the start symbol.

Equations

• g.IsNormalForm = ∀ r ∈ g.rules, IndexedGrammar.IRule.IsNF r g.initial

theorem IndexedGrammar.IRule.rhs_ne_nil_of_isNF {T N F : Type} [DecidableEq N] {r : IRule T N F} {start : N} (h : IsNF r start) : r.rhs ≠ []

theorem IndexedGrammar.IRule.terminalsIsolated_of_isNF {T N F : Type} [DecidableEq N] {r : IRule T N F} {start : N} (h : IsNF r start) : (∃ (a : T), r.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r.rhs, ∃ (n : N) (f : Option F), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.IRule.flagsSeparated_of_isNF {T N F : Type} [DecidableEq N] {r : IRule T N F} {start : N} (h : IsNF r start) : FlagsSeparated r

theorem IndexedGrammar.IRule.startNotOnRhs_of_isNF {T N F : Type} [DecidableEq N] {r : IRule T N F} {start : N} (h : IsNF r start) (s : IRhsSymbol T N F) : s ∈ r.rhs → match s with | IRhsSymbol.nonterminal n a => n ≠ start | IRhsSymbol.terminal a => True

theorem IndexedGrammar.noEpsilon_of_isNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] (h : g.IsNormalForm) : g.NoEpsilon'

theorem IndexedGrammar.terminalsIsolated_of_isNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] (h : g.IsNormalForm) : g.TerminalsIsolated

theorem IndexedGrammar.flagsSeparated_of_isNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] (h : g.IsNormalForm) : g.FlagsSeparated

theorem IndexedGrammar.startNotOnRhs_of_isNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] (h : g.IsNormalForm) : g.StartNotOnRhs'