Decider closed states

.gitignore

@@ -1,3 +1,5 @@
+__pycache__
+venv
 decider-cyclers/decider-cyclers
 rsync_indexes.sh
 unsorted_indexes

decider-closed-states/README.md

@@ -0,0 +1,8 @@
+# Decider closed states
+
+```python
+python3.9 -m venv venv
+pip install -r requirements.txt
+python -m unittest main_test.py
+python main.py
+```

decider-closed-states/bbchallenge_utils.py

@@ -0,0 +1,77 @@
+import os
+from tabulate import tabulate
+
+
+def get_machine_i(machine_db_path, i, db_has_header=True):
+    with open(machine_db_path, "rb") as f:
+        c = 1 if db_has_header else 0
+        f.seek(30 * (i + c))
+        return f.read(30)
+
+
+def get_indices_from_index_file(index_file_path):
+    index_file_size = os.path.getsize(index_file_path)
+
+    machines_indices = []
+    with open(index_file_path, "rb") as f:
+        for i in range(index_file_size // 4):
+            chunk = f.read(4)
+            machines_indices.append(int.from_bytes(chunk, byteorder="big"))
+
+    return machines_indices
+
+
+R, L = 0, 1
+
+
+def ithl(i):
+    return chr(ord("A") + i)
+
+
+def g(move):
+    if move == R:
+        return "R"
+    return "L"
+
+
+def pptm(machine, return_repr=False):
+    headers = ["s", "0", "1"]
+    table = []
+
+    for i in range(5):
+        row = [ithl(i)]
+        for j in range(2):
+            write = machine[6 * i + 3 * j]
+            move = machine[6 * i + 3 * j + 1]
+            goto = machine[6 * i + 3 * j + 2] - 1
+
+            if goto == -1:
+                row.append("???")
+                continue
+
+            row.append(f"{write}{g(move)}{ithl(goto)}")
+        table.append(row)
+
+    if not return_repr:
+        print(tabulate(table, headers=headers))
+    else:
+        return tabulate(table, headers=headers)
+
+
+def format_machine(machine):
+    to_return = []
+    for i in range(5):
+        state_rep = ""
+        for j in range(2):
+            write = machine[6 * i + 3 * j]
+            move = machine[6 * i + 3 * j + 1]
+            goto = machine[6 * i + 3 * j + 2] - 1
+
+            if goto == -1:
+                state_rep += "---"
+                continue
+
+            state_rep += f"{write}{g(move)}{ithl(goto)}"
+        to_return.append(state_rep)
+
+    return "_".join(to_return)

decider-closed-states/main.py

@@ -0,0 +1,111 @@
+import tqdm
+from bbchallenge_utils import *
+
+DB_PATH = "../all_5_states_undecided_machines_with_global_header"
+UNDECIDED_INDEX_PATH = "../bb5_undecided_index"
+
+
+def get_states_with_undefined_transition(machine: bytes):
+    to_return = []
+    nb_states = len(machine) // 6  # 3 bytes per transition, 6 per state
+    for i_state in range(nb_states):
+        if machine[6 * i_state + 2] == 0 or machine[6 * i_state + 5] == 0:
+            to_return.append(i_state)
+
+    return to_return
+
+
+def get_states_reachable_from(
+    machine: bytes, i_state: int, debug: bool = False
+):
+    # BFS logic
+    visited = set({})
+    to_visit = [i_state]
+    if debug:
+        print()
+
+    while len(to_visit) != 0:
+        curr_state = to_visit[0]
+        to_visit = to_visit[1:]
+
+        if curr_state in visited:
+            continue
+
+        visited.add(curr_state)
+
+        goto_0 = machine[6 * curr_state + 2]
+        if goto_0 != 0:
+            to_visit.append(goto_0 - 1)
+
+        goto_1 = machine[6 * curr_state + 5]
+        if goto_1 != 0:
+            to_visit.append(goto_1 - 1)
+
+        if debug:
+            print(curr_state, goto_0, goto_1, to_visit)
+    return visited
+
+
+def decider_closed_states(
+    machine: bytes, debug: bool = False, reachables_to_return: set = {}
+):
+    """If the machine ever enters a closed set of states where
+    all transitions are defined, then it never halts.
+
+    Note that by:
+
+    1. By construction, any state of a machine of bbchallenge that
+    contains at least one defined transition has been reach at some point in the
+    execution of the machine.
+
+    2. Furthermore, there are no machines in the db with a state that has 2 undefined transitions,
+    since this is solved by BB(4) = 107 during enumeration. This means that with point 1. we know
+    that all the states of the machine are reached at some point by the machine when started from
+    blank tape.
+
+    Hence we don't need to run the machine at all, but we just need to check its code to see if there
+    exists such a closed set of states where all transitions are defined. We know that it'll be reached
+    and that the machine does not halt.
+    """
+
+    states_with_one_undefined_transition = get_states_with_undefined_transition(
+        machine
+    )
+
+    if debug:
+        pptm(machine)
+        print(states_with_one_undefined_transition)
+
+    nb_states = len(machine) // 6
+
+    for i_state in range(nb_states):
+        reachables = get_states_reachable_from(machine, i_state, debug)
+        if debug:
+            print(i_state, reachables)
+        closed_states = True
+        for reachable_state in reachables:
+            if reachable_state in states_with_one_undefined_transition:
+                closed_states = False
+                break
+
+        if closed_states:
+            reachables_to_return.update(reachables)
+            return True
+
+    return False
+
+
+if __name__ == "__main__":
+    undecided_machines_indices = get_indices_from_index_file(
+        UNDECIDED_INDEX_PATH
+    )
+
+    print("machine_id; machine; closed_states")
+
+    for machine_id in tqdm.tqdm(undecided_machines_indices):
+        machine = get_machine_i(DB_PATH, machine_id)
+        closed_states = set({})
+        if decider_closed_states(machine, reachables_to_return=closed_states):
+            print(machine_id, end="; ")
+            print(format_machine(machine), end="; ")
+            print(set(map(lambda x: chr(ord("A") + x), closed_states)))

decider-closed-states/main_test.py

@@ -0,0 +1,19 @@
+import unittest
+from main import decider_closed_states, DB_PATH
+from bbchallenge_utils import get_machine_i
+
+
+class TestDeciderClosedStates(unittest.TestCase):
+    def test_examples(self):
+        ids_to_test = [4, 9]
+
+        for machine_id in ids_to_test:
+            machine = get_machine_i(DB_PATH, machine_id)
+            self.assertTrue(decider_closed_states(machine))
+
+    def test_counterexamples(self):
+        ids_to_test = [5, 207]
+
+        for machine_id in ids_to_test:
+            machine = get_machine_i(DB_PATH, machine_id)
+            self.assertFalse(decider_closed_states(machine, debug=False))