From cat-dist Thu Jul 1 11:50:59 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA21793 for categories-list; Thu, 1 Jul 1999 09:51:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 30 Jun 1999 21:13:03 +0200 From: Eva Ullan Subject: categories: CSL'99 Programme and CFP 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 QAA02118 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ------------------------------------------------------------- CALL FOR REGISTRATION AND PARTICIPATION CSL'99 Annual Conference of the European Association for Computer Science Logic (EACSL) Madrid, Spain, September 20-25, 1999 ------------------------------------------------------------- http://mozart.sip.ucm.es:1580/csl99/ ***************************************************** Early registration deadline: July 15, 1999 ***************************************************** * Sponsored by: Departamento Sistemas Informaticos y Programacion (SIP) - UCM European Research Consortium for Informatics and Mathematics - ERCIM Esprit Working Group - CCLII Facultad de Matematicas - UCM Ministerio de Educacion y Ciencia - CICYT Vicerrectorado de Investigacion - UCM Vicerrectorado de Relaciones Internacionales - UCM * Organised by: SIP-UCM DACYA-UCM * 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) * Local Organizing Committee: J. Carlos Gonzalez-Moreno, Teresa Hortala-Gonzalez, Javier Leach-Albert (chair), Paco Lopez-Fraguas, Fernando Saenz-Perez, Eva Ullan-Hernandez. * Programme commitee of CSL'99: 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), Martin Wirsing (Munich, Germany). -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- The 1999 Annual Conference of the European Association for Computer Science Logic follows previous CSL Conferences: CSL'98 (Brno, Czech Republic), CSL'97 (Aarhus, Danemark), CSL'96 (Utrecht, Netherlands), CSL'95 (Paderborn, Germany), CSL'94 (Kasimierz, Poland), CSL'93 (Swansea, Great Britain), CSL'92(San Miniato/Pisa, Italy), CSL'91 (Bern, CH), CSL'90 (Heidelberg, Deutchland), CSL'89 (Kaiserslautern, Deutchland), CSL'88 (Duisburg, Deutchland), and CSL'87 (Karlsruhe, Deutchland), CSL'99 will be held in Madrid (Spain). The event is organized jointly by the Computer Science Departments (SIP and DACYA) of Universidad Complutense de Madrid (UCM). The scientific program includes 34 selected papers from among 91 submissions, five invited lectures, and two tutorials on theorem proving and rewriting techniques, scheduled on September 24 afternoon (Friday) and September 25 morning (Saturday), immediately after the main conference. In addition to the scientific program, the social program includes an excursion to Segovia (a nearby historic city), and a conference dinner. Madrid, a city of contrasts, traditional and contemporary at the same time, offers the opportunity to enjoy both Spain and one of the most attractive capitals in Europe. In this document you can find the Invited Lecturers, Tutorials, Scientific Programme, General Information, Registration and Accommodation Information. The CSL'99 Web page http://mozart.sip.ucm.es:1580/csl99/ contains additional information. -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- INVITED LECTURERS: Jose Luis Balcazar - Universidad Politecnica Cataluna Title: The consistency dimension, compactness, and query learning Javier Esparza - Technische Universitat Munchen Title: Partial order semantics help Martin Grohe - Albert-Ludwig-Universitat Freiburg Title: Descriptive and Parametrized Complexity Peter D. Mosses - University of Aarhus Title: Logical specification of operational semantics Victor Vianu - University California San Diego Title: Topological Queries in Spatial Databases TUTORIALS: Douglas J. Howe - Bell Labs Title: Interactive Theorem Proving using Type Theory Aart Middeldorp - University of Tsukuba Title: Term Rewriting PRELIMINARY SCIENTIFIC PROGRAMME: Monday 20th, September 9:00 Registration 9:45 Conference Opening 10:00 Invited Talk: V. Vianu Topological Queries in Spatial Databases 11:00 Coffee Break Session 1: Descriptive Complexity 11:20 E. Gradel and S. Kreutzer Descriptive complexity theory for constraint databases 11:50 D. Leivant Applicative control and computational complexity 12:30 Lunch Session 2: Verification 14:00 T. Arts and J. Giesl Applying Rewriting Techniques for Verification of Erlang Processes 14:30 J. Moller, J. Lichtenberg, H.R. Andersen and H. Hulgaard Difference Decision Diagrams 15:00 M. Fraenzle Analysis of Hybrid Systems: An ounce of realism can save an infinity of states 15:30 Y. Kesten and A. Pnueli Can Abstraction Replace Deduction? 16:00 Coffee break 16:30 EACSL Assembly Tuesday 21th, September 9:00 Invited Talk: J.L. Balcazar The consistency dimension, compactness, and query learning Session 3: Temporal Logic 10:30 T.M. Rasmussen Signed Interval Logic 11:00 Coffe break 11:20 Y. Hirshfeld and A. Rabinovich Quantitative Temporal Logic 11:50 V. Diekert and P. Gastin An expressively complete temporal logic without past tense operators for Mazurkiewicz traces 12:30 Lunch Session 4: Lambda Calculus, Linear Logic 14:00 E. Bonelli Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting 14:30 M. Fernandez and I. Mackie Closed Reductions in the l-calculus 15:00 S. Ishtiaq and D.J. Pym Kripke resource models of a dependently-typed, bunched l-calculus 15:30 R. Di Cosmo and V. Balat A linear logic view of linear type isomorphisms 16:00 Coffee break Session 5: Logic Programming, Modal Logic, Description Logic 16:30 M. De Vos Choice logic programs and Nash equilibria in strategic games 17:00 S. Hagihara and N. Yonekazi Resolution Method for Modal Logic with Well-founded Frames 17:30 S. Tobies A NExpTime-complete Description Logic Strictly Contained in C2 18:00 C. Areces, P. Blackburn and M. Marx A Road-map on Complexity for Hybrid Logics Wednesday 22th, September 9:30 Invited talk: M. Grohe Descriptive and Parametrized Complexity Session 6: Descriptive Complexity 10:30 C. Lautemann and B. Weinzinger Monadic NLIN and quantifier free reductions 11:00 Coffe break 11:20 J. Marcinkowski Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraise games 11:50 J.C. Bradfield Fixpoint alternation and the game quantifier 12:30 Lunch 13:30 Excursion to Segovia Thursday 23rd, September 9:30 Invited talk: P. Mosses Logical specification of operational semantics Session 7: Logic and Complexity 10:30 J. Toran Lower Bounds for Space in Resolution 11:00 Coffe break 11:20 I.A. Stewart Program schemes, arrays, Lindstrom quantifiers and zero-one laws 11:50 L.D. Blemishev Open least element principle and bounded query computation 12:30 Lunch Session 8: Lambda Calculus, Type Theory 14:00 A.D. Ker, H. Nickau and C.H.L. Ong More Universal Game Models of Untyped l-Calculus: The Bohm Tree Strikes Back 14:30 A. Compagnoni and H. Goguen Anti-Symmetry of Higher-Order Subtyping 15:00 H. Geuvers, E. Poll and J. Zwanenburg Safe Proof Checking in Type Theory with Y 15:30 T. Altenkirch and B. Reus Monadic presentations of lambda terms using generalized inductive types 16:00 Coffee break Session 9: Linear Logic, Mu Calculus, Concurrency 16:30 L. Roversi A Proof of Completeness for Light Logics 17:00 H. Seidl and A. Neumann On Guarding Nested Fixpoints 17:30 A. Kucera and J. Esparza A Logical Viewpoint on Finite-State Descriptions of Processes 18:00 P. Gastin and M. Mislove A Truly Concurrent Semantics for a Simple Parallel Programming Language Friday 24th, September 9:30 Invited talk: J. Esparza Partial order semantics help Session 10: Specification, Data Refinement 10:30 J.E. Hannay Specification Refinement with System F 11:00 Coffe break 11:20 F. Honsell and D. Sannella Pre-logical Relations 11:50 Y. Kinoshita and J. Power Data-refinement for call-by-value programming languages 12:20 Conference Closure 12:30 Lunch 14:30 A. Middeldorp Tutorial on Term Rewriting, 1st part 16:00 Coffee break 16:30 Tutorial on Term Rewriting, 2nd part Saturday 25th, September 9:30 D. Howe Tutorial on Interactive Theorem Proving using Type Theory, 1st part 11:00 Coffee break Tutorial on Interactive Theorem Proving using Type Theory, 2nd part -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- GENERAL INFORMATION Place and travel The Conference will be held in Madrid (Spain), at the Faculty of Mathematics of Universidad Complutense de Madrid (UCM), from the 20th to the 25th of September, 1999. Madrid has direct flights from most major cities and generally good connections from elsewhere. Barajas, the international Madrid airport, is only about10 km from the city. There are frequent regular buses and taxis to the city, as well as the new metropolitan line. The Faculty of Mathematics can be reached by metro (metropolitan station Ciudad Universitaria or Metropolitano) or by bus (bus lines 132, F, or 82). The CSL'99 Web page (http://mozart.sip.ucm.es:1580/csl99/) contains additional information such as the metropolitan network map, and the surroundings to CSL host site map. Social Events A guided excursion to Segovia will be held on Wednesday, 22th. The departure will be after lunch, at 14:00. Registered participants have this excursion included, and accompanying persons can buy an excursion ticket (60 euros) during the Registration and Opening Session to CSL'99. The excursion includes dinner. Languages The official language of the Conference is English. REGISTRATION AND ACCOMMODATION INFO REGISTRATION INFO CSL'99 Registration to the Conference and/or Tutorial must be made sending the Conference Registration Form and/or the Tutorial Registration Form and a copy of your corresponding bank transfer (via fax) directly to: CSL'99 attention of ms. Eva Ullan fax +34/91/394 46 02 Electronic mail registration will not be accepted The conference registration fee includes: - admission to the conference - morning and afternoon coffee breaks during the conference - lunches during the conference - excursion and social event - a copy of the proceedings volume - one year subscription to EACSL The tutorial registration fee includes: - admission to the tutorials - afternoon and morning coffee breaks during the tutorials - working material EARLY CONFERENCE REGISTRATION FEE: 270 EUROS. For early registration, the registration form together with a the copy of your bank remittance must reach us by July 15, 1999 LATE CONFERENCE REGISTRATION FEE: 300 EUROS. After July 15, 1999 SUBSIDISED STUDENT CONFERENCE REGISTRATION FEE: 150 EUROS If you want to apply for subsidised student registration fee, please type out your e-mail address and send the applying form for student registration fee, with a copy of your student certification via fax before July 1, 1999. You will receive a notification before July 5, 1999 if there is a student grant available for you. Since there are a reduced number of student grants, a positive answer will be possible only on a first come first serve basis. TUTORIAL REGISTRATION FEE: 60 EUROS For early tutorial registration, the tutorial registration form with a copy of your bank remittance must reach us by July 15, 1999 LATE TUTORIAL REGISTRATION FEE: 80 EUROS. After July 15, 1999 Payments should be made in EURO currency by bank transfer WITHOUT CHARGES FOR THE BENEFICIARY payable to: CAJA DE MADRID Donoso Cortes 80 28015 MADRID FUNDACION GENERAL UCM (CSL'99) Account: 2038/1735/09/2000001375 Do not forget the specification CSL'99 !!! -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- ACCOMMODATION INFO CSL'99 A) For those who would like a simple accommodation lodging in a student room, we have made arrangements with "Colegio Mayor Loyola", Paseo Juan XXIII 17, 28040 MADRID, SPAIN, Fax +34/91/535 22 05 In "Colegio Mayor Loyola" the price for single rooms, full board, is 4,600 pts + 7% VAT per day (27.646 EUROS + 7% VAT) If you want a "Colegio Mayor Loyola" accommodation you have to fill in the accommodation form and return in printed form via fax before July 15, 1999 to "Colegio Mayor Loyola". After July 15, the accommodation is not guaranteed. B) For those who would like a three/four star hotel accommodation, we have made arrangements with "Grandes Rutas Travel", fax +34/91/543 35 50 Hotel "Tirol" (***) Room for 1 person, breakfast included, 8,800 pts + 7% VAT Room for 2 persons, breakfast for 2 persons included, 11,500 pts + 7% VAT Hotel "Conde Duque" (****) Room for 1 person, breakfast included, 11,600 pts + 7% VAT Room for 2 persons, breakfast for 2 persons included, 14,800 pts + 7% VAT If you want a hotel accommodation you have to fill in the hotel accommodation form and return in printed form via fax before July 15, 1999 to "Grandes Rutas Travel". If you have any problem in relation with your hotel accommodation please get in contact via telephone with Mauro Martin or Ana Garcia (+34/91/543 33 62). <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> CONFERENCE REGISTRATION FORM Please type out and return via fax with a copy of your bank remittance to CSL'99 attention of ms. Eva Ullan FAX +34/91/394 46 02 Surname ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ e-mail _____________________________________________________ Hereby please receive a copy of my bank transfer. Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> APPLYING FORM FOR A SUBSIDISED STUDENT REGISTRATION FEE Please type out and return via fax with a copy of your student certification to CSL'99 attention of ms. Eva Ullan FAX +34/91/394 46 02 I apply for a subsidised student certification fee. Surname ____________________________________________________ First Name(s) ________________________________________________ Affiliation ___________________________________________________ e-mail address________________________________________________ Hereby please receive a copy of my student certification. Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> TUTORIAL REGISTRATION FORM Please type out and return via fax with a copy of your bank remittance to CSL'99 attention of ms. Eva Ullan FAX +34/91/394 46 02 Surname ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ e-mail _____________________________________________________ Hereby please receive a copy of my bank transfer. Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> ACCOMMODATION FORM FOR COLEGIO MAYOR LOYOLA Please fill in and return before the July 15, 1999 via fax to CSL'99 "Colegio Mayor Loyola" attention of ms. Aurora fax +34/91/535 22 05 Surname(s) ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Arrival day ________________________________________________ Departure day ______________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> ACCOMMODATION FORM FOR "GRANDES RUTAS TRAVEL" Please fill in and return before the July 15, 1999 via fax to CSL'99 "Grandes Rutas Travel" attention of mr. Mauro Martin or Ana Garcia fax +34/91/543 35 50 Hotel _____________________________________________________ Surname(s) __________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ [ ] Single room [ ] Double room Arrival day ________________________________________________ Departure day ______________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ Signature: From cat-dist Tue Jul 6 17:17:20 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA05035 for categories-list; Tue, 6 Jul 1999 15:57:34 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 6 Jul 1999 13:25:14 -0500 (CDT) From: Hongseok Yang To: categories@mta.ca Subject: categories: Internal sheaf Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Does anyone help me to figure out what internal sheaf means? I mean, for any internal category (C0, C1, id, src, tgt, comp), there is a definition of a internal presheaf (also called category action). If it is, I want to know the canonical definition of an internal sheaf. Thanks in advance, Hongseok From cat-dist Thu Jul 8 17:02:19 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA29419 for categories-list; Thu, 8 Jul 1999 15:58:30 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Williams To: categories@mta.ca Subject: categories: Permanent position in foundations of computation Message-Id: Date: Wed, 7 Jul 1999 10:52:01 +0100 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: UNIVERSITY OF SUSEX SCHOOL OF COGNITIVE AND COMPUTING SCIENCES LECTURER (Grade A/B) - Foundations of Computer Science (Ref 131) Applications are invited for this position in Foundations of Computer Science. Candidates should be able to show evidence of significant research achievement in any aspect of the Foundations of Computation. The successful applicant will be expected to expand significantly the existing high research profile of the Group in this area. Applicants should also be willing to teach in areas of Computer Science other than their research speciality. Salary in the range: £16,655 - £21,815 per annum (Grade A) or £22,726 - £29,048 per annum (Grade B). Salaries under review. Closing date: Friday 13 August 1999. Informal enquiries may be made to Professor Matthew Hennessy, COGS, University of Sussex, Falmer, Brighton BN1 9QH, UK. Tel +44 1273 678101 Email matthewh@cogs.susx.ac.uk. Application forms and further particulars are available from and should be returned to Liz Showler, Staffing Services Office, Sussex House, University of Sussex, Falmer, Brighton BN1 9RH, UK. Tel +44 1273 877324 Email E.S.Showler@sussex.ac.uk. Details of the School are available at http://www.cogs.susx.ac.uk. Details of all posts can also be found via the website below. http://www.susx.ac.uk/Units/staffing An Equal Opportunity Employer From cat-dist Thu Jul 8 19:06:15 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id SAA07117 for categories-list; Thu, 8 Jul 1999 18:00:49 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: ramshaw@pa.dec.com Message-Id: <199907082050.AA20109@mercury.pa.dec.com> To: categories@mta.ca Subject: categories: an early exercise in Mac Lane Date: Thu, 08 Jul 1999 13:50:51 -0700 X-Mts: smtp Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I am puzzled by an exercise on page 15 of Mac Lane's classic text "Categories for the Working Mathematician": exercise 5 for section 3 of Chapter I: 5. Find two different functors T: Grp --> Grp with object function T(G) = G the identity for every group G. One such functor, of course, is the identity on every arrow as well. So the challenge is to find a functor that leaves all objects unchanged, but changes around at least some arrows. There is one easy way to do that, which may well be what Mac Lane had in mind as the solution to this exercise. For each group G, we choose some automorphism of G, say a_G. We then define our functor T to take the arrow f: G --> H to the arrow (a_H)^(-1) f a_G : G --> H. This preserves identities and compositions, so it does define a functor. But it seems like cheating, in a way. For one thing, this new functor is structurally the same as the identity functor. All that we've done is to change the scheme by which we name the elements of the various groups, using the automorphism a_G as our rule for renaming the elements of G. Note also that we haven't used any properties of the particular category Grp. This renaming technique would work equally well for Ab or Set. If renaming was what Mac Lane had in mind, why did he specify Grp in the exercise? I've spent some time trying to construct a more interesting solution to the exercise: a functor from Grp to Grp that leaves objects alone and transforms arrows in some way that clearly changes the structure. In particular, I started out hoping to take some non-null arrows to null arrows. For example, consider the homomorphism h : C_2 --> A_5 from the cyclic group C_2 to the alternating group A_5 that takes the lone non-identity element of C_2 to the permutation (12)(34). That permutation is even, and hence belongs to A_5; and it has order two, so the map h is a homomorphism. Initially, I thought that it would be pretty safe for my functor to map h to the null homomorphism. Note that A_5 is a simple group, so any homomorphism from A_5 to any other group has to be either injective or null -- there are no intermediate possibilities. But then I thought about situations like the following: C_2 ---> C_2 x G | | | h | (h, id) V V A_5 <--- A_5 x G The map on the top line takes t |--> (t, e) where e is the identity of G, while the map on the bottom line is the projection (s, u) |--> s. This diagram commutes before I apply my functor, and my functor presumably leaves the top and bottom arrows alone. If my functor takes the h on the left to the null homomorphism, it must also take the h component of the map (h, id) on the right to null; but it can't alter the id component of that map. So my functor has to take some arrows only partway to the null arrow. Given an arbitrary arrow, how far towards the null arrow should my functor take it? Finding a rule that works seems hard, even for direct products, not to mention semi-direct products and non-split extensions. Is there some interesting solution to this exercise that I am missing? Or did Mac Lane have the boring, renaming solution in mind? Thanks, Lyle Ramshaw From cat-dist Fri Jul 9 13:13:42 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA19917 for categories-list; Fri, 9 Jul 1999 11:26:56 -0300 (ADT) X-Authentication-Warning: math.ucr.edu: smap set sender to using -f From: baez@math.ucr.edu (john baez) Message-Id: <199907091339.GAA26491@charity.ucr.edu> Subject: categories: an early exercise in Mac Lane To: categories@mta.ca (categories) Date: Fri, 9 Jul 1999 06:39:25 -0700 (PDT) X-Mailer: ELM [version 2.4 PL24 PGP3 *ALPHA*] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Lyle Ramshaw writes: > 5. Find two different functors T: Grp --> Grp with object function > T(G) = G the identity for every group G. > > One such functor, of course, is the identity on every arrow as well. > So the challenge is to find a functor that leaves all objects > unchanged, but changes around at least some arrows. > I've spent some time trying to construct a more interesting solution > to the exercise: a functor from Grp to Grp that leaves objects alone > and transforms arrows in some way that clearly changes the structure. > In particular, I started out hoping to take some non-null arrows to > null arrows. I assume that by "null arrow" you mean what some folks call "the trivial homomorphism". Why not go all the way and consider the functor that leaves objects alone and maps all arrows to null arrows? Best, John Baez From cat-dist Sat Jul 10 11:23:07 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA27986 for categories-list; Sat, 10 Jul 1999 10:23:48 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Fri, 9 Jul 1999 16:05:05 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: categories Subject: categories: Re: an early exercise in Mac Lane Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I am afraid that does not work. You have to take an identity to an identity. The suggested conjugation by choosing an automorphism for each object does that. It may be the answer Mac Lane had in mind, although that works for any category, as noted. I cannot think of any other example. ------------------------------------------------------------------- If a society puts up with bad plumbers because plumbing is such a low calling, and if it puts up with bad philosophers because philosophy is such a high calling---then neither its pipes nor its theories will hold water. --- Slight paraphrase of former HEW secretary John Gardner On Fri, 9 Jul 1999, john baez wrote: > Lyle Ramshaw writes: > > > 5. Find two different functors T: Grp --> Grp with object function > > T(G) = G the identity for every group G. > > > > One such functor, of course, is the identity on every arrow as well. > > So the challenge is to find a functor that leaves all objects > > unchanged, but changes around at least some arrows. > > > I've spent some time trying to construct a more interesting solution > > to the exercise: a functor from Grp to Grp that leaves objects alone > > and transforms arrows in some way that clearly changes the structure. > > In particular, I started out hoping to take some non-null arrows to > > null arrows. > > I assume that by "null arrow" you mean what some folks call "the trivial > homomorphism". > > Why not go all the way and consider the functor that leaves objects > alone and maps all arrows to null arrows? > > Best, > John Baez > > > From cat-dist Sat Jul 10 16:28:11 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA16581 for categories-list; Sat, 10 Jul 1999 15:32:43 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sat, 10 Jul 1999 14:09:40 -0400 (EDT) Message-Id: <3.0.16.19990710141033.7b37ec5a@wesleyan.edu> X-Sender: flinton@wesleyan.edu X-Mailer: Windows Eudora Pro Version 3.0 (16) To: categories@mta.ca From: "Fred E.J. Linton" Subject: categories: New book (shameless commerce division) Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Participants of the recent AMS Special Session at Buffalo this past April may be interested to learn that the photos my wife Barbara snapped there have now been incorporated into a book, "This is Us ... at Buffalo." I'll be bringing a few pre-publication demo copies with me to the Coimbra SCTA summer school and CT99 conference later this month, in the hope of drumming up some sales. Cheers, -- Fred [E.J. Linton, aka ] From cat-dist Sat Jul 10 16:29:00 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA16888 for categories-list; Sat, 10 Jul 1999 15:32:21 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sat, 10 Jul 1999 14:02:48 -0400 (EDT) Message-Id: <3.0.16.19990710140340.7a0f4d1c@wesleyan.edu> X-Sender: flinton@wesleyan.edu X-Mailer: Windows Eudora Pro Version 3.0 (16) To: categories@mta.ca From: "Fred E.J. Linton" Subject: categories: Re: an early exercise in Mac Lane Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: At 01:50 PM 7/8/99 -0700, Lyle Ramshaw was > ... puzzled by an exercise on page 15 of Mac Lane's classic text ... I have three remarks to add to this discussion. The first is more of a confession: for nigh onto thirty years I seem to have misread this problem, thinking what it sought was a functor Grp ---> Grp commuting with the underlying-set functors, like the passage from a group to its opposite. I now stand, belatedly, corrected. Second (and surely others will be chiming in on this point too), Baez's suggestion to trivialize all homomorphisms can't work -- you can't be a functor if you trivialize identity maps. Finally, the sort of example Mac Lane probably had in mind for an exercise on such an early page as p. 15: writing t for the only non-identity automorphism (an central involution, actually) of, say, the chosen group G = Z (or of G = Z/3Z , if you prefer), define T: Grp ---> Grp as follows: T(X) = X , whatever the group X , and, for f: X --> Y in Grp , set + - | f , if either X = G = Y or neither X nor Y is G ; T(f) = | ft , if only X = G ; | tf , if only Y = G . + - (This ASCII graphic works best if you display it in a fixed-width font.) I'll spare CATEGORIES readers the straightforward details of the checking that T really is a functor. But I'll add the aside that there's nothing special about the choices of G and t above, beyond G being a group and t being a central, involutive automorphism of G . Even "involutive" isn't really needed, except for the typographical convenience, here in ASCII-land, of not having to compose a " t-inverse " with f in *one* (but, please, *not* in the other) of the last two lines of the definition of T(f) :-) . Cheers, -- Fred [E.J. Linton, aka From cat-dist Sun Jul 11 03:39:08 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA04746 for categories-list; Sat, 10 Jul 1999 20:50:31 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Sat, 10 Jul 1999 15:03:48 -0400 (EDT) From: Michael Barr Subject: categories: *-autonomous non-category X-Sender: barr@triples.math.mcgill.ca To: Categories list Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Peter Freyd has talked, maybe written, about a cartesian closed non-category. I have a *-autonomous non-category. I wonder if this rings any bells with anyone. In order to talk about it on this unforgiving medium, I will use the following notation: 2^X for the powerset of X, \/ and /\ for union and intersection, resp. ~Y for the complement of Y (in X), T for the top and I for the bottom of the lattice 2^2^X. Now, the objects of this non-catgory are the upclosed subsets of 2^X. I will use a, b, c, ... for upclosed subsets of 2^X and Y, Z, W, ... for subsets of X. Given a, let a* denote the { Y | ~Y is in ~a }. So Y is in a* iff the complement of Y is not in X. These Y can also be characterized as meeting every set in a (which is obviously upclosed). It is the case that a** = a. Moreover, if we define a --o b = a* \/ b, we get something like an internal hom. What about composition? Well, first, what about identities. The sets of the form a --o a = a* \/ a are characterized by the property that for any Y, either Y or ~Y is in it. That is, a* \/ a has this property and if b has this property, then b contains b*, so b = b* \/ b. It is not hard to show that (a \/ b)* = a* /\ b* and vice versa, so that the tensor product should be /\. The unit for the tensor product is thus T, so there wants to be a map T --> a as soon as for each Y, either Y or ~Y is in a. Let me call such a set large. An interesting observation is that ((a --o b) /\ (b --o c)) --o (a --o c) is large, so it looks like we have a category if we define there to be an arrow a --> b whenever a --o b is large. Unfortunately, despite the internal composition above, there is no external composition. In fact, call a small if a* is large. The same reason there is a map T --> a when a is large forces there to be a map a --> I (the empty set) when a is small. But the principal ultrafilter at any x in X is both large and small (it is self-dual), so there is both T --> a and a --> I. Needless T --o I is not large (it is I). So that is it. There is a graph, not closed under composition, but there is an internal composition. I suppose I should check if there is an arrow ((a --o b) /\ (b --o c) /\ (c --o d)) --> (a --o d) and so on but I'll bet there is. (The binary composition involves 64 cases and I wrote a simple computer program to check them. This one would requre 256 and while there is no problem extending it to that number, there needs to be a new idea to do it for an arbitrary number of factors. Of course, one way of making a category is to make all objects isomorphic, with internal structure that separates them. This seems perverse, since the whole idea of categories is that isomorphic objects should not be distinguishable. Michael ------------------------------------------------------------------- If a society puts up with bad plumbers because plumbing is such a low calling, and if it puts up with bad philosophers because philosophy is such a high calling---then neither its pipes nor its theories will hold water. --- Slight paraphrase of former HEW secretary John Gardner From cat-dist Tue Jul 13 08:23:08 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id GAA06304 for categories-list; Tue, 13 Jul 1999 06:44:52 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3789F9EC.3A638DE6@unidhp1.uni-c.dk> Date: Mon, 12 Jul 1999 16:21:32 +0200 From: Anton Antonov Organization: UNI-C, Denmark X-Mailer: Mozilla 4.04 [en] (X11; I; AIX 4.3) MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Category theory for Mathematica -> HPF Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Hi, Recently I presented in the Hewlett Packard conference HiPer'99 the paper "Translating Mathematica expressions to High Performance Fortran" with the following abstract: This paper introduces some ideas for translating the functional language Mathematica to the data-parallel language High Performance Fortran (HPF). It first discusses why we have the ability to do that. Then it gives some interpretations by Category Theory. Third the translating approach is presented for different Mathematica expressions that could be interpreted as specifications for parallel independence, reduction, task parallelism and subprogram's data mapping. Last is shown a simple executable program generated by the translator. You can find more about that on http://www.imm.dtu.dk./~aaa/MathematicaToHPF.html . I am glad that Category theory exists! With it I was able to express that Functional, Object-oriented and Parallel programing are the same kind of management. Regards Anton From cat-dist Thu Jul 15 13:12:17 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA31927 for categories-list; Thu, 15 Jul 1999 10:57:22 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 15 Jul 1999 10:43:56 +0200 From: Philippe Gaucher Message-Id: <199907150843.AA01264@irmast1.u-strasbg.fr> To: categories@mta.ca Subject: categories: Maple program for cubical categories ? Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-Md5: /AfxONXzx0Uk8JWtuIQGMA== Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Bonjour, I have calculations to do in a cubical omega-category (see works of Brown, Higgins, etc... for the definition). I have to verify some equalities. I am wondering whether there is a program (Maple, anything else) in order to simplify automatically expressions containing only the usual operators like the three families of degeneracy maps of a cubical set with connections, operations +_j, and the usual face maps. Every composition of degeneracy maps and face maps can be ordered with the degeneracy maps of the cubical sets in the first place (in a canonical order), followed by the connection maps, followed by the face maps. But I do not see a canonical way to deal with +_j (because of the interchange law for example). pg. From cat-dist Thu Jul 15 13:21:17 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA30107 for categories-list; Thu, 15 Jul 1999 10:53:37 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 14 Jul 1999 18:03:06 +0200 From: Eva Ullan Subject: categories: CSL99 Programme and Call for Participation 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 NAA17550 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ____________________________________________________ My apologies if you receive this more than once! ____________________________________________________ ------------------------------------------------------------- PROGRAMME AND CALL FOR PARTICIPATION CSL'99 Annual Conference of the European Association for Computer Science Logic (EACSL) Madrid, Spain, September 20-25, 1999 ------------------------------------------------------------- http://mozart.sip.ucm.es:1580/csl99/ ________________________________________ ***EARLY REGISTRATION DEADLINE*** July 15, 1999 ________________________________________ The 1999 Annual Conference of the European Association for Computer Science Logic follows previous CSL Conferences: CSL'98 (Brno, Czech Republic), CSL'97 (Aarhus, Denmark), CSL'96 (Utrecht, The Netherlands), CSL'95 (Paderborn, Germany), CSL'94 (Kazimierz, Poland), CSL'93 (Swansea, United Kingdom), CSL'92(San Miniato, Italy), CSL'91 (Berne, Switzerland), CSL'90 (Heidelberg, Germany), CSL'89 (Kaiserslautern, Germany), CSL'88 (Duisburg, Germany), and CSL'87 (Karlsruhe, Germany). CSL'99 will be held in Madrid (Spain). The event is organized jointly by the Computer Science Departments (DSIP and DACYA) of Universidad Complutense de Madrid (UCM). The scientific program includes 34 selected papers from among 91 submissions, five invited lectures, and two tutorials on theorem proving and rewriting techniques, scheduled on September 24 afternoon (Friday) and September 25 morning (Saturday), immediately after the main conference. In addition to the scientific program, the social program includes an excursion to Segovia (a nearby historic city), and a conference dinner. Madrid offers the opportunity to enjoy both Spain and one of the most attractive capitals in Europe. In this document you can find the Invited Lecturers, Tutorials, Scientific Programme, General Information, Registration and Accommodation Information. The CSL'99 Web page http://mozart.sip.ucm.es:1580/csl99/ contains additional information. -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- INVITED LECTURERS: Jose Luis Balcazar - Universidad Politecnica Cataluna The consistency dimension, compactness, and query learning Javier Esparza - Technische Universitat Munchen Partial order semantics help Martin Grohe - Albert-Ludwig-Universitat Freiburg Descriptive and Parametrized Complexity Peter D. Mosses - University of Aarhus Logical specification of operational semantics Victor Vianu - University California San Diego Topological Queries in Spatial Databases TUTORIALS: Douglas J. Howe - Bell Labs Interactive Theorem Proving using Type Theory Aart Middeldorp - University of Tsukuba Term Rewriting PRELIMINARY SCIENTIFIC PROGRAMME: Monday 20th, September 9:00 Registration 9:45 Conference Opening 10:00 Invited Talk: V. Vianu Topological Queries in Spatial Databases 11:00 Coffee Break Session 1: Descriptive Complexity 11:20 E. Gradel and S. Kreutzer Descriptive complexity theory for constraint databases 11:50 D. Leivant Applicative control and computational complexity 12:30 Lunch Session 2: Verification 14:00 T. Arts and J. Giesl Applying Rewriting Techniques for Verification of Erlang Processes 14:30 J. Moller, J. Lichtenberg, H.R. Andersen and H. Hulgaard Difference Decision Diagrams 15:00 M. Fraenzle Analysis of Hybrid Systems: An ounce of realism can save an infinity of states 15:30 Y. Kesten and A. Pnueli Can Abstraction Replace Deduction? 16:00 Coffee break 16:30 EACSL Assembly Tuesday 21st, September 9:00 Invited Talk: J.L. Balcazar The consistency dimension, compactness, and query learning Session 3: Temporal Logic 10:30 T.M. Rasmussen Signed Interval Logic 11:00 Coffe break 11:20 Y. Hirshfeld and A. Rabinovich Quantitative Temporal Logic 11:50 V. Diekert and P. Gastin An expressively complete temporal logic without past tense operators for Mazurkiewicz traces 12:30 Lunch Session 4: Lambda Calculus, Linear Logic 14:00 E. Bonelli Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting 14:30 M. Fernandez and I. Mackie Closed Reductions in the lambda-calculus 15:00 S. Ishtiaq and D.J. Pym Kripke resource models of a dependently-typed, bunched lambda-calculus 15:30 R. Di Cosmo and V. Balat A linear logic view of linear type isomorphisms 16:00 Coffee break Session 5: Logic Programming, Modal Logic, Description Logic 16:30 M. De Vos and D. Vermeir Choice logic programs and Nash equilibria in strategic games 17:00 S. Hagihara and N. Yonezaki Resolution Method for Modal Logic with Well-founded Frames 17:30 S. Tobies A NExpTime-complete Description Logic Strictly Contained in C^2 18:00 C. Areces, P. Blackburn and M. Marx A Road-map on Complexity for Hybrid Logics Wednesday 22th, September 9:30 Invited talk: M. Grohe Descriptive and Parametrized Complexity Session 6: Descriptive Complexity 10:30 C. Lautemann and B. Weinzinger Monadic NLIN and quantifier-free reductions 11:00 Coffe break 11:20 J. Marcinkowski Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraise games 11:50 J.C. Bradfield Fixpoint alternation and the game quantifier 12:30 Lunch 13:30 Excursion to Segovia Thursday 23rd, September 9:30 Invited talk: P. Mosses Logical specification of operational semantics Session 7: Logic and Complexity 10:30 J. Toran Lower Bounds for Space in Resolution 11:00 Coffe break 11:20 I.A. Stewart Program schemes, arrays, Lindstrom quantifiers and zero-one laws 11:50 L.D. Beklemishev Open least element principle and bounded query computation 12:30 Lunch Session 8: Lambda Calculus, Type Theory 14:00 A.D. Ker, H. Nickau and C.H.L. Ong More Universal Game Models of Untyped Lambda-Calculus: The Bohm Tree Strikes Back 14:30 A. Compagnoni and H. Goguen Anti-Symmetry of Higher-Order Subtyping 15:00 H. Geuvers, E. Poll and J. Zwanenburg Safe Proof Checking in Type Theory with Y 15:30 T. Altenkirch and B. Reus Monadic presentations of lambda terms using generalized inductive types 16:00 Coffee break Session 9: Linear Logic, Mu Calculus, Concurrency 16:30 L. Roversi A Proof of Completeness for Light Logics 17:00 H. Seidl and A. Neumann On Guarding Nested Fixpoints 17:30 A. Kucera and J. Esparza A Logical Viewpoint on Finite-State Descriptions of Processes 18:00 P. Gastin and M. Mislove A Truly Concurrent Semantics for a Simple Parallel Programming Language Friday 24th, September 9:30 Invited talk: J. Esparza Partial order semantics help Session 10: Specification, Data Refinement 10:30 J.E. Hannay Specification Refinement with System F 11:00 Coffe break 11:20 F. Honsell and D. Sannella Pre-logical Relations 11:50 Y. Kinoshita and J. Power Data-refinement for call-by-value programming languages 12:20 Conference Closure 12:30 Lunch 14:30 A. Middeldorp Tutorial on Term Rewriting, 1st part 16:00 Coffee break 16:30 Tutorial on Term Rewriting, 2nd part Saturday 25th, September 9:30 D. Howe Tutorial on Interactive Theorem Proving using Type Theory, 1st part 11:00 Coffee break Tutorial on Interactive Theorem Proving using Type Theory, 2nd part -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- * PROGRAMME COMMITTEE 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) Martin Wirsing (Munich, Germany) * 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) * LOCAL ORGANIZING COMMITTEE J. Carlos Gonzalez-Moreno Teresa Hortala-Gonzalez Javier Leach-Albert (chair) Paco Lopez-Fraguas Fernando Saenz-Perez Eva Ullan-Hernandez * SPONSORED BY Comision Interministerial de Ciencia y Tecnologia (CICYT) European Research Consortium for Informatics and Mathematics (ERCIM) Esprit Working Group EP 22457 (CCL II) UCM Department 'Arquitectura de Computadores y Automatica' (DACYA) UCM Department 'Sistemas Informaticos y Programacion' (DSIP) UCM Faculty of Mathematics UCM Technical Highschool of Informatics UCM Vicerrectorado de Investigacion UCM Vicerrectorado de Relaciones Internacionales * Organized by SIP-UCM and DACYA-UCM -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- GENERAL INFORMATION Place and travel The Conference will be held in Madrid (Spain), at the Faculty of Mathematics of Universidad Complutense de Madrid (UCM), from the 20th to the 25th of September, 1999. Madrid has direct flights from most major cities and generally good connections from elsewhere. Barajas, the international Madrid airport, is only about 10 km from the city. There are frequent regular buses and taxis to the city, as well as the new metropolitan line. The Faculty of Mathematics can be reached by metro (metropolitan station Ciudad Universitaria or Metropolitano) or by bus (bus lines 132, F, or 82). The CSL'99 Web page (http://mozart.sip.ucm.es:1580/csl99/) contains additional information such as the metropolitan network map, and the surroundings to CSL host site map. Social Events A guided excursion to Segovia will be held on Wednesday, 22th. The departure will be after lunch, at 14:00. Registered participants have this excursion included, and accompanying persons can buy an excursion ticket (60 euros) during the Registration and Opening Session to CSL'99. The excursion includes dinner. Languages English is the Conference official language. -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- REGISTRATION INFO CSL'99 Registration to the Conference and/or Tutorial must be made sending the Conference Registration Form and/or the Tutorial Registration Form and a copy of your corresponding bank transfer (via fax) directly to: CSL'99 attention of ms. Eva Ullan fax +34/91/394 46 02 Electronic mail registration will not be accepted The conference registration fee includes: - admission to the conference - morning and afternoon coffee breaks during the conference - lunches during the conference - excursion and social event - a copy of the proceedings volume - one year subscription to EACSL The tutorial registration fee includes: - admission to the tutorials - afternoon and morning coffee breaks during the tutorials - working material EARLY CONFERENCE REGISTRATION FEE: 270 EUROS. For early registration, the registration form together with a copy of your bank remittance must reach us by July 15, 1999 LATE CONFERENCE REGISTRATION FEE: 300 EUROS. After July 15, 1999 TUTORIAL REGISTRATION FEE: 60 EUROS For early tutorial registration, the tutorial registration form with a copy of your bank remittance must reach us by July 15, 1999 LATE TUTORIAL REGISTRATION FEE: 80 EUROS. After July 15, 1999 Payments should be made in EURO currency by bank transfer WITHOUT CHARGES FOR THE BENEFICIARY payable to: CAJA DE MADRID Donoso Cortes 80 28015 MADRID FUNDACION GENERAL UCM (CSL'99) Account: 2038/1735/09/2000001375 Do not forget the specification CSL'99 !!! -*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*- ACCOMMODATION INFO CSL'99 A) For those who would like a simple accommodation lodging in a student room, we have made arrangements with "Colegio Mayor Loyola", Paseo Juan XXIII 17, 28040 MADRID, SPAIN, Fax +34/91/535 22 05 In "Colegio Mayor Loyola" the price for single rooms, full board, is 4,600 pts + 7% VAT per day (27.646 EUROS + 7% VAT) If you want a "Colegio Mayor Loyola" accommodation you have to fill in the accommodation form and return in printed form via fax before July 15, 1999 to "Colegio Mayor Loyola". After July 15, the accommodation is not guaranteed. B) For those who would like a three/four star hotel accommodation, we have made arrangements with "Grandes Rutas Travel", fax +34/91/543 35 50 Hotel "Tirol" (***) Room for 1 person, breakfast included, 8,800 pts + 7% VAT Room for 2 persons, breakfast for 2 persons included, 11,500 pts + 7% VAT Hotel "Conde Duque" (****) Room for 1 person, breakfast included, 11,600 pts + 7% VAT Room for 2 persons, breakfast for 2 persons included, 14,800 pts + 7% VAT If you want a hotel accommodation you have to fill in the hotel accommodation form and return in printed form via fax before July 15, 1999 to "Grandes Rutas Travel". If you have any problem in relation with your hotel accommodation please get in contact via telephone with Mauro Martin or Ana Garcia (+34/91/543 33 62). <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> CONFERENCE REGISTRATION FORM Please type out and return via fax with a copy of your bank remittance to CSL'99 attention of ms. Eva Ullan FAX +34/91/394 46 02 Surname ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ e-mail _____________________________________________________ Hereby please receive a copy of my bank transfer. Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> TUTORIAL REGISTRATION FORM Please type out and return via fax with a copy of your bank remittance to CSL'99 attention of ms. Eva Ullan FAX +34/91/394 46 02 Surname ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ e-mail _____________________________________________________ Hereby please receive a copy of my bank transfer. Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> ACCOMMODATION FORM FOR "COLEGIO MAYOR LOYOLA" Please fill in and return before the July 15, 1999 via fax to CSL'99 "Colegio Mayor Loyola" attention of ms. Aurora fax +34/91/535 22 05 Surname(s) ____________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ Affiliation ________________________________________________ Arrival day ________________________________________________ Departure day ______________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ Signature: <><><><><><><><><><><><> Cut here <><><><><><><><><><><><> ACCOMMODATION FORM FOR "GRANDES RUTAS TRAVEL" Please fill in and return before the July 15, 1999 via fax to CSL'99 "Grandes Rutas Travel" attention of mr. Mauro Martin or Ana Garcia fax +34/91/543 35 50 Hotel _____________________________________________________ Surname(s) __________________________________________________ First Name(s) ______________________________________________ Mr/Ms + Title ______________________________________________ [ ] Single room [ ] Double room Arrival day ________________________________________________ Departure day ______________________________________________ Home or Work Address: Street _____________________________________________________ Code, City _________________________________________________ Country ____________________________________________________ Signature: From cat-dist Thu Jul 15 14:12:56 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA13889 for categories-list; Thu, 15 Jul 1999 12:46:54 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 15 Jul 1999 16:32:22 +0100 (BST) From: Ronnie Brown X-Sender: mas010@publix To: categories@mta.ca Subject: categories: Re: Maple program for cubical categories ? In-Reply-To: <199907150843.AA01264@irmast1.u-strasbg.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: This is a very sophisticated problem, involving rewrite theory. Without the compositions, and with only one connection, there is work in 86. (with A.P.TONKS), ``Calculations with simplicial and cubical groups in AXIOM'', {\em J. Symbolic Computation}, 17 (1994) 159-179. But AXIOM is not the easiest to get working for you! I have not looked at this for a long time. The difficulties of using the interchange rule are quickly seen by considering pre crossed and crossed modules. We actually did some calculations of induced crossed modules in 92. (with C.D.WENSLEY), ``On finite induced crossed modules and the homotopy 2-type of mapping cones'', {\em Theory and Applications of Categories} 1(3) (1995) 54-71. 95. (with C.D.WENSLEY), ``Computing crossed modules induced by an inclusion of a normal subgroup, with applications to homotopy 2-types'', {\em Theory and Applications of Categories} 2 (1996) 3-16. There is more on rewriting in Heyworth-Wensley Mathematics, abstract math.CO/9907082 Logged Rewriting Procedures with Application to Identities Among Relations I thoroughly appreciate the need! Ronnie Brown On Thu, 15 Jul 1999, Philippe Gaucher wrote: > Bonjour, > > I have calculations to do in a cubical omega-category > (see works of Brown, Higgins, etc... for the definition). > I have to verify some equalities. > I am wondering whether there is a program (Maple, anything else) > in order to simplify automatically expressions containing > only the usual operators like the three families of degeneracy > maps of a cubical set with connections, operations +_j, and the > usual face maps. > > Every composition of degeneracy maps and face maps can be > ordered with the degeneracy maps of the cubical sets in the > first place (in a canonical order), followed by the connection > maps, followed by the face maps. But I do not see a canonical > way to deal with +_j (because of the interchange law for example). > > > pg. > 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 Jul 16 16:14:45 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA13626 for categories-list; Fri, 16 Jul 1999 14:25:17 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199907151732.NAA17230@babar.INS.CWRU.Edu> Date: Thu, 15 Jul 1999 13:32:06 -0400 (EDT) X-Sender: cxm7@pop.cwru.edu X-Mailer: Windows Eudora Version 1.4.4 Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" To: categories@mta.ca From: cxm7@po.cwru.edu (Colin McLarty) Subject: categories: Mac Lane's inclusions Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: This note gives an alternative characterization of "inclusions" in Mac Lane's sense; and proves every category with selected monics is equivalent to one with "inclusions". Some of it may have been known before and if so I would appreciate references. In a circular letter Saunders Mac Lane has suggested paying attention to "inclusions" in categorical set theory. The main questions about this have general categorical answers as follows. A category has "selected monics" if for each object C, each equivalence class of monics to C has one selected representative. The selected monics are called "inclusions" if whenever C'>->C and C">->C' are selected, the composite C">->C is also selected. The following alternative characterization motivates the construction in the next theorem but is not actually used to prove it. Given monics i and j to a single object, with i->C and j:J>->C are selected, and selected monics compose. The transition h must have some selected equivalent k:K>->J, and so jk is selected and equivalent to i, which implies jk=i and k=h so h is selected. Conversely suppose h:I>->J and j:J>->C are selected and transition monics between selected monics are selected. Then jh:I>->C has some selected equivalent m and for some iso g we have jhg=m. Thus hg is transition monic between the selected m and j, and so hg is selected. But hg is also equivalent to the selected h so hg=h and g is an identity. Thus jh=m is selected. In any topos with selected pullbacks we have selected monics, since for any equivalence class of monics we can take the selected pullback of "true" along the characteristic arrow. These need not be inclusions. However, we have: Theorem: Any category A with selected monics is equivalent to a category AI with inclusions. Proof: Let the objects of AI be the selected monics C>->B of A. An AI arrow from C'>->B' to C>->B is simply an A arrow C'-->C. That is, AI arrows ignore the monics and just look at the domains. Obviously AI is equivalent to A and an arrow is monic in AI iff it is monic in A. As the selected monics to an AI object C>->B we take those AI monics h h:C'>-------->C v v | | | | v v B = B which lie over the same B and make the triangle commute in A. Clearly these compose, and each monic to C>->B in AI is equivalent to exactly one of these. In particular, given any axiomatic theory of a topos with selected pullbacks: if the axioms are preserved by equivalence, then we can consistently add the assumption of inclusions. We can assume selected monics compose. Of course it remains to actually use this assumption to secure the advantages that Saunders sees for it. From cat-dist Mon Jul 19 13:07:55 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA09144 for categories-list; Mon, 19 Jul 1999 11:52:17 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <19990716195548.73188.qmail@hotmail.com> X-Originating-IP: [131.107.3.74] From: "Bill Halchin" To: categories@mta.ca Subject: categories: co-exponential question Date: Fri, 16 Jul 1999 12:55:48 PDT Mime-Version: 1.0 Content-Type: text/plain; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: This is actually a "dual" question. Basically I want to do the dual of the construction gives the notion of an exponential or map object. Suppose we have a category C with sums. Then we build the following category from C. object: T+X<-----Y map: from T+X<-----Y to T+X'<-------Y is a C map "alpha" such that we have the following diagram: I-sub-T+alpha T+X---------------------------->T+X' ^ ^ \ / \ / \ / \ / \ / \ / \ / \ / \ / \ / \ / \ / \ / \ / \/ Y Then suppose there exists a C-object called Y**T such that T+Y**T<-------Y is the initial object of the category just built above. What significance does Y**T have opposed to the concept of an exponential???? If I did everything correctly it (Y**T) should be the dual of T**Y. Regards, Bill Halchin From cat-dist Mon Jul 19 13:12:41 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA11011 for categories-list; Mon, 19 Jul 1999 11:56:34 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <01BECFE0.BB5BEBA0.robert.mcgrail@marist.edu> From: "Robert W. McGrail" Reply-To: "robert.mcgrail@marist.edu" To: "categories@mta.ca" Subject: categories: RE: Mac Lane's inclusions Date: Fri, 16 Jul 1999 23:11:58 -0500 Organization: Marist College X-Mailer: Microsoft Internet E-mail/MAPI - 8.0.0.4211 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Colin, Correct me if I am wrong, but it seems to me that every \tau-category is a category with inclusions. Moreover, I recall a result by Freyd that every (sufficiently small? cartesian?) category is equivalent to a \tau-category. The proof does not use choice. In any event, see Categories, Allegories by Freyd and Scedrov for \tau-categories. Hope this helps. Bob McGrail On Thursday, July 15, 1999 12:32 PM, Colin McLarty [SMTP:cxm7@po.cwru.edu] wrote: > This note gives an alternative characterization of "inclusions" in Mac > Lane's sense; and proves every category with selected monics is equivalent > to one with "inclusions". Some of it may have been known before and if so I > would appreciate references. > > In a circular letter Saunders Mac Lane has suggested paying attention to > "inclusions" in categorical set theory. The main questions about this have > general categorical answers as follows. A category has "selected monics" if > for each object C, each equivalence class of monics to C has one selected > representative. The selected monics are called "inclusions" if whenever > C'>->C and C">->C' are selected, the composite C">->C is also selected. > > The following alternative characterization motivates the construction in > the next theorem but is not actually used to prove it. Given monics i and j > to a single object, with i "transition monic" from i to j. (For e-mail convenience I write i i is included in or equal to j.) > > Fact: In any category with selected monics, the selected monics are > inclusions if and only if: for all selected monics i and j with i transition monic h is also selected. > > Proof: First suppose i:I>->C and j:J>->C are selected, and selected monics > compose. The transition h must have some selected equivalent k:K>->J, and so > jk is selected and equivalent to i, which implies jk=i and k=h so h is > selected. Conversely suppose h:I>->J and j:J>->C are selected and transition > monics between selected monics are selected. Then jh:I>->C has some selected > equivalent m and for some iso g we have jhg=m. Thus hg is transition monic > between the selected m and j, and so hg is selected. But hg is also > equivalent to the selected h so hg=h and g is an identity. Thus jh=m is > selected. > > > In any topos with selected pullbacks we have selected monics, since for any > equivalence class of monics we can take the selected pullback of "true" > along the characteristic arrow. These need not be inclusions. However, we > have: > > Theorem: Any category A with selected monics is equivalent to a category AI > with inclusions. > Proof: Let the objects of AI be the selected monics C>->B of A. An AI > arrow from C'>->B' to C>->B is simply an A arrow C'-->C. That is, AI arrows > ignore the monics and just look at the domains. Obviously AI is equivalent > to A and an arrow is monic in AI iff it is monic in A. As the selected > monics to an AI object C>->B we take those AI monics h > > h:C'>-------->C > v v > | | > | | > v v > B = B > > which lie over the same B and make the triangle commute in A. Clearly these > compose, and each monic to C>->B in AI is equivalent to exactly one of these. > > In particular, given any axiomatic theory of a topos with selected > pullbacks: if the axioms are preserved by equivalence, then we can > consistently add the assumption of inclusions. We can assume selected monics > compose. Of course it remains to actually use this assumption to secure the > advantages that Saunders sees for it. > > From cat-dist Tue Jul 20 08:52:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id HAA01355 for categories-list; Tue, 20 Jul 1999 07:14:50 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <19990719150943.3947.rocketmail@web105.yahoomail.com> Date: Mon, 19 Jul 1999 11:09:43 -0400 (EDT) From: Nikita Danilov Subject: categories: universal property of tangent bundle To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Dear category people, Given an object M in the ``normal'' category of finitely dimensional smooth manifolds Man (not in SDG sense), what it the universal property of the tangent bundle TM? So far, I found only the following: For every manifold M there is a functor F:I -> Man0, where Man0 is category of open areas in R^n and smooth mapping, such that M=Colim F, F corresponding to the atlas on M and M is represented as a result of gluing instances of R^n in the atlas. This functor can be trivially modified (by multiplying its values on objects on R^n and modifying morphisms appropriately) to get functor TF:I -> Man0, such that TM=Colim TF. But this doesn't seem satisfactory because: 1. Construction of TF follows one particular construction of TM as a set of triples (x,(U,f),h) where x \in U, (U,f) is in atlas and h \in R^n with appropriate points identified. 2. I hope there should be universal construction with \pi: TM -> M as universal arrow. 3. As tangent bundle is so ubiquitous there should be nice universal property for it. With regards, N. Danilov. From cat-dist Tue Jul 20 09:00:27 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id HAA29969 for categories-list; Tue, 20 Jul 1999 07:22:10 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199907191945.PAA22541@babar.INS.CWRU.Edu> Date: Mon, 19 Jul 1999 15:45:29 -0400 (EDT) X-Sender: cxm7@pop.cwru.edu X-Mailer: Windows Eudora Version 1.4.4 Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" To: categories@mta.ca From: cxm7@po.cwru.edu (Colin McLarty) Subject: categories: RE: Mac Lane's inclusions Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Robert W. McGrail wrote: >Correct me if I am wrong, but it seems to me that every \tau-category is a >category with inclusions. Moreover, I recall a result by Freyd that every >(sufficiently small? cartesian?) category is equivalent to a \tau-category. > The proof does not use choice. There is certainly a similarity. Tau categories are cartesian categories (categories with all finite limits) which not only have selected monics but also selected jointly-monic n-tuples for all finite n; and all these things compose. Freyd shows every cartesian category is equivalent to a tau category. My construction seems very like Peter's but shortened by working only on monics and not jointly monic lists, and never using limits. best, Colin From cat-dist Tue Jul 20 14:44:27 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA04661 for categories-list; Tue, 20 Jul 1999 13:23:37 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Thomas Streicher Message-Id: <199907201218.AA014623080@fb0448.mathematik.tu-darmstadt.de> Subject: categories: Position To: categories@mta.ca Date: Tue, 20 Jul 1999 14:18:00 +0200 (MESZ) X-Mailer: ELM [version 2.4ME+ PL47 (25)] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: A position of a Professor (C3) is advertised at the Department of Mathematics, Darmstadt University of Technology, in the area of Mathematical Foundations of Computer Science. Deadline for Applications: September 3, 1999. For details see http:// www.mathematik.tu-darmstadt.de/Math-Net/Dekanat/Ausschreibungen/c3_de.html Thomas Streicher From cat-dist Tue Jul 20 15:08:21 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA07442 for categories-list; Tue, 20 Jul 1999 13:20:20 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3794E2AC.425B@latrobe.edu.au> Date: Tue, 20 Jul 1999 13:57:18 -0700 From: William James X-Mailer: Mozilla 3.04 (Win16; I) MIME-Version: 1.0 To: Bill Halchin CC: categories@mta.ca Subject: categories: Re: co-exponential question References: <19990716195548.73188.qmail@hotmail.com> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Bill Halchin wrote: > > This is actually a "dual" question. > Basically I want to do the dual of the construction > gives the notion of an exponential or map object. > > Suppose we have a category C with sums. Then we build the > following category from C. > > object: T+X<-----Y > > map: from T+X<-----Y to T+X'<-------Y is a C map "alpha" such > that we have the following diagram: > > I-sub-T+alpha > T+X---------------------------->T+X' > ^ ^ > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \ / > \/ > Y > > Then suppose there exists a C-object called Y**T such > that T+Y**T<-------Y is the initial object of the category > just built above. What significance does Y**T have opposed > to the concept of an exponential???? If I did everything > correctly it (Y**T) should be the dual of T**Y. Forgive my ignorance: is T+Y**T<----Y to be initial because the usual construction for the exponential has the relevant arrow as terminal? Can you suggest to me a reference for that construction of exponentials? As for significance: my own research into co-exponentials is in terms of them as characteristic of lattices dual to Heyting algebras. These dual-Heyting algebras work well as algebras for a brand of paraconsistent logic (they have a complement operator which has in general that an element and its complement overlap). Alternatively, you can think of co-exponentials as productive of the interesting topological notions associated with closed sets, like boundary. My feeling is that co-exponentials count as useful in more interesting kinds of maths than turn up simply in those categories dual to toposes. William James From cat-dist Tue Jul 20 15:09:43 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA06851 for categories-list; Tue, 20 Jul 1999 13:14:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: exmh version 2.0.2+CL 2/24/98 To: categories@mta.ca Subject: categories: British Logic Colloquium 1999 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Mon, 19 Jul 1999 12:32:28 +0100 From: Anuj Dawar Message-Id: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: British Logic Colloquium 1999 - Second Announcement - The 1999 meeting of the British Logic Colloquium will be held from 23 to 25 September at the University of Wales conference centre, Gregynog. Programme --------- The meeting will include a celebration of Roger Hindley's contributions to logic, on the occasion of his retirement from the Department of Mathematics at the University of Wales Swansea. In addition, there will be lectures covering a wide variety of areas of mathematical and philosophical logic as well as the history of logic. The provisional programme is: Thursday 23 September --------------------- 1:00pm Lunch 2:00pm Robin Milner (Cambridge) What is the Logic of Communication? 3:00pm Giuseppe Longo (CNRS and ENS, Paris) Prototype Proofs and Genericity in Type Theories 4:00pm Tea 4:30pm Roger Hindley (Swansea) Curry's Last Problem, Imitating Lambda-beta-reduction in Combinatory Logic 6:00pm BLC General Meeting. 7:00pm Dinner Friday, 24 September -------------------- 8:00am Breakfast 9:00am Henk Barendregt (Nijmegen) The Perpendicular Lines Lemma for Lambda Terms and Boehm Trees 10:00am Mariangiola Dezani (Turin) Intersection Types and Properties of Lambda Terms 11:00am Coffee 11:45am Jonathan Seldin (Concordia) Roger Hindley's work on Lambda-calculus and Combinatory Logic 1:00pm Lunch 2:00pm Ivor Grattan-Guinness (Middlesex) The Reception of 'Principia Mathematica' in Britain and Abroad, 1913-1935 3:00pm David Miller (Warwick) Some Neglected Work in General Metamathematics 4:00pm Tea 4:30pm Mirna Dzamonja (East Anglia) Cardinal Spectra 7:00pm Banquet in honour of Roger Hindley, Saturday, 25 September ---------------------- 8:00am Breakfast 9:00am Richard Kaye (Birmingham) A Nonstandard Approach to Baire Category 10:00am Jens Blanck (Uppsala/Swansea) Computations on Topological Algebras 11:00am Coffee 11:45am Conference ends. Location -------- The meeting will take place in the conference centre of the University of Wales at Gregynog. Gregynog is a large Victorian country house in mid-Wales, standing in 750 acres of wooded parkland. It is located five miles north of Newtown, Powys, with a regular train link to Birmingham (taking approximately 1h45m). All participants will be offered rooms in the house. The number of places is limited, and early registration is advised. Cost ---- The cost of participation, including registration, two days lodging at Gregynog with full board and the conference banquet is as follows: non-BLC members 140 GBP BLC members 120 GBP students 70 GBP As the number of subsidised student places is limited, early registration is advised. Registration ------------ To register, please complete the form below and send it, with the appropriate payment (cheques should be made payable to the University of Wales Swansea) to: Jill Edwards Department of Computer Science University of Wales Swansea Singleton Park Swansea SA2 8PP, U.K. Enquiries may be addressed to the organisers: Anuj Dawar anuj.dawar@cl.cam.ac.uk John Tucker j.v.tucker@swansea.ac.uk See also: http://www.cl.cam.ac.uk/~ad260/blc99.html Form ---- NAME: AFFILIATION: ADDRESS: EMAIL ADDRESS: PAYMENT: non-BLC member 140 GBP BLC member 120 GBP student 70 GBP SPECIAL DIETARY REQUIREMENTS: Support ------- The meeting is generously supported by grants from the London Mathematical Society and the British Logic Colloquium. From cat-dist Tue Jul 20 15:16:57 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA06983 for categories-list; Tue, 20 Jul 1999 13:21:39 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 20 Jul 1999 13:44:27 +0200 From: Philippe Gaucher Message-Id: <199907201144.AA15930@irmast1.u-strasbg.fr> To: categories@mta.ca Subject: categories: looking for reference Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-Md5: 1Vqr4iBKy8Cnrvf9ekmHZA== Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Dear catetory theorist, I am looking for a precise reference about the construction of the free cubical omega category (with connnections I mean) generated by a cubical set (I am not interested in the proof : I have already a proof). I just need a bibliographical reference. If possible in a paper easily available, not a preprint difficult to find :-). Thank you in advance. pg. From cat-dist Thu Jul 22 12:04:30 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06539 for categories-list; Thu, 22 Jul 1999 10:32:32 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 20 Jul 1999 09:24:51 +1000 (EST) From: Graham Wrightson To: categories@mta.ca cc: jwl@discus.anu.edu.au Subject: categories: Re: Australasian Workshop on Computational Logic Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Australasian Workshop on Computational Logic, AWCL Australian National University, Canberra February 3-4, 2000 Call for Papers A workshop on Computational Logic will take place during the Australasian Computer Science Week at the Australian National University in February, 2000. The purpose of the workshop is to bring together researchers who have common interests in Computational Logic. While the workshop is particularly aimed at researchers in Australasia, anyone interested from elsewhere is strongly encouraged to submit a paper or to attend. Papers on all aspects of the theory, implementation, and application of Computational Logic are invited, where Computational Logic is to be understood broadly as the use of logic in Computer Science. Program Committee ----------------- Ross Brady (LaTrobe) John Cleary (Waikato) Norman Foo (UNSW) Lindsay Groves (Victoria) Rao Kotagiri (Melbourne) John Lloyd (ANU, Chair) Kim Marriott (Monash) Malcolm Newey (ANU) Claude Sammut (UNSW) John Slaney (ANU) John Staples (Qld) Rodney Topor (Griffith) David Wolfram (ANU) Graham Wrightson (Newcastle) Deadlines --------- Papers must be submitted by 15 November, 1999 Authors will be notified of acceptance/rejection by 15 December, 1999 Further information is available at the workshop web site: http://discus.anu.edu.au/~jwl/AWCL.html Further information about the Australasian Computer Science Week 2000 is available at: http://cs.anu.edu.au/ACSW2k/ From cat-dist Thu Jul 22 12:07:11 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06681 for categories-list; Thu, 22 Jul 1999 10:40:31 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: To: categories@mta.ca Subject: categories: Cartesian Monads and Pullbacks Mime-Version: 1.0 (generated by tm-edit 7.108) Content-Type: text/plain; charset=US-ASCII Date: Wed, 21 Jul 1999 12:56:40 +0200 From: N Ghani Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Do cartesian monads preserve pullbacks. May be with some extra conditions such as finitariness? Thanks for any help/references Neil From cat-dist Thu Jul 22 12:10:40 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06696 for categories-list; Thu, 22 Jul 1999 10:37:39 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 20 Jul 1999 18:41:59 +0100 (BST) Message-Id: <199907201741.SAA29163@gentzen.dcs.qmw.ac.uk> From: Paul Levy To: bhalchin@hotmail.com CC: w.james@latrobe.edu.au, categories@mta.ca In-reply-to: <3794E2AC.425B@latrobe.edu.au> (message from William James on Tue, 20 Jul 1999 13:57:18 -0700) Subject: categories: Re: co-exponential question Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I don't know if this is relevant to your question, but there is an example in programming semantics where the dual of a cartesian closed category has independent significance, due to Lafont, Streicher, Reus and Hofmann. (Some further work was done by Selinger.) It is found in the following paper: @Article{StreicherReus:continuations, title = "Classical logic, continutation semantics and abstract machines", author = "Th. Streicher and B. Reus", pages = "543--572", journal = "Journal of Functional Programming", month = nov, year = "1998", volume = "8", number = "6", } The construction is as follows. Let C be a distributive category, and let Ans (the "answer type") be an object in C, such that the exponential X -> Ans exists for each object X. Define two categories K and N as follows. Both have the same objects as C. In K, a morphism from X to Y is a C-morphism from X x (Y -> Ans) to Ans. In N, a morphism from X to Y is a C-morphism from (X -> Ans) x Y to Ans. Clearly these two categories are dual. Streicher and Reus' paper makes it clear that just as K can be used to interpret a typed call-by-value language with control effects (which was well-known), N can be used to interpret a typed call-by-name language with control effects. Like any call-by-name model, N is cartesian closed: the product of X and Y in N is given by X+Y the exponential from X to Y in N is given by (X -> Ans) x Y K is certainly an important category, but I wouldn't say that the fact that it has coexponentials is significant. Paul =========================================================================== Paul Blain Levy, Department of Computer Science, Queen Mary and Westfield College, LONDON E1 4NS http://www.dcs.qmw.ac.uk/~pbl/ =========================================================================== From cat-dist Thu Jul 22 12:16:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA08115 for categories-list; Thu, 22 Jul 1999 10:46:49 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from porky.mta.ca (porky.mta.ca [138.73.101.9]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id MAA28330 for ; Wed, 21 Jul 1999 12:58:16 -0300 (ADT) X-Received: FROM gip.u-picardie.fr BY porky.mta.ca ; Wed Jul 21 13:02:48 1999 X-Received: from ppp1.u-picardie.fr (ppp1.u-picardie.fr [194.57.109.97]) by gip.u-picardie.fr (8.9.1/8.9.1) with SMTP id RAA07166 for ; Wed, 21 Jul 1999 17:58:09 +0200 Date: Wed, 21 Jul 1999 17:58:09 +0200 Message-Id: <1.5.4.16.19990721180227.1c4f8688@mailx.sc.u-picardie.fr> X-Sender: ehres@mailx.sc.u-picardie.fr X-Mailer: Windows Eudora Light Version 1.5.4 (16) Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" To: cat-dist@mta.ca From: Andree Ehresmann Subject: categories: Answer to Davilov Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Davilov writes: >Given an object M in the ``normal'' category of finitely dimensional >smooth manifolds Man (not in SDG sense), what it the universal property >of the tangent bundle TM? Several authors have been interested in this problem many years ago, that has led to the study of the functors from Man to the category of vector bundles. Such functors are completely characterized in Epstein, "Natural vector bundles", Lecture Notes in Math. 99, Springer 1969, p. 171-195. >From his theorems, it results in particular that Ehresmann's first order velocity functors Tn which associate to a manifold M the vector bundle of the 1-jets from R^n to M (in particular T for n=1) are the only such product preserving functors. This result is generalized in an abstract setting to characterize connections in: Bowshell, "Abstract velocity functors", Cahiers de Topologie et Geom. Diff. XII-1 (1971), 57-82. Later on, related (or more general) problems are considered in: Palais & Terng, "Natural bundles have finte order", Topology 16 (1977), 271-277, Epstein & Thurston, "Transformation groups and natural bundles", Proc. London Math. Soc. 38 (1979), 219-236. Eck, "Product preserving functors on smooth manifolds, J. Pure & App. Algebra 42 (1986), 133-140. Kolar, An abstract characterization of the jet spaces, Cahiers de Topologie et Geom. Diff. XXXIV-2 (1993), 121-125. Dupovec & Kolar, On the jets of fibered manifold morphisms, Cahiers de Topologie et Geom. Diff. XXXIV-2 (1993), 121-125. Hoping these old references can be of some interest Best regards Andree C. Ehresmann From cat-dist Thu Jul 22 12:28:36 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA05040 for categories-list; Thu, 22 Jul 1999 10:34:56 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 20 Jul 1999 10:08:56 +1000 (EST) From: Graham Wrightson To: categories@mta.ca cc: Dana_Scott@POP.CS.CMU.EDU, siekmann@dfki.de Subject: categories: Int. Federation Computational Logic 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 INTERNATIONAL FEDERATION FOR COMPUTATIONAL LOGIC (IFCoLog) A MANIFESTO Computational Logic has outgrown its humble beginnings and early expectations by far: with close to ten thousand people working in research and development of logic-related methods, with several dozen international conferences and workshops addressing the growing richness and diversity of the field, and with the foundational role and importance these methods now assume in mathematics, computer science, artificial intelligence, cognitive science, linguistics and many engineering fields -- where logic-related techniques are used inter alia to state and settle correctness issues -- the field has diversified in ways that the pure logicians working in the early decades of this century could have hardly anticipated. Dating back to its roots in Greek philosophy as presented in the works of Aristotle, logic has grown in richness and diversity over the centuries to finally find today's methodological approach in the work of Frege. These logical calculi, which capture an important aspect of human thought, were now amenable to investigations with mathematical rigor and the beginning of this century saw the influence of these developments in the foundation of mathematics with the work of Hilbert, Russell and Whitehead, in the foundation of syntax and semantics of language, and in philosophical foundations expressed most explicitly by the logicians in the Vienna Circle. Picking up on these developments and on the early dreams of mechanized reasoning the Dartmouth Conference in 1956 advocated explicitly the hopes for the new possibilities that the advent of electronic computing machinery offered: logical statements could now be executed on a machine with all its far-reaching consequences that ultimately led to logic programming, deduction systems for mathematics and engineering, logical design and verification of computer software and hardware, deductive databases and software synthesis as well as logical techniques for the analysis of mechanical machinery. In this way the growing richness of foundational and purely logical investigations that had led to such developments as: - first order calculi - type theory and higher order logic - non-classical logics - semantics - constructivism and others were enriched by new questions and problems to be asked in particular in computer science and artificial intelligence, leading to: - denotational semantics for programming languages - nonmonotonic reasoning - logical foundations for computing machinery such as CSP, ?-Calculs and others for program verification - logical foundations for cognitive robotics (the frameproblem) - syntax and semantics for natural language processing - logical foundations for data bases - linear logics - logical foundations and the philosophy of mind and many others. This growing diversity is reflected in the numerous conferences and workshops that address particular aspects of the fields mentioned. For example, only twenty years ago, there was just one international conference on automated deduction (later to be called CADE). Today there is not only CADE but also: - RTA (Rewriting Techniques and Applications) - LPAR (Logic Programming and Automated Reasoning) - the TABLEAUX Conference - UNIF (Unification Workshop) - FTP (First Order Theorem Proving), and - LICS (Logic in Computer Science), each of which is held regularly with its own set of proceedings and supported by a mature community. Frequently these conferences are backed up by dozens of national and international workshops, such as JELIA, CALCULEMUS, the Induction Workshops, PROOF.PRESENTATION, USERINTERFACES for ATP; the Nonmonotonic Reasoning Workshops, the Knowledge Representation Conference(s), the Frame Problem meetings and many more. A similar growth of meetings has been seen in the other areas mentioned before, namely logic programming with its main conferences and workshops (more than two dozen regular meetings and events) which are now somehow unified into CL 2000. Similar growth and diversity can be seen in linguistics and natural language processing with its conferences and workshops (again about a dozen conferences and workshops) as well as logic and the philosophy of science with its world conference: Congress for Logic, Methodology and Philosophy of Science. Logical foundations of computer science and verification has seen a major growth with its traditional conference LICS, but nowadays represented also by CAV (Computer Aided Verification), FM-Europe (Formal Methods) and others, each of which accompanied again by a few dozen national and international workshops and many events that reflect the growing industrial importance of these techniques. This diversity is not necessarily disadvantageous, as every community that has evolved addresses its own important set of problems and issues, and it is clear that one group cannot address them all. However, fragmentation can carry a heavy price intellectually -- as well as politically -- in the wider arena of scientific activity where, unfortunately, logical investigations are still often perceived as limited. For these and other reasons we hereby propose the establishment of an international federation -- IFCoLog -- to be registered as a legal entity and possibly accepted as a member society in the International Union of Sciences (IUS). The members of the International Federation for Computational Logic (IFCoLog) will be the communities attached to the major conferences and logic societies, and they in turn will encompass the individual members working on logic related topics. THE FEDERATION How can these dozens of societies, sociologically grown communities and conference affiliates be re-united without losing their historical identities? One possible solution is inspired by the manner in which the European AI societies are organised into ECCAI (European Co-ordinating Committee for Artificial Intelligence): there is one registered society, namely ECCAI, whose members are the European national AI-Societies. With the growing unification of Europe there are currently about 25 members who represent all AI researchers and whose representatives meet every two years at the time of ECAI, the European Conference of Artificial Intelligence. So the idea for IFCoLog is as follows: An International Federation for Computational Logic (IFCoLog) will be created and legally registered, whose members are the current (and future) communities related to computational logic. Currently, this would include the groups and their respective representatives who are listed below for the Board of IFCoLog. Some of these are actually organised into legal societies, others are just centred around a conference or not legally organised at all, but still form a scientific community of considerable size and importance. To make this workable, it will be required to form an organisational structure that does not infringe on the interests of the individual communities but nevertheless ensures maximum cohesion. The following organization is therefore proposed: THE BOARD The Board should be composed of one representative from each member society or community. This may be a delegate elected by the society or simply the current chairperson. Initial members would be the dozen or so groups listed below. Subsequently newcomers will be able to apply formally and be admitted on the basis of a majority vote of the Board. The idea is that this should be an open process with as little factionalism as possible: the main motivation is not to alienate, but to unite. THE EXECUTIVE COUNCIL This is the actual executive that would run the business of the Federation, and it should be comprised of: - The President - Five Vice-presidents - A Chief Executive Officer - The Treasurer - The PR Officer (for journals, WWW, press releases, etc), and possibly - A full-time co-ordinator and a halftime secretary. 1. The President. This should be an outstanding scientist with appropriate presidential personality who can unite and bring together the many factions. He or she is not necessarily active in the day-to-day running of the Federation. The President will be elected by the Board and the Executive Council. 2. The Vice-Presidents. There should be five vice-presidents elected by the Board and the Executive Council for a limited period of time (say 3 years). Ideally the five VPs should represent the major scientific subareas, such as symbolic logic, logic programming, automated deduction, logic in computer science and artificial intelligence, formal methods and verification, logic and language as well as logic and philosophy. Three of the vice presidents should come from the three major geographical regions of the world: North America, Europe, and the Pacific Rim. This reflects the current shape of the global village, which is likely to remain dominant for the first part of the next century at least. The fourth Vice-President should come from the Network of Excellence in Computational Logic (Compulog Net) which would provide some initial funds and resources and the fifth vice president should represent any of the other subfields. THE JOINT CONFERENCE Every four years, the member communities agree to hold one major conference -- IJCoLog: The International Joint Conference of the Federation for Computational Logic -- that consists of the back-to-back conferences of the individual members, similar to FLoCS which is held every two years, while the individual conferences like CADE, LICS; CL 2000 etc. will be held yearly or biannually. This united conference, with probably more than a thousand expected participants, will be a major show of strength, unification and cross-fertilisation, and will ensure the overall visibility of the Federation. OTHER TASKS Inasmuch as the Federation aims to counterbalance the growing division in the field and to represent it once again in its entirety, it is deemed to work in order to: - influence funding policy - increase international visibility - set up concrete educational curricula - set up special chairs - encourage high-quality teaching materials (books, videos, etc) - maintain an active information policy similar to COMPULOG-Net - create an infrastructure for web sites and links - maintain a register of individual and corporate e-mail addresses - establish an informal journal, (such as AI Magazine, "Computational Logic" or others) - found a formal scientific journal (possibly electronic). - foster an association with the databases of DBLP, COMPULOG etc. THE EXECUTIVE COUNCIL For the period 1999-2002, the proposed officers are: President: Dana Scott Vicepresident: (US/Logic) John Barwise Vicepresident (US/LICS) Moshe Vardi Vicepresident (Pacific Rim/CL) John Lloyd Vicepresident (Europe/CoLi/LLI) Johan v. Bentham Vicepresident: COMPULOG-Net Joerg Siekmann Chief Executive Officier: Graham Wrightson Treasurer: N.N. Coordinator COMPULOG: David Pearce Public Relations Officer: N.N. Secretary (halftime): N.N. THE BOARD - Automated Deduction (CADE, TABLEAUX, FTP, LPAR etc.): Ulrich Furbach - Term Rewriting and Verification (RTA, UNIF, etc.): Claude Kirchner - Logic in Computer Science (LICS, etc.): Moshe Vardi - Verification (CAV, etc.): Edmund Clarke - Formal Methods (FM Europe, and US, etc.): Jeanette Wing - Association of Automated Reasoning (AAR and JAR): Deepak Kapur - Association of Symbolic Logic (ASL): John Barwise - Association for Logic Programming (ALP): Krzysztof Apt - CL 2000 (LP, Logic in D.B., LP workshops etc.): John Lloyd - Logic and Language (Coli, LCI, etc.): Johan v. Bentham - Congress for Logic, Methodology and Philosphy of Science: Jens Erik Fenstad - European Computer Science and Logic Society: Egon Boerger - Nonmonotonicc Reasoning (NMR, RMS, etc.): Eric Sandevall - HOL (Conferences and Society): Tobias Nipkow - Knowledge Representation, Logic in AI (KR, JELIA, etc.): Tony Cohn - Symbolic Computation (JSC): Bruno Buchberger - Special Intersest Group on Foundations of AI (SIGFAI)of the Japanese Society for AI: Koichi Furukawa Further Applications of logic related conferences and societies are under way, but no consensus yet. For further information see http://www.compulog.org/net/IFCoLog.html Special requests and queries should be sent to Graham Wrightson graham@cs.newcastle.edu.au or to David Pearce for COMPULOG.NET: pearce@dfki.de There is also an email distributor IFCoLog-all@dfki.de which will automatically send your email to all officers of the board and of the executive council. From cat-dist Fri Jul 23 11:42:54 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06209 for categories-list; Fri, 23 Jul 1999 10:24:21 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Andrzej Filinski MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14231.32476.50008.946207@harald.daimi.au.dk> Date: Thu, 22 Jul 1999 22:28:12 +0200 (MET DST) To: categories@mta.ca Subject: categories: Re: co-exponential question X-Mailer: VM 6.50 under 21.0 "Corsican" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Paul Levy writes: > I don't know if this is relevant to your question, but there is an > example in programming semantics where the dual of a cartesian closed > category has independent significance, due to Lafont, Streicher, Reus > and Hofmann. (Some further work was done by Selinger.) It is found > in the following paper: [Streicher & Reus 1998] Indeed, co-exponentials are closely tied the semantics of call/cc-like control operators. This connection is perhaps expressed more directly in the following (regrettably somewhat unpolished) work: @MastersThesis{Filinski:89a, author = "Andrzej Filinski", title = "Declarative Continuations and Categorical Duality", school = "Computer Science Department, University of Copenhagen", year = 1989, month = Aug, note = "DIKU Report 89/11", URL = "http://www.brics.dk/~andrzej/papers/DCaCD.ps.gz" } @InProceedings{Filinski:89b, author = "Andrzej Filinski", title = "Declarative Continuations: An Investigation of Duality in Programming Language Semantics", booktitle = "Category Theory and Computer Science", series = LNCS, number = 389, address = "Manchester, UK", month = Sep, pages = "224-249" } Specifically, in the category induced by the types and terms of a call-by-value language with first-class continuations, the coproduct functor - + A actually has a left adjoint - x (A -> 0), where 0 is the empty type. The operational intuition behind this construction is that a function f : X -> Y + A returning either a "normal" (Y) or an "exceptional" (A) result corresponds to a function f' : X x (A -> 0) -> Y, returning only the normal result, but passing any exceptional results to an additional, non-returning-function parameter. (In a purely functional language, the type A -> 0 would of course contain at most one value; but in the presence of control effects, such as exceptions, there can be many distinct "functions" of this type. And with a sufficiently powerful control operator, it actually becomes possible to define co-application and co-currying with equational properties exactly mirroring those of CCC exponentials.) Still, as Paul notes, > K is certainly an important category, but I wouldn't say that the fact > that it has coexponentials is significant. constructing a categorical semantics of a language with control operators _directly_ in terms of coexponentials is somewhat awkward, and the formulation used by Streicher and Reus is almost certainly nicer to work with in practice. -- Andrzej From cat-dist Fri Jul 23 11:52:02 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06542 for categories-list; Fri, 23 Jul 1999 10:25:41 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: To: Thomas Streicher cc: categories@mta.ca Subject: categories: Re: Cartesian Monads and Pullbacks In-reply-to: Your message of "Thu, 22 Jul 1999 17:01:02 +0200." <199907221501.AA104505662@fb0448.mathematik.tu-darmstadt.de> Mime-Version: 1.0 (generated by tm-edit 7.108) Content-Type: text/plain; charset=US-ASCII Date: Fri, 23 Jul 1999 11:28:56 +0200 From: N Ghani Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I asked the question >> Do cartesian monads preserve pullbacks. May be with some extra >> conditions such as finitariness? without properly defining what I meant by a cartesian monad. What I mean was that the unit and multiplication of the monad are cartesian natural transformations, ie the associated naturality squares are pullbacks. Soory for the confusion Neil From cat-dist Mon Jul 26 12:15:40 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA15513 for categories-list; Mon, 26 Jul 1999 10:24:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Selinger Message-Id: <199907231940.PAA02826@eratosthenes.math.lsa.umich.edu> Subject: categories: Re: co-exponential question To: categories@mta.ca Date: Fri, 23 Jul 1999 15:40:52 -0400 (EDT) In-Reply-To: <14231.32476.50008.946207@harald.daimi.au.dk> from "Andrzej Filinski" at Jul 22, 99 10:28:12 pm X-Mailer: ELM [version 2.4 PL25] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: I agree completely with Paul and Andrzej, except possibly for this: > Still, as Paul notes, > > > K is certainly an important category, but I wouldn't say that the fact > > that it has coexponentials is significant. > > constructing a categorical semantics of a language with control operators > _directly_ in terms of coexponentials is somewhat awkward, and the > formulation used by Streicher and Reus is almost certainly nicer to work > with in practice. The _direct_ categorical semantics of languages with control operators is actually not too unnatural and leads to some interesting category theory. Let me first clarify the difference between direct and indirect semantics. To give a direct semantics, one starts with a class of categories with algebraic structure (for our purposes: structure that is given by object constructors, morphism constructors, and equations on morphisms). In the direct interpretation of a language, types are interpreted as objects, type constructors as object constructors, and typing judgments as morphisms, in such a way that the language forms an _internal language_ for the class of categories at hand. This means, among other things, that one can construct a syntactic category from a theory of the language. Thus, all structure of the category (on objects and morhpisms) is denotable in the language. The usual interpretation of the simply-typed lambda calculus in a cartesian-closed category is perhaps the best-known example of a direct semantics. (Direct semantics of higher order can be given in fibered categories, but this is not necessary for our purposes here). In an indirect semantics, one does not interpret the language directly in a category with algebraic structure, but in a derived auxiliary category. Moggi's monadic semantics is an example of an indirect semantics. Given a category C with a monad T, one interprets the language (for instance, a call-by-value lambda calculus) in the Kleisli category of the monad. Notice that the structure of the Kleisli category, per se, is not necessarily algebraic in the above sense. The Reus-Streicher-Lafont-Hofmann semantics is indirect; in fact it is the monadic semantics for the continuations monad R^(R^(-)). Indirect semantics are very successful in practise. Among other things, they have proven excellent tools for reasoning about and implementing control effects. This point is made convincingly in Andrzej Filinski's PhD thesis [1]. However, the correspondence between syntax and semantics is not as close as in the direct case: one cannot usually speak of internal languages in the context of indirect semantics. The reason is that, from a syntactic theory of the language, one can reconstruct only the Kleisli category of T, but not the underlying category C or the monad T itself. Thus, direct semantics might be more satisfying to the theorist, because they capture the essence of the language precisely, and without resorting to a translation to a meta-language. The difference between direct and indirect semantics is explained very nicely in a recent paper by Carsten Fuhrmann [2], where he also gives a general method of constructing direct semantics from indirect ones. It seems that direct semantics are often characterized by the presence of certain _non-natural_ transformations, and that indirect semantics are a way of hiding this non-naturality. The first direct semantics for a call-by-value language with control effects are the tensor-not categories of Hayo Thielecke [3]. His work was later extended by me to a language with finite coproducts (this is where co-exponentials enter the picture) and to the call-by-name case [4]. I called the resulting class of categories "control categories". The connection between the direct and indirect semantics can be established via categorical representation theorems, and such theorems were shown by Fuhrmann for tensor-not categories [5], and independently by myself for control categories [4]. It is interesting that a call-by-name language is an internal language for control categories, and the corresponding call-by-value language is an internal language for the dual co-control categories. As a consequence, one obtains a syntactic duality between call-by-name and call-by-value [4]. Such a duality was conjectured by Streicher and Reus [6], and certainly anticipated by Filinski's work on the symmetric lambda calculus [7]. Best wishes, -- Peter [1] A. Filinski. Controlling effects. PhD Thesis in Computer Science, Carnegie Mellon University, 1996. [2] C. F\"uhrmann. Direct models for the computational lambda-calculus. Technical Report ECS-LFCS-98-400, Edinburgh, 1998. [3] H. Thielecke. Categorical structure of continuation passing style. PhD Thesis in Computer Science, Edinburgh, 1997. [4] P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Submitted 1999. Available from Hypatia or http://www.math.lsa.umich.edu/~selinger/papers.html [5] C. F\"uhrmann. Exponential categories and semantics of continuations. Presented at MFPS, 1998. [6] T. Streicher, B. Reus. Classical Logic, continuation semantics and abstract machines. Journal of Functional Programming 8(6)543-572, 1998. [7] A. Filinski. Declarative continuations and categorical duality. Masters Thesis in Computer Science, DIKU, University of Copenhagen, 1989. DIKU Report 89/11. From cat-dist Mon Jul 26 17:16:43 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA18873 for categories-list; Mon, 26 Jul 1999 15:28:43 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <379C882A.233C7CA8@dcs.ed.ac.uk> Date: Mon, 26 Jul 1999 17:09:14 +0100 From: Samson Abramsky Organization: Dept. of Computer Science, University of Edinburgh X-Mailer: Mozilla 3.04 (X11; I; Linux 2.0.35 i686) MIME-Version: 1.0 To: categories@mta.ca Subject: categories: CTCS`99 Call for Participation Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: CATEGORY THEORY AND COMPUTER SCIENCE (CTCS'99) 10-12 SEPTEMBER 1999, EDINBURGH, SCOTLAND http://www.dcs.ed.ac.uk/home/ctcs99 CALL FOR PARTICIPATION EARLY REGISTRATION DEADLINE: 10th August 1999 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. Previous meetings have been held in Guildford (Surrey), Edinburgh, Manchester, Paris, Amsterdam, Cambridge, and S. Margherita Ligure (Genova). This document contains 1. Invited speakers 2. List of accepted papers 3. Programme committee 4. Registration form A WWW-version containing all this information plus abstract of contributed papers can be found under www.dcs.ed.ac.uk/home/ctcs99 1. Invited speakers ------------------- Ryu Hasegawa Univ. of Tokyo (Japan) Peter Freyd Univ. of Pennylvania (USA) Marcelo Fiore Univ. of Sussex (UK) Doug Smith Kestrel Institute (USA) 2. List of accepted papers (19 out of 39 submissions) -------------------------- Concurrent Realizations of Reactive Systems. Marek Bednarczyk, Andrzej Borzyszkowski Functorial semantics for Petri nets under the individual token philosophy. Roberto Bruni, Jose Meseguer, Ugo Montanari, Vladimiro Sassone Equational Lifting Monads. Anna Bucalo, Alex Simpson, Carsten Fuehrmann Structured Theories and Institutions F Duran, J Meseguer Coalgebra to Algebra Morphisms. A Eppendahl On the Semantics of Message Passing Processes. Lindsay Errington A Fully abstract presheaf semantics for SCCS with finite delay. Thomas Hildebrandt Abstract Games for Linear Logic. Martin Hyland, Andrea Schalk Internal Languages for Autonomous and *-Autonomous Categories. T W Koh and C-H L Ong Dependent Coercions. Zhaohui Luo and Sergei Soloviev Precategories for combining probabilistic automata. Paulo Mateus, Amilcar Sernadas, Cristina Sernadas Monads, shapely functors, and traversals. E Moggi, G Belle, C B Jay Exhausting Strategies, Joker Games and IMLL with Units. A S Murawski and C-H L Ong Hilbert Q-Modules and Nuclear Ideals in the Category of v-Semilattices with a Duality. Jan Paseka A Coalgebraic Foundation for Linear Time Semantics. John Power, Daniele Turi Denotational Completeness Revisited. Thomas Streicher A domain-theoretic semantics of lax generic functions. Hideki Tsuiki A Bi-Categorical Axiomatisation of Concurrent Graph Rewriting. Fabio Gadducci, Reiko Heckel and Merce Llabres. Higher-dimensional syntax. Martin Wehr. 3. 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) 4. Registration form -------------------- Please complete this form and email it to ctcs99-reg@dcs.ed.ac.uk before 10th August 1999. You can also fax the form to +44 131 667 7209 Attn: CTCS-REG or send it to M Lekuse, CTCS-REG, JCMB, KB, Mayfield Rd, Edinburgh EH9 3JZ, UK. ******************************************************* * REGISTRATION FOR CTCS '99 * ******************************************************* A PERSONAL DETAILS ------------------ LAST NAME: _______________________________ FIRST NAME: ______________________________ AFFILIATION: _____________________________ ADDRESS: _________________________________ _________________________________ _________________________________ PHONE NUMBER: ____________________________ FAX: _____________________________________ E-MAIL: __________________________________ WWW (optional): __________________________ DATE OF ARRIVAL: __/__ 1999 DATE OF DEPARTURE: __/__ 1999 ANY SPECIAL DIETARY REQUIREMENTS (e.g. vegetarian): ______________________ B CONFERENCE FEES ----------------- The conference fee will cover lunches, coffee breaks, and proceedings. (It also includes costs for invited speakers and seminar room bookings.) Regular Student -------------------------------------------- Early registration: GBP115 GBP95 by 19th July Late registration: GBP170 GBP170 after 19th July There will be a conference dinner on Saturday, 11th September. It will cost GBP30 (students GBP15). I will attend the dinner YES ( ) NO ( ) Total fees payable: GBP ____ I have paid the fees by ____________________ on __/__1999. Please pay your fee by - bank draft in GBP - Eurocheque in GBP - any other cheque drawn on a British bank payable to "The University of Edinburgh". Unfortunately, we cannot acccept credit cards and bank transfers. C ACCOMMODATION --------------- We should like to ask you to book your own accommodation directly. The Edinburgh Tourist Board offers a very efficient booking service. You can either book by phone (+44-131-473-3874), fax (+44-131-473-3636) or e-mail (conventions@eltb.org). When you contact them they will supply you with a booking form which lists a number of accommodation types from simple guest houses to 5* hotels. Please book early. Although the Edinburgh International Festival will be over, September is still a very busy time. ---------------------------------------------------------------- **Please state clearly on the accommodation booking form that your accommodation should be within easy reach of the King's Buildings, University of Edinburgh.** ---------------------------------------------------------------- You should receive confirmation of your booking within one day. You need to give them your credit card number which will serve as a security. You will actually have to pay your accommodation directly later. If you do not have a credit card, or you encounter any difficulties in booking your accommodation, then please get in touch with us directly. Please contact (ctcs99-reg@dcs.ed.ac.uk) and state your requirements. The conference will be held in the James Clerk Maxwell Building (Lecture theatre B), King's Buildings, Edinburgh EH9 3JZ. You will find maps at http://www.visres.ed.ac.uk/internal/maps. 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 From cat-dist Tue Jul 27 17:04:38 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA20388 for categories-list; Tue, 27 Jul 1999 15:38:47 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <002501bed83f$f769d500$443cfea9@frank.129.78.68.10> From: "walters" To: Subject: categories: CT 2000 Date: Tue, 27 Jul 1999 16:47:58 +0200 MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Category Theory 2000 CT 2000 will be held from 16th to 22nd July 2000, at Villa Olmo, Como, Italy. RFC Walters From cat-dist Tue Jul 27 17:10:16 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA17265 for categories-list; Tue, 27 Jul 1999 15:39:33 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 27 Jul 1999 18:56:16 +0100 (BST) From: Achim Jung X-Sender: axj@preston To: categories@mta.ca Subject: categories: Lectureship in Theoretical Computer Science in Birmingham 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 University of Birmingham School of Computer Science LECTURER IN THEORETICAL COMPUTER SCIENCE Applications are invited for a permanent lectureship in Theoretical Computer Science in the School of Computer Science at the University of Birmingham. Applications from all areas of Theoretical Computer Science will be considered but preferential treatment will be given to candidates who show promise to strengthen existing activities. These encompass Mathematical Structures in Computer Science, Lambda Calculus, Type Theory, and Verification of Systems. The School has recently appointed Uday Reddy to a Chair in Programming Languages and close cooperation between the existing Theory group and this new strand of activity is expected. For further information, please see ftp://ftp.cs.bham.ac.uk/pub/dist/info/lect.tcs/particulars.htm Please pass this advert on to any interested individuals in your department. Kind regards, Achim Jung. ------------------------------------------------------------------------- Prof Achim Jung Tel.: (+44) 121 414 4776 School of Computer Science Sec.: (+44) 121 414 3711 The University of Birmingham Fax.: (+44) 121 414 4281 Edgbaston Email: A.Jung@cs.bham.ac.uk BIRMINGHAM, B15 2TT Web: http://www.cs.bham.ac.uk England ------------------------------------------------------------------------- From cat-dist Wed Jul 28 11:32:58 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA06506 for categories-list; Wed, 28 Jul 1999 10:15:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 28 Jul 1999 14:37:44 +0200 (MET DST) X-Sender: gran@mail.math.ucl.ac.be Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Mailer: Eudora F1.5.3 To: categories@mta.ca From: gran@agel.ucl.ac.be (Marino Gran) Subject: categories: PSSL 71: First announcement Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: PERIPATETIC SEMINAR ON SHEAVES AND LOGIC 71st meeting -- First Announcement As announced in Coimbra, the 71st meeting of the PSSL will be held in Louvain-la-Neuve on the weekend of 16-17 October 1999. We welcome contributed talks on category theory and related areas. Further details of the arrangements for the meeting, and a registration form, will be sent out in August. Francis Borceux Marino Gran Mamuka Jibladze Enrico Vitale From cat-dist Wed Jul 28 18:13:27 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA11579 for categories-list; Wed, 28 Jul 1999 15:41:50 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Sender: johanj@pop.cs.uu.nl X-Mailer: QUALCOMM Windows Eudora Pro Version 4.0 Date: Wed, 21 Jul 1999 14:45:46 +0200 To: categories@mta.ca From: Johan Jeuring Subject: categories: Call for papers: Workshop on Generic Programming 2000 Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Message-Id: <19990721124403.428434540@mail.cs.uu.nl> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Workshop on Generic Programming http://www.cs.uu.nl/~johanj/wgp2000/wgp2000cfp.html 6th July 2000 Ponte de Lima, Portugal Call for papers Generic programming is about making programs more adaptable by making them more general. Generic programs often embody non-traditional kinds of polymorphism; ordinary programs are obtained from them by suitably instantiating their parameters. In contrast with normal programs, the parameters of a generic programs are often quite rich in structure. For example they may be other programs, types or type constructors, kinds, or even programming paradigms. This workshop follows on the 5th Mathematics of Program Construction conference. This is the second workshop on generic programming, the first workshop on generic programming (proceedings) was held on Marstrand, Sweden, in 1998. Submission Papers (preferably short, no more than 15 pages) should be submitted in Postscript format by e-mail to reach Johan Jeuring by March 20, 2000. Accepted papers will be published in the proceedings of the workshop, which will appear as a technical report at Utrecht University. Submission deadline: 20 March Notification: 30 April Final version due: 20 May Workshop: 6 July Topics Generic programming techniques have always been of interest, both to practitioners and theoreticians, but have rarely been a specific focus of research, until recently. In the last couple of years we have seen: * several language extensions for generic programming (PolyP,DrIFT,FML,AOOP,FiSH); * lots of examples of generic programming (generalized tries, unification, data compression, XML applications) ; * programming calculi for generic programming. We solicit papers on these topics. The list of topics is not exclusive: papers on other topics related to generic programming are also welcome. Programme Committee Gianna Belle (Genova, Italy) Patrik Jansson (Chalmers, Sweden) Ralf Hinze (Bonn, Germany) Graham Hutton (Nottingham, Great Britain) Johan Jeuring (Utrecht, The Netherlands, chair) Colin Runciman (York, Great Britain) Fritz Ruehr (Willamette, USA) Tim Sheard (OGI, USA) Doaitse Swierstra (Utrecht, The Netherlands) Address Johan Jeuring Department of Computer Science Utrecht University P.O.Box 80.089 NL-3508 TB Utrecht The Netherlands email: johanj@cs.uu.nl url: http://www.cs.uu.nl/~johanj/ From cat-dist Fri Jul 30 16:18:01 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA17492 for categories-list; Fri, 30 Jul 1999 15:09:24 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.19990730101113.0096fac0@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Fri, 30 Jul 1999 10:12:46 -0400 To: categories@mta.ca From: Charles Wells Subject: categories: New edition of "Category Theory for Computing Science" Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Category Theory for Computing Science (Third edition) By Michael Barr and Charles Wells This new edition contains all the material from the first and second editions, including the four chapters excised from the second edition and the solutions to all the exercises, as well as added material on factorization systems, monoidal categories, and other topics. All errors known to the authors have been corrected. The price is only Can$45, approximately US$31, postpaid anywhere on earth. It should be available for ordering from http://crm.umontreal.ca/pub/Ventes/CatalogueEng.html by mid-August. You can also order the book directly by sending an email to sales@crm.umontreal.ca. Charles Wells, Department of Mathematics, Case Western Reserve University, 10900 Euclid Ave., Cleveland, OH 44106-7058, USA. EMAIL: charles@freude.com. OFFICE PHONE: 216 368 2893. FAX: 216 368 5163. HOME PHONE: 440 774 1926. HOME PAGE: URL http://www.cwru.edu/artsci/math/wells/home.html From cat-dist Sat Jul 31 11:39:15 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA32002 for categories-list; Sat, 31 Jul 1999 10:41:19 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Selinger Message-Id: <199907310445.AAA06766@blackbox.math.lsa.umich.edu> Subject: categories: Paper announcement To: categories@mta.ca (Categories List) Date: Sat, 31 Jul 1999 00:45:43 -0400 (EDT) X-Mailer: ELM [version 2.4 PL25] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear Category Theorists, I am pleased to announce the availability of a new paper, Categorical Structure of Asynchrony, available via http://www.math.lsa.umich.edu/~selinger/papers.html. In this paper, I investigate properties of traced monoidal categories that are satisfied by networks of asynchronously communicating processes. Among these properties are Hasegawa's uniformity principle, as well as a version of Kahn's principle: the subcategory of *deterministic* processes is equivalent to a category of domains. The paper also contains the following observation, which may be of interest to categorists. I do not know whether this was observed before, and would be grateful for references. Suppose T:Set-->Set is a functor which is lax for the symmetric monoidal structure given by products on the category of sets. Then T associates to any category C another category C', which Benabou called the "direct image of C by T". This category is defined as follows: obj(C') = obj(C), and C'(X,Y) = T(C(X,Y)). The observation is that direct images preserve linear structure. More precisely, if the category C possesses some algebraic structure which is given by linear equations, then C' inherits that structure. Non-linear structure is not in general preserved, although one can give conditions on T under which the construction will preserve, for instance, affine structure. One can also loosen the conditions on T, so that it will only preserve non-commutative linear structure. One can use the direct image construction to extract the linear "part" of an arbitrary algebraic structure: for instance, if C has finite products, then C' has a monoidal structure with diagonals, which is precisely the part of a finite product structure which is given by linear equations. Traced monoidal structure with diagonals is the linear part of finite product structure with fixpoints. One direction of this, namely that the latter structure is a special case of the former, was observed by Hasegawa and by Hyland, but I don't know whether it had been noticed that the former is precisely the linear part of the latter. An example of a non-commutative linear structure (given by linear equations where the variables occur in the same left-to-right order on both sides) is the premonoidal structure of Power and Robinson. This is precisely the non-commutative part of monoidal structure. More details and examples are in the paper. Comments are, as usual, welcome. Best wishes, -- Peter Selinger ---------------------------------------------------------------------- ABSTRACT: We investigate a categorical framework for the semantics of asynchronous communication in networks of parallel processes. Abstracting from a category of asynchronous labeled transition systems, we formulate the notion of a categorical model of asynchrony as a uniformly traced monoidal category with diagonals, such that every morphism is total and the focus is equivalent to a category of complete partial orders. We present a simple, non-deterministic, cpo-based model that satisfies these requirements, and we discuss how to refine this model by an observational congruence. We also present a general construction of passing from deterministic to non-deterministic models, and more generally, from non-linear to linear structure on a category.