[Decider] Bouncers

Deciders
22

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)

23

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
24

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.