Encodings of context-free grammars
TheoremRenaming the nonterminals of a symbol twice#✓fully proved
For maps \(f : N_1 \to N_2\) and \(b : N_2 \to N_3\) and a grammar symbol \(s\) with terminals in \(T\) and nonterminals in \(N_1\), renaming the nonterminals of \(s\) by \(f\) and then by \(b\) gives the same symbol as renaming them by \(b \circ f\).
@[simp]
theorem mapSymbol_mapSymbol {N₁ N₂ N₃ : Type*} (f : N₁ → N₂) (b : N₂ → N₃) (s : Symbol T N₁) :
mapSymbol b (mapSymbol f s) = mapSymbol (b ∘ f) sdef mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 1
TheoremGrammars with renamings in both directions generate the same language#✓fully proved
Let \(g\) and \(G\) be context-free grammars over the same terminals. Suppose there are maps \(f\) from the nonterminals of \(g\) to those of \(G\) and \(b\) from the nonterminals of \(G\) to those of \(g\) such that renaming the nonterminals of any production of \(g\) by \(f\) gives a production of \(G\), renaming the nonterminals of any production of \(G\) by \(b\) gives a production of \(g\), \(f\) sends the start nonterminal of \(g\) to that of \(G\), and \(b\) sends the start nonterminal of \(G\) to that of \(g\). Then \(g\) and \(G\) generate the same language. The renamings need not be inverse to each other.
theorem language_eq_of_maps {g G : ContextFreeGrammar T} (f : g.NT → G.NT) (b : G.NT → g.NT)
(hf : ∀ r ∈ g.rules, mapRule f r ∈ G.rules) (hb : ∀ r ∈ G.rules, mapRule b r ∈ g.rules)
(hfi : f g.initial = G.initial) (hbi : b G.initial = g.initial) :
G.language = g.languagedef 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
Uses 4 · Used by 1
StructureEncoded context-free grammars#✓fully proved
An encoded context-free grammar over a terminal type \(T\) consists of a start nonterminal, which is a natural number, and a list of productions. Each production is a pair of a left-hand side, a natural number, and a right-hand side, a list of elements of the disjoint union \(\mathbb{N} \sqcup T\), in which a number \(i\) from the left summand stands for nonterminal \(i\) and an element \(a\) of \(T\) for terminal \(a\).
Unlike a general context-free grammar, whose type of nonterminals is part of its data, an encoded grammar is a concrete object that computable functions can take and return.
structure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))Used by 127
DefinitionDecoding a grammar symbol#✓fully proved
Decoding sends an element of the disjoint union \(\mathbb{N} \sqcup T\) to a grammar symbol with terminals \(T\) and nonterminals \(\mathbb{N}\): a natural number \(i\) from the left summand goes to the nonterminal \(i\), and an element \(a\) of \(T\) from the right summand goes to the terminal \(a\).
def decodeSymbol : ℕ ⊕ T → Symbol T ℕ
| .inl i => .nonterminal i
| .inr a => .terminal aUsed by 39
DefinitionEncoding a grammar symbol#✓fully proved
Encoding sends a grammar symbol with terminals \(T\) and nonterminals \(\mathbb{N}\) to an element of the disjoint union \(\mathbb{N} \sqcup T\): the terminal \(a\) goes to \(a\) in the right summand \(T\), and the nonterminal \(i\) goes to \(i\) in the left summand \(\mathbb{N}\).
def encodeSymbol : Symbol T ℕ → ℕ ⊕ T
| .terminal a => .inr a
| .nonterminal i => .inl iDefinitionDecoding a production#✓fully proved
Decoding a pair \((A, s)\) of a natural number \(A\) and a list \(s\) of elements of the disjoint union \(\mathbb{N} \sqcup T\) gives the production, with terminals \(T\) and nonterminals \(\mathbb{N}\), whose left-hand side is the nonterminal \(A\) and whose right-hand side is \(s\) with each entry decoded as a symbol: a number \(i\) from the left summand becomes the nonterminal \(i\) and an element \(a\) of \(T\) becomes the terminal \(a\).
def decodeRule (e : ℕ × List (ℕ ⊕ T)) : ContextFreeRule T ℕ :=
⟨e.1, e.2.map decodeSymbol⟩def decodeSymbol : ℕ ⊕ T → Symbol T ℕ
| .inl i => .nonterminal i
| .inr a => .terminal aCSLibExt/Computability/Languages/ContextFree/Encoded.lean:83
Uses 1 · Used by 43
DefinitionEncoding a production#✓fully proved
Encoding a production with terminals \(T\) and nonterminals \(\mathbb{N}\) gives the pair \((A, s)\) where \(A \in \mathbb{N}\) is its left-hand side and \(s\) is its right-hand side with each symbol encoded as an element of the disjoint union \(\mathbb{N} \sqcup T\): the terminal \(a\) becomes \(a\) in the right summand and the nonterminal \(i\) becomes \(i\) in the left summand.
def encodeRule (r : ContextFreeRule T ℕ) : ℕ × List (ℕ ⊕ T) :=
(r.input, r.output.map encodeSymbol)def encodeSymbol : Symbol T ℕ → ℕ ⊕ T
| .terminal a => .inr a
| .nonterminal i => .inl iCSLibExt/Computability/Languages/ContextFree/Encoded.lean:88
Uses 1 · Used by 3
Semantics
AbbreviationGrammar denoted by an encoding#✓fully proved
For an encoded context-free grammar \(g\) over \(T\), the context-free grammar over \(T\) whose nonterminals are the natural numbers, whose initial nonterminal is the start nonterminal of \(g\), and whose productions are the decodings of the encoded productions of \(g\): an encoded production \((i, u)\) becomes the production rewriting the nonterminal \(i\) to the word obtained from \(u\) by reading each entry \(\mathrm{inl}\, j\) as the nonterminal \(j\) and each entry \(\mathrm{inr}\, a\) as the terminal \(a\).
abbrev toCFG (g : EncodedCFG T) : ContextFreeGrammar T where
NT := ℕ
initial := g.start
rules := (g.rules.map decodeRule).toFinsetstructure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
def decodeRule (e : ℕ × List (ℕ ⊕ T)) : ContextFreeRule T ℕ :=
⟨e.1, e.2.map decodeSymbol⟩CSLibExt/Computability/Languages/ContextFree/Encoded.lean:101
Uses 2 · Used by 59
DefinitionLanguage of an encoded grammar#✓fully proved
The language of an encoded context-free grammar \(g\) over \(T\) is the language generated by the context-free grammar that \(g\) denotes, whose nonterminals are the natural numbers, whose initial nonterminal is the start nonterminal of \(g\) and whose productions are the decoded productions of \(g\).
def language (g : EncodedCFG T) : Language T :=
g.toCFG.languagestructure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
Uses 2 · Used by 57
TheoremEncoded grammars generate context-free languages#✓fully proved
The language of an encoded grammar is context-free.
theorem language_isContextFree (g : EncodedCFG T) : g.language.IsContextFreestructure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
Uses 3 · Used by 1
Numbering
DefinitionNonterminal of a symbol#✓fully proved
The partial map from grammar symbols with terminals in \(T\) and nonterminals in \(N\) to \(N\) that sends a nonterminal \(A\) to \(A\) and has no value on terminals.
DefinitionList of nonterminals mentioned by a grammar#✓fully proved
For a context-free grammar \(G\), the list consisting of the initial nonterminal of \(G\) followed, for each production of \(G\) in turn (in some fixed order of its finite set of productions), by the left-hand side of the production and then the nonterminals of its right-hand side in order. Nonterminals may occur more than once.
noncomputable def usedNT (G : ContextFreeGrammar T) : List G.NT :=
G.initial :: G.rules.toList.flatMap fun r => r.input :: r.output.filterMap ntOfdef ntOf {N : Type*} : Symbol T N → Option N
| .terminal _ => none
| .nonterminal A => some ACSLibExt/Computability/Languages/ContextFree/Encoded.lean:151
Uses 1 · Used by 4
DefinitionNumbering of nonterminals#✓fully proved
For a context-free grammar \(G\), the number of a nonterminal \(A\) of \(G\) is the position, counting from \(0\), of the first occurrence of \(A\) in the list of nonterminals that \(G\) mentions (its initial nonterminal first); if \(A\) does not occur in that list, its number is the length of the list.
noncomputable def ntIndex (G : ContextFreeGrammar T) (A : G.NT) : ℕ :=
(usedNT G).idxOf Anoncomputable def usedNT (G : ContextFreeGrammar T) : List G.NT :=
G.initial :: G.rules.toList.flatMap fun r => r.input :: r.output.filterMap ntOfCSLibExt/Computability/Languages/ContextFree/Encoded.lean:156
DefinitionNonterminal with a given number#✓fully proved
For a context-free grammar \(G\) and a natural number \(n\), the nonterminal of \(G\) with number \(n\) is the entry at position \(n\), counting from \(0\), of the list of nonterminals that \(G\) mentions (its initial nonterminal first); if the list has no entry at position \(n\), it is the initial nonterminal of \(G\).
noncomputable def ntOfIndex (G : ContextFreeGrammar T) (n : ℕ) : G.NT :=
(usedNT G).getD n G.initialnoncomputable def usedNT (G : ContextFreeGrammar T) : List G.NT :=
G.initial :: G.rules.toList.flatMap fun r => r.input :: r.output.filterMap ntOfCSLibExt/Computability/Languages/ContextFree/Encoded.lean:156
Uses 1 · Used by 2
TheoremNumbering the nonterminals of a production and back recovers it#✓fully proved
Let \(G\) be a context-free grammar over \(T\) and \(r\) a production of \(G\). Replacing each nonterminal \(A\) of \(r\) by its number, the position, counting from \(0\), of the first occurrence of \(A\) in the list of nonterminals that \(G\) mentions, and then replacing each number \(n\) by the nonterminal of \(G\) with number \(n\) (the entry at position \(n\) of that list, or the initial nonterminal of \(G\) if the list has no such entry) gives \(r\) again.
theorem mapRule_ntOfIndex_ntIndex {G : ContextFreeGrammar T} {r : ContextFreeRule T G.NT}
(hr : r ∈ G.rules) : mapRule (ntOfIndex G) (mapRule (ntIndex G) r) = 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
noncomputable def ntOfIndex (G : ContextFreeGrammar T) (n : ℕ) : G.NT :=
(usedNT G).getD n G.initialCSLibExt/Computability/Languages/ContextFree/Encoded.lean:177
noncomputable def ntIndex (G : ContextFreeGrammar T) (A : G.NT) : ℕ :=
(usedNT G).idxOf ACSLibExt/Computability/Languages/ContextFree/Encoded.lean:173
Uses 6 · Used by 1
Encoding
DefinitionEncoding of a context-free grammar#✓fully proved
For a context-free grammar \(G\) over \(T\), the encoded grammar whose start nonterminal is the number of the initial nonterminal of \(G\) and whose productions are the productions of \(G\), listed in some fixed order, with every nonterminal \(A\) replaced by its number, the position, counting from \(0\), of the first occurrence of \(A\) in the list of nonterminals that \(G\) mentions (its initial nonterminal first).
noncomputable def ofCFG (G : ContextFreeGrammar T) : EncodedCFG T :=
⟨ntIndex G G.initial, G.rules.toList.map fun r => encodeRule (mapRule (ntIndex G) r)⟩structure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
noncomputable def ntIndex (G : ContextFreeGrammar T) (A : G.NT) : ℕ :=
(usedNT G).idxOf ACSLibExt/Computability/Languages/ContextFree/Encoded.lean:173
def encodeRule (r : ContextFreeRule T ℕ) : ℕ × List (ℕ ⊕ T) :=
(r.input, r.output.map encodeSymbol)CSLibExt/Computability/Languages/ContextFree/Encoded.lean:105
def 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
TheoremThe encoding of a grammar generates the same language#✓fully proved
The encoding of a grammar generates the same language.
theorem language_ofCFG (G : ContextFreeGrammar T) : (ofCFG G).language = G.languagenoncomputable def ofCFG (G : ContextFreeGrammar T) : EncodedCFG T :=
⟨ntIndex G G.initial, G.rules.toList.map fun r => encodeRule (mapRule (ntIndex G) r)⟩CSLibExt/Computability/Languages/ContextFree/Encoded.lean:211
Uses 15 · Used by 1
TheoremA language is context-free exactly when an encoded grammar generates it#✓fully proved
A language is context-free exactly when an encoded grammar generates it.
theorem isContextFree_iff {L : Language T} :
L.IsContextFree ↔ ∃ g : EncodedCFG T, g.language = Lstructure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
Uses 5 · Used by 1
Encoding as pairs
DefinitionEncoded grammars as pairs#✓fully proved
Sending an encoded grammar over \(T\) to the pair of its start nonterminal and its list of productions is a bijection from encoded grammars over \(T\) onto pairs \((s, R)\) of a natural number \(s\) and a list \(R\) of pairs of a natural number and a list of elements of the disjoint union \(\mathbb{N} \sqcup T\).
def equivProd : EncodedCFG T ≃ ℕ × List (ℕ × List (ℕ ⊕ T)) where
toFun g := (g.start, g.rules)
invFun p := ⟨p.1, p.2⟩
left_inv _ := rfl
right_inv _ := rflstructure EncodedCFG (T : Type*) where
/-- The start nonterminal. -/
start : ℕ
/-- The productions. -/
rules : List (ℕ × List (ℕ ⊕ T))CSLibExt/Computability/Languages/ContextFree/Encoded.lean:74
Uses 1 · Used by 32
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.