4 ms·

You have missed an important point: Your technology is not yes/no/dunno, but yes/no/dunno/loop. Turing-completeness implies Rice's Theorem, which is basically a

You have missed an important point: Your technology is not yes/no/dunno, but yes/no/dunno/loop. Turing-completeness implies Rice's Theorem, which is basically a fancy way of saying that you can't escape Turing's results just by claiming that you're solving an "easier" problem as long as that problem is still non-trivial. I'm sorry that you think that our amazing farsighted glimpse of the edge of computational infinity is "short-sighted", but in reality these upper bounds are very useful for reminding us of the certain futility of certain tasks. Moreover, I am also happy to point out that a problem not need be Turing-complete to be computationally intractable even if decidable. Compilers happily cheat on optimizations, register layout, etc. if it means not having to run expensive algorithms. When a type-checker is accidentally quadratic-time, people roll their eyes and fix it; when it's intentionally exponential-time, people will avoid it entirely.

SamReidHughes 10y ago
You can bound your loops and say you don't know. I thought that's what the parent meant by "don't know."
bbcbasic 10y ago
if loopcount > limit then Left Dunno else Right ...
DannyBee 10y ago
Except you can bound it, and you can escape it that way. IE "not gotten anywhere after 30 iterations, so don't know". Otherwise, you couldn't, for example, ever compute the tripcount for a loop without risking running forever. " Compilers happily cheat on optimizations, register layout, etc." They don't cheat. They just make the problem easier at a cost of optimality. Or, they discover they didn't need to solve the problem they thought they did. A great example is register allocation. NP-complete to do graph coloring. NP-complete to decide if a given graph admits a k-coloring for a given k except for the cases k ∈ {0,1,2}. NP-hard to compute the chromatic number (ie just figuring out the minimum number of colors for a graph) This was the state, right up until a number of people proved that, if you do it on SSA form (a linear time transformation), you can optimally color it in linear time. A small difference. So, often, these upper bounds that seem "futile", maybe are not as futile as one thinks.
- theseoafs 10y ago
  > Except you can bound it, and you can escape it that way. IE "not gotten anywhere after 30 iterations, so don't know". It should go without saying that this system is not Turing-complete anymore if you bound the runtime.
  - UncleMeat 10y ago
    But you aren't bounding the runtime of the thing. You are bounding the runtime of your abstract interpreter of the thing.
  - oculusthrift 10y ago
    that is correct. the whole point is we can make practical real world tradeoffs and break out of the shackles of theoretical constraints.
  - Klockan 10y ago
    This is like saying that no programming language is Turing-complete since they are all implemented with finite memory.
  - DannyBee 10y ago
    As someone points out, no system we use is really turing complete, since no system has truly infinite memory. In most systems with finite memory, the halting problem is solvable anyway. (this includes linear bounded automatons and deterministic/non-deterministic machines with finite memory). It's just going to take a long ass time.
johncolanduoni 10y ago
All type checkers for sophisticated dependent type theories (e.g. MLTT) will resist any bound on time or memory you try to place, let alone a quadratic or exponential one. Somehow nobody seems to complain about how long they take to type-check. Both decidability and worst case time bounds are red herrings when it comes to a good type system (even for proof assistants).

SamReidHughes 10y ago

You can bound your loops and say you don't know. I thought that's what the parent meant by "don't know."

bbcbasic 10y ago

if loopcount > limit then Left Dunno else Right ...

DannyBee 10y ago

Except you can bound it, and you can escape it that way. IE "not gotten anywhere after 30 iterations, so don't know". Otherwise, you couldn't, for example, ever compute the tripcount for a loop without risking running forever. " Compilers happily cheat on optimizations, register layout, etc." They don't cheat. They just make the problem easier at a cost of optimality. Or, they discover they didn't need to solve the problem they thought they did. A great example is register allocation. NP-complete to do graph coloring. NP-complete to decide if a given graph admits a k-coloring for a given k except for the cases k ∈ {0,1,2}. NP-hard to compute the chromatic number (ie just figuring out the minimum number of colors for a graph) This was the state, right up until a number of people proved that, if you do it on SSA form (a linear time transformation), you can optimally color it in linear time. A small difference. So, often, these upper bounds that seem "futile", maybe are not as futile as one thinks.

theseoafs 10y ago
> Except you can bound it, and you can escape it that way. IE "not gotten anywhere after 30 iterations, so don't know". It should go without saying that this system is not Turing-complete anymore if you bound the runtime.
- UncleMeat 10y ago
  But you aren't bounding the runtime of the thing. You are bounding the runtime of your abstract interpreter of the thing.
- oculusthrift 10y ago
  that is correct. the whole point is we can make practical real world tradeoffs and break out of the shackles of theoretical constraints.
- Klockan 10y ago
  This is like saying that no programming language is Turing-complete since they are all implemented with finite memory.
- DannyBee 10y ago
  As someone points out, no system we use is really turing complete, since no system has truly infinite memory. In most systems with finite memory, the halting problem is solvable anyway. (this includes linear bounded automatons and deterministic/non-deterministic machines with finite memory). It's just going to take a long ass time.

johncolanduoni 10y ago

All type checkers for sophisticated dependent type theories (e.g. MLTT) will resist any bound on time or memory you try to place, let alone a quadratic or exponential one. Somehow nobody seems to complain about how long they take to type-check. Both decidability and worst case time bounds are red herrings when it comes to a good type system (even for proof assistants).