Curious how difficult it would be to write a formal proof of non-halting for an individual machine, I decided to give it a go. I picked Skelet #34 and formalized the proof on @sligocki’s blog.
You can find my Coq proof here – the parts of interest will probably be the definition of the TM, and the final non-halting theorem.
Formal proofs have the tendency to expose small gaps in handwritten proofs, though rarely compromising the big ideas of the argument. This one was no different.
First, in the proof of Lemma 10:
I leave this proof as an exercise to the reader. We have already proven the case of
a = 1in the Counter Phase section. The proof fora = 0is very similar.
In fact, Counter Phase makes use of the a = 0 case, and it is a = 1 we must carefully consider.
Secondly, the proof of Corollary 11 isn’t valid as written:
Lemma 10: If
b(m) > 1andb(n) > 1, thenL(n) <C 101a R(m) -> L(n+1) <C 101a R(m+1)for anyain{0, 1}.Corollary 11: For all
k,ain{0, 1}, andmsuch thatb(m) > 2^k - 1, then0000^k <C 101a R(m) -> 1000^k <C 101a R(t)wheret = m + 2^k - 1.This follows directly from Lemma 10 when you note that the condition
b(m) > 2^k - 1assures that you can apply Lemma 102^k - 1times.
The general idea is that L(0) = 0000^k, and so we count in binary until we reach 2^k - 1. Except, Lemma 10 requires that b(n) > 1, i.e. that we don’t cross a power-of-two boundary. And we are crossing many such boundaries!
In fact, if you take a closer look, you’ll notice that in fact L(0) is not 0000^k, but the empty string. Corollary 11 would be valid as written when surrounded by empty tape on both sides, but that is not the context in which it is used.
If you did the exercise left to the reader in the proof of Lemma 10, you might wonder why the assumption of b(n) > 1 is even there – it is a bit subtle (I got confused by this at first), but for a rewrite rule like this to make sense, both sides need to have the same length – and that won’t be the case if we cross a power-of-two boundary.
The problem can be fixed by defining L_k(n), which is the k-bit, fixed-width counter:
L_0(0) = empty string
L_{k + 1}(2*n) = L_k(n) 0000
L_{k + 1}(2*n+1) = L_k(n) 1000
Having proven Skelet #34, we also get Skelet #35 for free – the same proof Just Works if we change the definition of the TM, as the only details that change are the ones that have been automated away with Coq tactics.
All this took quite some effort, mostly because the problem domain creates opportunities to use all three of Coq’s natural number types – nat, positive and N. The interactions can be gnarly.
This is to say that for now I’ll probably work on formally-verified deciders, as that just seems more pleasant, but I’m open to suggestions of what other machines would most benefit from a similar proof – i.e. which ones are least likely to be solved by a decider in the end.
