4 ms·

Stupid question, isn't this the Halting Problem?

johnbender 9y ago
Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
- schoen 9y ago
  I keep encountering what I think is a misunderstanding of Rice's Theorem. Rice's Theorem says no program can correctly decide any nontrivial property for every program. However, there are programs that can correctly decide nontrivial properties for many programs! To avoid the Rice's Theorem issue, you just need to be able to say "Don't know"/"Couldn't decide".
  - kobeya 9y ago
    The important word there was “every”.
    - schoen 9y ago
      Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
      - nullc 9y ago
        This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner. An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction. It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case. In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
        unboxed_type 9y ago
        > it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land. I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.
hossbeast 9y ago
Which is why the language is not Turing complete
mietek 9y ago
This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit uncontrolled general recursion. (Likewise for Rice's theorem.) Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps. See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/master/doc/pdf/turner-2004.pdf https://github.com/mietek/total-functional-programming/blob/... Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving. Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...

Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.

schoen 9y ago
I keep encountering what I think is a misunderstanding of Rice's Theorem. Rice's Theorem says no program can correctly decide any nontrivial property for every program. However, there are programs that can correctly decide nontrivial properties for many programs! To avoid the Rice's Theorem issue, you just need to be able to say "Don't know"/"Couldn't decide".
- kobeya 9y ago
  The important word there was “every”.
  - schoen 9y ago
    Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
    - nullc 9y ago
      This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner. An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction. It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case. In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
      - unboxed_type 9y ago
        > it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land. I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.

hossbeast 9y ago

Which is why the language is not Turing complete

mietek 9y ago

This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit uncontrolled general recursion. (Likewise for Rice's theorem.) Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps. See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/master/doc/pdf/turner-2004.pdf https://github.com/mietek/total-functional-programming/blob/... Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving. Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...