4 ms·
I'd love to see what you come up with! Here are lots of CL terms you can use: http://share.begriffsschrift.com/joe/bank-17.txt.bz2 http://share.begriffsschrift.
by begriffs 15y ago
I'd love to see what you come up with! Here are lots of CL terms you can use:
http://share.begriffsschrift.com/joe/bank-17.txt.bz2 http://share.begriffsschrift.com/joe/bank-17.txt.bz2
It is a tab delimited file. The first column is all CL terms of length 17 which reduce to a normal form. The second column is what they reduce to, and the last column is the number of reduction steps it took in a leftmost-outermost evaluation order.
- viraptor 15y agoI'm not sure how comparable it is to your program since I cannot run it in batch mode (memory leaking...), but I'm able to process the first 340k rows of that file in under 7 seconds with cache limited to 15 characters. That makes 20 microseconds per row (with checking the result). Or another way - 7 microseconds per reduction step on average. Without cache, it takes minutes, so I didn't want to wait for the actual time. See http://imgur.com/FL2Eg http://imgur.com/FL2Eg for seconds per row -vs- cache limit. Ah... written in python without using the bit-packing tricks. I guess the 100+ times speedup is enough anyways... https://bitbucket.org/viraptor/ski/src https://bitbucket.org/viraptor/ski/src
- begriffs 15y agoNicely done, and good analysis. It's a fascinating problem, isn't it? Simple rules, but an opportunity to approach it several ways and refine the solution.