Emptiness of context-free grammars

36 fully proved

The procedure

DefinitionAcceptable symbols#✓fully proved

Given a list \(G\) of natural numbers and a symbol \(s\) of an encoded grammar over an alphabet \(T\), which is either a nonterminal \(i \in \mathbb{N}\) or a terminal in \(T\), \(s\) is acceptable when it is a terminal or a nonterminal that occurs in \(G\). The test returns a Boolean.

def symOk (G : List ℕ) (s : ℕ ⊕ T) : Bool :=
  Sum.elim (memB G) (fun _ => true) s

Uses 1 · Used by 4

Statement usesBoolean membership test for lists of natural numbers

Used bySoundness of the productive-nonterminal iteration · The generating nonterminals are closed under one more round · Acceptable productions · Completeness of the generating-nonterminal computation

DefinitionAcceptable productions#✓fully proved

Given a list \(G\) of nonterminals (natural numbers), the test accepts an encoded production \((A, \rho)\) when every symbol of \(\rho\) is acceptable: a terminal always is, and a nonterminal is when it belongs to \(G\). So the production is accepted exactly when every nonterminal occurring in \(\rho\) belongs to \(G\).

def ruleOk (G : List ℕ) (e : ℕ × List (ℕ ⊕ T)) : Bool :=
  e.2.foldr (fun s b => symOk G s && b) true

Uses 1 · Used by 7

Statement usesAcceptable symbols

Used byReduction is primitive recursive · Emptiness of regular expressions is decidable · Emptiness of context-free grammars is computable · Soundness of the productive-nonterminal iteration · One round of the generating-nonterminal computation · The generating nonterminals are closed under one more round · Completeness of the generating-nonterminal computation

DefinitionOne round of the generating-nonterminal computation#✓fully proved

Let a list of productions be given, each a pair of a nonterminal \(A \in \mathbb{N}\) and a right-hand side made of nonterminals and terminals, together with a list \(G\) of nonterminals. One round returns, in order, the left-hand sides of those productions in whose right-hand side every nonterminal belongs to \(G\).

def genStep (rules : List (ℕ × List (ℕ ⊕ T))) (G : List ℕ) : List ℕ :=
  rules.filterMap fun e => cond (ruleOk G e) (some e.1) none

Uses 1 · Used by 7

Statement usesAcceptable productions

Used byReduction is primitive recursive · Emptiness of regular expressions is decidable · Emptiness of context-free grammars is computable · Soundness of the productive-nonterminal iteration · The generating nonterminals are closed under one more round · Generating nonterminals · Completeness of the generating-nonterminal computation

DefinitionGenerating nonterminals#✓fully proved

For an encoded grammar \(g\), start from the empty list of nonterminals and, in each round, replace the current list \(G\) by the list of left-hand sides of those productions of \(g\) whose right-hand sides contain no nonterminal outside \(G\). The generating nonterminals of \(g\) are the list obtained after as many rounds as \(g\) has productions.

Every nonterminal in this list derives a terminal word, and the start nonterminal is in it whenever the grammar generates some word.

def generating (g : EncodedCFG T) : List ℕ :=
  (genStep g.rules)^[g.rules.length] []

Uses 2 · Used by 9

Statement usesEncoded context-free grammars · One round of the generating-nonterminal computation

Used byThe nullable nonterminals are computed · Computed nullable nonterminals of an encoded grammar · Reduction is primitive recursive · Emptiness of regular expressions is decidable · Emptiness of context-free grammars is computable · The generating nonterminals are closed under one more round · The emptiness test for context-free grammars · Correctness of the emptiness test · Completeness of the generating-nonterminal computation

DefinitionThe emptiness test for context-free grammars#✓fully proved

For an encoded grammar \(g\), the test returns true exactly when the start nonterminal of \(g\) is not among the generating nonterminals of \(g\).

def isEmptyB (g : EncodedCFG T) : Bool :=
  !memB g.generating g.start

Uses 3 · Used by 4

Statement usesBoolean membership test for lists of natural numbers · Encoded context-free grammars · Generating nonterminals

Used byEmptiness test for regular expressions · Emptiness of regular expressions is decidable · Emptiness of context-free grammars is computable · Correctness of the emptiness test

Stabilization

TheoremThe generating nonterminals are closed under one more round#✓fully proved

For an encoded grammar \(g\), one more round of the generating-nonterminal computation, applied to the productions of \(g\) and the generating nonterminals of \(g\), yields only generating nonterminals of \(g\): every left-hand side of a production of \(g\) whose right-hand side has all its nonterminals among the generating nonterminals of \(g\) is itself a generating nonterminal of \(g\).

theorem genStep_generating_subset (g : EncodedCFG T) :
    genStep g.rules g.generating ⊆ g.generating

Uses 7 · Used by 1

Statement usesEncoded context-free grammars · One round of the generating-nonterminal computation · Generating nonterminals

Proof usesBounded monotone rounds on lists close off · Boolean membership test for lists of natural numbers · Acceptable productions · Acceptable symbols

Used byCompleteness of the generating-nonterminal computation

Correctness

TheoremSentential forms of productive nonterminals derive terminal words#✓fully proved

In a context-free grammar \(G\), if every nonterminal occurring in a sentential form \(u\) derives some terminal word, then \(u\) derives some terminal word.

theorem exists_derives_of_forall {G : ContextFreeGrammar T} :
    ∀ u : List (Symbol T G.NT),
      (∀ A, Symbol.nonterminal A ∈ u → ∃ w : List T, G.Derives [.nonterminal A] (w.map .terminal))
      → ∃ w : List T, G.Derives u (w.map .terminal)

Uses 1 · Used by 1

Proof usesConcatenating derivations

Used bySoundness of the productive-nonterminal iteration

TheoremSoundness of the productive-nonterminal iteration#✓fully proved

Let \(g\) be an encoded context-free grammar. A round sends a list \(H\) of nonterminals to the left-hand sides of those productions of \(g\) in whose right-hand side every nonterminal belongs to \(H\). For every \(k \ge 0\), every nonterminal obtained after \(k\) rounds starting from the empty list derives some terminal word in the context-free grammar that \(g\) denotes.

theorem exists_derives_of_mem_iterate (g : EncodedCFG T) :
    ∀ (k : ℕ) {j : ℕ}, j ∈ (genStep g.rules)^[k] [] →
      ∃ w : List T, g.toCFG.Derives [.nonterminal j] (w.map .terminal)

Uses 9 · Used by 2

Statement usesEncoded context-free grammars · One round of the generating-nonterminal computation · Grammar denoted by an encoding

Proof usesBoolean membership test for lists of natural numbers · Decoding a production · Decoding a grammar symbol · Sentential forms of productive nonterminals derive terminal words · Acceptable productions · Acceptable symbols

Used byThe nullable nonterminals are computed · Correctness of the emptiness test

TheoremA sentential form containing an empty nonterminal denotes the empty language#✓fully proved

Let \(T\) be an alphabet and \(N\) a set of nonterminals, and let \(V\) assign a language over \(T\) to each nonterminal. A sentential form \(X_1 \cdots X_m\) over \(T\) and \(N\) denotes under \(V\) the concatenation \(L_1 \cdots L_m\), where \(L_t = V(X_t)\) if \(X_t\) is a nonterminal and \(L_t = \{X_t\}\) if \(X_t\) is a terminal; the empty form denotes \(\{\varepsilon\}\). Let \(A \in N\) with \(V(A) = \emptyset\). Then every sentential form over \(T\) and \(N\) in which \(A\) occurs denotes the empty language under \(V\).

theorem evalForm_eq_zero_of_mem {N : Type*} {V : N → Language T} {A : N} (hA : V A = 0) :
    ∀ {u : List (Symbol T N)}, Symbol.nonterminal A ∈ u → evalForm V u = 0

Uses 2 · Used by 1

Statement usesInterpretation of a sentential form

Proof usesInterpretation of a grammar symbol

Used byCompleteness of the generating-nonterminal computation

TheoremCompleteness of the generating-nonterminal computation#✓fully proved

If an encoded grammar \(g\) generates some word \(w\), then the start nonterminal of \(g\) is among the generating nonterminals of \(g\) computed by the emptiness procedure.

theorem start_mem_generating_of_mem_language {g : EncodedCFG T} {w : List T}
    (hw : w ∈ g.language) : g.start ∈ g.generating

Uses 15 · Used by 2

Statement usesEncoded context-free grammars · Generating nonterminals · Language of an encoded grammar

Proof usesBoolean membership test for lists of natural numbers · Decoding a production · Decoding a grammar symbol · A sentential form containing an empty nonterminal denotes the empty language · One round of the generating-nonterminal computation · The generating nonterminals are closed under one more round · Acceptable productions · Acceptable symbols · Grammar denoted by an encoding · Valuation of a grammar · Interpretation of a sentential form · Valuations bound the language of a grammar

Used byThe nullable nonterminals are computed · Correctness of the emptiness test

TheoremCorrectness of the emptiness test#✓fully proved

For every encoded context-free grammar \(g\), the emptiness test returns true on \(g\) if and only if the language of \(g\) is empty.

theorem isEmptyB_iff (g : EncodedCFG T) : g.isEmptyB = true ↔ g.language = 0

Uses 8 · Used by 2

Statement usesEncoded context-free grammars · The emptiness test for context-free grammars · Language of an encoded grammar

Proof usesBoolean membership test for lists of natural numbers · Soundness of the productive-nonterminal iteration · Generating nonterminals · Completeness of the generating-nonterminal computation · Grammar denoted by an encoding

Used byEmptiness of regular expressions is decidable · Emptiness of context-free grammars is computable

Emptiness is computable

TheoremEmptiness of context-free grammars is computable#✓fully proved

Let \(T\) be an alphabet with decidable equality and a primitive recursive encoding into the natural numbers. The predicate on encoded context-free grammars \(g\) over \(T\) that holds exactly when the language of \(g\) is empty is a computable predicate.

theorem computablePred_language_eq_zero :
    ComputablePred fun g : EncodedCFG T => g.language = 0

Uses 9 · Used by 1

Statement usesEncoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesBoolean membership test for lists of natural numbers · One round of the generating-nonterminal computation · Generating nonterminals · The emptiness test for context-free grammars · Correctness of the emptiness test · Acceptable productions

Used byEmptiness of context-free grammars is decidable

TheoremEmptiness of context-free grammars is decidable#✓fully proved

For every alphabet \(T\) with decidable equality and a primitive recursive encoding, the property of an encoded context-free grammar \(g\) over \(T\) that the language of \(g\) is empty is decidable by a multi-stack machine. This is Sipser, Theorem 4.8: the problem \(E_{\mathrm{CFG}}\) is decidable.

theorem tm2Decidable_language_eq_zero :
    Cslib.Decidability.TM2Decidable fun g : EncodedCFG T => g.language = 0

Uses 6

Statement usesDecidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesMulti-stack decidable predicates are exactly the computable predicates · Emptiness of context-free grammars is computable

Factors

DefinitionFactor of a word#✓fully proved

For a word \(w = w_0 w_1 \cdots w_{n-1}\) and natural numbers \(i\) and \(j\), the factor of \(w\) from position \(i\) to position \(j\) is obtained by dropping the first \(i\) letters of \(w\) and keeping at most the first \(j - i\) letters of the rest, where \(j - i\) is \(0\) when \(j \le i\). For \(i \le j \le n\) it is \(w_i w_{i+1} \cdots w_{j-1}\).

def factor (w : List T) (i j : ℕ) : List T :=
  (w.drop i).take (j - i)

Used by 4

Used bySplitting a factor · Correctness of the membership test · Completeness of the start positions · Sound items

TheoremSplitting a factor#✓fully proved

Let \(w\) be a word and \(i \le j \le |w|\), and write \(w[i, j)\) for the factor of \(w\) from position \(i\) to position \(j\). If \(w[i, j) = uv\), then \(i + |u| \le j\), \(w[i, i + |u|) = u\) and \(w[i + |u|, j) = v\).

theorem factor_eq_append {w u v : List T} {i j : ℕ} (hij : i ≤ j) (hj : j ≤ w.length)
    (h : factor w i j = u ++ v) :
    i + u.length ≤ j ∧ factor w i (i + u.length) = u ∧ factor w (i + u.length) j = v

Uses 1 · Used by 1

Statement usesFactor of a word

Used byCompleteness of the start positions

Matching right-hand sides

DefinitionFitting a symbol at a position#✓fully proved

Write \(\langle s, t \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) given by \(\langle s, t \rangle = t^2 + s\) if \(s < t\) and \(\langle s, t \rangle = s^2 + s + t\) otherwise. Given a word \(w\), a list \(R\) of items, a list \(S\) of positions and an encoded symbol \(X\), the test at a position \(i\) succeeds when either \(X\) is a terminal \(a\), \(i + 1 \in S\) and the letter of \(w\) at position \(i\) (counting from \(0\)) is \(a\); or \(X\) is a nonterminal \(B\) and some \(k \in S\) has \(\langle B, \langle i, k \rangle \rangle \in R\).

In use, \(S\) holds the positions where the rest of the right-hand side can start.

def symFits (w : List T) (R : List ℕ) (S : List ℕ) (X : ℕ ⊕ T) (i : ℕ) : Bool :=
  match X with
  | .inr a => memB S (i + 1) && decide (w[i]? = some a)
  | .inl B => S.any fun k => memB R (Nat.pair B (Nat.pair i k))

Uses 1 · Used by 7

Statement usesBoolean membership test for lists of natural numbers

Used byThe equivalence test is primitive recursive · Membership for regular expressions is decidable · Correctness of the membership test · Completeness of the start positions · Start positions of a right-hand side · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable

DefinitionStart positions of a right-hand side#✓fully proved

Write \(\langle s, t \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) given by \(\langle s, t \rangle = t^2 + s\) if \(s < t\) and \(\langle s, t \rangle = s^2 + s + t\) otherwise. Given a word \(w\), a list \(R\) of items (natural numbers), a position \(j\) and an encoded right-hand side \(X_1 \cdots X_m\), a position \(i\) is a start when there are positions \(i = p_0, p_1, \ldots, p_m = j\) with \(p_0, \ldots, p_{m-1} \le |w|\) such that for each \(l = 1, \ldots, m\): if \(X_l\) is a terminal \(a\), then \(p_l = p_{l-1} + 1\) and the letter of \(w\) at position \(p_{l-1}\) (counting from \(0\)) is \(a\); if \(X_l\) is a nonterminal \(B\), then \(R\) contains the code \(\langle B, \langle p_{l-1}, p_l \rangle \rangle\). The starts are computed from the right, one symbol at a time, by the symbol-fitting test; for the empty right-hand side the only start is \(j\).

def starts (w : List T) (R : List ℕ) (j : ℕ) (rhs : List (ℕ ⊕ T)) : List ℕ :=
  rhs.foldr (fun X S => (List.range (w.length + 1)).filter (symFits w R S X)) [j]

Uses 1 · Used by 7

Statement usesFitting a symbol at a position

Used byThe equivalence test is primitive recursive · Membership for regular expressions is decidable · Correctness of the membership test · Completeness of the start positions · One round of the membership procedure · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable

DefinitionOne round of the membership procedure#✓fully proved

Write \(\langle s, t \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) given by \(\langle s, t \rangle = t^2 + s\) if \(s < t\) and \(\langle s, t \rangle = s^2 + s + t\) otherwise. Given an encoded grammar \(g\), a word \(w\) and a list \(R\) of items found so far, the round lists, for every production \(A \to \rho\) of \(g\), every position \(j \le |w|\) and every start \(i\) of \(\rho\) for the factor of \(w\) ending at \(j\) given \(R\), the code \(\langle A, \langle i, j \rangle \rangle\) of the item \((A, i, j)\).

def memStep (g : EncodedCFG T) (w : List T) (R : List ℕ) : List ℕ :=
  g.rules.flatMap fun e => (List.range (w.length + 1)).flatMap fun j =>
    (starts w R j e.2).map fun i => Nat.pair e.1 (Nat.pair i j)

Uses 2 · Used by 7

Statement usesEncoded context-free grammars · Start positions of a right-hand side

Used byThe equivalence test is primitive recursive · Membership for regular expressions is decidable · Items found by the membership procedure · Correctness of the membership test · Completeness of the start positions · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable

DefinitionCandidate items for membership#✓fully proved

For an encoded grammar \(g\) and a word \(w\), the candidate items are the triples \((A, i, j)\), encoded as natural numbers by pairing, where \(A\) is the left-hand side of a production of \(g\) and \(i, j \le |w|\); each triple is listed once for every production whose left-hand side is \(A\).

def items (g : EncodedCFG T) (w : List T) : List ℕ :=
  (g.rules.map Prod.fst).flatMap fun A => (List.range (w.length + 1)).flatMap fun j =>
    (List.range (w.length + 1)).map fun i => Nat.pair A (Nat.pair i j)

Uses 1 · Used by 7

Statement usesEncoded context-free grammars

Used byThe equivalence test is primitive recursive · Membership for regular expressions is decidable · Items found by the membership procedure · Correctness of the membership test · Completeness of the start positions · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable

DefinitionItems found by the membership procedure#✓fully proved

Let \(g\) be an encoded context-free grammar and \(w = w_0 \cdots w_{n-1}\) a word. An item is a triple \((A, i, j)\) of natural numbers, coded as a natural number by nested pairing. A round sends a list \(R\) of items to the items \((A, i, j)\) such that \(A \to X_1 \cdots X_m\) is a production of \(g\), \(j \le n\), and there are positions \(i = k_0, k_1, \ldots, k_m = j\), each at most \(n\), such that for every \(t\) with \(1 \le t \le m\), either \(X_t\) is the terminal \(w_{k_{t-1}}\) and \(k_t = k_{t-1} + 1\), or \(X_t\) is a nonterminal \(B\) with \((B, k_{t-1}, k_t)\) in \(R\). The items found are the result of applying the round \(M\) times to the empty list, where \(M\) is \((n + 1)^2\) times the length of the list of productions of \(g\).

def found (g : EncodedCFG T) (w : List T) : List ℕ :=
  (memStep g w)^[(items g w).length] []

Uses 3 · Used by 7

Statement usesEncoded context-free grammars · Candidate items for membership · One round of the membership procedure

Used byThe equivalence test is primitive recursive · Membership for regular expressions is decidable · The membership test for context-free grammars · Correctness of the membership test · Completeness of the start positions · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable

DefinitionThe membership test for context-free grammars#✓fully proved

For an encoded grammar \(g\) with start nonterminal \(S\) and a word \(w\), the test returns true exactly when the item \((S, 0, |w|)\) is among the items found for \(g\) and \(w\).

def memLanguageB (g : EncodedCFG T) (w : List T) : Bool :=
  memB (found g w) (Nat.pair g.start (Nat.pair 0 w.length))

Uses 3 · Used by 10

Statement usesBoolean membership test for lists of natural numbers · Encoded context-free grammars · Items found by the membership procedure

Used byThe equivalence test is correct · Membership test for regular expressions · The equivalence test is primitive recursive · Membership for regular expressions is decidable · The infiniteness test · Correctness of the infiniteness test · Correctness of the membership test · Infiniteness of context-free languages is decidable · Membership for context-free grammars is decidable · Correctness of the Boolean atom checker

Soundness

DefinitionSound items#✓fully proved

Write \(\langle s, t \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) given by \(\langle s, t \rangle = t^2 + s\) if \(s < t\) and \(\langle s, t \rangle = s^2 + s + t\) otherwise. Given an encoded grammar \(g\) and a word \(w\), a natural number \(x\) is a sound item when \(x = \langle A, \langle i, j \rangle \rangle\) for some \(A\), \(i\), \(j\) with \(i \le j \le |w|\) such that the nonterminal \(A\) yields, in the decoded grammar of \(g\), the factor of \(w\) from position \(i\) to position \(j\).

def SoundItem (g : EncodedCFG T) (w : List T) (x : ℕ) : Prop :=
  ∃ A i j, x = Nat.pair A (Nat.pair i j) ∧ i ≤ j ∧ j ≤ w.length ∧
    Yields g.toCFG [.nonterminal A] (factor w i j)

Uses 4 · Used by 1

Statement usesEncoded context-free grammars · Factor of a word · Grammar denoted by an encoding · Yield of a sentential form

Used byCorrectness of the membership test

Completeness

TheoremCompleteness of the start positions#✓fully proved

Let \(g\) be an encoded context-free grammar over an alphabet \(T\) with decidable equality, let \(w\) be a word over \(T\), and let \(\rho\) be an encoded right-hand side whose decoding yields a word \(u\) in the grammar that \(g\) denotes. If \(i \le j \le |w|\) and \(u\) is the factor of \(w\) from position \(i\) to position \(j\), then \(i\) is a start position of \(\rho\) at \(j\) for the word \(w\) and the list of items found by the membership procedure on \(g\) and \(w\).

theorem mem_starts_of_yields {g : EncodedCFG T} {w : List T} {β : List (Symbol T g.toCFG.NT)}
    {u : List T} (h : Yields g.toCFG β u) :
    ∀ (rhs : List (ℕ ⊕ T)) (i j : ℕ), β = rhs.map decodeSymbol → u = factor w i j → i ≤ j →
      j ≤ w.length → i ∈ starts w (found g w) j rhs

Uses 14 · Used by 1

Statement usesEncoded context-free grammars · Decoding a grammar symbol · Factor of a word · Items found by the membership procedure · Start positions of a right-hand side · Grammar denoted by an encoding · Yield of a sentential form

Proof usesBounded monotone rounds on lists close off · Boolean membership test for lists of natural numbers · Decoding a production · Splitting a factor · Candidate items for membership · One round of the membership procedure · Fitting a symbol at a position

Used byCorrectness of the membership test

TheoremCorrectness of the membership test#✓fully proved

For every encoded context-free grammar \(g\) and every word \(w\), the membership test returns true on \(g\) and \(w\) if and only if \(w\) belongs to the language of \(g\).

theorem memLanguageB_iff {g : EncodedCFG T} {w : List T} :
    memLanguageB g w = true ↔ w ∈ g.language

Uses 19 · Used by 5

Statement usesEncoded context-free grammars · Language of an encoded grammar · The membership test for context-free grammars

Proof usesBoolean membership test for lists of natural numbers · Sound items · Decoding a production · Decoding a grammar symbol · Factor of a word · Items found by the membership procedure · Candidate items for membership · One round of the membership procedure · Completeness of the start positions · Start positions of a right-hand side · Fitting a symbol at a position · Grammar denoted by an encoding · Yield of a sentential form · Concatenation of yields · Language membership through yields · Yield through one production

Used byThe equivalence test is correct · Membership for regular expressions is decidable · Correctness of the infiniteness test · Membership for context-free grammars is decidable · Correctness of the Boolean atom checker

TheoremMembership for context-free grammars is decidable#✓fully proved

For every alphabet \(T\) with decidable equality and a primitive recursive encoding, the property of a pair \((g, w)\), where \(g\) is an encoded context-free grammar over \(T\) and \(w\) is a word over \(T\), that \(w\) is in the language of \(g\) is decidable by a multi-stack machine. This is Sipser, Theorem 4.7: the problem \(A_{\mathrm{CFG}}\) is decidable.

theorem tm2Decidable_mem_language :
    Cslib.Decidability.TM2Decidable fun p : EncodedCFG T × List T => p.2 ∈ p.1.language

Uses 14 · Used by 5

Statement usesDecidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesPredicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Items found by the membership procedure · Candidate items for membership · The membership test for context-free grammars · Correctness of the membership test · One round of the membership procedure · Start positions of a right-hand side · Fitting a symbol at a position

Used byMembership in the first grammar of a pair is computable · Equivalence of context-free grammars is co-recognizable · Inclusion of context-free languages is co-recognizable · Universality of context-free grammars is co-recognizable · The overlap problem for context-free grammars is recognizable

Infiniteness

DefinitionRight-hand side length bound#✓fully proved

For an encoded grammar \(g\), the length bound is the maximum of \(2\) and the lengths of the right-hand sides of the productions of \(g\).

def lenBound (g : EncodedCFG T) : ℕ :=
  g.rules.foldr (fun e m => max e.2.length m) 2

Uses 1 · Used by 3

Statement usesEncoded context-free grammars

Used byPumping bound of an encoded grammar · Pumping lemma for encoded grammars · Infiniteness of context-free languages is decidable

DefinitionPumping bound of an encoded grammar#✓fully proved

For an encoded grammar \(g\), let \(L\) be the length bound of \(g\), the larger of \(2\) and the largest length of a right-hand side of a production of \(g\), and let \(K\) be the number of distinct left-hand sides of the productions of \(g\). The pumping bound of \(g\) is \(L^{K+1}\).

With this bound, Ogden's lemma with every letter marked gives the pumping lemma for the decoded grammar.

def pumpBound (g : EncodedCFG T) : ℕ :=
  g.lenBound ^ ((dedupB (g.rules.map Prod.fst)).length + 1)

Uses 3 · Used by 6

Statement usesDuplicate removal for lists of natural numbers · Encoded context-free grammars · Right-hand side length bound

Used byContext-free pumping down below twice the pumping bound · The infiniteness test · Correctness of the infiniteness test · Long words make a context-free language infinite · Pumping lemma for encoded grammars · Infiniteness of context-free languages is decidable

DefinitionThe words of a given length over a list of letters#✓fully proved

For a list \(A\) of letters and a natural number \(n\), the list obtained from the list whose only entry is the empty word by \(n\) rounds, each of which replaces every word \(w\), in order, by the words \(a w\) for the letters \(a\) of \(A\), in order. Its entries are exactly the words of length \(n\) all of whose letters occur in \(A\).

def wordsOver (A : List T) (n : ℕ) : List (List T) :=
  (fun W => W.flatMap fun w => A.map fun a => a :: w)^[n] [[]]

Used by 3

Used byThe infiniteness test · Correctness of the infiniteness test · Infiniteness of context-free languages is decidable

DefinitionThe terminals of an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\) over an alphabet \(T\) with decidable equality, the list of the terminals that occur in the right-hand sides of the productions of \(g\), each listed once.

Listing each terminal once keeps the enumeration of the words over these terminals free of repetitions.

def terminals (g : EncodedCFG T) : List T :=
  (g.rules.flatMap fun e => e.2.filterMap Sum.getRight?).foldr
    (fun a acc => cond (acc.any fun b => decide (b = a)) acc (a :: acc)) []

Uses 1 · Used by 4

Statement usesEncoded context-free grammars

Used byThe infiniteness test · Correctness of the infiniteness test · Letters of generated words occur in the productions · Infiniteness of context-free languages is decidable

DefinitionThe infiniteness test#✓fully proved

Let \(g\) be an encoded grammar and \(N\) its pumping bound. The test returns true exactly when some word \(w\) whose letters all occur as terminals in the productions of \(g\), with \(N \le |w| < 2N\), is accepted by the membership test for \(g\).

def infiniteB (g : EncodedCFG T) : Bool :=
  (List.range g.pumpBound).any fun i =>
    (wordsOver g.terminals (g.pumpBound + i)).any g.memLanguageB

Uses 5 · Used by 2

Statement usesEncoded context-free grammars · The membership test for context-free grammars · Pumping bound of an encoded grammar · The terminals of an encoded grammar · The words of a given length over a list of letters

Used byCorrectness of the infiniteness test · Infiniteness of context-free languages is decidable

TheoremLetters of generated words occur in the productions#✓fully proved

If a word \(w\) is generated by an encoded grammar \(g\), then every letter of \(w\) is among the terminals of \(g\), that is, it occurs in the right-hand side of some production of \(g\).

theorem mem_terminals_of_mem_language {g : EncodedCFG T} {w : List T} (hw : w ∈ g.language)
    {a : T} (ha : a ∈ w) : a ∈ g.terminals

Uses 8 · Used by 1

Statement usesEncoded context-free grammars · Language of an encoded grammar · The terminals of an encoded grammar

Proof usesDecoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Yield of a sentential form · Language membership through yields

Used byCorrectness of the infiniteness test

TheoremPumping lemma for encoded grammars#✓fully proved

Let \(g\) be an encoded grammar with pumping bound \(N\). Every word \(w\) generated by \(g\) with \(|w| \ge N\) can be written as \(w = uvxyz\) with \(vy\) nonempty and \(|vxy| \le N\), such that \(u v^i x y^i z\) is generated by \(g\) for every natural number \(i\), including \(i = 0\).

theorem pumping_pumpBound (g : EncodedCFG T) :
    ∀ w ∈ g.language, g.pumpBound ≤ w.length → ∃ u v x y z : List T,
      w = u ++ v ++ x ++ y ++ z ∧ v ++ y ≠ [] ∧ (v ++ x ++ y).length ≤ g.pumpBound ∧
      ∀ i : ℕ, u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++ z ∈
        g.language

Uses 10 · Used by 2

Statement usesEncoded context-free grammars · Language of an encoded grammar · Pumping bound of an encoded grammar

Proof usesDuplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Decoding a production · Decoding a grammar symbol · Right-hand side length bound · Grammar denoted by an encoding · The pumping lemma for a grammar, with an explicit bound

Used byContext-free pumping down below twice the pumping bound · Long words make a context-free language infinite

TheoremLong words make a context-free language infinite#✓fully proved

If the language of an encoded grammar \(g\) contains a word whose length is at least the pumping bound of \(g\), then the language of \(g\) is infinite.

theorem infinite_of_mem_of_le {g : EncodedCFG T} {w : List T} (hw : w ∈ g.language)
    (hlen : g.pumpBound ≤ w.length) : g.language.Infinite

Uses 4 · Used by 1

Statement usesEncoded context-free grammars · Language of an encoded grammar · Pumping bound of an encoded grammar

Proof usesPumping lemma for encoded grammars

Used byCorrectness of the infiniteness test

TheoremContext-free pumping down below twice the pumping bound#✓fully proved

Let \(g\) be an encoded context-free grammar, let \(L\) be the largest of \(2\) and the lengths of the right-hand sides of the productions of \(g\), let \(K\) be the number of distinct left-hand sides of these productions, and let \(N = L^{K+1}\) be the pumping bound of \(g\). For every word \(w\) in the language of \(g\) with \(|w| \ge N\), there is a word \(v\) in the language of \(g\) with \(N \le |v| < 2N\).

theorem exists_mem_le_lt {g : EncodedCFG T} :
    ∀ (n : ℕ) (w : List T), w.length = n → w ∈ g.language → g.pumpBound ≤ w.length →
      ∃ v ∈ g.language, g.pumpBound ≤ v.length ∧ v.length < 2 * g.pumpBound

Uses 4 · Used by 1

Statement usesEncoded context-free grammars · Language of an encoded grammar · Pumping bound of an encoded grammar

Proof usesPumping lemma for encoded grammars

Used byCorrectness of the infiniteness test

TheoremCorrectness of the infiniteness test#✓fully proved

For every encoded context-free grammar \(g\), the infiniteness test returns true on \(g\) if and only if the language of \(g\) is infinite.

theorem infiniteB_iff {g : EncodedCFG T} : g.infiniteB = true ↔ g.language.Infinite

Uses 11 · Used by 1

Statement usesEncoded context-free grammars · The infiniteness test · Language of an encoded grammar

Proof usesContext-free pumping down below twice the pumping bound · Long words make a context-free language infinite · The membership test for context-free grammars · Correctness of the membership test · Letters of generated words occur in the productions · Pumping bound of an encoded grammar · The terminals of an encoded grammar · The words of a given length over a list of letters

Used byInfiniteness of context-free languages is decidable

TheoremInfiniteness of context-free languages is decidable#✓fully proved

For every alphabet \(T\) with decidable equality and a primitive recursive encoding, the property of an encoded context-free grammar \(g\) over \(T\) that the language of \(g\) is infinite is decidable by a multi-stack machine. This is the problem \(\mathrm{INFINITE}_{\mathrm{CFG}}\).

theorem tm2Decidable_language_infinite :
    Cslib.Decidability.TM2Decidable fun g : EncodedCFG T => g.language.Infinite

Uses 20

Statement usesDecidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Language of an encoded grammar

Proof usesPredicates with a primitive recursive decision procedure are computable · Duplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Items found by the membership procedure · The infiniteness test · Correctness of the infiniteness test · Candidate items for membership · Right-hand side length bound · The membership test for context-free grammars · One round of the membership procedure · Pumping bound of an encoded grammar · Start positions of a right-hand side · Fitting a symbol at a position · The terminals of an encoded grammar · The words of a given length over a list of letters

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.