sligocki / busy-beaver Goto Github PK
View Code? Open in Web Editor NEWTools for finding Busy Beaver Turing Machines and Proving others as non-halting
License: MIT License
Tools for finding Busy Beaver Turing Machines and Proving others as non-halting
License: MIT License
Code/Quick_Sim.py -r --exp-linear-rules --no-steps <(echo 1RB2RB3LA2RA3RA_0LA1RB4RA1LB1RZ)
There is a bug in the Limited_Diff_Rule code. See last rule proven by:
$ Code/Quick_Sim.py <(echo "1RB 3RB 3LB 0RB 0LA 2LB 3RA 3RB 4RA 2LA") -bn1 -r --limited-rules -v
...
** New rule proven **
Limited Diff Rule 3
Initial Config: 3^1 4^1 A> 2^(k + 2) (2,1)
Diff Config: 3^0 4^0 A> 2^-1
Steps: 5, Loops: 5
This is clearly an incorrect rule (if it deletes a 2 each iteration, it must add some symbol somewhere!).
In fact it adds a 0. The rule should actually be:
but, the way the proof system works, it is actually proving:
it never "looks at" the 0s to the left (and the exponent doesn't change ... b/c inf), so our system incorrectly removes the 0^inf from the limited diff rule.
Here's one that seems like it could be handled by your simulator:
1RB 2LA 1RA 1LA 0LB 2RB
Every so often it gets into a configuration just a solid block of 2s:
0^inf <A (2) 2^6 0^inf
The length of the block extends each time by 2^n. So the numbers are:
This is one of the few Christmas tree-like machines left unhandled among the short categories. All the rest are counters.
The following 10 machines were categorized as halting in < 1000 steps by the Enumerate.py --recursive
:
1RB 1LA 1RC 0LE 1RD 1LC 1LA 0RF 1RD 0LA 1RZ 0RE | None Halt 22 243
1RB 1LA 1RC 0LE 1RD 1LC 1LA 0RF 1LB 0LA 1RZ 0RE | None Halt 22 255
1RB 0LF 1LC 1RB 1LE 0RD 1RC 0RB 1LA 1RE 1RZ 0LD | None Halt 22 259
1RB 0LF 1LC 1RB 1LE 0RD 1LA 0RB 1LA 1RE 1RZ 0LD | None Halt 22 247
1RB 0RE 1LB 1LC 1LD 1RC 1RE 0LF 0RA 1RE 1RZ 1LB | None Halt 48 600
1RB 0LC 1RC 0RE 0LD 1RB 1LB 1LD 1LF 1RE 1RZ 0LA | None Halt 18 550
1RB 0RE 1LB 1LC 1LD 1RC 1LE 0LF 0RA 1RE 1RZ 1LB | None Halt 27 226
1RB 1RC 1RC 0LE 1RD 1LC 1LE 0RF 0LB 1LE 1RZ 1RA | None Halt 38 908
1RB 0LB 1RC 1RB 1RD 1LF 0RE 1LC 1LD 1RE 1RZ 0LA | None Halt 16 185
1RB 0LE 1RC 1LB 1LD 0RF 1RA 1LD 1RD 0LD 1RZ 0RE | None Halt 22 225
However, none of these were not classified as halting by the C++ direct simulation code lr_enum
which was run for 1000 steps.
Looking at just the first machine: Quick_Sim.py -rn1
shows it halting at step 243! But Quick_Sim.py -rn2
shows it infinite ...
With Quick_Sim
, I can verify the BB(6) second-place program (1RB 0LD 1RC 0RF 1LC 1LA 0LE 1LZ 1LA 0RB 0RC 0RE
) after just 1873 loops. But the first-place program (1RB 1LE 1RC 1RF 1LD 0RB 1RE 0LC 1LA 0RD 1LZ 1RC
) I can't verify at all. Often the process gets killed.
Are there some particular settings that will make it work?
Running program 1RB---_1LC0RB_1LD0RD_0RE1LB_0RC1RF_0RA1RE
:
Code/Quick_Sim.py -r --exp-linear-rules <(echo 1RB---_1LC0RB_1LD0RD_0RE1LB_0RC1RF_0RA1RE)
Raises exception:
Exp_Int.ExpIntException: Cannot evalulate sign of ExpInt: ((12096 + -2576 * 6^((1 + 69 * 6^((-4 + 69 * 6^((-4 + 69 * 6^13)/5))/5))/5) + 2116 * 6^((-3 + 23 * 6^((1 + 69 * 6^((-4 + 69 * 6^13)/5))/5))/5) + -46 * 6^((11 + 69 * 6^((-4 + 69 * 6^((-4 + 69 * 6^13)/5))/5))/5))/25) ((3, 140252096236.63162) == (3, 140252096236.63162))
I think it's infinite, but not 100% sure. Running with --no-steps
raises no error and seems to run without stopping.
I finally got around to trying out the CTL filter. I'm not sure if I'm using it right, but I ran it against my list of 11,702 4-state 2-color holdouts, and it failed on just 8 of them:
1RB 0LA 1LC 0RB 1RD 1LD 1LA 1RC
1RB 0LA 1LC 1RC 1RD 1LB 1LA 0RD
1RB 0LC 1LC 1RD 1LA 1LC 0LB 0RD
1RB 0LC 1LD 1RC 0LB 0RC 1LA 1LD
1RB 1LC 0LA 0RB 1RA 1RD 0LC 1LD
1RB 1LC 0RC 0LC 1LD 1RA 0RA 0LD
1RB 1RC 0LC 1LB 1RD 1LA 0LA 0RD
1RB 1RC 1LC 0LB 1RD 1LA 0RD 0LA
It's definitely possible that I'm misinterpreting things, but this list is somewhat interesting in any case. In particular the first program there is nifty. It sets up bound markers on either side of the head and gradually pushes them out.
Do you get similar results?
I profiled Quick Sim running over a list of programs for 10,000 loops.
A lot of time is getting spent in strip_config
and its subsidiary stripped_info
.
I don't know what the solution is exactly, but I bet there is a simple change that could be applied here to speed things up.
I see from the code comments that this is a known issue. Hopefully the graph is helpful anyway.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.