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.

October 31, 2011

Coalgebra Paper

Posted by David Corfield

That paper I was writing on coalgebra has finally appeared. Thanks again for the help I received back at these posts (I and II).

It’s good to see that defining entities coinductively continues to be a topic of interest, e.g., here, here and here.

Perhaps once the proof assistant Coq’s coinductive types are made more powerful, we’ll see results worth mentioning in a sequel.

Posted at October 31, 2011 10:27 AM UTC

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

14 Comments & 0 Trackbacks

Re: Coalgebra Paper

Is there a way for poor people interested in such things but not affiliated with any universities to read the paper free?

Posted by: D on October 31, 2011 7:40 PM | Permalink | Reply to this

Re: Coalgebra Paper

+1

Posted by: Dan Piponi on November 1, 2011 4:09 AM | Permalink | Reply to this

Re: Coalgebra Paper

They can ask. Which I take it you’ve just done, so a copy will be wending its way to you.

Posted by: David Corfield on November 1, 2011 9:49 AM | Permalink | Reply to this

Re: Coalgebra Paper

I’d appreciate a free copy as well if it’s possible.

Posted by: Balazs on November 1, 2011 1:57 PM | Permalink | Reply to this

Re: Coalgebra Paper

I’m sure you have your reasons, David, but I’m curious to know them: why not put a free copy online?

Posted by: Tom Leinster on November 1, 2011 3:22 PM | Permalink | Reply to this

Re: Coalgebra Paper

It’s a combination of things really. There’s less of a preprint culture in philosophy. Philosophy of science does at least have its archive, but unlike your ArXiv it’s frowned upon to submit improved versions of a paper, or at least it was when last I tried it. Perhaps also in philosophy you expect more to change in an article through the refereeing process, so if there’s a clause in the copyright agreement which only allows you to make available versions written before you submitted it to the journal, you may end up with quite a different version being the one that gets read.

I take it that in mathematics you’re allowed to bring in corrections suggested by journal referees and still submit that as a later version to the ArXiv.

Also, in Humanities here at Kent, staff are not given their own institutional websites that they can write on.

Perhaps we just imagine our discipline moves more slowly. What is important to read is spread out in time, so there’s less of a need to have access to the work of the past few years. We’re still reading Aristotle after all. In fact, my reading group starts looking at his Metaphysics this week.

Posted by: David Corfield on November 2, 2011 9:39 AM | Permalink | Reply to this

Re: Coalgebra Paper

I take it that in mathematics you’re allowed to bring in corrections suggested by journal referees and still submit that as a later version to the ArXiv.

Everyone certainly does this. It’s not entirely clear to me, from reading the standard copyright agreement forms used by major publishing houses, whether their wording technically allows it or not. (The one I’m looking at does explicitly allow bringing in such corrections on a version posted on a personal or institutional web site, and forbids posting to public web sites whose purpose is to collect refereed manuscripts, but the allowability of posting a refereed version to a preprint server is not entirely clear.) However, I have been assured by someone high up at Elsevier that this is okay with them; they “don’t want to interfere with the common practice of many mathematicians and physicists.”

If they didn’t allow it, then I think that would be the last straw for me and I would give up publishing in such journals altogether. Fortunately, the available free journals have been growing recently, at least in mathematics; I don’t know anything about other disciplines. I feel that part of my duty to the mathematics community, present and future (and to the taxpayers who fund my fellowship), is to ensure that my work is easily available to everyone, whether or not they are affiliated with a university that is willing to pay high journal subscription fees. (There are many people who feel that we should all give up publishing in journals run by big publishing houses regardless. I have sympathy with that point of view, but I’m also selfish and want to publish in “prestigious” journals, at least until I have tenure (or have given up all hope of getting it).)

Posted by: Mike Shulman on November 3, 2011 10:53 PM | Permalink | PGP Sig | Reply to this

Re: Coalgebra Paper

An alternative to transferring copyright is “license to publish.” Apparently it gives your publisher a number of exclusive commercial rights while allowing you to retain the actual copyright. Elsevier and other commercial publishers supposedly reluctantly allow such deals. I am yet to determine this experimentally.

Posted by: Eugene Lerman on November 3, 2011 11:20 PM | Permalink | Reply to this

Re: Coalgebra Paper

Elsevier and other commercial publishers supposedly reluctantly allow such deals.

Yes, they do; at least Elsevier does. I generally insist on this for all my single-author papers, as a matter of principle, although I’m reluctant to force my coauthors through the process unless I know that they feel similarly. It’s not clear to me that it has much practical effect, since you still have to give them exclusive publication rights, but it makes me happier to keep the copyright in things that, after all, I’ve written.

Posted by: Mike Shulman on November 4, 2011 1:37 AM | Permalink | Reply to this

Re: Coalgebra Paper

Also, in Humanities here at Kent, staff are not given their own institutional websites that they can write on.

I see, and I’m shocked: I thought this was a given for all academics.

Posted by: Tom Leinster on November 4, 2011 2:57 PM | Permalink | Reply to this

Re: Coalgebra Paper

I love this line:

“A general rule is that no thingie will be the same ‘size’ as the collection of its subthingies.”

Posted by: David Roberts on November 1, 2011 12:44 AM | Permalink | Reply to this

Re: Coalgebra Paper

Technically, that should be its thingie of subthingies.

Posted by: John Baez on November 1, 2011 8:26 AM | Permalink | Reply to this

Re: Coalgebra Paper

I don’t think that Coq in its present form can support a useful equality (ie, bisimilarity) on its coinductive types, for the same reason that it cannot support extensional equality for functions.

But that suggests a question: the univalence axiom implies function extensionality. Can it also be used to show that bisimilarity implies equality?

Posted by: Neel Krishnaswami on November 1, 2011 9:58 AM | Permalink | Reply to this

Re: Coalgebra Paper

Neel: my off-the-cuff guess is that the answer is more likely to be “yes” than “no”. The reasoning is: once you have function extensionality, I believe that you can encode any coinductive using functions. E.g. instead of Stream A defined with head and tail, you define it as Nat -> A. I don’t know exactly how this goes in general, but I think I’ve heard other people in the dependent types community say that you can do it. My mental model for it is to use the representation of a negative type in terms of functions from its destructor patterns, a la Zeilberger. Then, since you have the “right” equality for functions, you might be able to derive the “right” equality for coinductives via this translation. E.g. bisimilarity means two streams agree on all heads and tails, which is what function extensionality equality for Nat -> A tells you. Of course, there’s still the question of whether you can get off the ground and show that the functional encoding matches the definition, without already knowing that bisimilarity works, if you’re not willing to take the functional representation as the definition. This might be where things get stuck. Anyway, I agree that someone should work this all out!

Posted by: Dan Licata on November 2, 2011 3:28 AM | Permalink | Reply to this

Post a New Comment