Yes, I read that paper but I had no idea what any of it meant, unfortunately. I gather it does something which means you can evaluate a function for some number of substitutions/timesteps and if it hasn’t terminated with output yet, give a meaningful probability for whether it ever halts, but I don’t understand anything about what that something is, what sort of probability it’s giving, or what one could do with this.
you can evaluate a function for some number of substitutions/timesteps and if it hasn’t terminated with output yet, give a meaningful probability for whether it ever halts
Yep, that’s what it does.
I don’t understand anything about what that something is, what sort of probability it’s giving
The computational “something” is actually just “run the evaluation for m steps”. The clever bit is the “sort of probability”, which is a loose upper-bound on the measure of halting times we’ve already exceeded after m steps. Demonstrating how that measure makes sense is what takes up the meat of the paper.
a loose upper-bound on the measure of halting times we’ve already exceeded after m steps. Demonstrating how that measure makes sense is what takes up the meat of the paper.
Can you motivate the construction any? I doubt it’s as simple as 1/n timesteps because that would be too convenient, but what is it?
You could place bets on anything involving the Halting Problem, with sensible, well-defined, nonrandom odds.
That’s a tad contrived… I was thinking more along the lines of whether such an estimate could be useful in any of the traditional applications stymied by the Halting Problem, such as showing the equivalence of two functions, anti-virus checking, model checking, running sandboxed functions, resource limits, peephole optimization, etc.
By the way, I thought you knew computability theory professionally. Don’t you do something-or-other academic?
No, I’m afraid I only know what I’ve picked up here and there. Not nearly enough to understand a paper like that.
That’s a tad contrived… I was thinking more along the lines of whether such an estimate could be useful in any of the traditional applications stymied by the Halting Problem, such as showing the equivalence of two functions, anti-virus checking, model checking, running sandboxed functions, resource limits, peephole optimization, etc.
It’s all the same, really. You can do all those things, but probabilistically, up to the probabilities allowed by how long you’ve run the program for. Unless and until the program halts, there will always be some chance that you were wrong about its nonhalting and it does actually halt. If it actually doesn’t halt, your confidence that it doesn’t will asymptotically approach 1.0 in the limit.
Can you motivate the construction any? I doubt it’s as simple as 1/n timesteps because that would be too convenient, but what is it?
It’s not 1/n timesteps, yeah. It’s more along the lines of “Halting times for long-running programs turn out to be algorithmically non-random, which means we use this class of functions called incompressibility cut-off functions to bound the measure of halting times.” Beyond that, I’d have to start and finish a couple of textbooks (at least an intro to topology and then Calude’s own Information and Randomness) to explain more deeply.
It doesn’t help that Calude tends to use different notation in his papers from the standard notations used for studying Kolmogorov complexity/AIT.
Not really. ‘You can bet on halting’ is not a use. There is no website I can go to which has 24⁄7 gambling on randomly-generated lambda functions which I can use that code to clean up on; there is no lambda function e-sports league where competitors race to write or crack their rival’s functions, etc. This could be said of any method for calculating probabilities of anything: ‘you can bet on it!’ That’s not what I mean by use. What I meant are some of the applied tasks, but I’m not clear exactly on whether this probability applies: can I usefully use it to timeout functions being evaluated for superoptimization or peephole optimization or is there some catch or other issue? Can it be transformed from running times to other properties, similar to the connections between Halting & Godel & Rice’s theorem? etc.
which means we use this class of functions called incompressibility cut-off functions to bound the measure of halting times.” Beyond that, I’d have to start and finish a couple of textbooks (at least an intro to topology and then Calude’s own Information and Randomness) to explain more deeply.
That’s a little disappointing. But if you can’t explain what incompressibility cut-off functions are like, can you maybe give an idea of their general shapes? How does this scale with program length? How many steps in general would it take to reach something like 99% probability of non-halting? etc.
This could be said of any method for calculating probabilities of anything: ‘you can bet on it!’
Which is exactly why I said “bet”: it’s a 1-normalized measure, and can thus be mathematically applied in all the ways that 1-normalized measures (probabilities) are otherwise applied.
can I usefully use it to timeout functions being evaluated for superoptimization or peephole optimization or is there some catch or other issue? Can it be transformed from running times to other properties, similar to the connections between Halting & Godel & Rice’s theorem?
Yes and yes, provided that you are willing to accept uncertainty. This is where we get into the distinction between “in theory” and “in practice”: in theory, we have not solved the Halting Problem. In practice, whether we can use this solution depends on what happens if we’re wrong.
If I apply a peephole optimization on the assumption that some computation is nonhalting, but it actually does halt, how bad is it for the performance or correctness of my program? I can just refuse to apply the optimization if “p >= 0.05” that the program actually will halt, of course: in general, it usually doesn’t seem as if we’re going to lose much for betting conservatively by refusing to act on the probabilistic assumption of nonhalting. That would just leave us with the same state of knowledge we had before applying Calude’s anytime algorithm.
In what cases do we really need this “solution”, then? Mostly the issues precisely connected with Halting, such as Incompleteness Theorems and Rice’s Theorem. In those cases, we face the very peculiar problem that our formal systems will not only never be able to prove most nonhalting programs to be nonhalting, but that certain programs do halt and the formal systems still can’t prove that. In those cases, Calude’s “solution” is a big help, because all we need to do is run the program until it halts, and we’ve proven it to halt, giving us constructive evidence to add the “Program X terminates” theorem to our formal system. Likewise, in cases where we need to formally prove that one-or-another program never halts, we can run the program for a long time, and then assign a probability to the formal statement “Program X never terminates”, which then lets us start assigning probabilities to theorems derived from that statement.
The question then becomes, “What degree of probability in the half-open interval [0, 1) is acceptable to me, the program’s human operator, to go ahead and believe that Program X Never Halts?”
If you want to phrase it in terms of cognition, we can then apply notions of utility and bounded-rational reasoning: a principled calculation for bounded-rational utility maximization should let you say, my agent has so-and-so much computing power, and gets so-and-so much utility out of a Halting Solution, and it thus ought to spend so-and-so much of its compute-power to obtain such-and-so a level of probabilistic confidence. The ordinary Dutch Book stuff from probability theory then tells us that the agent is behaving rationally about how it treats Halting Problems.
Wherever a limitary theorem has been established by reduction to the Halting Problem, Calude’s probabilistic “Halting Solution” can be useful, provided that you are willing to reason explicitly about what you mean by “useful” in terms of trade-offs between compute-time, surety, and utility.
Can you explain what you did?
From the github description:
The github README is “Short summary, build instructions, examples”.
Yes, I read that paper but I had no idea what any of it meant, unfortunately. I gather it does something which means you can evaluate a function for some number of substitutions/timesteps and if it hasn’t terminated with output yet, give a meaningful probability for whether it ever halts, but I don’t understand anything about what that something is, what sort of probability it’s giving, or what one could do with this.
Yep, that’s what it does.
The computational “something” is actually just “run the evaluation for
msteps”. The clever bit is the “sort of probability”, which is a loose upper-bound on the measure of halting times we’ve already exceeded aftermsteps. Demonstrating how that measure makes sense is what takes up the meat of the paper.You could place bets on anything involving the Halting Problem, with sensible, well-defined, nonrandom odds.
By the way, I thought you knew computability theory professionally. Don’t you do something-or-other academic?
Can you motivate the construction any? I doubt it’s as simple as 1/n timesteps because that would be too convenient, but what is it?
That’s a tad contrived… I was thinking more along the lines of whether such an estimate could be useful in any of the traditional applications stymied by the Halting Problem, such as showing the equivalence of two functions, anti-virus checking, model checking, running sandboxed functions, resource limits, peephole optimization, etc.
No, I’m afraid I only know what I’ve picked up here and there. Not nearly enough to understand a paper like that.
It’s all the same, really. You can do all those things, but probabilistically, up to the probabilities allowed by how long you’ve run the program for. Unless and until the program halts, there will always be some chance that you were wrong about its nonhalting and it does actually halt. If it actually doesn’t halt, your confidence that it doesn’t will asymptotically approach 1.0 in the limit.
It’s not 1/n timesteps, yeah. It’s more along the lines of “Halting times for long-running programs turn out to be algorithmically non-random, which means we use this class of functions called incompressibility cut-off functions to bound the measure of halting times.” Beyond that, I’d have to start and finish a couple of textbooks (at least an intro to topology and then Calude’s own Information and Randomness) to explain more deeply.
It doesn’t help that Calude tends to use different notation in his papers from the standard notations used for studying Kolmogorov complexity/AIT.
Not really. ‘You can bet on halting’ is not a use. There is no website I can go to which has 24⁄7 gambling on randomly-generated lambda functions which I can use that code to clean up on; there is no lambda function e-sports league where competitors race to write or crack their rival’s functions, etc. This could be said of any method for calculating probabilities of anything: ‘you can bet on it!’ That’s not what I mean by use. What I meant are some of the applied tasks, but I’m not clear exactly on whether this probability applies: can I usefully use it to timeout functions being evaluated for superoptimization or peephole optimization or is there some catch or other issue? Can it be transformed from running times to other properties, similar to the connections between Halting & Godel & Rice’s theorem? etc.
That’s a little disappointing. But if you can’t explain what incompressibility cut-off functions are like, can you maybe give an idea of their general shapes? How does this scale with program length? How many steps in general would it take to reach something like 99% probability of non-halting? etc.
Which is exactly why I said “bet”: it’s a 1-normalized measure, and can thus be mathematically applied in all the ways that 1-normalized measures (probabilities) are otherwise applied.
Yes and yes, provided that you are willing to accept uncertainty. This is where we get into the distinction between “in theory” and “in practice”: in theory, we have not solved the Halting Problem. In practice, whether we can use this solution depends on what happens if we’re wrong.
If I apply a peephole optimization on the assumption that some computation is nonhalting, but it actually does halt, how bad is it for the performance or correctness of my program? I can just refuse to apply the optimization if “p >= 0.05” that the program actually will halt, of course: in general, it usually doesn’t seem as if we’re going to lose much for betting conservatively by refusing to act on the probabilistic assumption of nonhalting. That would just leave us with the same state of knowledge we had before applying Calude’s anytime algorithm.
In what cases do we really need this “solution”, then? Mostly the issues precisely connected with Halting, such as Incompleteness Theorems and Rice’s Theorem. In those cases, we face the very peculiar problem that our formal systems will not only never be able to prove most nonhalting programs to be nonhalting, but that certain programs do halt and the formal systems still can’t prove that. In those cases, Calude’s “solution” is a big help, because all we need to do is run the program until it halts, and we’ve proven it to halt, giving us constructive evidence to add the “Program X terminates” theorem to our formal system. Likewise, in cases where we need to formally prove that one-or-another program never halts, we can run the program for a long time, and then assign a probability to the formal statement “Program X never terminates”, which then lets us start assigning probabilities to theorems derived from that statement.
The question then becomes, “What degree of probability in the half-open interval [0, 1) is acceptable to me, the program’s human operator, to go ahead and believe that Program X Never Halts?”
If you want to phrase it in terms of cognition, we can then apply notions of utility and bounded-rational reasoning: a principled calculation for bounded-rational utility maximization should let you say, my agent has so-and-so much computing power, and gets so-and-so much utility out of a Halting Solution, and it thus ought to spend so-and-so much of its compute-power to obtain such-and-so a level of probabilistic confidence. The ordinary Dutch Book stuff from probability theory then tells us that the agent is behaving rationally about how it treats Halting Problems.
Wherever a limitary theorem has been established by reduction to the Halting Problem, Calude’s probabilistic “Halting Solution” can be useful, provided that you are willing to reason explicitly about what you mean by “useful” in terms of trade-offs between compute-time, surety, and utility.