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 UTCTrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2452
+1
They can ask. Which I take it you’ve just done, so a copy will be wending its way to you.
I’d appreciate a free copy as well if it’s possible.
I’m sure you have your reasons, David, but I’m curious to know them: why not put a free copy online?
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.
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).)
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.
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.
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.
I love this line:
“A general rule is that no thingie will be the same ‘size’ as the collection of its subthingies.”
Technically, that should be its thingie of subthingies.
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?
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!
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?