Following section 8 of Equational Logic by George McNulty, I understand the approach of reducing this decision to the halting problem by modelling Turing machines with equational theories. The construction is as follows:

Let $M$ be a Turing machine with instructions of the form $(a,b,q,r,D)$, where $a$ is the letter read by $M$, $b$ is what will replace the letter on the tape (namely $a$), $q$ is the current state, $r$ is the new state, and D is the direction the head moves along the tape (either $R$ or $L$). We can then build a theory $\Sigma$ by, for each letter $c$ in our alphabet, adding in the equation

$$F_cG_qF_ax = G_rF_cF_bx$$

for each instruction $(a,b,q,r,L)$, and

$$F_cG_qF_ax = F_cF_bG_rx$$

for each instruction $(a,b,q,r,R)$.

Note that $F_x$ and $G_y$ are simply unary operators. We also introduce unary operators H to represent the point beyond which the tape is blank, and J to represent the halting state.

Equipped with this construction, it is clear that every Turing machine computation details a proof in our theory. This tells us that if $M$ halts, then

$$\Sigma_M \vdash HG_{q_0}Hx = HJHx,$$

where $q_0$ is the initial state, and we assume we are launching $M$ on the blank tape.

On the other hand, if we could show that $\Sigma_M \vdash HG_(q_0)Hx = HJHx$ implies that $M$ halts then we would be done. This is the direction I don't understand. I am having trouble following McNulty's proof.

We do know that if $\Sigma_M \vdash HG_{q_0}Hx = HJHx$, then there is a proof of this from our theory because equational logic is complete. Naively, one might think that this proof gives us exactly the steps $M$ will take when launched on the blank tape. If the proof is essentially just a list of axioms, then this would be true. But what if the proof uses other rules and is more complex? I am willing to believe that one could still extract the sequence of steps the turing machine will take, but how?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.