# The formal proof that one Turing Machine recognizes one specific language

When given one grammar, we can formally prove that it can recognize one language using QA_1

Since Kleene's Theorem gives the equivalence between the regular grammar and the NFA, we can also use QA_1 to prove that one NFA can recognize one language by transfroming the NFA to the grammar firstly.

Then how to prove that one Turing Machine recognizes one specific language? This QA_2 answer uses contradiction to prove. But it seems informal for me.

Take $$\{0^n 1^n:n\ge 1\}$$ for example. I followed this lecture.

Since there is no non-terminal/terminal symbols for the Turing Machine, it seems inconvenient to construct $$M_i$$ when following QA_1.

So I followed QA_3 answer. It is trivial to prove the Turing Machine in p4 of the above lecture can accept $$\{0^n 1^n:n\ge 1\}$$, but how to prove that it can't accept others?

Both the reference QA_3 answer and QA_4 answer gives one strategy to construct states, but they didn't give one formal proof.

Q:

How to prove the Turing Machine in the above reference lecture recognizes $$\{0^n 1^n:n\ge 1\}$$? Is it impossible to give one formal proof since the halting problem is an unsolvable decision problem?

The halting problem doesn't really tell you anything about whether you can prove that a TM recognises a given language.

We can prove that the TM recognises $$\{0^n1^m : n \geq 1\}$$ using the definition of $$L(M)$$ and $$\mapsto_M$$. One thing to note is that the machine is deterministic, so for each state and character there's at most one transition. Therefore for each input $$w$$ there's only one sequence of IDs (one computation) we need to consider to decide if $$w \in L(M)$$.

These proofs can get very long since there are a lot of cases to consider, so I'll just give a rough sketch.

For simplicity we'll write $$\mapsto$$ instead of $$\mapsto_M$$, note the following:

Lemma 1: $$X^kq_00^nY^k1^m \mapsto^* X^{k + 1}q_00^{n - 1}Y^{k + 1}1^{m - 1}$$ for $$k, n, m \in \mathbb{N}; n,m \geq 1$$ using only states $$q_0, q_1, q_2 \notin F$$.

This can be proven by applying the definitions of $$\mapsto$$ and $$M$$. A corollary of Lemma 1 is that for $$n \geq m$$

$$X^kq_00^nY^k1^m \mapsto^* X^{k + m}q_00^{n - m}Y^{k + m}$$

and for $$m \geq n$$

$$X^kq_00^nY^k1^m \mapsto^* X^{k + n}q_0Y^{k + n}1^{m - n}$$

using only transitions through $$q_0, q_1$$ and $$q_2$$. From this it follows that for all $$n \in \mathbb{N}; n \geq 1$$

$$\underbrace{q_00^n1^n}_{=\ X^0q_00^nY^01^n} \mapsto^* X^nq_0Y^n \mapsto X^nYq_3Y^{n - 1} \mapsto^* X^nY^nq_3B \mapsto X^nY^nBq_4B$$

with $$q_4 \in F$$, so by definition $$0^n1^n \in L(M)$$.

Now assume that $$w \in \Sigma^*; w \notin \{0^n1^n : n \geq 1\}$$, then one of the following cases must be true:

• $$w = \varepsilon$$ or $$w = 1x$$ for $$x \in \Sigma^*$$, then $$M$$ on $$w$$ directly halts in $$q_0 \notin F \Rightarrow w \notin L(M)$$.
• $$w = 0^n$$ for $$n \in \mathbb{N}; n \geq 1$$, then $$q_0w \mapsto Xq_10^{n - 1} \mapsto^* X0^{n - 1}q_1B$$ so the machine halts in $$q_1$$ without ever entering a final state. Thus $$w \notin L(M)$$.
• $$w = 0^n1^m$$ for $$n, m \geq 1; n \neq m$$, if $$n > m$$ then by the corollary of Lemma 1 $$q_0w \mapsto^* X^mq_00^{n - m}Y^m \mapsto^* X^{m + 1}0^{n - m - 1}Y^mq_1B$$ so $$M$$ halts in $$q_1$$ without having entered a final state. If $$m > n$$ then again by Lemma 1 $$q_0w \mapsto^* X^nq_0Y^n1^{m - n} \mapsto^* X^nY^nq_31^{m - n}$$ so $$M$$ halts in $$q_3$$ without having entered a final state. Thus $$w \notin L(M)$$.
• $$w = 0^n1^m0x$$ for $$n, m \geq 1$$ and $$x \in \Sigma^*$$, $$w \notin L(M)$$ can be proven similar to the cases above by considering $$n = m$$, $$n > m$$ and $$m > n$$.

So $$w \in \{0^n1^n : n \geq 1\} \iff w \in L(M)$$, thus $$L(M) = \{0^n1^n : n \geq 1\}$$.

• Thanks for your patient explanation. 1. I add some correction of your answer based on my understanding. Hope the correction isn't wrong. 2. For the last case, I proved as the following hinted by your answer. Hope they are right. 2.1 $n=m$ which is similar to $w = 0^n1^m,m>n$: $$q_0w \mapsto^* X^nq_0Y^n0x \mapsto^* X^n Y^n q_30x$$ 2.2 $m>n$ similar to $w = 0^n1^m,m>n$: $$q_0w \mapsto^* X^nq_0Y^n1^{m - n}0x \mapsto^* X^nY^nq_31^{m - n}0x$$ Commented Mar 8 at 10:06
• 2.3 $n>m$ 2.3.1 $1\not\subseteq x$ we have $$q_0w \mapsto^* X^mq_00^{n - m}Y^m0^k \mapsto^* X^{m + 1}0^{n - m - 1}Y^mq_10^k \mapsto^* X^{m + 1}0^{n - m - 1}Y^m 0^kq_1B$$ 2.3.2 $1\subseteq x$ we have $$q_0w \mapsto^* X^mq_00^{n - m}Y^m0x \mapsto^* X^{m + 1}0^{n - m - 1}Y^mq_10x \mapsto^* X^{m + 1}0^{n - m - 1}Y^m 0^{k'} q_1 1 \mapsto^* X^{m + 1}0^{n - m - 1}Y^m 0^{k'-1}q_2 0Y \mapsto^* X^{m + 1}0^{n - m - 1}Y^{m-1} q_2 Y0^{k'}Y$$ Commented Mar 8 at 10:13
• Hi @An5Drama, thanks for taking the time to review my answer. One thing has me confused though, why would you restrict the lemma to $n \neq m$? It should hold true either way, but it can't be applied to prove $0^n1^n \in L(M)$ using the addition. Commented Mar 8 at 10:22
• Oh ok, maybe my phrasing wasn't great there. What was meant was that during the steps from $X^kq_00^nY^k1^m$ to $X^{k + 1}q_00^{n - 1}Y^{k + 1}1^{m - 1}$ it never enters a final state. It might enter a final state afterwards. Commented Mar 8 at 10:49
• I've changed the phrasing now (and applied your correction in one of the cases, thanks btw), is this better? Commented Mar 8 at 11:05