Mongruences

Before saying anything I'd be interested in feedback on whether the mathematical symbols below are visible in your browser. Things like right arrow ⇒, infinity ∞ and union ∪.

Anyway, I've been trying to understand exactly what coindunction is all about. In particular I've been trying to figure out exactly what the duality is between induction and coinduction. The problem I was having was that induction and coinduction seemed not to be dual to each other at all, and weirder still, almost every discussion of coindunction that I looked at seemed to completely ignore the issue.

So here's my problem: in order to carry out an induction argument over the naturals, say, we find a predicate on the naturals, P, such that

P(0) and P(n) ⇒ P(s(n))

We can then conclude that P holds for all naturals.

In order to carry out a coindunction argument over the set of streams over A, say, we find a binary relation R (called a bisimulation) such that

R(a,b) ⇒ head(a)=head(b) and R(tail(a),tail(b)).

I can point out a certain amount of duality: The naturals form an initial F-algebra which is a fancy way of saying that they form a least fixed point to some equation, in this case N≅1+N. Here '1' means the type with one element called '*' and '+' is the disjoint union. We have a map s:1+N→N where s(*) = 0 and s(n) = n+1. s can
be thought of as a 'constructor'. Given something of type 1+N it shows how to construct an object of type N from it. Loosely speaking we can now see that induction is about forming a predicate that still holds after we apply a constructor.

Now consider the coinduction over all streams. A stream is a final F-coalgebra which is a fancy way of saying it's a greatest fixed point of the equation S≅A×S. We have a map (head,tail):S→A×S which maps a stream to its head (an element of A) and its tail (another stream). We can think of these as 'destructors' which reduce a stream back down to its component parts. And now we can see that coinduction is essentially about finding a binary predicate that still holds after applying a destructor.

But to my eyes, despite the duality there is a glaring difference: induction is about a unary predicate and coindunction is about a binary predicate. And through no amount of messing about with categories and their opposites was I able to find a way to see a unary predicate to be dual to a binary predicate.

So I gave in and tried to find something on the web about this subject and eventually was led to Bart Jacobs' paper Mongruences and Cofree Coalgebras. Inductive predicates aren't dual to bisimulations at all, rather inductive predicates are dual to what Jacobs calls mongruences. Unsurprisingly, this horrible neologism was dropped in favour of the term τ-invariant or just invariant in later papers. But I'm going to use the term out of sheer perversity.

But this paper still doesn't explicitly talk about coinduction over the naturals leaving me to work out the details. After chasing round the diagrams, including a nice demonstration of left and right adjoint functors (about which I seem to have managed to develop a crude intuition, who said you can't teach an old dog new tricks?) I managed to figure out what I think is the fairly simple definition of a congruence predicate for the naturals.

So instead of working over the naturals we actually work over N'=N∪{∞}, the set of 'conaturals'. The reason is that we are now looking at the final F-coalgebra that is the greatest fixed point to the equation X≅X+1, not the least fixed point. N' is equipped with a map p:N'→1+N' where p(0)=*, p(∞)=&infin and p(n)=n-1 otherwise. With this in mind a coinductive predicate for the conaturals (ie. a mongruence or invariant) turns out to be a P such that

P(n) ⇒ n=0 or n=∞ or P(n-1).

At least I think so. (This could be embarassing.) And now I can see why coinduction talks about bisimulations - mongruences aren't very interesting for the conaturals. Bit of a letdown really!

On the other hand there are some mongruences that are of mild interest in a more general setting. For example consider a finite state automaton with some terminal states. You can define a state to be safe if at no future point it's possible to reach the terminal state. So a state is safe if it isn't terminal and if all of its successor states are safe. If you think of a finite state automaton as a function f:X→(X×O)^I, where X is the set of states, I is the set of inputs and O is the set of outputs, then f is a 'destructor' and you can see that this definition fits into the same general pattern for coinductive definitions. So safety is a mongruence.

The obvious next question is: what is the dual of a bisimulation? These are called congruences but I haven't yet worked through the details of what these are.

My next question is this: given an inductive predicate you get to apply "proof by induction". What is the corresponding "proof by coinduction" for the conaturals? I'm not sure there is one. I have a vague sense of what proof by coinduction might look like for a more general mongruence but haven't figured out a non-trivial example yet.

But despite having learned about a concept that was uninteresting, and a proof method that I can't figure out how to apply, I have picked up something useful. The standard notions of proof by induction and proof by coinduction aren't straightforwardly dual to each other. So now I can stop worrying about it and get on with reading Vicious Circles.