[Decider] Translated cyclers

Deciders
10

I’ve written an implementation of this decider, and an associated verifier, with a formal proof of correctness in Coq for the latter: GitHub - meithecatte/busycoq: Busy Beaver deciders backed by Coq proof

Since in the decider I use an algorithm based on Floyd’s tortoise and hare, it finds slightly less machines when ran with a time limit of 4M, than @TonyG reports.

I also ran it with a time limit of 50M and a space limit of 65536 cells (where the head starts in the middle, so realistically it’s half that).

This gave the following results, after 2.5h:

Translated Cyclers:
  73861235 Decided
        25 OutOfSpace
    480775 OutOfTime

This is 616 more machines than what has been marked as “decided by Translated Cyclers” in the database. This breaks down as follows:

    534 backward-reasoning-run-7edeea99bc2d-depth-50-minIndex-0-maxIndex-88664064
     10 FAR-finite-automata-reduction-run-JEB-max-6-DFA-states
     72 halting-segment-reproduction-run-2vlymsaql86b-max-distance-to-end-6

Unfortunately, nothing newly decided. If it is of any interest, here is the indices file:

newly-decided.dat (2.4 KB)

1 Like