In the Coq'Art book the authors mention in passing that any language that can calculate all computable functions must also be able to express diverging computations. Or in other words, there can be no Coq' that is Turing-complete that maintains the guarantee that all computations describable in that language terminate.

How would I go about formalizing this statement? I feel it's a simple corollary to the Halting problem, but I don't know enough about formal semantics of programming languages to express or prove this.


2 Answers 2


Let us take a somewhat simplified view of a programming language as a mapping $C$ (the compiler) from finite strings of characters (source code) to descriptions of Turing machines (machine code). A description of a Turing machine is just a finite string of characters of a certain kind. And since finite strings of characters are computably isomorphic to natural numbers (we can computably encode string as numbers and vice versa), we can pretend that both source code and Turing machines are described by numbers.

Under this view a programming language $C$ is a partial map from natural numbers to natural numbers which accepts a number $n$ (the source code) and either diverges or returns a number $C(n)$ (the "compiled" Turing machine). It makes sense to require that $C$ is a computable map, i.e., that there is in fact a Turing machine that calculates it, otherwise magic is required to understand the programming language.

Note that I can enumerate all possible outputs of $C$. I simply try $C$ on every input in parallel by dovetailing, and whenever any parallel copy gives a result, I enumerate it. Let $f : \mathbb{N} \to \mathbb{N}$ be an enumeration of all outputs of $C$.

Let $\phi_k$ be the partial computable map that is computed by the Turing machine described by the number $k$.

We now come to the crux of the matter. Suppose $f$ enumerated precisely the total computable maps, i.e., $\phi_{f(n)}$ is a total computable map for all $n \in \mathbb{N}$, and for every computable map $g$ there is $n$ such that $g = \phi_{f(n)}$. Consider the computable map $d(n) = 1 + \phi_{f(n)}(n)$. This map is total because $\phi_{f(n)}$ is total for every $n$. There is $j$ such that $\phi_{f(j)} = d$, but then $\phi_{f(j)}(j) = d(j) = 1 + \phi_{f(j)}(j)$, contradiction.

The conclusion is that $f$ cannot possibly enumerate precisely the total computable maps. Therefore it either misses out some total maps, or enumerates some partial ones.


If you restrict to decidable languages, then the decision procedure for the language would solve the Halting problem. If you don't restrict to decidable languages then the language of Turing machines that halt on any input is a counterexample (in classical logic).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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