[Animats]

That's correct. With determinism and finite memory, you must eventually either repeat a previous state, or halt.

This is useful. Verifiers which work by symbolic execution examine large numbers of cases they work through the control flow. Each case can contain a large number of states; you only need one case for each control flow pattern. Now, some programs run into combinatorial explosion when you do that. The number of cases to be examined grows rapidly. That means halting detection is NP-hard, not impossible. There's a difference.

The Microsoft Static Driver Verifier operates on the assumption that if symbolic execution doesn't terminate after a reasonable amount of automatic analysis, your driver doesn't get to run in the kernel. This is a good, practical solution.

[andreareina]

Checking my understanding: Are you saying that the halting problem is computable (if still completely infeasible in general) for all finite deterministic machines, and that the uncomputability of the busy beaver sequence[1] is due to the infinite memory of Turing machines even though the busy beavers themselves are finite?

ETA: wait that doesn't make sense because it's equivalent to computing the busy beaver number for the program under consideration. What am I missing?

[1] I'm aware there's no unique BB sequence, I don't know that the rigorous phrasing is.

[Animats]

Checking my understanding: Are you saying that the halting problem is computable (if still completely infeasible in general) for all finite deterministic machines

Yes. There's even a practical way to check if a finite deterministic machine has repeated a previous state. Run two of them in parallel, in lockstep so that one takes two steps while the other takes one. If they ever have identical state, they're in a loop. This takes 1.5x the compute power plus 2x as much memory, so it's far cheaper than storing all previous states.

(Some early mainframe era educational interpreter supposedly did this, to stop simple student infinite loops quickly in a batch system.)

Here's a paper on the busy beaver problem which discusses upper bounds.[1] The key here is that the upper bound on states is not computable. However, if you force an upper bound by limiting memory, it becomes computable. But really hard. That paper discusses how very rapidly the number of states grows for that problem.

[1] https://homepages.hass.rpi.edu/heuveb/Teaching/Logic/CompLog...

[andreareina]

I see! I didn't make the connection that bounding the memory necessarily bounds the number of steps as well. Obvious in hindsight.