Three announcements
(-3) Bonus Announcement of May 30: As a joint effort by Yuri Matiyasevich, Stefan O’Rear, and myself, and using the Not-Quite-Laconic language that Stefan adapted from Adam Yedidia’s Laconic, we now have a 744-state TM that halts iff there’s a counterexample to the Riemann Hypothesis.
(-2) Today’s Bonus Announcement: Stefan O’Rear says that his Turing machine to search for contradictions in ZFC is now down to 1919 states. If verified, this is an important milestone: our upper bound on the number of Busy Beaver values that are knowable in standard mathematics is now less than the number of years since the birth of Christ (indeed, even since the generally-accepted dates for the writing of the Gospels).
Stefan also says that his Not-Quite-Laconic system has yielded a 1008-state Turing machine to search for counterexamples to the Riemann Hypothesis, improving on our 5372 states.
(-1) Another Bonus Announcement: Great news, everyone! Using a modified version of Adam Yedidia’s Laconic language (which he calls NQL, for Not Quite Laconic), Stefan O’Rear has now constructed a 5349-state Turing machine that directly searches for contradictions in ZFC (or rather in Metamath, which is known to be equivalent to ZFC), and whose behavior is therefore unprovable in ZFC, assuming ZFC is consistent. This, of course, improves on my and Adam’s state count by 2561 states—but it also fixes the technical issue with needing to assume a large cardinal axiom (SRP) in order to prove that the TM runs forever. Stefan promises further state reductions in the near future.
In other news, Adam has now verified the 43-state Turing machine by Jared S that halts iff there’s a counterexample to Goldbach’s Conjecture. The 27-state machine by code golf addict is still being verified.
(0) Bonus Announcement: I’ve had half a dozen “Ask Me Anything” sessions on this blog, but today I’m trying something different: a Q&A session on Quora. The way it works is that you vote for your favorite questions; then on Tuesday, I’ll start with the top-voted questions and keep going down the list until I get tired. Fire away! (And thanks to Shreyes Seshasai at Quora for suggesting this.)
(1) When you announce a new result, the worst that can happen is that the result turns out to be wrong, trivial, or already known. The best that can happen is that the result quickly becomes obsolete, as other people race to improve it. With my and Adam Yedidia’s work on small Turing machines that elude set theory, we seem to be heading for that best case. Stefan O’Rear wrote a not-quite-Laconic program that just searches directly for contradictions in a system equivalent to ZFC. If we could get his program to compile, it would likely yield a Turing machine with somewhere around 6,000-7,000 states whose behavior was independent of ZFC, and would also fix the technical problem with my and Adam’s machine Z, where one needed to assume a large-cardinal axiom called SRP to prove that Z runs forever. While it would require a redesign from the ground up, a 1,000-state machine whose behavior eludes ZFC also seems potentially within reach using Stefan’s ideas. Meanwhile, our 4,888-state machine for Goldbach’s conjecture seems to have been completely blown out of the water: first, a commenter named Jared S says he’s directly built a 73-state machine for Goldbach (now down to 43 states); second, a commenter named “code golf addict” claims to have improved on that with a mere 31 states (now down to 27 states). These machines are now publicly posted, but still await detailed verification.
(2) My good friend Jonah Sinick cofounded Signal Data Science, a data-science summer school that will be running for the second time this summer. They operate on an extremely interesting model, which I’m guessing might spread more widely: tuition is free, but you pay 10% of your first year’s salary after finding a job in the tech sector. He asked me to advertise them, so—here!
(3) I was sad to read the news that Uber and Lyft will be suspending all service in Austin, because the city passed an ordinance requiring their drivers to get fingerprint background checks, and imposing other regulations that Uber and Lyft argue are incompatible with their model of part-time drivers. The companies, of course, are also trying to send a clear message to other cities about what will happen if they don’t get the regulatory environment they want. To me, the truth of the matter is that Uber/Lyft are like the web, Google, or smartphones: clear, once-per-decade quality-of-life advances that you try once, and then no longer understand how you survived without. So if Austin wants to maintain a reputation as a serious, modern city, it has no choice but to figure out some way to bring these companies back to the negotiating table. On the other hand, I’d also say to Uber and Lyft that, even if they needed to raise fares to taxi levels to comply with the new regulations, I expect they’d still do a brisk business!
For me, the “value proposition” of Uber has almost nothing to do with the lower fares, even though they’re lower. For me, it’s simply about being able to get from one place to another without needing to drive and park, and also without needing desperately to explain where you are, over and over, to a taxi dispatcher who sounds angry that you called and who doesn’t understand you because of a combination of language barriers and poor cellphone reception and your own inability to articulate your location. And then wondering when and if your taxi will ever show up, because the dispatcher couldn’t promise a specific time, or hung up on you before you could ask them. And then embarking on a second struggle, to explain to the driver where you’re going, or at least convince them to follow the Google Maps directions. And then dealing with the fact that the driver has no change, you only have twenties and fifties, and their little machine that prints receipts is out of paper so you can’t submit your trip for reimbursement either.
So yes, I really hope Uber, Lyft, and the city of Austin manage to sort this out before Dana and I move there! On the other hand, I should say that there’s another part of the new ordinance—namely, requiring Uber and Lyft cars to be labeled—that strikes me as an unalloyed good. For if there’s one way in which Uber is less convenient than taxis, it’s that you can never figure out which car is your Uber, among all the cars stopping or slowing down near you that look vaguely like the one in the app.
Follow
Comment #1 May 9th, 2016 at 5:58 pm
I would happily pay more for an Uber than a taxi. Having pickup/dropoff location and payment managed by the app is so convenient. (Also no fumbling around with tips.)
However, I think the pricing of Uber is not set to compete with taxis; it’s set to compete with public transport. My “marginal” uber trip is when I have a choice between 10 minutes in an Uber for $10 versus 40 minutes walking/waiting/bussing for $3.
Comment #2 May 9th, 2016 at 6:00 pm
From what I understand, the original data science training program, Insight Data Science, is free for students (and funded by a set of sponsoring companies, who get first dibs on hiring said students). Why would anyone join the Signal Data Science program and agree to pay 10% of their salary (~$12-15k at 2016-salary levels) when they can get a better education and stronger network for free? Is it because IDS is only for people with Ph.D.’s, so SDS is going to target non-Ph.D.’s?
Comment #3 May 9th, 2016 at 6:23 pm
Can you expand on why Uber, Lyft, etc., should not have to follow the same rules that traditional taxi cab companies do?
Comment #4 May 9th, 2016 at 6:47 pm
The fact that the advantage of Uber and Lyft is largely about convenience and not just about being a cheaper option is really brought home by their impact on the rental car business:
http://www.bloomberg.com/news/articles/2016-04-21/uber-overtakes-rental-cars-among-business-travelers
Comment #5 May 9th, 2016 at 7:15 pm
Re Uber, it’s actually the cheaper price that makes the whole Uber experience worthwhile and great. Not to undermine the other obvious advantages you mentioned, of course.
But there’s one con to uber: you always have to wait, it’s not like a taxi that you can spontaneously stop it in the street.
Comment #6 May 9th, 2016 at 8:11 pm
Raoul #3:
Can you expand on why Uber, Lyft, etc., should not have to follow the same rules that traditional taxi cab companies do?
I never actually wrote that they shouldn’t have to! I could easily believe that the truth is split: that some taxi regulations are genuinely important, and should be applied to Uber/Lyft even if they cause fares to go up; while others served only to help the taxi companies maintain a cartel, and Uber and Lyft’s success helps demonstrate their superfluity.
The one thing I’m certain about is that I hope cities like Austin manage to reach agreements with Uber and Lyft—because if they don’t, then that’s a serious degradation in quality of life for everyone like me, not to mention all the drivers who are now suddenly without their income source.
Of course, the other solution from my standpoint would be if the taxi companies “moved in an Uber direction,” and let you arrange rides and pay for them with a smartphone app. But without any competition from Uber or Lyft, I don’t see why they’d have an incentive to improve their service in that way.
Comment #7 May 9th, 2016 at 9:20 pm
Joe #2:
I’m Jonah Sinick, cofounder of Signal Data Science. Signal has pros and cons relative to other programs. Insight Data Science is more tried and true, and is prima facie a better financial deal for PhDs, but Signal is still plausibly a better option for some:
We serve a more diverse population. Insight is selective to the point of being able to boast 100% placement rate. We think that there are a lot of people who have very strong chances of getting data science jobs who are not presently being served. This is especially true of non-PhDs, but also of PhDs of nontraditional backgrounds as well as PhDs whose current personal presentation skills are less polished.
We offer an extraordinary peer group: Because we don’t restrict ourselves to PhDs, we’re able to offer a peer group of significantly higher intellectual caliber than is typical of science PhDs (including veteran software engineers who are transitioning to data science, and exceptionally gifted recent college grads). I did a PhD in math, and the intellectual vibrancy of the environment here comes close to being without parallel in my academic experience.
We start sooner: Insight Data Science lists the next cohort that they’re accepting applications as [starting* in September 6, a couple of weeks after our next cohort will finish. So students who attend our next cohort have prospects for getting jobs sooner than students who attend Insight Data Science’s next cohort.
Feel free to drop us a line if you have more questions!
Comment #8 May 9th, 2016 at 10:40 pm
There is at least one competitor to Uber and Lyft in Austin which is still available: GetMe (getme.com). Apparently they’ve been complying with the extra background check and fingerprint requirements all along, so they’re still operating. Haven’t tried them yet myself, but I hear they’re a perfectly acceptable alternative.
Comment #9 May 9th, 2016 at 10:54 pm
the paul #8: Thanks! Will try when I’m there.
Comment #10 May 10th, 2016 at 12:13 am
Well, Scott, it looks like you’ll have to buy a pick-up truck.
Comment #11 May 10th, 2016 at 1:42 am
I claim, which equally strong evidence, that this is the hash of a 10 state Goldbach Turing machine:
5cebf541ae783c67b3565be8ec0e48f29e41dbf0c7a84269207db84ca28f7259
Comment #12 May 10th, 2016 at 4:55 am
Hi Scott, suppose that:
1. The 31 states Turing Machine designed by “code golf addict” turns out to be correct.
2. Someone furnishes a proof that BB( k ) is computable, for some k > 30.
If I’m not mistaken, the combination of these 2 facts would constitute a proof that the Goldbach conjecture can be either proved or refuted (i.e. it is not independent of ZFC).
Comment #13 May 10th, 2016 at 6:52 am
Giorgio #12: Yup! But maybe a better way to say it is that nobody will do what you mention without Goldbach being solved first.
Comment #14 May 10th, 2016 at 6:57 am
ninguem #10: LOL! I do plan to take up bicycling again when I’m there—but will have to look into a gun rack and “bike nuts” for my bicycle.
Comment #15 May 10th, 2016 at 7:36 am
What are the known (or easily provable) lower bounds on the number of Turing machine states for encoding the problems you mentioned?
Comment #16 May 10th, 2016 at 7:52 am
PX #15: For Con(ZFC), all we know is that at least 5 states are needed.
For RH and Goldbach, if those statements are ever proven, there will then be a 1-state machine “encoding” them: namely, a machine that just goes into a trivial infinite loop, representing the fact that the statements are now known to be true!
Comment #17 May 10th, 2016 at 7:59 am
Scott #13: 🙂 I have to recognize that expecting a proof of the computability of BB( k > 30 ), when our exact knowledge stops at BB( 4 ), can be regarded as a further definition of utopia.
Comment #18 May 10th, 2016 at 8:58 am
The things that people object to about Uber are actually quite interesting and complicated.
Fundamentally, 25% (or whatever it is in your area) of the salary of many thousands of people from all over the world is going to one business HQ’ed in San Francisco even though they are not employees of that company. The salaries of taxi drivers are plummeting and local businesses are collapsing in its wake. It’s hard to predict exactly what the consequences will be but it does look a little like a new feudal system with robot overlords with Californian accents.
This article was written before the Uberization of the planet but it is generally on a similar theme http://www.nytimes.com/2012/12/10/opinion/krugman-robots-and-robber-barons.html?_r=0 .
Comment #19 May 10th, 2016 at 9:07 am
Scott #13
So, if I understand correctly, no computable function f(n) can possibly grow faster than BB(n).
But do we know what’s the “slowest” growing non-computable function? (not sure the question even makes sense.. it still would have to grow to infinity).
How slow can it get compared to the fastest growing computable functions?
Is big O() notation still useful to express all this?
Comment #20 May 10th, 2016 at 12:47 pm
irt. fred #19:
I think I have an idea for this one: BB^(-1)(n) where the ^(-1) is not 1/(), but “inverse”- as in, if m = BB^(-1)(n), then n = BB(m).
With the BB(n) being a function on integers, and growing very quickly, there will be many numbers for which BB^(-1) isn’t defined. But nevermind, let’s abuse the notation a little. It’s been done before– the complexity of the Tarjan set-union algorithm is expressed in terms of the inverse Ackermann function.
Cheers.
Comment #21 May 10th, 2016 at 1:00 pm
fred #19: Yes, as BLANDCorporatio (?) said, given any fast-growing function you want, you can just take the inverse of it to get a comparably slowly-growing function.
If you instead meant: what’s the slowest-growing function that nevertheless grows faster than all computable functions, there won’t be a single one (growth rates are not well-ordered), but there definitely will be ones that grow much more slowly than Busy Beaver (that can be proved using a diagonalization argument).
And yes, you can use O-notation for all of this, but it’s not especially useful, since for the sorts of functions we’re talking about f(n)=o(g(n)) tends to be a wild understatement—if g dominates f at all, then it probably just blows it out of the water.
Comment #22 May 10th, 2016 at 1:44 pm
@fred #13
Well, there are uncomputable functions that only take the values 0 or 1. But I assume you mean uncomputable functions that eventually outgrow every computable function. Call such functions BIG.
Let f(1,n), f(2,n), … be an enumeration of computable functions. Then you can define a BIG function F(n) as the maximum of f(1,n), f(2,n), …, f(a(n), n), where a(n) is some extremely slow-growing function of n.
Every BIG function is at least as large of a function of the above form (exercise for the reader?)
Comment #23 May 10th, 2016 at 1:51 pm
fred #19: You can for example let f(n)=BB(alpha(n)), where alpha is the inverse of the Ackermann function. Or instead of alpha you can take the inverse of an even faster-growing computable function. Then f(n) will grow faster than any computable function, though slower than BB(n).
Comment #24 May 10th, 2016 at 1:53 pm
Spitball idea: As far as I can tell, upper-bounding BB(k) is just about as good as finding BB(k) itself, correct?
So seems to be it should be kind-of-easier to find upper bounds for BB(k) (at least where it is possible). For example, proving somehow that it would be impossible to represent the steps needed to compute Ack(5000) with just 6 symbols, and thus BB(6) < Ack(5000)?
(Waving hands wildly…)
Comment #25 May 10th, 2016 at 1:59 pm
On Uber, a compilation of readings:
“It did not take technology to spur the on-demand economy. It took masses of poor people.
The notion that brilliant young programmers are forging a newfangled “instant gratification” economy is a falsehood. Instead, it is a rerun of the oldest sort of business: middlemen insinuating themselves between buyers and sellers.
All that modern technology has done is make it easier, through omnipresent smartphones, to amass a fleet of increasingly desperate jobseekers eager to take whatever work they can get.”
http://qz.com/312537/the-secret-to-the-uber-economy-is-wealth-inequality/
“This is the Amazon move: absolute obfuscation of labor and logistics behind a friendly buy button. The experience for a customer is super convenient, almost magical; the experience for a courier or driver or warehouse picker…? We don’t know. We don’t get to know. We’re just here to press the button.”
http://www.theatlantic.com/technology/archive/2015/11/the-food-delivery-start-up-you-havent-heard-of/414540/
https://www.policyalternatives.ca/publications/monitor/apploitation-city-instaserfs
http://citypaper.net/uberdriver/
This is by a journalist who worked as an Uber driver, with the numbers on how much they can actually earn.
Certainly the Uber experience for the customer is good. The experience for the driver, and for the cities, is in general not.
Comment #26 May 10th, 2016 at 3:03 pm
Gabriel #23: Right, but something even stronger is true: one can design functions f that grow faster than any computable function, but such that an oracle for f would not give you the ability to solve the halting problem (as an oracle for BB(n) or BB(α(n)) would). Andy Drucker showed how to do that in some long-ago Shtetl-Optimized comment section (anyone want to dig it up? 🙂 )
Comment #27 May 10th, 2016 at 3:06 pm
Dave #24:
As far as I can tell, upper-bounding BB(k) is just about as good as finding BB(k) itself, correct?
The two things are precisely equivalent. If you knew an upper bound U on BB(k), you’d just run all the k-state Turing machines until each of them had either halted or else run for more than U steps, and then you’d know BB(k) precisely.
This means, in particular, that upper-bounding BB(k) is “no easier” than determining it outright.
Comment #28 May 10th, 2016 at 3:16 pm
Doug K. #25: I’d have an easier time taking those sorts of arguments against Uber and Amazon seriously, if they didn’t seem like completely general arguments against a market economy and the specialization of labor! A few miscellaneous comments:
– Did the writers of these thinkpieces actually ask any Uber drivers, or Amazon warehouse workers, whether they preferred to continue doing their jobs or to be laid off (as just happened to thousands of drivers in Austin)?
– Quite plausibly the workers would want to continue at their jobs, but just make more money. I want that too! I’ve always supported strong minimum wage laws, and in the case of Uber/Lyft, could easily support a mandatory minimum fare that was higher than the market rate.
– FWIW, I’ve had conversations with Uber drivers who seemed anything but desperate—some even told me they didn’t really need the money, but were retirees who drove part-time just to get out the house and talk to people. (But, paradoxically, maybe the thinkpiece writers would rather I’d gotten a ride from a desperate person who needed the money?)
– I’ve already said that I’d happily pay standard taxi fares, if I could just order with my smartphone and thereby bypass the huge “noisy channel” and “uncertainty of arrival” problems outlined in my post. So for me at least, the argument in that QZ piece that the technology is irrelevant is the complete opposite of the truth.
Comment #29 May 10th, 2016 at 4:33 pm
But there are taxi companies here that support ordering taxis with a smartphone app, for the people who want that. And there also are taxi companies that let you pay with a bank card on a POS terminal in the taxi. I think there’s even intersection of the two, and I think both of those have appeared a year or two before Uber launched here. If those things don’t exist in the U. S., then you just gave me another part of the explanation why Uber is so popular there. (There’s lots of other obvious parts of the explanation too, like how public transport is bad or non-existant in most of the cities in the U. S.)
Comment #30 May 10th, 2016 at 5:58 pm
Business and everything else is evolving much faster than the ability of society and civilization to deal with, and regulate, it. This is not a good thing.
The taxi business and Uber are a good example.
Taxi services have no doubt been around for thousands of years. During this time, many governments have regulated taxis. There are many reasons for this. No doubt some big players have bribed the powers that be to enact regulations to curtail competition; and so on. Other regulations are a response to certain down sides to free-for-all taxi operations — robbery, rape, kidnapping, murder, and similar sordid stuff.
So in most places taxis are regulated, with rules good, bad, and so-so. I would guess that background checks and fingerprinting of drivers is common and a good idea. Furthermore, this kind of job is usually unionized, with another set of good and bad aspects.
There is no doubt that taxi service can be greatly improved by business models like Uber, and there should be plenty of money to be made by playing within the existing rules and out competing the old guard.
But — Oh, No!! — Uber is an “on line business”, which means they do not expect to have to follow any rules. Unions and prevailing wages? Screw that! With computer power to orchestrate things, everyone can be an independent contractor, and fight to work for the lowest wage.
How about city regulations, licences, fees, taxes, background checks? But they are different everywhere! Uber’s computers are not smart enough to deal with that! What about all the people involved in taxi companies playing by the rules? Tough luck, suckers.
And for this contribution, Uber is making how much money? Did Dorthy say 25% of all fares?
Comment #31 May 10th, 2016 at 7:15 pm
Liberty Cab in and around Buffalo, NY has a phone app for curb-side use and a website for automated online reservations. Its taxis take credit cards and use a GPS system for directions. It also accepts Medicaid for doctor visits. I’ll bet a modest amount that Austin Taxi companies are similar. Why not?
I’ve never owned a car, and there isn’t much public transportation here in Orchard Park so when I need to go somewhere that’s not in a five-mile radius but not far enough to warrant renting a car I use Liberty, and have never had a problem with them. It seems expensive – about $50 for a 25-mile trip, but the cab drivers seem to really need the money.
Comment #32 May 10th, 2016 at 11:28 pm
Re : a function that grows uncomputably fast (a BIG function), but much slower than BB(n).
A function that, I think (I might be wrong) should eventually surpass any computable function, yet be slower than BB(f(n)) for any computable f, would be:
Q(n) := BB( (BB^(-1)(n)) + 1 )
Where (BB^(-1)(n)) is the least number m such that BB(m) >= n .
A better definition might be to make it so that the function is strictly increasing instead of being constant most of the time, but the important bit is that Q(BB(n)) := BB(n+1)
Q is not computable because iterating it n-1 times starting with BB(1) yields BB(n), and iterating something computable n times is computable.
I think it also surpasses any computable function because , if any computable function surpassed it, then iterating that function would give larger results than iterating it, and would therefore give an upper bound for BB(n) , which is not computable.
So it should eventually surpass any computable function.
Further, it should be slower than BB(f(n)) for any computable f , because BB^(-1)(n) is incomputably slow growing.
Of course, it can still be made “even slower” while still surpassing any computable function by applying the same process to Q that was done to BB to produce Q.
(The specifics might need some modifications though).
I would think that this would give rise to a hierarchy of BIG functions that grow increasing slowly. I’m not sure how to make the hierarchy go past just iterating the process some number of times though.
I’m not sure how to make it go to omega on the hierarchy without making it not be usable to get BB(n).
Please tell me if I made errors in this reasoning.
Comment #33 May 11th, 2016 at 1:04 am
I posted a link for Goldbach testing programs of 27 and 31 states in the last thread, but probably no one read that far down, so here it is again:
https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6
Comment #34 May 11th, 2016 at 5:59 am
Raoul #30 Uber takes 25% now in London UK and slightly less in other places I believe. See https://www.theguardian.com/business/2015/nov/12/uber-drivers-protest-at-fee-hike-in-first-london-demo .
Scott #28. I don’t think the complaints are completely generic. They are specific to a sort of revolution in the labor marketplace that Uber has pioneered. Of course there are similarities to other parts of the labor force but that doesn’t make it the same. Specifics matter.
However back on the slightly generic front, there are serious problems with global capitalism and in particular the tax system that companies like Uber, Google and Amazon are exposing in dramatic fashion. These companies pay hardly any tax in the countries where by any normal interpretation they do a huge amount of their business. The tax system as we have it simply wasn’t set up with these modern globalised business models in mind.
Comment #35 May 11th, 2016 at 7:55 am
dorothy #34:
These companies pay hardly any tax in the countries where by any normal interpretation they do a huge amount of their business. The tax system as we have it simply wasn’t set up with these modern globalised business models in mind.
I don’t know the facts well enough, but if true, that strikes me as a perfect example of a good argument against Uber, Amazon, etc.—one that engages the specifics and immediately suggests possible remedies—as opposed to the arguments quoted by Doug K. #25, which are just about shaming the people who use these services (presumably most of us?) as complacent bourgeoisie.
Incidentally, are you the same Dorothy from the discussion with Amy? If so, welcome back.
Comment #36 May 11th, 2016 at 8:34 am
New extensions of economic analysis indeed are “completely general”, in that older economic models founded upon the notion that “economies are created by rational actors whose self-interested choices generate efficient markets” are being extended, and arguably even supplanted, by post-rational models of human cognition and economic choice.
For economic details, see for example the recent survey by Alan Kirman and Miriam Teschl “Selfish or selfless? The role of empathy in economics” (Phil Trans Roy Soc B, 2010).
Medical research affirms crucial roles for post-rational cognition in human social existence; see for example Watanabe et al. “Clinical and neural effects of six-week administration of oxytocin on core symptoms of autism” (2015).
The on-line rationalist community too is beginning to grapple with these extended models of human cognition and behavior; see for example David Chapman’s recent Meaningness weblog essay “A bridge to meta-rationality vs. civilizational collapse” (of April 26, 2016).
Observation Chapman’s essay effectively critiques some of weakest post-rational STEM literature, but shies from grappling directly with the implications of the strongest post-rational STEM literature. Still it is fun to see Chapman praising the late works of Michel Foucault!
Conclusion If to a considerable extent it has turned out that “game theory is for doing theory, not for playing games” (as Reinhard Selten has said), than similarly it may turn out that “rationality is for winning arguments, not for living rationally”.
Questions Does this mean that the classical literature of economics and rationality is destined be substantially rewritten, and in the process greatly extended? After all, the literature of classical physics received new quantum foundations — and thereby found extended applications — so shouldn’t we expect to witness comparable post-classical transformations in the study of economics and rationality?
Comment #37 May 11th, 2016 at 11:34 am
code golf addict #33
Thanks for the link. I was looking for this earlier and had a hard time finding it in the previous thread.
Comment #38 May 11th, 2016 at 12:03 pm
WIth three topics you get comments on all three and reading through them is… surreal. I’ll comment briefly on all three
1) Removing the Large Cardinal hypothesis. Actually I rather liked that a concrete statement seemed to need an LC hypothesis. Oh well.
2) Data Science- very interesting business model!
3) Uber- I thought that Uber/Lyft would force Taxi companies to improve their service to compete. NOT their prices, which perhaps they can’t improve, but their service. I still don’t know why this hasn’t happened.
I’ve heard that Uber does not want to label as such since then Cab drivers may vandalize their cars.
Comment #39 May 11th, 2016 at 1:04 pm
code golf addict #33: Thanks so much, and sorry for missing the link earlier!!
Comment #40 May 11th, 2016 at 1:59 pm
gasarch #38, simply because of scalability. Software enables scalability that “hard business” aren’t even able to embrace, they don’t have the mindset/flexibility necessary. They have been doing business locally for decades… A company that scales will have a better software and particularly *data* to such a point the local business won’t be able to compete with…
Comment #41 May 11th, 2016 at 2:47 pm
(1) Something almost worse than the worst case: New Scientist write a piece explaining the result while getting almost everything wrong:
https://www.newscientist.com/article/2087845-this-turing-machine-should-run-forever-unless-maths-is-wrong/?utm_source=NSNS&utm_medium=SOC&utm_campaign=hoot&cmpid=SOC|NSNS|2016-GLOBAL-hoot
Comment #42 May 11th, 2016 at 3:33 pm
#35 “[…]which are just about shaming the people who use these services (presumably most of us?) as complacent bourgeoisie.”
To be fair, my assumption is also that most of us are indeed both complacent and bourgeois. I could be wrong about one of those 🙂
About Uber again, the problem really isn’t only tax. Imagine if much of the economy of country X took this same form. That is the population of economy X mostly pay 25% of their salary to some company in California (which pays almost no tax within Xistan), all these workers within Xistan are on a minimal salary with none of them in senior or even middle ranked positions in the company, those workers have next to no workers’ right as their government won’t regulate as they live in fear of the jobs disappearing, their government has no real influence over the company as the company is too big to challenge and in any case is backed by the US government in trade talks, the only way to setup a competing business is a multi-billion pound capital expenditure which people in Xistan simply don’t have.
This is a significant triumph of capital over labor which is not necessarily a good thing.
And… yes it is the same me.
Comment #43 May 11th, 2016 at 6:25 pm
This statement (which is accurate as far as it goes) expands naturally to
It is interesting that David Foster Wallace’s later essays (which recent Shtetl Optimized comments have mentioned) reflect both propositions.
Wallace’s article “Rhetoric and the math melodrama” (Science 2000) describes mathematics as a intrinsically “hard business” (compatibly with the viewpoint of comment #38).
In opposition, Wallace’s subsequent speech “This is water” (Kenyon College Commencement Speech, 2005) concisely summarizes and vigorously advocates (what amounts to) the post-rational faith-and-practice tenets of the Peace Churches (during the previous decade Wallace had been intermittently a Mennonite “attendee”, as they are called).
Search engines readily find both Wallace’s 2000 article and his 2005 speech. It is greatly to be regretted (as it seems to me), and mighty sobering too, that David Foster Wallace never achieved a personal synthesis of the points-of-view that his two works present.
Conclusion Grappling with these tough issues requires all of the rationality that we can muster, and all of the humanity too.
Comment #44 May 12th, 2016 at 2:34 am
drdeca #32: I think you are right. Your function Q is uncomputable and yet slower-growing than the function I mentioned in #23. However, the function Scott mentions in #26 would be even slower-growing, because an oracle for your Q *would* allow you to solve the halting problem.
By the way, your technique is interesting. Suppose we apply it to Ackermann’s function A(n), and we let f(n) = A(1+alpha(n)). Then f(n) is like taking one “step” back from A. Meaning, if A is called A_omega, where omega is the first infinite ordinal, then f could be called “A_{omega-1}”.
Comment #45 May 12th, 2016 at 10:31 am
Here is a detailed write-up of my 73-state Goldbach TM, which I’ve reduced to 47 states but which has nonetheless beaten soundly by code golf addict. Goldbach 47 Gist This is well-tested (it can print Goldbach sums very fast, and if 7 is artificially treated as composite, it halts on N=12) and carefully explained, but not formally proven.
My high-level algorithm is, for each N:
1. Perform the sieve of Eratosthenes on an array from 1 to N-2, inclusive. Each element of the arrays is a data/mark pair of cells on the tape. The data cells hold the primality, and the markers allow the TM to keep track of what it’s doing.
2. Simultaneously move a pair of markers inward, checking the primality of each pair from (2,N-2) to (N/2,N/2). If any of these pairs are both prime, add 2 to N and start over. Otherwise, halt.
I haven’t verified code golf addict’s solution yet, but the description is sound and I would expect it to need significantly fewer states than mine by virtue of not operating on pairs of cells. The core unary primality test is similar enough to “filtering” phase of my sieve that I make this judgment with confidence. Nonetheless, I did not make the leap until I saw addict’s solution, so I happily concede.
Geoffrey Irving #11: You can download goldbach73.c from the Gist above and verify that I posted its SHA-256 sum a week ago. Obviously that post wasn’t supposed to prove anything by itself. What you didn’t see is that I’d e-mailed the file to Scott, so he wasn’t operating on blind faith.
Comment #46 May 12th, 2016 at 3:26 pm
Jared S #45:
Also, I noticed that the sha256 from Geoffrey Irving #11 is
$ echo “Yo.” | sha256sum
5cebf541ae783c67b3565be8ec0e48f29e41dbf0c7a84269207db84ca28f7259
I think some of the people here miss the point of the code golf. The hash is merely a timestamp, and of course the proof will be revealed at the end, but it ruins the fun to see other people’s solutions before that.
code golf #33:
Thanks for sharing! I wonder what other CS questions which would be interesting with code golf.
Comment #47 May 12th, 2016 at 7:13 pm
Curious Nerd #46: Wow, do you have a SHA-256 rainbow table? haha
Comment #48 May 12th, 2016 at 11:40 pm
Scott, Adam Bravo!!!
Today, I IMed a colleague (working in quantitve finance, he has a PhD degree in physics but does options volatilty research) in company chat.
– You know about Busy Beavers, right?
– No
– Well then you should google it and read about it! There’s this recent breakthrough that shows that there exists a not so large table of a few thousand columns only (and perhaps much smaller – maybe just a few 10s) that encodes simple behavior eluding the ability to reason about it not just practically, but theoretically! (link included to your blog post and the wikipedia article of busy beavers with the TM tables)
(half an hour later said colleague stops by my desk)
– after reading and learning about this, I feel like retiring and devoting my time to studying the behavior of Turing Machines
😀
followed by some blabber/chat/jokes with another colleague how the least N for which BB(N) is unknowable might be related to some fundamental boundary/constant for things that can be “predicted” and things that cannot be with vague references to what minimum “complexity” does a system require to have “free will”, or minimum complexity of something that can be considered “alive” etc etc. (not that there is any real relationship, just laymen musing)
in short – ruined productivity 😀
Comment #49 May 13th, 2016 at 2:22 am
Scott #28:
Long time reader, first time commenter here. Your support for minimum wage laws (or minimum fare laws) greatly surprised me given the model that I had built of your views from many years of reading your blog and comments. That this view was based on the idea that such laws would just enable those workers to make more money struck me as very simplistic.
A surprise is an opportunity to learn and change one’s mind. So in that spirit, would you elaborate a bit more on why you are persuaded of that view? Or link to something on the issue that you find pretty compelling? I’m sure you’re aware of standard econ 101 counter-arguments to minimum wages and price controls. I’m curious why you don’t find them compelling. Most arguments in favor of minimum wage laws (except monopsony in labor markets) strike me as largely general arguments against market economies. And low-wage/unskilled labor markets, precisely the ones that minimum wage laws are meant to affect, don’t seem monopsonistic to me.
Comment #50 May 13th, 2016 at 7:42 am
RP #49: I think these questions are messy and empirical rather than a-priori. I.e., yes, there’s clearly some amount to which we could raise the minimum wage that would cause unacceptably-large unemployment. But right now, the US has a minimum wage high enough to have forced many jobs overseas, but it also has 5.5% unemployment, which is reasonable. It will be interesting to see what happens if Hillary gets elected and manages to pass a $12-$15 minimum wage.
There are the constraints of the market economy, and then there’s also the constraint that people who work full-time shouldn’t be starving and unable to feed their families. And aside from compassion for those people, there’s also the empirical observation that, if enough people are starving, they’ll violently revolt, and then what happens to the assumptions of Econ 101?
Having said that, it’s possible that if I thought it through enough, I would support a Universal Basic Income, as many of my rationalist friends do. (Or rather: a basic income conditional on the person working if physically and mentally able to, and receiving a nominal co-payment from their employer?) A direct transfer of wealth to poor people certainly seems simpler than the whole constellation of policies—welfare, food stamps, minimum wage, Medicaid, etc.—currently used to achieve some of the same ends.
But in the contemporary US, where a universal basic income is outside the realm of political possibility (not even Bernie Sanders suggested one), a minimum wage that it’s possible to live on seems important for maintaining a stable market economy.
Comment #51 May 13th, 2016 at 7:46 am
Scott: I’m a bit afraid of this quora thing. If the questions go on a popularity poll, then we’ll just get answers on those questions that may be important but not very original, so either you can’t give good answers to them, or you’ve already given good answers to them in previous articles. For example, “What is quantum computing in layman’s terms?” is one of the higher voted questions currently. I hope at least you’ll be able to skip those sorts of questions quickly by linking to an earlier article. I’d be more interested in unique and original questions that only one reader asks.
Comment #52 May 13th, 2016 at 8:52 am
jonas #51: Yeah, I’ve noticed that a lot of the highest-voted questions are things we’ve already tackled BB(7910) times on this blog. Don’t worry—for those questions, my answer will indeed consist mainly of links to where I’ve answered the question previously.
Comment #53 May 13th, 2016 at 1:03 pm
If people frequently ask you the same questions, maybe you should write a…
Comment #54 May 13th, 2016 at 3:38 pm
Gabriel Nivasch #44
Thank you for your response!
Can you tell me if I understood your point about A_omega-1 ?
So, you were saying that, because A(n) is roughly the same as f_omega in the fast growing hierarchy, and in the fast growing hierarchy, the next function is the current one iterated the input number of times, and the process I described is sort of the opposite of doing that, doing it to the Ackerman function would be like taking the “previous” value for it?
That sounds interesting. Do you think that, with iterating the process to get functions for omega-2, omega-3, etc. could be used to get some function which could be considered to have index omega/2 like in the surreal numbers, with omega/2 being greater than 1,2,3,… And less than omega-1,omega-2,… , so getting a function which would still be faster than primitive recursive functions, but slower than any f_omega-1, f_omega-2, …?
(I also looked at applying the f(f^-1(n)+1) thing to functions that grow relatively slowly, to get a feel of how many iterations it takes for it to get to something ~n+1 , for how fast they get slower.
n^c (for example) does immediately, e^n gives e*n , e^e^n gives , unless I made an error, e^(ln^e(n)), which in turn gives something which is Theta(n), which then gives something ~n+1 , so only 3 steps.
)
Again, thanks
Comment #55 May 14th, 2016 at 8:13 pm
Scott:
Alright, the upper bound to ZF-provable values of BB(k) is now 5349.
I now have a working version of my not-quite-Laconic compiler, (thank you for naming my language 🙂 ), using the BDD construction, and it works modestly better than the original:
$$ python3 nqlaconic.py –print-tm squaresaresmall.nql | wc -l
384
$$ python3 nqlaconic.py –print-tm goldbach.nql | wc -l
1145
$$ python3 nqlaconic.py –print-tm riemann.nql | wc -l
2681
$$ python3 nqlaconic.py –print-tm zf.nql | wc -l
5349
The construction hasn’t been optimized at all, so expect these numbers to continue to go down a bit.
An earlier version of the backend was tested with a hand-entered AST for squaresaresmall; no end-to-end correctness verification has been done yet (so the bound could theoretically go up as well 🙁 ).
Notable differences between NQL and Laconic:
• NQL does not support negative numbers. – clamps at zero.
• NQL implements only procs, not funcs; in other words your procedures are copied for every distinct combination of variables passed to them.
• NQL supports global variables which can be referenced from any function.
• NQL functions cannot be recursive (in other words, the call graph must be directed acyclic).
• NQL does not have any native support for lists (this is the only reason there is no “friedman.nql” above
• NQL presently distinguishes between numbers and booleans, and trying to mix them will cause an assertion fault
• NQL doesn’t require return statements
Comment #56 May 14th, 2016 at 8:17 pm
Let’s try that again with hopefully less broken formatting:
%% python3 nqlaconic.py –print-tm squaresaresmall.nql | wc -l
384
%% python3 nqlaconic.py –print-tm goldbach.nql | wc -l
1145
%% python3 nqlaconic.py –print-tm riemann.nql | wc -l
2681
%% python3 nqlaconic.py –print-tm zf.nql | wc -l
5349
Comment #57 May 14th, 2016 at 10:38 pm
Stefan O’Rear: To be clear, is your 5349-state program directly searching for contradictions in ZF? Or what?
Comment #58 May 15th, 2016 at 4:54 am
Scott #50, the nominal “unemployment rate” may be 5.5% or whatever, but the “labor non-participation rate” is much, much higher. (These are the people who have stopped looking for work, who think the jobs available are unacceptable to them, who claim various mental or physical disabilities, who are unemployable for various reasons (felons, uneducated, mental issues, work ethic issues).
Another way of looking at this is that 90 million or so Americans of working age (18-65) are NOT in the labor force.
The unemployment stats are misleading.
And remember, relatively fewer households now have one breadwinner and a non-working spouse, so the comparisons to the 1950s, 60s, and even the 70s are even more striking.
And since most of the income taxes are paid for by those in the top earning section (5%, 10%, 20%, as one wishes), that 90 million people of working age are collecting from the few who earn at the top is….disturbing.
People yammer about “income inequality” but this particular inequality has never been seen before. Certainly the Chinese and Soviet systems never tolerated having fully half of their working-age people watching t.v., eating Cheetos, and breeding while the highest earners paid most of the money to support them.
Comment #59 May 15th, 2016 at 12:41 pm
Scott: I think you’ve linked to the wrong thing in announcement -1; you’ve linked to Stefan’s comment #250 on the other thread, which doesn’t talk about this, instead of his comment #55 here, which does.
Stefan: Oops, I missed the github link which explains!
Questions regarding ways of getting it down further: Would it be possible to shrink it further by using collection instead of replacement, since collection is simpler to state? Or is the metamath version of replacement already actually collection? (I find the way metamath writes its axioms to be too hard to read; I honestly can’t tell.)
I was also wondering whether going for NBG might be shorter than ZFC, since it’s finitely axiomatizable, but it looks like the way that metamath handles axiom schemas means those aren’t actually too horrible and so doing this might actually make things worse?
Also, would you mind explaining just why you re-added foundation? Seeing as there’s no link to the list discussion. Thank you!
Comment #60 May 15th, 2016 at 1:47 pm
drdeca #54: How would you define f_{omega/2} given f_{omega-1}, f_{omega-2}, f_{omega-3}, …?
Comment #61 May 15th, 2016 at 3:45 pm
Sniffnoy #59: (gasp) Sorry, fixed now!
Comment #62 May 15th, 2016 at 4:32 pm
Sniffnoy #59: the discussion about the need for Foundation is here: https://groups.google.com/forum/#!topic/metamath/OumBq83Ksqs
Comment #63 May 15th, 2016 at 4:39 pm
Stefan O’Rear #56: Wow, awesome!
Also, I have gone through Jared’s comments on his Turing machine in detail, and verified its behavior! I confirm that Jared’s Turing machine does indeed halt if and only if Goldbach’s conjecture is false. Congratulations, Jared!
I’ve been having a bit more trouble understanding code golf addict’s solution–addict, let me know by email if you’d like me to put effort into verifying your solution, in which case I’ll start asking you questions.
Comment #64 May 15th, 2016 at 6:57 pm
I do not understand. A turing machine is a program. How about this?
n=2;
While(iscounterexampletoGoldbach(++n) );
Assume iscounterexampletoGoldbach(++n) returns 1 if not a counter example else 0.
I have a two line code. How does this correspond to number of states?
Comment #65 May 15th, 2016 at 7:03 pm
@Stefan #55 congratulations! Any chance of seeing what the list of actual TM states is, à la the appendix in the paper of Scott and Adam?
Comment #66 May 15th, 2016 at 7:04 pm
4th attempt. sending this without links or blockquotes. Hail Mary.
Sniffnoy #59:
(I lost the first version of this reply)
Would it be possible to shrink it further by using collection instead of replacement, since collection is simpler to state?
Maybe? The Metamath version of the collection principle is shorter than its axiom of replacement; but you’ll notice we don’t have Separation in our list, because it can be derived from Replacement, but unless I’m missing something you can’t do that with Collection and we’d need to re-add Separation.
So far I’ve been focusing on compiler improvements. I’d hoped to get down to 1000 states with no substantive changes to zf.nql itself (as I told Scott in an email earlier), but I greatly underestimated the state budget for jumps, and I’m already hitting diminishing returns on optimizations. Current scores are 432 states for Goldbach, 1008 for RH, and 1929 for Con(ZF). Only one of these reaches Scott’s objectives.
Or is the metamath version of replacement already actually collection?
It’s not.
I find the way metamath writes its axioms to be too hard to read; I honestly can’t tell.
Are you talking about the RPN garbage in zf.nql or the infix version in the actual database and the website? If the former, I completely agree, if the latter I’m curious what changes you’d make.
I was also wondering whether going for NBG might be shorter than ZFC, since it’s finitely axiomatizable, but it looks like the way that metamath handles axiom schemas means those aren’t actually too horrible and so doing this might actually make things worse?
Yeah, I don’t think that’d help — one scheme is simpler than N (10?) Gödel operators. This is a systems perspective: we already need schemes to support propositional and predicate axioms in a Hilbert-style formalism, so we might as well keep using them for set theory.
Also, would you mind explaining just why you re-added foundation?
Metamath’s basic axiom of infinity (ax-inf) asserts the existence of a non-empty set y such that for each element z, y contains another element that contains z. In other words, y has no rank-maximal element. If you have Foundation, that forces y to be infinite, which means it has subsets of every finite cardinality, which gives you omega by replacement. If you don’t have Foundation … y could just be a Quine atom and you’ve achieved nothing.
There’s another version (ax-inf2) which directly asserts the existence of (a superset of) omega and stands without Foundation; we can try that later.
Seeing as there’s no link to the list discussion.
I linked the Metamath thread on the previous Shtetl-Optimized thread.
Norm called out my lack of Foundation here.
Comment #67 May 15th, 2016 at 7:08 pm
Scott, Sniffnoy: I had to delete all the links from comment #64 for it to take (if someone would explain precisely what went wrong, or better yet put a “technical commenting FAQ” in the sidebar, I would appreciate that immensely). The correct version is https://gist.github.com/sorear/be14b38faa2062662e34116e2b9e7865
Comment #68 May 15th, 2016 at 7:29 pm
turbo #64:
I have a two line code. How does this correspond to number of states?
Yes, that’s the question, isn’t it? 🙂
Comment #69 May 15th, 2016 at 7:53 pm
David Roberts #65: Here. You’ll notice it doesn’t have 5349 states anymore.
Comment #70 May 15th, 2016 at 8:17 pm
Stefan #69: Wait, you’ve gotten it down to 1920 states?? (Forgive me; I don’t know how the lines in that program correspond to TM states.)
Comment #71 May 15th, 2016 at 8:24 pm
Scott #70: Yes. Each line is a state: “name = write(0) direction(0) nextstate(0) write(1) direction(1) nextstate(1)”. (When you get a chance, I’d like to know what’s up with #67.)
Comment #72 May 15th, 2016 at 8:54 pm
@Stefan #69: so how many lines now? 1929, 1920 or 1919?
Comment #73 May 15th, 2016 at 8:55 pm
Scott #50:
Thanks for the response. I also think that a UBI is preferable to the constellation of safety-net programs.
However, both systems need to decide how large the safety net ought to be. I suspect that the safety net that you deem minimally acceptable is vastly larger than preventing starvation. You certainly don’t need $7.25 an hour to not starve. For instance, migrant labor in Qatar from places like Nepal manage to survive and save quite a lot of money while earning less than $7.25 an hour. And not only do they not revolt but hundreds of thousands of people line up for the opportunity to go there. This, of course, is driven by how shitty economic conditions in Nepal are.
I imagine that you use ‘not starving’ to really mean living a ‘minimally decent’ life. So what is a minimally decent life? What is a good way to determine the appropriate size of the safety net? How should it scale with the prosperity of a society?
Comment #74 May 15th, 2016 at 8:57 pm
Stefan: You might want to use italics or blockquotes when quoting, your post is pretty hard to read as it is.
OK, so I see — regularity is included because metamath uses an unusually weak version of infinity that only works with regularity. And it makes sense that weak infinity + regularity would be simpler than usual infinity.
Good point about transformation/collection. I forgot that you can drop separation if you have null set (which follows from infinity; I guess here it follows from weak infinity + regularity) and “strong transformation” (where you assert that the resulting set is exactly the image rather than merely containing it). That’s a nice shortcut.
I find the way they write their axioms on the website hard to read. I’m used to reading them with all quantifiers explicit, whereas they seem to have lots of implicit stuff going on with their quantifiers and I can’t figure out how it’s supposed to work. (Also, I’m used to predicates being written as the more eplicit “φ(x,y,z)”, rather than “φ, where x, y, and z are free in φ”).
Man, if you have this, you may as well go for Peano Arithmetic as well, right? 🙂 That should be a lot simpler, I figure. (Now I’m wondering about the logic — would you be able to save any states by replacing Peano Arithmetic by Heyting Arithmetic? Since each is consistent iff the other is.)
Comment #75 May 15th, 2016 at 9:01 pm
Er. I may have stated that freeness bit wrong. Point is I’m used to having predicates having their parameters explicitly listed.
Comment #76 May 15th, 2016 at 9:04 pm
Stefan #71: Sorry about that! Comments with too many links in them sometimes get caught by my spam filter. Do you want me to dig them out now (which will mess up the comment numbering, but no matter), or have those comments already been superseded by later ones?
Awesome that you’ve gotten to ~2000 states for ZFC now! (And to ~1000 for RH.)
Comment #77 May 15th, 2016 at 9:17 pm
RP #73:
I imagine that you use ‘not starving’ to really mean living a ‘minimally decent’ life. So what is a minimally decent life? What is a good way to determine the appropriate size of the safety net? How should it scale with the prosperity of a society?
Important questions that lack obvious answers! Once people agree that these are the relevant questions, frankly my main remaining concern is just that they get decided on democratically, and without the public getting lied to (by the left, the right, or anywhere else) about the meanings of the various policy options or their empirical track records.
Comment #78 May 15th, 2016 at 9:40 pm
Sniffnoy #74
Well, the blockquotes are all there in the gist. Still figuring out this “WordPress commenting” thing. Apparently it’s links that cause problems, so I can use blockquotes freely.
Actually what we have here is a form of strong transformation where the function is allowed to be partial, so we can get the null set by transforming with an empty function (axnulALT).
All free individual variables in a theorem are virtually universally quantified. That confused me quite a bit too, but I think it has more to do with the Hilbert/Gentzen divide than anything else. Most computer proof systems follow Gentzen, Metamath doesn’t.
Not going to make excuses for that one, although it’s discussed in appendix 3 of http://us.metamath.org/mpegif/mmset.html.
Unfortunately a weaker logic is not necessarily the same as a simpler logic. Most treatments of PA I’ve seen have four non-logical operators, zero/0, successor/1, add/2, and multiply/2, which would erase your PA axiom gains under a substantially more complicated logic compared to set theory’s single connective. Is there a well-known form of PA with only one connective? Personally I’d take set theory and leave out Infinity and Regularity, the resulting system is equiconsistent to PA and also much easier to work with. (You can also replace Replacement with separate Separation and Pairing axioms, but that might not save states.)
Scott #75:
The comment isn’t superseded, but it looks like Sniffnoy got the message so I won’t press it. So I shouldn’t link every vaguely relevant concept in my comments then? 🙁
I’m a little surprised at the fact that this is the first comment on the RH machine.
David #72:
1919 with the –no-cfg-optimize option. 1929 with default options (that work better for my other three test programs). No idea where 1920 came from.
Comment #79 May 15th, 2016 at 9:41 pm
Sniffnoy #74
Well, the blockquotes are all there in the gist. Still figuring out this “WordPress commenting” thing. Apparently it’s links that cause problems, so I can use blockquotes freely.
Actually what we have here is a form of strong transformation where the function is allowed to be partial, so we can get the null set by transforming with an empty function (axnulALT).
All free individual variables in a theorem are virtually universally quantified. That confused me quite a bit too, but I think it has more to do with the Hilbert/Gentzen divide than anything else. Most computer proof systems follow Gentzen, Metamath doesn’t.
Not going to make excuses for that one, although it’s discussed in appendix 3 of (MMSET).
Unfortunately a weaker logic is not necessarily the same as a simpler logic. Most treatments of PA I’ve seen have four non-logical operators, zero/0, successor/1, add/2, and multiply/2, which would erase your PA axiom gains under a substantially more complicated logic compared to set theory’s single connective. Is there a well-known form of PA with only one connective? Personally I’d take set theory and leave out Infinity and Regularity, the resulting system is equiconsistent to PA and also much easier to work with. (You can also replace Replacement with separate Separation and Pairing axioms, but that might not save states.)
Scott #75:
The comment isn’t superseded, but it looks like Sniffnoy got the message so I won’t press it. So I shouldn’t link every vaguely relevant concept in my comments then? 🙁
I’m a little surprised at the fact that this is the first comment on the RH machine.
David #72:
1919 with the –no-cfg-optimize option. 1929 with default options (that work better for my other three test programs). No idea where 1920 came from.
Comment #80 May 15th, 2016 at 9:42 pm
Scott: your spam filter ate the first version of comment #77 which had exactly one link in it. Is this a leaky bucket thing where my link-rich comments from the last few days are counting against my IP address? Is there any way I can register so that it’ll stop hating me?
Comment #81 May 15th, 2016 at 10:42 pm
Stefan: Oh, that’s quite troublesome. I was thinking it was simpler because aside from induction, the axioms are just very short equations (or almost so). I wasn’t thinking about how much complexity a larger signature would add.
Wait, so your current one, it leaves out pairing, since that can be accomplished with replacement and the existence of a two-element set? Which could be accomplished either via infinity or via ℘(℘(∅))? Man, that’s another shortcut I didn’t know about! I guess I’m learning quite a bit about compressing ZFC today…
Comment #82 May 15th, 2016 at 11:50 pm
When you say that some of these Turing machines have been “verified”, what does that mean? Have any of them been formally proven equivalent to the statement of the appropriate conjecture (i.e., Goldbach or con-ZFC, or whatever)? If not, do you think that would be hard to do?
Comment #83 May 16th, 2016 at 9:04 am
Scott #52
“There are the constraints of the market economy, and then there’s also the constraint that people who work full-time shouldn’t be starving and unable to feed their families.”
Raising minimum wages is one thing, but what’s really nonsensical is the gigantic amount of perfectly good food that gets wasted (and the same applies to most goods now becoming disposable commodities). It probably wouldn’t take a huge amount of investment to turn all that waste into something useful.
Comment #84 May 16th, 2016 at 9:10 am
matt #82: No, we only meant “verified” in the physics sense—i.e., Adam communicated with the authors, understood what in the machine’s behavior was supposed to correspond to generating the primes, searching for Goldbach counterexamples, etc., and then checked in a simulator that the machine actually had that behavior.
I do think it would be feasible (though nontrivial) to verify using an automated proof-checker that Turing machines such as these actually do what they’re supposed to. That’s something that we thought about, but decided to leave to future work.
Comment #85 May 16th, 2016 at 10:04 am
#83 Don’t waste and pointless and desperate greed form a crucial part of the (modern) capitalist system? If we all fixed things at home when they broke, or even stopped working when we had enough money to live comfortably, then I think economics 101 tells us we don’t get the shiny things many people seem to want.
Comment #86 May 16th, 2016 at 3:04 pm
Do I understand correctly that the ZFC search is currently the most interesting one because it’s the known undecidable problem where you can currently create the smallest TMs? And the choice is a bit arbitrary in that you don’t have a good overview of other undecidable problems that could translate into Turing machines more efficiently?
Would (known) variants of well known problems be different enough to fit in the required arithmetical hierarchy, like various Collatz-like sequences?
I assume there’s been a lot of thought put into similar stuff before; see e.g. http://cstheory.stackexchange.com/questions/20978/what-is-the-smallest-turing-machine-where-it-is-unknown-if-it-halts-or-not
Comment #87 May 16th, 2016 at 9:03 pm
Probably a stupid question, but do we know that Stefan’s machine generates all possible statements of ZFC if it runs long enough? Otherwise it could be that the machine never halts and one could eventually prove that without proving that ZFC is consistent.
Comment #88 May 16th, 2016 at 9:16 pm
wolfgang #87: Well, if Stefan’s machine doesn’t generate all possible statements of ZFC, that would simply mean there’s a bug in his code (which, of course, is possible). If you wanted to be confident there was no bug, then besides testing the machine, you could use an automated proof assistant to prove that the machine’s running forever was equivalent to Con(ZFC), as I said to Matt in comment #84. But that’s something that would take substantially more work and hasn’t been attempted yet.
Comment #89 May 16th, 2016 at 11:52 pm
Hi Scott,
When attempting to view the answers on Quora (I know you haven’t answered yet, but there are comments there from others), I’m prompted to sign in via my google account, at which point I’m told that Quora wants to: (1) View my email address, (2) View my basic profile info, (3) Manage my contacts.
Of course, for privacy reasons, I want none of this. Subsequently, I’m denied viewing any of the answers on Quora. Is there a way around this? Perhaps I’m missing something.
If this is truly a requirement, I want to point out that this (1) seems like a scummy tactic on Quora’s part, and (2) makes it hard to partake in your Q&A session. If they really care about people “pitching in” (which is how they justify their login requirement), then I don’t understand why they need to manage my contacts.
Comment #90 May 17th, 2016 at 12:47 am
FYI, Peter Taylor just sent in a change to riemann.nql which gets us past the 1000-state cognitive milestone for RH. Anyone think they can get to Scott’s 750?
Comment #91 May 17th, 2016 at 1:04 am
@anon
Yes, quora is scummy. It used to even require that you sign in merely to view answers I recall.
I’ve given up on quora. Stackexchange, reddit, ycombinator offer far better venues for similar topics.
Comment #92 May 17th, 2016 at 1:17 am
#89 anon – For privacy reasons, I second your sentiment. When I visited Quora and was asked to sign-in with an existing Google or Facebook account, I simply closed the page.
Comment #93 May 17th, 2016 at 5:48 am
Answer to (1) No.
Answer to (2) Yes.
Three Quora ‘gotcha’ that were unexpected (to me) were: [A] logging into Quora even once grants Quora permanent management privileges to one’s Google Contacts, and [B] deleting one’s Quora account, via Quora’s account management site, does NOT rescind Quora’s Contact-management privileges; instead Quora retains those privileges indefinitely, and [C] Read carefully, it turns out that Quora’s account management interface does NOT promise that your once-created Quora account will EVER be entirely deleted; nor does it promise that Quora will EVER cease using its Google Contact privileges.
Resolution Once-only Quora uses can rescind Quora’s indefinitely-retained management privileges for Google Contacts by descending through these five levels:
-> Google
-> My Account
-> Sign-In and Security
-> Manage Apps
-> Delete ‘Quora’
Conclusion Richard Stallman’s concerns regarding privacy and democracy are rationally grounded.
Comment #94 May 17th, 2016 at 7:51 am
Using Stefan O’Rear’s NQL I’ve got a Laver table checker to 522 states, but I think it can be improved more by adding direct support for “while(true)” loops.
Comment #95 May 17th, 2016 at 10:01 am
Scott, you should turn this TM optimization into a little video game, and leverage the power of crowd sourcing:
Last year this came out: https://en.wikipedia.org/wiki/TIS-100
Tons of smart developers got hooked on solving its “puzzles”, which consisted in optimizing the hell out of assembly language routines. And since the thing has leaderboards, it got very competitive https://twitter.com/rygorous/status/607132847250378753
Comment #96 May 17th, 2016 at 10:40 am
Peter Taylor #97: well, that was easy enough to add. Try now?
Comment #97 May 17th, 2016 at 10:49 am
anon #89: if you’re using Chrome, you can bypass this for read access pretty easily:
. click on the icon just left of the URL
. make sure you’re on the Permissions tab
. click the “[n] from this site” link
. select the http://www.quora.com cookie
. click “Block”
Comment #98 May 17th, 2016 at 12:53 pm
anon@89
Appending “?share=1” to a Quora URL makes it viewable without login.
(I’m still not a huge fan of Quora/its policies.)
Comment #99 May 17th, 2016 at 12:57 pm
My thanks to John Sidles and terete for the info.
Comment #100 May 17th, 2016 at 5:15 pm
Thanks, Stefan. 483 states to check Laver tables for periodicity of 32, as suggested in the comments to the previous post by Joseph Van Name.
I suspect there’s quite a bit of inefficiency due to the register machine layer: I’m having to encode a stack using multiplication and divrem, and I expect that by encoding it directly on the tape it can be reduced by 50% or so.
Comment #101 May 17th, 2016 at 8:57 pm
Peter Taylor #103: Wonderful! Any objections to merging that? Should we rename the repository?
Regarding registers, the fundamental limitation of the BDD approach is that the tape head needs to return to the home position when the sequencing states are re-entered, which limits our ability to do anything fancy with the tape head. The low-level routines don’t need to be a simple register machine; the first version I published in fact used a Brainfuck-style one-sided infinite tape of natural numbers, and I had an earlier version which was the same with two tape heads (when I was still trying to use on-tape execution).
Laver tables are simple enough that a direct (not BDD, using ad-hoc means to control state) machine might be doable.
I think that at a modest cost in state count (50ish?) I could modify the low-level support so that each register would actually be a stack, and support STASH and RETRIEVE operations. Cost would be slightly lower if only one stack were required. The reason this wasn’t done earlier was because zf.nql needed a pairing function anyway, and it was simpler to reuse that.
Comment #102 May 18th, 2016 at 12:21 am
Hi Scott. I saw this and thought of you. Looks like Austin loves its regulation. Don’t hold your breath for ride-sharing.
Comment #103 May 18th, 2016 at 7:25 pm
Stefan, I have no objections to the merge, and no strong opinion on the name.
A one-sided infinite tape of natural numbers is exactly the model which I was thinking of using for a hand-crafted Laver table machine.
If you want to use GitHub’s chat system to discuss details rather than comments on Scott’s blog, I’ve created a Gitter room linked to my fork of the repo at https://gitter.im/pjt33/metamath-turing-machines . That would improve the signal-to-noise ratios around announcements such as:
By micro-optimising Stefan’s ZF-consistency checker, I’ve reduced it to 1895 states.
Comment #104 May 18th, 2016 at 8:32 pm
The 3x+1 problem has a simulation with 13 states and 2 symbols. Could that be adapted to get a program that searches for nontrivial 3x+1 cycles using fewer states than the 27 (claimed) for Goldbach?
Comment #105 May 18th, 2016 at 8:33 pm
(forgot the link: http://arxiv.org/abs/1409.7322 by Pascal Michel. He has other papers at Arxiv on collatz-like behavior of small busy beaver champions.)
Comment #106 May 19th, 2016 at 1:20 am
Peter Taylor #106:
I’ve never used gitter. From skimming their website, it appears to be operated by an entirely different legal entity, not even incorporated in the same country, and GitHub themselves doesn’t link to it, so it’s kinda odd the way many people describe it as “GitHub’s chat system”. I’m open to using it if you want, but I’m also kind of interested in having information about NQL searchable on the public Web; does gitter enable that?
To all interested:
I remembered today another unsolved problem in elementary number theory that could possibly result in a smaller TM than Goldbach: Does there exist an odd perfect number?
Comment #107 May 27th, 2016 at 7:08 pm
Following up on the Laver tables: I have a hand-constructed machine with 77 states. 44 states compute the tables themselves, and 33 handle the bookkeeping. I’m working on a write-up.
Comment #108 May 30th, 2016 at 10:02 am
Hi Scot et al. big up for the TMs.!! Mucho mucho congrats!!
Comment #109 May 31st, 2016 at 2:52 pm
Scott #26: I couldn’t track down Andy’s comment, but I was curious so I tried to construct such a function myself. The construction has some caveats: it only rules out bounded Turing reductions; and I wasn’t sure how to go about showing that BB dominates all oracle machines given an oracle for this function. I’d be curious to see if Andy’s construction manages to address those caveats.
The construction: given an enumeration of TM’s M_0, M_1, M_2, … which compute total non-decreasing functions on the natural numbers, and an enumeration of oracle machines O_0, O_1, O_2, … , we define our function f to be
f(n) = BB(a_n)
where the sequence of natural numbers (a_n) is defined in stages — specifically, in stage 2k we’ll have a_n grow until M_k fails to compute f, and in stage 2k+1 we’ll have a_n “plateau” until O_k fails to compute BB with bounded calls to an oracle for f.
To that end, we’ll use a sequence of natural numbers s_i to denote the input n at which stage i begins. The first stage begins at 0, i.e. s_0 = 0.
Stage i = 2k: set a_m = a_(m-1) + 1 for all m from s_i up until BB(a_m) > M_k(m). If this doesn’t happen, then M_k bounds BB on all but finitely many inputs (albeit shifted along a little, so BB(n) <= M_k(s_i – a_s_i + n)), so M_k bounds BB, which is a contradiction. Set s_(i+1) to the first m such that BB(a_m) > M_k(m).
Stage i = 2k+1: let f_k be the function which agrees with f up until this stage, and then plateaus forever, i.e. f_k(n) = f(s_i) for all n > s_i. Then f_k is computable (trivially, just use a lookup table), so oracle machine O_k cannot bound BB using an oracle for f_k, otherwise we could transform O_k into a regular TM which simply computes values of f_k as needed, and in doing so arrive at a contradiction. So there is a first input n such that O_k with an oracle for f_k fails to bound BB, and, assuming O_k is only allowed a bounded amount of calls to the oracle, there is a greatest value p which O_k queries. Set s_(i+1) = p, and set a_m = a_(m-1) for m between s_i and p, so that on input n, O_k doesn’t distinguish f_k from f.
By construction, f is not computed by any TM, and no oracle machine computes a bound on BB using f as an oracle. It also isn’t hard to see that BB beats each oracle machine with f on infinitely many values, and the construction of f can be (messily) modified to guarantee that f eventually dominates every computable function. (Instead of plateuing, grow like the greatest delta among all prior computable functions.)
That said, “BB beats each oracle machine given f on infinitely many values” is a weaker statement than “BB dominates each oracle machine given f eventually”, and I’m not sure how to get the latter. (Though I suspect it holds.) I also don’t know how to shed the bounded Turing reduction requirement. Certainly you can’t shed it in the above construction: an oracle machine need only successively query along the plateaus until f starts growing again. Now, there’s a slight modification which “blows chunks in BB” rather than “shifting BB rightward” like the above construction does which might lose the information an oracle machine might need to bound BB, but it’s not immediate that this stumps general Turing reductions: oracle machines can do crazy things with no query bound, they need not halt, they could query f on every possible input. It makes it difficult to conceive of an incremental way of constructing f which rules out each oracle machine in succession (and also rules out regular TMs from computing f), without a decision made later down the line undoing the work done to rule out a previous oracle machine — but I won’t be surprised if that’s my inexperience speaking, so if someone knows better I’d be glad to be enlightened! Meanwhile, I’ll probably come back to this problem a few more times when I can spare a moment, because I have some ideas about how to approach it myself.
Comment #110 June 1st, 2016 at 3:24 pm
As a non-expert, i find this extremly exciting – but would like to understand more: “43-state Turing machine by Jared S that halts iff there’s a counterexample to Goldbach’s Conjecture.”
1) Could this realistically help in proving Goldbach by proving that the TM does (not) halt?
2) In particular: Could numerical approaches help here? How many states do exist, i mean the band is still infinitly long, right?
3) is there any way to restrict the size of the tape?
sorry for these superlowlevel questions.
Comment #111 June 1st, 2016 at 3:45 pm
Hi Guys, what is the philosophical justification (if any) for saying the “43 states for Goldbach”, “744 states for Riemann”, “1919 states for Con(ZFC)”, are measures of the difficulty of these problems?
Also, if an axiomatic theory can compute BB(n), does that mean it can compute BB(n-1), BB(n-2) etc?
Comment #112 June 2nd, 2016 at 1:04 pm
Andreas #110:
1) No, this won’t help with proving Goldbach.
2) Yes, the tape is still infinitely long.
3) No, if you could restrict the size of the tape, you’d reduce Goldbach to a finite computation, and thereby essentially solve it.
Comment #113 June 10th, 2016 at 5:53 pm
I got the Laver table TM down to 64 states. http://cheddarmonk.org/papers/laver.pdf