Turing Machine that deletes a word after accepting it?

Question

I want to make a TM $\text{TM}_{\text{Erase}}$ that given another TM $M$ and a word $w$, will accept iff $M$ accepts it and deletes $w$ from the input line.

My solution was using two symbols ([ and ] for example) that puts [ in the beginning of the movie and ] in the end of the word and when we get to ] we will move the ] one more to the right. Then, if the word is accepted by $M$, $\text{TM}_{\text{Erase}}$ will go the left until encountering [ and then will erase after encountering ], which will erase and return. My problem is how do I prove that $L(\text{TM}_{\text{Erase}})=L(M)$ without it being a headache?

Answer 1

Yes, that'll probably work. Formally proving anything about Turing machines is a headache, because Turing machines are a big headache. There's no way to avoid the headache if you want to fill out all the details in the proof in a detailed and rigorous way.

Generally, theorists have done enough of this that they can see when this is unnecessary. Thus, they skip the headache, when the reduction is obviously correct and the tedious details aren't adding any insight.

Turing machines are like a particularly ugly and tedious programming language. Conceptually, if you can convince yourself that the reduction is "obviously right", we don't bother writing out all the tedious details of a proof of correctness, but let the reader verify for themselves the points that are obvious. This is the same as correctness for an algorithm. When you have some pseudocode for an algorithm and it is obviously correct, we don't bother writing out all the tedious details of a Hoare-logic style proof of correctness -- we just let the reader convince themself it is correct.

It's important to avoid abusing this. Don't do this for anything where correctness is non-obvious. As you practice exercises with writing code, you usually get a good sense of which algorithms are "obviously correct". Similarly, as you practice exercises with Turing machines, you'll usually get a good sense of which reductions are "obviously correct".

Proofs are a form of communication. You should only omit the details where it will be obvious to the reader that the claims are correct, and where it is straightforward for an interested reader to work out the detailed rigorous proof if they care (no insight is needed, only tedious tracking through details). This also suggests that the amount of detail needed is likely to depend on the intended audience of the proof, i.e., the level of people who are likely to read the proof. When you get started in the field, it might be best to write more detailed proofs. Once you get the hang of it, you'll see that there are some parts of proofs that are obvious and boring for everyone, and you'll get a better sense of what needs to be explained in detail and what can be left to the reader to verify.