Finite terminal support for context-sensitive languages

Every grammar in this repository has finitely many rules, and every rule is a finite list of symbols. Hence every grammar-generated language uses only finitely many terminal symbols. This file packages that observation for context-sensitive languages as a finite-alphabet image theorem.

def GrammarFiniteAlphabet.symbolTerminals {T N : Type} : symbol T N → List T

The terminals appearing in a grammar symbol.

Equations

• GrammarFiniteAlphabet.symbolTerminals (symbol.terminal t) = [t]
• GrammarFiniteAlphabet.symbolTerminals (symbol.nonterminal a) = []

def GrammarFiniteAlphabet.stringTerminals {T N : Type} (w : List (symbol T N)) : List T

The terminals appearing in a sentential form.

Equations

• GrammarFiniteAlphabet.stringTerminals w = List.flatMap GrammarFiniteAlphabet.symbolTerminals w

def GrammarFiniteAlphabet.ruleTerminals {T N : Type} (r : grule T N) : List T

The terminals appearing anywhere in a grammar rule.

Equations

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

def GrammarFiniteAlphabet.grammarTerminalSet {T : Type} [DecidableEq T] (g : grammar T) : Finset T

The finite terminal support syntactically mentioned by a grammar.

Equations

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

def GrammarFiniteAlphabet.symbolSupported {T N : Type} (S : Finset T) : symbol T N → Prop

Equations

• GrammarFiniteAlphabet.symbolSupported S (symbol.terminal t) = (t ∈ S)
• GrammarFiniteAlphabet.symbolSupported S (symbol.nonterminal a) = True

def GrammarFiniteAlphabet.sententialSupported {T N : Type} (S : Finset T) (w : List (symbol T N)) : Prop

Equations

• GrammarFiniteAlphabet.sententialSupported S w = ∀ s ∈ w, GrammarFiniteAlphabet.symbolSupported S s

def GrammarFiniteAlphabet.restrictSymbolOfSupported {T N : Type} (S : Finset T) (s : symbol T N) (h : symbolSupported S s) : symbol { t : T // t ∈ S } N

Equations

• GrammarFiniteAlphabet.restrictSymbolOfSupported S (symbol.terminal t) h_2 = symbol.terminal ⟨t, h_2⟩
• GrammarFiniteAlphabet.restrictSymbolOfSupported S (symbol.nonterminal n) h_2 = symbol.nonterminal n

def GrammarFiniteAlphabet.restrictStringOfSupported {T N : Type} (S : Finset T) (w : List (symbol T N)) (h : sententialSupported S w) : List (symbol { t : T // t ∈ S } N)

Equations

• GrammarFiniteAlphabet.restrictStringOfSupported S w h = List.map (fun (s : { x : symbol T N // x ∈ w }) => GrammarFiniteAlphabet.restrictSymbolOfSupported S ↑s ⋯) w.attach

def GrammarFiniteAlphabet.unrestrictSymbol {T : Type} {S : Finset T} {N : Type} : symbol { t : T // t ∈ S } N → symbol T N

Equations

• GrammarFiniteAlphabet.unrestrictSymbol (symbol.terminal t) = symbol.terminal ↑t
• GrammarFiniteAlphabet.unrestrictSymbol (symbol.nonterminal n) = symbol.nonterminal n

theorem GrammarFiniteAlphabet.rule_input_L_supported {T : Type} [DecidableEq T] {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : sententialSupported (grammarTerminalSet g) r.input_L

theorem GrammarFiniteAlphabet.rule_input_R_supported {T : Type} [DecidableEq T] {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : sententialSupported (grammarTerminalSet g) r.input_R

theorem GrammarFiniteAlphabet.rule_output_supported {T : Type} [DecidableEq T] {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : sententialSupported (grammarTerminalSet g) r.output_string

theorem GrammarFiniteAlphabet.grammar_derives_supported {T : Type} [DecidableEq T] (g : grammar T) {w : List (symbol T g.nt)} (h : grammar_derives g [symbol.nonterminal g.initial] w) : sententialSupported (grammarTerminalSet g) w

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

def GrammarFiniteAlphabet.restrictRule {T : Type} [DecidableEq T] (g : grammar T) (r : grule T g.nt) (hr : r ∈ g.rules) : grule { t : T // t ∈ grammarTerminalSet g } g.nt

Equations

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

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

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

Equations

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

def GrammarFiniteAlphabet.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

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

theorem GrammarFiniteAlphabet.grammar_language_finiteAlphabetGrammar {T : Type} [DecidableEq T] (g : grammar T) : grammar_language (finiteAlphabetGrammar g) = finiteAlphabetRestriction (grammarTerminalSet g) (grammar_language g)

theorem GrammarFiniteAlphabet.finiteAlphabetRestriction_is_CS {T : Type} [DecidableEq T] (g : grammar T) (hg : grammar_context_sensitive g) : is_CS (finiteAlphabetRestriction (grammarTerminalSet g) (grammar_language g))

theorem GrammarFiniteAlphabet.grammar_language_supported {T : Type} [DecidableEq T] (g : grammar T) {w : List T} (hw : w ∈ grammar_language g) (t : T) : t ∈ w → t ∈ grammarTerminalSet g

Every word generated by a grammar is supported by the finite terminal set occurring in the grammar's rules.

theorem GrammarFiniteAlphabet.map_finiteAlphabetRestriction_eq_of_supported {T : Type} (S : Finset T) (L : Language T) (hS : ∀ w ∈ L, ∀ t ∈ w, t ∈ S) : (Language.map fun (t : { t : T // t ∈ S }) => ↑t) (finiteAlphabetRestriction S L) = L

If S supports L, then L is the image of its restriction to the finite subtype S.

theorem GrammarFiniteAlphabet.grammar_language_finiteAlphabet_image {T : Type} [DecidableEq T] (g : grammar T) : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = grammar_language g

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

theorem GrammarFiniteAlphabet.grammar_language_finiteAlphabet_CS_image {T : Type} [DecidableEq T] (g : grammar T) (hg : grammar_context_sensitive g) : ∃ (S : Finset T) (L' : Language { t : T // t ∈ S }), is_CS L' ∧ (Language.map fun (t : { t : T // t ∈ S }) => ↑t) L' = grammar_language g

A context-sensitive grammar language is the image of a context-sensitive language over the finite subtype of terminals appearing in the grammar.

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

Every context-sensitive language is the image of a language over a finite subtype of its terminal alphabet.

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

Every context-sensitive language is equivalent to a context-sensitive language over a finite terminal subtype.

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

Every context-sensitive language is equivalent to a context-sensitive 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_CS_of_finiteAlphabet_CS_image {T : Type} {S : Finset T} {L' : Language { t : T // t ∈ S }} (hL' : is_CS L') : is_CS ((Language.map fun (t : { t : T // t ∈ S }) => ↑t) L')

The inclusion image of a context-sensitive language over a finite subtype is context-sensitive over the ambient alphabet.

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

A language is context-sensitive iff it is the inclusion image of a context-sensitive language over a finite terminal subtype.

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

A language is context-sensitive iff it is the image of a context-sensitive language over some finite terminal alphabet.

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

Every context-sensitive language has finite terminal support.