Undecidable problems for context-free grammars

TheoremWhether two context-free languages intersect is undecidable#✓fully proved

There is an alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for a pair \((G_1, G_2)\) of encoded context-free grammars over \(T\), whether some word lies in both \(L(G_1)\) and \(L(G_2)\), where \(L(G)\) is the language of \(G\).

\(T\) is not required to be finite. This is Sipser's problem \(\mathit{OVERLAP}_{\mathit{CFG}}\).

theorem exists_not_tm2Decidable_overlap :
    ∃ (T : Type) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T × EncodedCFG T ↦
        ∃ w, w ∈ g.1.language ∧ w ∈ g.2.language

Uses 9 · Used by 2

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

Proof usesPCP many-one reduces to nonemptiness of the intersection of two context-free languages · Domino (Post correspondence problem) · The Post correspondence problem · The Post correspondence problem is undecidable · Decidability transfers along mapping reductions

Used byWhether two context-free languages are disjoint is undecidable · Disjointness of context-free languages is not recognizable

TheoremWhether two context-free languages are disjoint is undecidable#✓fully proved

There is an alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for a pair \((G_1, G_2)\) of encoded context-free grammars over \(T\), whether no word lies in both \(L(G_1)\) and \(L(G_2)\), where \(L(G)\) is the language of \(G\).

\(T\) is not required to be finite.

theorem exists_not_tm2Decidable_disjoint :
    ∃ (T : Type) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T × EncodedCFG T ↦
        ∀ w, ¬(w ∈ g.1.language ∧ w ∈ g.2.language)

Uses 6

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

Proof usesDecidability by multi-stack machines is closed under complement · Whether two context-free languages intersect is undecidable

TheoremWhether a context-free grammar is ambiguous is undecidable#✓fully proved

There is an alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for an encoded context-free grammar \(G\) over \(T\), whether \(G\) is ambiguous, that is, whether some word has two different leftmost derivations from the start nonterminal of \(G\).

\(T\) is not required to be finite. This is Sipser's problem \(\mathit{AMBIG}_{\mathit{CFG}}\).

theorem exists_not_tm2Decidable_isAmbiguous :
    ∃ (T : Type) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T ↦ IsAmbiguous g.toCFG

Uses 10

Statement usesDecidability by multi-stack machines · Encoded context-free grammars · Encoded grammars as pairs · Grammar denoted by an encoding · Ambiguous grammar

Proof usesPCP many-one reduces to ambiguity of context-free grammars · Domino (Post correspondence problem) · The Post correspondence problem · The Post correspondence problem is undecidable · Decidability transfers along mapping reductions

TheoremWhether a context-free grammar generates every word is undecidable#✓fully proved

There is a finite alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for an encoded context-free grammar \(G\) over \(T\), whether every word over \(T\) lies in the language of \(G\).

This is Sipser's problem \(\mathit{ALL}_{\mathit{CFG}}\).

theorem exists_not_tm2Decidable_univ :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T ↦ ∀ w, w ∈ g.language

Uses 10 · Used by 3

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

Proof usesThe complement of PCP many-one reduces to universality of context-free grammars · Domino (Post correspondence problem) · The Post correspondence problem · Decidability by multi-stack machines is closed under complement · The Post correspondence problem is undecidable · Decidability transfers along mapping reductions

Used byRegularity of context-free languages is undecidable · Equivalence of context-free grammars is undecidable · Inclusion of context-free languages is undecidable

DefinitionGrammar of all words#✓fully proved

For a finite alphabet \(T\), the encoded context-free grammar over \(T\) whose start nonterminal is \(S = 0\) and whose productions are \(S \to \varepsilon\) and \(S \to a S\) for every letter \(a \in T\).

It generates every word over \(T\).

noncomputable def allWordsCFG : EncodedCFG T :=
  ⟨0, (0, []) :: (Finset.univ : Finset T).toList.map fun a ↦ (0, [Sum.inr a, Sum.inl 0])⟩

Uses 1 · Used by 4

Statement usesEncoded context-free grammars

Used byEquivalence of context-free grammars is undecidable · Inclusion of context-free languages is undecidable · Equivalence of context-free grammars is not recognizable · Inclusion of context-free languages is not recognizable

TheoremEquivalence of context-free grammars is undecidable#✓fully proved

There is a finite alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for a pair \((G_1, G_2)\) of encoded context-free grammars over \(T\), whether \(L(G_1) = L(G_2)\), where \(L(G)\) is the language of \(G\).

This is Sipser's problem \(\mathit{EQ}_{\mathit{CFG}}\).

theorem exists_not_tm2Decidable_language_eq :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language = g.2.language

Uses 14

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

Proof usesGrammar of all words · Whether a context-free grammar generates every word is undecidable · Decidability transfers along mapping reductions · Decoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Valuation of a grammar · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal

TheoremInclusion of context-free languages is undecidable#✓fully proved

There is a finite alphabet \(T\), with decidable equality and a primitive recursive encoding into \(\mathbb{N}\), such that no multi-stack machine decides (in the sense of TM2-decidability), for a pair \((G_1, G_2)\) of encoded context-free grammars over \(T\), whether \(L(G_1) \subseteq L(G_2)\), where \(L(G)\) is the language of \(G\).

theorem exists_not_tm2Decidable_language_le :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Decidable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language ≤ g.2.language

Uses 14

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

Proof usesGrammar of all words · Whether a context-free grammar generates every word is undecidable · Decidability transfers along mapping reductions · Decoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Valuation of a grammar · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal

TheoremPost's theorem, contrapositive#✓fully proved

A recognizable undecidable predicate has an unrecognizable complement.

theorem not_tm2Recognizable_not_of {α : Type*} [Primcodable α] {p : α → Prop}
    (hp : TM2Recognizable p) (hd : ¬TM2Decidable p) : ¬TM2Recognizable fun a ↦ ¬p a

Uses 4 · Used by 2

Statement usesDecidability by multi-stack machines · Recognizability by multi-stack machines

Proof usesCo-recognizability by multi-stack machines · Post's theorem for multi-stack machines

Used byDisjointness of context-free languages is not recognizable · The complement of PCP is not recognizable

TheoremThe complement of PCP is not recognizable#✓fully proved

The complement of PCP is not recognizable, over some finite alphabet.

theorem exists_not_tm2Recognizable_not_pcp :
    ∃ (α : Type) (_ : Fintype α) (_ : Primcodable α),
      ¬TM2Recognizable fun P : List (Domino α) ↦ ¬PCP P

Uses 7 · Used by 1

Statement usesDomino (Post correspondence problem) · The Post correspondence problem · Recognizability by multi-stack machines

Proof usesPCP is Turing-recognizable · Decidability by multi-stack machines · The Post correspondence problem is undecidable · Post's theorem, contrapositive

Used byUniversality of context-free grammars is not recognizable

TheoremMembership in the first grammar of a pair is computable#✓fully proved

Let \(T\) be an alphabet with a primcodable encoding and decidable equality. The predicate that holds of a pair \(((g_1, g_2), w)\), where \(g_1, g_2\) are encoded context-free grammars over \(T\) and \(w\) is a word over \(T\), exactly when \(w\) lies in the language of \(g_1\), is a computable predicate.

theorem computablePred_mem_fst :
    ComputablePred fun p : (EncodedCFG T × EncodedCFG T) × List T ↦ p.2 ∈ p.1.1.language

Uses 6 · Used by 3

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

Proof usesDecidability by multi-stack machines · Multi-stack decidable predicates are exactly the computable predicates · Membership for context-free grammars is decidable

Used byEquivalence of context-free grammars is co-recognizable · Inclusion of context-free languages is co-recognizable · The overlap problem for context-free grammars is recognizable

TheoremThe overlap problem for context-free grammars is recognizable#✓fully proved

Let \(T\) be an alphabet with a primitive recursive coding into the natural numbers and decidable equality. For an encoded context-free grammar \(G\) over \(T\), write \(L(G)\) for the language it generates. The problem \(\mathrm{OVERLAP}_{\mathrm{CFG}}\), the set of pairs \((G, H)\) of encoded context-free grammars over \(T\) such that some word \(w\) over \(T\) lies in both \(L(G)\) and \(L(H)\), is recognizable by a multi-stack machine.

The proof searches for a common word, using that membership in a context-free language is decidable.

theorem tm2Recognizable_overlap :
    TM2Recognizable fun g : EncodedCFG T × EncodedCFG T ↦
      ∃ w, w ∈ g.1.language ∧ w ∈ g.2.language

Uses 11 · Used by 1

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

Proof usesDecidability by multi-stack machines · Membership in the first grammar of a pair is computable · Multi-stack decidable predicates are exactly the computable predicates · Multi-stack recognizable predicates are exactly the r.e. predicates · Membership for context-free grammars is decidable · Computable predicates are closed under conjunction · Existential projection preserves recursive enumerability

Used byDisjointness of context-free languages is not recognizable

TheoremUniversality of context-free grammars is co-recognizable#✓fully proved

For every alphabet \(T\) with a primcodable encoding and decidable equality, the set of encoded context-free grammars over \(T\) whose language contains every word over \(T\) is co-recognizable by a multi-stack Turing machine.

A recognizer for the complement searches for a word outside the language.

theorem tm2CoRecognizable_univ :
    TM2CoRecognizable fun g : EncodedCFG T ↦ ∀ w, w ∈ g.language

Uses 9

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

Proof usesDecidability by multi-stack machines · Multi-stack co-recognizable predicates are exactly the co-r.e. predicates · Multi-stack decidable predicates are exactly the computable predicates · Membership for context-free grammars is decidable · Existential projection preserves recursive enumerability

TheoremEquivalence of context-free grammars is co-recognizable#✓fully proved

For every alphabet \(T\) with a primcodable encoding and decidable equality, the set of pairs \((g_1, g_2)\) of encoded context-free grammars over \(T\) whose languages are equal is co-recognizable by a multi-stack Turing machine.

A recognizer for the complement searches for a word in exactly one of the two languages.

theorem tm2CoRecognizable_language_eq :
    TM2CoRecognizable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language = g.2.language

Uses 12

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

Proof usesDecidability by multi-stack machines · Membership in the first grammar of a pair is computable · Multi-stack co-recognizable predicates are exactly the co-r.e. predicates · Multi-stack decidable predicates are exactly the computable predicates · Membership for context-free grammars is decidable · Computable predicates are closed under conjunction · Computable predicates are closed under disjunction · Existential projection preserves recursive enumerability

TheoremInclusion of context-free languages is co-recognizable#✓fully proved

For every alphabet \(T\) with a primcodable encoding and decidable equality, the set of pairs \((g_1, g_2)\) of encoded context-free grammars over \(T\) for which the language of \(g_1\) is contained in the language of \(g_2\) is co-recognizable by a multi-stack Turing machine.

theorem tm2CoRecognizable_language_le :
    TM2CoRecognizable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language ≤ g.2.language

Uses 11

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

Proof usesDecidability by multi-stack machines · Membership in the first grammar of a pair is computable · Multi-stack co-recognizable predicates are exactly the co-r.e. predicates · Multi-stack decidable predicates are exactly the computable predicates · Membership for context-free grammars is decidable · Computable predicates are closed under conjunction · Existential projection preserves recursive enumerability

TheoremDisjointness of context-free languages is not recognizable#✓fully proved

There is an alphabet \(T\), with a primcodable encoding and decidable equality, such that the set of pairs \((g_1, g_2)\) of encoded context-free grammars over \(T\) whose languages are disjoint (no word lies in both) is not recognizable by a multi-stack Turing machine.

theorem exists_not_tm2Recognizable_disjoint :
    ∃ (T : Type) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Recognizable fun g : EncodedCFG T × EncodedCFG T ↦
        ∀ w, ¬(w ∈ g.1.language ∧ w ∈ g.2.language)

Uses 8

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

Proof usesDecidability by multi-stack machines · Whether two context-free languages intersect is undecidable · Post's theorem, contrapositive · The overlap problem for context-free grammars is recognizable

TheoremUniversality of context-free grammars is not recognizable#✓fully proved

There is a finite alphabet \(T\), with a primcodable encoding and decidable equality, such that the set of encoded context-free grammars over \(T\) whose language contains every word over \(T\) is not recognizable by a multi-stack Turing machine.

The complement of the Post correspondence problem reduces to this problem.

theorem exists_not_tm2Recognizable_univ :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Recognizable fun g : EncodedCFG T ↦ ∀ w, w ∈ g.language

Uses 9 · Used by 2

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

Proof usesThe complement of PCP many-one reduces to universality of context-free grammars · Domino (Post correspondence problem) · The Post correspondence problem · The complement of PCP is not recognizable · Recognizability transfers along mapping reductions

Used byEquivalence of context-free grammars is not recognizable · Inclusion of context-free languages is not recognizable

TheoremEquivalence of context-free grammars is not recognizable#✓fully proved

There is a finite alphabet \(T\), with a primcodable encoding and decidable equality, such that the set of pairs \((g_1, g_2)\) of encoded context-free grammars over \(T\) whose languages are equal is not recognizable by a multi-stack Turing machine.

theorem exists_not_tm2Recognizable_language_eq :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Recognizable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language = g.2.language

Uses 14

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

Proof usesGrammar of all words · Universality of context-free grammars is not recognizable · Recognizability transfers along mapping reductions · Decoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Valuation of a grammar · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal

TheoremInclusion of context-free languages is not recognizable#✓fully proved

There is a finite alphabet \(T\), with a primcodable encoding and decidable equality, such that the set of pairs \((g_1, g_2)\) of encoded context-free grammars over \(T\) for which the language of \(g_1\) is contained in the language of \(g_2\) is not recognizable by a multi-stack Turing machine.

theorem exists_not_tm2Recognizable_language_le :
    ∃ (T : Type) (_ : Fintype T) (_ : Primcodable T) (_ : DecidableEq T),
      ¬TM2Recognizable fun g : EncodedCFG T × EncodedCFG T ↦ g.1.language ≤ g.2.language

Uses 14

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

Proof usesGrammar of all words · Universality of context-free grammars is not recognizable · Recognizability transfers along mapping reductions · Decoding a production · Decoding a grammar symbol · Grammar denoted by an encoding · Valuation of a grammar · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.