Lambda the Ultimate

Here's a concrete example of an interesting semi-decidable problem: full intuitionistic first-order predicate logic. You can write a theorem prover that will always find the proof of a proposition P, if it is in fact true. However, there's no way to make this complete: there's no way to ensure that the theorem prover will halt if P is not provable. (If it were, then you could solve the Halting problem.)

So a complete theorem prover for FOL has to be written in a Turing-complete language.

One can write an interpeter for an Turing-complete language in a Turing-complete language. You can, obviously, write an interpreter for something less than Turing-complete in a Turing complete langauge.

However, less powerful formalisms are generally incapable of self-interpretation. You cannot create a "universal state machine"--a device which takes as input a "program" (for state machines, a regex or some other means of specifying an arbitrary regular language), followed by input strings to match against that language--using a state machine.

Likewise, you cannot write an intepreter for a primitive-recursive language using a primitive-recursive language; you need full recursion.

This paper may be of interest; it covers the relevant computational theory and its consequences.

despite the fact that there are indeeed practical problems (not just theoretical exercises like computing Ackerman's function) that require full-Turing-completeness...

there are many that do not, and benefit from decideability.

Consider the advice of Sir Tim Berners-Lee, expressed as the Principle of Least Power. Also consider the similar (and excellent) advice by LtU's own Peter Van Roy in Concepts, Techniques, and Models of Computer Programming, although in the context of choosing a declarative vs an imperative programming model/language. PVR advises choosing more declarative models when you can, the less declarative models (which are more expressive, but harder to reason about) when you have to. (If I have misquoted you Peter--I don't have my copy of CTM handy to browse here at work--please correct me).

There's a practical argument as well. It's usually much easier and more natural to express an algorithm using general recursion than primitive recursion or another sub-Turing language that guarantees termination. A trivial example is the factorial function; you can write it using primitive recursion, but the excercise is a lot more intuitive with general recursion.

Most programming in languages guaranteed to terminate reduces to writing programs in a very convoluted way so as to prove that they terminate. Turing-complete languages have no such burden, so you can just write your algorithm directly.

Here's a couple more examples of algorithms that would be annoying to write in a language where all computations provably terminate.

Consider this plausible algorithm to give a uniformly distributed random number <200, given a source of uniformly distributed random bytes:

def random_lt_200():
    while True:
        v = get_random_byte()
        if v < 200: return v

In practice, this will terminate very quickly; but if get_random_byte returns truly random numbers, this may not terminate at all (although it will terminate with probability 1). If get_random_byte() returns pseudo-random numbers with a reasonable generator, then this probably can be proved to terminate with pencil and paper, but the proof may not be simple enough to encode in your language (depending on where the non-Turing-completeness comes from).

As another example, consider the Simplex algorithm for linear programming. This starts with an initial solution, then incrementally improves the solution until it reaches the final, optimal answer. This could be written in a non-Turing-complete language by computing an upper bound on the number of improvement iterations required, and then iterating at most that many times, but this has a couple of problems: 1) this upper bound is not an interesting number, so computing it and maintaining a loop counter is wasted work and clutters the code; and 2) you have to write code to deal with the loop ending without finding a solution, even though this can never happen.

On the other hand, sub-Turing-complete languages are very interesting, and can be useful in their niches. I have a programming language design in my head where the core language is sub-Turing-complete (basically Haskell with only primitive recursion), but Turing completeness is restored with a Nontermination monad that allows general looping.

At least imperative ones.

If your programming language permits unbounded recursion or loops, then its Turing-complete.

Generally, the languages which are not Turing-complete are not things like BlooP (a non-Turing complete, though primitive recursive, language in imperative style developed by Douglas Hofstadter as a pedagogical exercise)--but data-declarative languages which support limited transforms/queries on the data. The query subset of SQL is not Turing complete, but still highly useful.

On a practical level, it's much easier for those of us that are at the subgenius level to actually get our work done. Sure there are DSL's and sub-turing languages that allow us to get things done. And a more comprehensive set of languages are always welcomed for specialty tasks. But there is still a lot of territory that is much easier to travel in Turing complete languages.

To take a practical example - SQL. SQL is a very useful language for getting at the data (warts and all). But it has it's limitations. Either you get around those limitations via stored procs (PL/SQL, T-SQL, etc). Or you dive off into a different programming language. The practical question is whether we could keep the determinism of SQL without having to resort to more powerful languages? And if we designed a non-Turing query language that could do all the things we do in stored procs or Java/C#, is it possible for an average programmer to get work done.

On a different note, modularity is also an important concern - the main thrust of any software engineering. We can not tackle problems as one gigantic equation to be solved. We must be able to build it up from pieces of smaller solutions. So any idea on practicality has to incorporate the idea of the open-closed principle. We must be able to isolate things in the small.

So, I still feel like I am missing something; what are the practical benefits of making a language Turing complete? Or to ask another side of the question: what practical benefits would be lost by not being Turing complete?

I think this is a little bit like asking "What are the practical benefits of having a complete car?" It's easiest to answer if we know which part you're thinking of removing. Each of the decidable systems you mentioned has serious limitations that would make it unsuitable for general computation. You can do alot better (like taking a Turing language and restricting to the portion that can be proved total in ZFC with plenty of inaccessible cardinals), but that will require significant programmer help and/or be unusably slow (edit: to compile).

We can divide computation in two groups: those that are supposed to terminate (i.e. algebraic) and those that may not terminate but must do something useful as they go (i.e. coalgebraic, and this property is called productivity). It's very hard to find examples of programs (that are useful, common and aren't theorem provers) that aren't supposed to either terminate or be productive. The main problem isn't writing programs that terminate or are productive but convincing the compiler that the code we wrote has one of these properties, that's the primary reasons why we use Turing complete languages.

Also as a general rule of thumb we can always convert an undecidable program to a provably terminating one by defining a maximum amount of time before timeout, it can even be arbitrarily high, and the vast majority of useful programs are supposed to do what we want in a finite amount of time. A similar trick can be done for programs that we don't know if are productive. In a sense I prefer languages that lack Turing completeness because they allow me to understand the programs better: if a function provably terminates it's easier to reason about the program that uses it. OTOH I agree with many of the above comments: it's usually painful to write certain algorithms without being able to use general recursion. The usual strategies is relying on well known combinators that are proved, fall back to folds and unfolds when they are insufficient and ask for help if this doesn't work. The quality of a language without Turing completeness can be measured by how much work you can do before asking for help ;)

The point about making life easier actually makes a lot of sense. In a language that lacks Turing completeness, the programmer must do a great deal more work.

Thus it seems that the biggest benefit of Turing complete languages are that better/more abundant abstraction is available; which in turn allows efficient solutions and algorithms.

Of course, there are algorithms that cannot be done in a decidable language, but I feel I was missing the point that in a non-Turing complete language everything must be spelled out to explicitly halt.

However, there is a language Charity which can express the Ackerman function which cannot be done through primitive recursion, yet the language is not Turing complete. I have not used Charity and only looked into briefly as I sometimes get pulled into the world of categories. So now I am wondering, if many of the concerns expressed about primitive recursive languages would be much less a problem in a language like Charity.

That paper is exactly the kind of thing I was hoping to see. A very interesting read.

neelk wrote

Basically, fold captures the principle of one-step structural induction.
However, we often want to recursions that have more complex structure, and
emulating them with folds gets yucky. For example, here are two examples which
are doable but ugly with folds:

Well, these particular examples are actually quite easily doable with
folds.

(* We want both 0 and 1-element lists as base cases here *)
fun concat [] = ""
| concat [x] = x
| concat (x :: xs) = x ^ ", " ^ (concat xs)

With fold (and using OCaml), we write just as easily:

let concat = function
| [] -> ""
| [x] -> x
| (x::xs) -> List.fold_left (fun seed a -> seed ^ ", " ^ a) x xs

# concat [];;
- : string = ""
# concat ["a"];;
- : string = "a"
# concat ["a";"b";"c"];;
- : string = "a, b, c"


The second example:

(* We are using a course-of-values recursion here *)
fun fib 0 = 1
| fib 1 = 1
| fib n + 2 = (fib n) + (fib (n + 1))
(* with folds, you need a higher-order fold to emulate course-of-values *)

actually, no. A simple fold suffices:


let rec foldnat s z n =
if n = 0 then z else s (foldnat s z (n-1));;

# fib 0;;
- : int = 1
# fib 1;;
- : int = 1
# fib 2;;
- : int = 2
# fib 8;;
- : int = 34


Things get more annoying when you want to iterate over two collections at once
naturally.

Not that annoying:

How to zip folds: A library of fold transformers (streams)

Once we know how to get takeWhile and dropWhile via folds, the rest is
quite trivial. Essentially, we need a way to `split a stream', which
is doable for any stream represented as fold -- and even represented
as a monadic fold (where the production of each element may incur a
side effect, and we have to be careful not to repeat the
side-effects).

My "Turing Completeness Considered Harmful" unpublished paper might be related here. I think its much harder to design a simple language that is not expressive but still useful than it is to design a powerful language that can do anything. The benefit, at least in the area that I'm in, is usability: these languages are easier to use even if they put users in a straightjacket.

...an if, cond or branching conditional statement to the language?

If not, what am I missing?