Closure properties of context-free languages
TheoremClosure of context-free languages under union#✓fully proved
If \(L\) and \(M\) are context-free languages over the same alphabet, then their union \(L \cup M\) is context-free.
theorem IsContextFree.add {L M : Language T} (hL : L.IsContextFree) (hM : M.IsContextFree) :
(L + M).IsContextFreeUses 11 · Used by 3
TheoremClosure of context-free languages under concatenation#✓fully proved
If \(L\) and \(M\) are context-free languages over the same alphabet, then their concatenation \(LM = \{uv : u \in L,\ v \in M\}\) is context-free.
theorem IsContextFree.mul {L M : Language T} (hL : L.IsContextFree) (hM : M.IsContextFree) :
(L * M).IsContextFreeUses 12 · Used by 4
TheoremClosure of context-free languages under Kleene star#✓fully proved
If \(L\) is a context-free language, then its Kleene star \(L^*\) is context-free.
theorem IsContextFree.kstar {L : Language T} (hL : L.IsContextFree) :
(L∗).IsContextFreeUses 12 · Used by 3
TheoremPowers of a context-free language are context-free#✓fully proved
If \(L\) is a context-free language, then for every natural number \(n\) the power \(L^n\), the concatenation of \(n\) copies of \(L\) (with \(L^0\) the language containing only the empty word), is context-free.
theorem IsContextFree.pow {L : Language T} (hL : L.IsContextFree) :
∀ n : ℕ, (L ^ n).IsContextFreeTheoremFinite languages are context-free#✓fully proved
Every finite language is context-free.
theorem IsContextFree.of_finite {L : Language T} (h : Set.Finite L) : L.IsContextFreeUses 3 · Used by 1
TheoremLanguages of bounded word length are context-free#✓fully proved
Over a finite alphabet, if \(n\) is a natural number and every word of a language \(L\) has length at most \(n\), then \(L\) is context-free.
theorem IsContextFree.of_length_le [Finite T] {L : Language T} (n : ℕ)
(h : ∀ w ∈ L, w.length ≤ n) : L.IsContextFreeUses 1
TheoremContext-free languages are closed under homomorphic images#✓fully proved
Let \(T\) and \(T'\) be alphabets, \(L\) a context-free language over \(T\), and \(\varphi\) a map sending each letter of \(T\) to a word over \(T'\). Then the language of all words \(\varphi(a_1) \cdots \varphi(a_n)\) with \(a_1 \cdots a_n \in L\) is context-free.
A grammar for it replaces every terminal \(a\) in every production by the word \(\varphi(a)\).
theorem IsContextFree.homImage {L : Language T} (hL : L.IsContextFree)
(φ : T → List T') :
Language.IsContextFree ((fun w => (w.map φ).flatten) '' L)Uses 8 · Used by 3
TheoremIntersection of a context-free language with the language of a DFA#✓fully proved
If \(L\) is a context-free language over an alphabet \(T\) and \(M\) is a deterministic finite automaton over \(T\) with finitely many states, then the intersection of \(L\) with the language accepted by \(M\) is context-free.
theorem IsContextFree.inf_dfa_accepts [Finite σ] {L : Language T}
(hL : L.IsContextFree) (M : DFA T σ) :
(L ⊓ M.accepts).IsContextFreeTheoremIntersection of a context-free language with a regular language#✓fully proved
If \(L\) is a context-free language and \(R\) a regular language over the same alphabet, then \(L \cap R\) is context-free.
No finite-alphabet assumption is needed: the grammar built in the proof only mentions terminals that occur in the productions of the original grammar.
theorem IsContextFree.inf_isRegular {L R : Language T} (hL : L.IsContextFree)
(hR : R.IsRegular) :
(L ⊓ R).IsContextFreeUses 1 · Used by 3
TheoremContext-free languages are closed under letter maps#✓fully proved
Let \(L\) be a context-free language over an alphabet \(T\) and let \(f \colon T \to T'\) be a map of alphabets. Then the image of \(L\) under \(f\), the language \(\{f(a_1) \cdots f(a_n) \mid a_1 \cdots a_n \in L\}\) over \(T'\), is context-free.
theorem IsContextFree.map {L : Language T} (hL : L.IsContextFree) (f : T → T') :
(Language.map f L).IsContextFreeDefinitionLetter numbering for the substitution grammar#✓fully proved
For a context-free grammar \(g\) and a letter \(a\), the number of \(a\) is the position (counted from \(0\)) of the first occurrence of \(a\) in the list of terminals occurring in the productions of \(g\), or the length of that list when \(a\) does not occur in it.
def code (a : T) : ℕ :=
(grammarTerminals g).idxOf anoncomputable def grammarTerminals (g : ContextFreeGrammar T) : List T :=
g.rules.toList.flatMap fun r => r.output.filterMap fun s =>
match s with
| .terminal a => some a
| .nonterminal _ => noneCSLibExt/Computability/Languages/ContextFree/ChomskyNormalForm.lean:66
Uses 1 · Used by 3
DefinitionLetter decoding for the substitution grammar#✓fully proved
For a context-free grammar \(g\) and a natural number \(k\), the letter with number \(k\) is the entry at position \(k\) (counted from \(0\)) of the list of terminals occurring in the productions of \(g\); there is no such letter when \(k\) is at least the length of that list.
def decode (k : ℕ) : Option T :=
(grammarTerminals g)[k]?noncomputable def grammarTerminals (g : ContextFreeGrammar T) : List T :=
g.rules.toList.flatMap fun r => r.output.filterMap fun s =>
match s with
| .terminal a => some a
| .nonterminal _ => noneCSLibExt/Computability/Languages/ContextFree/ChomskyNormalForm.lean:66
Uses 1 · Used by 2
DefinitionSubstituting the symbols of a grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\) with nonterminals \(N_g\), and let \(e\) assign to each letter \(a \in T\) an encoded grammar \(e(a)\) over \(T'\). Each symbol of \(g\) becomes a nonterminal in \(N_g \sqcup (\mathbb{N} \times \mathbb{N})\): a nonterminal \(B\) of \(g\) becomes \(B\) in the left part, and a terminal \(a\) becomes the pair \((k, n)\), where \(k\) is the number of \(a\) (the position, counted from \(0\), of the first occurrence of \(a\) in the list of terminals occurring in the productions of \(g\), or the length of that list when \(a\) does not occur in it) and \(n\) is the start nonterminal of \(e(a)\).
DefinitionMain production of the substitution grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\) with nonterminals \(N_g\), and let \(e\) assign to each letter \(a \in T\) an encoded grammar \(e(a)\) over \(T'\). A production \(A \to \alpha\) over \(T\) with nonterminals in \(N_g\) gives the production \(A \to \alpha'\) over \(T'\) with nonterminals in \(N_g \sqcup (\mathbb{N} \times \mathbb{N})\), where \(A\) is taken in the left part and \(\alpha'\) is obtained from \(\alpha\) by replacing each nonterminal \(B\) by \(B\) in the left part and each terminal \(a\) by the nonterminal \((k, n)\); here \(k\) is the number of \(a\) (the position, counted from \(0\), of the first occurrence of \(a\) in the list of terminals occurring in the productions of \(g\), or the length of that list when \(a\) does not occur in it) and \(n\) is the start nonterminal of \(e(a)\).
def mainRule (r : ContextFreeRule T g.NT) : ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ)) :=
⟨.inl r.input, r.output.map (substSymbol g e)⟩def substSymbol : Symbol T g.NT → Symbol T' (g.NT ⊕ (ℕ × ℕ))
| .terminal a => .nonterminal (.inr (code g a, (e a).start))
| .nonterminal B => .nonterminal (.inl B)CSLibExt/Computability/Languages/ContextFree/Substitution.lean:67
Uses 2 · Used by 2
DefinitionLetter productions of the substitution grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\) with nonterminals \(N_g\), let \(a \in T\) have number \(k\) (the position, counted from \(0\), of the first occurrence of \(a\) in the list of terminals occurring in the productions of \(g\), or the length of that list when \(a\) does not occur in it), and let \(n \to w\) be a production over \(T'\) whose nonterminals are natural numbers. It gives the production \((k, n) \to w'\) with nonterminals in \(N_g \sqcup (\mathbb{N} \times \mathbb{N})\), where \(w'\) keeps the terminals of \(w\) and replaces each nonterminal \(m\) by \((k, m)\).
def subRule (a : T) (r : ContextFreeRule T' ℕ) : ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ)) :=
mapRule (fun n => .inr (code g a, n)) rdef mapRule {N' : Type*} (f : N → N') (r : ContextFreeRule T N) :
ContextFreeRule T N' :=
⟨f r.input, r.output.map (mapSymbol f)⟩CSLibExt/Computability/Languages/ContextFree/Basic.lean:174
def code (a : T) : ℕ :=
(grammarTerminals g).idxOf aCSLibExt/Computability/Languages/ContextFree/Substitution.lean:56
DefinitionProductions of the substitution grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\), and let \(e\) assign to each letter \(a \in T\) an encoded grammar \(e(a)\) over \(T'\). The productions of the substitution grammar are the main productions obtained from the productions of \(g\), together with, for each terminal \(a\) occurring in a production of \(g\), the letter productions for \(a\) obtained from the productions of \(e(a)\).
def rules : Finset (ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ))) :=
g.rules.image (mainRule g e) ∪
(grammarTerminals g).toFinset.biUnion fun a => (e a).toCFG.rules.image (subRule g a)def mainRule (r : ContextFreeRule T g.NT) : ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ)) :=
⟨.inl r.input, r.output.map (substSymbol g e)⟩CSLibExt/Computability/Languages/ContextFree/Substitution.lean:72
noncomputable def grammarTerminals (g : ContextFreeGrammar T) : List T :=
g.rules.toList.flatMap fun r => r.output.filterMap fun s =>
match s with
| .terminal a => some a
| .nonterminal _ => noneCSLibExt/Computability/Languages/ContextFree/ChomskyNormalForm.lean:66
def subRule (a : T) (r : ContextFreeRule T' ℕ) : ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ)) :=
mapRule (fun n => .inr (code g a, n)) rCSLibExt/Computability/Languages/ContextFree/Substitution.lean:76
Uses 5 · Used by 2
AbbreviationThe substitution grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\) with nonterminals \(N_g\) and start symbol \(S\), and let \(e\) assign to each letter \(a \in T\) an encoded grammar \(e(a)\) over \(T'\). The substitution grammar is the context-free grammar over \(T'\) with nonterminals \(N_g \sqcup (\mathbb{N} \times \mathbb{N})\), start symbol \(S\) taken in the left part, and the productions of the substitution grammar for \(g\) and \(e\).
abbrev grammar : ContextFreeGrammar T' where
NT := g.NT ⊕ (ℕ × ℕ)
initial := .inl g.initial
rules := rules g edef rules : Finset (ContextFreeRule T' (g.NT ⊕ (ℕ × ℕ))) :=
g.rules.image (mainRule g e) ∪
(grammarTerminals g).toFinset.biUnion fun a => (e a).toCFG.rules.image (subRule g a)CSLibExt/Computability/Languages/ContextFree/Substitution.lean:80
Uses 2 · Used by 1
DefinitionIntended languages of the substitution grammar#✓fully proved
Let \(g\) be a context-free grammar over \(T\) with nonterminals \(N_g\), let \(e\) assign to each letter \(a \in T\) an encoded grammar \(e(a)\) over \(T'\), and let \(s\) assign to each letter \(a \in T\) a language \(s(a)\) over \(T'\). Each element of \(N_g \sqcup (\mathbb{N} \times \mathbb{N})\), the nonterminals of the substitution grammar, is assigned a language over \(T'\). A nonterminal \(B \in N_g\) is assigned the substitution of \(s\) into the language generated by \(g\) from \(B\). A pair \((k, n)\) is assigned, when \(k\) is less than the length of the list of terminals occurring in the productions of \(g\) and \(a\) is the entry at position \(k\) of that list (counted from \(0\)), the language generated from the nonterminal \(n\) by the grammar that \(e(a)\) denotes, and the empty language otherwise.
def val : g.NT ⊕ (ℕ × ℕ) → Language T'
| .inl B => substitution (languageFrom g B) s
| .inr (k, n) =>
match decode g k with
| some a => languageFrom (e a).toCFG n
| none => 0def substitution (L : Language T) (s : T → Language T') : Language T' :=
{y | ∃ x ∈ L, y ∈ (x.map s).prod}CSLibExt/Computability/Languages/Substitution.lean:33
def languageFrom (g : ContextFreeGrammar T) (A : g.NT) : Language T :=
{ w : List T | g.Derives [Symbol.nonterminal A] (w.map Symbol.terminal) }CSLibExt/Computability/Languages/ContextFree/Basic.lean:219
def decode (k : ℕ) : Option T :=
(grammarTerminals g)[k]?CSLibExt/Computability/Languages/ContextFree/Substitution.lean:60
Uses 5 · Used by 1
TheoremDerivations keep the terminals among those of the grammar#✓fully proved
Let \(g\) be a context-free grammar and let the sentential form \(u\) derive \(v\) in \(g\) in zero or more steps. If every terminal occurring in \(u\) occurs in some production of \(g\), then every terminal occurring in \(v\) occurs in some production of \(g\).
theorem mem_grammarTerminals_of_derives {u v : List (Symbol T g.NT)} (h : g.Derives u v)
(hu : ∀ a, Symbol.terminal a ∈ u → a ∈ grammarTerminals g) :
∀ a, Symbol.terminal a ∈ v → a ∈ grammarTerminals gnoncomputable def grammarTerminals (g : ContextFreeGrammar T) : List T :=
g.rules.toList.flatMap fun r => r.output.filterMap fun s =>
match s with
| .terminal a => some a
| .nonterminal _ => noneCSLibExt/Computability/Languages/ContextFree/ChomskyNormalForm.lean:66
Uses 1 · Used by 1
TheoremContext-free languages are closed under substitution by context-free languages#✓fully proved
Context-free languages are closed under substitution by context-free languages.
theorem IsContextFree.substitution {L : Language T} (hL : L.IsContextFree)
{s : T → Language T'} (hs : ∀ a, (s a).IsContextFree) :
(Cslib.Language.substitution L s).IsContextFreedef substitution (L : Language T) (s : T → Language T') : Language T' :=
{y | ∃ x ∈ L, y ∈ (x.map s).prod}CSLibExt/Computability/Languages/Substitution.lean:33
Uses 28
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.