5 ms·
This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerf
by feanaro 4y ago
This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.
- mkleczek 4y agoThere are two problems with this: 1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help. 2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.
- ncmncm 4y agoIt is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.
- mkleczek 4y ago> It suffices that we can reliably construct machines that perform a desired function and have the desired property. See above - there is no reliable procedure (algorithm) that would allow you to do that.
- feanaro 4y agoYet languages with totality checkers and coinduction like Idris exist. These allow you to make useful but provably terminating programs. Humans are able to construct these termination proofs, though presumably not for all programs. In practice, this means that the reductive take of Turing completeness, the halting problem and Rice's theorem is misleading in some way. Yes, there is no general algorithm for constructing termination proofs for any arbitrary Turing machine. But there are clearly classes of problems for which a biological computer (a human) is able to construct termination proofs and proofs regarding other semantic properties.
- deleted 4y ago[deleted]