From cat-dist Tue Mar 2 00:40:54 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id XAA04339 for categories-list; Mon, 1 Mar 1999 23:45:16 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199903011147.MAA14256@mammut.informatik.uni-rostock.de> Date: Mon, 1 Mar 1999 12:47:34 +0100 (MET) From: Natalia Ioustinova Reply-To: Natalia Ioustinova Subject: categories: OOSDS'99 CALL FOR PAPERS To: benelog@cs.kuleuven.ac.be Cc: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: RmHKT9X1e1il/ws10TZw1w== X-Mailer: dtmail 1.2.1 CDE Version 1.2.1 SunOS 5.6 sun4u sparc Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: This message contains public information, only, and the receiver is allowed, and invited, to copy it and distribute it further. Our apologies if you received duplicates of this message due to the mailing list aliases. You can also visit the OOSDS'99 web site at http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ================================================================================ CALL FOR PAPERS OOSDS'99 Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours Paris, France, September 27, 1999 http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ================================================================================ SCOPE OF WORKSHOP: ================= The workshop is focused on specification languages for distributed systems which are extensions of object-oriented languages or have an object-oriented kind of base structure. The aim is to bring together researchers interested in incorporating object-oriented concepts and formal methods for specification of distributed systems and behaviours. TOPICS (NOT EXCLUSIVE LIST): ============================ Object-oriented approaches to specification of distributed systems and behaviours. Semantic models for concurrency and object-orientation (e.g. based on the lambda-calculus, process algebra, pi-calculus, linear logic). Characteristic examples of object-oriented specification from real application domains (e.g. distributed algorithms, workflow specification, communication protocols). Logic reasoning on distributed systems and behaviours. SUBMISSION: =========== The deadline for submission is September 14, 1999. Submission is in electronic form only. Submission may be of two forms: Extended abstracts: up to 3 pages. Papers and reports: up to 6 pages. In both cases a separate page with the following information: title, author(s), corresponding author, contact information and a 12-15 lines summary should be included. The papers and/or abstracts should be sent by e-mail to ustin@informatik.uni-rostock.de. PUBLICATION: ============ Selected submissions will be published in a refereed journal after the workshop. The others will be published electronically. RELATED EVENTS: ============== This workshop is organized as a satellite workshop of PPDP'99, The 1999 International Conference on Principles and Practice of Declarative Programming, Paris, France, September 29-October 1, 1999 http://www.dmi.ens.fr/~fages/PPDP99/ ORGANIZATION COMMITTEE: ======================= Clemens H. Cap (Rostock University, Germany) Natalia Ioustinova (Rostock University, Germany) Javier Oliver (Technical University of Valencia, Spain) Nobuko Yoshida (University of Sussex, UK) ADDITIONAL INFORMATION: ======================= WEB: http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ MAIL: ustin@informatik.uni-rostock.de Natalia Ioustinova Dept.of Computer Science office phone +49-(0)381-498/3375 University of Rostock Albert Einstein Strasse 21 mailto:ustin@informatik.uni-rostock.de D-18051 Rostock, Germany http://www.tec.informatik.uni-rostock.de/IuK From cat-dist Tue Mar 2 00:43:56 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id XAA06414 for categories-list; Mon, 1 Mar 1999 23:58:45 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: To: categories@mta.ca Subject: categories: PhD positions Mime-Version: 1.0 (generated by tm-edit 7.108) Content-Type: text/plain; charset=US-ASCII Date: Mon, 01 Mar 1999 17:13:14 +0100 From: N Ghani Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ---------------------------------------------------------------------- Leicester University, U.K. Department of Mathematics & Computer Science 3 PH.D. STUDENTSHIPS IN MATHEMATICS OR COMPUTER SCIENCE Applications are invited for three fully funded research studentships leading to the degree of Ph.D. in any aspect of Mathematics or Computer Science. The studentships are available for studies beginning in October 1999 to persons who are normally resident in the E.U. Applicants should have, or expect to obtain, a first or upper second class degree in a relevant subject area. The Department of Mathematics and Computer Science is divided into three groups: Pure Mathematics, Applicable Mathematics and Computer Science. The Pure Mathematics Group carries out research in various aspects of algebra, algebraic topology and symbolic dynamics. The key areas of expertise are in the representation theory of finite dimensional algebras, of finite groups and of quantum groups and in algebraic topology and its applications to dynamical systems, algebra and analysis. The Applicable Mathematics Group focuses mainly on numerical analysis, and in particular on: approximation theory; the numerical solution of ordinary and partial differential equations; and integral equations. Research in the Computer Science Group has three main themes: logic, algebra and complexity; the theory of distributed systems; and semantics. There is an active Graduate Programme. Candidates should identify their preferred area of research and supervisor. Details of the possible areas of research and supervisors are available via the Departmental web pages (http://www.mcs.le.ac.uk) or the Department's Postgraduate Brochure. The Postgraduate Brochure, application forms and further details are available from Dr. S. J. Ambler, Department of Mathematics and Computer Science, Leicester University, Leicester LE1 7RH (telephone: 0116 252 3406, email: S.Ambler@mcs.le.ac.uk). The closing date for applications is 1st May 1999. ---------------------------------------------------------------------- From cat-dist Tue Mar 2 21:12:54 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA14689 for categories-list; Tue, 2 Mar 1999 20:17:27 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Karel Stokkermans Date: Tue, 2 Mar 1999 13:55:11 +0100 (MET) Message-Id: <199903021255.NAA29041@lemur.cosy.sbg.ac.at> To: categories@mta.ca Subject: categories: geometric formulae and axioms Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear category theorists, Recently I came across geometric formulae (built up from atomic formulae using only conjunction, disjunction and existential quantification). I would know like to know whether there is any way to decide whether an arbitrary given first order formula is (classically) equivalent to a geometric formula (or geometric axiom: phi -> psi where phi and psi are both geometric formulae). I've looked in the book by Mac Lane and Moerdijk but didn't discover a general decision method. Any hints or references to relevant literature would be much appreciated. Best regards, Karel Stokkermans From cat-dist Wed Mar 3 19:35:40 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id SAA02291 for categories-list; Wed, 3 Mar 1999 18:39:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 3 Mar 1999 12:33:12 -0500 (EST) From: F W Lawvere Reply-To: wlawvere@ACSU.Buffalo.EDU To: Karel Stokkermans cc: categories@mta.ca Subject: categories: Re: geometric formulae and axioms In-Reply-To: <199903021255.NAA29041@lemur.cosy.sbg.ac.at> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Yes, this question is disussed in Kieslers' paper on "Generalized Atomic Formulas" from the early 1960s. The third name , which I prefer, for the class is simply "positive" formulas. They are of course a key tool in the Presentations of a Positive Theory. This may not agree exactly with some previous uses of the term "positive", since the not-so-innocuous use of universal prefixes has been eliminated along with the excessive burden that had been put on the single element "TRUE"; the presentation machinery for positive theories must involve a BINARY relation of entailment (for each admitted arity of formula) in place of the single 0-ary relation of provability. This is actually a simplication rather than a complication although that may not have been clear in the 1930s As far as expressive power is concerned, one can say that for Boolean models (as opposed to models in more general toposes) positive theories are as general as what have been called "standard presentation first order theories" : Any particular negation occurring in a presentation of one of the latter can be replaced by a new primitive relation symbol, nailed to what it is to negate by the usual pair of lattice (hence positive) new axioms. The geometric role of positive theories is that via the classifying-topos construction they provide a standard way to geometrically visualize models of arbitrary theories via the algebraic-geometry paridigm (ie via the body of mathematics created by Kan, Isbell, Grothendieck, and Yoneda in the decade 1954-1964). Of course, one of the theories which most interested the model theory pioneers Birkhoff, Robinson, and Tarski was the theory of commutative rings, so this extension may seem as natural to us as it did to them. Kiesler's paper shows us that the explicit relation between positivity and preservation under morphisms was recognized clearly quite a long time ago. Are there papers which also draw the conclusion that the "standard" theories and presentations should really be the positive ones, with negation as a cared-for particular rather than a blanket general ? Whether the possibility of recursive presentability of a given mathematical concept might vary under this change is not clear to me.(Of course "quantifier elimination" in some cases changes to an exceptional "quantifier definability"). Also, the original question concerning whether (for example) the inclusion, of a positive theory into the associated theory in the doctrine which has negation and universal quantifiers, is itself recursive qua inclusion, probably has a negative answer, but I don't have a reference. Bill ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA ******************************************************************************* On Tue, 2 Mar 1999, Karel Stokkermans wrote: > Dear category theorists, > > Recently I came across geometric formulae (built up from atomic formulae > using only conjunction, disjunction and existential quantification). I > would know like to know whether there is any way to decide whether an > arbitrary given first order formula is (classically) equivalent to a > geometric formula (or geometric axiom: phi -> psi where phi and psi are > both geometric formulae). I've looked in the book by Mac Lane and Moerdijk > but didn't discover a general decision method. Any hints or references > to relevant literature would be much appreciated. > > Best regards, > Karel Stokkermans > > From cat-dist Thu Mar 4 21:27:08 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA09787 for categories-list; Thu, 4 Mar 1999 20:21:11 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 4 Mar 1999 10:00:37 +0100 (MET) From: Natalia Ioustinova Message-Id: <199903040900.KAA20773@mammut.informatik.uni-rostock.de> To: categories@mta.ca Subject: categories: OOSDS99 Call for papers Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ======================================================================== This message contains public information, only, and the receiver is allowed, and invited, to copy it and distribute it further. Our apologies if you received duplicates of this message due to the mailing list aliases. You can also visit the OOSDS'99 web site at http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ======================================================================== CALL FOR PAPERS OOSDS'99 Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours Paris, France, September 27, 1999 http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ======================================================================== SCOPE OF WORKSHOP: ================= The workshop is focused on specification languages for distributed systems which are extensions of object-oriented languages or have an object-oriented kind of base structure. The aim is to bring together researchers interested in incorporating object-oriented concepts and formal methods for specification of distributed systems and behaviours. TOPICS (NOT EXCLUSIVE LIST): ============================ Object-oriented approaches to specification of distributed systems and behaviours. Semantic models for concurrency and object-orientation (e.g. based on the lambda-calculus, process algebra, pi-calculus, linear logic). Characteristic examples of object-oriented specification from real application domains (e.g. distributed algorithms, workflow specification, communication protocols). Logic reasoning on distributed systems and behaviours. SUBMISSION: =========== The deadline for submission is September 2, 1999. Submission is in electronic form only. Submission may be of two forms: Extended abstracts: up to 3 pages. Papers and reports: up to 6 pages. In both cases a separate page with the following information: title, author(s), corresponding author, contact information and a 12-15 lines summary should be included. The papers and/or abstracts should be sent by e-mail to ustin@informatik.uni-rostock.de. Selection for presentation will be carried out by the organizers. Emphasis is put on the potential of the submission to stimulate discussions in the above-mentioned scope. Notification of acceptance is expected for September 14, 1999. PUBLICATION: ============ The accepted submissions will be published electronically, i.e. they will remain available from the workshop web page. Furthermore, selected papers will be invited for post workshop publication. RELATED EVENTS: ============== This workshop is organized as a satellite workshop of PPDP'99, The 1999 International Conference on Principles and Practice of Declarative Programming, Paris, France, September 29-October 1, 1999. http://www.dmi.ens.fr/~fages/PPDP99/ ORGANIZATION COMMITTEE: ======================= Clemens H. Cap (Rostock University, Germany) Natalia Ioustinova (Rostock University, Germany) Javier Oliver (Technical University of Valencia, Spain) Nobuko Yoshida (University of Sussex, UK) ADDITIONAL INFORMATION: ======================= WEB: http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ MAIL: ustin@informatik.uni-rostock.de >From ustin Thu Mar 4 09:48:06 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, acclaim@sics.se, cat, echo, for, papers, sleep, to, ustin@informatik.uni-rostock.de, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:48:16 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, afp@cs.chalmers.se, alp-diffusion@univ-lille1.fr, cat, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:48:26 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, alp-list@intellektik.informatik.th-darmstadt.de, benelog@cs.kuleuven.ac.be, cat, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:48:36 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, categories@mta.ca, cav-all@csa.cs.technion.ac.il, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:48:47 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, ccl@dfki.de, ccp@sics.se, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:48:57 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, choose-news@iam.unibe.ch, clp@comp.nus.edu.sg, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:49:07 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, compulog-deduction@cs.bham.ac.uk, compulog-list@cwi.nl, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:49:17 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, compunode@compulog.org, compunode@dfki.de, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 >From ustin Thu Mar 4 09:49:27 1999 To: -s, 5, Call, Mail, OOSDS99, Sent, cat, concurrency@cwi.nl, conferences@iao.fhg.de, echo, for, papers, sleep, to, | Subject: OOSDS99 Content-Length: 0 From cat-dist Thu Mar 4 21:27:22 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA10467 for categories-list; Thu, 4 Mar 1999 20:22:16 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 4 Mar 1999 09:29:42 +0100 (MET) From: "tlca99.aquila" Message-Id: <199903040829.JAA01231@univaq.it> To: categories@mta.ca Subject: categories: TLCA'99 (Second Call for Participation) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: - Our apologies if you receive multiple copies of this message - ---------------------------------------------------------------------------- | Note the early registration and accommodation deadline: MARCH 7th, 1999. | ---------------------------------------------------------------------------- ---------------------------------------------- | | | TLCA '99 | | | | Fourth International Conference on | | Typed Lambda Calculi and Applications | | | | April 7-9, 1999, L'Aquila (Italy) | | | ---------------------------------------------- You can find the preliminary schedule and all information about the conference venue, conference registration and hotel accommodation at the TLCA '99 web site: http://w3.dm.univaq.it/tlca99 For any further information, please contact the TLCA '99 Organizing Committee at the email address: tlca99.aquila@univaq.it ----------------------------------------------------------- Organizing Committee Chairman: Benedetto Intrigila Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di L'Aquila via Vetoio, Loc. Coppito 67100 L'Aquila Italy fax: (+)-39-0862-433180 e-mail: tlca99.aquila@univaq.it home page: http://w3.dm.univaq.it/tlca99 ----------------------------------------------------------- From cat-dist Sat Mar 6 18:49:38 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id RAA20093 for categories-list; Sat, 6 Mar 1999 17:49:21 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Sender: sjv@pop.doc.ic.ac.uk Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Fri, 5 Mar 1999 10:15:45 +0000 To: categories@mta.ca From: s.vickers@doc.ic.ac.uk (Steven Vickers) Subject: categories: Re: geometric formulae and axioms Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: >Dear category theorists, > >Recently I came across geometric formulae (built up from atomic formulae >using only conjunction, disjunction and existential quantification). I >would know like to know whether there is any way to decide whether an >arbitrary given first order formula is (classically) equivalent to a >geometric formula (or geometric axiom: phi -> psi where phi and psi are >both geometric formulae). I've looked in the book by Mac Lane and Moerdijk >but didn't discover a general decision method. Any hints or references >to relevant literature would be much appreciated. > >Best regards, >Karel Stokkermans For myself, the short answer is I don't know. Perhaps I ought to, since I've made lots of geometric theries out of classical ones, but in practice the problem goes further than a strict answer to the question would provide. One often needs not just to transform the theories within a fixed language but to tranform the language itself. A simple example is negation as "cared-for particular" to use Bill's phrase. It is especially true once one starts using the full geometric logic, with infinitary disjunctions (unlike the coherent logic in Mac Lane and Moerdijk). One then sees, for instance, that geometric logic is actually weak second order, with universal quantification bounded over finite sets. Steve Vickers. http://www.doc.ic.ac.uk/~sjv/ From cat-dist Sat Mar 6 18:50:35 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id RAA20025 for categories-list; Sat, 6 Mar 1999 17:50:26 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from callisto.acsu.buffalo.edu (qmailr@callisto.acsu.buffalo.edu [128.205.7.122]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id MAA00063 for ; Fri, 5 Mar 1999 12:53:16 -0400 (AST) X-Received: (qmail 3663 invoked by uid 39883); 5 Mar 1999 16:53:17 -0000 Date: Fri, 5 Mar 1999 11:53:17 -0500 (EST) From: F W Lawvere Reply-To: wlawvere@ACSU.Buffalo.EDU To: categories Subject: categories: AMS Buffalo, April 24/25 Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: THIRD ANNOUNCEMENT SMOOTH CATEGORIES IN GEOMETRY AND MECHANICS Special session of AMS Meeting No. 943 in Buffalo, N.Y. April 24/25, 1999 Abstracts are accessible via Http://www.ams.org./meetings/ SCHEDULE: Saturday, April 24, 1999 9:00 - 9:20 James FARAN: A Synthetic Approach to Characteristic Cohomology (Abstract # 943-18-72) 9:30 - 9:50 Hirokazu NISHIMURA: Infinitesimal Calculus of Variations (Abstract # 943-18-71) 10:00 - 10:20 Jonathon FUNK: Lebesgue Toposes (Abstract # 943-18-65) 10:30 - 10:50 George JANELIDZE: (joint work with Walter Tholen) Strongly Separable Morphisms (Abstract # 943-18-73) *** 2:30 - 2:50 Gonzalo REYES: (joint work with Anders Kock) Atoms and Categories of Differential Equations in SDG (Abstract # 943-18-109) 3:00 - 3:20 Felipe GAGO: Transversal Stability for Infinitesimally Represented Germs (Abstract # 943-18-66) 3:30 - 3:50 Anders KOCK: Infinitesimal Geometric Aspects of Riemannian Metrics (Abstract # 943-18-109) *** 4:30 - 4:50 Rene LAVENDHOMME: Infinitesimal Deformations in SDG (Abstract # 943-18-70) 5:00 - 5:20 Marta BUNGE: Single Universe for Intensive and Extensive Quantities in a Topos (Abstract # 943-18-76) Sunday, April 25, 1999 9:00 - 9:20 Peter FREYD: Arithmetic Categories (Abstract # 943-18-69) 9:30 - 9:50 Ali MADANSHEKAF: The Automorphism Group of the First-Order Infinitesimals (Abstract # 943-18-32) 10:00 -10:20 David WRAY: The Existence of Localised Quanta at Spatial Infinity: How Sheaves Replace Heisenberg (Abstract # 943-18-92) 10:30 - 10:50 Craig SNYDAL: Vertex Algebras, an Example of a Relaxed Multilinear Category (Abstract # 943-18-67) *** 2:30 - 2:50 Walter NOLL: Isocategories in Continuum Physics 3:00 - 3:20 Bill LAWVERE Smoothness of Cubical Splines (Abstract # 943-18-145) ALL SESSIONS AND TALKS WILL TAKE PLACE IN DIEFENDORF HALL AT THE MAIN STREET CAMPUS. ****************************************************************** ARRIVAL DATE: Friday, April 23, 1999 ACCOMODATIONS: For the participants of the meeting the downtown HYATT REGENCY BUFFALO has special rates. For more information about hotels, etc. see Http://www.acsu.buffalo.edu/~jjfaran/AMS_MEETING_home.html A block of rooms under the name AMS SMOOTH CATEGORIES has been reserved at the UNIVERSITY MANOR, near the intersection of Main Street and Bailey Avenue, at walking distance from the Mathematics Department (Diefendorf Hall) where the Sessions will be held. Prices are: Queen US$ 50.--/ King or 2 beds US$ 54.--, minus 10% for participants, plus 13% tax. Tel. (716) 837-3344; Fax (716)834-6246 Reservations should be made directly as early as possible! REGISTRATION: Room 114, Diefendorf Hall Fees are $ 30.--/AMS or CMS members, $ 45.-- /nonmembers, $ 10.-- emeritus members, students, unemployed mathematicians, (payable on-site only) ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA ******************************************************************************* From cat-dist Mon Mar 8 12:07:59 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA14281 for categories-list; Mon, 8 Mar 1999 09:07:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from callisto.acsu.buffalo.edu (qmailr@callisto.acsu.buffalo.edu [128.205.7.122]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id SAA26739 for ; Sun, 7 Mar 1999 18:37:53 -0400 (AST) X-Received: (qmail 4073 invoked by uid 39883); 7 Mar 1999 22:37:54 -0000 Date: Sun, 7 Mar 1999 17:37:54 -0500 (EST) From: F W Lawvere Reply-To: wlawvere@ACSU.Buffalo.EDU To: categories Subject: categories: AMS Buffalo, revised Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: PLEASE NOTE: There is an error in our announcement of March 5th: The abstract number for Anders Kock's paper should be Abstract # 943-18-68 (not 943-18-109). Here is the revised version. THIRD ANNOUNCEMENT SMOOTH CATEGORIES IN GEOMETRY AND MECHANICS Special session of AMS Meeting No. 943 in Buffalo, N.Y. April 24/25, 1999 Abstracts are accessible via Http://www.ams.org./meetings/ SCHEDULE: Saturday, April 24, 1999 9:00 - 9:20 James FARAN: A Synthetic Approach to Characteristic Cohomology (Abstract # 943-18-72) 9:30 - 9:50 Hirokazu NISHIMURA: Infinitesimal Calculus of Variations (Abstract # 943-18-71) 10:00 - 10:20 Jonathon FUNK: Lebesgue Toposes (Abstract # 943-18-65) 10:30 - 10:50 George JANELIDZE: (joint work with Walter Tholen) Strongly Separable Morphisms (Abstract # 943-18-73) *** 2:30 - 2:50 Gonzalo REYES: (joint work with Anders Kock) Atoms and Categories of Differential Equations in SDG (Abstract # 943-18-109) 3:00 - 3:20 Felipe GAGO: Transversal Stability for Infinitesimally Represented Germs (Abstract # 943-18-66) 3:30 - 3:50 Anders KOCK: Infinitesimal Geometric Aspects of Riemannian Metrics (Abstract # 943-18-68) *** 4:30 - 4:50 Rene LAVENDHOMME: Infinitesimal Deformations in SDG (Abstract # 943-18-70) 5:00 - 5:20 Marta BUNGE: Single Universe for Intensive and Extensive Quantities in a Topos (Abstract # 943-18-76) Sunday, April 25, 1999 9:00 - 9:20 Peter FREYD: Arithmetic Categories (Abstract # 943-18-69) 9:30 - 9:50 Ali MADANSHEKAF: The Automorphism Group of the First-Order Infinitesimals (Abstract # 943-18-32) 10:00 -10:20 David WRAY: The Existence of Localised Quanta at Spatial Infinity: How Sheaves Replace Heisenberg (Abstract # 943-18-92) 10:30 - 10:50 Craig SNYDAL: Vertex Algebras, an Example of a Relaxed Multilinear Category (Abstract # 943-18-67) *** 2:30 - 2:50 Walter NOLL: Isocategories in Continuum Physics 3:00 - 3:20 Bill LAWVERE Smoothness of Cubical Splines (Abstract # 943-18-145) ALL SESSIONS AND TALKS WILL TAKE PLACE IN DIEFENDORF HALL AT THE MAIN STREET CAMPUS. ****************************************************************** ARRIVAL DATE: Friday, April 23, 1999 ACCOMODATIONS: For the participants of the meeting the downtown HYATT REGENCY BUFFALO has special rates. For more information about hotels, etc. see Http://www.acsu.buffalo.edu/~jjfaran/AMS_MEETING_home.html A block of rooms under the name AMS SMOOTH CATEGORIES has been reserved at the UNIVERSITY MANOR, near the intersection of Main Street and Bailey Avenue, at walking distance from the Mathematics Department (Diefendorf Hall) where the Sessions will be held. Prices are: Queen US$ 50.--/ King or 2 beds US$ 54.--, minus 10% for participants, plus 13% tax. Tel. (716) 837-3344; Fax (716)834-6246 Reservations should be made directly as early as possible! REGISTRATION: Room 114, Diefendorf Hall Fees are $ 30.--/AMS or CMS members, $ 45.-- /nonmembers, $ 10.-- emeritus members, students, unemployed mathematicians, (payable on-site only) ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA ******************************************************************************* From cat-dist Mon Mar 8 12:58:58 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA18230 for categories-list; Mon, 8 Mar 1999 09:08:42 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 08 Mar 1999 11:53:22 +0100 From: Eva Ullan Subject: categories: Computer Science Logic Conference (CSL'99) X-Sender: evah@147.96.1.121 To: csl99org@eucmos.sim.ucm.es Message-id: MIME-version: 1.0 Content-type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id HAA10156 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ____________________________________________________ My apologies if you receive this more than once! ____________________________________________________ ******************************************************** **** D E A D L I N E March 19, 1999 **** ******************************************************** ------------------------------------------------------------- LAST CALL FOR PAPERS -- CSL'99 Annual Conference of the European Association for Computer Science Logic September 20-25, 1999, Madrid, Spain ------------------------------------------------------------- CSL is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested, but not exclusive, topics of interest include: * abstract datatypes, * automated deduction, * categorical and topological approaches, * concurrency theory, * constructive mathematics, * database theory, * domain theory, * finite model theory, * lambda and combinatory calculi, * logical aspects of computational complexity, * logical foundations of programming paradigms, * linear logic, * modal and temporal logics, * model checking, * program logics and semantics, * program specification, transformation and verification, * rewriting, * symbolic computation. PROGRAM COMMITEE Samson Abramsky (Edinburgh, UK) Marc Bezem (Utrecht, The Netherlands) Peter Clote (Munich, Germany) Hubert Comon (Cachan, France) Jorg Flum (Freiburg i.Br., Germany) (co-chair) Harald Ganzinger (Saarbrucken, Germany) Neil Immerman (Amherst, USA) Neil Jones (Copenhagen, Denmark) Jan Maluszynski (Linkoping, Sweden) Michael Maher (Brisbane, Australia) Catuscia Palamidessi (Pennsylvania, USA) Mario Rodriguez-Artalejo (Madrid, Spain) (co-chair) Wolfgang Thomas (Aachen, Germany) Jerzy Tiuryn (Warsaw, Poland) Glynn Winskel (Aarhus, Denmark) Martin Wirsing (Munich, Germany) SCIENTIFIC PROGRAMME In addition to invited lectures and contributed papers, there will be two tutorials on theorem proving and rewriting techniques, scheduled on September 24 afternoon (Friday) and September 25 morning (Saturday), immediately after the main conference. ** September 20--24, 1999: Invited Lectures and Contributed Papers The list of invited speakers will include: Jose Luis Balcazar (Barcelona, Spain) Javier Esparza (Munich, Germany) Martin Grohe (Freiburg, Germany) Peter D. Mosses (Aarhus, Denmark) V. Vianu (San Diego, USA) ** September 24--25, 1999: CSL Tutorials Douglas Howe (Bell Labs, USA) Aart Middeldorp (Tsukuba, Japan) LOCAL ORGANIZING COMMITTEE J. Carlos Gonzalez-Moreno Teresa Hortala-Gonzalez Javier Leach-Albert (chair) Paco Lopez-Fraguas Fernando Saenz-Perez Eva Ullan EACSL BOARD Marc Bezem (Utrecht, President) Ian Stewart (Leicester, Vice-President) Clemens Lautemann (Mainz, Treasurer) Peter Hajek (Prague) Simone Martini (Udine) Christine Paulin (Paris) Moshe Vardi (Houston) Johann Makowsky (Haifa) Alexander Razborov (Moscow) EACSL homepage: http://www.dimi.uniud.it/~eacsl IMPORTANT DATES Paper submissions March 19, 1999 Notifications of acceptance May 31, 1999 Final version due: July 12, 1999 CSL'99 main conference September 20-24, 1999 CSL'99 Tutorials September 24-25, 1999 PAPER SUBMISSIONS Submitted papers must be written in English and describe work not previously published. They must not be submitted concurrently to a journal or to another conference. Papers authored or coauthored by members of the Program Committee are not allowed. Submissions must not exceed 15 pages, including title page, figures, and references. The title page must contain: title and authors; physical and e-mail addresses; telephone and (if available) fax number for each author; identification of corresponding author, if not the first author; an abstract of no more than 200 words; a list of keywords. Submissions must arrive by March 19, 1999, and notifications of acceptance will be sent by May 31, 1999. Authors are invited to send manuscripts by electronic mail, as uuencoded gzipped postcript files: * see the conference home page for instructions http://mozart.sip.ucm.es:1580/csl99 * or send an empty message with subject "submission information'' to csl99org@eucmos.sim.ucm.es Those authors without access to the facilities for electronic submission can alternatively submit five hardcopies to: Prof. Mario Rodriguez Artalejo, CSL'99 Departamento de Sistemas Informaticos y Programacion Facultad de Matematicas, Universidad Complutense de Madrid Av. Complutense s/n E-28040 Madrid Spain E-mail: mario@sip.ucm.es Phone: +34 91 3 94 45 12 Fax: +34 91 3 94 46 07 PUBLICATION Papers accepted by the Program Committee must be presented at the conference and will appear in a proceedings volume, to be published by Springer Verlag in the "Lecture Notes in Computer Science" series. The second refereeing round which was requested in previous CSL editions before accepting a paper for publication in the proceedings, has been suppressed following the decision taken by the EACSL membership meeting held during CSL'98 (Brno, Czech Republic, August 25th 1998). Final versions of accepted papers will be due by July 12, 1999. The format for camera-ready manuscripts will be that of Springer LNCS; instructions can be found in the LNCS home page at: http://www.springer.de/comp/lncs/index.html ADDITIONAL INFORMATION CSL'99 home page: http://mozart.sip.ucm.es:1580/csl99 CSL'99 local organization: csl99org@eucmos.sim.ucm.es %%%%%%%%%%%%%%%%%%%%%% LATEX VERSION %%%%%%%%%%%%%% % Last Call for Papers, CSL'99. % Last revision: March 8, 1999 \documentstyle{article} \oddsidemargin 6pt \evensidemargin 6pt \marginparwidth 90pt \marginparsep 10pt \topmargin -30pt \headheight 12pt \headsep 25pt \footheight 12pt \footskip 30pt \columnsep 10.5pt \columnseprule 0pt \addtolength{\oddsidemargin}{-2.3cm} \setlength{\textwidth}{20cm} %{18.7cm} \addtolength{\topmargin}{-1cm} \setlength{\textheight}{27cm} \pagestyle{empty} \begin{document} % Heading \begin{center} {\large \bf LAST CALL FOR PAPERS -- CSL'99} \end{center} \begin{center} {\Large \bf Annual Conference of the }\\[1.5ex] {\Large \bf European Association for Computer Science Logic} \end{center} \begin{center} {\large \bf Madrid, Spain, September 20-25, 1999} \end{center} \vspace*{0.15in} % Left column \parbox[t]{6.5cm}{%6.3cm \footnotesize \noindent {\bf Program Committee:} \vspace*{0.05in} \begin{tabular}{l} Samson Abramsky (Edinburgh, UK)\\ Marc Bezem (Utrecht, The Netherlands)\\ Peter Clote (Munich, Germany)\\ Hubert Comon (Cachan, France)\\ J\"{o}rg Flum (Freiburg i.Br., Germany) \\ \hspace{1cm} ({\bf co-chair})\\ Harald Ganzinger (Saarbr\"{u}cken, Germany)\\ Neil Immerman (Amherst, USA)\\ Neil Jones (Copenhagen, Denmark)\\ Jan Maluszynski (Link\"{o}ping, Sweden)\\ Michael Maher (Brisbane, Australia)\\ Catuscia Palamidessi (Pennsylvania, USA)\\ Mario Rodr\'{\i}guez-Artalejo (Madrid, Spain) \\ \hspace{1cm} ({\bf co-chair})\\ Wolfgang Thomas (Aachen, Germany)\\ Jerzy Tiuryn (Warsaw, Poland)\\ Glynn Winskel (Aarhus, Denmark)\\ Martin Wirsing (Munich, Germany)\\ \end{tabular} \vspace*{0.10in} \noindent {\bf Invited Speakers:} \vspace*{0.05in} \begin{tabular}{l} Jos\'{e} Luis Balc\'{a}zar (Barcelona, Spain)\\ Javier Esparza (Munich, Germany)\\ Martin Grohe (Freiburg, Germany)\\ Peter D. Mosses (Aarhus, Denmark)\\ V. Vianu (San Diego, USA) \end{tabular} \vspace*{0.10in} \noindent {\bf Tutorialists:} \vspace*{0.05in} \begin{tabular}{l} Douglas Howe (Bell Labs, USA)\\ Aart Middeldorp (Tsukuba, Japan) \end{tabular} \vspace*{0.10in} \noindent {\bf Local Organizing Committee:} \vspace*{0.05in} \begin{tabular}{l} J. Carlos Gonz\'{a}lez-Moreno\\ Teresa Hortal\'{a}-Gonz\'{a}lez\\ Javier Leach-Albert ({\bf chair})\\ Paco L\'{o}pez-Fraguas\\ Fernando S\'{a}enz-P\'{e}rez\\ Eva Ull\'{a}n \end{tabular} \vspace*{0.10in} \noindent {\bf EACSL Board:} \vspace*{0.05in} \begin{tabular}{l} Marc Bezem (Utrecht, President)\\ Ian Stewart (Leicester, Vice-President)\\ Clemens Lautemann (Mainz, Treasurer)\\ Peter Hajek (Prague)\\ Simone Martini (Udine)\\ Christine Paulin (Paris)\\ Moshe Vardi (Houston)\\ Johann Makowsky (Haifa)\\ Alexander Razborov (Moscow)\\ \end{tabular} \vspace*{0.15in} \noindent {\bf EACSL homepage:} \vspace*{0.05in} \begin{tabular}{l} http://www.dimi.uniud.it/\~{}eacsl \end{tabular} \vspace*{0.15in} \noindent {\bf Important Dates:} \vspace*{0.05in} \begin{tabular}{l} Paper submissions: \\ ~~~~ March 19, 1999 \\ Notifications of acceptance: \\ ~~~~ May 31, 1999 \\ Final version due: \\ ~~~~ July 12, 1999 \\ CSL'99 main conference: \\ ~~~~ September 20-24, 1999 \\ CSL'99 Tutorials: \\ ~~~~ September 24-25, 1999 \end{tabular} } % \end{parbox} % Right column. No blank line here! \parbox[t]{5mm}{ \rule[-22.0cm]{0.2mm}{22.5cm} } %\end{parbox} \begin{minipage}[t]{11.0cm}%{11.5cm} \small {\bf Aims and Scope of the Conference:} {\bf CSL} is the annual conference of the {\em European Association for Computer Science Logic} (EACSL). The conference is intended for computer scientistswhose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested, but not exclusive, topics of interest include: abstract datatypes, automated deduction, categorical and topological approaches, concurrency theory, constructive mathematics, database theory, domain theory, finite model theory, lambda and combinatory calculi, logical aspects of computational complexity, logical foundations of programming paradigms, linear logic, modal and temporal logics, model checking, program logics and semantics, program specification, transformation and verification, rewriting, symbolic computation. \vspace*{0.12in} \noindent {\bf Scientific Programme:} In addition to invited lectures and contributed papers, there will be two tutorials on theorem proving and rewriting techniques, scheduled on September 24 afternoon (Friday) and September 25 morning (Saturday), immediately after the main conference. \vspace*{0.12in} \noindent {\bf Paper Submissions:} Submitted papers must be written in English and describe work not previously published. They must not be submitted concurrently to a journal or to another conference. Papers authored or co-authored by members of the Program Committee are not allowed. Submissions must not exceed 15 pages, including title page, figures, and references. The title page must contain: title and authors; physical and e-mail addresses; telephone and (if available) fax number for each author; identification of corresponding author, if not the first author; an abstract of no more than 200 words; a list of keywords. Submissions must arrive by {\bf March 19, 1999}, and notifications of acceptance will be sent by {\bf May 31, 1999}. Authors are invited to send manuscripts by electronic mail, as uuencoded gzipped postcript files (see the conference home page for instructions, or send an empty message with subject ``submission information'' to csl99org@eucmos.sim.ucm.es). Those authors without access to the facilities for electronic submission can alternatively submit {\em five hardcopies} to: \vspace*{0.05in} \begin{tabular}{l} Prof. Mario Rodr\'{\i}guez-Artalejo, CSL'99 \\ Departamento de Sistemas Inform\'{a}ticos y Programaci\'{o}n \\ Facultad de Matem\'{a}ticas, Universidad Complutense de Madrid \\ Av. Complutense s/n ~~~~~~~~~~ Phone: +34 91 3 94 45 12 \\ E-28040 Madrid ~~~~~~~~~~~~~~~~~ Fax: +34 91 3 94 46 07 \\ Spain ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ E-mail: mario@sip.ucm.es \end{tabular} \vspace*{0.12in} \noindent {\bf Publication:} Papers accepted by the Program Committee must be presented at the conference and {\bf will appear in a proceedings volume}, to be published by Springer Verlag in the ``Lecture Notes in Computer Science'' series. The second refereeing round which was requested in previous CSL editions before accepting a paper for publication in the proceedings, has been suppressed following the decision taken by the EACSL membership meeting held during CSL'98 (Brno, Czech Republic, August 25th 1998). Final versions of accepted papers will be due by {\bf July 12, 1999}. The format for camera-ready manuscripts will be that of Springer LNCS; instructions can be found in the LNCS home page at http://www.springer.de/comp/lncs/index.html. \vspace*{0.12in} \noindent {\bf Important Remark:} The proceedings volume will be available at the conference. In order to enable this, the deadlines for paper submission and notification of acceptance have been slightly modified w.r.t. the announcement made in the 1st call for papers. \vspace*{0.15in} \noindent {\bf Additional Information:} \vspace*{0.05in} \begin{tabular}{ll} CSL'99 home page: & http://mozart.sip.ucm.es:1580/csl99 \\ CSL'99 local organization: & E-mail: csl99org@eucmos.sim.ucm.es \end{tabular} \end{minipage} \end{document} From cat-dist Mon Mar 8 20:14:28 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA22969 for categories-list; Mon, 8 Mar 1999 19:21:54 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 8 Mar 1999 17:54:20 -0500 (EST) From: Andreas Blass Reply-To: Andreas Blass To: categories@mta.ca Subject: categories: geometric formulas Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Karel Stokkermans asked about a decision procedure for checking whether an arbitrary given first-order formula is classically equivalent to a geometric one. There is no such algorithm. The reason is that any such algorithm could easily be converted into an algorithm for testing (classical, first-order) validity, which is well-known to be undecidable. To test a formula A for validity, take a 0-ary predicate symbol P that doesn't occur in A, and let A' be the formula "A or not P". Then A' is equivalent to a geometric formula (namely "true") if and only if A is valid. So just test A' for geometricity and you'll know whether A is valid. (If, like some textbook authors, you don't believe in 0-ary predicate symbols, use P(x) instead, where P is unary.) Bill Lawvere asked whether there are "papers which also draw the conclusion that the 'standard' theories and presentations should really be positive ones, with negation as a cared-for particular rather than a blanket general". I assume he means papers where this is done for a purpose other than having geometric theories or the nice things that come with them, like classifying topoi. In a paper that Yuri Gurevich and I wrote long ago ["Existential fixed-point logic" in "Computation Theory and Logic", edited by Egon Boerger, Springer Lecture Notes in Comp. Sci. 270 (1987) pp.20-36], we found it convenient to adopt the following convention, which though not quite what Bill described, is similar in spirit: A first-order language (or signature or similarity-type) should have its predicate symbols classified into two sorts, positive and negatable. Negation can be applied only to atomic formulas whose predicate symbol is negatable. Homomorphisms are required to preserve the interpretations of all predicate symbols and to reflect the interpretations of the negatable ones. Andreas Blass From cat-dist Tue Mar 9 16:23:10 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA29660 for categories-list; Tue, 9 Mar 1999 14:03:02 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 9 Mar 1999 10:17:18 -0500 (EST) From: James Stasheff To: categories@mta.ca Subject: categories: Quantum vertex algebras Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: 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@math.upenn.edu 146 Woodland Dr Lansdale PA 19446 (215)822-6707 Jim Stasheff jds@math.unc.edu Math-UNC (919)-962-9607 Chapel Hill NC FAX:(919)-962-2568 27599-3250 From cat-dist Thu Mar 11 15:49:21 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA14192 for categories-list; Thu, 11 Mar 1999 13:06:54 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 11 Mar 1999 14:20:07 +0000 (GMT) From: Anne Heyworth X-Sender: map130@publix To: categories@mta.ca Subject: categories: Rewrite Methods for Kan Extensions of Actions of Categories Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: 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 From cat-dist Thu Mar 11 21:32:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA30544 for categories-list; Thu, 11 Mar 1999 20:49:24 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 10 Mar 1999 14:29:03 +0800 (CST) From: farn@iis.sinica.edu.tw (Farn Wang) Message-Id: <199903100629.OAA24756@ccs1.iis.sinica.edu.tw> To: categories@mta.ca Subject: categories: Report on verification of unknown number of processes Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: 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. From cat-dist Sat Mar 13 11:23:57 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA26225 for categories-list; Sat, 13 Mar 1999 10:28:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Subject: categories: BCTCS 15 Content-Type: text Message-Id: From: "John G. Stell" To: categories@mta.ca Date: Sat, 13 Mar 1999 12:19:17 +0000 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: 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@cs.keele.ac.uk or at: Department of Computer Science, Keele University, Keele, Staffs, U. K., ST5 5BG. ___________________________________________________________________________ From cat-dist Sat Mar 13 11:23:59 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA26407 for categories-list; Sat, 13 Mar 1999 10:26:26 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.19990312230448.0094d330@ichthus.syr.edu> X-Sender: gaunce@ichthus.syr.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Fri, 12 Mar 1999 23:10:26 -0500 To: categories@mta.ca From: Gaunce Lewis Subject: categories: lax monad Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: 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 From cat-dist Sun Mar 14 21:52:03 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA11456 for categories-list; Sun, 14 Mar 1999 20:30:29 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199903142238.JAA04945@hera.mpce.mq.edu.au> X-Sender: street@hera.mpce.mq.edu.au Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Mon, 15 Mar 1999 09:39:21 +1000 To: categories@mta.ca From: street@mpce.mq.edu.au (Ross Street) Subject: categories: Re: lax monad Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: >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? Some good old references are: M. Barr "Relational algebras" SLNM 137 (1970) 39-55 M. Bunge, "Coherent extensions and relational algebras" Transactions AMS around 1974. G.M. Kelly & R. Street, "Review of the elements of 2-categories" SLNM 420 (1974) 75-103. --Ross From cat-dist Tue Mar 16 13:05:41 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA28416 for categories-list; Tue, 16 Mar 1999 10:19:03 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 16 Mar 1999 10:06:40 GMT From: Marta Z Kwiatkowska Message-Id: <199903161006.KAA03824@chip.cs.bham.ac.uk> To: categories@mta.ca Subject: categories: Research scholarships available at Birmingham X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: 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}@cs.bham.ac.uk u-reddy@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 From cat-dist Wed Mar 17 14:35:08 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA06946 for categories-list; Wed, 17 Mar 1999 11:48:30 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <36EFC92A.6C34DC4B@loria.fr> Date: Wed, 17 Mar 1999 16:24:26 +0100 From: Francois Lamarche Organization: LORIA X-Mailer: Mozilla 4.5 [en] (X11; I; SunOS 5.5 sun4m) X-Accept-Language: fr, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Monoidal structure on graphs Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: 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 From cat-dist Thu Mar 18 12:44:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA20914 for categories-list; Thu, 18 Mar 1999 08:49:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <36F0E6ED.7EF7BB45@loria.fr> Date: Thu, 18 Mar 1999 12:43:41 +0100 From: Francois Lamarche Organization: LORIA X-Mailer: Mozilla 4.5 [en] (X11; I; SunOS 5.5 sun4m) X-Accept-Language: fr, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Monoidal structure, take II Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: 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 From cat-dist Thu Mar 18 12:44:20 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA18822 for categories-list; Thu, 18 Mar 1999 08:48:14 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: Re: Monoidal structure on graphs Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-MD5: rUxkjrwDZJdVdKTrk48DUA== Message-Id: From: "John G. Stell" Date: Thu, 18 Mar 1999 10:55:08 +0000 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: A structure closely related to the one which Francois Lamarche asked about appeared in my thesis (1992) [see below] as a simple example of a sesqui-category which is not a 2-category. I too would expect it's appeared elsewhere, but I don't know where. John Stell \subsubsection{An Example of a Sesqui-Category} We include an example to show that there are naturally occurring sesqui-categories other than in connection with modelling term rewriting. The underlying category is {\bf Graph}. Suppose there are graphs $G$ and $H$, and graph morphisms $g,h : G \rightarrow H$. In this situation, the 2-cells $\alpha : g \rightarrow h$ are assignments to each node $n$ of $G$ of a path of edges from $ng$ to $nh$ in $H$. The compositions $\circ_R$ and $\circ_L$ are readily defined. If $f : F \rightarrow G$ then $f \circ_R \alpha$ assigns to a node $m$ of $F$ the path $(mf)\alpha$ in $H$. For the left composition, suppose we have $k : H \rightarrow K$. Since $n\alpha$ is a path in $H$, we obtain a path $(n\alpha)k$ by applying $k$ to each of the edges in the path $n \alpha$. Thus we define $\alpha \circ_L k$ to be the assignment to $n$ of the path $(n \alpha)k$. The vertical composition is the usual concatenation of paths. The identity 2-cells are assignments of zero length paths. From cat-dist Thu Mar 18 16:25:02 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA26306 for categories-list; Thu, 18 Mar 1999 14:10:36 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 18 Mar 1999 11:33:10 -0300 (EST) From: Elaine Gouvea Pimentel Reply-To: Elaine Gouvea Pimentel To: categories@mta.ca Subject: categories: Polymorphic lambda-calculus Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Hi! I'd like to know if there is any categorical model for polymorphic lambda-calculus. Thanks, Elaine. From cat-dist Thu Mar 18 16:36:24 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA26035 for categories-list; Thu, 18 Mar 1999 14:07:46 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 18 Mar 1999 12:46:52 -0500 (EST) From: Michael Barr To: categories@mta.ca Subject: categories: Re: Monoidal structure, take II In-Reply-To: <36F0E6ED.7EF7BB45@loria.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: I did not quite understand Francois' construction. However, my first reaction to a question like that is that it ought to be a homotopy. So I will say what a homotopy reduces to in this case and leave it to Francois to decide if this is what he has. I suspect that rather few people know what a simplicial homotopy is and, of those, rather few have ever actually verified one. I am in that minority^2, so perhaps I tend to see them where they are not the most natural, but I think it quite remarkable that they can arise where no real topology (but some combinatorics) is present. I have to begin by saying how a graph becomes a simplicial set. Actually, that is a lie, since unless you are dealing with reflexive graphs--that are equipped with a selected loop at each vertex--you will only get a face complex. But homotopies are still definable. A category is a simplicial set by taking for n-simplexes composable n-tuples of arrows. This doesn't work for graphs, since the "interior faces" (all except the lowest and highest numbered) all depend on composition. But there is a face complex in which an n-simplex is simply an n-simplex in the graph. So a 2-simplex is a triangle--obviously non-commutative and a 3-simplex is a tetrahedron and so on. You can describe a composable n-tuple in a category as commutative n-simplex, so this isn't so different. Now given this, if f,g: X --> Y are graph morphisms, what is a homotopy? Well, write X as d^0,d^1: X_1 --> X_0 and similarly for Y. Then f consists of f_0: X_0 --> Y_0 and f_1: X_1 --> Y_1 giving a serially commutative square. Just a homomtopy between functors turns out to be simply a natural transformation, a homotopy in this case turns out to consist of a function p_0: X_0 --> Y_1 and a function p_1: X_1 --> Y_1 such that there is a diagram (not, of course commutative; what a diagram does is specify source and target) as follows. In this diagram I assume x: x^0 --> x^1 in X, and f(x): y^0 --> y^1 and g(x): z^0 --> z^1 in Y. f(x) y^0 -----------> y^1 | \ | | \ | | \ | | \ | | \ | | \ | | \ | p_0(x^0)| p_1(x)\ |p_0(x^1) | \ | | \ | | \ | | \ | | \ | | \ | v g(x) vv z^0 -----------> z^1 So if this is what Francois was saying, then the answer is it a homotopy of face complexes. Of course, if you replaced X_1 by X_1 + X_0, you would have a reflexive graph and I assume (I have not checked this) you would then get a simplicial homotopy. BTW, homotopies do not generally compose--and the ones described here do not appear to either. Categories are special because of their internal composition. It makes me wonder if the well-known failure of dinats to compose could be related to this in some way. Having seen Francois' clarification, I think this is exactly what he had. Michael ------------------------------------------------------------------- History shows that the human mind, fed by constant accessions of knowledge, periodically grows too large for its theoretical coverings, and bursts them asunder to appear in new habiliments, as the feeding and growing grub, at intervals, casts its too narrow skin and assumes another... Truly the imago state of Man seems to be terribly distant, but every moult is a step gained. - Charles Darwin, from "The Origin of Species" From cat-dist Thu Mar 18 16:40:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA25117 for categories-list; Thu, 18 Mar 1999 14:07:04 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Thu, 18 Mar 1999 18:27:30 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Re: Monoidal structure, take II Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: On Francois Lamarche's question. If I understand correctly, the tensor product X tensor Y has the obvious objects (x, y) and arrows of three types (a, y): (x, y) --> (x', y), for a: x -> x' in X, y in Y, (x, b): (x, y) --> (x, y'), for x in X, b: y -> y' in Y, (a, b): (x, y) --> (x', y'), for a and b as above. *** Remark 1. We are thus simulating "identities" of X and Y (which are not given). In other words, we are considering the cartesian product X'xY' of the free reflexive graphs over X and Y, and taking out its identities. Would it not be simpler to work with REFLEXIVE GRAPHS and their cartesian closed structure? In my opinion, reflexive graphs are more natural than graphs: reflexive graph = 1-truncated simplicial set = 1-truncated cubical set It is the topos of presheaves over a FULL subcategory of non-empty ordinals (or cardinals as well), actually the initial segment 1, 2. Remark 2. Roughly speaking, a category enriched over reflexive graphs (wrt the cc structure) is a "2-category without vertical composition". It has cells a: f -> g: X -> Y, with a categorical horizontal composition; it also has trivial cells f -> f: X -> Y ("vertical identities"). All this is clearly related to homotopy and its abstract settings in "2-dimensional categories" (in some sense). And indeed topological spaces, with continuous maps and homotopies, form a rather obvious example. The horizontal composition of homotopies a: f -> g: X -> Y, b: h -> k: Y -> Z is b(a(x, t), t) t in [0, 1], which is indeed categorical. Remark 3. [The sequel is relevant for homotopy; I do not know if it may be relevant in CS, but I always had the impression that abstract homotopy should be of use there, eg with respect to deformations of processes, in some sense.] I do not think that the latter is the "right" 2-dimensional categorical setting for abstract homotopy (even as a starting point). The previous horizontal composition of homotopies is rather artificial; it is what you get from the "double homotopy" b(a(x, t), t') (t, t') in [0, 1]^2 through the diagonal t = t' of the square. (The "double homotopy" itself is quite natural, as produced by the cubical enrichment due to the cylinder functor; it is also important in homotopy.) When the diagonal of the "standard interval" is missing (eg for chain complexes of abelian groups), there is no canonical horizontal composition of homotopies (working with the vertical composition, you get two of them; the middle four interchange does not hold). But there still are canonical horizontal compositions of "maps with homotopies" and "homotopies with maps". This is why I think that the basic 2-dimensional categorical setting for abstract homotopy should only treat such "reduced horizontal composition": arrows with cells, cells with arrows, but NOT cells with cells. Formally, it is again a category enriched over reflexive graphs, BUT wrt the following monoidal closed structure: X tensor Y: - the subgraph of XxY whose arrows are pairs (a, b), where a or b is an identity; [X, Y]: - vertices: the graph morhisms; - arrows: their transformations (without "diagonals"). References: a) The last enrichment (with further developments) has been used for abstract homotopy in: M. Grandis, On the categorical foundations of homological and homotopical algebra, Cahiers Top. Geom. Diff. Categ. 33 (1992), 135-175. [sketch] - , Homotopical algebra in homotopical categories, Appl. Categ. Structures 2 (1994), 351-406. b) A notion equivalent to a category enriched in the same sense had already been studied in: K.H. Kamps, Ueber einige formale Eigenschaften von Faserungen und h-Faserungen, Manuscripta Math. 3 (1970), 237-255. c) For homotopy in groupoid-enriched categories, see Gabriel-Zisman's text (1967). *** With best regards Marco Grandis Dipartimento di Matematica Universita' di Genova via Dodecaneso 35 16146 GENOVA, Italy e-mail: grandis@dima.unige.it tel: +39.010.353 6805 fax: +39.010.353 6752 http://www.dima.unige.it/STAFF/GRANDIS/ ftp://pitagora.dima.unige.it/WWW/FTP/GRANDIS/ From cat-dist Thu Mar 18 16:59:01 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA02580 for categories-list; Thu, 18 Mar 1999 14:55:19 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <36F148B9.E669FE07@loria.fr> Date: Thu, 18 Mar 1999 19:40:57 +0100 From: Francois Lamarche Organization: LORIA X-Mailer: Mozilla 4.5 [en] (X11; I; SunOS 5.5 sun4m) X-Accept-Language: fr, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: and there is a topological connection too References: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Various replies to my query during the day (my thanks to Ronnie Brown and Lutz Schroeder) made me realize that my SMC structure was actually the lifting of the CC structure on reflexive graphs (those with a choice of loop) to ordinary non-reflexive graphs. Here is a bit more detail: We all know these two categories are categories of presheaves. So let G and R be the categories such that Set^G is graphs and Set^R is reflexive graphs. There is an embedding G --> R, which generates the usual triple of functors between the presheaf categories. So it seems this functorial machinery allows to transform the CC structure in Set^R into an SMC structure in Set^G, preserving the forgetful functor. There must be general conditions that allow this. I'm not pursuing this any more right now, because it has to have been done before, and in a much more general setting. Now Michael's comment is also (among other things) about the tension between graphs and reflexive graphs, and naturally there is Lawvere's "Qualitative distinctions between some toposes of generalized graphs" that says a lot about that tension. there may be more in there than we suspect Francois From cat-dist Thu Mar 18 17:24:15 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA13393 for categories-list; Thu, 18 Mar 1999 15:44:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 18 Mar 1999 19:31:58 GMT From: Paul Taylor Message-Id: <199903181931.TAA02244@wax.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: polymorphic lambda-calculus. Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Elaine Gouvea Pimentel would "like to know if there is any categorical model for polymorphic lambda-calculus". Oh dear. I can see that this one is going to haunt me for the rest of my life, besides provoking some "discussion" here. I wrote my thesis on this subject. Perhaps I will be personally rid of this albatross when my book comes out. Chapter VIII contains the definitive account of [my] notion of a "category with a class of display maps" (or, more briefly, display category). This is how I deal with dependent types at the algebraic level (superseding essentially algebraic theories encoded as categories with all finite limits). In my view, discussion of quantifiers (whether first order or over types) should be based on this, as is in fact done in Chapter IX. There are several different things that you might mean by "polymorphic lambda-calculus", and no doubt Bart Jacobs or Thomas Streicher will contribute an overview of the "Barendregt cube". [Robert Seely also did some work in this area before most of the other people.] One thing is that types are expressions involving type variables, with a universal quantifier over types. Girard calls this System F, and there is an introductory account in "Proofs and Types" - Girard's book that Yves Lafont and I translated. Numerous domain theoretic models of System F were found in the later 1980s, using both "Scott"-like "continuous" domains and "stable" domains which were introduced by Berry and popularised by Girard. ALL of the domain theoretic models, so far as I am aware, had THE SAME interpretation of type-dependency and the quantifier. I have seen this interpretation attributed to Girard, but I regarded it as "well known" when I was writing my thesis - before Girard's models - and my guess is that it is due to Gordon Plotkin, probably in the "Pisa notes". This interpretation of the dependency of the type T[x] on x:X, where X is in the first instance a domain (and in particular a poset, therefore a category) is most simply described as a functor T:X->Dom^adj where Dom^adj denotes the category whose objects are domains and whose morphisms are [left] adjoint pairs of continuous functions. Many authors took embeddings (monos with continuous right adjoints) instead, but the restriction is irrelevant. The functor T must also be continuous in the sense of taking directed joins to filtered colimits of left adjoints, which are also the cofiltered limits of the right adjoints. For the stable case, replace "continuous" by "stable", where a stable functor preserves pullbacks, and the unit and counit of the adjunctions have pullbacks for their naturality squares. This situation is so over-constrained that some pretty amazing things (that I discovered but never wrote up) happen. The universal quantifier is most concisely described as the category of sections of the fibration (Grothendieck construction) corresponding to the functor T above. That was for first order dependency over a particular domain X. For dependency over all domains (System F), replace X by Dom^adj. It doesn't matter whether this category happens to be one of your (poset) domains, so long as you only want System F. (At the time of my thesis I considered this to be cheating, and laboriously constructed a poset-domain that "covered" Dom^adj in a suitable sense. Thierry Coquand and his co-authors did not consider this to be cheating, and thereby beat me to finding a model of System F.) If Dom^adj really is a domain then you get a model of Coquand's Calculus of Constructions. Such a model of CoC was described by Martin Hyland and Andy Pitts in the Boulder proceedings in 1987. If I still had the inclination to work on such matters, I could give a simpler version of their model (replacing the lex categories by display categories). This was on the "to do" list throughout the writing of my book - I wanted to include this "simplified" version as a sequence of exercises - but it was always just over the horizon of what could be done with the tools available, given that the necessary domain-theoretic techniques had been debarred from the book from its conception. Another model, whose types are named by countable groupoids (or by the corresponding presheaf toposes of G-sets) is to be found in my paper "Quantitative Domains, Groupoids and Linear Logic" in the proceedings of the 1989 Manchester CTCS. When I was writing this paper I tried to get Francois Lamarche to read it, but he said he didn't know anything about / hated permutation representations. Nobody else, so far as I can gather, has ever read it, and now I can no longer follow the most difficult calculations. However, it is a very pretty model nevertheless. All of this was a bit of a Holy Grail. When you come to calculate the interpretations of types like Pi X. X -> (X->X) -> X, they turn out to be the most horrendous mess. The "coherence space" model in "Proofs and Types" may well be the only one in which you can give an explicit desciption of Pi X. X -> X -> X, and even that has four elements, where there are only two closed lambda terms. There are of course other ways of finding models of the polymorphic lambda calculus, such as using the "small complete category" in Hyland's effective topos, but I'll leave someone else to write about that. In conclusion, this particular dragon's den has already been explored, and the corpses are still there to prove it. Paul You can find this stuff on my page at Hypatia, http://hypatia.dcs.qmw.ac.uk/author/TaylorP and on the corresponding pages of the other people mentioned above. From cat-dist Thu Mar 18 23:12:48 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id WAA04703 for categories-list; Thu, 18 Mar 1999 22:22:12 -0400 (AST) X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Thu, 18 Mar 1999 18:26:32 -0500 (EST) From: "R.A.G. Seely" To: categories@mta.ca Subject: categories: Re: Polymorphic lambda-calculus Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: My 1987 JSL paper is a start - "Categorical Semantics for Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, pp 969 - 989. In particular, look at section 3, where the model of closure operators is described in categorical terms. = rags = On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote: > I'd like to know if there is any categorical model for > polymorphic lambda-calculus. ================================= From cat-dist Thu Mar 18 23:31:58 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id WAA07137 for categories-list; Thu, 18 Mar 1999 22:38:57 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 18 Mar 1999 20:44:39 GMT From: Paul Taylor Message-Id: <199903182044.UAA02495@wax.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: "Practical Foundations of Mathematics" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: 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@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. From cat-dist Fri Mar 19 12:07:05 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA15658 for categories-list; Fri, 19 Mar 1999 09:21:55 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Fri, 19 Mar 1999 09:27:02 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Errata corrige to my previous message Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: 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 From cat-dist Fri Mar 19 12:21:52 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA21505 for categories-list; Fri, 19 Mar 1999 09:37:28 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <36F250DE.DF267D0A@loria.fr> Date: Fri, 19 Mar 1999 14:27:58 +0100 From: Francois Lamarche Organization: LORIA X-Mailer: Mozilla 4.5 [en] (X11; I; SunOS 5.5 sun4m) X-Accept-Language: fr, en MIME-Version: 1.0 To: categories@mta.ca, grandis@dima.unige.it Subject: categories: more on monoidal structure of graphs Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Since Michael's posting leapfrogged Marco's in the aether (at least from the viewpoint of our server) what I'll be saying may not appear in the right order threadwise to some. Marco Grandis wrote: > > Would it not be simpler to work with REFLEXIVE GRAPHS and their cartesian > closed structure? > In my opinion, reflexive graphs are more natural than graphs: The answer is no, because of the application in mind. We want to consider a graph as a constructive binary relation X(x,y), where an edge x-->y is a proof that (x,y) are related. We also want to build such things by induction, using universal properties. Reflexivity is often a desirable feature of the free structures you want to build, but you don't want it to come for free, since it creates redundancies and can mess up the induction principle associated with the structure. In certain situations you want reflexivity to be a consequence of the induction principle. > Remark 3. > [The sequel is relevant for homotopy; I do not know if it may be relevant > in CS, but I always had the impression that abstract homotopy should be of > use there, eg with respect to deformations of processes, in some sense.] > There are two connections I know about between homotopy and computer science. The first has to do with process algebras, and originates in Eric Goubault's thesis, I think. Philippe Gaucher just sent a paper annoucement on this server about this line of research. The second connection is something Thomas Streicher, Martin Hoffmann and I discuss whenever we meet, which is not often enough. In constructive type theory there is a gadget called the Martin-L"of intensional equality predicate, J(x,y). So this is a version of equality, where you have to name the proofs that x=y. It has very simple (but rather mysterious) introduction and elimination rules, which can be translated as a universal property in a kind of higher-order universal algebra, where arities can not only be seen as finite sets, but also as families of sets, and families of families of sets and so on. In particular, since everything is a type, you have a type/predicate of equality proofs between equality proofs, and so on. For example given proofs that x=y and y=z, you can construct a proof that x=z, and you can do this uniformly, getting a term/algorithm J(x,y)*J(y,z) --> J(x,z) (here the * means a fibered product over y). But you cannot show that this operation is itself associative, it is only associative at a higher order. Ah! some kind of multiple category is involved! But so far all attempts to use higher-order categories to describe those weird algebras have failed. It only works at level one: when you collapse all proofs of equality between proofs of equality you get that the predicate J(x,y) is a groupoid structure. But when you try to go to level 2 the ordinary 2- or bi- or lax- or whatever- categorical machinery fails. You realize that simplicial sets are a better paradigm/starting point, but we need simplicial sets with operations. BTW is anybody from G"oteborg reading this? > This is why I think that the basic 2-dimensional categorical setting for > abstract homotopy should only treat such "reduced horizontal composition": > arrows with cells, cells with arrows, but NOT cells with cells. > Formally, it is again a category enriched over reflexive graphs, BUT wrt > the following monoidal closed structure: > > X tensor Y: > - the subgraph of XxY whose arrows are pairs (a, b), where a or b > is an identity; > > [X, Y]: > - vertices: the graph morphisms; > - arrows: their transformations (without "diagonals"). > Hm... the geometrical motivations for not having full composition(s) here might well be related to the logical ones I mentioned briefly above. Francois From cat-dist Fri Mar 19 12:24:19 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA22497 for categories-list; Fri, 19 Mar 1999 09:55:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <36F25658.4F862077@loria.fr> Date: Fri, 19 Mar 1999 14:51:20 +0100 From: Francois Lamarche Organization: LORIA X-Mailer: Mozilla 4.5 [en] (X11; I; SunOS 5.5 sun4m) X-Accept-Language: fr, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: They often come in pairs References: <199903181931.TAA02244@wax.dcs.qmw.ac.uk> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Perhaps some precisions should be added to Paul's msg. > Another model, whose types are named by countable groupoids (or by the > corresponding presheaf toposes of G-sets) is to be found in my paper > "Quantitative Domains, Groupoids and Linear Logic" in the proceedings > of the 1989 Manchester CTCS. When I was writing this paper I tried to > get Francois Lamarche to read it, but he said he didn't know anything > about / hated permutation representations. Nobody else, so far as I can > gather, has ever read it, and now I can no longer follow the most > difficult calculations. However, it is a very pretty model nevertheless. Because of my thesis' work (on not-unrelated subjects to those mentioned by Paul) I had already dealt with permutations in power types when Paul started pushing his groupoid models. They indeed give rise to "the most horrendous mess". This was a long time ago, my memory is vague, but I probably told him, or hinted, that in my opinion they were most likely a blind alley. I still think that if I started working again in this field, the problem I would zero in would be to get rid of the permutation groups, by "unraveling" them by the means of actions (the groupoid associated with the action of a group on a set can be made much simpler than the group itself). The point of semantics is to give you insights about the logic, so simplicity is... a big plus. And since I refereed his CTCS paper, I *did* read it. Francois From cat-dist Fri Mar 19 16:35:06 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA13645 for categories-list; Fri, 19 Mar 1999 14:57:50 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Fri, 19 Mar 1999 16:03:40 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Re: more on monoidal structure of graphs Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Francois Lamarche wrote >...But you cannot show that this >operation is itself associative, it is only associative at a higher >order. Ah! some kind of multiple category is involved! But so far all >attempts to use higher-order categories to describe those weird algebras >have failed. It only works at level one: when you collapse all proofs of >equality between proofs of equality you get that the predicate J(x,y) is >a groupoid structure. But when you try to go to level 2 the ordinary 2- >or bi- or lax- or whatever- categorical machinery fails. I wonder whether the notion of "h4-category" which I introduced for abstract homotopy theory (see the references in my first reply) might be of use for this. It is a sort of "2-category vertically relaxed up to a 'shadow' of 3-cells" (whereas bi-categories are horizontally relaxed up to invertible 2-cells). To begin with, it is a category enriched over reflexive graphs in the sense previously described: there is a reduced horizontal composition, of maps with cells and cells with maps, which is strictly associative as far as this makes sense. There also are vertical identities, vertical involution and vertical composition, which only satisfy the usual axioms up to an assigned equivalence relation ("2-homotopy"). This approach is truncated at the level of usual (first-order) homotopies; 3-cells (homotopies of homotopies) only leave their 'shadow', as an equivalence relation. If you want to proceed further, my impression is that the relaxed categorical machinery becomes too heavy (at least for my taste). However, if your 2-cells (homotopies) can be represented - by a cylinder functor I, as arrows IX -> Y, - or dually by a path functor P, as arrows X -> PY, (or by both, forming an adjoint pair I -| P) as it happens for most "concrete" homotopy theories, then the powers of such endofunctor and the clone of operations (natural transformations) linking them, derived from the basic ones (faces, degeneracy, concatenation, etc.), seem to give all what we need in any dimension. This machinery of derived operations can be seen in a paper of mine Categorically algebraic foundations for homotopical algebra, Appl. Categ. Structures 5 (1997), 363-413, but of course "abstract cylinder functors" go back, at least, to Kan; other references can be found in the paper above. Regards Marco Grandis From cat-dist Fri Mar 19 16:40:11 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA26240 for categories-list; Fri, 19 Mar 1999 14:58:03 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 19 Mar 1999 16:13:02 +0000 (GMT) From: Ronnie Brown X-Sender: mas010@publix To: categories@mta.ca Subject: categories: Naive question on Polymorphic lambda-calculus, etc In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: This is written from the point of view of someone who would like to see a computational system which is much nearer to real mathematics than the current widely used systems (Maple, Mathematica, and various more specialised systems, e.g. Singular). Of these the only one which is clearly typed is Singular. There is also AXIOM, which has parametrised types, types can be variables, there is multiple inheritance and coercion. It looks much nearer to what should be mathematics. On the other hand, its literature does not include any theory of the type system, so consistency is not clear, and it is not generally used. So my question is: does all this general theory of types give a clear indication as to what should be, not necessarily a final, but certainly a convenient theory adequate for expressing a majority of present day maths? Let's make up a test case: one should be able to code reasonably conveniently the type of a general groupoid acting on exterior algebras over a commutative ring, and also of course the category of such objects. A groupoid acting on exterior algebras with zero multiplication should be coercible to a groupoid acting on graded modules. I would prefer the sytem to be so simple that it will allow tests for consistency of new proposed types. Also it should be easy to understand, since it would represent nicely current practice. Is this idea a mirage? Ronnie On Thu, 18 Mar 1999, R.A.G. Seely wrote: > My 1987 JSL paper is a start - "Categorical Semantics for > Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, > pp 969 - 989. In particular, look at section 3, where the > model of closure operators is described in categorical terms. > > = rags = > > On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote: > > > I'd like to know if there is any categorical model for > > polymorphic lambda-calculus. > > > ================================= > > > > 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 From cat-dist Fri Mar 19 16:45:31 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA17367 for categories-list; Fri, 19 Mar 1999 15:23:45 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 19 Mar 1999 19:05:39 GMT From: Paul Taylor Message-Id: <199903191905.TAA08502@wax.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: my groupoid model Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Francois Lamarche says: > I still think that if I started working again in this field, > the problem I would zero in would be to get rid of the permutation groups, This would be a great pity. Girard's coherence spaces (see "Proofs and Types"), ordinary relational algebra (in which Shroeder identified the par, writing +, for it, I think, in 1895) and my model with groupoids all illustrate a common theme in the workings of models of linear logic. In all of these structures, there are extremely natural ways of defining the structure on disjoint unions and cartesian products, and of turning the structure inside out or upside down. These turn out to be the additive, multiplicative and negative connectives in linear logic. There are less natural ways of defining the structure on powersets, finite powersets and other variations on this theme. These are the exponentials. It is important to note that there are several different exponential operations available to interpret ! and ? . Girard got function spaces out of such constructions (as did Francois, myself and numerous other people). What I hope to show soon is how to get higher order logic too. Paul From cat-dist Sat Mar 20 10:22:39 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA17076 for categories-list; Sat, 20 Mar 1999 09:30:13 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sat, 20 Mar 1999 03:19:01 +0100 (MET) From: Tom KRANTZ To: categories@mta.ca Subject: categories: On reflexivity Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: A 'philosophical' interpretation of oriented graphs might be out of the scope of the categories mailing list, it seems elucidating to me though.(It could have been for Heraclit and Parmenides.) I suggest to consider vertices as states and edges as transitions. A reflexive edge corresponds to a transition from a state to itself. Two notions of morphism of oriented graphs come seem natural: - A rigid embedding which preserves difference of states - A notion of morphism which may equalize different states. The meaning of equality of states needs precision then. Coherence semantics deals with a different notion of graph. This is clear to me and can also be deduced from a discussion between Thomas Ehrhard and his student Pierre to which I assisted. This bears an answer to the question of reflexivity I think. Sincerely, Tom From cat-dist Sat Mar 20 12:10:33 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA22550 for categories-list; Sat, 20 Mar 1999 11:10:49 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 19 Mar 1999 19:23:37 GMT From: Paul Taylor Message-Id: <199903191923.TAA08560@wax.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: Ronnie Brown's type-dream Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Ronnie Brown asked, > This is written from the point of view of someone who would like to see a > computational system which is much nearer to real mathematics than the > current widely used systems (Maple, Mathematica, and various more > specialised systems, e.g. Singular). .... > So my question is: does all this general theory of types give a clear > indication as to what should be, not necessarily a final, but certainly a > convenient theory adequate for expressing a majority of present day maths? > > Let's make up a test case: one should be able to code reasonably > conveniently the type of a general groupoid acting on exterior algebras > over a commutative ring, and also of course the category of such objects. > A groupoid acting on exterior algebras with zero multiplication should be > coercible to a groupoid acting on graded modules. > > I would prefer the sytem to be so simple that it will allow tests for > consistency of new proposed types. Also it should be easy to understand, > since it would represent nicely current practice. > > Is this idea a mirage? No, I don't think it's a mirage, though [help me somebody I need a good pun here] the answer I have in mind may involve some altered states of perception. For the moment I want to steer clear of the "computational" question, as I haven't begun work on that, and would like to read his "current widely used systems" to refer to set theory, elementary toposes, Martin-Lof type theory and so on. That being said, I wonder whether the discussion and results in my "Abstract Stone Duality" paper (that I advertised on "categories" in the new year and which has since been revised) might appeal to Ronnie. It bases "set theory" on topology and not vice versa. It identifies categories of open discrete and compact Hausdorff spaces that are both pretoposes, and therefore suitable for doing algebra in, though the open discrete spaces are more appropriate for this as they admit free algebras. I do, as I said, have a computational model in mind, but am not yet in a position to say anything about it. Paul This paper, like most of what I talk about, is accessible from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP From cat-dist Wed Mar 24 15:22:09 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA12177 for categories-list; Wed, 24 Mar 1999 13:12:11 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Gordon Plotkin MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Date: Wed, 24 Mar 1999 14:55:57 +0000 (GMT) To: categories@mta.ca, types@cis.upenn.edu Subject: categories: PhD Studentship at Edinburgh cc: gdp@dcs.ed.ac.uk, dt@dcs.ed.ac.uk, eak@dcs.ed.ac.uk X-Mailer: VM 6.43 under 20.4 "Emerald" XEmacs Lucid Message-ID: <14072.64322.657269.150765@dulnain.dcs.ed.ac.uk> Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Division of Informatics University of Edinburgh Announcement of PhD Studentship in The Structure of Programming Languages: Syntax and Semantics A PhD student is sought for three years from October 1999 to work under the supervision of Prof. Gordon Plotkin on a UK EPSRC-funded project: ``The Structure of Programming Languages: Syntax and Semantics.'' The project aims at a general theory of the syntax and semantics of programming languages. The student will work on a categorical theory of structural operational semantics and its relation to denotational semantics. (See http://www.dcs.ed.ac.uk/home/dt/lics97.ps.) Example topics include: variations on GSOS for computational effects other than non-determinism; linguistic expressions of categorical operational semantics; and a theory of language translation incorporating both denotational and operational semantics. The studentship is for three years and pays for all fees and includes maintenance (living expenses) at the usual EPSRC rate. The studentship will be held at the Laboratory for Foundations of Computer Science (LFCS), Division of Informatics, University of Edinburgh. The LFCS provides an ideal environment for postgraduate research. The first six months of postgraduate training are supported by a unique postgraduate course on the theory of computation. In addition, there are regular short courses on advanced research topics, and a number of forums provide weekly research seminars. The LFCS is particularly strong in the area of semantics of programming languages. The PhD studentship is relevant to computer science or mathematics graduates who are interested in at least one topic from: theory of programming languages, operational semantics, category theory. For additional information contact Gordon Plotkin: gdp@dcs.ed.ac.uk http://www.dcs.ed.ac.uk/home/gdp/ For an application form write to Eleanor Kerse PhD Admissions, Department of Computer Science, University of Edinburgh, JCMB, King's Buildings, Edinburgh EH9 3JZ Scotland or use the HTML form available from http://www.dcs.ed.ac.uk/deptinfo/admissions/phd ----------------------------------------------------------------------------- Prof. Gordon Plotkin E-Mail: gdp@dcs.ed.ac.uk LFCS, University of Edinburgh Tel: +44 131 650 5158 JCMB, The King's Buildings Fax: 667 7209 Edinburgh EH9 3JZ, UK http://www.dcs.ed.ac.uk/home/gdp/ From cat-dist Fri Mar 26 09:05:27 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id GAA31006 for categories-list; Fri, 26 Mar 1999 06:17:25 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <2.2.32.19990325140903.0085efe4@163.10.5.24> Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Date: Thu, 25 Mar 1999 11:09:03 -0300 To: categories@mta.ca From: Gabriel Baum Subject: categories: WAIT99 - Call for Papers Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id JAA22733 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Please find below the WAIT'99 Call for Papers. We apologize if you receive this message more than once. Call for Papers 28 JAIIO - WAIT'99 Argentinian Workshop on Theoretical Computer Science Buenos Aires - Argentina September 6-7, 1999 ---------------------------------------------------------------------------- --------- The 3rd Argentinian Workshop on Theoretical Computer Science (WAIT'99) will be part on the 28th Argentinean Conference on Informatics and Operations Research (28 JAIIO), to be held in Buenos Aires from September 6th to September 10th, 1999. The goal of the workshop is bringing together researchers from academy (from Argentinean and other universities) and industry professionals in order to discuss theoretical, empirical and experimental results on the field of theoretical computer science. This workshop will consist of invited talks and technical presentations. Contributions are expected in all the areas of theoretical computer science, including the following: * Logical and algebraic foundations for computer science (logics for computer science, category theory, relation algebras, type theory, etc.), * Formal program construction (formal specification of sequential and concurrent programs; analysis, verification and transformation of programs, etc.), * Algorithms and data structures (sequential, parallel, distributed, on-line, probabilistic, etc.), * Computational complexity, * Automata theory, * Graph theory, * Symbolic and algebraic computation. The expected contributions will describe original results as well as undergoing research and development projects on theoretical computer science coming from academy and industry. Papers will be refereed by the International Program Committee, based on the following: * Papers reporting research / experimental results: these papers must present previously unpublished results and will be judged based on their originality, significance, relevance and clarity of presentation. Authors must submit an extended abstract of up to 4 pages containing enough information to allow the referees to determine the merits of their work. It is also allowed to submit the full paper of up to 12 pages including figures and references. * Research projects: aiming to fostering the cooperation among national and foreign researchers, short papers describing ongoing research will be considered. Papers in this category may report already published results. In that case, the authors must include the corresponding references. * Industrial / Commercial applications: also relevant are papers describing applications of theoretical results to real-life situations. Short papers describing results that are both of significance for industry and that make novel or defying applications of theoretical results are sought. INVITED SPEAKERS Thomas S. E. Maibaum (Imperial College, London, UK) Bernhard Moeller (Universitaet Augsburg, Germany) INSTRUCTIONS FOR AUTHORS: In order to facilitate the widest dissemination of the papers, authors are recommended the use of the English language. Nevertheless, papers in Spanish or Portuguese are also welcome. The deadline for submission of papers is May 3rd, 1999. Papers must be submitted electronically in PostScript format (ghostview-readable) to the e-mail address: wait99@sol.info.unlp.edu.ar Authors must send in a separate message in ASCII format the following: title of the paper, name and affiliation of all the authors, their e-mail addresses, phone and FAX numbers, an abstract of their contribution of at most ten lines, a list of keywords that best describe the paper, and also the category within which the paper is to be evaluated. Alternative ways for paper submission are possible and must be discussed with the workshop co-chairs. The format for camera-ready papers will be announced with the letter of acceptance. IMPORTANT DATES: Deadline for reception of papers....................May 3rd, 1999 Notification of acceptance..........................June 15th, 1999 Deadline for reception of camera-ready versions.....July 16th, 1999 WORKSHOP CO-CHAIRS: Prof. Gabriel Baum LIFIA Dto. de Informatica Universidad Nacional de La Plata Calle 50 y 115 1er piso. (1900) La Plata - Argentina Tel/Fax : +54-21-22-8252 e-mail: gbaum@sol.info.unlp.edu.ar Prof. Marcelo Frias Dpto. De Computacion -FCEyN- Universidad de Buenos Aires Pabellon I - Ciudad Universitaria 1428- Buenos Aires - ARGENTINA Tel/Fax : +54-1-783-0729 e-mail: mfrias@sol.info.unlp.edu.ar PROGRAM COMMITTEE: Gabriel Baum (Universidad Nacional de La Plata, Argentina) Javier Blanco (Universidad Nacional de Cordoba, Argentina) Luis Fariñas del Cerro (Universite Paul Sabatier, France) Esteban Feuerstein (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Marcelo Frias (Universidad Nacional de Buenos Aires, Argentina) Armando Haeberer (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Joos Heintz (Universidad Nacional de Buenos Aires, Argentina) Roger Maddux (Iowa State University, USA) Tom Maibaum (Imperial College, UK) Bernhard Moeller (Universitaet Augsburg, Germany) Gonzalo Navarro (Universidad de Chile, Chile) Alfredo Olivero (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Ruy de Queiroz (Universidade Federal de Pernambuco, Brazil) Alvaro Tasistro (Universidad de la Republica, Uruguay) Sergio Yovine (CNRS-VERIMAG, France) For more information send e-mail to: jaiio@sadio.edu.ar, write to: SADIO / WAIT'99 Uruguay 252 2D 1015 - Buenos Aires ARGENTINA TEL: +54-1-3715755/4763950 FAX: +54-1-3723950 or see http://www.uba.ar/wwws/sadio ___________________________________________ Gabriel Baum LIFIA Facultad de Ciencias Exactas Universidad Nacional de La Plata Calle 50 y 115 - 1er piso (1900) La Plata e-mail: gbaum@sol.info.unlp.edu.ar Tel/Fax: +54 21 228252 ___________________________________________ From cat-dist Wed Mar 31 10:56:05 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA21698 for categories-list; Wed, 31 Mar 1999 08:46:24 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 31 Mar 1999 08:43:50 -0400 (AST) From: Bob Rosebrugh To: categories Subject: categories: list outage Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Note from moderator: Posts sent to the categories list in the past few days (roughly since March 26) will have bounced back to the sender. The cause was, ironically, a sendmail patch to scan for the "Melissa" virus/worm that corrupted the alias database for the majordomo software used by the list. If you sent a post recently and have not seen it please resend,things are working again. Sorry about any delays, and thanks to the Mount Allison network manager for immediate response when the problem was detected. regards, Bob Rosebrugh From cat-dist Wed Mar 31 11:05:00 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA13692 for categories-list; Wed, 31 Mar 1999 08:28:36 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from linc.cis.upenn.edu (LINC.CIS.UPENN.EDU [158.130.12.3]) by mailserv.mta.ca (8.9.3/8.9.3) with ESMTP id PAA02795 for ; Tue, 30 Mar 1999 15:38:19 -0400 (AST) Message-Id: <199903301752.MAA18177@saul.cis.upenn.edu> X-Received: from linc.cis.upenn.edu (LINC.CIS.UPENN.EDU [158.130.12.3]) by saul.cis.upenn.edu (8.8.5/8.8.5) with ESMTP id HAA23457 for ; Tue, 30 Mar 1999 07:51:56 -0500 (EST) X-Received: from muck.dcs.ed.ac.uk (root@muck.dcs.ed.ac.uk [129.215.160.15]) by linc.cis.upenn.edu (8.8.5/8.8.5) with ESMTP id HAA19638 for ; Tue, 30 Mar 1999 07:51:54 -0500 (EST) X-Received: from samphrey.dcs.ed.ac.uk (ctcs99@samphrey.dcs.ed.ac.uk [129.215.160.238]) by muck.dcs.ed.ac.uk with ESMTP id NAA10491; Tue, 30 Mar 1999 13:51:26 +0100 (BST) Date: Tue, 30 Mar 1999 13:51:21 +0100 (BST) To: categories@mta.ca Subject: categories: CTCS '99 (Deadline 23 April 1999) From: "Martin Hofmann" Content-Type: text Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: CATEGORY THEORY AND COMPUTER SCIENCE (CTCS'99) 10-12 SEPTEMBER 1999, EDINBURGH, SCOTLAND SECOND CALL FOR PAPERS SUBMISSION DEADLINE: 23 APRIL 1999 CHANGED SUBMISSION PROCEDURE (see below) CTCS '99 is the 8th conference on "Category Theory and Computer Science." The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory. While the emphasis is upon applications of category theory, it is recognized that the area is highly interdisciplinary. Topics of interest - - ------------------ include but are not limited to category-theoretic aspects of the following: concurrent and distributed systems constructive mathematics declarative programming and term rewriting domain theory and topology linear logic models of computation program logics, data refinement, and specification programming language semantics type theory Previous meetings have been held in Guildford (Surrey), Edinburgh, Manchester, Paris, Amsterdam, Cambridge, and S. Margherita Ligure (Genova). Programme committee - - ------------------- J. Adamek TU Braunschweig (Germany) N. Benton Microsoft Research, Cambridge (UK) R. Blute U. Ottawa (Canada) T. Coquand Chalmers (Sweden) M. Escardo LFCS Edinburgh (UK) M. Hasegawa Kyoto Univ. (Japan) M. Hofmann (Chair) LFCS Edinburgh (UK) P. O'Hearn Queen Mary West (UK) D. Pavlovic Kestrel Institute (California) H. Reichel TU Dresden (Germany) G. Rosolini U. Genova (Italy) A. Scedrov U. Penn (Pennsylvania) Organising Committee - - -------------------- S. Abramsky LFCS Edinburgh (UK) P. Dybjer Chalmers U. (Sweden) E. Moggi U. Genova (Italy) A. Pitts U. Cambridge (UK) Submission procedure - - -------------------- E-mail your contribution as a PostScript file to the programme chair (ctcs99@dcs.ed.ac.uk) to be received by 23 April 1999. Alternatively, you can send 5 hardcopies by air mail. Authors with restricted copying facilities may also send a single hardcopy. Please make sure mail submissions arrive before the deadline (we'll definitely take submissions postmarked 7 April 1999 or earlier.). We would appreciate an informal notification of intention to submit 2 weeks prior to the deadline. Papers should allow the Programme Committee to assess the merits of the work: in particular references and comparisons with related work should be included. Submission of material already published or submitted to other Conferences with Proceedings is not allowed. There is no strict page limit; however authors are strongly encouraged to try not to exceed 20 A4 pages. Conference proceedings will appear in Electronic Notes in Theoretical Computer Science (http://www.elsevier.com/locate/entcs). Paper copies of the proceedings will be available to participants at the conference. Important dates - - --------------- 9 April 1999 Notification of intention to submit 23 April 1999 Submission deadline 4 June 1999 Notification of authors of accepted papers 30 July 1999 Deadline for final versions of accepted papers Address for paper submissions - - ----------------------------- Martin Hofmann Laboratory for Foundations of Computer Science Division of Informatics JCMB, King's Buildings Mayfield Road Edinburgh EH9 3JZ Scotland Local organization - - ------------------ Monika Lekuse Laboratory for Foundations of Computer Science Division of Informatics JCMB, King's Buildings Mayfield Road Edinburgh EH9 3JZ Scotland Conference e-address ctcs99@dcs.ed.ac.uk - - -------------------- Conference homepage http://www.dcs.ed.ac.uk/home/ctcs99 - - ------------------- Related event 2nd APPSEM workshop, 6-9 September 1999 - - ------------- http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/index.html - ------- End of forwarded message ------- ------- End of forwarded message -------