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

Ma

SQL would be my best bet. But no, a general-purpose language that isn't turing complete is pretty impractical. You'd have no way to do loops or recursion. – Admissive

what does the halting problem have to do with this??? – Hermaphrodite

Imagine a language where, by design, all programs halt - I realize that this is largely a theoretical CS exercise, but it does have some practical application as well. – Ma

SQL, (without recursion, dynamic SQL or the general WHILE loop) is guaranteed to halt (and thus, not Turing-complete) but is still pretty darn usable. Of course, technically, it's not general-purpose either. – Faline

If possible, please provide a meaningful definition of "General Purpose". Here is a definition that is probably appropriate to the context, "Can complete decide all problems that are decidable by a universal Turing machine", which of course is a tautology, since the language would now be Turing complete. If you have a weaker definition in mind, please suggest it. – Griskin

OK, I'll admit that "general purpose" is sort of unclear and subjective. However, as developers, we try to have all our programs halt (otherwise they would be of limited use). Given this, would it be possible to write said programs in a language that guaranteed such a property? – Ma

GLSL ? Not sure of the newer versions though, since the C subset for CUDA kernels is probably Turing complete – Bowing

Look into Simply Typed Lambda Calculus – Duong

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

Hutner

I'm glad you like them. If those were interesting, you might also want to take a look at Epigram (e-pig.org and e-pig.org/downloads/ydtm.pdf are good places to start). Though perhaps slightly off topic, there is an interesting discussion in section 3 of the above paper about the value of totality and in being able to indicate in a program which parts are total and which parts are not. The point from the Epigram perspective being that dependent types allow one to do just that. – Hutner

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

Contraband

BlooP is a great example. Also see FlooP (same link), the Turing-complete version with Free (unbounded) loops. – Piranesi

One could argue that "at most x times" disqualifies it as "general purpose." This necessarily injects insight into the problem's outcome into the definition of the problem. – Equilibrist

Assuming of course that they do not have either unbound recursion or the ability to Dynamically self-evaluate/execute, both are unbounded-iteration backdoors. – Faline

BlooP's ability is useless. for(bounded 2^32 - 1) for (bounded 2^32 - 1) stepwise-evaluate plausible-infinite-loop is infinite in practice. – Confessor

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

Kazmirci

A language without recursion or looping wouldn't be very useful (for most purposes), but a language with only guarded recursion can be total and still useful for many purposes. – Mosul

all languages which always halt and cannot express an infinite are not turing-equivalent (or is it -complete?). But there are languages such are Charity which can express general recursion (not just its proper subset Primitive Recursion) which are also not turing complete. – Emplace

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

Tetryl

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

Interrupt

"Even in a non-Turing complete language which supported loops you would still have the halting problem." If the Church--Turing thesis holds, you are wrong. – Mortenson

@Rhymoid Can you elaborate? – Interrupt

The halting problem is effectively decidable for models of computation X that are strictly weaker than Turing machines (that is, Turing machines can simulate all instances of X, but X can't simulate all Turing machines). After all, such models can be simulated by Deciders, for which the halting problem is decidable (Deciders always halt). What does the CTT have to do with this? It can be interpreted as "Turing-completeness is the most powerful", so if it holds, non-T-c things are always weaker, and therefore their HP is decidable. – Mortenson

By the way, there are many languages that guarantee termination. The most appropriate one here is LOOP (Meyer & Ritchie, 1967; also described by Hofstadter in 'Gödel, Escher, Bach'), which is based on loops... but they're always bounded. Therefore, all LOOP programs will eventually halt, thus their halting problem is decidable. Also, as mentioned in other answers, dependently-typed programming languages often restrict you to writing total functions, which must terminate by definition. – Mortenson

Changed may answer to clarify that it is unbounded loops which give you a halting problem. – Interrupt

Which is also false. Finite state automata are allowed to have unbounded loops (e.g. they can recognize a*), but are definitely not Turing-complete. The halting problem for finite state automata is decidable. – Mortenson

@Rhymoid Further clarified, in theory you can decide if the program will halt, but in practice it may take so long to halt that the universe will fall into heat death first, which is probably not what the OP wanted. Thanks for keeping me honest. :) – Interrupt

@Rhymoid actually they are bounded by the length of the input (always finite for DFA's and NFA's) – Preliminaries

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

Equilibrist

In practice that's a good solution, though it's possible you will abort instances which eventually will terminate. That's the issue with the halting problem: one will never know whether the program just takes awfully long or won't terminate at all. – Preliminaries

With a good proof that a program halts though you can get a good guess of how long the program is going to take and how much memory it will use (its complexity) – Preliminaries

"General-purpose" though most of the time means a language suited to implement most computer software, from "hello world" to ego-shooter to text processors. – Preliminaries

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

Marr

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

Rhadamanthus