March 1999 - Categories - categories.org.au

Errata corrige to my previous message
by grandis＠dima.unige.it 19 Mar '99

19 Mar '99

In my previous reply to F. Lamarche's question, please take off from the last line of Remark 1: " (or cardinals as well) ". The site of cardinals 1, 2 also has the non-trivial involution 2 -> 2; its topos of presheaves is "INVOLUTIVE reflexive graphs" (which is also of interest in homotopy, of course). M. Grandis

1 0

"Practical Foundations of Mathematics"
by Paul Taylor 19 Mar '99

19 Mar '99

Practical Foundations of Mathematics Paul Taylor Department of Computer Science Queen Mary and Westfield College London E1 4NS http://www.dcs.qmw.ac.uk/~pt/book/ Cambridge Studies in Advanced Mathematics #59 (the series in which "Stone Spaces" by Johnstone and "Introduction to Higher Order Categorical Logic" by Lambek and Scott appeared.) ISBN: 0-521-63107-6 xii+576 pages List price: �50 or $80 I understand that the text and cover have now been printed, and are due to be bound on Monday 22 March in Cambridge, so I expect to see my own copy by the end of next week; orders should be dispatched after the Easter holiday. PLEASE SEE BELOW FOR THE BEST WAY TO ORDER YOUR COPY. The (not very informative) names of the chapters are: I First Order Reasoning VI Structural Recursion II Types and Induction VII Adjunctions III Posets and Lattices VIII Algebra with Dependent Types IV Cartesian Closed Categories IX The Quantifiers V Limits and Colimits The back cover "blurb" reads: Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming. The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the ``box method'' of proof taught successfully to first year informatics students. Chapters IV, V and VII are an introduction to categorical logic. Between the formal languages translations are provided which are fluent, showing how to write vernacular proofs which are sound in formal logics. Chapter VI is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naively or with set theory. The last two chapters prove in detail the equivalence of types and categories, in particular between generalised algebraic theories and categories with display maps. Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work. The web page currently just gives just the list of contents (down to the names of subsections), but when I have time to work on it I intend use it to publish many of the specific comments that people have made about the text (if those people are willing), and provide an interface for making further comments, and, of course, corrections. CUP has indicated that they have no objection to my publishing the entire text on the web in any form short of a printable DVI or PS file; when I have found a translator that actually works on my text, I intend to make an HTML version, obviously without most of the mathematical formulae, to feed to the web crawlers. HOW BEST TO ORDER YOUR COPY This depends on whether you would like to make a large donation to (a) your bookstore's profits: just quote the ISBN to them; (b) CUP's profits: fill in their web order form (no discount, by policy, and you pay cost of postage); (c) the UK Inland Revenue: wait until April 6 before you do anything; (d) the author, who has committed career suicide by writing this book at all. The special deal that I have negotiated is this. CUP is ADAMANT that it is contrary to their policy to give discounts for direct orders, even though the Web is now clearly the best way of ordering research-level books. However, by personal arrangement with my editor and the marketing manager, if you email, fax or phone the marketing manager, Richard Knott, email: rknott(a)cup.cam.ac.uk tel: +44 1223 325 916 fax: +44 1223 315 052, with your address and credit card number, mentioning that you saw this message from me, you get the book at list price INCLUSIVE of overland postage (normally �2.50), and I get some commission. If you want airmail delivery, there is an extra �2.50 charge. If you are not sure whether you actually want to buy the book yet, but you think you might (or might be teaching a course based on it) please email Richard Knott and say so, as soon as possible. If I get evidence of respectable sales prospects then I might persuade them to pay me an advance on royalties THIS MONTH - in the tax year during which I was unemployed for five months - instead of having a lump sum in May 2000 taxed at 40%. Please, this is important if you think that academic authors deserve some reward for the labour and demoralisation of eight years writing a book. �50 is pretty good value for a research book of this size. A recently announced book on similar material, published by the Dutch company Elsevier (North-Holland) costs TWICE the price (for 1/3 more pages). CUP, being part of Cambridge University, has no shareholders and counts as a charity for tax purposes, and there is no VAT on books in Britain. Even so, other recent books of same size in the same series as mine retail at �65. I kept the price of mine down by doing the whole of the typographical work myself (of course), and by NOT claiming the �2350 that I could have got for providing lower quality camera-ready hard copy instead of PostScript. Paul PS Unfortunately, despite my best efforts, I was not able to negotiate a reduction in the Bank of England's interest rates, and therefore in the present absurdly high Sterling exchange rate. Sorry. I will try to do better next time. CUP's postal address is Cambridge University Press, The Edinburgh Building, Shaftesbury Road, Cambridge, CB2 2RU, UK.

1 0

Monoidal structure, take II
by Francois Lamarche 19 Mar '99

19 Mar '99

Given the private replies I got to yesterday's queries, it is obvious I was not clear enough, and indeed there was an unhelpful typo. > > I'm wondering, if anybody has ever described the following monoidal > structure on the category of oriented multigraphs, what MacLane calls > graphs, the most common kind of graph in category theory (but not OK Saunders, from now on they're graphs. This what happens when you hang out with combinatorists AND category theorists. > > Given graphs X, Y, the set |X-oY| of vertices on X-oY is the set of graph > morphisms > X --> Y. So right from the start this is not the usual presheaf CC structure, where the set of vertices is the set of all functions |X| --> |Y| . So in what follows I use categorical notation for vertices, arrows, etc. > Given f,g : X --> Y the set of arrows f-->g is the set of pairs > (p_0,p_1) of functions such that > > forall x in |X|, p_0(x) : f(x)-->g(x) > > forall k: x-->y in X, p_1(k) : f(x)-->g(y) Now the typo has been corrected. So an arrow f --> g is like a natural transformation, with p_0 the usual familly of arrows indexed by the vertices/objects of X, but since things don't compose, you add the diagonal p_1 as part of the information. There is some kinship to homotopies, as M. Barr has remarked. > This co-contra bifunctor has a tensor left adjoint, which is symmetric > and monoidal. > Is this more understandable? Thanks again Francois

3 3

Monoidal structure on graphs
by Francois Lamarche 18 Mar '99

18 Mar '99

Greetings, fellow categorists. I'm wondering, if anybody has ever described the following monoidal structure on the category of oriented multigraphs, what MacLane calls graphs, the most common kind of graph in category theory (but not everywhere) : Given mgs X, Y, the set |X-oY| of vertices on X-oY is the set of mg morphisms X --> Y. Given f,g : X --> Y the set of arrows f-->g is the set of pairs (p_0,p_1) of functions such that forall x in |X|, p_0(x) : f-->g forall k: x-->y in X, p_1(k) : f(x)-->g(y) This co-contra bifunctor has a tensor left adjoint, which is symmetric and monoidal. I would be quite surprised if this structure had never been seen before. Enriched universal algebra in there has applications in computer science. Thanks, Francois Lamarche

2 1

Research scholarships available at Birmingham
by Marta Z Kwiatkowska 16 Mar '99

16 Mar '99

Please bring this to the attention of potential applicants. Apologies for duplicate mailing. Thanks Marta _____ The University of Birmingham School of Computer Science Research scholarships in Computer Science and Artificial Intelligence The School of Computer Science has research strengths in the areas of Theoretical Computer Science, Artificial Intelligence and Cognitive Science, and Software Engineering. The Theory of Computation group concentrates on the development of logics and semantics for programming languages. The overall aim is to provide intuitive conceptual tools for the everyday practice of programming. Within this framework, the activities range from abstract mathematics to issues of implementation and software development. Current research projects include probabilistic modelling and model checking, software verification, semantics for concurrent systems, observation logics, exact real number computation, semantics for databases, (linear) functional programming, type systems for optimization of programs, type theory and automated deduction. Current academic and research members of the Theory group are: Dr Viviana Bono, Dr Valeria de Paiva (on leave during 1999), Dr Mateja Jamnik, Professor Achim Jung, Mr Mathias Kegelmann, Dr Manfred Kerber, Dr Marta Kwiatkowska, Dr Emilia Maietti, Dr Gethin Norman, Dr Eike Ritter and Dr Mark Ryan. Professor Uday Reddy will be joining from January 2000. There are also 8 PhD students associated with the group, of the total of 30 in the School. Possible topics for research include, but are not restricted to: Probabilistic and stochastic systems Software verification Model checking of probabilistic systems Semantics for concurrency Temporal and modal logics Domain theory Extensions to the relational database model (theory and implementation) Semantics of object-oriented languages Parametricity and foundations of data abstraction Type systems for imperative and OO programming Linear logic, type theory and corresponding categorical semantics Linear abstract machines Machine-assisted reasoning Diagrammatic reasoning Theorem proving and proof planning Applicants must have or be about to gain at least an upper second class honours degree or an overseas equivalent in Computer Science or a related degree title. The School has a number of EPSRC Studentships, School Studentships and Teaching Assistantships available to UK and European Union applicants. School Studentships and Teaching Assistantships cover tuition fees and maintenance for UK and European Union students. EPSRC studentships do not pay maintenance costs for non-UK students. Further details of these studentships and also of studentships for international students are given in: http://www.cs.bham.ac.uk/~pjh/prospectus/funding/research.html The School's research student prospectus and application form are available from: http://www.cs.bham.ac.uk/studentinfo/form_mailer.html Informal enquiries can be directed to any member of the group: Valeria de Paiva (on leave during 1999) Achim Jung +44 121 414 4776 Manfred Kerber +44 121 414 4787 Marta Kwiatkowska +44 121 414 7264 Eike Ritter +44 121 414 4772 Uday Reddy (joining in January 2000) Mark Ryan +44 121 414 7361 email {vdp,axj,mmk,mzk,exr,mdr}(a)cs.bham.ac.uk u-reddy(a)reddy.cs.uiuc.edu URLs http://www.cs.bham.ac.uk/{~vdp,~axj,~mmk,~mzk,~exr,~mdr} http://www.uiuc.edu/ph/www/u-reddy

1 0

lax monad
by Gaunce Lewis 15 Mar '99

15 Mar '99

I am looking for literature references for the notion of a 'lax' monad (or triple), and lax algebras over such, in the context of 2-categories--the definition being that the usual diagrams commute only up to a 2-cell. Can anyone suggest good references? Thanks, Gaunce Lewis

2 1

BCTCS 15
by John G. Stell 13 Mar '99

13 Mar '99

SECOND CALL FOR CONTRIBUTIONS AND PARTICIPATION 15th British Colloquium for Theoretical Computer Science (BCTCS 15) 14th - 16th April 1999 at Keele University Supported by EPSRC and the London Mathematical Society ___________________________________________________________________________ ** FREE places for EPSRC funded students are still available ** Special REDUCED RATE for other students ** Further CONTRIBUTED TALKS on any relevant topic are still needed ** Register before 23rd MARCH to avoid late registration charge ** INVITED SPEAKERS: Wan Fokkink (Swansea) Martin Hofmann (Edinburgh) Bill McColl (Oxford) Ian Pratt (Manchester) David Pym (QMW, London) Glynn Winskel (Aarhus) Mike Worboys (Keele) ___________________________________________________________________________ CONTRIBUTED TALKS Contributions are sought on any aspect of theoretical computer science. Research areas within the scope of BCTCS include, but are not limited to, the following list: Concurrency, types, semantics, formal methods, computational complexity, algorithms, discrete mathematics, proof theory and logic, artificial intelligence, database theory, theorem proving, symbolic computation and experimental work. This year for the first time, authors will have the OPTION to submit papers based on their talks to a special issue of the Journal of Universal Computer Science. However, the meeting will retain its informal character, and it is still possible for researchers to give a presentation at the meeting but not have their paper considered for publication. Details of the submission of papers for the special issue can be found on the BCTCS 15 web page. ___________________________________________________________________________ SUPPORT FOR POSTGRADUATE STUDENTS A limited number of fully funded places are available to postgraduate students who are supported by EPSRC. For other students there is a SPECIAL REDUCED RATE for the meeting, and some additional financial support may be available in special cases. ___________________________________________________________________________ FURTHER DETAILS Further details, including registration forms, prices, and forms for submission of contributed talks, are available from the BCTCS15 web page: http://www.keele.ac.uk/depts/cs/Announcements/bctcs/ The web page has a list of contributed talks offered so far for BCTCS 15. The web page also has links to previous BCTCS meetings, which provide a useful guide to the wide range of topics which have been covered by past contributions. BCTCS15 is organized by John Stell, who can be contacted by email: john(a)cs.keele.ac.uk or at: Department of Computer Science, Keele University, Keele, Staffs, U. K., ST5 5BG. ___________________________________________________________________________

1 0

Rewrite Methods for Kan Extensions of Actions of Categories
by Anne Heyworth 12 Mar '99

12 Mar '99

The following is available on the xxx archive. http://xxx.soton.ac.uk/abs/math.CO/9903032 Title: Using Rewriting Systems to Compute Kan Extensions and Induced Actions of Categories Authors: Ronald Brown, Anne Heyworth (University Of Wales, Bangor) Comments: 31 pages, LaTeX2e, (submitted to JSC) Subj-class: Combinatorics MSC-class: 68Q42 18A40 68Q40 The basic method of rewriting for words in a free monoid given a monoid presentation is extended to rewriting for paths in a free category given a `Kan extension presentation'. This is related to work of Carmody-Walters on the Todd-Coxeter procedure for Kan extensions, but allows for the output data to be infinite, described by a language. The result also allows rewrite methods to be applied in a greater range of situations and examples, in terms of induced actions of monoids, categories, groups or groupoids. (28kb) Prof R. Brown, School of Mathematics, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382475 fax: +44 1248 383663 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ New article: Higher dimensional group theory Symbolic Sculpture and Mathematics: http://www.bangor.ac.uk/SculMath/ Mathematics and Knots: http://www.bangor.ac.uk/ma/CPM/exhibit/welcome.htm Dr Anne Heyworth, School of Mathematics, University of Wales, Bangor home page: http://www.bangor.ac.uk/~map130/welcome.html

1 0

Report on verification of unknown number of processes
by farn＠iis.sinica.edu.tw 10 Mar '99

10 Mar '99

Recently, we have developed a new verification technique which can be used to verify infinite state systems. A manuscript: Verification of Dynamic Linear Lists for All Numbers of Processes in PostScript format can be obtained through my webpage: http://www.iis.sinica.edu.tw/~farn/index.html#quo A preliminary report can also be found in TR-IIS-98-019 published last year. Thank you for reading this email. Best wishes, Farn ABSTRACT: In real-world design and verification of concurrent systems with many identical processes, the number of processes is never a factor in the system correctness. This paper embodies such an engineering reasoning to propose an almost automatic method to safely verify safety properties of such systems. The central idea is to construct a finite collective quotient structure (CQS) which collapses state-space representations for all system implementations with all numbers of processes. The problem is presented as safety bound problem which ask if the number of processes satisfying a certain property exceeds a given bound. Our method can be applied to systems with dynamic linear lists of unknown number of processes. Processes can be deleted from or inserted at any position of the linear list during transitions. We have used our method to develop CQS constructing algorithms for two classes of concurrent systems : (1) untimed systems with a global waiting queue and (2) dense-time systems with one local timer per process. We show that our method is both sound and complete in verifying the first class of systems. The verification problem for the second class systems is undecidable even with only one global binary variable. However, our method can still automatically generate a CQS of size no more than 1512 nodes to verify that an algorithm in the class: Fischer's timed algorithm indeed preserves mutual exclusion for any number of processes.

1 0

Quantum vertex algebras
by James Stasheff 10 Mar '99

10 Mar '99

math.QA/9903038 [abs, src, ps, other] : Title: Quantum vertex algebras Authors: Richard E. Borcherds Comments: 18 pages, plain tex Subj-class: Quantum Algebra; Category Theory concludes with a large set of problems some of which are strictly n-categorical The purpose of this paper is to make the theory of vertex algebras trivial. We do this by setting up some categorical machinery so that vertex algebras are just ``singular commutative rings'' in a certain category. This makes it easy to construct many examples of vertex algebras, in particular by using an analogue of the construction of a twisted group ring from a bicharacter of a group. We also define quantum vertex algebras as singular braided rings in the same category and construct some examples of them. The constructions work just as well for higher dimensional analogues of vertex algebras. (18kb) ************************************************************ Jim Stasheff jds(a)math.upenn.edu 146 Woodland Dr Lansdale PA 19446 (215)822-6707 Jim Stasheff jds(a)math.unc.edu Math-UNC (919)-962-9607 Chapel Hill NC FAX:(919)-962-2568 27599-3250

1 0