5 ms·

This is a very common misconception. While Turing complete computational models "suffer" from the halting problem that makes arbitrary "reasoning" uncomputable,

by pron 9y ago

This is a very common misconception. While Turing complete computational models "suffer" from the halting problem that makes arbitrary "reasoning" uncomputable, that is 1. not quite the problem that makes reasoning hard, and 2. that does not mean that reasoning in weaker models is feasible. 1. What makes reasoning hard is not quite the halting theorem as normally stated, but a generalization of it that's sometimes called "bounded halting", and was used in the proof of the time-hierarchy theorem, possibly the most important theorem in theoretical computer science. Bounded halting roughly states that it's impossible to know in under N steps whether an arbitrary program P would halt when operating on input X in fewer than N steps. A simple corollary also shows the impossibility of generalizing the program's operation from one input to another. In short, this theorem means that it's impossible to know what a program would do for any input any faster than running it for every input. It can roughly be stated as saying that the verification or "reasoning" complexity for a program with a state space S of size |S| is θ(|S|) (where theta is like big-O, except it roughly means "no more and no less than", whereas big-O means "no more than"). Most importantly, this theorem does not require the programming model to be Turing complete. For example, it applies directly -- using the same proof -- to programming models that only allow primitive recursive functions. 2. Even the simplest computational model -- the barely useful finite-state machine -- is already too complicated for arbitrary reasoning. Its verification complexity also happens to be θ(|S|) (but with a different proof than that of the bounded halting theorem), where |S| is usually at least exponential in the size of the program. In general it can very easily be shown that if your programming languages has nothing more than boolean variables and the ability to write loops of length of no more than 2 or, alternatively, it has subroutines even if they cannot be recursive and there are no first-class subroutines -- reasoning is also infeasible (it's PSPACE-complete) and you might as well be Turing complete, as that won't make the worst-case any harder in practice (it makes no difference if the worst case is truly infinite or "just" much longer than the expected lifespan of the universe). The above fact means it is provably impossible to create a programming language -- no matter how limited -- where every program would be easily verifiable. To make a language feasibly verifiable in all/most cases, its state space must grow slowly (polynomially) with program size; this means that not only must the programming model be weak (basically just FSM), but the language exceptionally inexpressive. Regular expressions are pretty much the farthest we can go, and even then some simple questions about regexps are infeasible (such as whether two regexps are equivalent; I believe that problem is PSPACE complete, even though there are heuristic algorithms that work in many instances). For further discussion and complete results, see my post: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

vidarh 9y ago
> 2. that does not mean that reasoning in weaker models is feasible. If you limit it explicitly to models powerful enough to run arbitrary computation, then that sounds reasonable. But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations. A simple example is that you can easily define a model of computation that "solves" the halting problem the crude way: Just add an upper bound to the number of steps, and halt the problem after that number of steps. Now you know any program halts. Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs. More reasonable examples would be specialized domain languages like Sieve for filtering e-mail, that address reasoning by having no branching or loops or writable state. The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.
- pron 9y ago
  > But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations. This is not true, and precisely the point of my comment. There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case. When I said "arbitrary" I meant arbitrary in whatever restricted model you give me. We can reason about many special cases, but we can (and do) do that for Turing complete languages, too. > Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs. Again, this is not true. Knowing that your algorithm is bounded by some number, gives you no additional information usable in verifying it. There is still no faster way of answering questions than running the program on all inputs up to that number. > that address reasoning by having no branching or loops or writable state. If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them. > The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy. This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve. For almost any computational model (barring a couple of very special exceptions), the verification complexity is θ(|S|). As we know the minimum number of states for algorithms, the verification cost is known. The only thing you can do is make the languages so inexpressive that programs increase polynomially or exponentially in size, and so the verification complexity would decrease. In general, the idea that a weaker computational model makes reasoning easy is a myth (obviously not one shared among researchers). The myth is probably because many practitioners know about the halting theorem but not about more significant computational complexity results, and mistakenly believe that it is that result which is the cause of the difficulty of verification.

by pron 9y ago

vidarh 9y ago

> 2. that does not mean that reasoning in weaker models is feasible. If you limit it explicitly to models powerful enough to run arbitrary computation, then that sounds reasonable. But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations. A simple example is that you can easily define a model of computation that "solves" the halting problem the crude way: Just add an upper bound to the number of steps, and halt the problem after that number of steps. Now you know any program halts. Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs. More reasonable examples would be specialized domain languages like Sieve for filtering e-mail, that address reasoning by having no branching or loops or writable state. The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.

pron 9y ago
> But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations. This is not true, and precisely the point of my comment. There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case. When I said "arbitrary" I meant arbitrary in whatever restricted model you give me. We can reason about many special cases, but we can (and do) do that for Turing complete languages, too. > Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs. Again, this is not true. Knowing that your algorithm is bounded by some number, gives you no additional information usable in verifying it. There is still no faster way of answering questions than running the program on all inputs up to that number. > that address reasoning by having no branching or loops or writable state. If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them. > The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy. This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve. For almost any computational model (barring a couple of very special exceptions), the verification complexity is θ(|S|). As we know the minimum number of states for algorithms, the verification cost is known. The only thing you can do is make the languages so inexpressive that programs increase polynomially or exponentially in size, and so the verification complexity would decrease. In general, the idea that a weaker computational model makes reasoning easy is a myth (obviously not one shared among researchers). The myth is probably because many practitioners know about the halting theorem but not about more significant computational complexity results, and mistakenly believe that it is that result which is the cause of the difficulty of verification.