Giter Club home page Giter Club logo

busy-beaver's People

Contributors

sligocki avatar tjligocki avatar tjligocki-lbl avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar

busy-beaver's Issues

Limited_Diff_Rules and 0^inf

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:

  • 34 A> 2 -> 034 A>

but, the way the proof system works, it is actually proving:

  • 0^inf 34 A> 2^k+1 0^inf -> 0^inf 34 A> 2^k 0^inf

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.

Machine to handle

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:

  • 1 + 2^1 = 3
  • 1 + 2^1 + 2^2 = 7
  • 1 + 2^1 + 2^2 + 2^3 = 15
  • 1 + 2^1 + 2^2 + 2^3 + 2^4= 31
  • ...

This is one of the few Christmas tree-like machines left unhandled among the short categories. All the rest are counters.

Recursive Proof Bug

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 ...

Can't verify BB(6) champion

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?

Exp int exception

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.

CTL filter results

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?

stripped_info is expensive

I profiled Quick Sim running over a list of programs for 10,000 loops.

profile

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.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.