Dear Tom, I will do my best to answer your question writing on mi iPad - my only tool here in Greece for the summer. The first part of the article by Julie Rehmayer is standard and I find no fault with it. It is in the second part that the author reveals her ignorance of the subject. The assertion "the theory of programming languages and the field of logic can be seen as essentially identical to category theory " is pure nonsense, even more so as it is given an outrageous name - "computational trinitarianism" even if spoken in jest. Why is this assertion wrong? Because it distorts completely the nature and role of category theory. Firstly, category theory is a field in itself, its main virtue being, not to compute but to better understand, simplify, unify several mathematical fields and in turn their applications. Secondly, category theory serves as a foundation of mathematics that is closer to mathematical practice than set theory ever was. Within category theory there are, as you know, several distinct but related areas - fibered categories, algebraic theories monads and their algebraic, topos theory, model structures, 2-categories ( and reasonably beyond without falling into science fiction). These in turn have been succesfully employed in several areas in mathematics, such as algebraic geometry, homotopy theory, differential geometry and topoly, functional analysis, as well as in computer science, logic, model theory, physics, linguistics. Some of those applications have promoted further developments of the theory of categories itself. Instead of pointing this out, the author of this article jumps to mention solely applications which are sure to impress the naive reader, such as quantum information theory, biological systems, linguistics, even music, as if the fundamental role of category theory in mathematics were not as important or even more so. In short, her report on category theory is more typical of a tabloid than of serious scientific journalism. The last part is an instance of what I mean by doing more harm than good. Instead of directing the reader to the best texts for introducing the subject of category theory to a wide audience, she implicitly recommends a book by David Spivak, " published" in Arxives. This book. which I perused solely on account of the article by Julie Rehmeyer, promotes category theory mostly as a language for recording data bases in an efficient way. It dismisses the far superior text by F. W. Lawvere and S. Schanuel, Conceptual Mathematics, Cambridge University Press, 1997. The latter not only instructs but motivates. Even for an expert in the subject, to read it is pure pleasure. Another valuable elementary textbook is one by M. Barr and C. Wells, Category Theory for Computing Science, CRM, Third edition, 1999. I hope that this partially answers your question. Kind regards, Marta Sent from my iPad On 2013-06-07, at 8:33 AM, "Tom Hirschowitz" <tom.hirschowitz@univ-savoie.fr> wrote:
Dear Marta,
I'm curious to know why you think the article may do more harm than good. It sures simplifies matters a lot, and forgets important aspects of category theory. But `distorting' surprises me. Of course, my education was not in category theory, so probably there are historical aspects I know nothing about.
Best, Tom
On 06/06/2013 04:38 PM, Marta Bunge wrote:
Dear Ross,
I find this article not only superficial but misleading. Its presentation of category theory is not only simplified but distorting. I think that it may do more harm than good It is important to know how we are seen in some sources,
but we need not pay attention to them. Even if (or particularly because) an article like this one is seemingly laudatory.
Best regards, Marta
Sent from my iPad
On 2013-06-06, at 9:24 AM, "Ross Street"<ross.street@mq.edu.au> wrote:
http://www.sciencenews.org/view/generic/id/350567/description/One_of_the_mos...
Perhaps the above article is more good than harm.
Ross www.math.mq.edu.au/~street
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 8 Jun 2013, at 10:39, Marta Bunge wrote:
It is in the second part that the author reveals her ignorance of the subject. The assertion "the theory of programming languages and the field of logic can be seen as essentially identical to category theory " is pure nonsense, even more so as it is given an outrageous name - "computational trinitarianism" even if spoken in jest.
Don't blame Rehmayer for the "computational trinitarianism" line; that's Bob Harper's invention, tongue in cheek. But I don't think Harper is to blame for equating CT with PL and logic. He does say
The doctrine of computational trinitarianism holds that computation manifests itself in three forms: proofs of propositions, programs of a type, and mappings between structures. These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures. The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation.
http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ All I take him to mean is that logic, languages, and categories offer three complementary perspectives on computation. I don't think you can read this as "computation subsumes category theory". Jeremy Jeremy.Gibbons@cs.ox.ac.uk Oxford University Department of Computer Science, Wolfson Building, Parks Road, Oxford OX1 3QD, UK. +44 1865 283521 http://www.cs.ox.ac.uk/people/jeremy.gibbons/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
These discussions on trinity and similar seem to raise only irritation where there would be opportunity to provide constructive discussions. CT has done a good job in explaining and providing rigour. Some like it, some don't. Type theory is a typical example where computer science is "on its own", unless trying to understand trinity like suggestions. Take 'lambda', for instance. Church said already back in 1940 that 'lambda' is an "improper symbol" and that his 'o' type for something in direction of propositions, but Church says: "We purposely refrain from making more definite the nature of the types o and iota" (peklund: the 'type' type!) ", the formal theory admitting of a variety of interpretations in this regard. Of course the matter of interpretation is in any case irrelevant to the abstract construction of the theory, and indeed other and quite different interpretations are possible (formal consistency assumed)." 'Trinity' also raises irritation and even fear as it refers to the Holy Trinitiy, and many feel very uncomfortable even talking about these things. The wordpress blog mentioned is also very shallow in its introduction, just mentioning "manifest in three persons". Some may be interested to look more into the relation of "the three" as it has been part of history and e.g. the split of the Latin and Greek Churches. The so called Filioque addition and why it happened, and how it appears in the Latin language is far beyond just saying "manifests". The way Augustinus opposed Arianism and his choices of 'language' is, I think, a bit interesting in this context. Or maybe not. Rigour to me is just being clear about what is what. For instance, sentences build upon terms, and satisfaction/entailment needs sentences. This shold mean we need to be precise about terms, and then closing that door. Then we are precise about sentences, and closing that door, and so on. We should somewhere along that path, e.g. after having closed the "sentences door", come up with new and nice sentences still to be used. G?del was doing that all the time. We shouldn't, I think, allow "circadian rhythms" into science and mathematics, in particular in type theory concerning how types and propositions are "manifested" in each other. Cheers, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
Jeremy Gibbons -
Marta Bunge -
Patrik Eklund