In computability theory, a decider is a Turing machine that halts for every input.
Because it always halts, such a machine is able to decide whether a given string is a member of a formal language.
Given an arbitrary Turing machine, determining whether it is a decider is an undecidable problem.
As a trivial example, a machine implementing a finitary decision tree will always halt.
It is not required that the machine be entirely free of looping capabilities, however, to guarantee halting.
An example of such a machine is provided by the toy programming language PL-{GOTO} of Brainerd and Landweber (1974).
We can further define a programming language in which we can ensure that even more sophisticated functions always halt.
For example, the Ackermann function, which is not primitive recursive, nevertheless is a total computable function computable by a term rewriting system with a reduction ordering on its arguments (Ohlebusch, 2002, pp. 67).
This is because existence of such a programming language would be a contradiction to the non-semi-decidability of the problem whether a Turing machine halts on every input.
This fact is closely related to the algorithmic unsolvability of the halting problem.
The decision problem of whether the Turing machine with index e will halt on every input is not decidable.
One may be interested not only in whether a Turing machine is total, but also in whether this can be proven in a certain logical system, such as first order Peano arithmetic.
In a sound proof system, every provably total Turing machine is indeed total, but the converse is not true: informally, for every first-order proof system that is strong enough (including Peano arithmetic), there are Turing machines which are assumed to be total, but cannot be proven as such, unless the system is inconsistent (in which case one can prove anything).
One can also create a Turing machine that will halt if and only if the proof system is inconsistent, and is thus non-total for a consistent system but cannot be proven such: This is a Turing machine that, regardless of input, enumerates all proofs and halts on a contradiction.
A Turing machine that goes through Goodstein sequences and halts at zero is total but cannot be proven as such in Peano arithmetic.