February 1998 - Categories - categories.org.au

Paper on Feedback announced
by Robert Seely 01 Mar '98

01 Mar '98

The following paper is available on RAG Seely's WWW home page at <http://www.math.mcgill.ca/~rags> or directly by ftp at <ftp://triples.math.mcgill.ca/pub/rags/linear/trace.ps.gz> or <ftp://triples.math.mcgill.ca/pub/rags/linear/trace.dvi.gz> Comments are most welcome; please send them to any of the authors. Any problems in obtaining the paper should be sent to rags(a)math.mcgill.ca. Feedback for linearly distributive categories: traces and fixpoints by R.F. Blute J.R.B. Cockett R.A.G. Seely ABSTRACT In the present paper, we develop the notion of a trace operator on a linearly distributive category, which amounts to essentially working within a subcategory (the "core") which has the same sort of "type degeneracy" as a compact closed category. We also explore the possibility that an object may have several trace structures, introducing a notion of compatibility in this case. We show that if we restrict to compatible classes of trace operators, an object may have at most one trace structure (for a given tensor structure). We give a linearly distributive version of the "geometry of interaction" construction, and verify that we obtain a linearly distributive category in which traces become canonical. We explore the relationship between our notions of trace and fixpoint operators, and show that an object admits a fixpoint combinator precisely when it admits a trace and is a cocommutative comonoid. This generalises an observation of Hyland and Hasegawa. This paper is presented to Bill Lawvere on the occasion of his 60th birthday. =================================== RAG Seely <rags(a)math.mcgill.ca> <http://www.math.mcgill.ca> [ NB - please use the "generic" email address above and not machine specific e-addresses like "rags(a)triples.math.mcgill.ca" ] ===================================

1 0

Paper available
by rblute＠mathstat.uottawa.ca 28 Feb '98

28 Feb '98

The following paper is available by anonymous ftp at triples.math.mcgill.ca in the directory pub/blute as nuclear.ps.gz. It is also on Prakash Panangaden's homepage at www-acaps.cs.mcgill.ca. Feel free to contact me if there are any problems. Cheers, Rick Blute Nuclear and Trace Ideals in Tensored *-Categories ================================================= Samson Abramsky Richard Blute Department of Computer Science Department of Mathematics University of Edinburgh and Statistics Edinburgh, Scotland University of Ottawa Ottawa, Ontario, Canada Prakash Panangaden Department of Computer Science McGill University Montreal, Quebec, Canada Presented to Mike Barr on the occasion of his 60th birthday. Abstract ======== We generalize the notion of nuclear maps from functional analysis by defining nuclear ideals in tensored *-categories. The motivation for this study came from attempts to generalize the structure of the category of relations to handle what might be called ``probabilistic relations''. The compact closed structure associated with the category of relations does not generalize directly, instead one obtains nuclear ideals. Most tensored *-categories have a large class of morphisms which behave as if they were part of a compact closed category, i.e. they allow one to transfer variables between the domain and the codomain. We introduce the notion of nuclear ideals to analyze these classes of morphisms. In compact closed categories, we see that all morphisms are nuclear, and in the category of Hilbert spaces, the nuclear morphisms are the Hilbert-Schmidt maps. We also introduce two new examples of tensored *-categories, in which integration plays the role of composition. In the first, morphisms are a special class of distributions, which we call tame distributions. We also introduce a category of probabilistic relations which was the original motivating example. Finally, we extend the recent work of Joyal, Street and Verity on traced monoidal categories to this setting by introducing the notion of a trace ideal. For a given symmetric monoidal category, it is not generally the case that arbitrary endomorphisms can be assigned a trace. However, we can find ideals in the category on which a trace can be defined satisfying equations analogous to those of Joyal, Street and Verity. We establish a close correspondence between nuclear ideals and trace ideals in a tensored *-category, suggested by the correspondence between Hilbert-Schmidt operators and trace operators on a Hilbert space. When we apply our notion of trace ideal to the category of Hilbert spaces, we obtain the usual trace of an endomorphism in the trace class.

1 0

CONCUR98: final CFP (EXTENDED deadline)
by Davide.Sangiorgi＠sophia.inria.fr 27 Feb '98

27 Feb '98

[Apologies if you receive multiple copies] !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! Please note: -- extended deadline -- (very likely) The auditorium of Nice Museum of Modern and Contemporary Art as venue !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! Last Call for Papers CONCUR'98 9th International Conference on Concurrency Theory Nice, France, September 8-11, 1998 <http://www.inria.fr/concur98/> Important dates ~~~~~~~~~~~~~~~ Paper submissions: March 18, 1998 (EXTENDED deadline) Notifications: May 8, 1998 Final versions: June 10, 1998. Venue and local arrangements ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Nice is ideally located on the French Riviera. September is still very pleasant, while less crowded than the high season. Nice's international airport is well-connected to all major european and non-european cities. Most likely the conference will be held at the auditorium of Nice Museum of Modern and Contemporary Art, which is conveniently located in the heart of Nice, between the city center and the old town, and 20 minutes walk to the beach. The Museum is next to the Hotel Novotel, where satellite workshops and registration will be held. CONCUR 98: Purpose and Scope ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications. Interest in this topic is continuously growing, as a consequence of the importance of concurrent systems and their applications, and of the scientific relevance of their foundations. The scope of CONCUR'98 covers all areas of semantics, logics, and verification techniques for concurrent systems. A list of specific topics includes (but is not limited to) concurrency related aspects of models of computation and semantic domains, process algebras, Petri nets, event structures, real-time systems, hybrid systems, decidability, model-checking, verification techniques, refinement techniques, term and graph rewriting, distributed programming, logic constraint programming, object-oriented programming, typing systems and algorithms, case studies, tools and environments for programming and verification. Submissions: ~~~~~~~~~~~~~ Submissions should consist of a 100-200 word ASCII abstract and summary (up to 15 pages, typeset 12 points; about 7000 words, excluding bibliography and figures). Simultaneous submissions to other conferences or journals are not allowed. Electronic submissions in PostScript(tm) are strongly encouraged; instructions can be found at the URL <http://www.inria.fr/concur98/submissions.html>, or can be obtained by sending an email with subject "submission information" to c98-subm(a)sophia.inria.fr. If surface mail is used, then five (5) copies of the paper should be sent to the following address: Concur'98, INRIA Sophia-Antipolis, BP 93, F-06902 Sophia-Antipolis Cedex, France. Program Committee ~~~~~~~~~~~~~~~~~~~ M. Abadi (Digital,Systems Research Center) A. Asperti (University of Bologna) J. Bradfield (University of Edinburgh) E. Clarke (Carnegie Mellon University) R. de Simone (INRIA Sophia-Antipolis, co-chair) J. Esparza (Technische Universitat Munchen) P. Gastin (University of Paris 7) R. van Glabbeek (Stanford University) G. Gonthier (INRIA Rocquencourt) M. Hennessy (Sussex University) O. Maler (Verimag Grenoble) F. Moller (Uppsala University) U. Montanari (University of Pisa) M. Mukund (SMI Madras) M. Nielsen (University of Aarhus) P. Panangaden (Mc Gill University) J. Parrow (Royal Institute of Technology, Stockholm) A. Rensink (University of Hildesheim) D. Sangiorgi (INRIA Sophia-Antipolis, co-chair) C. Talcott (Stanford University) J. Winkowski (Polish Academy of Sciences) Invited Speakers and Tutorials: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (in square brackets, the topic of the talk) Invited Speakers: T. Henzinger (University of California at Berkeley, USA) [Hybrid systems]; U. Herzog (Erlangen, Germany) [Process algebra for performance evaluation]; J. Rutten (CWI, Netherlands) [Coalgebraic models of computation]; J.-B. Stefani (CNET, France Telecom) [Open distributed systems]; M. Vardi (Rice University, USA) [Branching and linear time temporal logics]. Invited Tutorials : G. Berry (CMA Ecole des Mines, France) [Synchronous reactive programming and Esterel]; J.F. Groote (CWI, Netherlands) [Theorem provers in concurrency]; B. Pierce (Indiana U., USA) [Types in concurrency]. Financial Support ~~~~~~~~~~~~~~~~~~ We wish to thank the following companies and organisations for financial support: CNET France Telecom, Dassault Aviation, Simulog, CMA-Ecole des Mines, INRIA. Satellite events ~~~~~~~~~~~~~~~~~ COTIC'98: 2nd international workshop on Concurrent Constraint Programming for Time Critical Applications EXPRESS'98: 5th international workshop on Expressiveness in Concurrency HLCL'98: 3rd international workshop on High-Level Concurrent Languages PAPM'98: 6th international workshop on Process Algebra and Performance Modeling CONFER W.G.: 4th workshop of the CONFER (Concurrency and Functions: Evaluation and Reduction) working group. Publications ~~~~~~~~~~~~ The proceedings will be published by Springer-Verlag in the LNCS series. A special issue of Theoretical Computer Science is planned. Steering Committee ~~~~~~~~~~~~~~~~~~ The Steering Committee of CONCUR is composed of Jos Baeten (chair, Eindhoven), Eike Best (Oldenburg), Kim Larsen (Aalborg), Ugo Montanari (Pisa), Scott Smolka (Stony Brook) and Pierre Wolper (Liege). Organizing Committee ~~~~~~~~~~~~~~~~~~~~~ The Organizing Committee of CONCUR 98 is composed of Amar Bouali, Gerard Boudol, Ilaria Castellani, Robert de Simone, Catherine Juncker, Francoise Martin-Trucas, Davide Sangiorgi, and Dany Sergeant. ============================== For further information, check URL <http://www.inria.fr/concur98/>, or mail to concur98(a)sophia.inria.fr.

1 0

new paper: A Relevant Analysis of Natural Deduction
by Samin Ishtiaq 25 Feb '98

25 Feb '98

We apologize for multiple copies of this mail. The following paper will appear in the Journal of Logic and Computation (expected in Vol. 8) later this year: A Relevant Analysis of Natural Deduction S Ishtiaq and DJ Pym Queen Mary and Westfield College University of London {si,pym}(a)dcs.qmw.ac.uk We study a framework, RLF, for defining natural deduction presentations of linear and other relevant logics. RLF consists in a language together, in a manner similar to that of LF, with a representation mechanism. The language of RLF, the $\lambda\Lambda_{\kappa}$-calculus, is a system of first-order linear dependent function types which uses a function $\kappa$ to describe the degree of sharing of variables between functions and their arguments. The representation mechanism is judgements-as-types, developed for linear and other relevant logics. The $\lambdal\Lambda_{\kappa}$-calculus is a conservative extension of the $\lambda\Pi$-calculus and RLF is a conservative extension of LF. The paper will be available from our Hypatia entries, at http://hypatia.dcs.qmw.ac.uk. It is also available at http://www.dcs.qmw.ac.uk/~si. We are currently engaged in further study of the proof theory of the $\lambda\Lambda_{\kappa}$-calculus; this includes setting up a proposition-as-types correspondence and a Gentzenization of the type theory. We are also investigating categorical models, specifically resourced-indexed Kripke models, of the $\lambda\Lambda_{\kappa}$-calculus. Samin Ishtiaq David Pym

1 0

email address
by maxk＠maths.usyd.edu.au 17 Feb '98

17 Feb '98

Please note that my old email address kelly_m(a)maths.su.oz.au is soon to be obsolete, and should be replaced by maxk(a)maths.usyd.edu.au Regards - Max Kelly.

1 0

CATEGORY THEORY WORKSHOP
by rjwood＠mscs.dal.ca 17 Feb '98

17 Feb '98

ANNOUNCEMENT WORKSHOP In conjunction with the Category Theory Symposium at the Canadian Mathematical Society's (Northern) Summer 1998 Meeting, there will be a workshop on the Applications of Category Theory to Computer Science, directed towards graduate students and young researchers. June 8-12, 1998 (arrival day Sunday, June 7,1998) Mount Allison University (home of CATEGORIES and TAC) Sackville, New Brunswick, Canada The invited instructors are M. Barr (McGill) and R.F.C. Walters (Sydney). Residence accommodation will be available at Mount Allison University at a cost of $27.60/person/night for a single room $24.30/person/night for a shared double room $23.00/person/night for either of the above for students upon presentation of a student card. (All prices are in Canadian dollars and include taxes.) Bookings can be made at http://www.mta.ca/conference/overnigh.htm There will be a registration fee of $50 for the workshop. To preregister send e-mail to ct95(a)mscs.dal.ca (sic) with subject heading `workshop'. On the evening of Friday June 12 the Workshhop participants will receive free transportation to Saint John, New Brunswick, site of the aforementioned Category Theory Symposium. Sponsored by The Fields Institute for Research in Mathematical Sciences and AARMS, The Atlantic Association for Research in the Mathematical Sciences

1 0

CATEGORY THEORY SYMPOSIUM
by rjwood＠mscs.dal.ca 17 Feb '98

17 Feb '98

ANNOUNCEMENT CATEGORY THEORY SYMPOSIUM A special session of the Canadian Mathematical Society Summer 1998 Meeting June 13-15, 1998 University of New Brunswick (Saint John) Saint John, New Brunswick, Canada The symposium follows the usual format found at society meetings in North America. Thus it is part of a larger programme including plenary talks, one of which will be given by S. Schanuel (SUNY Buffalo). The larger programme also features a public lecture by F.W. Lawvere (SUNY Buffalo). The invited speakers for the Category Theory Symposium are M. Barr (McGill), M. Bunge (McGill), P. Freyd (Pennsylvania), A.Joyal (UQAM), F.W. Lawvere (SUNY Buffalo), M. Makkai (McGill), S. Niefield (Union), R. Pare (Dalhousie), J.W. Pelletier (York), S. Schanuel (SUNY Buffalo), M. Tierney (Rutgers), W. Tholen (York), and R.F.C. Walters (Sydney). Registration for the meeting, including fees, is handled by the Canadian Mathematical Society (CMS). A pre-registration form can be obtained by writing to meetings(a)cms.math.ca Electronic pre-registration is available on the CMS site at http://camel.math.ca/CMS/Events/summer98 At this site complete information about all necessities, such as accommodation, is provided. However, category theorists who plan to attend are strongly urged to also send e-mail to ct95(a)mscs.dal.ca (sic) where it will be readily available to RJ Wood (Dalhousie), Category Theory Session Organizer and Robert Rosebrugh (Mount Allison), Meeting Director

1 0

CATS Are primes ever generators?
by David Espinosa 16 Feb '98

16 Feb '98

We can say that an object P in a category with coproducts is *prime* if whenever f : P -> A+B, f factors through one of the injections into A+B. (1) I didn't find any reference to this (obvious) notion of primality in the standard texts. Does it occur anywhere? (2) Is there any condition on the category under which the set of primes is a generating family? Since objects are decomposable into a "quotient of a coproduct of generators" (Borceux, volume 1, page 151), this would give a decomposition into primes. Thanks, David

2 1

CATS Re: Categorical model for Floyd-Hoare logic?
by Roy L. Crole 16 Feb '98

16 Feb '98

There is some work by Paul Taylor on categorical models of while in Theory and Formal Methods 1993, Springer Workshops in Computing, p302 on. Roy Crole

2 1

correction
by Paul Taylor 16 Feb '98

16 Feb '98

> My motication (in 1987 this was) This should have been 1984 (and motivation). I'd also like to add: I had some difficulty in getting my ideas about stable coequalisers across (partly, of course, my fault, because I didn't get the rigt answer, involving stable transitive closures, until 1993). People said, "while programs can't possibly be described by finitary first order theories, because the theory of the natural numbers is an example". I knew that, and it wasn't what I meant. This illustrates a subtlely in first order categorical logic: that the relevant structure consists of *less* than all finite (limits and) stable disjoint colimits. The categorical structure corresponding to first order logic is a (Heyting) pretopos, which need not have coequalisers of arbitrary parallel pairs. For example, the category of compact Hausdorff spaces is a pretopos but does not have all stable coequalisers. (I have a feeling I haven't got this quite right, and Peter Freyd is going to jump on me. I shouldn't be so foolish as to answer mathematical questions on the modem from home!) More recently, Jiri Rosicky and Peter Johnstone have considered the question of what theories can be expressed with finite sketches. As Peter Freyd showed in 1972, this includes the natural numbers. My results and those of Jiri and Peter are more complicated forms of Peter Freyd's original observation. Finally, since my more recent work on categorical recursion, I no longer think that a coequaliser diagram is the best way of presenting a WHILE program categorically (though the diagram I would use now expresses the same logical content). Paul

1 0