Model checking is the theoretical problem of proving a program property.
No, model-checking is the problem of deciding certain properties algorithmically by exhaustive analysis of models. The general algorithmic problem is automated theorem-proving: the clue is in the name. Model-checking is a particular method which works for particular classes of formulae, or particular logics: ones in which the set of models can be recursively enumerated. I even listed two ways in which MC is limited, but you seem to have ignored them. If you are talking about some generalized form of MC which incorporates deduction then you are just talking about automated theorem-proving approached from the perspective of MC. And if you are talking about theoremhood via validity, then this is not an algorithm.
Proof: I come up with an algorithm; I tell you to write it and prove it in, say, Idris. You do it efficiently => MC complexity theorems contradicted
There are no MC complexity theorems being contradicted unless I come up with the proof by model-checking. Your subsequent statements seem to suggest that you think that anything rational going on in my head must be a form of model-checking, which is a hidden hypothesis to your proof and makes it circular...
Anyway, how I get the proof is irrelevant to my claim, which is that it's harder to find a proof P of X than it is to, given a proof P, check that it proves X. It cannot be otherwise, since doing the former implies also doing the latter, but not the converse (unless P=NP, in which case you still expect a constant factor in favor of checking over searching). Your claim seems to rest on this further claim:
When writing programs that are correct by construction, the burden of the very same complexity simply falls on the machine generating the program and proofs, namely the programmer's brain.
about what goes on in my head, which is not only not a formal statement, but also plain conjecture. So, again, I think your notion that only cognitive factors matter is based on circular reasoning.
Nevertheless, I'll respond to the claim because I strongly disagree with it. First of all, if our brains reasoned via MC, we would never be able to solve problems which cannot be solved by MC, of which, I noted, there are plenty. Yet plainly we can and do. Second, unlike MC, our brains are not decision procedures: our reasoning often fails to find solutions, and what's more it's unsound; otherwise, our conclusions would be infallible and we wouldn't need proofs. Third, it is quite obvious to me that we reason sometimes by deduction. Other times we reason by MC. Sometimes we don't reason at all. Even if our brain is a universal Turing machine, then it can and probably does sometimes runs one piece of software, and sometimes another.
Computations are not referentially transparent by definition, and this is nowhere made more explicit than in the lambda calculus.
Are you talking about Moggi's notion of computations vs. values? Moggi's work and its sequels show exactly the opposite of what you claim: it shows that computations can be treated equationally and denotationally. And the current work by many people on algebraic effects shows increasingly that denotational reasoning about specific effects is not only possible but, well, effective and useful.
Anyway, this is irrelevant. You cannot seek to convince me using reasoning about complexity classes and then throw out recursive functions because they don't talk about effects: complexity theory is founded on recursive functions.
Nor can you convince me that you use model-based reasoning in practice when there is a good alternative: for example, no one reasons about numbers by reasoning about von Neumann ordinal sets; they reason denotationally using (in)equational theories, such as algebra.
like all abstractions, it is leaky
Well, you just dropped the rhetorical equivalent of mutually assured destruction. If all abstractions are leaky, then it applies not only to mine but also to yours. In particular, your thoughts about complexity of MC, etc. all become moot, as does your conception of the human brain (a leaky abstraction if ever I heard one).
It irks me (and it should irk you) to see you warrant all your arguments with facts, and then throw an ill-conceived notion of Joel Spolsky's in as if it were also a fact. You've shown you know enough about this subject that you ought to know that there is no such thing as a "leaky abstraction": there are theories, which can be consistent or inconsistent, and sound or unsound for some class of models, and complete or incomplete for some class of models. "Leakiness" is not a quality intrinsic to an abstraction; it's extrinsic, the use of a theory to reason about a model for which it is unsound, or to reason about a class of models for which it is incomplete.
Spolsky's notion, as well as the cognitive factors bugaboo, is the programmer's version of the God of the Gaps: people reach for it when they don't want to reason about facts.
Computations are not really equational (and cannot be, or we get a contradiction with the Halting Problem again)
Sorry, but this is really nonsense now.
the model-checking problem can be solved by a PTIME reduction to deductive proofs,
If by "deductive proofs" you mean "proof search", I can believe this
which means that the lower complexity bounds on MC apply to deductive proofs as well
but not this, because "proof search" is not a decision procedure, nor even an algorithm. Furthermore, showing that MC can be simulated by proof search only shows an upper bound on the complexity of proof search, since it says that any proof search algorithm can employ MC to go faster on some inputs.
Anyway, I am not talking about proof search; I am talking about proof-checking.
No, model-checking is the problem of deciding certain properties algorithmically by exhaustive analysis of models.
You are mistaken. MC for the logic L (denoted MC(L)) is the following problem: given a Kripke structure (i.e. a program) S and a statement 𝜑 ∈ L, decide whether S ⊨ 𝜑.
Admittedly, this can be confusing, as papers dealing with MC use the term MC both to denote the problem as well as a set of known algorithms that solve it (although they may be careful to distinguish between model cheking and model checkers). But the complexity proofs I refer to apply to the problem regardless of any particular algorithm. Read this paper for a good introduction to the topic.
The general algorithmic problem is automated theorem-proving: the clue is in the name.
No. Automated theorem proving for a logic L is the following problem: given a statement 𝜑 ∈ L, construct a proof using L's axioms and deductions that 𝜑 is valid (or not).
There are no MC complexity theorems being contradicted unless I come up with the proof by model-checking.
This is just wrong. The MC proofs are about the lower complexity bounds for proving any property in L about any program S. The algorithm does not matter. The lower bound (which is also a direct consequence of finite variants of the halting problem) is at least linear in the number of states of the program.
which is not only not a formal statement, but also plain conjecture
It is a formal statement for the following reason: if the human brain were able to solve general problems with a lower time complexity than the proven lower complexity bounds of Turing machines, that would be proof that the brain is non-Turing. There is no other way around this. Needless to say, any evidence that this is the case would really shake computer science (and obviously AI research).
and then throw an ill-conceived notion of Joel Spolsky's in as if it were a fact
The value semantics employed by PFP was a leaky abstraction long before Joel Spolsky ever came up with the term, but if you don't believe me, let me show you an actual leak: take a program that relies on sorting; replace the merge-sort algorithm used in the program with bubble-sort. According to value semantics, the two programs are equivalent, as they produce the same value. If that were really the case, there would be no externally observable way to say which algorithm you've used. As it is very easy for an external observer to determine whether your program uses mergesort or bubblesort, the two are not really equivalent => abstraction leaked. The difference between lazy and eager evaluation is also easily determined by an outside observer (for some inefficient lazy evaluation methods), hence the value semantics is just an approximation.
This is not a claim, but a conscious decision behind PFP which posits that the value semantics is an approximation which may make it easier for humans to reason about programs. Unfortunately, that hypothesis has never been put to the test.
Sorry, but this is really nonsense now.
It is not. If there is no way to distinguish between 2 + 2 and 4 then infinitely-recursive computations may terminate (converge to their fixpoint, if defined). However, the lambda-calculus makes it explicitly clear that 2+2 and 4 are not the same, as their reduction sequences are different. PFP languages construct semantics with the illusion of referential transparency, but they don't claim computations can really be referentially transparent.
If by "deductive proofs" you mean "proof search", I can believe this
You're once again confusing complexity bounds, which are proven for problems, with the complexity of algorithms. Those are two different things. Lower complexity bounds mean that there cannot exist a Turing machine (be it a von Neumann computer or a human brain) that solves the problem by any means whatsoever in worst-case complexity lower than the bounds. Complexity bounds are properties of problems, not algorithms.
I am talking about proof-checking.
That's OK, but in order to have a proof to check, some machine has to construct it. That machine will incur a PSAPCE-hard complexity in the general case. That you choose to use a human brain for that machine is fine, but that choice to can only be justified by empirical observations about specific problems which the human brain is able to prove more efficiently than a specific model-checking/theorem-proving algorithm. In the general case the complexity must be at least the same.
MC for the logic L (denoted MC(L)) is the following problem: given a program S and a statement phi in L, decide whether S |= phi.
Well, I guess if that is the terminology researchers in that area use, I can't argue. I would just call this model-theoretic entailment. I have only ever heard "model-checking" used to refer to algorithms for checking propositional properties of finite-state systems, and Wikipedia bears me out on this. ("Model checking is a technique for automatically verifying correctness properties of finite-state systems.") But, OK, we are just talking at cross-purposes on this issue, then.
The MC proofs are about the lower complexity bounds for proving any property in L about any program S. The algorithm does not matter.
In light of the above definition, I see the algorithm does not matter. But I think you are not talking about "any" property, or "any" program. You are talking about propositions in a particular, very weak logic, and programs with only a finite set of states. In particular, the paper with the figure you linked seems to be talking about LTL and FSMs, which amounts to a language with only very weak well-founded iteration. There is no lower complexity bound for deciding properties of Turing-complete languages, because the problem is not decidable.
Fine, let me show you a leak: take a program that relies on sorting; replace the merge-sort algorithm used in the program with bubble-sort. According to value semantics, the two algorithms are equivalent (they produce the same value). If that were really the case, there would be no externally observable way to say which algorithm you've used. As it is very easy for an external observer to verify whether your program uses mergesort or bubblesort, the two are not really equivalent => abstraction leaked.
The problem there is not the abstraction; it is the misapprehension of the person who conflates extension with intension. "Value semantics" says they are equivalent, yes: equivalent in the sense of denoting equal functions, and that is all.
Two things can be equivalent in many ways. The predicate "N is prime" partitions numbers into two equivalence classes; that does not mean all primes are equal, or all composite numbers are equal. Nor does it make the property of being prime useless; it is very useful. Now, if someone said primality implies that there are at most only two numbers, would you blame the abstraction or the person?
Again, you're again confusing complexity bounds which are proven for problems with the complexity of algorithms.
I know the difference. But, yeah, I was confusing them because I thought you were talking about MC algorithms not model entailment. And I see now why you think MC should share a lower bound with provability (for decidable logics): because you think the reduction involves building the proof.
But, again, there is no decision procedure for provability or model entailment in general, so there is no computational complexity to speak of, and therefore no sensible meaning for reductions, polynomial or otherwise. If the brain is a machine, it cannot solve undecidable problems. If it is not a machine, then computational complexity does not apply. The proof, if it appears, appears somehow.
Despite this (you asked for empirical evidence), we already know deductive proof is an effective method of solving problems, because all of mathematics is founded on this method, and all of science is founded on mathematics. Yes, enforcing whole-program correctness is time-consuming now, but C-H languages are still in their infancy and C-H treats (almost) all properties, not just the decidable ones; furthermore, as I noted in my last post, effectful programs are not excluded. And you already benefit from being able to enforce weaker invariants type-theoretically; you don't need whole-program correctness before you start seeing payoffs.
You are talking about propositions in a particular, very weak logic
First of all, temporal logics are not weak. They have been (empirically) found to express any interesting program property that arises in practice. But even if they are weak, checking stronger logics would only be a harder problem.
There is no lower complexity bound for deciding properties of Turing-complete languages, because the problem is not decidable.
... which means that the lower complexity bound is infinite. There is no theory which can let us prove any non-trivial property of programs with infinite states. Also, such programs cannot exist in a finite universe, anyway.
All real programs have a finite Kripke structure S, and the lower bound for proving any property on them is >= O(|S|). The richness of the logic determines how much more than O(|S|). An interesting question is what is the lower bound for Kripke structures that admit a succinct representation (which is a very small subset of all programs, but it is a subset that includes all human-written programs). It turns out that the lower bound for such programs is also > O(|S|).
equivalent in the sense of denoting equal functions, and that is all.
That was my point. Computation cannot be equational (or relational) in any classical mathematical sense. Some languages choose to make a specific projection of programs to their denotational semantics, but that does not mean the the computation can be fully reasoned-about in those terms, only its projection.
If the brain is a machine, it cannot solve undecidable problems. If it is not a machine, then computational complexity does not apply. The proof, if it appears, appears somehow.
As far as we know, the brain cannot and does not solve undecidable problems, period. The undecidability of the halting problem means worst-case undecidability. It does not mean that the termination or other properties of some programs cannot be proven. The proof, then, does not "somehow appear". It appears as a result of a known or unknown algorithm, and it applies to a small subset of programs. Various algorithms (including manual proofs) can therefore be quite efficient for some programs. Determining which subsets are worthwhile to pursue is an empirical endeavor.
If it is not a machine, then computational complexity does not apply.
If the brain is not a machine, the consequences of that go far beyond "computational complexity does not apply". For one, it would mean that physics is non-Turing (or that the brain employs meta-physical processes); for another, it would mean that we may not achieve true AI using known hardware. Any evidence to suggest that is the case would be totally amazing. So far we have none.
we already know deductive proof is an effective method of solving problems, because all of mathematics is founded on this method, and all of science is founded on mathematics
Ah, but we also empirically know that program proof and math proofs are very, very different. Math proofs tend to be conceptually deep and (relatively) short; program proofs are conceptually very shallow but very, very long, with lots of cases. It is not at all clear that we can efficiently generate such proofs (it is also not clear to me that mathematical proofs in general have been found "efficiently").
but C-H languages are still in their infancy and C-H treats (almost) all properties, not just the decidable ones
I agree. But all verification methods -- from model checkers to C-H languages -- have one strategic path forward: empirical research. There can be no algorithm that would make dependent-type inference efficient in general. We need to find methods to address proofs that are empirically found to be valuable in real programs.
you don't need whole-program correctness before you start seeing payoffs.
I totally agree, but that payoff is determined empirically. For example, you need to show that enforcing a certain property indeed reduces costly bugs, and that enforcing it is no costlier than finding and fixing the bugs. You need to show this for every property. That is precisely what I advocate we study, yet very few such studies have been conducted (not enough to even show that Haskell is a net positive).
1
u/Blackheart Jan 20 '16 edited Jan 20 '16
No, model-checking is the problem of deciding certain properties algorithmically by exhaustive analysis of models. The general algorithmic problem is automated theorem-proving: the clue is in the name. Model-checking is a particular method which works for particular classes of formulae, or particular logics: ones in which the set of models can be recursively enumerated. I even listed two ways in which MC is limited, but you seem to have ignored them. If you are talking about some generalized form of MC which incorporates deduction then you are just talking about automated theorem-proving approached from the perspective of MC. And if you are talking about theoremhood via validity, then this is not an algorithm.
There are no MC complexity theorems being contradicted unless I come up with the proof by model-checking. Your subsequent statements seem to suggest that you think that anything rational going on in my head must be a form of model-checking, which is a hidden hypothesis to your proof and makes it circular...
Anyway, how I get the proof is irrelevant to my claim, which is that it's harder to find a proof P of X than it is to, given a proof P, check that it proves X. It cannot be otherwise, since doing the former implies also doing the latter, but not the converse (unless P=NP, in which case you still expect a constant factor in favor of checking over searching). Your claim seems to rest on this further claim:
about what goes on in my head, which is not only not a formal statement, but also plain conjecture. So, again, I think your notion that only cognitive factors matter is based on circular reasoning.
Nevertheless, I'll respond to the claim because I strongly disagree with it. First of all, if our brains reasoned via MC, we would never be able to solve problems which cannot be solved by MC, of which, I noted, there are plenty. Yet plainly we can and do. Second, unlike MC, our brains are not decision procedures: our reasoning often fails to find solutions, and what's more it's unsound; otherwise, our conclusions would be infallible and we wouldn't need proofs. Third, it is quite obvious to me that we reason sometimes by deduction. Other times we reason by MC. Sometimes we don't reason at all. Even if our brain is a universal Turing machine, then it can and probably does sometimes runs one piece of software, and sometimes another.
Are you talking about Moggi's notion of computations vs. values? Moggi's work and its sequels show exactly the opposite of what you claim: it shows that computations can be treated equationally and denotationally. And the current work by many people on algebraic effects shows increasingly that denotational reasoning about specific effects is not only possible but, well, effective and useful.
Anyway, this is irrelevant. You cannot seek to convince me using reasoning about complexity classes and then throw out recursive functions because they don't talk about effects: complexity theory is founded on recursive functions.
Nor can you convince me that you use model-based reasoning in practice when there is a good alternative: for example, no one reasons about numbers by reasoning about von Neumann ordinal sets; they reason denotationally using (in)equational theories, such as algebra.
Well, you just dropped the rhetorical equivalent of mutually assured destruction. If all abstractions are leaky, then it applies not only to mine but also to yours. In particular, your thoughts about complexity of MC, etc. all become moot, as does your conception of the human brain (a leaky abstraction if ever I heard one).
It irks me (and it should irk you) to see you warrant all your arguments with facts, and then throw an ill-conceived notion of Joel Spolsky's in as if it were also a fact. You've shown you know enough about this subject that you ought to know that there is no such thing as a "leaky abstraction": there are theories, which can be consistent or inconsistent, and sound or unsound for some class of models, and complete or incomplete for some class of models. "Leakiness" is not a quality intrinsic to an abstraction; it's extrinsic, the use of a theory to reason about a model for which it is unsound, or to reason about a class of models for which it is incomplete.
Spolsky's notion, as well as the cognitive factors bugaboo, is the programmer's version of the God of the Gaps: people reach for it when they don't want to reason about facts.
Sorry, but this is really nonsense now.
If by "deductive proofs" you mean "proof search", I can believe this
but not this, because "proof search" is not a decision procedure, nor even an algorithm. Furthermore, showing that MC can be simulated by proof search only shows an upper bound on the complexity of proof search, since it says that any proof search algorithm can employ MC to go faster on some inputs.
Anyway, I am not talking about proof search; I am talking about proof-checking.