Can a total programming language be Turing-complete?

Question

I've seen two answers to this:

Wikipedia says no:

These restrictions mean that total functional programming is not Turing-complete.

And the Wikipedia article cites D.A. Turner as the coiner of "total functional programming," and Turner says on page 755 of Total Functional Programming:

There are two obvious disadvantages of total functional programming

1. Our programming language is no longer Turing complete
2. If all programs terminate, how do we write an operating system?

But Conor McBride says total programming languages can be Turing-complete:

Now represent the semantics of Turing machines as coinductive processes and review your hasty and inaccurate repetition of the common falsehood that totality prevents Turing-completeness. You exactly get to say “we know how to run it for as long as we’re willing to wait, but we can’t promise you it will stop”, which is both the truth, and exactly the deal when you work in a partial language. The only difference is that when you promise something does work, you’re believable. The expressive weakness is on the partial side.

Turner had indeed thought about codata, and it plays a big role in their article re problem (2), but they don't seem to think codata helps with (1).

Would an answer to McBride's Retort be something like:

Re "Now represent the semantics of Turing machines as coinductive processes ..." A Universal Turing Machine won't halt (if executing a program with an infinite loop), but a copgram will always halt until someone asks it to compute some more: to actually do computation for infinite time rather than just representing an infinite computation requires non-termination.

Answer 1

I'm pretty sure McBride isn't claiming that a total programming language can be Turing complete, just that it's a useless distinction in practice. You can take any program in a partial language and replace all not-provably-terminating loops with loops that run at most $2^{128}$ times, and the result is theoretically different but not observably different.

You exactly get to say “we know how to run it for as long as we’re willing to wait, but we can’t promise you it will stop”, which is [...] exactly the deal when you work in a partial language.

I.e. maximum run times are bounded in the real world.

The only difference is that when you promise something does work, you’re believable. The expressive weakness is on the partial side.

I.e. there's an expressivity tradeoff in using total vs partial languages, but the expressive advantage of total languages is useful in practice, while the theoretical expressive advantage of partial languages has no practical consequence.

---

Edit: In response to OP's comment, I think ruakh's comment is correct. McBride is implicitly suggesting that a better notion of completeness ought to not only replace Turing completeness as the de facto standard for real-world languages, but also take the name of Turing completeness and the brand identity associated with it, because it's more deserving of it. Maybe it would be more accurate to say he thinks the better notion of completeness ought to have been called Turing completeness from the beginning. It matters because the perception that total languages are deficient in some practical way, due to their lack of Turing completeness, may have actually hindered their real-world adoption.

Answer 2

A rhetorical question to keep in mind: would anyone take you seriously if you said ZFC is "not Turing complete" and therefore insufficient to express the algorithms that we write in mainstream programming languages?

First, what is the usual argument about total languages? The reasoning is as follows:

1. In a total language, the function type $A → B$ classifies only¹ the functions that are somehow able to be verified total.
2. Any feasible verifier is going to reject some actual total definitions.
3. Therefore, $A → B$ does not contain all Turing-computable, total functions from $A$ to $B$.

This reasoning is correct. However, what is not correct is the further assumption that to write a program accepts an $A$ and produces a $B$, it must be recognized by the system as a (total) function $A → B$. Certainly the total part is not the case in mainstream programming languages, because there $A → B$ means some class of partial functions from $A$ to $B$.

So, are total languages incapable of representing partial functions? No. There are potentially many ways to do it. One of the fancier ways is to define the free ω-complete partial order $A_⊥$ over a type $A$. Then the total functions $A → B_⊥$ act much like the partial functions from $A$ to $B$ from current (eagerly evaluated) programming languages.

From a practical perspective, this $A_⊥$ is not really very different from the previous coinductive definitions of a 'partiality monad.' The actual differences I can think of are:

1. The quotient inductive-inductive type (QIIT) would be a lot slower in certain scenarios, because it is based around representing successive approximations as $ℕ → A_⊥$ (note the similarity to emulating a partial recursive function using "fuel"). With the coinductive type, if you observe a value and get $\mathsf{later}\ x$, then $x$ is a value that represents something closer to the answer. The analogue of this with the QIIT is trying $f\ 0$ and getting $⊥$, so you need to try $f\ 1$, but there is no work shared between $f\ 0$ and $f\ 1$, it just restarts from the beginning.

2. The quotienting ensures that people can't quibble about the type "not really" representing partial functions, but something else. I think this might be the reason that people reject the coinductive version. You can observe how long its taking, and stop running at some point, so it's "not really" modelling partial functions, and therefore "not really" Turing complete. This is the reason why it has its advantages in #1, though.

So, even total languages without the features needed to faithfully represent the more 'topological' aspects of partial recursive functions have at least one way of representing practical aspects of them. If your 'main program' is allowed to be a total function of type $A → B_⊥$, with the proviso that it will (somehow) just be executed similarly to a partial function in a normal programming language, then there essentially aren't any $A$-to-$B$ programs that we genuinely can't express in this total language.

What does our argument above actually show in this light? That there are partial functions, i.e. total functions $f_⊥ : A → B_⊥$ that 'actually' converge to a well-defined value on every input, but we cannot exhibit corresponding total functions $f : A → B$, and prove that $f_⊥\ x$ converges to $f\ x$. But, this is also true of, say, ZFC (hence the earlier rhetorical question), the mathematical system often considered to underlie all our mathematical reasoning, including about programming. Some of the details differ a bit,² but the discrepancy still exists.

And what is the limitation of not being able to recognize some actually total functions as such? It is good to be able to show that large parts of our program are (more) genuine total functions. But, if that is impossible or infeasible, we are not worse off by only recognizing them as an encoding of partial functions, so long as we are still allowed to execute partial functions as programs. As McBride says, we are actually more honest in distinguishing recognizably total functions from partial functions, which most languages don't do. Another major use for total function is that they make sense to use in dependently typed languages for calculations that happen (and must terminate) during type checking, and we can't just use partial functions for those purposes. But most 'Turing complete' languages also don't let you do this. Many don't have anything like this period, and at best you usually get a stilted total language to program in at the type level, rather than one that has comparable convenience to the value level.

There are engineering questions to be considered. For instance, neither the QIIT nor the codata solution seem like the ideal encoding from a performance perspective. It's possible (something like) the QIIT is actually not as bad as I made it seem, if the runtime executor can somehow pass it a fake value that makes a 'limit' actually run with infinite "fuel," and never have to restart from scratch. That'd take care, though, and probably still have overhead. These are questions about efficiency of the representation of partial functions, though, not whether or not they can be represented.

---

1: For the purposes of this answer, where a programmer would care what functions they are able to write syntactically and get accepted by the language. The fact that there are mathematical models of the total language where the semantics of $A → B$ includes things that are not the image of any syntax doesn't help them write the missing programs as total functions.

2: E.G. you might be able to define non-computable ZFC functions that 'actually' correspond to converging partial recursive functions, but not prove that the partial recursive function converges to the values of the non-computable function. Whereas in a total programming languages, the functions are all expected to be computable, so you'd be stopped at the step of defining the corresponding function, rather than the proof that the function is computable.

Answer 3

I'm inclined to disagree with McBride here, for the simple reason that while you can express program semantics totally via coinduction, it is not enough to solve the halting problem for the object language (because you would need to run the coinductive trace to exhaustion, which of course may be infinite).

---

I think he has an important point, though: In functional programming, we often conflate divergence of a program with the mathematical meaning of partiality of a function.

Consider an evaluation function of an operational semantics eval : term -> value, returning the value whenever the expression halts. eval is a partial function, undefined on inputs that diverge, because then it diverges itself and never produces a value.

In some sense, divergence in the object language is lumped into partiality of the meta language.

That is a problem in mathematics, because you can never say "give me the value v of e", because that value does not always exist. If you prove theorems about v, you better be sure that the v in question actually exists. So now you have got to figure out what the domain of eval is. At best, eval is written in a way that it loops only when the inputs e diverge! And now you need two artefacts: eval as well as the "ground truth" semantics that tells you when e diverges; that's exactly when v := eval e is undefined. Well, hopefully. That's what you have to prove about eval.

Note that the halting problem doesn't have anything to do with it since we are determining divergence of an object program in the meta language, math.

Traditional denotational semantics solves this problem by returning a distinct element ⊥ when e diverges. The main point is that this yields a total function! Alas, the clever use of topology means that the naive translation into a program (denotational semantics look like definitional interpreters, after all!) simply loops on diverging inputs. Nevertheless, it is a mathematically sound and thus total definition.

I think the confusion of divergence and partiality presumably stems from the fact that traditionally, ⊥ is a partial element in the underlying approximation order, which means there are (many) other elements d that are strictly larger than ⊥, while for converging e what you get back is a total element, i.e., one that does not have a d that is strictly larger. At some point, we seem to have identified "eval e returns a partial element in some approximation order in the meta language" with "eval is a partial function, and undefined for e", with "e diverges".

---

But since at least a decade, Xavier Leroy (perhaps among others? Not exactly my area of expertise, I'm afraid) popularised a coinductive definition of the operational semantics. I find these slides quite approachable. He defines Capretta's coinductive delay monad

and then he asks

Yes, we can, as he shows us, by only doing small, incremental steps before each now or later constructor (productivity). That is quite like a trace produced by a small-step operational semantics; indeed the type of potentially infinite traces can be regarded as a concretisation/elaboration of the delay type. A diverging program would simply produce an infinite sequence of later (later ( ... )), a well-defined mathematical object.

Now that we have at our hands a function definition of a Turing-complete programming language's semantics that is totally defined as a mathematical function, we can reason about it in proofs and theorem provers such as Coq.

All this does not imply that there is a total (in the unfortunate sense that it diverges nowhere) function program halts : term -> bool that we can define in terms of eval; for that we'd need some worker function that keeps on eating later constructors from the result of eval until it finds a now; and that might take an infinite amount of time (when a now never happens). Of course, such a definition will not yield a total definition either, because it will not be guarded recursive in the delay (option term), so you wouldn't be able to define halts in the total fragment of Coq.