[Decider] Backward reasoning

Backward reasoning: principle

This decider is not related to a specific family of the zoology.

We take the same idea of “Backward reasoning” as in Heiner Marxen - Attacking the Busy Beaver 5.

We can afford to run the decider on depth 300 (instead of 5 in Heiner Marxen - Attacking the Busy Beaver 5) thanks to having more computing power and the relatively small subset of machines on which it was run.

Click on the image below for more details about the technique:

More at https://github.com/bbchallenge/bbchallenge-proofs/blob/main/deciders/correctness-deciders.pdf.

Decider examples and counterexamples

Decider code


Decider tests



Decider correctness

Proof available at https://github.com/bbchallenge/bbchallenge-proofs/blob/main/deciders/correctness-deciders.pdf.

@atticuscull, @pg132, @DunDunDunDone, and @modderme123 have found a bug in the current implementation of this decider: Backtracking Bug · Issue #1 · bbchallenge/bbchallenge-deciders · GitHub

Hence it is back to work in progress! The machines have been removed of the undecided index.

I wrote some python code that implements backward reasoning. It uses a breadth first approach instead of the depth first approach that the current code uses. I’m not sure if there is an advantage either way - perhaps the depth first approach is better optimized for space by limiting the tree depth as opposed to the number of steps you run it for, which is what the current code does.

Anyway, here is my code:

# Single instance of a state transition, i.e. 1LB
class Transition:
    def __init__(self, write=None, direction=None, state=None):
        if direction is not None and direction != "?":
            self.direction = direction
            self.write = write
            self.state = state
            self.direction, self.write, self.state = (None,)*3

# Just a wrapper class for a state table essentially
class TuringMachine:
    def __init__(self, states, state_table):
        # list of states
        self.states = states
        # A dictionary containing transitions
        self.state_table = state_table
        # What state + bit combinations directly precede that state
        self.predecessors = {s: set() for s in states}
        # None is the halting state
        self.predecessors[None] = set()
        for s in states:
            zero, one = state_table[s]
            self.predecessors[zero.state].add("0" + s)
            self.predecessors[one.state].add("1" + s)

    def get_predecessors(self, state):
        return self.predecessors[state]

# Storing a tape along with the head and current state
class Configuration:
    def __init__(self, tape, state, head):
        self.state = state
        self.tape = tape
        self.head = head

    def __str__(self):
        tape = list(" " + "  ".join(list(self.tape)) + " ")
        tape[3 * self.head] = "["
        tape[3 * self.head + 2] = "]"
        return self.state + ":  " + "".join(tape)

def breadth_first_backtrack(turing_machine, step_limit):
    # Which configuration should we backtrack from first
    process_order = Queue()
    # Which configurations have we seen already
    discovered_configs = set()

    # Add all the halting configurations to the process,
    # seeding the search process
    for halt_pred in turing_machine.get_predecessors(None):
        config = Configuration(halt_pred[0], halt_pred[1:], 0)

    steps = 0
    # While there are still branches that aren't contradicitons,
    # and while we haven't ran the search for the search limit,
    # process the next leaf
    while (not process_order.is_empty()) and steps < step_limit:
        steps += 1
        config = process_order.dequeue()
        possible_preds = turing_machine.get_predecessors(config.state)
        for pred in possible_preds:
            transition = turing_machine.state_table[pred[1:]][int(pred[0])]
            write = transition.write
            direction = transition.direction
            # If we're at the left of the tape, add to the left
            # R corresponds to left because we are going backwards
            if config.head == 0 and direction == "R":
                new_config = Configuration(pred[0] + config.tape, pred[1:], 0)
            # If we're at the right of the tape, add to the right
            elif config.head == len(config.tape) - 1 and direction == "L":
                new_config = Configuration(config.tape + pred[0], pred[1:],
                                           config.head + 1)
            # Checking that config.tape[config.head - 1] == write makes sure
            # that after transitioning from that state, the bit we write
            # agrees with the tape what we currently have
            elif direction == "R" and config.tape[config.head - 1] == write:
                new_tape = list(config.tape)
                new_tape[config.head - 1] = pred[0]
                new_tape = "".join(new_tape)
                new_config = Configuration(new_tape, pred[1:], config.head - 1)
            elif direction == "L" and config.tape[config.head + 1] == write:
                new_tape = list(config.tape)
                new_tape[config.head + 1] = pred[0]
                new_tape = "".join(new_tape)
                new_config = Configuration(new_tape, pred[1:], config.head + 1)
                # If the the transition does not agree with the proposed path
                # towards halting, move on to the next possible predecessor
            # If we have not seen this configuration before, add it to the
            # set of open branches to search
            if new_config not in discovered_configs:

    # If there is nothing more to process then we know the while loop broke
    # because all of the branches lead to contradictions.
    if process_order.is_empty():
        return "contradiction"
    # Otherwise, the while loop broke because of the step limit
    return "no contradiction found in " + str(step_limit) + " steps"

STATES = ["A", "B", "C", "D", "E"]

def check_from_data(data_string, step_limit=1000):
    # Convert the string into a state table
    ST = {STATES[i//6]: [Transition(*data_string[i + j: i + j + 3])
          for j in [0, 3]] for i in range(0, 30, 6)}

    TM = TuringMachine(STATES, ST)

    print(breadth_first_backtrack(TM, step_limit))

check_from_data("1RB0LD1LC0RE???1LD1LA1LD1RA0RA")   # 55897188
check_from_data("1RB???1LC???0LD0LC1RD0RE1LB0RE")   # 27879939
check_from_data("1RB???1LC0RB1LD0LC0LE1RE0RA1RB")   # 2713328
check_from_data("1RB1LC1RC1RB1RD0LE1LA1LD???0LA")   # BB5 Champion

Thank you very much and welcome to the forum :slight_smile:

I will dive in your code as soon as I get a chance. If you have time would you mind writing, in plain English, a small argument of why your code is correct?

On a side note, I like your compact strings such as 1RB0LD1LC0RE???1LD1LA1LD1RA0RA for machine representations. It’s probably better and more straightforward than the current base-64 representation.

The only annoyance is that ? is not URL safe… We could consider getting rid of base-64 representation for something like the strings you use. I opened a discussion on that point on github: Get rid of base-64 representations for something simpler? · Issue #6 · bbchallenge/bbchallenge · GitHub

I believe this algorithm has a flaw…

First, it will return invalid results for machines that use the starting state of A with tape head 0. (I realize that any machine that halts within 1000 steps would’ve already been ruled out by the seed, but this might be worth noting.) For example, consider ??????1LC0RB1LD0LC0LE1RE0RA1RB which immediately halts but this function returns a contradiction.

Additionally, and probably more importantly, I believe the algorithm should need to remove items from the discovered_configs set or else two branches that both point towards the same end state may both find a contradiction with the opposite branch (however, I have not confirmed this theory)

Update: @atticuscull explained that my second critique was wrong, we are just backtracking forever while there are still possible previous states (but if there are no possible previous states to all states that could reach the halting state, then the machine runs forever)

Thank to both of you for looking at this in more details.

I need to wrap my head around it soon.

Here is an argument of why the algorithm works. This has in mind the go implementation, as opposed to the above python, seeing as the go code is more relevant. Not much is changed besides that a stack is used instead of a queue, making it depth first, and some of the variable names have changed. Let me know if this is not what you asked for; I’m happy to try and shorten it, or fill in other details that I breezed over.

The algorithm works backwards from all halting states to see if there is no possible way to reach a halting state. Abstractly, we are exploring a digraph where each node is a local configuration, that is a small section of the tape where no assumptions are made about the rest of the tape (put another way, each node represents all possible extensions of the local section of the tape). This differs from the usual notation wherein the rest of the unseen tape is assumed to be zeroes. The goal of the algorithm is to show that this digraph of predecessor configurations is self-contained finite by exploring it entirely. Technically we also need to show that the digraph does not contain a local configuration of state A and only zeroes on the tape, however I do not imagine that we will run the decider for 47 million steps on every undecided machine, and we already know that the digraph doesn’t contain a local configuration of the starting state if it has size less than 47 million.

Concretely, the algorithm implements a depth first search on the digraph (limited by a search depth). stack contains the current leaves of our search. seenStates stores the configurations we’ve seen already so that we don’t repeat unnecessary computation. That is, once we’ve found all of the predecessors of a configuration, we don’t need to look at it again.

To start the search, we add all of the local configurations consisting of a state s along with a single cell of exposed tape with bit b, where (s b) is an undefined transition. Next, as long as there are possible local configurations that we haven’t checked yet, we take the next one from the stack, and find all of the predecessor configurations. We do that by looking at all state + bit combinations (s’, b’) that transition to the current state s, and for each one checking that the place where that transition moved from (i.e. if (s’ b’) moves right then we look at the cell to the left of the current head), has the same bit as what the transition (s’ b’) writes. If the current head is at the far left (respectively right) and (s’ b’) moves right (respectively left) then the local configuration expands in scope; this is always acceptable as we made no assumptions about the tape outside of the scope of the local configuration.

For example, if we are in state A with tape 000[1]101, then we want any transition rules that transition to A and either
1. move right and write 0, or
2. move left and write 1
Then, for each pair (s’ b’) satisfying this, we add
1. s’: 00[b’]1101 or
2. s’: 0001[b]01
to stack respectively, if it is not in seenStates.

If this process terminates in 47 million steps or fewer, we know that the halting states are in a different connected component in the configuration graph than the starting configuration (A with all 0s), and so it is not possible for the machine to halt.


Thanks to the work of @modderme123 and @atticuscull, the decider was debugged and successfully applied!

It decided 2,243,340 machines :partying_face:

The index file of undecided machines has been updated: https://github.com/bbchallenge/bbchallenge-undecided-index

A new bug has been found and hopefully fixed: Debuggin Shawn's bug by tcosmo · Pull Request #7 · bbchallenge/bbchallenge-deciders · GitHub

Don’t hesitate to review the code!

Hence this voids the results claimed in the previous message, the new result is 2,035,610 machines decided!

The index file of undecided machines has been updated: https://github.com/bbchallenge/bbchallenge-undecided-index