What are very short programs with unknown halting status?

Question

This 579-bit program in the Binary Lambda Calculus has unknown halting status:

01001001000100010001000101100111101111001110010101000001110011101000000111001110
10010000011100111010000001110011101000000111001110100000000111000011100111110100
00101011000000000010111011100101011111000000111001011111101101011010000000100000
10000001011100000000001110010101010101010111100000011100101010110000000001110000
00000111100000000011110000000001100001010101100000001110000000110000000100000001
00000000010010111110111100000010101111110000001100000011100111110000101101101110
00110000101100010111001011111011110000001110010111111000011110011110011110101000
0010110101000011010

That is, it is not known whether this program terminates or not. In order to determine it, you must solve the Collatz conjecture - or, at least, for all numbers up to 2^256. On this repository there is a complete explanation of how this program was obtained.

Are there (much) shorter BLC programs that also have unknown halting status?

Answer 1

Yes. ​ This page says there are 98 5-state Turing machines whose halting statuses are unknown. ​ Annoyingly, it does not give any examples of such machines, but this 26-year-old page gives 2 5-state Turing machines whose halting statuses were apparently unknown at that time. ​ (Searching for "simple counter" will take you right between those 2.) ​ I copied them here in case that link goes down:

Input Bit   Transition on State     Steps            Comment
             A   B   C   D   E

    0       B1L C1R D0R A1L H1L   > 2*(10^9)       ``chaotic''
    1       B1R E0L A0L D0R C0L

    0       B1L A0R C0R E1L B0L       ?        complex ``counter''
    1       A1R C0L D1L A0R H1L

Answer 2

Collatz conjecture:

The following program always halts:

void function( ArbitraryInteger input){
     while( input > 1){
            if(input % 2 == 0)
                input /= 2;
            else
                input = (input*3) + 1;
     }

     // Halt here
}

Slight variation (still a conjecture, because it's based on a result from Collatz's one):

For some input the following program will never enter the same state twice (where the state is determined by the value held by "input"):

void function( ArbitraryInteger input){
     while( input >= 1){ // notice the "="
            if(input % 2 == 0)
                input /= 2;
            else
                input = (input*3) + 1;
     }
}

Note that the second program never halts, regardless of whether the first program halts or not.

It is believed that the first program always terminates for any input, however, we don't have the proof of that, and there may still exist some integer for which the program don't halt (there's also a $100 prize for proving it).

The second program is interesting too: it states that the program will never enter the same state twice for some input, which basically requires the first program to have a sequence known to diverge without repeating. It does not only require the Collatz conjecture to be false, but it requires it to be false and without loops, apart from the obvious 1,4,2,1 loop.

• If Collatz has only looping counter-examples the variation on the conjecture is false

• If Collatz is false without loops, the variation on the conjecture is true

• If Collatz is true, the variation is false

• If Collatz is false both because it has loops and because it has a number for which it diverges, the variation on the conjecture is true (it just requires a number for which it diverges without entering a loop)

I think the variation is more interesting (not just because I found it by accident and noticed it thanks to @LieuweVinkhuijzen), but because it actually requires a real proof. By brute forcing, we may be able to find a loop one day or another (and that will be a loop longer than 70 numbers: current state of the art is that there can't infinite loops shorter than 68 or so), and brute forcing is not interesting: it is just number crunching. However we cannot brute-force an infinite divergent sequence, we don't know if it will really end without a real proof.

EDIT: I skipped the part about Collatz Conjecture sorry, I genuinely answered by heart with an algorithm I read about some years ago, I didn't expect that was already mentioned.

EDIT2: A comment made me notice I wrote the algorithm with a mistake, however, that mistake indeed makes my answer different from Collatz conjecture (but a direct variation of it).

Answer 3

Overview of Turing Machine decidability starting on the a blank tape (Busy Beaver style)

For the blank tape input only:

• 4-state machines: all decided in 1983
• 5-state machines: as of 2023 it is generally believed that all 5-state machines have been decided pending only better verification and perhaps boring proofs analogous to other existing proofs
• 6-state machines: might quite possibly remain forever open however, see the BB(6) section below

The best overview of "lists of unproven machines" by various sources currently is this page from the "The Busy Beaver Challenge" (bbchallenge): https://bbchallenge.org/story#skelets-43-undecided-machines As of 2023 The bbchallenge is the most visible ongoing project to calculate BB(5), the Busy Beaver "shift" function of 5 AKA s(5) in some older literature, which counts how many steps a Turing machine runs for on a tape full of 0's before halting. Non-halting ones are excluded. So calculating BB(5) implies solving the halting problem for every single Turing machine with 5 states.

As highlighted by the bbchallenge, it also depends a lot on what you consider "verified", ranging from manual proof, to unverified programmatic checks, to formal proofs.

One of the major features of the bbchallenge are deciders. Deciders are programs that attempt to decide if a large number of Turing machines halt or not. But note that all deciders seem to be parameterized with "search depth like parameters", so it is not easy to be sure if more would be solved with larger parameters and more computational time. And in is a notable example of that some rare cases, time can get ridiculously large, requiring more advanced/specialized techniques in practice for proving specific machines, Skelet #1 below.

Back in 2003, Skelet produced a list of only 43 machines that he was not able to decide with a large formally unverified Pascal decider program, plus a few manual proofs. That list has generally considered to contain some of the "most likely unproven/hardest to prove ones".

Then more recently and independently, bbproject contributors also managed to decide all machines except 34 with deciders, but with much better review/verification procedures: https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/3

So it is interesting to see that both approaches found about ~30-40 machines that were not "easily" automatically provable and required manual proofs. This is of course where the gold lies, as these non-automatable machines are the ones most likely to represent "complex theorems worthy of mathematician's brain time", see also: ""Real" open conjectures reduced to Turing Machines below."

If these are worth a mathematician's brain time or not, is another story. Some of the machines appear to require computational + brain approaches, e.g. Skelet #1, which while epic, might not hold that much insight into Life, the Universe and Everything. Some however will hold deeper meaning of course.

Skelet's 43 holdouts

Skelet's holdouts were initially published at: https://skelet.ludost.net/bb/nreg.html

Dan Briggs manage to prove some of Skelet's 43 never halt circa 2021: https://github.com/danbriggs/Turing/blob/master/paper/HNRs.pdf

The BB challenge also solved some with their own deciders: https://bbchallenge.org/skelet

The "individual machines" section of the bbchalenge Discuss is likely best way to find an publish state of the art, it is basically the "Journal of BB(5) Research" if you will! https://discuss.bbchallenge.org/c/individual-machines/7 Some early movements occasionally also happen on Discord, go figure: https://discord.com/channels/960643023006490684/1026577255754903572 Notably, #1 and #34 also fell:

• #1 https://www.sligocki.com/2023/03/13/skelet-1-infinite.html | https://discuss.bbchallenge.org/t/skelet-1-is-a-translated-cycler-coq-agrees/166
• https://www.sligocki.com/2023/02/02/skelet-34.html

#1 was particularly epic, a shifted cycle with cycle of about ~8 billion steps.

It seems likely that the bbproject managed to resolve all of the holdouts as mentioned at: http://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/4?u=cirosantilli and surrounding posts.

BB(6)

It currently looks like will likely never know BB(6). Or it would require a CERN-like mega-project, or AGI. Therefore if you are looking for some small Turing machines to prove, going through BB(6) one a time, trying every known decider on it, and failing that going for manual proof seems like a good approach!

A good argument we think BB(6) might never be known is that $BB(6) \ge 10 \uparrow \uparrow 15$, overview: https://www.sligocki.com/2022/06/21/bb-6-2-t15.html (Pavel Kropitz, 2022) i.e. Pavel came up with a machine he managed to prove halts after that time/many 1's written.

Therefore, if there are any BB(6) holdouts that take nearly as much computation time to decide, we might really never solve them. Compare that e.g. to BB(5), where the current champion halts after ~47 million steps, but where Skelet #1 has a cycle of the order of billions.

"Real" open conjectures reduced to Turing Machines

Some mathematical problems can be reduced to deciding the halting problem of a specific Turing machine. The best example of this is perhaps Goldbach conjecture, where it is obvious how you can make a Turing machine that just walks every positive number one by one, tries every possible pair of smaller numbers that sum up to it, and checks if they are prime. Then it halts if no valid pair is found for a number, or continues to infinity otherwise.

Such Turing machines serve therefore as examples of "known hard to prove problems". Going down that route also allows to show that certain Turing machines are undecidable in a certain proof system, e.g. ZF. This is done by modelling the logic system itself with a Turing machine.

https://bbchallenge.org/story#what-is-known-about-bb is the best list available as of 2023:

• BB(15) is at least as hard as Erdős' conjecture on powers of 2: "for n > 8, there is at least one digit 2 in the base-3 representation of 2n". [Stérin and Woods, 2021]
• BB(27) is at least as hard as Goldbach conjecture: “for n > 2, every even integer is the sum of two primes” unverified construction [Aaronson, 2020]
• BB(744) is at least as hard as Riemann Hypothesis [Matiyasevich and O’Rear and Aaronson, unpublished]
• BB(748) is independent of ZF [O’Rear, unpublished]
• BB(5,372) is at least as hard as Riemann Hypothesis [Yedidia and Aaronson, 2016]
• BB(7, 910) is independent of ZFC [Yedidia and Aaronson, 2016]

Most/all of these proofs involved compiling down simple programming languages to Turing machines programmatically, see also: Compiler that compiles to a Turing machine?

It is worth noting however that not all mathematical problems can be directly reduced to a "simpler halting problem" (that does not directly involve proving another Halting problem). E.g. this is not the case for Collatz conjecture, as a counterexample would go off to infinity and you wouldn't be able to tell: https://mathoverflow.net/questions/309044/is-there-a-known-turing-machine-which-halts-if-and-only-if-the-collatz-conjectur Goldbach is fundamentally different from Collatz in that you can just try every smaller number and be done for each integer.

Some real cool but mostly philosophical aspects of such reductions are:

• they allow us to estimate how hard a conjecture might be to prove: the more states in the Turing machine the harder
• they might allow for automated proofs to be carried out via deciders. In this way, they can be seen as a sort of "normal form" for large chunks of mathematics, much like 3SAT is a kind of normal form for NP.

Blank tapes vs arbitrary tapes

As highlighted by Marzio, the question of "decide every N-state Turing machine for every possible input" has already reached the wall basically:

• 3 states: decidable
• 4 states: unknown believed to be decidable
• 5 states: a Collatz-like problem
• 10 states: Collatz itself
• 15 states: Turing machine simulation (Universal Turing machine)

These numbers were extracted from the following answers which give their references:

• https://cstheory.stackexchange.com/questions/10207/whats-the-simplest-noncontroversial-2-state-universal-turing-machine/10390#10390
• https://cstheory.stackexchange.com/questions/11611/what-is-the-nearest-problem-to-the-collatz-conjecture-that-has-been-successful/11614#11614

Also note that the second image is already outdated as we have a 15-state universal machine as per first image, just it simulates slower than the previously known 19-state one.

While those could potentially be reduced slightly if an even smaller machine is found, we are already basically bricked at 5 states in terms of what we can prove.

This is what makes the blank-tape only problem more compelling to me. It is fundamentally simpler, as we don't have to consider infinitely many inputs for each machine: one machine, one input, can I decide it.

As a result, we get to zoom in much more, and the boundary between decidable, hard maths problem and undecidable has humongous gaps that beg to be improved. Notably, given that we got away with only 30-40 manual proofs for BB(5), it is not clear if BB(6) will present fundamentally hard maths problems or not. What about BB(7)? And so on. Because now we are at BB(15), which is a monumental gap away from BB(5).