# Example of R and G when $R \subseteq L(G)$ is undecidable [closed]

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.

• You're in luck, your question has already been answered in the SE network. – chazisop Aug 11 '15 at 22:41
• This question is off-topic here and more suitable for Computer Science: as the answer implies below every decision problem without a varying input is trivially decidable by either always Yes or always No algorithm. – Kaveh Aug 11 '15 at 23:35

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.)

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

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.