// When we show this program to industry professionals, they usually figure out the right answer quickly. * A few, especially those who are aware of results in theoretical computer science, sometimes mistakenly think that we can't answer this question, with the rationale “This is an example of the halting problem, which has been proved insoluble”. * In fact, we can reason about the halting behavior for specific programs, including this one.
In other words, where a mid-wit would step through the code (and be right), a high-brow might deems the problem impossible because it fits to a generic class of which this particular instance is trivial.
It's kinda "word thinking" concept where you substitute actual understanding by being able to slap a familiar label on something and then use the label to decide how to feel about it (kinda like feeling differently about a topic based on whether you call it "social justice" which sounds good or "letting criminals roam your city" which sounds bad - whereas in reality it's probably more nuanced and different than either of these labels suggests.)
For those confused by the warm plate thing, it’s a reference to this trick the author had posted the previous day https://www.lesswrong.com/posts/fysgqk4CjAwhBgNYT/fake-expla... where the reason the plate it warmer farther away from the radiator, is because the instructor spun it around prior to the students entering the room.
Yep, it's a sort of accidental form of making perfect the enemy of better, forgetting that while a problem may be undecidable in general, there may still be a useful semi-/decidable subset. E.g. my IDE can still tell me that my program won't halt when I've been an idiot and forgot to update the `while` variable in a loop, halting problem notwithstanding
And similarly with regards to tractability and approximations. The travelling salesman problem is hard, and yet Google Maps works very well. And even when not using an approximation, sometimes n really is small enough to be tractable
> there may still be a useful semi-/decidable subset.
Yes, but note that the entire language HALT is semi-decidable (or Turing-recognisable if you use Sipser’s terminology); in this case it’s only the (strictly) decidable subset that is useful.
So is there any result on "how much" of the halting problem is solvable? E.g. is there a result that says there is a program which can decide whether the input halts for "most" inputs, in some sense of "most"?
> In other words, where a mid-wit would step through the code (and be right), a high-brow might deems the problem impossible because it fits to a generic class of which this particular instance is trivial.
In this situation, “mid-wit” might best apply to the person who studies theoretical computer science, but never manages to understand when this result is applicable: these people will fall into the second category. But see my comment at the end about whether this terminology is really appropriate.
Someone who quotes the undecidability of HALT in reference to the question of whether that specific program halts is probably not a “high-brow” (whatever that means). It’s a perfect example of “a little knowledge being a dangerous thing”: those who actually understand the theory will know when it applies; it’s those who don’t have a good internalised model of the theory, but who have a vague recollection of something along the lines “it’s impossible to tell if programs halt or not”, who are going to get it wrong.
As a side note, I don’t think “mid-wit” vs. “high-brow” is a good distinction here: whether or not you remember (or were taught) about the halting problem is not a matter of intelligence, and I suspect most people who get it wrong aren’t doing so because they never understood theoretical computer science, but rather because they haven’t been practicing academia, but rather the craft/art of software engineering, and have just forgotten it.
This situation is portrayed in the "bell curve" meme format, a ternary extension of the "go brr" meme format.
Dimwit at the far left side of the bell curve (somewhat offensively portrayed as a disfigured drooling person) does a simple/stupid thing that works.
Expert at the far right side of the bell curve (portrayed in a Jedi robe) does the same simple/stupid thing as the dimwit.
Person at the middle of the bell curve (with the late-'10s side-buzz hipster haircut) doing some complicated thing based on principle, theory, textbook-correct procedure, etc. This person is in tears, presumably upset that the expert is doing it the simple or stupid way, and believing themselves superior to the dimwit,
The ints being a total ordered set is why the example will terminate.
Change that to a float, where -0,0,+0 don't have a successor and it could be problematic.
Effectively the example was an existential quantifier, but will universal quantification, termination analysis would be less optimistic.
While it doesn't cover special cases like Ackerman functions, the time complexity is fairly easy to build intuition about with loops being forms of recusion for me.
While is Turning complete or a general recursive functions
For loops are primitive recursive functions
The reason c make choices it made as an example is shown in this paper. For those who haven't seen it.
Seems to me a case of people vaguely remembering long gone concepts from their university years.
The halting problem stipulates that it's impossible to have an algorithm that takes any program and decides if it halts. It doesn't say that there could be certain subclasses of programs for which such a procedure could exist.
I’ll also note that the humans aren’t reasoning in their sense. We use a combination of intuition and reasoning which feed into each other. Sometimes on the whole problem, sometimes pieces. That has implications for what to expect out of reasoning tools trying to do what people do.
A solution similar to us would probably train classical analyzers and NN’s side by side on many things. They could use the traditional tools for all the analyses computers can handle. Feed the source and analysis results to NN’s to train them. Then, use them to assist in harder, contextual analyses or probabilistic predictions.
There’s a lot of unexplored territory, with potential gains, if we can mix intuition and reasoning in computers more like people do.
I'm thinking about how LLMs like chatGPT did a complete end-run around the more historical attempts of formulating a grammar, translating English into some kind of logical form, using that to query a database, etc etc.
24 comments
[ 2.7 ms ] story [ 71.3 ms ] thread// When we show this program to industry professionals, they usually figure out the right answer quickly. * A few, especially those who are aware of results in theoretical computer science, sometimes mistakenly think that we can't answer this question, with the rationale “This is an example of the halting problem, which has been proved insoluble”. * In fact, we can reason about the halting behavior for specific programs, including this one.
In other words, where a mid-wit would step through the code (and be right), a high-brow might deems the problem impossible because it fits to a generic class of which this particular instance is trivial.
It's kinda "word thinking" concept where you substitute actual understanding by being able to slap a familiar label on something and then use the label to decide how to feel about it (kinda like feeling differently about a topic based on whether you call it "social justice" which sounds good or "letting criminals roam your city" which sounds bad - whereas in reality it's probably more nuanced and different than either of these labels suggests.)
https://www.lesswrong.com/posts/NMoLJuDJEms7Ku9XS/guessing-t...
And similarly with regards to tractability and approximations. The travelling salesman problem is hard, and yet Google Maps works very well. And even when not using an approximation, sometimes n really is small enough to be tractable
Yes, but note that the entire language HALT is semi-decidable (or Turing-recognisable if you use Sipser’s terminology); in this case it’s only the (strictly) decidable subset that is useful.
In this situation, “mid-wit” might best apply to the person who studies theoretical computer science, but never manages to understand when this result is applicable: these people will fall into the second category. But see my comment at the end about whether this terminology is really appropriate.
Someone who quotes the undecidability of HALT in reference to the question of whether that specific program halts is probably not a “high-brow” (whatever that means). It’s a perfect example of “a little knowledge being a dangerous thing”: those who actually understand the theory will know when it applies; it’s those who don’t have a good internalised model of the theory, but who have a vague recollection of something along the lines “it’s impossible to tell if programs halt or not”, who are going to get it wrong.
As a side note, I don’t think “mid-wit” vs. “high-brow” is a good distinction here: whether or not you remember (or were taught) about the halting problem is not a matter of intelligence, and I suspect most people who get it wrong aren’t doing so because they never understood theoretical computer science, but rather because they haven’t been practicing academia, but rather the craft/art of software engineering, and have just forgotten it.
Dimwit at the far left side of the bell curve (somewhat offensively portrayed as a disfigured drooling person) does a simple/stupid thing that works.
Expert at the far right side of the bell curve (portrayed in a Jedi robe) does the same simple/stupid thing as the dimwit.
Person at the middle of the bell curve (with the late-'10s side-buzz hipster haircut) doing some complicated thing based on principle, theory, textbook-correct procedure, etc. This person is in tears, presumably upset that the expert is doing it the simple or stupid way, and believing themselves superior to the dimwit,
Change that to a float, where -0,0,+0 don't have a successor and it could be problematic.
Effectively the example was an existential quantifier, but will universal quantification, termination analysis would be less optimistic.
While it doesn't cover special cases like Ackerman functions, the time complexity is fairly easy to build intuition about with loops being forms of recusion for me.
While is Turning complete or a general recursive functions
For loops are primitive recursive functions
The reason c make choices it made as an example is shown in this paper. For those who haven't seen it.
https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
The halting problem stipulates that it's impossible to have an algorithm that takes any program and decides if it halts. It doesn't say that there could be certain subclasses of programs for which such a procedure could exist.
A solution similar to us would probably train classical analyzers and NN’s side by side on many things. They could use the traditional tools for all the analyses computers can handle. Feed the source and analysis results to NN’s to train them. Then, use them to assist in harder, contextual analyses or probabilistic predictions.
There’s a lot of unexplored territory, with potential gains, if we can mix intuition and reasoning in computers more like people do.