[Decider] Translated cyclers

Translated cyclers: principle

The goal is to decide [Family] Translated cyclers.

Principle:

The main idea for recognising ``Translated Cyclers’’ is to find two configurations that break a record (i.e. visit a memory cell that was never visited before) in the same state (here state D, color green) such that the content of the memory tape at distance L from the record positions is the same in both record configurations. Distance L is defined as being the maximum distance to record position 1 (green cell in record 1) that was visited between the configuration of record 1 and record 2.

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

Decider examples and counterexamples

Decider code

https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-translated-cyclers

Decider tests

https://github.com/bbchallenge/bbchallenge-deciders/blob/main/decider-translated-cyclers/main_test.go

Results

Database subset of application

  • 01/04/22 results were run on the 3,575,540 machines remaining after [Decider] Cyclers and the first passes of translated cyclers and after discarding the machines decided by [Decider] Backward reasoning because of a bug needing to be resolved in it.

  • 05/03/22 results were run on all machines that remained undecided after [Decider] Cyclers, the first results of this decider and the backward reasoning decider. This corresponds to a total of 2,323,786 machines tested.

  • 29/01/22 results were run on the machines starting at index 14,322,029 until final index 88,664,063 of the seed database which are the machines that exceeded the 12k memory limit. Indeed, it is unlikely that a translated cycler would exceed 47M time limit before reaching 12k visited memory cells. This corresponds to a total of 74,342,035 machines tested.

Decider correctness

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

I have written a Translated Cyclers Decider in C++, which outputs a Decider Verification File (dvf) as well as an Undecided Machines File (umf). I also wrote a Verifier, which checks the dvf for correctness. You can find them at bbchallenge/TranslatedCyclers at main · TonyGuil/bbchallenge · GitHub.

The Decider was run on the output file Cyclers.umf from the Cyclers Decider, with time limit 10,000 and space limit 1,000. It found 73,860,604 Translated Cyclers, as expected. Afterwards I ran it with time limit 4,000,000, and it found 566 more Translated Cyclers (in about 12 hours). The longest of these Translated Cyclers was found after 3,092,791 steps, so there might well be more out there. TC_4000000.dvf is the Decider Verification File for this run; you can check the new Translated Cyclers for yourselves using the data in this file. The format of the dvf is described in the README file at the link. My TranslatedCyclersVerifier program takes about 0.4 seconds to verify this file.

See the README file at the link for the format of the dvf.

1 Like

That’s really nice work, thank you very much!

I’ll repost the exact same answer as I did in [Decider] Cyclers but that is more relevant here:

@sligocki has found a 4-state translated cycler (yes, not a cycler, a translated cycler so not directly comparable) with period of 7,129,704 steps.

So, as you said, there is a little chance that some monstrous translated cyclers are still lingering around.

1 Like

@TonyG said:

@cosmo: I am having trouble verifying the machines at that link. It seems to me that the repeated states are not occurring at record values of the tape head, which means they can’t be Translated Cyclers. Have I misunderstood something? If only they provided proper Verification Data!

I’ll let @sligocki jump in as he found those machines but I believe that his output contains verification data:

1RB 0LD 1RC 1LD 1LD 0RC 0LA 1LB | Lin_Recur 7129704 512 <536870912

I believe that 7,129,704 is the length of the period and 512 536,870,912 when the machines enters the period?

@cosmo, @sligocki:

After 512 steps, that machine has tape head = -16, but the leftmost and rightmost tape cells visited are -28 and 8.

After 7,129,704 steps, the machine has tape head = -1840, but the leftmost and rightmost tape cells are -2335 and 532.

So neither of these is a record, and neither of these possible interpretations can be correct.

This notation means that the TM has period 7,129,704, offset 512 (to the right) and has started cycling by step 536,870,912 (This is not a minimum start time, but by then it is cycling for sure).

So the main issue in finding this one is running your simulator for half a billion steps! This, specifically, is the most extreme result I found before giving up my search for long periods.

Thanks for that! I can verify your machine now. The tape head after 536,870,912 is indeed not a record, but that doesn’t matter because we can verify that the tape contents to the right of the tape head are the same after 536,870,912 and (536,870,912 + 7,129,704) steps.

1 Like

Note that the method based on records that I have presented in this post and implemented is not universal and @sligocki’s implementation is probably based on a different idea.

@TonyG I have included your additional 568 translated cyclers to the official index of bbchallenge :slight_smile:

To be more precise, I included the 15 of them that were still undecided after backward reasoning and halting segment:

 31357173,
 42634480,
 42724921,
 45615747,
 46454294,
 46678518,
 49011952,
 52708280,
 55767995,
 58211439,
 59014181,
 60535952,
 60581745,
 83417747,
 84938097

Thanks to this we have gain more decided Skelet’s machines :)) (https://bbchallenge.org/skelet), thank you for the work!

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

That’s really cool work, thank you very much :pray: