Comment by eru | Hacker News Reader

Comment by eru | Hacker News Reader

Parent Full thread

Interesting article!

> Furthermore, there is literally no way to tell whether your program will ever actually terminate without actually executing it. And there are many, many, many, ways to write a program which make it “slow” to execute. “Slow” being… like really slow.

Nitpick: there are some languages where you can tell whether your program will terminate without running it. There are even languages where you can tell whether your program will be slow.

And there are even more specialised languages where any program will be 'fast'.

Obviously, these languages aren't Turing complete. It's an interesting exercise to explore the design space to find languages that are both useful and avoid being Turing complete.

Agda is an example of a language that allows you to run approximately any practical computation, but it's not Turing complete. Oversimplified: in Agda a program is only considered valid by the compiler, if it comes with a computer-checkable proof of halting on all inputs.

> Obviously, these languages aren't Turing complete.

Interestingly, a Turing complete language without non-halting programs could exist conceptually (rather, many do); it's just impossible to know it has that property (hard to use in practice if you don't know it has the guarantees you'd like), and it can't be finitely describable (impossible to implement a compiler for it which doesn't sometimes "succeed" at compiling invalid programs).

You can also construct programs in Turing complete languages to always halt (e.g. by bounding the number of iterations of all loops, usually with the tradeoff of limited input size).

Yes, you can program in a subset of your language that is not Turing complete.

You'd also need to forbid (even indirect) recursion, i. e. one function cannot appear in a callstack twice.

I think you can allow finite recursions, eg, a maximum stack depth.

But then reaching it will mean a crash. I could use a similar approach to say that any program will terminate if I set a fixed time (instruction count) limit.

Yes — that’s correct.

Programs with a fixed amount of execution time always terminate. That’s why we add timeouts to executions, because they’re a solution to the halting problem, which guarantees execution flow of our machines always returns at some point.

Isn't that overly restrictive? Some programs are guaranteed to terminate even with mutual recursion.

For example, these (obviously inefficient) functions always terminate for all values of x, since both terminate given an input of 0, and 0 is the minimum possible input to these functions.

  bool even(unsigned int x)
  {
    return (n == 0) ? true : odd(n - 1);
  }

  bool odd(unsigned int x)
  {
    return (n == 0) ? false : even(n - 1);
  }

The point of these restrictions is that you can formally verify that a given program will terminate in a way which can be checked by e.g. a compiler or some other kind of checker.

While statically verifying your snippet is possible, it is also significantly more difficult to do than enforcing rules like "all loops must have an upper limit". I also think that you'd need dependent types to make this approach viable. Your simple example is IMHO rather an exception, just having "unsigned int" parameters / return types would mostly not suffice to statically verify that a recursive method will finish or not. (plus things like global state etc.)

A language with your suggested restriction (and a few more) might be possible.

But it's not the only way to get a total language (that always halts), contrary to what your original comment claims.

Agda doesn't need that restriction, as far as I know. And neither does Dhall. See https://dhall-lang.org/

Neither language is Turing complete.

Reply on news.ycombinator.com