37
$\begingroup$

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?

$\endgroup$
5
  • 7
    $\begingroup$ Very related question. Community votes, please: duplicate? $\endgroup$
    – Raphael
    Commented Jun 7, 2016 at 6:59
  • 3
    $\begingroup$ See also What is the smallest Turing machine where it is unknown if it halts or not? $\endgroup$
    – OrangeDog
    Commented Jun 7, 2016 at 11:17
  • 6
    $\begingroup$ You are missing a key detail: you have not specified what language the program must be written in. Your example uses binary lambda calculus -- is that the only language you are interested in? We can see it is trivial to develop a 1 bit program that has unknown halting status, simply by embedding the body of the algorithm directly into the language itself. It's a loophole, but one you have to pay attention to when asking for golf solutions. They love their loopholes! Kolmogov complexity may be an important topic to explore here. $\endgroup$
    – Cort Ammon
    Commented Jun 7, 2016 at 15:27
  • $\begingroup$ @CortAmmon an 1 bit program that has unknown halting status? Pardon, I don't get what you mean. The BLC doesn't even accept 1 bit strings as valid programs. Yes, the λ-calculus is the only language I'm interested in, but I realized there are too few people that care about it to make it worth making a thread, so I gave up. $\endgroup$
    – MaiaVictor
    Commented Jun 7, 2016 at 18:24
  • 1
    $\begingroup$ @srvm If you are only interested in $\lambda$-calculus you should have explicitly said that. You did not tag your question with the $\lambda$-calculus tag, nor did you say that you weren't interested in other languages. $\endgroup$
    – Bakuriu
    Commented Jun 8, 2016 at 7:51

3 Answers 3

7
$\begingroup$

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

For the blank tape input only:

The best overview of "unproven small machines which are likely hard" is: https://wiki.bbchallenge.org/wiki/Cryptids maintained by the "The Busy Beaver Challenge" (bbchallenge). https://bbchallenge.org/story#skelets-43-undecided-machines is another good similar summary by the same project.

As of 2023 the bbchallenge was 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 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!

On June 2024,a hard looking "Collataz-like" 6-state halting problem was found. The associated machine was named "Antihydra" and is described at: https://wiki.bbchallenge.org/wiki/Antihydra

Another 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.

Here's a [GMP](Here's a GMP simulation of the equivalent antihydra problem with some performance diagnostics added: ) simulation of the equivalent antihydra problem with some performance diagnostics added:

antihydra.c

#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>
#include <time.h>

#include <gmp.h>

static uint64_t get_milis(void) {
    struct timespec ts;
    timespec_get(&ts, TIME_UTC);
    return (uint64_t)(ts.tv_sec * 1000 + ts.tv_nsec/1000000);
}

int main(int argc, char **argv) {
    char *as, *bs;
    mpz_t a, aq, ar, b;
    uint64_t i, time, newtime;

    /* CLI and init. */
    if (argc > 1) {
        as = argv[1];
    } else {
        as = "8";
    }
    if (argc > 2) {
        bs = argv[2];
    } else {
        bs = "0";
    }
    mpz_init_set_str(a, as, 10);
    mpz_init_set_str(b, bs, 10);
    mpz_init(aq);
    mpz_init(ar);
    i = 0;
    time = get_milis();

    /* Run. */
    while (1) {
        /* aq = a / 2
         * ar = a % 2 */
        mpz_fdiv_qr_ui(aq, ar, a, 2);
        if (
            /* odd */
            mpz_cmp_ui(ar, 0)
        ) {
            /* b == 0 */
            if (!mpz_cmp_ui(b, 0)) break;
            /* a = aq * 3 + 1 */
            mpz_mul_ui(a, aq, 3);
            mpz_add_ui(a, a, 1);
            /* b -= 1 */
            mpz_sub_ui(b, b, 1);
        } else {
            /* a = aq * 3 */
            mpz_mul_ui(a, aq, 3);
            /* b += 2 */
            mpz_add_ui(b, b, 2);
        }
        i++;
        if (i % 100000 == 0) {
            newtime = get_milis();
            gmp_printf("%" PRIu64 " ms=%" PRIu64 " log10(a)=%ju log10(b)=%ju\n",
                       i/100000, newtime - time, mpz_sizeinbase(a, 10), mpz_sizeinbase(b, 10));
            time = newtime;
        }
    }

    /* Cleanup if we ever reach it. */
    mpz_clear(a);
    mpz_clear(aq);
    mpz_clear(ar);
    mpz_clear(b);
    return 0;
}

Compile and run:

gcc -ggdb3 -O2 -pedantic-errors -std=c11 -Wall -Wextra -o 'antihydra.out' 'antihydra.c' -lgmp
./antihydra.out

Tested on Tested on GMP 6.3.0, Ubuntu 24.04.

"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:

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
  • BB(5, 2) was settled by the Busy Beaver Challenge project, actual Collatz-like is at BB(6, 2)

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).

$\endgroup$
34
$\begingroup$

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
$\endgroup$
3
  • $\begingroup$ The bottom of the page says: $Date: 2007/11/03, then how it is 26 year old? $\endgroup$
    – Falaque
    Commented Jun 8, 2016 at 6:56
  • 1
    $\begingroup$ @Falaque The top of the page states "This page is the author's HTML rewrite of ... February 1990". The text is 26 years old, the rendition into HTML is from (or last updated) in 2007. $\endgroup$
    – IMSoP
    Commented Jun 8, 2016 at 9:03
  • $\begingroup$ All 5 state machines were now proven in Coq in 2024: quantamagazine.org/… There is a 6 state machine which may be hard: cs.stackexchange.com/a/162108/10517 $\endgroup$ Commented Jul 10 at 7:50
5
$\begingroup$

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).

$\endgroup$
8
  • 1
    $\begingroup$ I think you mean to write input > 1 instead of input >= 1? As it stands now, this program will loop $1\rightarrow 4 \rightarrow 2 \rightarrow 1$ $\endgroup$ Commented Jun 7, 2016 at 11:37
  • $\begingroup$ You are right, I wanted to put a >, however as long as we don't have a proof for halt-ness with > we can't be sure we will reach the 1 -> 4 -> 2 -> 1 loop (in example if it don't terminate for > it don't reach >=) $\endgroup$ Commented Jun 7, 2016 at 12:36
  • 1
    $\begingroup$ A proof your program with $>=$ does not halt: Suppose the Collatz conjecture is true, then we reach the loop $1421$ on all inputs. Otherwise, if it is false, then we reach the loop $1421$ on some inputs, and on other inputs the sequence either loops elsewhere or else it diverges into infinity (and therefore loops forever). In either scenario, the program with $>=$ never halts, independent of whether Collatz' conjecture is true or not. The program with $>$ halts on all inputs iff the Collatz conjecture is true, which is unresolved. $\endgroup$ Commented Jun 7, 2016 at 12:44
  • 2
    $\begingroup$ There is a much simpler proof that the second program does not halt, which does not invoke the Collatz theorem as a conditional result. The program halts when $n<1$. But neither of the two cases will effect that. If $n=1$, then $n$ becomes $4$. If $n>1$, then $n$ becomes some other number greater than or equal to $1$. In any case, it never goes below $1$, which is necessary to terminate the loop. I do not understand your last comment. $\endgroup$ Commented Jun 7, 2016 at 12:51
  • 1
    $\begingroup$ That's true :) You're right, I should have added 'iff the Collatz conjecture is true' to my first comment. I see your edit, very good. You do not need the second program, because the conjecture 'this program never enters the same state twice' is also unresolved of the first program: it is possible there is a number which does not diverge off into infinity, but instead gets stuck in a large loop somewhere up in very high numbers. $\endgroup$ Commented Jun 7, 2016 at 12:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.