Finite terminal support for indexed languages

Every indexed grammar has finitely many rules, and every rule has a finite right-hand side. Therefore each generated word uses only terminals from a finite set syntactically present in the grammar. This file packages that fact as a finite-alphabet restriction theorem.

def IndexedGrammarFiniteAlphabet.rhsSymbolTerminals {T N F : Type} : IRhsSymbol T N F → List T

The terminals appearing in a right-hand-side symbol.

Equations

• IndexedGrammarFiniteAlphabet.rhsSymbolTerminals (IRhsSymbol.terminal t) = [t]
• IndexedGrammarFiniteAlphabet.rhsSymbolTerminals (IRhsSymbol.nonterminal a a_1) = []

def IndexedGrammarFiniteAlphabet.ruleTerminals {T N F : Type} (r : IRule T N F) : List T

The terminals appearing in an indexed production rule.

Equations

• IndexedGrammarFiniteAlphabet.ruleTerminals r = List.flatMap IndexedGrammarFiniteAlphabet.rhsSymbolTerminals r.rhs

def IndexedGrammarFiniteAlphabet.grammarTerminalSet {T : Type} [DecidableEq T] (g : IndexedGrammar T) : Finset T

The finite terminal support syntactically mentioned by an indexed grammar.

Equations

• IndexedGrammarFiniteAlphabet.grammarTerminalSet g = (List.flatMap IndexedGrammarFiniteAlphabet.ruleTerminals g.rules).toFinset

def IndexedGrammarFiniteAlphabet.rhsSymbolSupported {T N F : Type} (S : Finset T) : IRhsSymbol T N F → Prop

Equations

• IndexedGrammarFiniteAlphabet.rhsSymbolSupported S (IRhsSymbol.terminal t) = (t ∈ S)
• IndexedGrammarFiniteAlphabet.rhsSymbolSupported S (IRhsSymbol.nonterminal a a_1) = True

def IndexedGrammarFiniteAlphabet.rhsSupported {T N F : Type} (S : Finset T) (rhs : List (IRhsSymbol T N F)) : Prop

Equations

• IndexedGrammarFiniteAlphabet.rhsSupported S rhs = ∀ s ∈ rhs, IndexedGrammarFiniteAlphabet.rhsSymbolSupported S s

def IndexedGrammarFiniteAlphabet.isymSupported {T : Type} {g : IndexedGrammar T} (S : Finset T) : g.ISym → Prop

Equations

• IndexedGrammarFiniteAlphabet.isymSupported S (IndexedGrammar.ISym.terminal t) = (t ∈ S)
• IndexedGrammarFiniteAlphabet.isymSupported S (IndexedGrammar.ISym.indexed a a_1) = True

def IndexedGrammarFiniteAlphabet.sententialSupported {T : Type} {g : IndexedGrammar T} (S : Finset T) (w : List g.ISym) : Prop

Equations

• IndexedGrammarFiniteAlphabet.sententialSupported S w = ∀ s ∈ w, IndexedGrammarFiniteAlphabet.isymSupported S s

def IndexedGrammarFiniteAlphabet.restrictRhsSymbolOfSupported {T N F : Type} (S : Finset T) (s : IRhsSymbol T N F) (h : rhsSymbolSupported S s) : IRhsSymbol { t : T // t ∈ S } N F

Equations

• IndexedGrammarFiniteAlphabet.restrictRhsSymbolOfSupported S (IRhsSymbol.terminal t) h_2 = IRhsSymbol.terminal ⟨t, h_2⟩
• IndexedGrammarFiniteAlphabet.restrictRhsSymbolOfSupported S (IRhsSymbol.nonterminal n push) h_2 = IRhsSymbol.nonterminal n push

def IndexedGrammarFiniteAlphabet.restrictRhsOfSupported {T N F : Type} (S : Finset T) (rhs : List (IRhsSymbol T N F)) (h : rhsSupported S rhs) : List (IRhsSymbol { t : T // t ∈ S } N F)

Equations

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

def IndexedGrammarFiniteAlphabet.unrestrictRhsSymbol {T : Type} {S : Finset T} {N F : Type} : IRhsSymbol { t : T // t ∈ S } N F → IRhsSymbol T N F

Equations

• IndexedGrammarFiniteAlphabet.unrestrictRhsSymbol (IRhsSymbol.terminal t) = IRhsSymbol.terminal ↑t
• IndexedGrammarFiniteAlphabet.unrestrictRhsSymbol (IRhsSymbol.nonterminal n push) = IRhsSymbol.nonterminal n push

theorem IndexedGrammarFiniteAlphabet.rule_rhs_supported {T : Type} [DecidableEq T] {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) : rhsSupported (grammarTerminalSet g) r.rhs

def IndexedGrammarFiniteAlphabet.restrictRule {T : Type} [DecidableEq T] (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : IRule { t : T // t ∈ grammarTerminalSet g } g.nt g.flag

Equations

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

def IndexedGrammarFiniteAlphabet.finiteAlphabetGrammar {T : Type} [DecidableEq T] (g : IndexedGrammar T) : IndexedGrammar { t : T // t ∈ grammarTerminalSet g }

The same indexed grammar, with terminals restricted to the finite set appearing in rules.

Equations

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

theorem IndexedGrammarFiniteAlphabet.finiteAlphabetGrammar_noEpsilon {T : Type} [DecidableEq T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : (finiteAlphabetGrammar g).NoEpsilon'

theorem IndexedGrammarFiniteAlphabet.restrictRule_isNF {T : Type} [DecidableEq T] {g : IndexedGrammar T} [DecidableEq g.nt] {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hNF : IndexedGrammar.IRule.IsNF r g.initial) : IndexedGrammar.IRule.IsNF (restrictRule g r hr) g.initial

theorem IndexedGrammarFiniteAlphabet.finiteAlphabetGrammar_isNormalForm {T : Type} [DecidableEq T] (g : IndexedGrammar T) [DecidableEq g.nt] (hNF : g.IsNormalForm) : (finiteAlphabetGrammar g).IsNormalForm

def IndexedGrammarFiniteAlphabet.unrestrictISym {T : Type} [DecidableEq T] (g : IndexedGrammar T) : (finiteAlphabetGrammar g).ISym → g.ISym

Equations

• IndexedGrammarFiniteAlphabet.unrestrictISym g (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal ↑t
• IndexedGrammarFiniteAlphabet.unrestrictISym g (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed n σ

def IndexedGrammarFiniteAlphabet.restrictISymOfSupported {T : Type} [DecidableEq T] (g : IndexedGrammar T) (s : g.ISym) (h : isymSupported (grammarTerminalSet g) s) : (finiteAlphabetGrammar g).ISym

Equations

• IndexedGrammarFiniteAlphabet.restrictISymOfSupported g (IndexedGrammar.ISym.terminal t) h_2 = IndexedGrammar.ISym.terminal ⟨t, h_2⟩
• IndexedGrammarFiniteAlphabet.restrictISymOfSupported g (IndexedGrammar.ISym.indexed n σ) h_2 = IndexedGrammar.ISym.indexed n σ

def IndexedGrammarFiniteAlphabet.restrictStringOfSupported {T : Type} [DecidableEq T] (g : IndexedGrammar T) (w : List g.ISym) (h : sententialSupported (grammarTerminalSet g) w) : List (finiteAlphabetGrammar g).ISym

Equations

• IndexedGrammarFiniteAlphabet.restrictStringOfSupported g w h = List.map (fun (s : { x : g.ISym // x ∈ w }) => IndexedGrammarFiniteAlphabet.restrictISymOfSupported g ↑s ⋯) w.attach

theorem IndexedGrammarFiniteAlphabet.derives_supported_of_supported {T : Type} [DecidableEq T] (g : IndexedGrammar T) {w₁ w₂ : List g.ISym} (h₁ : sententialSupported (grammarTerminalSet g) w₁) (h : g.Derives w₁ w₂) : sententialSupported (grammarTerminalSet g) w₂

theorem IndexedGrammarFiniteAlphabet.derives_supported {T : Type} [DecidableEq T] (g : IndexedGrammar T) {w : List g.ISym} (h : g.Derives [IndexedGrammar.ISym.indexed g.initial []] w) : sententialSupported (grammarTerminalSet g) w

A derivation from the start symbol mentions only terminals syntactically present in the indexed grammar's rules.

theorem IndexedGrammarFiniteAlphabet.language_supported {T : Type} [DecidableEq T] (g : IndexedGrammar T) {w : List T} (hw : w ∈ g.Language) (t : T) : t ∈ w → t ∈ grammarTerminalSet g

Every word generated by an indexed grammar is supported by the finite terminal set occurring in its rules.

def IndexedGrammarFiniteAlphabet.finiteAlphabetRestriction {T : Type} (S : Finset T) (L : Language T) : Language { t : T // t ∈ S }

Restrict a language to words over a finite terminal set.

Equations

• IndexedGrammarFiniteAlphabet.finiteAlphabetRestriction S L w = (List.map (fun (t : { t : T // t ∈ S }) => ↑t) w ∈ L)

theorem IndexedGrammarFiniteAlphabet.grammar_language_finiteAlphabetGrammar {T : Type} [DecidableEq T] (g : IndexedGrammar T) : (finiteAlphabetGrammar g).Language = finiteAlphabetRestriction (grammarTerminalSet g) g.Language

The restricted indexed grammar generates exactly the finite-alphabet restriction.

theorem IndexedGrammarFiniteAlphabet.finiteAlphabetRestriction_is_Indexed {T : Type} [DecidableEq T] (g : IndexedGrammar T) : is_Indexed (finiteAlphabetRestriction (grammarTerminalSet g) g.Language)

theorem IndexedGrammarFiniteAlphabet.finiteAlphabetRestriction_is_Indexed_noEpsilon {T : Type} [DecidableEq T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : is_Indexed_noEpsilon (finiteAlphabetRestriction (grammarTerminalSet g) g.Language)

theorem IndexedGrammarFiniteAlphabet.indexed_language_finiteAlphabet_Indexed_image {T : Type} [DecidableEq T] (g : IndexedGrammar T) : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_Indexed L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = g.Language

Any indexed grammar language is an image of an indexed language over a finite subtype of its terminal alphabet.

theorem IndexedGrammarFiniteAlphabet.indexed_language_finiteAlphabet_Indexed_noEpsilon_image {T : Type} [DecidableEq T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_Indexed_noEpsilon L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = g.Language

Any ε-free indexed grammar language is an image of an ε-free indexed language over a finite subtype of its terminal alphabet.

theorem is_Indexed_exists_finiteAlphabet_Indexed_image {T : Type} {L : Language T} (hL : is_Indexed L) : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_Indexed L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = L

Every indexed language is equivalent to an indexed language over a finite terminal subtype.

theorem is_Indexed_exists_fintype_alphabet_Indexed_image {T : Type} {L : Language T} (hL : is_Indexed L) : ∃ (A : Type) (x : Fintype A) (x : DecidableEq A) (L' : Language A) (f : A → T), is_Indexed L' ∧ (Language.map f) L' = L

Every indexed language is equivalent to an indexed language over some finite terminal alphabet. The finite alphabet is represented as a type carrying Fintype and DecidableEq, together with a terminal map into the original alphabet.

theorem is_Indexed_noEpsilon_exists_finiteAlphabet_Indexed_noEpsilon_image {T : Type} {L : Language T} (hL : is_Indexed_noEpsilon L) : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_Indexed_noEpsilon L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = L

Every ε-free indexed language is equivalent to an ε-free indexed language over a finite terminal subtype.

theorem is_Indexed_noEpsilon_exists_fintype_alphabet_Indexed_noEpsilon_image {T : Type} {L : Language T} (hL : is_Indexed_noEpsilon L) : ∃ (A : Type) (x : Fintype A) (x : DecidableEq A) (L' : Language A) (f : A → T), is_Indexed_noEpsilon L' ∧ (Language.map f) L' = L

Every ε-free indexed language is equivalent to an ε-free indexed language over some finite terminal alphabet.

theorem is_Indexed_of_finiteAlphabet_Indexed_image {T : Type} {S : Finset T} {L' : Language { t : T // t ∈ S }} (hL' : is_Indexed L') : is_Indexed ((Language.map fun (t : { t : T // t ∈ S }) => ↑t) L')

The inclusion image of an indexed language over a finite subtype is indexed over the ambient alphabet.

theorem is_Indexed_iff_exists_finiteAlphabet_Indexed_image {T : Type} {L : Language T} : is_Indexed L ↔ ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_Indexed L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = L

A language is indexed iff it is the inclusion image of an indexed language over a finite terminal subtype.

theorem is_Indexed_iff_exists_fintype_alphabet_Indexed_image {T : Type} {L : Language T} : is_Indexed L ↔ ∃ (A : Type) (x : Fintype A) (x : DecidableEq A) (L' : Language A) (f : A → T), is_Indexed L' ∧ (Language.map f) L' = L

A language is indexed iff it is the image of an indexed language over some finite terminal alphabet.

theorem is_Indexed_finite_terminal_support {T : Type} {L : Language T} (hL : is_Indexed L) : ∃ (S : Finset T), ∀ w ∈ L, ∀ t ∈ w, t ∈ S

Every indexed language has finite terminal support.