[Decider] Bouncers

An interesting parsing problem arises from @savask’s bouncers code.

We try to match the format s(n) = u1 w1^n u2 w2^n ... uk wk^n S> being given s(0), s(1), s(2). Example from @savask:

For example, if we have
      s0 = 101 S>
      s1 = 110011 S>
      s2 = 110100111 S>
  then
      s(n) = 1 10^n 0 1^n 1 S>
  and the tape formula will be
      1 (10) 0 (1) 1 S>.

This is currently solved using dynamic programming, but we explore if there is a more efficient algo.

First, idea was the following greedy algorithm by @savask:

if all strings start with one symbol, throw it away. If not, try finding a longest prefix w of s1 such that w w is a prefix of s2, and throw those away.

Unfortunately, this fails on examples like the following:

s0 = 1111111011
s1 = 11110111101111011111111011
s2 = 111101111101111011110111101111011111111011
Correct parsing = 111 (101111) (0111101111) 1111011

@savask compiled a list of instances of s0, s1, s2 and correct parsing in the following text files as a benchmark to try algos on:

examples_hard.txt (16.1 KB)
examples.txt (104.8 KB)

I wrote another implementation of savask’s algorithm, in Rust. Like all my other deciders, it generates certificates that then get checked by a verifier proven correct in Coq. Thus, the results are almost guaranteed correct. This should brings us closer to a Bouncers decider that meets the verifiability & reproducibility standards – I think only the section of the decider-correctness document is missing?

When ran on the 32632 undecided machines, it decides 29799 machines in about 10 seconds. This is the same 29799 as Tony’s decider, according to @UncombedCoconut’s data. If I am understanding savask’s comments correctly, this also agrees with their implementation – since it’s slower by a few orders of magnitude, and requires a different I/O format, I didn’t bother actually running it to confirm.

The limits I need to get these results are

const SPACE_LIMIT: usize = 1024;
const TIME_LIMIT: u32 = 250000;

Notably, this is less than Tony’s decider – reducing the 1M step limit to 250k prevents it from deciding one machine.

3 Likes

This is very impressive work, you are really pushing bbchallenge on the tracks of automatic proofs at a faster rate than what I could have imagined in my dreams!!

I am going to read your code in depth as well as starting to write about bouncers in parallel.

Thank you!

Earlier in May @Iijil also proposed an implementation of bouncers: GitHub - Iijil1/Bouncers: A bouncer decider. Proving that some turing machines don't halt.

In compliance with our validation process, we’re officially releasing the decider for bouncers today!

  1. The formal presentation and proof of correctness of the decider is given in Section 7 of bbchallenge’s official write-up.

  2. The method decided 29,799 machines (91%) over the 32,632 that were left undecided after the previous [Decider] Finite Automata Reduction release.

  3. The official undecided index has been updated and certificates for the bouncers released: https://github.com/bbchallenge/bbchallenge-undecided-index/releases/tag/bouncers.

  4. The implementations (and reproductions) for the decider are:

Many thanks to @TonyG for initially presenting the method and to all the contributors that have participated in the release: @Iijil, @savask, @meithecatte, @UncombedCoconut, Pascal Michel, @cosmo.

Beaverly yours,

:beaver::beaver::beaver:

1 Like

Alternate upload, since Discord CDN links don’t work anymore: https://gist.github.com/CatsAreFluffy/e38bcd11f4796190e06487d69ae55a2a

1 Like