Practical non-Turing-complete languages?

Question

Nearly all programming languages used are Turing Complete, and while this affords the language to represent any computable algorithm, it also comes with its own set of problems. Seeing as all the algorithms I write are intended to halt, I would like to be able to represent them in a language that guarantees they will halt.

Regular expressions used for matching strings and finite state machines are used when lexing, but I'm wondering if there's a more general, broadly language that's not Turing complete?

edit: I should clarify, by 'general purpose' I don't necessarily want to be able to write all halting algorithms in the language (I don't think that such a language would exist) but I suspect that there are common threads in halting proofs that can be generalized to produce a language in which all algorithms are guaranteed to halt.

There's also another way to tackle this problem - eliminate the need for theoretically infinite memory. Once you limit the amount of memory the machine is allowed, the number of states the machine is in is finite and countable, and therefore you can determine if the algorithm will halt (by not allowing the machine to move into a state it's been in before).

Answer 1

Any non-Turing-complete language wouldn't be very useful as a general purpose language. You might be able to find something that bills itself as a general purpose language without being Turing-complete but I've never seen one.

Answer 2

The problem is not with the turing machine, it's with "algorithm". The reason why you can't predict if an algorithm will halt or not is because of this:

function confusion()
{
    if( halts( confusion ) )
    {
        while True:
            no-op
    }
    else
        return;
}

any language that can't do recursion or loops wouldn't really be "general-purpose".

Regular expressions and finite-state-machines are the same thing! lexing and string matching are the same thing! The reason FMSs halt is because they never loop; they just pass on the input char-by-char and exit.

EDIT:

For many algorithms, it's obvious whether or not they would halt.

for instance:

function nonhalting()
{
    while 1:
        no-op
}

This function clearly never halts.

and, this function obviously halts:

function simple_halting_function()
{
    return 1;
}

So the bottom line: you CAN guarantee that your algorithm halts, just design it so that it does.

If you are not sure whether the algorithm would halt all the time; then you probably cannot implement it in any language that guarantees "halting".

Answer 3

It turns out that it is fairly easy to be turing complete. For example you only need the 8 instructions ala BrainF**k, and more to the point you really only need one instruction.

The heart of these language is a looping construct, and as soon as you have loops you have an inherent halting problem. When will the loop terminate? Even in a non-Turing complete language which supported loops you would still have the halting problem.

If you want all your programs to terminate, then you just need to write your code carefully. A specific language may be more to your liking and style, but I don't think any language can guarantee absolutely that the resulting program will halt.

Answer 4

BlooP (short for Bounded loop) is an interesting non-Turing-complete language. It's a essentially a Turing-complete language, with one (major) caveat: every loop must contain a bound on the number of iterations. Infinite loops are not allowed. As a result, the Halting Problem can be solved for BlooP programs.

Answer 5

What you're asking for wouldn't be a very good language. You're not really asking for a language though, you're asking for a subset. It reminds me a bit of the whole SafeD concept with the D language. What you're looking for is a subset of a language, which can be attained by simply ignoring features you deem risky

Answer 6

"eliminate the need for theoretically infinite memory." -- well, yeah. Any physical computer is limited by the entropy of the universe and, even before that, by the speed of light (== maximum rate at which information can propagate).

Even easier, in a physically-realizable computer, just monitor resource consumption and put some bound on it. (i.e., when memory or time consumption > MY_LIMIT, kill the process).

If what you're asking is a purely mathematical / theoretical solution, how do you define "general purpose"?

Answer 7

Don't listen to the naysayers. There are very good reasons one might prefer a non-Turing complete language in some contexts, if you want to guarantee termination, or simplify code, for example by removing the possibility of runtime errors. Sometimes, just ignoring things may not be sufficient.

The paper Total Functional Programming argues more or less persuasively that in fact we should almost always prefer such a restricted language because the compiler's guarantees are so much stronger. Being able to prove a program halts can be significant in and of itself, but really this is the product of the much easier reasoning that the simpler languages afford. As one component in a hierarchy of languages of varying capability, the range of utility of non-universal languages is quite broad.

Another system that addresses this layering concept much more fully is Hume. The Hume Report gives a full description of the system and its five layers of progressively more complete, and progressively less safe, languages.

And finally, don't forget Charity. It's a bit abstract, but it is also a very interesting approach to a useful but not universal programming language, which is based very directly on concepts from category theory.

Answer 8

A very similar question was just asked on the programming language theory weblog Lambda the Ultimate. The ensuing discussion is interesting and detailed, but it does go pretty far into the weeds ultimately.

Answer 9

Charity is not Turing complete, still, it is not only theoretically, didactically interesting (category theory), but moreover, it can solve practical problems (Hanoi towers). Its strength is so great that it can express even Ackermann function.