Formal Proof of Turing Machine

Question

I designed a TM of the following language: {a^n b^n c^n | n E N0} Word of the language: abc, aabbcc, ...

Now I have to make a formal proof that this TM is working.

I understand how this TM works but I do not know how to make a formal proof of this. It would be great if anyone has got a good tip for me.

Answer 1

Proofs of program correctness are notoriously gritty work -- especially for models such as Turing machines where the internals of one part of the computation are not nicely isolated from internals of other parts of it.

Sometimes it turns out to be easier to change the program to something less efficient/elegant in order to support a simple proof.

Generally you'll probably end up with a sequence of lemmas of the shape

If the tape looks like such-and-such and the state is $p_{42}$, then after finite time the machine will end up with tape looking like this-or-that in state $p_{117}$.

where "such-and-such" is a description not of a single concrete tape, but of a whole family of possible tapes that the machine will handle in similar ways.

These lemmas will build on each other for their proof; some of them probably need to be proved by induction over a parameter in the "such-and-such" description. At the end you should have collected enough lemmas that every possible input will match a lemma of the form

If the tape looks like such-and-such and the state is $p_0$, then after finite time the machine will halt and accept (resp. halt and reject).

---

This would produce a reasonably rigorous proof; if you want a "formal proof" in some formal proof system (which I don't think you do, despite your wording), your only hope is probably to turn your rigorous proof into a computer program which generates that formal proof.

Answer 2

Above is a transition table for the machine in question, taken from Kozen's Automata.

WTS that L(M) = A:= $\{a^nb^nc^n| n \geq 0\}$.

Both directions are fairly straightforward, here are pointers for one. Consider any $x \in A$, WTS $x \in L(M)$. The base case with $x = \epsilon$ is clear, so assume that x = $a^nb^nc^n$ for some nonzero n. First, a high level description: M reads over x, ensuring that it is of the proper form. When it reaches the first blank, it writes a $\dashv$. It then replaces the first c it sees with a blank and leaves the rest untouched. It does the same with the first b and corresponding b's, and the same with the first a and corresponding a's. It reaches the $\vdash$ and performs the same operations on the resulting string, and continues until we are left with only blanks between the endmarkers, at which point it accepts. Here is the beginning of such a sequence of valid computations, corresponding exactly to the high level description above.

$(s, \vdash a.....ab.......bc......c\sqcup^{\omega}, 0)$ $(s, \vdash a.....ab.......bc......c\sqcup^{\omega}, 1)$ ... $(s, \vdash a.....ab.......bc......c\sqcup^{\omega}, n)$ $(q_1, \vdash a.....ab.......bc......c\sqcup^{\omega}, n+1)$ ... $(q_1, \vdash a.....ab.......bc......c\sqcup^{\omega}, 2n)$ $(q_2, \vdash a.....ab.......bc......c\sqcup^{\omega}, 2n+1)$ ... $(q_2, \vdash a.....ab.......bc......c\sqcup^{\omega}, 3n+1)$ $(q_3, \vdash a.....ab.......bc......c \dashv \sqcup^{\omega}, 3n)$ ...

Can you first show that M has the above configurations after consuming $a^n, b^n$, and $c^n$ characters respectively? (hint: induction)