Revision #2733 → #3272 · back to history
modifiedContext-free grammar28d3e7801ece
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar is a structure with nonterminal type, initial symbol, and rules each rewriting a single nonterminal, matching the CFG definition. | ContextFreeGrammar bundles a nonterminal type, initial symbol, and finite rule set, each rewriting a single nonterminal. |
modifiedFormal grammar287f76bbe6cc
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib only defines context-free grammars, not a general formal-grammar (arbitrary production system) structure. | Mathlib defines context-free grammars but no general formal-grammar (arbitrary Type-0 production system) structure. |
modifiedLanguage generated by a grammar52f2520b617c
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar.language is the set of terminal words derivable from the initial nonterminal. | ContextFreeGrammar.language is the set of terminal words w with g.Generates (w.map Symbol.terminal). |
modifiedContext-free languagecc152e598c76
| Field | From #2733 | To #3272 |
|---|
| note | Language.IsContextFree L holds iff some context-free grammar generates L. | Language.IsContextFree L asserts the existence of a ContextFreeGrammar g with g.language = L. |
modifiedLanguage equality undecidable0e1c84ef9209
| Field | From #2733 | To #3272 |
|---|
| note | No undecidability result about CFG language equivalence exists in Mathlib. | No undecidability result about equivalence of CFGs exists in Mathlib. |
modifiedCFG as 4-tuple1bebec028483
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar bundles terminals (type T), nonterminals (NT), rules, and the initial symbol, capturing the (V,Σ,R,S) tuple. | ContextFreeGrammar bundles terminals (T), nonterminals (NT), rules, and the initial symbol, capturing the (V,Σ,R,S) tuple. |
modifiedNonterminal / variablede2b01cb52d9
| Field | From #2733 | To #3272 |
|---|
| note | Symbol.nonterminal injects the nonterminal type into the grammar's symbol alphabet. | The Symbol.nonterminal constructor injects the nonterminal type into the grammar's symbol alphabet. |
modifiedTerminalsdf174e215d3b
| Field | From #2733 | To #3272 |
|---|
| note | Symbol.terminal injects terminals, kept disjoint from nonterminals by the inductive Symbol type. | Symbol.terminal injects terminals, kept disjoint from nonterminals by the two-constructor inductive Symbol type. |
modifiedProduction rulesdfbb12d6f9a5
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeRule represents a production with an input nonterminal and an output string, collected in g.rules. | ContextFreeRule packages an input nonterminal and an output string of symbols, collected in g.rules. |
modifiedStart variable1f3d497724b4
| Field | From #2733 | To #3272 |
|---|
| note | The initial field of ContextFreeGrammar is the start nonterminal. | The initial field of a ContextFreeGrammar is the start nonterminal used by Generates. |
modifiedProduction rule as pairb4b8f0628534
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeRule is exactly a pair of an input nonterminal and an output string of symbols. | ContextFreeRule is an input/output pair of a nonterminal and a list of symbols. |
modifiedε-production9c45aa67dde2
| Field | From #2733 | To #3272 |
|---|
| note | An ε-production is expressible as a ContextFreeRule with empty output, but Mathlib has no named ε-production concept. | An ε-production is a ContextFreeRule with empty output but Mathlib has no named ε-production predicate. |
modifiedAlternatives4ef8af31e9d9
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib has no notion of bundled alternatives; each alternative is just a separate rule. | Mathlib has no bundled rule-alternatives notion; each alternative is a separate ContextFreeRule. |
modifiedDirectly yieldsac42bd1ca268
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar.Produces u v is the one-step derivation relation via some rule of the grammar. | ContextFreeGrammar.Produces u v holds iff some rule of g rewrites u to v in one step. |
modifiedRule rewriting relation046dedafb2da
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeRule.Rewrites r u v holds when the single rule r sends the string u to v by rewriting one occurrence of r.input. | ContextFreeRule.Rewrites r u v is the inductive relation saying a single rule r sends string u to string v. |
modifiedYields / derived0976406a598d
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar.Derives is the reflexive-transitive closure of Produces, i.e. the multi-step derivation relation. | ContextFreeGrammar.Derives is Relation.ReflTransGen g.Produces, i.e. multi-step derivation. |
modifiedLanguage of a grammar00f00ccf5fbf
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar.language is exactly the set of terminal words derivable from the initial symbol. | ContextFreeGrammar.language is exactly the set of terminal words derivable from the initial nonterminal. |
modifiedContext-free language (CFL)fdf4299b0733
| Field | From #2733 | To #3272 |
|---|
| note | Language.IsContextFree L is defined as the existence of a CFG whose language equals L. | Language.IsContextFree L is defined as ∃ g : ContextFreeGrammar T, g.language = L. |
modifiedPushdown automata recognize CFLs2d0a48b991fe
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib has no pushdown automaton definition and hence no equivalence with context-free languages. | Mathlib has no pushdown automaton definition or equivalence with CFLs. |
modifiedWords with reverse grammar891ff5899a5b
| Field | From #2733 | To #3272 |
|---|
| note | This specific grammar/language example is not present in Mathlib. | This specific ww^R grammar example is not present in Mathlib. |
modifiedWell-formed parentheses5a0e816e18eb
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib's DyckWord formalizes the balanced-parenthesis language directly, but not via a context-free grammar. | Mathlib's DyckWord captures the balanced-parenthesis language directly, but not as a ContextFreeGrammar example. |
modifiedNested parentheses and bracketsbd8493a06e6d
| Field | From #2733 | To #3272 |
|---|
| note | No two-type nested-bracket grammar example exists in Mathlib. | No two-kind nested-bracket grammar example exists in Mathlib. |
modifiedMatching pairs a^n b^n (n≥1)f469c6c11961
| Field | From #2733 | To #3272 |
|---|
| note | The a^n b^n grammar example is not formalized in Mathlib. | The a^n b^n (n≥1) grammar example is not formalized in Mathlib. |
modifiedFirst-order logic formulas7c6e1a7c7447
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib defines first-order formulas (ModelTheory) inductively but not as a context-free grammar instance. | Mathlib defines first-order formulas inductively (ModelTheory) but not as an instance of a context-free grammar. |
addeda^n b^n c^n not context-freedd3c34b3f08e
modifiedRegular grammar to NFA315a52bf16d7
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib has NFA but no regular-grammar definition or correspondence to it. | Mathlib has NFA but no regular-grammar definition or correspondence. |
modifiedDerivationda853296eb5a
| Field | From #2733 | To #3272 |
|---|
| note | ContextFreeGrammar.Derives (reflexive-transitive closure of Produces) captures derivation as a sequence of rule applications. | ContextFreeGrammar.Derives (ReflTransGen of Produces) captures a derivation as a sequence of rule applications. |
modifiedLeftmost / rightmost derivation7f43809e81f0
| Field | From #2733 | To #3272 |
|---|
| note | Mathlib's derivation relation does not distinguish leftmost/rightmost rewriting. | Mathlib's derivation relation does not distinguish leftmost vs rightmost rewriting. |
modifiedEmptiness decidable for CFGs453b9e8dd98a
| Field | From #2733 | To #3272 |
|---|
| note | The decidability of CFG emptiness (vs. context-sensitive) is not formalized in Mathlib. | The decidability of CFG emptiness (vs context-sensitive) is not formalized in Mathlib. |