5 ms·

> It doesn't say anything about "non-trivial" programs. No, but its source does. The source for the Turing Halting problem is Gödel's incompleteness theorems,

• deleted 11y ago
  [deleted]
• geofft 11y ago
  > The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected. Gödel doesn't say anything about "non-trivial" any more than Turing does. His first theorem is a "there exists at least one statement" thing, just like the halting problem. Like the halting problem, the proof is a proof by construction, but that statement is not a statement that anyone would a priori are to prove, just like the program "If I halt, run forever" is not a program that anyone would particularly want to run. So while yes, they're deeply connected, from the point of view of proving actual systems correct, it's not clear they matter. And neither theorem says anything about "non-trivial" statements/programs (just about non-trivial formalizations and languages). Gödel's second theorem is super relevant, though: it says that any consistent system cannot prove its own consistency. But that's fine. Coq itself is implemented in a Turing-complete language (ML), not in Coq. It would be nice if we could verify Coq in Coq itself, but since Gödel said we can't, we move on with life, and we just verify other things besides proof assistants. (And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.) This is not waving away the problem, it's acknowledging it and working within the limits of the problem to do as much as possible. And while that's not everything, it turns out a lot of stuff of practical importance -- perhaps everything of practical importance besides proving the system complete in its own language -- is possible.
  • lutusp 11y ago
    > Gödel doesn't say anything about "non-trivial" any more than Turing does. Source: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem Quote: "Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions." Source: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Quote: "Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic." > It would be nice if we could verify Coq in Coq itself ... I was planning to bring this issue up, but you've done it for me. The simplest explanation of these two related theorems involves the issue of self-reference. Imagine there is a library, and a very conscientious librarian wants to have a provably correct account of the library's contents. The librarian therefore compiles an index of all the works in the library and declares victory. Then Gödel shows up and says, "On which shelf shall we put the index?" In the same way, and for the same reason, non-trivial logical systems cannot check themselves, computer languages cannot validate their products (or themselves), and compilers cannot prove their own results correct. > And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness. Yes, unless someone is misled into thinking this means the checked code has been proven correct. > This is not waving away the problem ... When someone declares that a piece of code has been proven correct, in point of fact, yes, it is.
    • geofft 11y ago
      > for any non-trivial property, there is no general decision procedure that, for all programs > all but the most trivial axiomatic systems This is about non-trivial properties on arbitrary programs, and non-trivial axiomatic systems proving arbitrary statements. It is not about non-trivial programs or non-trivial statements. Rice's theorem states that, for all non-trivial properties P, there exists a program S where you cannot compute P(S). (The Wikipedia phrasing puts the negative in a different spot, but this is de Morgan's law for quantifiers: ∀P ¬∀S P(S) is computable = ∀P ∃S ¬ P(S) is computable.) Gödel's first theorem is that, for all non-trivial formalizations P, there exists a statement S where you cannot prove P in S. You are claiming, for all non-trivial properties P, for all non-trivial programs S, you cannot compute P(S); for all non-trivial formalizations P, for all non-trivial statements S, you cannot prove P in S. This is not what Rice's or Gödel's theorems are, and not what the texts you quoted say. > Then Gödel shows up and says, "On which shelf shall we put the index?" You keep it outside the library. The index tells you where every single book is, other than the index. In particular, Gödel claims that, if the index has any chance of being correct, it must be outside the library. The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct; in fact, Gödel's second theorem means that if it could be proven in itself, we'd be confident it was wrong!