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