4 ms·

For me, Turing completeness means being able to implement every computable function of type Integer -> Integer. Total languages can't do that. They need an addi

For me, Turing completeness means being able to implement every computable function of type Integer -> Integer. Total languages can't do that. They need an additional input that bounds the number of steps, but the whole point of Turing completeness is not needing that input, but rather being able to run any Turing machine until it stops on its own. Otherwise you'd be forced to conclude that many languages known to be not Turing complete, like the simply typed lambda calculus, are Turing complete in disguise, and the definition loses all teeth. This is similar to the Brown-Palsberg self-interpreter in a total language, which caused a lot of confusion recently because it's not a self-interpreter (it doesn't take source code as an argument). I think it's better to stick with common definitions and accept that total languages are not Turing complete and can't self-interpret.

pron 10y ago
There's a subtlety here. Total functional languages are necessary when the language is used as a general theorem prover via propositions-as-types (it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations; for all intents and purposes, the halting theorem still holds, as its bounded version -- which is what matters -- does not require self-interpretation for diagonalization). Now, for this to work, any computation that is represented as a function -- how computations are normally represented in functional languages -- must provably terminate, otherwise an inconsistency may be introduced into the logic corresponding to the program (this inconsistency does not apply when actual computations are concerned, only when the program represents a general mathematical theorem). However, computations may be represented not as functions but as monads, too, and introducing a monad that, while not implementable in the language itself, loops forever does not harm the totality that matters to theorem proving.
- tome 10y ago
  > it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.
  - pron 10y ago
    > Can you link any examples There are a couple in this very discussion: https://news.ycombinator.com/item?id=12648261 https://news.ycombinator.com/item?id=12648261 https://news.ycombinator.com/item?id=12648932 https://news.ycombinator.com/item?id=12648932 A quick Google search I did just now came up with this one, by someone who knows better[1]: By writing programs in a total language like this, you can confidently answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering. The only question you can confidently answer is "does the program halt", to which the answer is always yes. You cannot confidently answer any other question any easier than in non-total languages. You can find more examples in recent discussions about the Ethereum heist, with many suggestions to "just use a non-Turing complete language". Many seem to believe that there are languages that make verification easy, or that Turing completeness is the problem. > It seems a really strange claim to make I guess the reasoning goes like this: the impossibility of proving things in general about programs is a result of the halting theorem; we can get around the halting theorem by using languages that only admit programs that halt; assuming the language is still useful -- problem solved! How many people know about bounded halting? I know I hadn't until rather recently, when I thought about it and somebody pointed out to me that it's at the very core of the time-hierarchy theorem. I think I actually thought about it because of total languages, when I realized that every program can be assumed to be total without loss of generality, and so totality cannot add actionable information. [1]: https://www.quora.com/Can-we-solve-the-halting-problem-by-defining-a-language-that-is-almost-Turing-complete-i-e-one-that-can-only-express-halting-programs-and-excludes-only-a-minimum-of-programs-that-are-weird-because-of-undecidability https://www.quora.com/Can-we-solve-the-halting-problem-by-de...
wyager 10y ago
You can't write every possible term of that type. However, you can write a program that performs the same computation as any expression of that type by explicitly breaking recursion out, e.g. via Free (() ->) Integer And then using corecursion to evaluate this step by step. The actual definition of Turing completeness is the ability to implement any program that a Turing machine can compute, which you can with corecursion.

pron 10y ago

There's a subtlety here. Total functional languages are necessary when the language is used as a general theorem prover via propositions-as-types (it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations; for all intents and purposes, the halting theorem still holds, as its bounded version -- which is what matters -- does not require self-interpretation for diagonalization). Now, for this to work, any computation that is represented as a function -- how computations are normally represented in functional languages -- must provably terminate, otherwise an inconsistency may be introduced into the logic corresponding to the program (this inconsistency does not apply when actual computations are concerned, only when the program represents a general mathematical theorem). However, computations may be represented not as functions but as monads, too, and introducing a monad that, while not implementable in the language itself, loops forever does not harm the totality that matters to theorem proving.

tome 10y ago
> it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.
- pron 10y ago
  > Can you link any examples There are a couple in this very discussion: https://news.ycombinator.com/item?id=12648261 https://news.ycombinator.com/item?id=12648261 https://news.ycombinator.com/item?id=12648932 https://news.ycombinator.com/item?id=12648932 A quick Google search I did just now came up with this one, by someone who knows better[1]: By writing programs in a total language like this, you can confidently answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering. The only question you can confidently answer is "does the program halt", to which the answer is always yes. You cannot confidently answer any other question any easier than in non-total languages. You can find more examples in recent discussions about the Ethereum heist, with many suggestions to "just use a non-Turing complete language". Many seem to believe that there are languages that make verification easy, or that Turing completeness is the problem. > It seems a really strange claim to make I guess the reasoning goes like this: the impossibility of proving things in general about programs is a result of the halting theorem; we can get around the halting theorem by using languages that only admit programs that halt; assuming the language is still useful -- problem solved! How many people know about bounded halting? I know I hadn't until rather recently, when I thought about it and somebody pointed out to me that it's at the very core of the time-hierarchy theorem. I think I actually thought about it because of total languages, when I realized that every program can be assumed to be total without loss of generality, and so totality cannot add actionable information. [1]: https://www.quora.com/Can-we-solve-the-halting-problem-by-defining-a-language-that-is-almost-Turing-complete-i-e-one-that-can-only-express-halting-programs-and-excludes-only-a-minimum-of-programs-that-are-weird-because-of-undecidability https://www.quora.com/Can-we-solve-the-halting-problem-by-de...

wyager 10y ago

You can't write every possible term of that type. However, you can write a program that performs the same computation as any expression of that type by explicitly breaking recursion out, e.g. via Free (() ->) Integer And then using corecursion to evaluate this step by step. The actual definition of Turing completeness is the ability to implement any program that a Turing machine can compute, which you can with corecursion.