5 ms·
> 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
by 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.
- deleted 9y ago[deleted]
- vidarh 9y ago> There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case. I gave you an example: Sieve. > 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. Sieve, as I mentioned fits in this category (though I'd not be surprised if there are extensions that break this; there are many, but the basic language is sufficiently constrained and still useful). The point is not to do "the vast majority of tasks" in them, but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care. (... but leads to unexpected Turing completeness now and again when people don't take care, as the article points out) E.g. aforementioned Sieve is constrained this way explicitly to be safe to let end-users -- or scripts on their behalf -- construct Sieve filters to run during delivery on mail servers without e.g. having to impose any other restrictions than a size limit. > This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve. I think you misunderstood what I wrote. The sentence you quoted here is arguing that people make mistakes when defining the kind of restricted languages I'm discussing all the time so that verification gets harder. You seem to think it was talking about making verification easier. > In general, the idea that a weaker computational model makes reasoning easy is a myth And again: This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation. Here's one: Consider a machine whose only instruction is "halt", which halts execution. Clearly this model is trivial to reason about. You may intend a "useful" in there somewhere, in which case I point you again to Sieve, which is still trivial enough unless you carelessly add extensions.
- pron 9y ago> I gave you an example: Sieve. I said "of wide utility". BTW, I don't know Sieve, but if it has regular expressions then reasoning about it is also infeasible (e.g. checking whether two filters based on regular expressions are equivalent). > but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care. I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case. > This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation. No. I'm talking about arbitrary programs in whatever language you give me. If your language has regular expressions -- game over. If it has variables and subroutines/limited loops -- game over. And those are just the PSPACE-hard cases. If all you have in your language is boolean connectives (i.e., it's a propositional calculus) -- no subroutines, no loops and no mutable variables -- verifying it is "just" NP-hard. Special cases, on the other hand, are often possible to reason about even automatically even in Turing complete languages. > You may intend a "useful" in there somewhere, in which case I point you again to Sieve, which is still trivial enough unless you carelessly add extensions. I did say useful, and either Sieve is not very widely applicable and/or, if it has regular expressions it cannot be feasibly reasoned about.