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
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?
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.
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 ...
It would be nice if we could tell Quick_Sim.py to watch for one specific config pattern that might have some exponents fixed with others variable. Specific example:
Code/Quick_Sim.py 1RB2RA1LB_0LC0RA1LA_---2LA--- -n2 --limited-rules -v | egrep "10\^1 22\^4 \(22\) A> 00\^inf"
1254 00^inf 10^1 22^5 10^1 22^2 10^1 22^42 10^1 22^4 (22) A> 00^inf (8, 12160)
2790 00^inf 10^1 22^5 10^1 22^2 10^1 22^486 10^1 22^4 (22) A> 00^inf (8, 978262)
4188 00^inf 10^1 22^5 10^1 22^2 10^1 22^4_482 10^1 22^4 (22) A> 00^inf (8, 80628268)
5586 00^inf 10^1 22^5 10^1 22^2 10^1 22^40_446 10^1 22^4 (22) A> 00^inf (8, 6545950210)
6984 00^inf 10^1 22^5 10^1 22^2 10^1 22^364_122 10^1 22^4 (22) A> 00^inf (8, 530361180376)
8382 00^inf 10^1 22^5 10^1 22^2 10^1 22^3_277_206 10^1 22^4 (22) A> 00^inf (8, 42960513309358)
9780 00^inf 10^1 22^5 10^1 22^2 10^1 22^29_494_962 10^1 22^4 (22) A> 00^inf (8, 3479812903236484)
11178 00^inf 10^1 22^5 10^1 22^2 10^1 22^265_454_766 10^1 22^4 (22) A> 00^inf (8, 281864947095759706)
12576 00^inf 10^1 22^5 10^1 22^2 10^1 22^2_389_093_002 10^1 22^4 (22) A> 00^inf (8, 22831061632167084592)
This appears to be a valid Level 2 rule, but we are not proving it. Probably b/c these stripped configs are happening with changing exponents and so we don't noticed this long-term pattern. Guessing these things is hard, but we could at least support validating them with command-line hints.
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.
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.
Quick_Sim.py
is able to run the below beavers to the point of halting. (I'm collecting, not claiming originality.)
1RB0LA_0RC1RE_0RD1RC_1LD1LA_1RF1RB_0LC1RZ
1RB0LA_0RC1RE_0RD1RC_1LD1LA_1RF1RB_0RD1RZ
1RB0LE_0RC1RZ_0LD0RF_1LA0LF_1LF1LD_0LA1LF
1RB0RA_1LC0LC_0LF0RD_1RA1LE_0LB1RZ_1LD1RB
1RB0RA_1RC0RB_1LD0RA_1LE0LC_0LA0LF_1LC1RZ
1RB0RC_1LC0RA_0LE1LD_1LE0LF_0RD0LB_1LA1RZ
1RB1LC_0RC1RD_1LD0LE_1RA1RE_1RF0LC_0RB1RZ
1RB1LD_1RC0LA_1LB0RD_0LA1RE_0RF1LA_1RZ0RB
1RB1RE_1LC0RF_0RA0LD_1LE1RZ_0LC0LE_0RB0RD
1RB1RE_1RC1LD_0RD1RA_1LA0LE_1RF0LD_0RC1RZ
1RB1RF_0LC1RZ_1LD0RD_1LE0LB_0RA1LC_0RC0RA
1RB0LF_0RC0RB_1LC0LD_1LE0RA_1LA0LD_0RC1RZ
[using -n 6
]1RB1LF_0RC0RB_1LC0LD_1LE0RA_1LA0LD_1LC1RZ
[using -n 6
]1RB1RE_1LC1LB_1RE0LD_1LB1LC_0RF1RA_1RZ0RA
[using -n 6
]1RB1RF_1LC0LA_1RZ1LD_1LE0LB_1RF0LB_0RA1RA
1RB1RZ_0LC0LF_1RF1LD_0LE0RA_1LC0LF_0LD0RC
1RB1RA_1LC0RE_0LF1LD_1LA1LC_1RA1RB_1RZ0LD
1RB0RA_1LC0RC_0LE0LD_1RA0LB_0RD1LF_1RZ0LB
1RB0RE_1LC1RD_1LA0LC_1RE1RF_0RB0LB_0RA1RZ
[warning: takes about 4 hours]mxdys also posted a batch BB6_halt_HashTM_32_2e7.txt
on which I haven't tested Quick_Sim
. One has an undefined transition in addition to the halting one.
1RB1RZ_0LC0LF_1RF1LD_0LE0RA_1LC0LF_0LD0RC
[H 1.62697e+11 T:15228698
]1RB1RF_1LC0LA_1RZ1LD_1LE0LB_1RF0LB_0RA1RA
[H 1.11891e+11 T:6442876
]1RB1LA_0RC1LE_0RD1RF_1RE0LB_0LA1RD_0RA1RZ
[H 4.53892e+09 T:9171692
]1RB0LC_1LA1RD_1LA0LC_0RE1RZ_1RF0RE_0RA1RE
[H 3.46401e+11 T:6578212
]1RB1LE_1RC0RF_1LD0LE_1RZ1LA_0LB1LC_1RB1RF
[H 1.72959e+09 T:5397908
]1RB0LE_0LC0RE_1LA0RD_1LB0RB_0RD1LF_0LD1RZ
[H 1.24486e+09 T:3955456
]1RB0LE_1RC0RE_0LD1LB_1LA1RD_1RF0LC_0RA1RZ
[H 1.76222e+10 T:3258040
]1RB1LC_1RC1RE_1LA0LD_0RD0LA_0RF0RE_1RA1RZ
[H 1.75709e+10 T:8182888
]1RB1RA_1LC0RA_0LE1LD_0LB1LC_1LF0LD_1LA1RZ
[H 7.8193e+11 T:9533324
]1RB1LA_0RC1RE_1LD0RB_1RA0LD_0RF1RC_1LD1RZ
[H 1.10102e+09 T:3025679
]1RB1RC_1LC1RC_1RE1LD_0LC0LD_0RF1RZ_1RA0LC
[H 1.39462e+11 T:3648921
]1RB0RC_1LC1RZ_1RF0LD_1LE1RD_0LC0LA_0RA1RF
[H 1.03714e+09 T:4184316
]1RB0LE_1RC1RZ_1LD0RC_1LF0RE_1RB1LC_0LA1LE
[H 1.44603e+11 T:8147149
]1RB0LE_0RC1RB_1RD0RA_1LA1RZ_1LF1RE_0LA0LC
[H 1.03714e+09 T:4187708
]1RB1RC_1LA1RF_1RZ0RD_1LE0RB_1LE0LF_1RA0LF
[H 1.73976e+10 T:5287167
]1RB1RZ_0RC0LF_1RD1RA_0RE1LD_1RF0RD_1LB0LF
[H 8.92475e+10 T:15149422
]1RB0LD_1RC0RE_1RD1RZ_1LE1RF_1LC0LF_1LA0RA
[H 3.80742e+11 T:12290395
]1RB1LE_0RC1RB_1RD1RF_0LA0LB_1LA0LD_1RZ1RA
[H 5.45548e+09 T:16882447
]1RB0RA_1LC0RA_1LD0LB_1RA1LE_0LA0LF_0LE1RZ
[H 5.15275e+10 T:7015811
]1RB0LE_1RC1RZ_1LD0RC_1LF1LA_1RB0LF_1RD1LC
[H 1.73976e+10 T:5291567
]1RB1LE_0RC1RB_1LD0RB_1LA1RZ_1LC0LF_1LA0LA
[H 1.01776e+09 T:10780802
]1RB0LF_1LC0RE_1LD0LB_1LA1RZ_0RB1LA_0LA0LE
[H 3.98952e+09 T:12971337
]1RB0LA_0RC0RD_1LC1LA_1RZ1RE_0RB1RF_1RA1RE
[H 4.62527e+09 T:3968022
]1RB0LD_0LC0RF_1LE0RD_1LB1RZ_1LA0LD_0RB0RA
[H 2.30537e+11 T:6971770
]1RB1LE_1RC0RF_1LD1RD_1RC1RA_0LB0LA_0RC1RZ
[H 2.48718e+09 T:5729195
]1RB0LE_0RC0RD_1LD0RF_0LA1RZ_1LA0RC_1RA1RB
[H 3.65383e+11 T:7695634
]1RB0RF_1LC1RC_1RB1RD_1RA1LE_0LA0LD_0RB1RZ
[H 1.15341e+09 T:3405749
]1RB0LE_0RC1RF_1RD0RF_1RE1RZ_1LA1LE_0RA1RB
[H 3.12768e+12 T:19048114
]1RB0LA_1RC1RD_1LB1RA_1RZ0RE_1LF0RC_1LA---
[H 1.73976e+10 T:5282649
]1RB0RC_1LC1RE_1RA0LD_1LC0LD_0RD0RF_0RE1RZ
[H 5.15281e+10 T:7016309
]1RB1LE_1LC0RD_1LA0LB_1RB0RD_0LD0LF_0LE1RZ
[H 5.15275e+10 T:7015844
]1RB0LC_1LA1RD_1LA0LC_1LE1RZ_0RA1RF_1RE0RF
[H 3.95886e+11 T:7517071
]1RB0LF_1RC0RF_1LD0RF_0RA0LE_0LD0LC_1RD1RZ
[H 2.3053e+11 T:7407081
]1RB0LC_1LC1LF_0RD0LB_1LB1RE_0RD1RD_1RZ1LA
[H 3.26024e+11 T:7774548
]1RB1LF_1LC0RE_1RC0LD_1LA1LD_1RA1LA_1RZ0LC
[H 1.23283e+11 T:10045033
]1RB1RZ_1LB1RC_1RD0LC_0RE0RF_1RF1RA_0RB0LF
[H 3.24088e+10 T:3523337
]1RB1RZ_1LC0LF_1RD0RC_0RE1RB_1LF1LA_0LB1LE
[H 2.1598e+11 T:14347981
]1RB0RD_1LC1RE_1LD0LC_1RA0LC_0RC0RF_0RE1RZ
[H 5.15281e+10 T:7016292
]1RB0LC_1RC1RF_1LD1LA_0LA1LE_1RA0RA_1RE1RZ
[H 6.45588e+10 T:5024954
]1RB0LD_1RC0RA_1LD1RE_1LA0LD_0RD0RF_0RE1RZ
[H 5.15269e+10 T:7015795
]1RB0LC_1LA1RE_0LD0LB_1LB1LE_1LF0RB_1RZ1LB
[H 1.66549e+09 T:6369426
]1RB1LC_1RC1RZ_1LD0RC_1LE1LD_0LF1LA_1RB0LA
[H 1.4001e+11 T:7884536
]1RB1RF_1LC0RD_0LD0LC_1RE1LC_0RB1RA_0LB1RZ
[H 3.6566e+12 T:18473722
]1RB1LA_1LC1RE_1LD0LC_0RA0LB_0RF1RZ_1RD1LA
[H 2.10217e+12 T:12189454
]1RB1LA_1LC1RE_1LD0LC_0RA0LB_0RF1RZ_1RD1LD
[H 2.36494e+12 T:13713936
]1RB0LD_1LC0RE_1RZ1LD_1LA0LE_0LF1LA_0RA0LB
[H 6.54971e+10 T:4292546
]1RB0LF_1RC0RD_1LD0RA_0LE0LC_0RB0LA_1RE1RZ
[H 2.85747e+10 T:19855880
]1RB1LB_1RC0RD_0LD1RB_0RA1RE_1LF1RZ_1LC0LF
[H 2.27574e+09 T:10568376
]1RB0LD_1RC0RA_1LA1RE_1LA0LD_0RD0RF_0RE1RZ
[H 5.15269e+10 T:7015808
]1RB0LB_1RC0LA_0LD0RE_1RF1LB_1RD1RZ_1LB0RA
[H 4.75041e+11 T:11023834
]1RB0LD_1LC1RF_0RE1RD_1LE1LA_1RA1RE_0RC1RZ
[H 2.70672e+10 T:7094089
]1RB1RF_1LC0LA_1RZ1LD_1LE0LB_1LF0LB_0RA1RA
[H 1.11891e+11 T:6442899
]1RB1LC_1LA1LD_1LB0RC_1RZ0LE_1RF0LA_1RF1RA
[H 1.9353e+10 T:5902023
]1RB1RF_1LC0LA_1RZ1LD_1LE0LB_1RF1RC_0RA1RA
[H 1.11892e+11 T:6444018
]1RB1LA_1RC0RF_0RD1RZ_1LE1RE_0LA0LE_0RE1LC
[H 2.74752e+09 T:11576855
]1RB1RZ_1RC1LD_1LD0RE_1RF0LE_1RD0LD_0LB0RA
[H 4.75023e+11 T:10624658
]1RB1LA_1RC0RF_0RD1RZ_1LE1RE_0LA0LE_0RE1RE
[H 2.49775e+09 T:10530510
]1RB1LA_0RC1RE_1LD0RB_1RA0LD_1RF1RC_1LA1RZ
[H 1.10102e+09 T:3025577
]1RB0LA_0LC1RD_1LB1LA_0RE1RZ_1RF1RE_0RC0LC
[H 1.70715e+12 T:13221670
]1RB0RF_1LC0RF_0RE0LD_0LC0LB_1RA0LF_1RC1RZ
[H 2.30525e+11 T:6839012
]1RB0RF_1LC0RD_0LD0LC_1RE1LC_0RB1RA_1RE1RZ
[H 3.25031e+12 T:14825820
]1RB0LC_1LA1RE_1LD1LA_1RA1RD_0RF1RZ_0RD1RC
[H 2.70671e+10 T:7093451
]1RB1RF_1RC0LB_0RD0RE_1LD1LB_1RZ1RF_0RC1RA
[H 4.62612e+09 T:3959919
]1RB1LF_0LC1LE_1LD1LC_1LA0RE_1RC1RD_0LB1RZ
[H 2.70696e+10 T:5112392
]1RB0LC_1LC1RD_1LA0LC_1LE1RZ_0RA1RF_1RE0RF
[H 3.95886e+11 T:7516964
]1RB1RZ_1LC0RF_1RE0LD_0LC1RB_1RA0RC_0RB0RD
[H 3.98952e+09 T:18939887
]1RB0LC_1LC1RD_1LA0LC_0RE1RZ_1RF0RE_0RA1RE
[H 3.46401e+11 T:6578107
]1RB0RE_1LC0LF_1RZ1LD_1RA1LF_1RA1RE_0LA1LB
[H 1.72312e+09 T:5469909
]1RB0LF_1LC0RF_0RE0LD_1LE1RZ_1LA1RB_1LB0RB
[H 4.7503e+11 T:10626761
]1RB1LE_1LC1RE_1LD0LC_0RA0LB_0RF1RZ_1RD1LA
[H 2.10217e+12 T:12189479
]1RB1RF_1LC0LA_1RZ1LD_1LE0LB_1LF1RC_0RA1RA
[H 1.11892e+11 T:6444041
]1RB0RB_1LC0RC_1LE0RD_0RB1LA_0LA0LF_0LD1RZ
[H 9.23399e+10 T:5789555
]1RB1LA_0RC1RE_1LD0RB_1RA0LD_0RF1RC_0LB1RZ
[H 1.10102e+09 T:3025781
]1RB0LA_1RC1RD_1LB1RA_0LF0RE_1LF0RC_1LA1RZ
[H 1.73976e+10 T:5282652
]1RB0LA_1RC1RD_1LB1RA_0RF0RE_1LF0RC_1LA1RZ
[H 1.73976e+10 T:5282650
]1RB0LA_1RC1RD_1LB1RA_1LF0RE_1LF0RC_1LA1RZ
[H 1.73976e+10 T:5282652
]1RB0LA_1RC1RD_1LB1RA_1RF0RE_1LF0RC_1LA1RZ
[H 1.73976e+10 T:5282650
]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?
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.
Code/Quick_Sim.py -r --exp-linear-rules --no-steps <(echo 1RB2RB3LA2RA3RA_0LA1RB4RA1LB1RZ)
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.