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.
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.