Non-closure of context-free languages

TheoremThe Kleene star of a one-letter word#✓fully proved

For a letter \(a\) of an alphabet, a word \(w\) belongs to the Kleene star of the language \(\{a\}\) whose only word is the one-letter word \(a\) if and only if \(w = a^k\) for some \(k \in \mathbb{N}\).

theorem mem_kstar_singleton {α : Type*} {a : α} {w : List α} :
    w ∈ KStar.kstar ({[a]} : Language α) ↔
      ∃ k, w = List.replicate k a

Used by 3

Used byContext-free languages are not closed under complement · Context-free languages are not closed under intersection · Inherently ambiguous example as a union of two languages

DefinitionThe language \(a^n b^n\)#✓fully proved

For letters \(a\) and \(b\) of an alphabet, this is the language of the words \(a^n b^n\) for \(n \in \mathbb{N}\): \(n\) copies of \(a\) followed by \(n\) copies of \(b\).

def eqPowLang {α : Type*} (a b : α) : Language α :=
  {w | ∃ n, w = List.replicate n a ++ List.replicate n b}

Used by 6

Used byThe grammar \(S \to aSb \mid \varepsilon\) generates \(a^n b^n\) · The language \(a^n b^n\) is context-free · Context-free languages are not closed under complement · Context-free languages are not closed under intersection · Inherently ambiguous example as a union of two languages · The example language is context-free

DefinitionThe grammar \(S \to aSb \mid \varepsilon\)#✓fully proved

For letters \(a\) and \(b\) of an alphabet with decidable equality, this is the context-free grammar with a single nonterminal \(S\), which is its start symbol, and the two rules \(S \to aSb\) and \(S \to \varepsilon\).

def eqPowGrammar {α : Type*} [DecidableEq α] (a b : α) :
    ContextFreeGrammar α where
  NT := Unit
  initial := ()
  rules := {⟨(), [Symbol.terminal a, Symbol.nonterminal (),
      Symbol.terminal b]⟩, ⟨(), []⟩}

Used by 2

Used byThe grammar \(S \to aSb \mid \varepsilon\) generates \(a^n b^n\) · The language \(a^n b^n\) is context-free

TheoremThe grammar \(S \to aSb \mid \varepsilon\) generates \(a^n b^n\)#✓fully proved

For letters \(a\) and \(b\) of an alphabet with decidable equality, the language of the context-free grammar with a single nonterminal \(S\), its start symbol, and the two rules \(S \to aSb\) and \(S \to \varepsilon\) is the language of the words \(a^n b^n\) for \(n \in \mathbb{N}\).

theorem eqPowGrammar_language {α : Type*} [DecidableEq α] (a b : α) :
    (eqPowGrammar a b).language = eqPowLang a b

Uses 9 · Used by 1

Statement usesThe grammar \(S \to aSb \mid \varepsilon\) · The language \(a^n b^n\)

Proof usesYield of a sentential form · Concatenation of yields · Interpretation of a sentential form · Interpretation of a grammar symbol · Valuations bound the language of a grammar · Language membership through yields · Yield through one production

Used byThe language \(a^n b^n\) is context-free

TheoremThe language \(a^n b^n\) is context-free#✓fully proved

For any alphabet and any letters \(a\) and \(b\) of it, the language of the words \(a^n b^n\) for \(n \in \mathbb{N}\) is context-free.

theorem eqPowLang_isContextFree {α : Type*} (a b : α) :
    (eqPowLang a b).IsContextFree

Uses 3 · Used by 3

Statement usesThe language \(a^n b^n\)

Proof usesThe grammar \(S \to aSb \mid \varepsilon\) · The grammar \(S \to aSb \mid \varepsilon\) generates \(a^n b^n\)

Used byContext-free languages are not closed under complement · Context-free languages are not closed under intersection · The example language is context-free

DefinitionThe language \(a^n b^n c^n\)#✓fully proved

Over the three-letter alphabet \(\{a, b, c\}\) (the letters \(0, 1, 2\)), this is the language of the words \(a^n b^n c^n\) for \(n \in \mathbb{N}\): \(n\) copies of \(a\), then \(n\) copies of \(b\), then \(n\) copies of \(c\).

def anbncnLang : Language (Fin 3) :=
  {w | ∃ n, w = List.replicate n 0 ++ List.replicate n 1 ++
    List.replicate n 2}

Used by 3

Used byThe language \(a^n b^n c^n\) is not context-free · Context-free languages are not closed under complement · Context-free languages are not closed under intersection

TheoremThe language \(a^n b^n c^n\) is not context-free#✓fully proved

Over the three-letter alphabet \(\{a, b, c\}\) (the letters \(0, 1, 2\)), the language of the words \(a^n b^n c^n\) for \(n \in \mathbb{N}\) is not context-free.

Proof idea: by the pumping lemma, pumping \(a^n b^n c^n\) down would keep the three letter counts equal, so the pumped factor has equal counts of all letters, but a short factor misses \(a\) or \(c\), forcing the factor to be empty.

theorem anbncnLang_not_isContextFree : ¬ anbncnLang.IsContextFree

Uses 2 · Used by 2

Statement usesThe language \(a^n b^n c^n\)

Proof usesPumping lemma for context-free languages

Used byContext-free languages are not closed under complement · Context-free languages are not closed under intersection

TheoremContext-free languages are not closed under intersection#✓fully proved

There are context-free languages \(L\) and \(M\) over the three-letter alphabet \(\{0, 1, 2\}\) whose intersection \(L \cap M\) is not context-free.

theorem exists_isContextFree_inf_not_isContextFree :
    ∃ L M : Language (Fin 3), L.IsContextFree ∧ M.IsContextFree ∧
      ¬ (L ⊓ M).IsContextFree

Uses 8 · Used by 1

Proof usesClosure of context-free languages under Kleene star · Closure of context-free languages under concatenation · Singleton languages are context-free · The language \(a^n b^n c^n\) · The language \(a^n b^n c^n\) is not context-free · The language \(a^n b^n\) · The language \(a^n b^n\) is context-free · The Kleene star of a one-letter word

Used byIntersections of context-free languages need not be context-free

TheoremContext-free languages are not closed under complement#✓fully proved

There is a context-free language \(L\) over the three-letter alphabet \(\{0, 1, 2\}\) whose complement is not context-free.

Closure under complement and union would give closure under intersection.

theorem exists_isContextFree_compl_not_isContextFree :
    ∃ L : Language (Fin 3), L.IsContextFree ∧
      ¬ (Lᶜ).IsContextFree

Uses 9 · Used by 1

Proof usesClosure of context-free languages under union · Closure of context-free languages under Kleene star · Closure of context-free languages under concatenation · Singleton languages are context-free · The language \(a^n b^n c^n\) · The language \(a^n b^n c^n\) is not context-free · The language \(a^n b^n\) · The language \(a^n b^n\) is context-free · The Kleene star of a one-letter word

Used byComplements of context-free languages need not be context-free

TheoremIntersections of context-free languages need not be context-free#✓fully proved

Over the three-letter alphabet \(\{0, 1, 2\}\), it is not the case that for all context-free languages \(L\) and \(M\) the intersection \(L \cap M\) is context-free.

theorem not_forall_isContextFree_inf :
    ¬ ∀ L M : Language (Fin 3), L.IsContextFree → M.IsContextFree →
      (L ⊓ M).IsContextFree

Uses 1

Proof usesContext-free languages are not closed under intersection

TheoremComplements of context-free languages need not be context-free#✓fully proved

It is not the case that for every context-free language \(L\) over the three-letter alphabet \(\{0, 1, 2\}\), the complement of \(L\) is context-free.

theorem not_forall_isContextFree_compl :
    ¬ ∀ L : Language (Fin 3), L.IsContextFree →
      (Lᶜ).IsContextFree

Uses 1

Proof usesContext-free languages are not closed under complement

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.