2 ms·

The undecidability of a specific formulation of the halting problem is practically irrelevant, but you should never take published results too literally. If the

The undecidability of a specific formulation of the halting problem is practically irrelevant, but you should never take published results too literally. If the halting problem is undecidable in one formalism, it is also undecidable in many other formalisms, and so is a wide class of other problems that can be reduced to the halting problem. Rice's theorem is one immediate consequence of the undecidability of the halting problem. It effectively states that if you are writing code that analyzes (certain external behavior of) other code, there will always be edge cases your code cannot handle. It is useful to understand that the perfect algorithm is not out there, just waiting to be discovered. Instead of searching for it, you should start thinking about the trade-offs between resource usage and the ability to handle increasingly rare edge cases. I'm not a fan of resource-bounded variants of decision problems, because the standard complexity classes are ugly beasts. Reasoning about them is so difficult that many fundamental problems remain unsolved. And even if you manage to prove something, the excessive use of quantifiers means that you only learn something about the worst-case behavior with some arbitrarily large inputs. The resource-bounded problems also miss the point. Impossibility results are not really about the impossibility of proving something with realistic or unrealistic resources. The proof ideas are often more important than the results. One idea is particularly simple: if you have already written your code, I can write an input that fools it.

skissane 5y ago
> Rice's theorem is one immediate consequence of the undecidability of the halting problem. I wonder if one could construct a bounded analogue of Rice's theorem? Something like "all non-trivial, semantic properties of programs that use maximum resources R are undecidable by programs using maximum resources R". > I'm not a fan of resource-bounded variants of decision problems, because the standard complexity classes are ugly beasts. Reasoning about them is so difficult that many fundamental problems remain unsolved. It seems to be that, reasoning about actual computers is harder than reasoning about physically impossible theoretical ones, so people would prefer to study the later than the former. Fair enough, but surely the former study is more practically relevant – even if harder – than the later; and I don't know why in the later the study of one particular class of physically impossible machines (Turing-equivalent machines) gets privileged over the study of other more powerful classes of physically impossible machines (such as oracle machines, or supertask machines). All physically impossible machines are equally physically impossible. (Privileged not in the sense of being ignored – of course there is a great deal of theoretical work done on super-Turing computation; but privileged in the sense that super-Turing computation is often presented as something only of interest to specialists, whereas work on Turing-equivalent computation gets promoted as something of practical relevance and general interest.) > One idea is particularly simple: if you have already written your code, I can write an input that fools it. Here's a very similar idea about computation with bounded resources: If you had a perfect program analysis program that only worked for programs consuming up to some resource limit R, then it would require more than R to apply the same analysis to itself. And either idea may not be true for dialetheic machines [0]. Dialetheic machines are, as far as we know, not physically realisable; but Turing machines aren't either. [0] https://www.springerprofessional.de/en/paraconsistent-computation-and-dialetheic-machines/11237682 https://www.springerprofessional.de/en/paraconsistent-comput...

skissane 5y ago

> Rice's theorem is one immediate consequence of the undecidability of the halting problem. I wonder if one could construct a bounded analogue of Rice's theorem? Something like "all non-trivial, semantic properties of programs that use maximum resources R are undecidable by programs using maximum resources R". > I'm not a fan of resource-bounded variants of decision problems, because the standard complexity classes are ugly beasts. Reasoning about them is so difficult that many fundamental problems remain unsolved. It seems to be that, reasoning about actual computers is harder than reasoning about physically impossible theoretical ones, so people would prefer to study the later than the former. Fair enough, but surely the former study is more practically relevant – even if harder – than the later; and I don't know why in the later the study of one particular class of physically impossible machines (Turing-equivalent machines) gets privileged over the study of other more powerful classes of physically impossible machines (such as oracle machines, or supertask machines). All physically impossible machines are equally physically impossible. (Privileged not in the sense of being ignored – of course there is a great deal of theoretical work done on super-Turing computation; but privileged in the sense that super-Turing computation is often presented as something only of interest to specialists, whereas work on Turing-equivalent computation gets promoted as something of practical relevance and general interest.) > One idea is particularly simple: if you have already written your code, I can write an input that fools it. Here's a very similar idea about computation with bounded resources: If you had a perfect program analysis program that only worked for programs consuming up to some resource limit R, then it would require more than R to apply the same analysis to itself. And either idea may not be true for dialetheic machines [0]. Dialetheic machines are, as far as we know, not physically realisable; but Turing machines aren't either. [0] https://www.springerprofessional.de/en/paraconsistent-computation-and-dialetheic-machines/11237682 https://www.springerprofessional.de/en/paraconsistent-comput...