1
$\begingroup$

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?

$\endgroup$

0

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.