Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive definitions (of sets, i.e., types if you will), such as the inductively defined set of first-order formulas for a given signature, and that one can do structural induction on these inductively defined sets. (Functional programmers call these inductively defined sets algebraic data types.) Similarly, one can define functions from these inductively defined sets by structural recursion.
I recently picked up that all these inductive and recursion principles can be dualized: there are coinductive data types and there's coinduction and corecursion.
It seems to me these concepts are only known to niche computer scientists and type theorists and almost no "normal" mathematician uses them.
Question: Is this because coinduction, while formally being dual to induction, is less fundamental and less important?
Are there any opportunities we miss because of hiding coinduction? For instance, are there topics in the undergraduate or graduate curriculum that could be simplified by telling students about coinduction?
I found a blog post arguing that coinduction might clarify some concepts in the study of $\infty$-categories, but my question is a bit broader: is coinduction fundamental enough that every pure mathematician should know about it?
En passant: One example the above blog post gives is the definition of $\omega$-categories as follows:
An $\omega$-category is a category enriched over $\omega$-categories.
It is then explained that this can be considered as the definition of $\omega$-categories as the terminal coalgebra for an endofunctor of some category. But I'd complain that even if the foundation one is using admits coinductive data types, in this case one needs to construct this terminal coalgebra by hand, because this endofunctor isn't an endofunctor on "types", but on "categories one can enrich over", for which the "principle of definitions of coinductive data types" doesn't apply. So I'm not sure if coinduction is really useful here (and everybody can talk about terminal coalgebras without knowing about coinduction).
Best Answer
This is a question that I've puzzled about myself, and I don't pretend to have The Answer. But here's one thought that I've found illuminating. Let's start by comparing the behavior of induction and coinduction in a programming language that has them both.
Inductive datatypes are static. They store information in a particular configuration, with constructors that put that information together and destructors that inspect that information recursively. The constructors of an inductive datatype compute immediately to a value, unless they get stuck on an axiom or a variable; this is the content of "canonicity" results for type theory.
By contrast, coinductive codatatypes are dynamic. According to the modern "copattern matching" perspective on computation with codata, the constructor of a codatatype doesn't compute until a destructor is applied to it, in which case it computes only one step to expose the result and another instance of the constructor. Thus, an inhabitant of a codatatype is like an "object" in the OOP sense, which maintains an internal state (the domain of an application of the corecursor) and can be sent messages (the destructors) that return results and alter the internal state. More precisely, the return values can include versions of the object with altered state, so this is "immutable OOP".
I was first clued into this viewpoint by a remark in Conor McBride’s "Let’s see how things unfold":
I found this remark rather cryptic at first, but recently I’ve come to appreciate it much more. In particular, I prefer this perspective on codata to its common description as "infinite objects". The infinite object underlying an element of a codatatype is essentially the trace of all possible execution paths of all possible method calls that might be applied to it in all possible sequences. This can be helpful to have in mind (particularly when constructing categorical semantics), but it has little to do with how we actually use codata. On the one hand, the "infinite object" description is static and fails to correctly describe the dynamic behavior of codata; while on the other hand, if what we actually care about is an infinite object, there are much more flexible and direct ways to represent them.
The simplest kind of codata is of course a stream, which corresponds to an "infinite list". But another way to represent an infinite list is with a function $\mathbb{N} \to A$. From the "static" perspective of "representing an infinite list" the two are equivalent, and the latter can even be preferable because it is more flexible in what we can do with it, and that style can represent more different kinds of infinite objects. But from a dynamic perspective, if we view a stream as a program that computes one result every time it is queried and moving into a new state suitable for computing the next result, then the representation as $\mathbb{N} \to A$ is terribly inefficient: every time we ask for the $n$th result, the program has to start from 0 and compute all the previous results on its way to the $n$th one, even if all those results were already computed. Can you imagine if the only way a web server could respond to a single request is by being passed, every time, the entire sequence of all the requests it had received up until that point, and replaying from square one all the calculations and updates it had to do in response to them?
Why, then, does coinduction get short shrift? From this perspective I would suggest that:
In programming, coinduction is implicitly present everywhere, particularly in object-oriented programming. But the prevalence of imperative programming languages and mutable state, which achieve essentially the same effect in an "easier" way (but without a conceptual framework and in a way that's hard to reason formally about), means that it is rarely explicitly recognized.
In mathematics, coinduction makes occasional appearances, but it is just not as useful, because mathematics (at least as it's generally done nowadays) is basically static. Apart from some constructivists and type theorists trying to change the world, mathematicians don't really care about computational interpretations of what they write; so it's natural to prefer the more flexible static representations of infinite objects over the coinductive versions that are more tailored to their computational behavior.