Theorems · Theorem · computer science

ContextFreeGrammar.mem_language_iff

∀ {T : Type u_1} (g : ContextFreeGrammar T) (w : List T),
  w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)

A given word w belongs to the language generated by a given context-free grammar g iff g can derive the word w (wrapped as a string) from the initial nonterminal of g in some number of steps.

Defined in

Mathlib.Computability.ContextFreeGrammar

Cited by

0 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound