Practical non-Turing-complete languages?

问题:

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).

回答1:

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.

回答2:

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.

回答3:

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 FSMs 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".

回答4:

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.

回答5:

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 unbounded loops you have an inherent halting problem. When will the loop terminate? Even in a non-Turing complete language which supported unbounded loops you might still have the halting problem in practice.

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.

回答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"?

回答7:

The right way to do this, IMHO, is to have a language which is Turing complete, but to provide a system for stating semantics amenable to processing by a proof checker.

Then, assuming you are writing a terminating program deliberately, you have in you mind a good argument as to why it halts, and with this new kind of language you should be able to express that argument, and have it proven.

As an aside in my production compiler I have recursions which I know, for sure, will NOT halt on certain inputs .. I use a nasty hack to stop this: a counter with a "sensible" limit. FYI the actual code is involve in monomorphising polymorphic code, and the infinite expansion occurs when using polymorphic recursion. Haskell catches this, my compiler for Felix doesn't (that's a bug in the compiler I happen not to know how to fix).

Following from my general argument .. I'd sure like to know what kinds of annotations would be good for the stated purpose: I happen to have control of a language and compiler so I could easily add such support if only I knew exactly what to add :) I have seen the addition of an "invariant" and "variant" clause to loops for this purpose, although I don't think the language extended to using that information for proof of termination (rather it checked the invariant and variant at run time if I remember correctly).

Maybe that deserves another question ..

回答8:

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.