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
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
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
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 "
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
and then he asks
Yes, we can, as he shows us, by only doing small, incremental steps before each
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)
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.