Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 28, 2009

Metric Coinduction

Posted by David Corfield

Dexter Kozen and Nicholas Ruozzi have a paper Applications of Metric Coinduction which begins

Mathematical induction is firmly entrenched as a fundamental and ubiquitous proof principle for proving properties of inductively defined objects. Mathematics and computer science abound with such objects, and mathematical induction is certainly one of the most important tools, if not the most important, at our disposal.

Perhaps less well entrenched is the notion of coinduction. Despite recent interest, coinduction is still not fully established in our collective mathematical consciousness. A contributing factor is that coinduction is often presented in a relatively restricted form. Coinduction is often considered synonymous with bisimulation and is used to establish equality or other relations on infinite data objects such as streams or recursive types.

In reality, coinduction is far more general. For example, it has been recently been observed that coinductive reasoning can be used to avoid complicated ϵδ\epsilon-\delta arguments involving the limiting behavior of a stochastic process, replacing them with simpler algebraic arguments that establish a coinduction hypothesis as an invariant of the process, then automatically deriving the property in the limit by application of a coinduction principle. The notion of bisimulation is a special case of this: establishing that a certain relation is a bisimulation is tantamount to showing that a certain coinduction hypothesis is an invariant of some process.

The paper involves a series of applications of the ‘coinductive rule’ for complete metric spaces. Let (V,d)(V, d) be a complete metric space, and H:VVH: V \to V a contractive function, i.e., there exists 0c<10 \leq c \lt 1 such that for all u,vVu, v \in V,

d(H(u),H(v))cd(u,v). d(H(u), H(v)) \leq c \cdot d(u, v).

Any such map has a unique fixed point, u *u^{*} in VV.

The authors then consider the category CC whose objects are nonempty closed subsets of VV and whose arrows are the reverse set inclusions. If we now define H¯(A)\bar{H}(A) as the closure of H(A)H(A), for AVA \subseteq V, then H¯\bar{H} is an endofunctor on CC. The terminal coalgebra for H¯\bar{H} is {u *}\{u^{*}\}, the singleton set of the fixed point.

Any nonempty closed subset, AA, of VV which contains its own image under HH is a coalgebra for H¯\bar{H}. The finality of the coalgebra {u *}\{u^{*}\} expresses itself then in the coinductive rule, that AA as above must contain u *u^{*}.

A couple of things I’m wondering now. Whether I’ve quite grasped the distinction between coinduction and corecursion. From what I wrote there, this might seem better described as a ‘corecursive rule for complete metric spaces’. Please modify those nnLab entries as necessary.

And second, relating to my current interest in ‘symmetry breaking’ in mathematics, couldn’t Kozen and Ruozzi have defined their category CC to be nonempty closed subsets of VV with inclusions as morphisms? Then {u *}\{u^{*}\} would have been the initial algebra of H¯\bar{H}, and all would go through as before, producing an ‘inductive rule for complete metric spaces’.

Surely the only way coinduction starts to look different from induction is when you have good reason to fix a non-self-dual category as the setting. So working in SetSet, algebras are about constructing sets from specific terms and constructors, whereas coalgebras are about unfolding the behaviour of a system. But this depends on certain features of SetSet.

Posted at May 28, 2009 9:34 AM UTC

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

9 Comments & 0 Trackbacks

Re: Metric Coinduction

I’m wondering now[ w]hether I’ve quite grasped the distinction between coinduction and corecursion.

I'd say yes. But I'd also warn anybody that the distinction between ‘induction’ and ‘recursion’ (and their duals) is not always observed in the literature.

There are actually three levels here. We produces proofs by (co)induction; that is, we define (which amounts to establishing the existence of, since they are necessarily unique) elements of a truth value. By (co)recursion, we define elements of a set, most fundamentally elements of a hom-set into a final coalgebra or out of an initial algebra. And then we can also define (co)inductive types, which are objects of a category.

Many people say ‘induction’ for all 33 levels. Many people say ‘induction’, ‘recursion’, and then ‘induction’ again, while many people say ‘induction’, ‘recursion’, and then ‘recursion’ again. I'm inclined to say (which I just thought of, but now it looks obvious) to say ‘induction’, ‘recursion’, and ‘22-recursion’.

For example, give the polynomial XX+1X \mapsto X + 1, we rely on abstract nonsense to assure us that the category of sets has an initial algebra for this endofunctor; in this way, we 22-recursively define the set N\mathbf{N} of natural numbers. Then when we run across some algebra AA for this endofunctor, such as a metric space equipped with a point (the theorem that you cite doesn't hold for the empty space) and a contractive endomap, we recursively define an algebra homomorphism rr from N\mathbf{N} to AA. Then when we run across some algebra homomorphism ff from N\mathbf{N} to AA, we inductively (or 00-recursively) conclude that ff equals rr.

Posted by: Toby Bartels on May 28, 2009 5:36 PM | Permalink | Reply to this

Re: Metric Coinduction

Very nice, and worth writing up at nLab.

Posted by: David Corfield on May 29, 2009 2:05 PM | Permalink | Reply to this

Re: Metric Coinduction

Very nice, and worth writing up at nLab.

Thanks, and I will write it up after giving people a bit of time to object to the term ‘recursion’. I'm also in the middle of writing an article (two, really) on inductive types, although I got a bit sidetracked, so maybe I should just put up what I have ….

Posted by: Toby Bartels on May 30, 2009 8:24 AM | Permalink | Reply to this

Re: Metric Coinduction

object to the term ‘recursion’

Sorry, ‘22-recursion’.

Posted by: Toby Bartels on May 30, 2009 8:27 AM | Permalink | Reply to this

Re: Metric Coinduction

A couple of things I’m wondering now. Whether I’ve quite grasped the distinction between coinduction and corecursion. From what I wrote there, this might seem better described as a ‘corecursive rule for complete metric spaces’. Please modify those nLab entries as necessary.

What you wrote in the nLab entry sure looks right to me. My only comment there is that you’ve generalized the quaternity “induction: coinduction :: recursion: corecursion” beyond the strictures of their usual meanings. For example, ordinary induction says that an FF-subalgebra of the initial FF-algebra \mathbb{N} is \mathbb{N} itself, where F:SetSetF: Set \to Set takes SS to 1+S1 + S. But the same principle applies to an initial algebra of any endofunctor FF on any category, and this is a generalized meaning of ‘the induction principle’. And dually for ‘coinduction’, just in the way you’ve written it.

That said, it also seems okay to me for the authors to refer to the argument as an instance of coinduction. If the argument is that every coalgebra contains this fixed point uu, then the terminal coalgebra TT, constructed very softly as the join

T= SH¯(S)ST = \bigvee_{\emptyset \neq S \leq \overline{H}(S)} S

in the power set P(X)P(X) under reverse inclusion, is nonempty, because it contains uu. In other words, T{u}T \leq \{u\}, so uu is a coalgebra quotient of TT (with respect to \leq), hence must be equal to TT by the coinduction principle as you’ve written it.

And second, relating to my current interest in ‘symmetry breaking’ in mathematics, couldn’t Kozen and Ruozzi have defined their category CC to be nonempty closed subsets of VV with inclusions as morphisms? Then {u *}\{u^*\} would have been the initial algebra of H¯\overline{H}, and all would go through as before, producing an ‘inductive rule for complete metric spaces’.

Absolutely. In fact, this statement is the precise formal dual of what they have! (And maybe easier to grasp this way.)

Posted by: Todd Trimble on May 28, 2009 5:59 PM | Permalink | Reply to this

Re: Metric Coinduction

Thanks!

Absolutely. In fact, this statement is the precise formal dual of what they have!

Not a great example then to make their case for correcting the current situation where

…coinduction is still not fully established in our collective mathematical consciousness.

Posted by: David Corfield on May 29, 2009 2:03 PM | Permalink | Reply to this

Re: Metric Coinduction

David wrote:

Not a great example then to make their case for correcting the current situation…

Maybe not. As you note, we need a category that’s noticeably different from its opposite category to make induction feel noticeably different from coinduction. SetSet is noticeably different from Set opSet^{op}. Here’s we’ve got a poset of closed subsets of a topological space. Is this category noticeably different from its opposite?

Well, yeah, but mainly in this way: an arbitrary intersection of closed subsets is a closed subset, but not an arbitrary union. So, this category has arbitrary colimits but not arbitrary limits — or the other way around, depending on your convention for interpreting inclusions as morphisms.

This difference may or may not seem sufficiently ‘noticeable’ to you. If you feel that all posets are alike and the opposite of a poset is just another poset, it probably won’t. But it’s worth noting that this asymmetry between infinite intersections and infinite unions is what gives topology its characteristic flavor.

You really need to do both induction and coinduction in one of these posets to get a feeling for how they’re different. By trading this poset for its opposite, we can always switch which process is called ‘induction’ and which is called ‘coinduction’. But the difference between them will remain.

Posted by: John Baez on May 29, 2009 8:51 PM | Permalink | Reply to this

Re: Metric Coinduction

One might note that while the poset of closed sets (under usual inclusion) is obviously closed under intersections and hence an inf-lattice, it also has aribitrary joins or sups: any inf-lattice is also a sup-lattice. (For a sup or l.u.b. is the intersection of all u.b.’s.) In other words, one way in which posets as categories are interesting is that complete posets are also cocomplete, and conversely.

One famous and very easy fixed-point theorem is that given a poset map

F:LLF: L \to L

between sup-lattices, there is an initial algebra = least fixed point pp of FF, given by the formula

p= fxxxp = \bigwedge_{f x \leq x} x

But in exactly the same situation, FF also has a greatest fixed point, because: sup-lattices are inf-lattices! (In fact, the poset of fixed points is also a sup-lattice.) This theorem only strengthens the impression that induction and coinduction aren’t significantly different in this context.

Posted by: Todd Trimble on May 29, 2009 9:33 PM | Permalink | Reply to this

Re: Metric Coinduction

Yeah, the real difference that you can detect categorically is that in the poset of closed subsets, finite unions distribute over arbitrary intersections, but finite intersections do not distribute over arbitrary unions.

Since arbitrary colimits in SetSet are preserved by pullback, but limits are not generally preserved by pushout, one could argue that the category of closed sets and reverse set inclusions (or, equivalently, the category of open sets) is more like SetSet.

I also observe that since they had to exclude the empty set, their category has no terminal object.

Posted by: Mike Shulman on May 30, 2009 2:57 PM | Permalink | Reply to this

Post a New Comment