Undecidability of a Formal Language I want to show that the following language is undecidable. Please help me verify the correctness of my solution. Thanks in advance!
\begin{equation}                                                                                                                                                                            
 OVERWRITE_{TM} = \{\langle M\rangle|M \text{ is a TM which writes a blank symbol over a non-blank symbol on any input}\}                                                    
\end{equation}
Intuitively, this problem should be undecidable because, how can we check if this happens in the TMs which do not halt? Anyway, I will give a reduction from:
\begin{equation}                                                                                                                                                                       
  A_{TM} = \{\langle M,w \rangle| M \text{ accepts } w\}                                                                                                                     
\end{equation}
Suppose that $OVERWRITE_{TM}$ is decidable, then let TM $R$ decide this language. Given $\langle M, w\rangle$ we must show that $M$ accepts $w$ iff $M$ writes a blank
symbol over a non-blank symbol an any input. Let us construct a TM $M'$ for this task:
$M' = $ ''on input $x$                                                                             


*

*Simulate $M$ on $w$

*If $M$ accepts $w$ then overwrite a non-blank symbol with a blank symbol.''
This has a potential problem, what if there are no non-blank symbols to overwrite? We can introduce a simple fix to this problem. Namely, take all blank symbols from $M$
and replace them with hash symbols '#.' Now we can guarantee that we can overwrite a non-blank symbol with a blank symbol. Our algorithm to decide $A_{TM}$ is as follows:
$S =$ "on input $\langle M, w\rangle$                                                                                                                                                      


*

*Construct $M'$ to use '#' instead of the blank symbol  

*Run R on input $M'$     

*If R accepts then accept; otherwise reject.''


Questions:


*

*At what level is my solution correct (I at least know that I need to give a reduction from an undecidable language)?

*Feel free to leave any comments or suggestions, there is always room for improvement!

 A: As noted in comments you need to be careful about how you simulate $M$ without overwriting any non-blank symbols -- such as this:
Assume our machines have only two symbols, "blank" and "mark". We can then simulate $M$ with a machine $\hat M$ that never changes "mark to "blank" except if $M$ halts. The trick is to represent $M$'s tape in an appropriate way.
First, since $\mathit{OVERWRITE_{TM}}$ is defined for "on any input", we will construct $\hat M$ such that if it ever discovers that its input tape was non-empty it will halt immediately. We're only interested in its behavior on an empty tape.
Each symbol on $M$'s tape will be represented by a run of marks on $\hat M$'s. A "blank" is represented by an even number of marks, and a "mark" by an odd number of marks (but at least 3); that allows the machine to distinguish between the symbols using only finite state. At each end of the $\hat M$ tape is an isolated mark, which will trigger special processing to extend the tape with a fresh blank when we run into it.
The symbols are separated by runs of blanks that shrink each time we change a symbol. Once one of these spaces becomes to small, we need to get some more working space. One way to do this would be to copy the entire tape to the right of the small space into a new position to the right of the right end marker, with plenty of space (say, 20 blanks) between the symbols. As the "old" symbols are copied, fuse them into the symbol to the left of the small space, taking care to keep it at the right parity. Finally, continue the simulation of $M$ where it left off.
If we make sure to start the copying whenever a gap shrinks to 3 spaces, there will be room to put an isolated mark in the gap, so we can recognize the right place in the tape during the copying phase.
Finally, if $M$ reaches a halting state, let $\hat M$ attempt to overwrite one of the marks that represent the symbol it is looking at with a blank, and then halt.
Then $\hat M$ will overwrite a mark exactly if $M$ halts on the empty tape, which is undecidable.
