3 ms·
>We know the effect of different programming constructs on expressive compression and reasoning costs. The closer we get to the limit, the less benefit we can h
by fauigerzigerk 7y ago
>We know the effect of different programming constructs on expressive compression and reasoning costs. The closer we get to the limit, the less benefit we can have.
>Here, too, there are theoretical results showing that increased expressiveness cannot lead to cheaper reasoning, which is not an obvious result even in the worst case (because there are far fewer "compressible" programs than non compressible ones).
I find that very interesting. Do you have a source for it?
- pron 7y agoYes. Some interesting papers are: * http://www.lsv.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf http://www.lsv.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf * http://www.lsv.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf http://www.lsv.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf * https://www.cis.upenn.edu/~alur/Zohar03.pdf https://www.cis.upenn.edu/~alur/Zohar03.pdf What's important to put those results in context for those who are not familiar with the subject is that, in the context of complexity theory, the "model checking problem" does not refer to the complexity of a particular model checker algorithm, but to the inherent complexity of the problem of deciding whether a program M satisfies some property 𝜑 (i.e. whether M is a model of 𝜑 in the formal logic sense). The "model checking problem" is the closest to a mathematical description of what we usually mean when we talk of "reasoning about a program." I've summarized these results and more here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity
- fauigerzigerk 7y agoThanks!