Proof by Coinduction

September 18, 2009

Posted by David Corfield

$MathML-enabled post (click for more details).$

The sophisticated take on mathematical induction is that the natural numbers form the inital algebra of the endofunctor on $Set$ , $F: X \to 1 + X$ . As such we have a map $\langle 0, s \rangle: 1 + \mathbb{N} \to \mathbb{N}$ , picking out the zero and the successor function. As an initial object in the category of $F$ -algebras we know that any monomorphism into it must be an isomorphism. So if I have a property, $P$ , of the natural numbers which holds for $0$ , and for which $P(n)$ implies $P(s(n))$ for all $n$ , then the set, $Y$ , of natural numbers satisfying $P$ forms an $F$ -algebra, $\langle 0, s \rangle: 1 + Y \to Y$ , with an obvious monomorphism into $\mathbb{N}$ . Hence $Y$ is isomorphic to $\mathbb{N}$ and $P$ holds for all natural numbers.

Now in the case of coalgebras, coinduction is going to rely on the fact that epimorphisms from terminal coalgebras are isomorphisms, i.e., there’s no quotient coalgebra of a terminal coalgebra. So if I want to establish that two elements of a terminal coalgebra are equal all I need do is find an equivalence relation which relates the elements and which is compatible with the coalgebra structure. Equivalence classes cannot contain more than one element, so I know these two elements are the same.

$MathML-enabled post (click for more details).$

A typical place to use coinduction is with streams. Let $A^{\omega}$ be the set of streams, or infinite sequences, of elements of the set $A$ . There is a map $A^{\omega} \to A \times A^{\omega}$ which takes a stream to the pair of its head (first element) and its tail (the rest). So $A^{\omega}$ is a coalgebra for the functor $G: X \to A \times X$ , and indeed is the terminal $G$ -coalgebra. A relation on $A^{\omega}$ compatible with the coalgebra structure is one for which $\sigma R \tau$ implies that $head(\sigma) = head (\tau)$ and $tail(\sigma) R tail (\tau)$ . To establish the identity of two streams, we define a relation with this property such that the streams relate to each other. We can happily use coinduction then to prove things such as the merger of the list of even positioned elements of a list with the list of odd positioned elements of the same list yields the original list.

But do we ever use coinduction for the terminal coalgebra of $F: X \to 1 + X$ ? This is the extended natural numbers $\mathcal{N} = \mathbb{N} \cup \{\infty\}$ with the predecessor function, which we discussed earlier. To establish whether two extended natural numbers are the same all we need do is find a relation such that either the predecessor is undefined for both numbers or the relation holds of the predecessors of both.

Now Jan Rutten puts coinduction to use to prove commutativity of addition on the conaturals on page 36 of Universal coalgebra: a theory of systems. This relies on the idea that postulating a relation $(n + m) R (m + n)$ is compatible with the coalgebra structure, so they must be equal.

But we might wonder if there isn’t an example like the high school proof of induction of

$\sum_{i = 1}^n i = \frac{1}{2}n(n + 1),$

where you show it true for $n = 0$ , and if true for $n$ then true for $(n + 1)$ .

This was the best I could come up with. Let me define a binary relation which includes pairs $\langle (\sum_{i = 1}^n i) - m, \frac{1}{2} n(n + 1) - m \rangle$ , for all natural numbers $n$ and $m$ such that $n \gt m \geq 0$ . We also throw in $\langle 0, 0 \rangle$ . To do this properly I would define subtraction coinductively, but we can take it that it works as it should.

Then I claim that this relation is compatible with the destructors. If $(n - 1) \gt m$ , then applying the predecessor to each member of a pair yields another pair specified to be in the relation. If $m = (n - 1)$ , we check that

$(\sum_{i = 1}^n i) - (m + 1) = (\sum_{i = 1}^n i) - n = \sum_{i = 1}^{n - 1} i.$

On the other hand,

$\frac{1}{2} n(n + 1) - (m + 1) = \frac{1}{2} n(n + 1) - n = \frac{1}{2} (n - 1)n.$

This pair is specified as being related. I probably need to say something about what happens for $n = 1$ , but how does this strike people as a proof by coinduction? I guess it’s a tad too similar to induction to merit much attention.

Elsewhere in the blogosphere, Sigfpe has struggled with such matters.

Posted at September 18, 2009 4:33 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2061

18 Comments & 0 Trackbacks

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

𝒩=ℕ∩{∞}

Did you mean union?

Posted by: Mike Stay on September 18, 2009 6:07 PM | Permalink | Reply to this

Re: Proof by Coinduction

Fixed. Thanks.

Posted by: David Corfield on September 19, 2009 1:52 PM | Permalink | Reply to this

“Mathematics Made Difficult”; Re: Proof by Coinduction

I just linked to this from my facebook page, with the comment: The Math-challenged might still enjoy this thread in the same sense as the book “Mathematics Made Difficult” by Carl E. Linderholm (1971), which is taken rather differently by the most advanced readers.

A number of my roughly 400 facebook “friends” show great sophistication in their comments on my Math and Science postings.

Posted by: Jonathan Vos Post on September 18, 2009 6:50 PM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

People are going to say that there's no need to prove things about $\bar{N}$ by coinduction, since you just break it into the cases of $N$ and $\infty$ and prove it for $N$ using induction. Perhaps constructivists (who consider that break into cases invalid) would like using coinduction better?

Your example really only seems to be about $N$ ; I don't even know what it's claiming for $\infty$ .

Posted by: Toby Bartels on September 18, 2009 11:07 PM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

There’s nothing to stop us defining $Sum(n)$ as $\sum_{i = 1}^n i$ for $n \neq \infty$ and $Sum(\infty) = \infty$ . Then the identity holds even for $\infty$ . But, yes, $\infty$ does seem somewhat isolated from the rest of the pack.

Is it that extended natural numbers only start to become interesting when they’re topologised, when we can talk about the limit of a converging sequence?

Posted by: David Corfield on September 21, 2009 8:48 AM | Permalink | Reply to this

Re: Proof by Coinduction

What does coinductively defined subtraction look like here? Coinduction is a useful concept in total functional programming languages, as it gets you a lot of the infinite structures that are available in, say, Haskell, but in such a way that the language remains total. Definition of functions via coinduction is often encoded in the language as guarded recursive defintions. However:

  n     - zero  = n
  zero  - suc m = zero
  suc n - suc m = n - m

which is a typical definition for the inductive naturals, is not a system of guarded equations, and is not productive. Subtracting ‘infinity’ from itself results in non-termination. And even trying for a definition in a more categorical style:

  m - n = unfold f (m,n)
   where
   f : (Conat,Conat) -> 1 + (Conat,Conat)
   ...

It’s not obvious to me what f should be, or if there is an appropriate f at all (as it should be non-recursive).

I think to rectify this, you might have to instead take the extended naturals to be the final coalgebra of:

  FX = 1 + X + X

Which allows you to yield a ‘skip’, like so (going back to guarded recursion):

  zero   - n      = zero
  skip m - n      = skip (m - n)
  suc  m - zero   = suc m
  suc  m - skip n = skip (suc m - n)
  suc  m - suc  n = skip (m - n)

And subtracting ‘infinity’ from itself yields an infinite nesting of ‘skip’.

Of course, this formulation is more of a pain to work with, due to equality needing to ignore skips and such.

(Sorry about the low-tech presentation, but I don’t know MathML. Also the above notation for guarded corecursion on coinductive values is perhaps a little misleading when you get into including it in a language, but I think it should suffice for here.)

Posted by: Dan Doel on September 19, 2009 1:47 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

Sorry about the low-tech presentation, but I don’t know MathML.

Neither do most of the posters here. Just put TeX math markup between dollar signs:

$ (math here) $

or, for centered and offset math, between backslash-brackets:

\[ (math here) \].

Posted by: Mike Stay on September 19, 2009 2:31 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

… and choose a Text Filter that includes the phrase “itex to MathML”.

Posted by: Mike Stay on September 19, 2009 2:32 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

I’ll have to think about that. I can see subtraction may be quite awkward which makes me wonder if I might not have avoided it initially.

Why not have in my relation $\langle m + (\sum_{i = 1}^n i), m + 1/2 n(n + 1) \rangle$ , for $0 \leq m \lt n$ . Then the only interesting step to check is:

$pred(0 + (\sum_{i = 1}^n i)) = (\sum_{i = 1}^{pred(n)} i) + n = n + (\sum_{i = 1}^{n -1} i).$

$pred(1/2 n(n + 1)) = 1/2(pred(pred(n(n + 1)))) = ... = n + 1/2 (n - 1)n.$

Posted by: David Corfield on September 21, 2009 9:00 AM | Permalink | Reply to this

Re: Proof by Coinduction

For the record, here is what (very simple) coinduction on the extended naturals looks like formalized in Agda. I take finality of the relevant coalgebra as a postulate (since Agda uses an intensional type theory, it can’t be proved), and use the standard technique to prove that bisimulations demonstrate equality.

I was contemplating showing commutativity of addition, too, but I wasn’t able to successfully download the paper you linked to, and developing a bisimulation for it was proving a little less than trivial (which was my breaking point, since I wanted the code to end up simple). So, that’s left as an exercise for the reader, I suppose. :)

Posted by: Dan Doel on September 22, 2009 6:10 AM | Permalink | Reply to this

Re: Proof by Coinduction

You can get Rutten’s paper also from CiteSeerX.

Posted by: David Corfield on September 22, 2009 8:42 AM | Permalink | Reply to this

Re: Proof by Coinduction

I was researching the FMathL thread when I came across coinduction and Coq, another proof assistant. Perhaps, you will at some point find this interesting; some of the paper was written using Coq.

hal.archives-ouvertes.fr/docs/00/28/95/45/PDF/coindsem.pdf
“Coinductive big-step operational semantics

The Coq proof assistant [3] provides built-in support for coinductive definitions and proofs by a limited form of coinduction called guarded structural coinduction.”

Posted by: Stephen Harris on September 20, 2009 4:51 AM | Permalink | Reply to this

Re: Proof by Coinduction

I am not sure that the following nice example of a terminal coalgebra is appropriate here, but I guess most of the proofs can be wrapped up as coinductions. Consider the category of sets equipped with two distinct basepoints (which a person with foresight might well call “bottom” and “top”, or “0” and “1”) and functions that preserve them. There is an evident bifunctor that sticks two such objects together by identifying the top of one with the bottom of another. We have an endofunctor that takes an object and joins it to itself. The unit interval is a terminal coalgebra for this endofunctor. The standard order relation on it, and hence its topology, are constructible solely from the coalgebra structure, once we decide that bottom is less than top, despite the absence of any order relations or topology in the initial set up. Sorry I cannot remember which of the usual suspects was responsible for pointing this out.

Posted by: Gavin Wraith on September 20, 2009 6:08 PM | Permalink | Reply to this

Re: Proof by Coinduction

Peter Freyd

Posted by: Tom Leinster on September 20, 2009 8:27 PM | Permalink | Reply to this

Re: Proof by Coinduction

A couple of things I’ve been wondering about:

1) Vaughan Pratt in Event Spaces and Their Linear Logic writes of

…the duality of bipointed sets, sets with two distinguished elements, and Boolean algebras without top or bottom. Contemplation of this duality, which Bill Lawvere suggested to me in a phone conversation as a simple construction of the theory of cubical sets…

Does something dual to the reals emerge as an initial algebra in cubical sets?

2) What to make of Peter Freyd’s Algebraic real analysis.

Posted by: David Corfield on September 21, 2009 9:10 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

A small mistake: in the first paragraph, Y→1+Y should be 1+Y→Y. Regards.

Posted by: ym on November 26, 2014 11:13 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

How about a proof by co-induction that $\sqrt{n\sqrt{(n+1)\sqrt{(n+2) \dots}}} \leq n+1$ (and hence converges)?

Assume that the co-inductive hypothesis is true for $k=n+1$ . We have that $\sqrt{n\sqrt{(n+1)\sqrt{(n+2)\dots}}} \leq \sqrt{n(n+2)}$ which then by AM-GM is at most $\frac{n + (n+2)}{2} = n+1$ , which was the result to be proved.

By the way, the form for posting comments appears to be partly broken.

Posted by: jkabrg on November 15, 2019 7:21 AM | Permalink | Reply to this

Re: Proof by Coinduction

$MathML-enabled post (click for more details).$

Never mind the above

Posted by: jkabrg on November 15, 2019 4:20 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

September 18, 2009