2
$\begingroup$

The wikipedia page for the Halting problem mentioned practical solutions to avoiding the halting problem such as avoiding infinite loops. And there is a mention that "by restricting the capabilities of general-purpose (Turing-complete) programming language, it is possible to guarantee the completion of all sub-routines (written under the restriction)".

What seems unclear to me is the underlying computation model of such restricted programming languages.

Say, if we remove -- from a general-purpose (Turing-complete) programming language -- the capability to conduct infinite loops (i.e. making the loop variable to always enumerate a finite list of elements, avoiding circular function recursions, etc), what would be the expressiveness of the resulting programming language or (the capabilities of) the corresponding computation model.

Possibly related questions

Is there an always-halting, limited model of computation accepting $R$ but not $RE$?

$\endgroup$
  • $\begingroup$ Keep in mind that as soon as you no longer have programs that sometimes don't halt, you can no longer program all total computable functions. $\endgroup$ – Raphael May 22 '16 at 18:25
2
$\begingroup$

It is absolutely theoretically justified.

First realize that a loop is just a form of recursion: do the loop body, then either stop or do the loop body again with different variable values.

System F is a lambda calculus (programming language) with no recursion built in, and it is known to be strongly normalization. That is well typed every computation in this system halts. It's also powerful enough to compute basically every function you can think of, including the infamous Ackerman function.

In this system, you can use Church numerals to simulate the finite looping you mention in your question.

If you take a programming language without loops, you can model it in System F, which will give you a guarantee that all programs in this system halt.

It's implicit that if you remove loops, you also remove GOTO, which can be used to build loops.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.