I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found?
Brainfuck's state consists of an array of integers, an index into that array, a program counter, and some bookkeeping required to track which "[" corresponds to which "]".
Let's assume the array a[:] is zeroed and the index i is set to 0 before the program begins executing.
Then `+` increments the cell in the array a at index i, i.e. `a[i] += 1`; `[` begins a while loop, equivalent to `while a[i] != 0 {`; and `]` ends the while loop: `}` .
So the program `+[]` is equivalent to something like
a := (allocate a length N array of bytes, set to zero)
i := 0
a[i] += 1
while a[i] != 0 {
}
Why is this the shortest?
`]` is the only instruction that might decrease the program counter, otherwise the program counter always increases by one or more. Therefore, a non-halting brainfuck program must include at least one `]`. Brainfuck programs are syntactically incorrect unless there is exactly one `]` occurring somewhere in the program after each `[`. So the shortest non-halting brainfuck program must have at least two instructions.
There is only one syntactically valid brainfuck program with two instructions that might not halt: `[]`. But this will halt, assuming that the array `a` is initialised to zero before execution begins. So the shortest non-halting brainfuck program contains three instructions.
In practice it may not there may not be enough resources to build something to enumerate all the states on all inputs, but we are talking theoretically here. Theoretically, there is no halting problem in a finite world. And we humans live in what looks to be a locally finite world, so it doesn't apply to us.
The halting problem is actually a statement on whether it's possible to always determine if a finite set of rules that have infinite memory will halt on all inputs. The answer is famously no. Thus the halting problem illustrates a property of infinities. It's a subtlety that's rarely mentioned.
It is an interesting property. One thing it says to me is there are things in an infinite world a finite computation machine (like our human brains) will never be able to understand. While locally (say within the Milky Way) we live in a finite world the Universe itself may well be infinite. Ergo, there may be some aspects of the Universe we can never understand, and some things may happen that we can never predict.
You could try defining H to only work on input machines smaller than itself. However there’s still problems.
If you don’t limit input size (aka the I in H(M,I) does machine M halt on input I), your code would still get tricked if M is just a tiny emulator and the input is the whole self defeating H program. So M and I both must be limited.
Anyway that’s not to say a finite H would work even if the input size is limited. You’d have to prove it’s impossible to self recurse - so you’d need good compression.
That’s all assuming self recursion is the only problem with the halt programs. Maybe it’s not, and it seems difficult to rule out other problems and see how they’d affect finitely bound TMs.
I’m just spitballing here. For a while I was infatuated by the idea of snuffing out self recursion or otherwise somehow making a variant of halting programs possible. But self referential poison seems really, really tough to prove the non existence of.
Anyways, I’m of the attitude that the proof for halting problem undecidability is a dumb trick. I’m simply fine with a halting program that doesn’t work correctly in self referential cases. As above though, that just leaves the whole problem vague aka don’t know about other issues and there’s the problem of actually solving it anyways (aka solving all of mathematics at once).
So it's definitely possible to decide halt problem for a bounded computer (any physical computer), it's just not practical in most cases, e.g. amount of memory needed to store graph of all states be bigger than amount of matter in the universe, etc.
The inputs to a halting decider TM is an infinite set (all TMs and all inputs to them) so that’s another reason why a finite graph can’t be represented. Even something like integer addition isn’t a finite graph if you enumerate all inputs
Sure one can say input is coming from a network stream then what? For practical issues then we can limit input size to N bits ... For theoretical issues we can discuss if there is a difference between halting or waiting for more input :)
It's a pretty trivial question in any language, it tends to just be while(true); or similar in that language.
For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).
Just for a short taste, in the lambda calculus the base entity is an abstract function that can be applied to a variable and return a result. You are probably familiar with formulae like `f(x) = x`. In the lambda calculus formalism, this is written as `\lambda x.x`. However, it's important to note that there is no direct equivalent to something like `f(x) = x + 1` - addition or numbers are not a part of the lambda calculus directly. Instead, you can define numbers and then addition in terms of functions and variables.
Instead, the lambda calculus has rules for how function application should work to reduce complex formulae to simpler ones. For example, `(\lambda x.x) y` reduces to `y` [equivalent to f(x) = x; f(y) = ? => y]. Or, `(\lambda x.y) z` reduces to `y` [equivalent to f(x) = y; f(z) = ? => y]. And, if we go on to more complex expressions: `(\lambda x.x) (\lambda x.y) z` reduces to y by applying the reductions above successively (first we reduce the initial expression to `(\lambda x.x) y` then we reduce this to just `y`.
It can be shown that this model of how to reduce the formulae of lambda calculus is in fact equivalent to the model of the Turing machine that can write a symbol on its tape.
- https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...