24
$\begingroup$

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).

$\endgroup$
14
  • $\begingroup$ I have a followup question to this: why is it that coinduction appears to be somehow more general than induction, even though (I assume!) it's not? $\endgroup$
    – Gro-Tsen
    Nov 7, 2021 at 17:44
  • $\begingroup$ "and everybody can talk about terminal coalgebras without knowing about coinduction": I don't get this comment, reasoning by coinduction is usually defined to mean reasoning from the existence and universal properties of some terminal coalgebras. $\endgroup$ Nov 7, 2021 at 19:02
  • $\begingroup$ @AndrásKovács I have in mind using a foundation like "Martin-Löf type theory + the principle of coinduction". That's syntax, we are using the foundation as a formal system to do mathematics. The semantics of coinduction is provided by terminal coalgebras. You are probably confused by the fact that inside the syntactical foundation you can talk about terminal coalgebras. But that's different from using the "principle of coinduction". $\endgroup$
    – user984603
    Nov 7, 2021 at 19:16
  • 3
    $\begingroup$ Hmm... Let's see. One of the simplest statements I can prove by induction to undergraduates is that $1+2+\dots+n=\frac{n(n+1)}{2}$. What is the simplest statement (preferably understandable to a reasonably smart middle school kid) you can prove by co-induction and what is its co-inductive proof? The tutorials in your links are rather hard to read and comprehend even for me because they take a vertical start to the stratosphere as far as the level of abstraction is concerned :-( $\endgroup$
    – fedja
    Nov 15, 2021 at 1:39
  • 1
    $\begingroup$ A couple more relevant n-Category Cafe posts: golem.ph.utexas.edu/category/2009/09/proof_by_coinduction.html, golem.ph.utexas.edu/category/2009/05/metric_coinduction.html. For a spell, I was interested in that asymmetry of status between algebra and coalgebra: golem.ph.utexas.edu/category/2008/12/…. $\endgroup$ Nov 15, 2021 at 7:27

1 Answer 1

18
$\begingroup$

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":

As a total programmer, I am often asked ‘how do I implement a server as a program in your terminating language?’, and I reply that I do not: a server is a coprogram in a language guaranteeing liveness.

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:

  1. 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.

  2. 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.

$\endgroup$
11
  • 1
    $\begingroup$ Great answer. However, reading your finale, I could not refrain from this crazy thought: there is classical mathematics, ie the mathematics from the point of view of God, where structures are God-given, static structures $\endgroup$ Nov 14, 2021 at 19:23
  • 1
    $\begingroup$ Then there is constructive math, where poor humans try to "build structures all the way up", for instance N, via induction schema. Then there is another math, still beyond our horizon, which I would call DESTRUCTIVISM, which starts from the opposite perspective: you begin with a static structure, generally infinite, and then proceed by EROSION, moving down the food chain. This math, of which there are already a few scanty examples, would leverage co-inductive methods... $\endgroup$ Nov 14, 2021 at 19:23
  • 2
    $\begingroup$ @MircoA.Mannucci: you might like ellerman.org/the-existence-information-duality $\endgroup$ Nov 14, 2021 at 20:56
  • $\begingroup$ Just a small technical remark to an otherwise very illuminating answer: a programming language cannot encounter a variable or an axiom, because only closed programs are ever executed (and there are no axioms). That at least is how I understand the PL canon. $\endgroup$ Nov 14, 2021 at 21:01
  • $\begingroup$ @AndrejBauer Is it possible, then, to have a dependently typed programming language? Typechecking dependent types in practice requires normalization under binders, no? $\endgroup$ Nov 15, 2021 at 15:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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