<p>If you mean "undecidable" in the computational sense, then see the answer of Suhail Sherif.</p>

<p>Your question becomes more interesting if we take "undecidable" in the proof-theoretic sense, i.e. there is no mathematical proof (say in ZFC) of $R\subseteq L(G)$ and no proof of $R\not\subseteq L(G)$ either.</p>

<p>Such languages exist, because for any undecidable problem $P$ (in the computational sense), there is a particular instance of $P$ which is undecidable in the proof-theoretic sense. Otherwise, enumerating proofs in ZFC would constitute an algorithm to decide $P$.</p>

<p>We can build these languages explicitely, using the proof that there is no TM deciding the problem $P$: given $R$ and $G$, do we have $R\subseteq L(G)$ ? It goes like this: look at how the halting problem for any TM $M$ reduces to $P$, and take the $R$ and $G$ obtained from the TM $M_{ZFC}$ which looks for a contradiction in ZFC, and whose halting is undecidable in the proof-theoretic sense. The $R_{ZFC}$ and $G_{ZFC}$ obtained will provably verify $R_{ZFC}\subseteq L(G_{ZFC})$ iff $M_{ZFC}$ halt, and therefore this inclusion will be undecidable in ZFC, by Gödel's second incompleteness theorem.</p>

CC BY-SA 3.0
2015-08-11T18:02:01.937Z
2015-08-11T18:02:01.937Z
Denis
<p>Given an $R$ and a $G$, one can easily construct a TM which outputs whether $R \subseteq L(G)$.</p>

<p>(Consider two TMs, one that just rejects and one that just accepts. If not the first, then the second TM would definitely be correct.)</p>

<p>What is not possible is this: Give a TM that takes as input any $R$ and any $G$ and accepts iff $R \subseteq L(G)$ and rejects otherwise.</p>

<p>Note that the same is true for the halting problem. Given a TM $M$, it is decidable whether $M$ halts or not. (The same two TMs mentioned above would do.) What's undecidable is the general problem of being able to decide whether a TM given as input halts or not. (A single machine that can take any TM as input and be correct on all of them.)</p>

CC BY-SA 3.0
2015-08-11T17:45:49.873Z
2015-08-11T17:45:49.873Z
Suhail Sherif
<p>Could anybody provide an example of regular language R and context-free grammar G such that $R \subseteq L(G)$ is undecidable. Of course, if such language could be constructed. </p>

<p>Thanks.</p>

CC BY-SA 3.0
2015-08-11T22:41:03.330Z
You're in luck, your question has already been [answered](http://math.stackexchange.com/questions/70349/is-the-inclusion-of-a-regular-language-in-a-context-free-language-decidable) in the SE network.
chazisop
CC BY-SA 3.0
2015-08-11T23:35:11.177Z
This question is off-topic here and more suitable for [cs.se]: as the answer implies below every decision problem without a varying input is trivially decidable by either always Yes or always No algorithm.
Kaveh
<regular-language><context-free><undecidability>
Example of R and G when $R \subseteq L(G)$ is undecidable
gsv
# Example of R and G when $R \subseteq L(G)$ is undecidable

(Asked by: username_0 on 2015-08-11)

Could anybody provide an example of regular language R and context-free grammar G such that $R \subseteq L(G)$ is undecidable. Of course, if such language could be constructed.

Thanks.

**Tags:** regular-language, context-free, undecidability

> **Comments:**
> **username_1**: You're in luck, your question has already been [answered](http://math.stackexchange.com/questions/70349/is-the-inclusion-of-a-regular-language-in-a-context-free-language-decidable) in the SE network.  
> **username_2**: This question is off-topic here and more suitable for [cs.se]: as the answer implies below every decision problem without a varying input is trivially decidable by either always Yes or always No algorithm.  

---

## 2 answers

### Answer by username_3 on 2015-08-11. Score: 3

If you mean "undecidable" in the computational sense, then see the answer of username_4.

Your question becomes more interesting if we take "undecidable" in the proof-theoretic sense, i.e. there is no mathematical proof (say in ZFC) of $R\subseteq L(G)$ and no proof of $R\not\subseteq L(G)$ either.

Such languages exist, because for any undecidable problem $P$ (in the computational sense), there is a particular instance of $P$ which is undecidable in the proof-theoretic sense. Otherwise, enumerating proofs in ZFC would constitute an algorithm to decide $P$.

We can build these languages explicitely, using the proof that there is no TM deciding the problem $P$: given $R$ and $G$, do we have $R\subseteq L(G)$ ? It goes like this: look at how the halting problem for any TM $M$ reduces to $P$, and take the $R$ and $G$ obtained from the TM $M\_{ZFC}$ which looks for a contradiction in ZFC, and whose halting is undecidable in the proof-theoretic sense. The $R\_{ZFC}$ and $G\_{ZFC}$ obtained will provably verify $R\_{ZFC}\subseteq L(G\_{ZFC})$ iff $M\_{ZFC}$ halt, and therefore this inclusion will be undecidable in ZFC, by Gödel's second incompleteness theorem.


---

### Answer by username_4 on 2015-08-11. Score: 3

Given an $R$ and a $G$, one can easily construct a TM which outputs whether $R \subseteq L(G)$.

(Consider two TMs, one that just rejects and one that just accepts. If not the first, then the second TM would definitely be correct.)

What is not possible is this: Give a TM that takes as input any $R$ and any $G$ and accepts iff $R \subseteq L(G)$ and rejects otherwise.

Note that the same is true for the halting problem. Given a TM $M$, it is decidable whether $M$ halts or not. (The same two TMs mentioned above would do.) What's undecidable is the general problem of being able to decide whether a TM given as input halts or not. (A single machine that can take any TM as input and be correct on all of them.)


---

