Deciding 5-state bouncers collaboratively

[Tristan Stérin]

Dear all,

What I consider to be an immediate next goal at https://bbchallenge.org is to decide unilateral and bilateral bouncing 5-state machines (such as https://bbchallenge.org/6048289 or https://bbchallenge.org/8929416). Concretely this means to write an algorithm that recognises this behavior and prove that the algorithm is correct. We estimate that bouncers account for at least 90% of the currently remaining undecided machines. Deciding them would hopefully leave us with less than 200,000 undecided machines left.

A lot of you, I believe, have thought about this kind of machines, or have even already decided them, probably using different names such as "Chrismas trees" (I used to call them "Wedding cakes").

I would be super interested in organising a collaborative call about these machines with the goal to share our techniques and hopefully come up with a decider that is provably correct (similarly to these). I would largely be happier with an incomplete decider (i.e. doesn't recognise all bouncers) that we can prove correct than with a complete one for which we cannot write the proof.

Would that be appealing to you? Concretly, I would propose a 2h Zoom call at a time that suits all time zones involved to collaboratively tackle this problem. From this initial call would probably come some follow up, either offline or online, to share implementations and proofs.

Given, the large number of machines that this effort will decide, it seems very worthwhile to me! Although, we are not in a huge rush and we could start this effort in a few months if it suits better.

Sincerely yours,

T

[Shawn Ligocki]

This is very exciting. However, I have an alternative proposal: I just wrote a blog post about the "CTL Filter": https://www.sligocki.com/2022/06/10/ctl.html

With this filter I've been able to decide 85% of your currently listed unproven machines. So, to me, this is a solid next step to aim for. This filter (like Backtracking) does not decide a specific type (Zoology) of machine, instead it can prove machines with many different behaviors (mostly by proving what they cannot do!).

If you're interested I would be glad to work with y'all to implement this and get down to ~200k unknown machines.

--
You received this message because you are subscribed to the Google Groups "Busy Beaver Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to busy-beaver-dis...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/f7ac7b28-226c-411f-b4fa-788b60230641n%40googlegroups.com.

[Tristan Stérin]

Waw, this sounds really cool, love your blog post.

It definitely looks to be a very good method to decide a lot of machines at once.

We should definitely implement it with your help!

Thank you again for sharing it!

[Nicholas Drozd]

Great post, Shawn! It's nice to finally get an explanation of CTL. I had seen those files in your repo and tried to make sense of them, but the comments are awfully cryptic :)

[Tristan Stérin]

Contributor @lijil has proposed a decider for Unilateral Bouncers: https://discuss.bbchallenge.org/t/decider-unilateral-bouncers/63 that I will study soon!