It’s fun to think about. What about the Collatz conjecture? If we run it for arbitrary n, on a computer that represents numbers up to n_max, we could know if it will halt within n_max steps. Since only n_max numbers are representable, we could track all visited numbers to detect any cycle that might occur. If on the other hand any iteration would exceed n_max, then the program would halt by crashing.

  hailstone :: Integer -> Integer
  hailstone n
    | n `mod` 2 == 0 = n `div` 2
    | otherwise      = 3 * n + 1
  
  collatz :: Integer -> Bool
  collatz n
    | hailstone n == 1 = True
    | otherwise        = collatz (hailstone n)

Edit: however, you would need enough disk space to store the cycle-detection index.

We have actually done something like that up to the 32bit n_max for sure (but maybe even 64bit?), without any number that would contradict the conjecture.

But yeah, it is not even trivial to say whether it has a bounded max memory, so in case of an arbitrary precision int type, it may not be LBA, but Turing?

I guess I was thinking about indexing the visited numbers from a graph-traversal-algorithm-interview perspective instead of a CS theory one.

We can actually do it in O(1) space complexity in exchange for higher time complexity.

For i in range 1..n, compute n_i, the ith number in the hailstone iteration, and then continue the hailstone iteration n_(i+1)..n_max to see if n_i is equal to any of them. This takes us to quadratic time complexity, O(n * n_max), or constant complexity depending on how you look at it, but it only requires storing a single n_i at a time for cycle detection.

But then again, if you actually loop for n_max iterations without halting by reaching 1 or crashing, then you had to reuse a number somewhere, so the explicit cycle detection isn’t really important.

I have to admit my knowledge of complexity theory doesn’t extend too far, but isn’t the solution to LBAs just.. brute forcing? Also, is it even decidable a priori whether a program is LBA vs requiring a tape that is not only linear function of its input?

The worst case solution is just brute forcing, yes.

An LBA is effectively "just" a Turing machine that has a finite tape.

A typical current computer is an LBA only if you disallow all IO of any sort or bound that IO and include it as part of the system you analyse and so fix the values which will be provided as IO, which of course is a very unusual situation, and so that constraint does not really make the halting problem more tractable in situations we usually care about.

The naive way of deciding it it halts is executing it and keep track of all state between steps. If the machine halts, you're done, if it repeats a state, it's looping.

If you can represent a program with an LBA, it is by definition a context sensitive language and decidable. You could also show it by making a equivalent gramma for the language, that accepts the same input as the program. This gramma must be constructed in a certain way, and then you know it is a context sensitive language.

A machine we have to today in isolation with no form of IO are not general Turing machines, but almost all of them do have that and so if you consider them in isolation rather than the full system (which would include all sources of inputs) the halting problem applies. E.g. code to the effect of "while gets() {}" will either halt or not halt depending on the input, but which isn't decidable without knowing or constraining that input.

We can certainly look for AGI that can do better at deciding the halting of decidable programs, but even for current computers the general halting problem is undecidable without adding artificial constraints.

IO is just state and can be represented on the tape. You can construct a machine for every conceivable input at every time during the execution and reason about them.

"while (gets()) {}" is undecidable because the "tape" is conceptually infinite.

So, no, you can not construct a machine for every conceivable input without imposing an artificial constraint on the input size.

Put another way: For every tape you construct and analyse, there is a tape one segment longer that might contain a symbol that can alter the outcome.

You can, theoretically, keep constructing machines for every input you need. Yes you are bounded, but you can say "this machine will halt for every input it can receive in the next 100 years", because you need to quantify the input in blocks of time.