So, the unknowable kicks in
July 30, 2016 11:42 AM Subscribe
Logic hacking - "Writing shorter and shorter computer programs for which it's unknowable whether these programs run forever, or stop... the winner of the Busy Beaver Game for N-state Turing machines becomes unknowable using ordinary math - somewhere between N = 5 and N = 1919."
Interview with a Mathematical Physicist: John Baez
-1+1 = 0
-Computing the uncomputable
-The inaccessible infinite
-The longest G+ post I'll ever write
-The world's most long-winded proof
-Paradoxes of randomness
-The surprising cleverness of modern compilers
Interview with a Mathematical Physicist: John Baez
- Part 1 - "Here's the first part of an interview. I used it as an excuse to say what I've been doing all these years. I also talk about my uncle Albert Baez, who got me interested in physics in the first place - and what I'm working on right now. I hope it's interesting even if you care more about math and physics. There's a lot here about quantum gravity, category theory and some of my hobbies, like the octonions."
- From crackpots to climate change - "Here's part two of my interview on Physics Forums. I talk about the early days of the internet, before the world-web caught on. First we started discussing physics on 'usenet newsgroups' like sci.physics - but then a flood of crackpots invaded... That's what led me to create the Crackpot Index. But spending lots of time on newsgroups was still worthwhile, and it led me to start writing 'This Week's Finds', which has been called the world's first blog, in 1993. I also talk about my physics and math heroes, what discoveries I'm most looking forward to, and why I switched to thinking about environmental problems. It was a great chance to ponder lots of things, including the far future of the Universe."
-1+1 = 0
-Computing the uncomputable
-The inaccessible infinite
-The longest G+ post I'll ever write
-The world's most long-winded proof
-Paradoxes of randomness
-The surprising cleverness of modern compilers
The Busy Beaver and ZFC. (Linked in the Busy Beaver link, but worth noting on its own.)
posted by Death and Gravity at 12:39 PM on July 30, 2016
posted by Death and Gravity at 12:39 PM on July 30, 2016
polymodus, I bet you BB(N) dollars that we will never find out what N is.
Speaking seriously though, I think N is quite small. I'd say less than 100.
posted by J.K. Seazer at 3:47 PM on July 30, 2016 [2 favorites]
Speaking seriously though, I think N is quite small. I'd say less than 100.
posted by J.K. Seazer at 3:47 PM on July 30, 2016 [2 favorites]
I don't know that we'll ever find out what N is, but if I were to guess, my guess would be under 30.
posted by Death and Gravity at 4:07 PM on July 30, 2016
posted by Death and Gravity at 4:07 PM on July 30, 2016
sci.physics - but then a flood of crackpots invaded...
ah, memories of ludwig plutonium...
posted by andrewcooke at 5:09 PM on July 30, 2016
ah, memories of ludwig plutonium...
posted by andrewcooke at 5:09 PM on July 30, 2016
if i was going to read one chaitin book, and i am already vaguely aware of his work and ideas, which one should i read?
posted by andrewcooke at 5:10 PM on July 30, 2016
posted by andrewcooke at 5:10 PM on July 30, 2016
wow. that final link. how on earth does clang "know" that?
posted by andrewcooke at 5:18 PM on July 30, 2016 [2 favorites]
posted by andrewcooke at 5:18 PM on July 30, 2016 [2 favorites]
Chaitin's books aren't that great.
Better to chase down the papers, he covers a lot of ground and it's all interesting.
posted by Death and Gravity at 5:20 PM on July 30, 2016 [3 favorites]
Better to chase down the papers, he covers a lot of ground and it's all interesting.
posted by Death and Gravity at 5:20 PM on July 30, 2016 [3 favorites]
wow. that final link. how on earth does clang "know" that?
Oh boy: I can't speak to the specifics of clang here, but back in grad school I taught the compilers class a couple times so I'm just trying to think how to distill this down from about a week of lecture notes on "basic optimization techniques"...
Ok, so a really simplistic compiler looking at that C code would use a parser derived from the formal specification of C's grammar to build up a "parse tree" representing what the code is, basically, saying. It would also have places in that parser picked out where it knows it will have seen just enough about a piece of the code to be able to emit some machine code to do the right thing for that part. So like, as soon as it's parsed int count(uint64_t x) { it can trigger the "semantic action" to emit a chunk of machine code for setting up the call stack after a function call, figuring out relative pointer addresses for whatever parameters were passed, things like that. In reality even a simple compiler isn't actually emitting true machine code yet, rather, it emits some kind of abstract virtual machine code that's architecture-neutral. Then in a second step it loads up a dictionary that translates from virtual instructions to the specific instructions for whatever architecture it's targeting and does a replacement.
And honestly that might be what's happening here: even basic compilers will try to optimize at this step, running a window over the virtual code with maps like "if you see these three instructions in a row you can replace them with this one fancy alternative". So possibly someone hard-coded an optimization map with rules about what sort of chunks of machine code can be replaced with one invocation of popcntq. But I doubt it—there's more than one way to write c code that counts bits in an integer, and anyway those maps would be really fragile to subtle changes in source code.
Nowadays even simple "real" compilers use basic well-known optimization techniques earlier than just a window over the final translation step. These techniques are based on not emitting machine code as soon as the parser sees just enough to squirt out a couple instructions. Instead when the parser reaches those points the "semantic actions" are to just add on to ongoing data structures it keeps about what it knows about the code's semantics. It builds up graphs and trees that are kind of like flowcharts (remember those?) built out of "basic blocks"—stretches of source code that always start at the top and end at the bottom, with no branching. It keeps track of what it can prove, mathematically, about the semantics of the code inside those blocks.
Once it's completely built up these datastructures for a section (typically one function, or something larger if it can) it starts running many transformations: it uses theorem proving techniques to infer new truths about the semantics of the code, it builds up graphs of where the value of this variable depends on the value of that variable (looking for places where it doesn't depend, because that means it's free to change things around). So like in this code, a complier can easily know that v = 0 immediately after int v = 0;. A better compiler can prove that v = the number of times that while loop ran immediately before return v;.
The compiler uses all these for many optimizing decisions: which parameters, variables, and temporaries to keep in registers vs. RAM, where it can use the same register to hold more than one thing (because they're never used at the same time), where it can move expensive instructions out of loops (because their value is never needed inside the loop, a technique called hoisting and the ur-example of this kind of optimization) and so on.
(In the dynamically-typed languages so popular these days, it might be looking at whether it could use a fast, hardware integer-compare instruction for while(x != 0) { because it could prove the types on both sides of the comparison were integers, or whether it would have to fall back to a function call to the dynamic dispatcher because it couldn't prove enough about their types. But that's not a question for C.)
So the alternative that I suspect clang is really doing, is being able to prove that all that code in the function results in the semantics "count of bits in x", as well as having some kind of architecture-specific knowledge that comes in during this early stage that says "there's an opcode for that". And this is pretty fancy, there are lots of gotchas to being able to transform code in ways you can prove are semantically equivalent—it's one thing to say "v = the number of times that while loop ran" but to be correct you also have to say "*and it might have overflowed into negatives", only to later prove "no it couldn't have actually" in order to get to "you know we could just replace all this stuff with popcntq!"
...Ok so that got long and complicated anyway. Hope it makes some kind of sense. Incidentally I believe this is one place where "know" is the correct term; in order to do this the compiler is using representations of the semantic truth of the code, and using some pretty fancy logical methods to infer new truths from that. The problem domain might be restricted but this as close to "knowing" as programs, even the trendiest and fanciest Deep Whatever, get. And it fits the classic "justified true belief" definition.
posted by traveler_ at 9:58 PM on July 30, 2016 [18 favorites]
Oh boy: I can't speak to the specifics of clang here, but back in grad school I taught the compilers class a couple times so I'm just trying to think how to distill this down from about a week of lecture notes on "basic optimization techniques"...
Ok, so a really simplistic compiler looking at that C code would use a parser derived from the formal specification of C's grammar to build up a "parse tree" representing what the code is, basically, saying. It would also have places in that parser picked out where it knows it will have seen just enough about a piece of the code to be able to emit some machine code to do the right thing for that part. So like, as soon as it's parsed int count(uint64_t x) { it can trigger the "semantic action" to emit a chunk of machine code for setting up the call stack after a function call, figuring out relative pointer addresses for whatever parameters were passed, things like that. In reality even a simple compiler isn't actually emitting true machine code yet, rather, it emits some kind of abstract virtual machine code that's architecture-neutral. Then in a second step it loads up a dictionary that translates from virtual instructions to the specific instructions for whatever architecture it's targeting and does a replacement.
And honestly that might be what's happening here: even basic compilers will try to optimize at this step, running a window over the virtual code with maps like "if you see these three instructions in a row you can replace them with this one fancy alternative". So possibly someone hard-coded an optimization map with rules about what sort of chunks of machine code can be replaced with one invocation of popcntq. But I doubt it—there's more than one way to write c code that counts bits in an integer, and anyway those maps would be really fragile to subtle changes in source code.
Nowadays even simple "real" compilers use basic well-known optimization techniques earlier than just a window over the final translation step. These techniques are based on not emitting machine code as soon as the parser sees just enough to squirt out a couple instructions. Instead when the parser reaches those points the "semantic actions" are to just add on to ongoing data structures it keeps about what it knows about the code's semantics. It builds up graphs and trees that are kind of like flowcharts (remember those?) built out of "basic blocks"—stretches of source code that always start at the top and end at the bottom, with no branching. It keeps track of what it can prove, mathematically, about the semantics of the code inside those blocks.
Once it's completely built up these datastructures for a section (typically one function, or something larger if it can) it starts running many transformations: it uses theorem proving techniques to infer new truths about the semantics of the code, it builds up graphs of where the value of this variable depends on the value of that variable (looking for places where it doesn't depend, because that means it's free to change things around). So like in this code, a complier can easily know that v = 0 immediately after int v = 0;. A better compiler can prove that v = the number of times that while loop ran immediately before return v;.
The compiler uses all these for many optimizing decisions: which parameters, variables, and temporaries to keep in registers vs. RAM, where it can use the same register to hold more than one thing (because they're never used at the same time), where it can move expensive instructions out of loops (because their value is never needed inside the loop, a technique called hoisting and the ur-example of this kind of optimization) and so on.
(In the dynamically-typed languages so popular these days, it might be looking at whether it could use a fast, hardware integer-compare instruction for while(x != 0) { because it could prove the types on both sides of the comparison were integers, or whether it would have to fall back to a function call to the dynamic dispatcher because it couldn't prove enough about their types. But that's not a question for C.)
So the alternative that I suspect clang is really doing, is being able to prove that all that code in the function results in the semantics "count of bits in x", as well as having some kind of architecture-specific knowledge that comes in during this early stage that says "there's an opcode for that". And this is pretty fancy, there are lots of gotchas to being able to transform code in ways you can prove are semantically equivalent—it's one thing to say "v = the number of times that while loop ran" but to be correct you also have to say "*and it might have overflowed into negatives", only to later prove "no it couldn't have actually" in order to get to "you know we could just replace all this stuff with popcntq!"
...Ok so that got long and complicated anyway. Hope it makes some kind of sense. Incidentally I believe this is one place where "know" is the correct term; in order to do this the compiler is using representations of the semantic truth of the code, and using some pretty fancy logical methods to infer new truths from that. The problem domain might be restricted but this as close to "knowing" as programs, even the trendiest and fanciest Deep Whatever, get. And it fits the classic "justified true belief" definition.
posted by traveler_ at 9:58 PM on July 30, 2016 [18 favorites]
If you were going to try to look for bit counting algorithms for your compiler to recognize and optimize, you'd probably feel pretty bad if you missed something in K&R.
posted by nom de poop at 10:55 PM on July 30, 2016 [1 favorite]
posted by nom de poop at 10:55 PM on July 30, 2016 [1 favorite]
So possibly someone hard-coded an optimization map with rules about what sort of chunks of machine code can be replaced with one invocation of popcntq.In this case, at least, a hard-coded rule is exactly how LLVM does it (check out LoopIdiomRecognize::recognizePopcount, the function responsible).
posted by panic at 11:36 PM on July 30, 2016 [3 favorites]
huh. i think i read k&r back in the day, but i had no idea that was a common idiom. thanks everyone.
posted by andrewcooke at 1:55 PM on July 31, 2016
posted by andrewcooke at 1:55 PM on July 31, 2016
I first read about the Busy Beaver problem in The Turing Omnibus and it always stuck with me. Good to know remember occasionally that we're not as smart as nature.
posted by RobotVoodooPower at 2:15 PM on July 31, 2016
posted by RobotVoodooPower at 2:15 PM on July 31, 2016
Incidentally I believe this is one place where "know" is the correct term; in order to do this the compiler is using representations of the semantic truth of the code, and using some pretty fancy logical methods to infer new truths from that. The problem domain might be restricted but this as close to "knowing" as programs, even the trendiest and fanciest Deep Whatever, get. And it fits the classic "justified true belief" definition.
That is very interesting. I suppose that you could also do something in the tradition of Gettier counterexamples, if you had an independent argument that there isn't any knowledge here, but agreed that there was justified true belief.
posted by thelonius at 2:44 PM on July 31, 2016
That is very interesting. I suppose that you could also do something in the tradition of Gettier counterexamples, if you had an independent argument that there isn't any knowledge here, but agreed that there was justified true belief.
posted by thelonius at 2:44 PM on July 31, 2016
Great post, kliuless. This was my bread and butter in undergrad... compiler optimizations make my brain hurt, but hurt so good. My absolute favorite paper was Superoptimizer, which is the ne plus ultra of this approach. You take a block of code, look at its inputs, look at it outputs, run it against a representative sample of data, and catalog the results. Then you set an upper bound for how long you're willing to let that sucker run, and you let fly. Superoptimizer then tries every combination that exists within the instruction set, running it against known inputs and outputs, checking to see if the random collection of things it's just emitted happens to compute the right result any faster than the original. You end up with seemingly-nonsensical code doing mundane things, but if you have three lines of code using 99% of your runtime CPU, it sometimes makes sense.
For example: is multiplication expensive on your hardware? Do you have to multiply by 29 a lot, but for some reason you don't want to keep a lookup table? Here it is with a move, a left shift, two subtractions, and an add:
posted by Mayor West at 5:29 AM on August 1, 2016
For example: is multiplication expensive on your hardware? Do you have to multiply by 29 a lot, but for some reason you don't want to keep a lookup table? Here it is with a move, a left shift, two subtractions, and an add:
d0 *= 29 move.l d0, d1 lsl.l #4,d0 sub.l d1,d0 add.l d0,d0 sub.l d1,d0
posted by Mayor West at 5:29 AM on August 1, 2016
It would be more aesthetic with either a shift and three subs or two shifts, two subs. But isn't that what a hardware multiplier would do anyway?
posted by Joe in Australia at 1:11 PM on August 1, 2016
posted by Joe in Australia at 1:11 PM on August 1, 2016
It'd be interesting to find an abelian, or maybe dihedral, group where computing the group operation was tractable but only by using large amounts of ram. It might've cryptography applications because post-quantum crypto systems have many drawbacks. Ain't clear if this is even possible though.
posted by jeffburdges at 3:45 PM on August 1, 2016
posted by jeffburdges at 3:45 PM on August 1, 2016
« Older Small Steps and Giant Leaps | The David Spade Index Newer »
This thread has been archived and is closed to new comments
posted by polymodus at 12:29 PM on July 30, 2016