Certificates of Nonhalting
I was reading a paper on Busy Beavers that introduces the notion of “Christmas tree recurrence” when it hit me that the concepts I discusses in the last post about “dynamical halting” are actually meant to describe Turing Machines that _don't_ halt. That is, the actual motivation for the concepts is exactly the opposite of the one I was talking about, and I believe this complicated matters. Those Turing Machines that we discussed _do_ get to a point of “dynamical halting” – it's just that that is an _a posteriori_ observation on the behaviour of machines that – and this is essential – _provably_ don't halt.
Sumarizing: machines that are ammenable to analysis exibit predictable behavior. Duh. But that's not so obvious – I mean, it's a single step in reasoning, but it's still a step. The interesting point is that the difference between halting and non-halting is _not_, as you'd have though from the definitions, as straigh-forward as yes--no. It's a lattice-work of predictability.
So, this leads to a simpler formalism. Suppose we have some logic to reason about Turing Machines; and suppose that logic's language allows us to express the notion of _halting_. Denote it by `H(m)`, for a machine `m`. Also, we require basic logical notions found in predicate logic ( a suitable type theory) – conjunction, disjunction, quantification, implication, _etc_.
Then, the notions we introduced before (those of quasihalting and Lin recurrence) _imply_ that the machine doesn't halt – _i.e._, `¬H(m)`. So, let us call a **certificate of non-halting**, non-halting certificate, any predicate `P` on Turing Machines that satisfies
∀m P(m) → ¬H(m)
What is the structure of the set of non-halting certificates?
Well, the first obvious observation is that it has a preorder relation given by the implication. I mean, say `P ⇒ Q` if
∀m P(m) → Q(m)
Then a non-halting certificate is one `P` for which `P ⇒ ¬H`. And, as you may verify, `⇒` is transitive and reflexive. If we quocient by equivalence, we have a partial order. Indeed, it is the subposet of subobjects of the type of Turing Machines which are smaller than `¬H`, in a suitable category.
If you don't know what that means, it doesn't matter. What matters is that there are operations `∧` and `∨` that behave the way you expect in relation to `⇒`. There's even a kind of negation – – but I suspect that is not that interesting.
So the set of non-halting certificates is a sort of algebra. What else? Indeed, there is a top element: `¬H` itself. There's even a bottom element: the constantly false predicate `F`. That algebra is a lattice.
What properties does it have as a lattice? I can think of some questions.
- Does it have atoms maximals?
- What are its ideals and filters?
- Is it decomposible into products of other lattices?
- Is it complete?
But there's one more layer to this. Not all certificates are the same: `H` itself is semidecidable, only, making `¬H` co-semidecidable. There are some certificates that are even undecidable, and furthermore, undecidable relative to the Halting Problem! One example is quasihalting, evidently.
So what if we restrict our attention to the semidecidable, decidable, even Halting Problem-reducible ones? Which Turing degrees are present in this space? What are the answers to those lattice questions for these? Can we know all of the decidable certificates?
The undecidability of the Halting problem is interesting, particularly, because it shows us not only that we can't decide if an arbitrary machine halts, there are machines for which there is no proof that it doesn't halt! (if it does, then obviously there is proof). If there weren't such machines, we could enumerate all proofs until we find one that any machine in question halts not.
How does this impact the lattice?
---
Why is this interesting? For multiple reasons, but my motivation to investigate such matters is practical. In order to implement a program that simulates Turing Machines but _stops_ if it can decide that machine doesn't halt, it's worth understanding a bit more about the structure surrounding machines that can be proved not to halt. More precisely, what is the best way to detect non-halting turing machines? What sorts of recurrence can we exploit?
I'll try to write about this things in the future.