From MAILER-DAEMON Fri Sep 5 15:23:03 2003 Date: 05 Sep 2003 15:23:03 -0300 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1062786183@mta.ca> X-IMAP: 1054586291 0000000062 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Mon Jun 2 17:35:29 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Jun 2003 17:35:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Mvzh-0004bG-00 for categories-list@mta.ca; Mon, 02 Jun 2003 17:33:25 -0300 Date: Sun, 1 Jun 2003 09:05:31 -0700 From: Toby Bartels To: Categories Subject: categories: Re: Topos logic arises naturally Message-ID: <20030601160531.GH20845@math-rs-n01.ucr.edu> References: <3ED34194.9050005@informatik.uni-bremen.de> <002801c326a1$05dc0000$f112fea9@essex.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <002801c326a1$05dc0000$f112fea9@essex.ac.uk> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 1 Elwood Wilkins wrote: >Isabelle's internal logic is not constructive. The existential clause of the >BHK-interpretation is violated so that a consquence of "all unicorns have >horns" is that "some unicorn has a horn". The moral (biased towards >theorists): software engineering considerations are not enough, a coherant >philosophy of mathematics is also needed. Is this a failure of constructivism as such, or just a bug? No doubt that a coherent philosophy of mathematics helps to avoid such mistakes, but would anybody ever claim that it's *not* a mistake? -- Toby From rrosebru@mta.ca Mon Jun 2 17:35:29 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Jun 2003 17:35:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Mw0v-0004eP-00 for categories-list@mta.ca; Mon, 02 Jun 2003 17:34:41 -0300 Date: Mon, 2 Jun 2003 09:02:07 -0400 (EDT) From: jlipton@wesleyan.edu To: categories@mta.ca Subject: categories: Re: Semantic tableaux and intuitionistic logic In-Reply-To: <20030530201401.40220.qmail@web12203.mail.yahoo.com> Message-ID: References: <20030530201401.40220.qmail@web12203.mail.yahoo.com> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-ECS-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 Nerode, Shore: logic for Applications, Springer, has detailed tableau development for intuitionistic, and modal logics: i.e. there is nothing intrinsically classical about the method. The ideas go back to Hintikka and Beth (at least) in the 1950s and 60s. On Fri, 30 May 2003, Galchin Vasili wrote: > Hello, > > I am only familiar with semantic tableaux for > classical propositional logic (and classical 1st order > logic). It seems that as an inference system it is > based squarely around the law of the excluded middle > because it is essentially reductio ad absurdum. Hence, > as an inference system it can't be simply modified for > intuitionistic propositional calculus?? (Of course, I > am bringing this because the role that Heyting > algebras play in Topos theory). > > Regards, Bill Halchin > > > -------------------------------------------------------------------- Jim Lipton Math Dept.Wesleyan University, Middletown,CT 06459-0128 www.wesleyan.edu/~jlipton jlipton@wesleyan.edu, (860) 685-2188 fax:685-2571 ==================================================================== From rrosebru@mta.ca Mon Jun 2 17:36:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Jun 2003 17:36:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Mw2G-0004mi-00 for categories-list@mta.ca; Mon, 02 Jun 2003 17:36:04 -0300 Date: Mon, 2 Jun 2003 16:14:16 +0200 (MESZ) From: Marc Olschok Message-Id: <200306021414.QAA18084@d2-hrz.uni-duisburg.de> To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Scanned-By: MIMEDefang 2.21 (www . roaringpenguin . com / mimedefang) Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 3 > Here is a technical/pedagogical question which has been bothering me for > about twelve years. > > In problem 5 on page 19 of "Categories for the Working Mathematician" (CWM), > Saunders Mac Lane points out that a natural transformation may be fully > extended to an intertwining function from one category to another, > intertwining meaning (except in the void case), that the function > transforms on one side according to its domain functor and on the > other according to its codomain functor. > Then on page 42 Mac Lane introduces what he calls "horizontal" composition > diagramatically and without reference to the fully extended intertwining > functions. But the function composite of such a pair of functions trivially > intertwines the function composite of the domain functors with that of > the codomain functors, and this function composition operation is very > quickly verified to be "horizontal" composition when written in terms > of restrictions to sets of objects. Thus Mac Lane and everyone else I > have read leaves the impression that an honest verification of, say, > the associativity of "horizontal" composition would require a somewhat > involved diagrammatic demonstration which, in fact, would be nothing > other than the hard way to prove the associativity of function composition. > Presumably this has been noticed for a long, long time, but the > 1998 edition of CWM did not mention it, and I can't help but be struck > by the fact that other authors' terminologies leave the impression that > they don't know or don't care that "horizontal", star or Godement > composition is function composition.[...] At least in the book "Elemente der Kategorientheorie" by D. Pumpl\"un the above characterization of natural maps is used explicitely; there is also a short discussion on obtaining simpler proofs this way. For the above reason \circ is used for the "horizontal composition"; \cdot or \ast (I do not remember which one) is used for the "vertical composition", which after all looks more "point-wise". Unfortunately some authors use these symbols just the other way round. Marc From rrosebru@mta.ca Mon Jun 2 17:37:33 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Jun 2003 17:37:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Mw3F-0004uI-00 for categories-list@mta.ca; Mon, 02 Jun 2003 17:37:05 -0300 Message-ID: <839BE2CA5177D3119C7000508B11F5DB0376B3B0@dagobah.parc.xerox.com> From: Valeria.dePaiva@parc.com To: categories@mta.ca Subject: categories: Re: Topos logic arises naturally Date: Mon, 2 Jun 2003 11:11:10 PDT MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2656.59) Content-Type: text/plain Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 My two cents worth: >The moral (biased towards > theorists): software engineering considerations are not enough, a coherent > philosophy of mathematics is also needed. John Harrison (the creator of HOL Light) has a very coherent, but pragmatic philosophy of mathematics. Let us see how much can we do with constructive logic, without getting rid of the classical principles: Add them at the end, so that if someone really needs it, they can use it. This is a philosophy quite widespread in Cambridge, with Peter Johnstone's books being the paradigmatic example. If classical reasoning is needed, it's used, but flagged. I also agree with Till that it's a cute example. Best, Valeria -----Original Message----- From: Till Mossakowski [mailto:till@Informatik.Uni-Bremen.DE] Sent: Friday, May 30, 2003 7:37 AM To: Categories Subject: categories: Re: Topos logic arises naturally I did not want to deny the need of mathematical thought, but I found this example of topos theory emerging unexpectedly quite pleasing. Note that the mail is *not* about Isabelle. Admittedly, I do not know anything about the quoted system HOL light, so I have not verified Slind's claim. Till Elwood Wilkins wrote: > Isabelle's internal logic is not constructive. The existential clause > of the BHK-interpretation is violated so that a consquence of "all > unicorns have horns" is that "some unicorn has a horn". The moral > (biased towards > theorists): software engineering considerations are not enough, a coherant > philosophy of mathematics is also needed. > > Elwood > > ----- Original Message ----- > From: Till Mossakowski > To: Categories > Sent: Tuesday, May 27, 2003 11:44 AM > Subject: categories: Topos logic arises naturally > > > >>You see: even with just aesthetic and software engineering >>considerations you are eventually lead to topos logic... >> >>-- >>Till Mossakowski Phone +49-421-218-4683 >>Dept. of Computer Science Fax +49-421-218-3054 >>University of Bremen till@tzi.de >>P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till >> >>Message-Id: <200305270616.h4R6G3w8008134@plxc2089.pdx.intel.com> >>To: Randy Pollack >>cc: John Harrison , >>isabelle-users@cl.cam.ac.uk >>Subject: Re: HOL without description operators >>Date: Mon, 26 May 2003 23:16:03 -0700 >>From: John R Harrison >>Sender: Larry Paulson >> >>Hi Randy, >> >>| Perhaps more usefully, how do you suggest I do this task of >>| developing > > HOL > >>| without description operators. >> >>You might find it interesting to look at HOL Light. This gives a >>different axiomatization of the HOL logic, developed precisely because >>I was dissatisfied with the one in the original HOL system, on which I >>believe the Isabelle/HOL logic is based. >> >>Although I do eventually introduce the description operator, quite a >>lot of the basic logic --- including the automation of inductive >>definitions >>--- is developed without it (and indeed without excluded middle or >>extensionality). You may find it a more congenial starting-point. >> >>As Konrad Slind later pointed out, what I settled on is remarkably >>close to the internal logic of a topos, as presented for example in >>Lambek and Scott's book. This was a surprise to me since at that time >>I knew next to nothing about toposes and was motivated by a mixture of >>aesthetic and software engineering considerations. >> >>Cheers, >> >>John. >> >> >> >> -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From rrosebru@mta.ca Mon Jun 2 17:38:30 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Jun 2003 17:38:30 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Mw4A-000514-00 for categories-list@mta.ca; Mon, 02 Jun 2003 17:38:02 -0300 Message-ID: <20030602200853.54626.qmail@web12205.mail.yahoo.com> Date: Mon, 2 Jun 2003 13:08:53 -0700 (PDT) From: Galchin Vasili Subject: categories: Re: Semantic tableaux and intuitionistic logic To: categories@mta.ca In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 The reason why I suggested that the Law of Excluded Middle is required is that reductio ad absurbdum is the core concept in Tableaux or to put it another way Tableaux is built around bivalent logic. Regards, Bill --- Christopher Townsend wrote: > I can only remember Tableux from many years ago, but > I don't think that > their structure forced you to use the excluded > middle? Can't you just drop > the excluded middle as a deduction rule and then use > whatever is left over > as a constructive propositional theory? > > Regards, Christopher Townsend > > > >From: Galchin Vasili > >To: categories@mta.ca > >Subject: categories: Semantic tableaux and > intuitionistic logic > >Date: Fri, 30 May 2003 13:14:01 -0700 (PDT) > > > >Hello, > > > > I am only familiar with semantic tableaux for > >classical propositional logic (and classical 1st > order > >logic). It seems that as an inference system it is > >based squarely around the law of the excluded > middle > >because it is essentially reductio ad absurdum. > Hence, > >as an inference system it can't be simply modified > for > >intuitionistic propositional calculus?? (Of course, > I > >am bringing this because the role that Heyting > >algebras play in Topos theory). > > > >Regards, Bill Halchin > > From rrosebru@mta.ca Tue Jun 3 12:03:03 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 12:03:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NDEl-0001wJ-00 for categories-list@mta.ca; Tue, 03 Jun 2003 11:58:07 -0300 Date: Tue, 3 Jun 2003 10:24:35 +0100 Subject: categories: Re: Topos logic arises naturally Content-Type: text/plain; charset=US-ASCII; format=flowed Mime-Version: 1.0 (Apple Message framework v552) To: Categories From: Lawrence Paulson Content-Transfer-Encoding: 7bit Message-Id: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> X-Mailer: Apple Mail (2.552) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 > -----Original Message----- > From: Elwood Wilkins [mailto:elwood@essex.ac.uk] > Sent: Friday, May 30, 2003 4:35 AM > To: Categories > Subject: categories: Re: Topos logic arises naturally > > Isabelle's internal logic is not constructive. The existential clause > of the BHK-interpretation is violated so that a consquence of "all > unicorns have horns" is that "some unicorn has a horn". The moral > (biased towards > theorists): software engineering considerations are not enough, a > coherant philosophy of mathematics is also needed. Isabelle's internal logic comes from Lambek and Scott. It is an instance of Example 1.1 on page 132, where all types are assumed to be non-empty. However, even their full system is unacceptable to many constructivists because it is impredicative. Constructive theories, like a certain commuting diagrams package, have a surprising tendency to "time out". Larry Paulson From rrosebru@mta.ca Tue Jun 3 12:03:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 12:03:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NDCJ-0001mE-00 for categories-list@mta.ca; Tue, 03 Jun 2003 11:55:35 -0300 Message-ID: <3EDC68AD.6060702@cs.bham.ac.uk> Date: Tue, 03 Jun 2003 10:21:49 +0100 From: Steve Vickers User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.3) Gecko/20030312 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? References: <200306021414.QAA18084@d2-hrz.uni-duisburg.de> In-Reply-To: <200306021414.QAA18084@d2-hrz.uni-duisburg.de> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 7 Marc Olschok wrote: >For the above reason \circ is used for the "horizontal composition"; >\cdot or \ast (I do not remember which one) is used for the >"vertical composition", which after all looks more "point-wise". > >Unfortunately some authors use these symbols just the other way round. > >Marc > It is also possible to use a 2-dimensional syntax, in which horizontal composition is composed horizontally and vertical composition is composed vertically. Then algebraic manipulations are a bit like sliding tiles around in a tray. Steve Vickers. From rrosebru@mta.ca Tue Jun 3 16:55:07 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 16:55:07 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NHqi-0004ah-00 for categories-list@mta.ca; Tue, 03 Jun 2003 16:53:36 -0300 From: Todd Wilson MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <16092.50933.427818.743898@localhost.localdomain> Date: Tue, 3 Jun 2003 09:04:05 -0700 To: Categories Subject: categories: Re: Topos logic arises naturally In-Reply-To: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> References: <30CB5DA5-95A5-11D7-BEF0-00039384D4B8@cam.ac.uk> X-Mailer: VM 7.07 under 21.4 (patch 8) "Honest Recruiter" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 8 On Tue, 3 Jun 2003, Lawrence Paulson wrote: > Isabelle's internal logic comes from Lambek and Scott. It is an > instance of Example 1.1 on page 132, where all types are assumed to be > non-empty. But this is the heart of the matter. There is a certain precise sense in which what happens in a topos between the empty set and a singleton set governs the behavior of the rest of the topos. Instead, why not factor out the topos logic and add whatever nonemptiness assumptions that are perceived necessary from a practical standpoint as an additional theory? This factoring shouldn't affect those that rely on the non-emptiness assumptions, but it would make a big difference to those who want to work in the topos logic. -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh From rrosebru@mta.ca Tue Jun 3 17:02:55 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Jun 2003 17:02:55 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NHzN-0005M6-00 for categories-list@mta.ca; Tue, 03 Jun 2003 17:02:33 -0300 Date: Tue, 3 Jun 2003 21:40:48 +0200 (MEST) From: Jean-Marie JACQUET Message-Id: <200306031940.h53JemF17544@backus.info.fundp.ac.be> To: categories@mta.ca Subject: categories: Foclasa: Last Call for Papers X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 9 [ Our apologies for multiple copies. ] ====================================================================== 2nd International Workshop on Foundations of Coordination Languages and Software Architectures (Foclasa 2002) September 2, 2003, Marseille, France Workshop affiliated to CONCUR'2003, 02 - 06 September 2003. http://www.info.fundp.ac.be/~jmj/Foclasa03.html ====================================================================== SCOPE AND TOPICS Modern information systems rely more and more on combining concurrent, distributed, mobile and heterogenous components. This move from old systems, typically conceived in isolation, induces the need for new languages and software architectures. In particular, coordination languages have been proposed to cleanly separate computational aspects and communication. On the other hand, software architects face the problem of specifying and reasoning on non-functional requirements. All these issues are widely perceived as fundamental to improve software productivity, enhance maintainability, advocate modularity, promote reusability, and lead to systems more tractable and more amenable to verification and global analysis. The aim of the workshop is to bring together researchers working on the foundations of component-based computing, coordination, and software architectures. Topics of interest include (but are not limited to): o Theoretical models for coordination (component composition, concurrency, dynamic aspects of coordination, semantics, expressiveness); o Specification, refinement, and analysis of software archi- tectures (patterns and styles, verification of functional and non-functional properties); o Coordination, architectural, and interface description languages (implementation, interoperability, heterogeneity); o Agent-oriented languages (formal models for interacting agents); o Dynamic software architectures (mobile agents, configuration, reconfiguration); o Modeling of information systems (groupware, internet and the web, workflow management, CSCW and multimedia applications) o Coordination patterns (mobile computing, internet computing); o Tools and environments for the development of coordinated applications o Methodologies for validating and certifying software compositions SUBMISSION GUIDELINES Papers describing original work are solicited as contributions to Foclasa. Submitted papers should be limited to 6 000 words, preferrably formatted according to the Electronical Notes in Theoretical Computer Science. They should be emailed as PostScript (PS) or Portable Document Format (PDF) files to jmj@info.fundp.ac.be. PUBLICATION Following the previous edition, the proceedings will be published as a volume of the Electronical Notes in Theoretical Computer Science. Selected papers will be published in a special issue of the journal Science of Computer Programming. IMPORTANT DATES: o June 9, 2003: Submission deadline. o July 15, 2003: Notification of acceptance. o August 25, 2003: Final version. o September 2, 2003: Meeting Date. LOCATION The workshop will be held in Marseille in September 2003. It is a satellite workshop of CONCUR 2003. For venue and registration see the CONCUR web page at http://concur03.univ-mrs.fr/ WORKSHOP ORGANIZERS o Antonio Brogi (University of Pisa, Italy) o Jean-Marie Jacquet (University of Namur, Belgium) o Ernesto Pimentel (University of Malaga, Spain) PROGRAMME COMITTEE: o Farhad Arbab (CWI, The Netherlands) o Antonio Brogi (University of Pisa, Italy) - Co-chair o Manfred Broy (University of Munich, Germany) o Jeff Kramer (Imperial College, United Kingdom) o Paola Inverardi (Univerity L'Aquila, Italy) o Jean-Marie Jacquet (University of Namur, Belgium) - Co-chair o Joost Kok (University of Leiden, The Netherlands) o Ernesto Pimentel (University of Malaga, Spain) - Co-chair o Antonio Porto (New University of Lisbon, Portugal) o Catalin Roman (Washington University, USA) o Pamela Zave (AT&T Labs Research, USA) From rrosebru@mta.ca Wed Jun 4 12:14:48 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Jun 2003 12:14:48 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NZpw-0003IR-00 for categories-list@mta.ca; Wed, 04 Jun 2003 12:06:00 -0300 From: Thomas Streicher Message-Id: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> Subject: categories: Re: topos logic arising nicely To: categories@mta.ca Date: Tue, 3 Jun 2003 22:14:04 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 10 I don't know Isabelle too well BUT in Higher Order Logic one may well assume inhabitedness of all types when these are built up from N (and 1) via x,-> and P(-). In higher order logic one cannot form subtypes in the logical sense and that's the only way how one can build types that aren't inhabited. Of course, even if type sigma is inhabited from (1) \forall x:\sigma. A(x)->B one must not conclude (2) \exists x:\sigma. A(x) /\ B BUT only (3) \exists x:\sigma. A(x) -> B BTW concluding (2) from (1) is false also classically. Thomas From rrosebru@mta.ca Wed Jun 4 12:14:48 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Jun 2003 12:14:48 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NZoe-0003BT-00 for categories-list@mta.ca; Wed, 04 Jun 2003 12:04:40 -0300 Date: Wed, 4 Jun 2003 10:25:49 +0100 X-Image-Url: http://www.cl.cam.ac.uk/users/lcp/images/new-larry-0-small.jpg Subject: categories: Re: Topos logic arises naturally Content-Type: text/plain; charset=US-ASCII; format=flowed Mime-Version: 1.0 (Apple Message framework v552) To: Categories From: Lawrence Paulson In-Reply-To: <16092.50933.427818.743898@localhost.localdomain> Message-Id: <879725FB-966E-11D7-BEF0-00039384D4B8@cam.ac.uk> Content-Transfer-Encoding: 7bit X-Mailer: Apple Mail (2.552) Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 11 On Tuesday, June 3, 2003, at 05:04 pm, Todd Wilson wrote: > But this is the heart of the matter. There is a certain precise sense > in which what happens in a topos between the empty set and a singleton > set governs the behavior of the rest of the topos. The point of my message is merely to counter suggestions on this mailing list that Isabelle's underlying logic was cooked up in some ad-hoc way and is incoherent. The basic logic comes from a standard source. Extensions (type classes especially) were thought through very carefully. We have never claimed allegiance to any school of constructivity. Larry Paulson From rrosebru@mta.ca Wed Jun 4 15:42:22 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Jun 2003 15:42:22 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19NdAG-0005ol-00 for categories-list@mta.ca; Wed, 04 Jun 2003 15:39:12 -0300 Date: Tue, 3 Jun 2003 13:32:48 -0700 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? Message-ID: <20030603203247.GB5160@math-rs-n01.ucr.edu> References: <200306021414.QAA18084@d2-hrz.uni-duisburg.de> <3EDC68AD.6060702@cs.bham.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <3EDC68AD.6060702@cs.bham.ac.uk> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 13 Steve Vickers wrote: >It is also possible to use a 2-dimensional syntax, in which horizontal >composition is composed horizontally and vertical composition is >composed vertically. Then algebraic manipulations are a bit like sliding >tiles around in a tray. Of course this can be done using big diagrams. But is there a tight syntax for this just using text? Can you point to an example? (preferably a TeX source online, but a printed page in a regular journal would also work). -- Toby From rrosebru@mta.ca Thu Jun 5 16:09:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:09:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O02v-00078q-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:05:09 -0300 Message-Id: <5.2.1.1.0.20030604150547.02799418@c30> X-Sender: sharoval@c30 (Unverified) X-Mailer: QUALCOMM Windows Eudora Version 5.2.1 Date: Wed, 04 Jun 2003 15:11:31 -0400 To: categories@mta.ca From: Alexei Sharov Subject: categories: categories and gene alignment Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 14 Did anybody apply the theory of categories to gene alignment problem? If you have 2 sequences then the alignment is a morfism. My impression is that many problems in genomic alignment can be formulated using the language of category theory (e.g., product = intersection of 2 alignments, coproduct = combining several alignments). If somebody knows any reference or interested in collaboration, please contact me. -Alexei Alexei Sharov, PhD, Staff Scientist Lab. of Genetics, National Institute on Aging (NIA/NIH) 333 Cassell Dr., Suite 3000, Baltimore, MD 21224 Phone: 410-558-8556 Fax: 410-558-8331 http://www.grc.nia.nih.gov/branches/lg/dgas/sharov.html From rrosebru@mta.ca Thu Jun 5 16:09:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:09:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O00W-0006vR-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:02:40 -0300 Date: Wed, 4 Jun 2003 16:42:32 +0100 (BST) From: Paul B Levy To: categories@mta.ca Subject: categories: Re: topos logic arising nicely In-Reply-To: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 15 On Tue, 3 Jun 2003, Thomas Streicher wrote: > I don't know Isabelle too well BUT in Higher Order Logic one may > well assume inhabitedness of all types when these are built up from > N (and 1) via x,-> and P(-). In higher order logic one cannot form > subtypes in the logical sense and that's the only way how one can > build types that aren't inhabited. "The neglect of sum types is the root of all evil." Paul From rrosebru@mta.ca Thu Jun 5 16:09:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:09:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O001-0006re-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:02:09 -0300 Date: Wed, 4 Jun 2003 08:20:39 -0700 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: topos logic arising nicely Message-ID: <20030604152039.GC11425@math-rs-n01.ucr.edu> References: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <200306032014.WAA05082@fb04305.mathematik.tu-darmstadt.de> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 16 Thomas Streicher wrote: >In Higher Order Logic one may >well assume inhabitedness of all types when these are built up from >N (and 1) via x,-> and P(-). In higher order logic one cannot form >subtypes in the logical sense and that's the only way how one can >build types that aren't inhabited. That may be the only way that one can *construct* such a type, hence the only way that one can *prove* that such a type exists, but how do you know that some unspecified type variable \sigma doesn't refer to an uninhabited type to begin with? The answer will depend on the interpretation, I suppose; some logics simply aren't applicable to some semantics. >Of course, even if type sigma is inhabited from > (1) \forall x:\sigma. A(x)->B >one must not conclude > (2) \exists x:\sigma. A(x) /\ B >BUT only > (3) \exists x:\sigma. A(x) -> B Of course. Only with \exists x:\sigma. A(x) will (2) follow. -- Toby From rrosebru@mta.ca Thu Jun 5 16:12:02 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:12:02 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O05V-0007Kq-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:07:49 -0300 From: Jpdonaly@aol.com Message-ID: <15f.2152bf37.2c0fa601@aol.com> Date: Wed, 4 Jun 2003 15:44:01 EDT Subject: categories: Re: Function composition of natural transformations? To: categories@mta.ca 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: X-Keywords: X-UID: 17 For function composition, I just use the standard small circle \circ. So the function composite of natural transformations \tau and \sigma (if it exists) is \tau\circ\sigma. It is advisable to give up subscripting as a way of denoting values of (fully extended) natural transformations: The value of \tau at morphism a is just \tau(a). I would not use juxtaposition or any other generic means (e.g., a centered dot) of denoting composition in a general category for function composition or, for that matter, for any other composition which already has a specified composition symbol, but I do denote pointwise ("vertical") composition generically. Here is an example of how this goes---a line proof of the interchange law for function and pointwise composition: {\noindent\bf Proposition (Interchange Law):} When $\nu\mu\circ\tau\sigma$ is defined for natural transformations $\nu$, $\mu$, $\tau$ and $\sigma$, then so is $(\nu\circ\tau)\cdot(\mu\circ\sigma)$, and $$\nu\mu\circ\tau\sigma=(\nu\circ\tau)\cdot(\mu\circ\sigma).$$ \medskip {\noindent\bf Proof:} The void cases are trivial. Assume that $\nu\mu\circ\tau\sigma$ is defined. Then surely $\nu\circ\tau$ and $\mu\circ\sigma$ are defined, and $$\dom(\nu\circ\tau)=\dom\nu\circ\dom\tau=\cod\mu\circ\cod\sigma=\cod(\mu\circ \sigma),$$ so $\nu\circ\tau$ composes pointwise with $\mu\circ\sigma$. Calculate as follows at an $a$ in the common domain category of both sides of the interchange formula: $$\eqalign{[(\nu\cdot\mu)\circ(\tau\cdot\sigma)](a)=&\nu[\tau(\cod a)\cdot\sigma(a)]\cdot\mu(\dom[\tau(\cod a)\cdot\sigma(a)])\cr &\cr =&\nu(\tau(\cod a))\cdot(\dom\nu)[\sigma(a)]\cdot\mu[\dom\sigma(a)]\cr &\cr =&(\nu\circ\tau)(\cod a)\cdot(\cod\mu)[\sigma(a)]\cdot\mu[\dom\sigma(a)]\cr &\cr =&(\nu\circ\tau)(\cod a)\cdot\mu(\sigma(a))\cr &\cr =&(\nu\circ\tau)(\cod a)\cdot(\mu\circ\sigma)(a)\cr &\cr =&[(\nu\circ\tau)\cdot(\mu\circ\sigma)](a).\cr}$$ So the two sides of the interchange equation have the same intertwining function. Checking domain functors, $$\eqalign{\dom(\nu\mu\circ\tau\sigma)&=\dom\nu\mu\circ\dom\tau\sigma\cr &=\dom\mu\circ\dom\sigma\cr &=\dom(\mu\circ\sigma)\cr &=\dom(\nu\circ\tau)(\mu\circ\sigma);\cr}$$ similarly, $\cod(\nu\mu\circ\tau\sigma)=\cod(\nu\circ\tau)(\mu\circ\sigma)$. Thus the two natural transformations are equal. In this, \dom and \cod are defined by \def\dom {\hbox{\rm dom }} \def\cod {\hbox{\rm cod }} and respectively represent the domain and the codomain function on the implicit category. The proof uses the following formulas for pointwise composition in terms of fully extended natural transformations (i.e., in terms of their intertwining functions \pi and \tau): (\pi\cdot\tau)(a)=\pi(a)\cdot\tau(\dom a)=\pi(\cod a)\cdot\tau(a) which I can't help mentioning as an aside shows that evaluation of fully extended natural transformations at a morphism intertwines evaluation at its domain object with evaluation at its codomain object. (And, incidentally, codomains are on the left in my notations, domains on the right.) If I haven't explained something necessary here, I hope that you can nevertheless see that the above line proof represents a moderately massive amount of diagram drawing and chasing and would fit convincingly on the page of a textbook. I hope that this addresses your request. The only examples which I know are all in my personal set of notes which I set up PCTex32 over the last dozen years and which come out at about 200 pages. This is probably a little too much to drop on you all at once. I am, however, anxious to answer any further questions which you may have. From rrosebru@mta.ca Thu Jun 5 16:12:12 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:12:12 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O06b-0007Ow-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:08:57 -0300 Date: Wed, 4 Jun 2003 21:53:51 +0100 (BST) From: Ronnie Brown X-X-Sender: mas010@publix To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? In-Reply-To: <20030603203247.GB5160@math-rs-n01.ucr.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 18 It may be useful to recall the Ehresmann method of setting up the exponential law for categories using the double categoy of commuting squares in a category. This is also written up in (R.Brown, P. NICKOLAS), ``Exponential laws for topological categories, groupoids and groups and mapping spaces of colimits'', {\em Cah. Top. G\'eom. Diff.} 20 (1979) 179-198. The nice point is that the category structure is induced by a double category composition, and so if you have extra structure, such as a topology, that carries over. Ronnie Brown On Tue, 3 Jun 2003, Toby Bartels wrote: > Steve Vickers wrote: > > >It is also possible to use a 2-dimensional syntax, in which horizontal > >composition is composed horizontally and vertical composition is > >composed vertically. Then algebraic manipulations are a bit like sliding > >tiles around in a tray. > > Of course this can be done using big diagrams. > But is there a tight syntax for this just using text? > Can you point to an example? (preferably a TeX source online, > but a printed page in a regular journal would also work). > > > -- Toby > > > Prof R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Centre for the Popularisation of Mathematics Raising Public Awareness of Mathematics CDRom Symbolic Sculpture and Mathematics: http://www.cpm.informatics.bangor.ac.uk/centre/index.html From rrosebru@mta.ca Thu Jun 5 16:14:47 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:14:47 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O09J-0007cl-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:11:45 -0300 Message-ID: <3EDF122A.5070206@bangor.ac.uk> Date: Thu, 05 Jun 2003 10:49:30 +0100 From: Tim Porter MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? References: <200306021414.QAA18084@d2-hrz.uni-duisburg.de> <3EDC68AD.6060702@cs.bham.ac.uk> <20030603203247.GB5160@math-rs-n01.ucr.edu> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 Toby Bartels wrote: >Steve Vickers wrote: > > > >>It is also possible to use a 2-dimensional syntax, in which horizontal >>composition is composed horizontally and vertical composition is >>composed vertically. Then algebraic manipulations are a bit like sliding >>tiles around in a tray. >> >> > >Of course this can be done using big diagrams. >But is there a tight syntax for this just using text? >Can you point to an example? (preferably a TeX source online, >but a printed page in a regular journal would also work). > > >-- Toby > > Dear All, In reply to Toby Bartels, there are various models of higher categories in which the syntax is well attested and the `sliding of tiles' is algebraically described. One possible one that extends to arbitrary dimensions is given in the paper: AL-AGL, A.A., BROWN, R. & STEINER, R., Multiple categories: the equivalence of a globular and a cubical approach, Advances in Math. 170 (2002) 71-118. The links between `cubical' syntax and a more globular syntax are at the heart of the extensive work on the equivalence between the various models for weak n-categories. One problem is that there are no normal forms for elements. In fact I think (possibly!) that the problem of rewriting in these higher dimensional settings needs a higher dimensional rewriting systems, and to model that one needs n-cateories (and so on!) Tim Porter From rrosebru@mta.ca Thu Jun 5 16:19:50 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:19:50 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0Cy-0000Ae-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:15:32 -0300 Date: Thu, 05 Jun 2003 15:45:12 +0100 Message-ID: From: Philippe Gaucher Subject: categories: technical question about omega-categories MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Bcc: Status: RO X-Status: A X-Keywords: X-UID: 20 Dear all, Let C be an omega-category (strict, globular). Let U be the forgetful functor from strict globular omega-categories to globular sets. And let F be its left adjoint. Let us suppose that we are considering an equivalence relation R on UC (the underlying globular set of C) such that the source and target maps pass to the quotient : i.e. one can deal with the quotient globular set UC/R. The canonical morphism of globular sets UC --> UC/R induces a morphism of omega-categories F(UC) --> F(UC/R) by functoriality of F. Consider the following push-out in the category of omega-categories : F(UC) -----> F(UC/R) | | | | | | v v C ---------> D The morphism F(UC)-->C (the counit of the adjonction) is surjective on the underlying sets. The morphism F(UC)-->F(UC/R) is generally not surjective on the underlying sets : because by taking the quotient by R, one may add composites in F(UC/R) which do not exist in F(UC). However the intuition tells (me) that the morphism F(UC/R)-->D is surjective on the underlying sets : this morphism only adds in F(UC/R) the calculation rules of C : this is precisely what I want by introducing D. But I cannot see why with a rigorous mathematical argument. Thanks in advance. pg. From rrosebru@mta.ca Thu Jun 5 16:28:08 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:28:08 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0L0-000125-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:23:50 -0300 From: Thomas Streicher Message-Id: <200306051108.NAA00738@fb04209.mathematik.tu-darmstadt.de> Subject: categories: Re: topos logic arising nicely To: categories@mta.ca Date: Thu, 5 Jun 2003 13:08:14 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 Toby Bartels wrote > That may be the only way that one can *construct* such a type, > hence the only way that one can *prove* that such a type exists, > but how do you know that some unspecified type variable \sigma > doesn't refer to an uninhabited type to begin with? > The answer will depend on the interpretation, I suppose; > some logics simply aren't applicable to some semantics. > > >Of course, even if type sigma is inhabited from > > (1) \forall x:\sigma. A(x)->B > >one must not conclude > > (2) \exists x:\sigma. A(x) /\ B > >BUT only > > (3) \exists x:\sigma. A(x) -> B > > Of course. Only with \exists x:\sigma. A(x) will (2) follow. Certainly, if you allow type variables then the problem crops up. I don't really see the point why one would like to have type variables unless one can perform constructions with types in a uniform way, e.g. when considering logic on top of system F, system F\omega or even on top of a dependent type theory (possibly with an impredicative universe). I guess that in case of HOL type variables were rather motivated by the analogy to functional languages with their "shallow" polymorphism. The point of my mail rather was that so-called topos logic admits subtype formation, i.e. that {x:A|phi(x)} is a type whenever \phi is a predicate on A. This, of course, allows one to introduce types with undecided inhabitedness. See W.Phoa's Edinburgh lecture notes for a calculus extending HOL with subtypes (or Bart Jacob's book). But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. Thomas From rrosebru@mta.ca Thu Jun 5 16:28:15 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:28:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0M7-00017i-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:24:59 -0300 Message-ID: <3EDEF348.4010107@bath.ac.uk> Date: Thu, 05 Jun 2003 08:37:44 +0100 From: "David J. Pym" MIME-Version: 1.0 To: categories@mta.ca, types@cis.upenn.edu Subject: categories: Preprint: semantics of classical proofs Content-Type: text/plain; charset=3DISO-8859-1; format=3Dflowed Content-Transfer-Encoding: 8bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 22 Dear Colleagues, The paper, "Order-enriched categorical models of the classical sequent calculus", by Carsten F=FChrmann and David Pym, may be of interest to readers of the recipient lists. It is available at =09http://www.cs.bath.ac.uk/~pym/oecm.pdf Abstract. It is well-known that weakening and contraction cause na=EFve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations. Please accept out apologies for the size (11.5 Mb) of the pdf file: the proof-net diagrams are rather complex. Kind regards, =09David Pym --=20 Prof. David J. Pym Telephone: +44 (0)1 225 38 3246 Professor of Logic & Computation Facsimile: +44 (0)1 225 38 3493 University of Bath Email: d.j.pym@bath.ac.uk Bath BA2 7AY, England, U.K. Web: http://www.bath.ac.uk/~cssdjp From rrosebru@mta.ca Thu Jun 5 16:37:53 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:37:53 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0Wu-0002PL-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:36:08 -0300 Message-ID: <20030605173938.64548.qmail@web12204.mail.yahoo.com> Date: Thu, 5 Jun 2003 10:39:38 -0700 (PDT) From: Galchin Vasili Subject: categories: Wesley Phoa's Intro on Fibrations, Toposes, Effective Toposes To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 23 Hello, Questions concerning: http://www.lfcs.informatics.ed.ac.uk/reports/92/ECS-LFCS-92-208/ I am familiar with natural deduction and sequents. In the chapter on Toposes (Chapter 3), I have some questions about the very beginning where propositional calculus (intuitionistic) is discussed 1) Did he leave out the Elimination rule for V? I do see in the second line on far right a rule for V, but it doesn't look like EV??? 2) I don't understand the Structual rules. Can anybody give me a short explanation? Regards, Bill Halchin From rrosebru@mta.ca Thu Jun 5 16:50:31 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 16:50:31 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O0hs-0004Sy-00 for categories-list@mta.ca; Thu, 05 Jun 2003 16:47:28 -0300 Date: Wed, 4 Jun 2003 22:07:51 +0200 (CEST) From: Tom LEINSTER To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset="US-ASCII" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 24 This may be `mere' pedagogy for ordinary categories, but if you try the same thing for 2-categories then it becomes a `genuine' issue. To put it another way, the two different but equivalent presentations of a concept (natural transformation) become, on categorification, significantly different. First the 1-dimensional situation. As I understand it, Pat Donaly's original point was that given functors F, G: C ---> D between categories, you can either define a natural transformation in the standard way (assigning an arrow of D to each object of C) or in an alternative way (assigning an arrow of D to each arrow of C). With the standard method, vertical composition of transformations is "easy" to define, and horizontal composition is "hard". With the alternative method, horizontal composition is now easy to define (as Pat noted), but vertical composition is "hard". So the situation is reversed. Of course, neither of these "hard"s is really hard, but in both cases you have two evident ways of defining a composite - one left-handed, one right-handed - and if you're going to do anything whatsoever with the definition then you need to show that these two ways give exactly the same result. Now suppose that C and D are 2-categories and F and G are 2-functors. It doesn't matter whether C, D, F and G are strict or weak for the purposes of this discussion. Suppose we're interested in defining weak (=pseudo) transformations F ---> G. The usual way is to say that such a transformation consists of a 1-cell alpha_c : Fc ---> Gc for each c in C, together with an invertible 2-cell inside each naturality square, satisfying axioms. With this definition, vertical composition of transformations is easy to define (and there's only one evident way of doing it), but horizontal composition can be defined in two different ways, which are not equal but canonically isomorphic. An alternative approach is to say that a transformation consists of a 1-cell alpha_f: Fc ---> Gc' for each 1-cell f: c ---> c' in C, together with certain further 2-cells, satisfying axioms. You can guess the rest of this paragraph: with this definition, horizontal composition is now easily (and canonically) defined, but vertical composition can be defined in two different ways, which are not equal but canonically isomorphic. You might think that this isn't a genuine difference or "problem" so far, because everything is the same up to isomorphism. But now suppose that you're interested in *lax* transformations F ---> G (where F and G are still 2-functors, as above). The usual definition is that such a lax transformation alpha consists of a 1-cell alpha_c as above for each object c of C, and then a not-necessarily-invertible 2-cell inside each naturality square (pointing in a direction fixed by convention), satisfying axioms. These lax transformations can still be composed vertically perfectly easily, but horizontal composition is now *impossible* to define. (More accurately, you can define two different horizontal compositions, but they're not isomorphic, only connected by a non-invertible cell; you could of course choose one over the other, but it won't have good properties.) And if you define "lax transformation" according to the alternative method, then horizontal composition is now easy and vertical composition impossible. In summary, if you define transformation of 1- or 2-category in the standard style then vertical composition is always easy, and regarding horizontal composition: - for transformations of categories, it's canonically defined - for weak transformations of 2-categories, it's not canonically defined (you have to choose "left" or "right"), but is canonically defined up to isomorphism - for lax transformations of 2-categories, it's not defined at all. If you use the alternative style then the situation is similar but with "vertical" and "horizontal" reversed. Puzzling. Tom From rrosebru@mta.ca Thu Jun 5 18:40:41 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Jun 2003 18:40:41 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19O2RD-0004vW-00 for categories-list@mta.ca; Thu, 05 Jun 2003 18:38:23 -0300 From: Thomas Streicher Message-Id: <200306051946.VAA19086@fb04305.mathematik.tu-darmstadt.de> Subject: categories: Re: topos logic arising nicely To: categories@mta.ca Date: Thu, 5 Jun 2003 21:46:23 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (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: X-Keywords: X-UID: 25 Hi Paul, > "The neglect of sum types is the root of all evil." To some extent this may be true for programming languages (but see recent work of Jim Laird). For logics it is less clear. Actually you mean the empty type, isn't it? Moreover, sunset types are slightly heavier than ordinary sum types. Subset types are rather dependent sum types. Thomas From rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONdl-0004PK-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:16:45 -0300 Message-ID: <3EE0A2CB.C5F6FD09@cwi.nl> Date: Fri, 06 Jun 2003 16:18:51 +0200 From: frb Organization: cwi X-Mailer: Mozilla 4.77 [en] (X11; U; Linux 2.4.3-12 i686) X-Accept-Language: en MIME-Version: 1.0 To: mobij-list@cwi.nl Subject: categories: Call for Papers on Compositional Verification of UML Models Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 26 Call for Papers Compositional Verification of UML Models Workshop of the UML 2003 Conference The definition of UML has been motivated by the need for a standard notation for modelling system architectures and behaviours at functional and implementation level. The main fqocus has been essentially on terminology, notation and syntax without addressing semantic, validation and methodology issues which are important for formal design and verification techniques. This workshop addresses the application of formal methods and techniques that exploit the architectural structure of UML models in a compositional manner. TOPICS The workshop topics include (but are not limited to): * semantic foundations of architectural and component-based design within UML * compositional techniques for the analysis embedded and real-time systems in UML * compositional model checking of UML behavioural models * compositional deductive methods based on OCL * methodologies based on compositional formal techniques FORMAT OF THE WORKSHOP The workshop will consist of presentations of the accepted papers, which will be the basis for an intensive discussion on the workshop topics. Extended abstracts of the presentations will be published after the workshop by Elsevier Science as a volume of the Electronic Notes in Theoretical Computer Science. For an up-to-date program and invited talks see the workshop web-site http://fmco.liacs.nl/compuml.html SUBMISSIONS Authors are invited to submit by August 25th an extended abstract not exceeding 20 pages electronically to F.S.de.Boer@cwi.nl. Submissions must be either in Postscript or PDF format and prepared for USLetter or A4 page sizes. Submissions will be evaluated by the program committee for inclusion in the proceedings, which will be published by Electronic Notes in Theoretical Computer Science series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Simultaneous submissions to other conferences are not allowed. IMPORTANT DATES 25 August Submission deadline 10 September Notification to authors 1 October Deadline for preliminary version 21 October Workshop date 21 November Deadline for final version PROGRAM COMMITTEE Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Werner Damm (OFFIS, DE) Susanne Graf (Verimag, France) David Harel (Weizmann Institute, Israel) Jozef Hooman (University of Nijmegen, NL) Bernhard Josko (OFFIS, DE) Amir Pnueli (Weizmann Institute, ISR) Willem-Paul de Roever (Kiel University, DE) Joseph Sifakis (Verimag, FR) ORGANIZERS Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Bernhard Josko (OFFIS, DE) SPONSORS This workshop is sponsored by the European R&D project OMEGA - Correct Development of Real-time Embedded Systems (http://www-omega.imag.fr), and the German-Dutch project Mobi-J (main sponsor of FMCO, http://fmco.liacs.nl). From rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONbk-0004IG-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:14:40 -0300 From: Thomas Streicher Message-Id: <200306060813.KAA04256@fb04209.mathematik.tu-darmstadt.de> Subject: categories: Re: Semantic tableaux and intuitionistic logic To: categories@mta.ca Date: Fri, 6 Jun 2003 10:13:44 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 27 > I am only familiar with semantic tableaux for > classical propositional logic (and classical 1st order > logic). It seems that as an inference system it is > based squarely around the law of the excluded middle > because it is essentially reductio ad absurdum. Hence, > as an inference system it can't be simply modified for > intuitionistic propositional calculus?? (Of course, I > am bringing this because the role that Heyting > algebras play in Topos theory). the point is that tableau calculus may be best understood as a search for cut-free proofs in either classical or intuitionistic logic; this fact is systematically overlooked in the literature on tableaux methods like in the logic programming community one hardly ever finds exposed the view that executing a logic program is nothing but unravelling an inductive definition for information on tableau methods from a proof-theoretic point of view see Troelstra & van Dalen's book "Constructivism in Mathematics" vol.2, the chapter on proof theory of intuitionistic logic Best, Thomas From rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONcO-0004L7-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:15:20 -0300 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <16096.24299.686053.329698@ithif51.inf.tu-dresden.de> Date: Fri, 6 Jun 2003 11:29:15 +0200 To: categories@mta.ca Subject: categories: Re: topos logic arising nicely In-Reply-To: <200306051108.NAA00738@fb04209.mathematik.tu-darmstadt.de> References: <200306051108.NAA00738@fb04209.mathematik.tu-darmstadt.de> X-Mailer: VM 7.14 under Emacs 21.2.1 From: Hendrik Tews Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 28 Hi, Thomas Streicher writes: Date: Thu, 5 Jun 2003 13:08:14 +0200 (CEST) Subject: categories: Re: topos logic arising nicely But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes). I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove hd [] = last [] (saying that the head of the empy list equals its last element) Bye, Hendrik From rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONeh-0004Rx-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:17:43 -0300 To: categories Date: Thu, 05 Jun 2003 15:49:07 +0100 From: Marco Mackaay Subject: categories: reference: normal categorical subgroup? Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-ID: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 29 To all category theorists, I'm looking for a reference to the definition of a normal categorical subgroup, i.e. the right kind of subgroupoid of a categorical group for taking the quotient. I know the definition, but I have no reference. Does anyone know a published origin of the definition? Best wishes, Marco Mackaay From rrosebru@mta.ca Fri Jun 6 17:22:34 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:22:34 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONgf-0004WN-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:19:45 -0300 Subject: categories: V-modules From: Stefan Forcey To: categories@mta.ca Date: Fri, 6 Jun 2003 12:32:25 -0400 (EDT) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20030606163239Z10345-15495+90@calvin.math.vt.edu> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 30 Hello! First here are some preprints that relate delooping in topology to the functor described by enriching over a monoidal category: http://arxiv.org/abs/math.CT/0304026 Enrichment as Categorical Delooping I: Enrichment Over Iterated Monoidal Categories http://arxiv.org/abs/math.CT/0306086 Higher Dimensional Enrichment In continuing this research my collaborator and I have become interested in extending results to V-modules (with hope of an explicit categorical looping given by taking endofunctors becoming clear.) I notice in the literature that there are two definitions of a V-module. Less common is a definition that corresponds more closely to a classical module. This is described as a category with a left (right) functorial action of V. Here V-module functors and natural transformations are easily defined as well (forming a 2-category Mod_V?) For instance, for c an object in C a V-module, v in V, then a V-mod-functor F:C->D repects the action: F(vc) = vF(c). V itself is a V-module in this sense, and End(V) = V seems to hold. It also looks as though for V braided, left V-modules have a canonical right structure, perhaps leading to a tensor product of V-V-bimodules. Any references on this? The second definition is more common: for V closed, braided, a V-module is a V-functor F:B^op tensor A -> V. These form the one-cells in a bicategory V-Mod (objects V-categories, two-cells V-nat.trans.). Here (given enough structure) we recover V as V-Mod(1,1) where 1 is the unit V-category |1| ={0} and 1(0,0) = I the unit object of V. I noticed that there may be a way to describe categories of these (Street's) V-modules as (classical) V-modules. Modulo some careful checking, V-Mod(A,B) has an action of V given by (vF)(A,B) = v tensor F(A,B). The details of this action on morphisms require the adjunction that makes V closed. Is there some well-known deep connection between the two concepts that I have missed due to my youth and naivete? We would be thankful for any helpful comments or suggested references. Thanks, Stefan Forcey VA Tech. From rrosebru@mta.ca Fri Jun 6 17:22:43 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:22:43 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONhJ-0004bR-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:20:25 -0300 To: categories Date: Thu, 05 Jun 2003 18:03:45 +0100 From: Galchin Vasili Subject: categories: Topoi, Heyting algebra and Lawvere's CAT book Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 31 Hello, This is a followup question to my other question about topoi and intuistionistic logic. On page 350, Lawvere is talking about logical operations (in a Heyting algebra I think??). In particular I having trouble understanding the narrative on the implication operation "=>" in the sense 1) I don't understand what . (e.g. is alpha meant to be an element: alpha:1->omega?) 2) also what alpha "subset" beta is! Please help me. Thanks and regards, Bill Halchin From rrosebru@mta.ca Mon Jun 9 11:41:33 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:41:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNmh-0002SZ-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:38:07 -0300 From: Thomas Streicher Message-Id: <200306081139.NAA21518@fb04305.mathematik.tu-darmstadt.de> Subject: categories: Re: topos logic arising nicely In-Reply-To: <16096.24299.686053.329698@ithif51.inf.tu-dresden.de> from Hendrik Tews at "Jun 6, 2003 11:29:15 am" To: categories@mta.ca Date: Sun, 8 Jun 2003 13:39:40 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 32 Dear Hendrik, > But I would be surprised if HOL has subtype formation as from a logical > point of view subtypes are neither necessary nor convenient. Adding subtypes > is only necessary for getting a topos out of a model of HOL. > > I don't know, if I miss the point here. However, PVS has a HOL > system with predicate subtypes. And it is _very very_ convenient > (because of the predicate subtypes). > > I don't know if it is a necessity, but the absence of subtypes in > Isabelle/HOL leads to a representation of partial functions, that > allows you to prove unexpected results. Despite what the Isabelle > tutorial says at page 187, you _can_ prove > > hd [] = last [] > > (saying that the head of the empy list equals its last element) thanks for the interesting information; you really pinpoint why subtypes are used in practice, namely for avoiding partial functions; if one wants to avoid subtypes and treat partial functions directly one might use the Fourman/Scott variant of the interpretation of topos logic; an alternative and actually the one common in mathematical practice is to introduce subtypes; however, to do this constructively one is forced to either treat partial functions as single-valued realtions OR to explicitly introduce proof objects as in Martin-Loef type theory; I am pretty certain that in systems like HA_\omega one cannot quantify over partial functions as these subsume prediacte types; but if one has Higher Order Logic already it seems more natural to treat partial functions as single valued relations; quantification over subtypes can then be reduced to pure Higher Order Logic via a straightforward translation (which, however, needs some care as one sees from HOL) Thomas From rrosebru@mta.ca Mon Jun 9 11:41:33 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:41:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNiy-00024J-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:34:16 -0300 From: Jpdonaly@aol.com Message-ID: <161.2136f0f8.2c1261ce@aol.com> Date: Fri, 6 Jun 2003 17:29:50 EDT Subject: categories: Re: Function composition of natural transformations? To: categories@mta.ca 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: X-Keywords: X-UID: 33 Tom---I understand your general point to be that 2-categories are different, and from this I tentatively suspect that you would not favor my habit of calling "horizontal" composition function composition if that proposition were before the board. I have to give the particulars of this some thought, but while I am thinking, I'm going to wish that you had been aware of my perspective on 2-categories when you made your comment. What follows is a failed attempt to convey this perspective in a reasonably brief email in hopes that you will kindly make some additional comments with this background in view. Reading this will require some patience, because my lack of erudition is going to show up here, but let me state that the objective is to define a general natural transformation to be a functor into a cell category which is actually the first participating category in a certain type of split interchange category, then to define its arithmetic in these terms. This is an extremely general but surely not unprecedented definition of naturality which provides a correspondingly general definition of "vertical" or (as I prefer) pointwise composition without any conflicts which I can see, although it is true that function composition does not seem to exist in this generality. Your sharpest criticisms are very welcome. To begin, everyone knows that a double category is an ordered pair of participating categories which have the same underlying set (of morphisms), and a double functor is a function between underlying sets which is functorial between first participants and also between second participants. Say that a double category splits if the domain and codomain function of each of these participants is endofunctorial on the other participant. First fact: In this case, the set of objects of each participant forms a subcategory of the other participant---call it the object subcategory of the other participant and be careful to distinguish it from the subcategory of objects which any category has. My excuse for using "split" in this context is that a category participates with itself in a split double category exactly when it is a disjoint union of monoids. Everyone also knows the interchange law for double categories: The compositions of the participants commute with each other in the weak sense that $ab\# cd=(a\#c)(b\#d)$ if both sides are defined (visible composition symbols are used as delimiters in the obvious fashion). Say that a double category is a split interchange category if it splits and satisfies this interchange law. To be brief, call it a splintor. A category participates in a splintor with itself exactly when it is synonymously its own reverse, opposite or dual category, which amounts to being the disjoint union of a set of commutative monoids. Call it a core splintor, because every splintor contains a strongly maximal core subsplintor whose underlying set consists of those elements at which all four object (i.e., domain and codomain) functions agree, so that the double objects are obviously in the core. Strongly maximal means that any core splintor which is a subsplintor of the given splintor is contained in its core. (Incidentally, aside from core splintors, I know of only one general type of splintor which has a nondiscrete core---namely splintors of classical natural transformations under pointwise and function composition. In fact, in this example, the core consists of those natural transformations which intertwine identity functors. If an identity functor is the identity functor of a monoid, the natural transformations which intertwine it with itself is isomorphic to the classical monoidal center by evaluation at the monoid's object, and from this I have picked up the habit of saying that a core component monoid is the center of its object.) There are a couple of other ways to come across splintors. The easiest is to just strip off the composition of a category---this gives the discrete, say, first participant of a splintor for which the second participant is just the given category itself, so that every category participates in a splintor of some kind. Call such a splintor a stripping splintor or strippor for short. As in the case of core categories, every subsplintor of a strippor is a strippor, and every splintor contains a strippor which is strongly maximal as a contained strippor: This strippor is just the discrete subcategory of objects of the first participant and the object subcategory of the second participant. I call the originally given splintor an objectification of this latter object subcategory, since it amounts to a way of converting the morphisms of the object subcategory into the objects of the first participant. Objectifications are good, because they give a systematic way of converting the objectified category into a category of functors under function composition, thus generalizing the Cayley Representation Theorem for groups in a fairly grandiose manner. This would not lead anyone to think that there would be any point to objectifying a category which is already discrete, but such objectifications are precisely the splintors whose second participant's objects are the splintor double objects. Because of the endofunctoriality of the second participant's object functions, the homsets of the second participant are subcategories of the first participant, and bicomposition---simultaneously composing on the left by one morphism and on the right by another---defines a homset structuring bifunctor. For this reason, I call objectifications of discrete categories structuring categories or just structors. This will disgust you, because structors are what everyone else calls 2-categories. At any rate, every subsplintor of a structor is a structor, and every splintor contains a structor which is strongly maximal in the splintor vis-a-vis being a structor. Core categories and strippors are structors. For that matter, so is a strict monoidal category, which is just a splintor whose second participant (say) is a monoid. Here is the crucial property as far as "vertical" or pointwise composition of natural transformations is concerned. One knows that the functions from a set into the underlying set of a category have a categorical pointwise composition: (fg)(xy)=f(x)g(y) when the right side is always defined. So fix a category and a splintor and consider the functors from the category into the splintor's first participant. The underlying functions of these functors are stable under pointwise composition in the second participant, and thus the functors themselves may be said to form a category under pointwise composition in that second participant. This is why the homomorphisms from a group into a commutative group form a group under pointwise composition---because the commutative group participates in a core splintor with itself. I would almost be willing to say that a hypergeneral natural transformation is a functor into a splintor first participant just because you get one of the primary operations of the arithmetic in this way, but I realistically know that this much generality isn't going to go far in terms of my talents; so there is a need for more specialized splintors which more visibly include the classical natural transformation concept. This strong market for splintors of various sorts necessitates a more categorical phrasing of the standard banalities on transitive relations. Given a set X, define transition composition on its self-cartesian product by (a,b)(b,c)=(a,c). Any subcategory of this is a transition category on X; the whole thing is the full transition category X* on X. A transition category is a transitive relation if it is reflexive in this full transition category; i.e., it has the same objects. The term "preorder" is dropped. A transitive relation is an equivalence relation if it is its own subcategory of isomorphisms; it is a partial ordering if this subcategory is discrete. A function h:X->Y defines a functor h* between full transition categories by slotwise evaluation: h*(a, b)=(h(a),h(b)). Every functor between transitive relations is obtained by restricting and narrowing some such h*. Every equivalence relation is the kernel of some h*, meaning that it is the inverse image of the discrete subcategory of objects of the codomain category of h*. This said, the full transition category of the underlying set of a category participates with the self-product of the category in a splintor. A subsplintor for which the first participant is a transitive relation on this underlying set is a stable transitive relation on the given category. So a partially ordered group is a splintor. Also interesting is the product category whose first component is the said full transition category and whose second component is the said self-product, since it contains various subcategories of "commutative squares", where I use quotes because I may be referring to commuting to within an isomorphism or to within an inequality or, generally, to within a morphism of some specified category which I'll call the value category. I'm now pretty close to the ideas of a cell category and a cell splintor. These are splintor concepts. Begin with an objectification (B,C) of the category A (with composition \# on C and hence on A) whose quasi-commutative squares are to be constructed. Form the product category A*\times(A\times A), where A* is the full transition category of the underlying set of A. Take the value category B to be the first participant of the given objectification, and form the set [A*\times(A\times A)]\times B, showing no interest in its cartesian product composition, because there is a subset S of it which has a more interesting cell composition. To bring this out, write the quintuples in [A*\times(A\times A)]\times B in attachment form, so that a member looks like (q,u,b,v,p) with b in B, (u,v) in A\times A and the transition (q,p) in A*. In this, ( q,u,v,p) is the square (of A-morphisms) which is to be regarded as commuting to within the morphism b. So S consists of those quintuples for which q\# u and v\# p are defined in A, while b is in the homset of B-morphisms from v\# p to q\# u, and domains and codomains are organized as follows: The domain of b in C is the domain of p in C which is also the domain of u in C, while the codomain of b in C is the codomain in C of q and also the codomain in C of v. These quintuples are the cells of (B,C). The cell composite of a cell (r,s,c,t,q) with cell (q,u,b,v,p) is the cell (r,s\#u,(c\#u)(t\#b),t\#v,p). The outside components are just the composite of (r,s,t,q) with (q,u,v,p) in [A*\times(A\times A)] when the members of this category are written as attached pairs. The middle term, which involves one composition in B, is defined whenever the composite (r,s,t,q)(q,u,v,p) is defined in [A*\times(A\times A)]. So this defines cell composition relative to an objectification. It is categorical, and the projection (q,u,b,v,p)->(q,u,v,p) is injective when restricted to the set of objects of S, thus has a subcategory of [A*\times(A\times A)] as image, and this subcategory is reasonably called the category of squares which commute to within a B-morphism. Now I can say that a natural transformation (to within B) is a functor from some category into the cell category S. To get the idea closer to the classical form, you notice that following such a functor by the detaching functors (q,u,b,v,p)->u and (q,u,b,v,p)->v gives candidates for the domain and codomain functors (my domains are on the right, and codomains are on the left) of the natural transformation, and, to get a fully extended intertwining function, follow by (q,u,b,v,p)->b. This last map is functorial into B exactly when the given splintor (B,C) is a structor (i.e., a 2-category), which is so if and only if it is surjective. Both B and C have functorial representations in S in this case, which is my personal, idiosyncratic explanation of why the elements of 2-categories are called cells. To get pointwise composition out of this, you construct a second participating cell category by first of all reversing B to get a splintor (B',C) which still objectifies A. Then you construct the cell category of this semireversed splintor and apply the double switch (q,u,b,v,p)->(v,p,b,q,u) to pull the semireverse cell composition back onto the underlying set of the first cell category S. This gives the second participant T of the the cell splintor (S,T) of (B,C). Pointwise composition of natural transformations means pointwise composition of functors into S in T. By the way, (S,T) is a structor exactly when the objectified category A is discrete, which reflects the fact that forming a cell splintor does not change (except by a functorial isomorphism) a splintor's maximal structor, nor does the core change. This is my argument that structors are not enough to fully describe the cell concept. To get the classical idea of a natural transformation, begin with a discrete value category B; that is, begin with the strippor of C, then regard the natural transformation as running from A to C. This is justified by the fact that, in this case, the cell category S is isomorphic to its commutation category by the projection (q,u,b,v,p)->(q,u,v,p); so the intertwining function (q,u,b,v,p)->b can just as well be written as (q,u,v,p)->qu=vp, and so on. When this follows the functor version of a classical natural transformation, it gives the fully extended intertwining function which I mentioned in my first email. You can see that, as far as this point of view goes, there is no particularly obvious conflict between function composition of natural transformations and pointwise composition. Function composition doesn't obviously exist when values are not discrete. There is presumably still plenty to be said in terms of function composition of splintor functors, but I haven't thought about this at all, and I'm not likely to start until I have understood your note. Thanks for your comments and your patience if you have any left. Pat Donaly From rrosebru@mta.ca Mon Jun 9 11:41:33 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:41:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNo1-0002cF-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:39:29 -0300 Message-ID: <005601c32ddd$f6137b00$0ed5f8c1@wanadoo.fr> Reply-To: "jpradines" From: "jpradines" To: Subject: categories: Re: reference : normal categorical subgroup ? Date: Sun, 8 Jun 2003 18:48:29 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 34 Though I have no reference for just the definition, I can make some historical remarks which perhaps explain the absence of reference, and = which may be of interest for some people, and also give references for some = (much less obvious) developments of the subject concerning groupoids in the category of manifolds and much more general ones. About 1964 or 5, I had the opportunity of mentioning to Charles = Ehresmann that I had noticed the fact that the theory of factoring a group by a = normal (or invariant or distinguished) subgroup extends almost obviously to = groupoids. I was very surprised with his answer : "The question of quotients is a = very difficult one which I have solved recently and a part of the theory will = be proposed as the subject of examination for my students of DEA. I really don't know how you could manage". It is likely that this was a polite = way of suggesting that I was certainly wrong in his opinion, but he didn't want = to listen more explanation. Sometimes later, reading chapter III of his book on categories = (published in 1965), I realized that he was certainly alluding to his very general = theory of factoring a category by an equivalence relation or by a subcategory, = while satisfying a universal property. Though this theory looks rather exhaustive and contains some rather deep and sophisticated statements, it seems in my opinion strictly impossible to deduce from any of these statements the very simple case of groupoids = and normal subgroupoids nor even the very definition of a normal = subgroupoid. I just recall here briefly what has certainly been discovered (at least = partially) by any people having had the opportunity of meeting the question and thinking ten = minutes to it, to know that the case of groups can be exactly mimicked for = groupoids with just two precautions : -first, of course, expressions such as xHy have to be understood as = denoting all the composites of the form xhy which are defined (where h runs in H) = ; as a consequence the condition of normality for H in G (in which y is = the inverse of x) bears only on the isotropy groups of H; -secund and more significantly it is no more true in general that the = right and left cosets xH and Hx coincide ; however one just has to define the elements = of the factor groupoid as consisting of two-sided cosets HxH ; with this slight = modification of the theory, everything becomes an obvious exercise. One has also to notice that there is a special case where no = modification is required, to know the case when H is actually a subgroup, i.e. just = reduced to its isotropy groups. In that case the base of the factor groupoid is = not changed. This case is the most obvious and also probably the best known = (and possibly for most people the only one known), but in my opinion = certainly not the most interesting, since it does not include the quotient of a = set by an equivalence relation, whose graph is viewed as a subgroupoid = of a coarse groupoid. Now what I really had in mind was not the purely algebraic (rather = obvious) setting, but the study of quotients for the differentiable groupoids (nowadays called smooth or Lie) introduced by Ehresmann in 1959, which = are groupoids in the category of manifolds. The statement I had obtained (which again certainly cannot by any means = be deduced from the general results of Ehresmann concerning topological or structured groupoids) was published in 1966 in my Note (prealably = submitted to Ehresmann and transmitted by him) : -Th=E9orie de Lie pour les groupo=EFdes diff=E9rentiables. Relations = entre propri=E9t=E9s locales et globales, CRAS (Paris), s=E9rie A, t.263, = p.907-910, 19 d=E9cembre 1966- in Th=E9or=E8me 5 (in this statement the Bourbaki term "subimmersion" is improperly used and has to be understood in the more restricted = acception "submersion onto a submanifold" ; note also that the implication from = 2=B0 to 1=B0 is valid only when the fibres of the domain map of H are connected). (Note that in = this statement the algebraic theory of the two-sided quotient of a = groupoid by an invariant subgroupoid is implicitely considered as "well = known" without reference. This was in fact a diplomatic consequence of = the above-mentionned conversation ! At least at that period it seems = absolutely certain that no reference did exist, and probably very few = people, if any, had had the opportunity of thinking to that sort of = questions, since the main stream of categoricists were despising = groupoids as beig trivial, since equvalent to groups). The unpublished proof of this statement relied on a careful and rather delicate study of the foliation defined by the two-sided cosets. The very elegant proof for the case of Lie groups given in Serre, Lie Algebras and Lie Groups (lecture in Harvard, 1964, p.LG 4.10-11), = relying on the so-called Godement's theorem, works only for one-sided cosets and yields only the too special = case above-mentioned or more generally the statement of Proposition 2 in the previous Note (which extends to groupoids the classical theory of = homogeneous spaces for possibly non invariant subgroups). It is clear that this last proof may be immediately written in a purely diagrammatic way and remains valid in much more general contexts when an abstract Godement's theorem is available. It turns out that this is the = case for most of (perhaps almost all) the categories considered by "working mathematicians", notably the abelian categories as well as toposes, the category of topological spaces (with a huge lot of variants), the category of Banach spaces, and many useful categories that are far from = being complete.The precise definitions for what is meant by an abstract = Godement's theorem were given in my paper : -Building Categories in which a Godement's theorem is available- published in the acts of the Second Colloque sur l'Alg=E8bre des = Cat=E9gories, Amiens 1975, Cahiers de Topologie....(CTGDC). In this last paper I introduced the term "dyptique de Godement" for a category in which one is given two subcategories of "good mono's" and = "good epi's" (playing the roles of embeddings and surmersions in Dif) such = that a formal Godement's theorem is valid. These considerations explain why I was strongly motivated for adapting Serre's diagrammatic proof to the case of two-sided cosets (since such a = proof would immediately extend the theory of quotients for groupoids in = various non complete categories used by "working mathematicians", = yielding a lot of theorems completely out of the range of Ehresmann's = general theory of structured groupoids). However this was achieved only in 1986 in my Note : -Quotients de groupo=EFdes diff=E9rentiables, CRAS (Paris), t.303, = S=E9rie I, 1986, p.817-820.- The proof requires the use of certain "good cartesian squares" or "good = pull back squares", which, though they are not the most general pull back's = existing in the category Dif of manifolds, cannot be obtained by the (too restrictive) classical condition of transversality. Though written in = the framework of the category Dif (in order not to frighten geometers, but = with the risk of frightening categoricists), this paper is clearly thought in order to be easily generalizable in any category where a suitable set of distinguished pull back's is available , assuming only some mild = stability properties. In this paper I introduced the seemingly natural term of "extensors" for naming those functors between (structured) groupoids which arise from = the canonical projection of a groupoid onto its quotient by a normal subgroupoid. Equivalent characterizations are given.(I am ignoring if = another term is being used in the literature).This notion is resumed and = used in my paper : -Morphisms between spaces of leaves viewed as fractions- CTGDC, vol.XXX-3 (1989),p. 229-246 which again is written in the smooth context, but using purely = diagrammatic descriptions (notably for Morita equivalences and = generalized morphisms) allowing immediate extensions for various = categories. As a prolongation of this last paper, I intend in future papers to give = a description of the category of fractions obtained by inverting those extensors with connected fibres. This gives a weakened form of Morita equivalence which seems basic for understanding the transverse structure = of foliations with singularities. Jean PRADINES ---- Original Message ----- From: Marco Mackaay To: categories Sent: Thursday, June 05, 2003 4:49 PM Subject: categories: reference: normal categorical subgroup? > To all category theorists, > , p.> I'm looking for a reference to the definition of a normal = categorical From rrosebru@mta.ca Mon Jun 9 11:41:33 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:41:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNp4-0002jE-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:40:34 -0300 Message-ID: <003001c32e09$ddf7e520$af51f8c1@wanadoo.fr> Reply-To: "jpradines" From: "jpradines" To: References: <1c5.9c17e04.2c097945@aol.com> Subject: categories: Re: Function composition of natural transformations? (Pat Donaly) Date: Mon, 9 Jun 2003 00:03:06 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 35 Just a few naive remarks about natural transformations and their two = compositions. I think comfortable to define natural transformations as functors, which = is not the case, neither for the classical "object to arrow" nor for the = "arrow to arrow" definition. Now this can be achieved in two obviously equivalent ways. In the following the letter I (though or because it is frequently used = also to denote the unit interval) will picture the category denoted by 2 = in CWM (just one arrow e going from the object 0 to the object 1) while = QA will denote the category of commutative squares in the category A, = endowed with the "horizontal" composition. (Note that the arrows of A = may be described as functors from I to A and the arrows of QA as = functors from the product category I x I to A). Then the first definition is : a natural transformation between the = categories A and B is nothing else than a functor from A to QB.=20 With this first definition, the vertical composition of natural = transformations comes immediately from the "vertical" composition in QB = (which is indeed a double category). The secund definition (which is just a more symmetric reformulation of = the "arrow to arrow" definition) seems to be less popular, though very = useful in my opinion : a natural transformation between the categories A = and B is also nothing else than a functor from the product category I x = A to B.=20 This can also may be viewed as a functor from I x A to I x B, letting = the first component be just the canonical projection from I x A to I. Then the horizontal composition is just the composition of functors. The latter definition is especially convenient when working with = categories (or groupoids) in a category. For instance one knows = immediately what is a smooth natural transformation (of course I is = endowed with the discrete structure). It also allows to define = immediately the horizontal composition for "higher order natural = transformations", replacing I by its n'th power. Jean PRADINES ----- Original Message -----=20 From: To: Sent: Saturday, May 31, 2003 5:19 AM Subject: categories: Function composition of natural transformations? = (Pat Donaly) > Here is a technical/pedagogical question which has been bothering me = for > about twelve years. >=20 > In problem 5 on page 19 of "Categories for the Working Mathematician" = (CWM), > Saunders Mac Lane points out that a natural transformation may be = fully > extended to an intertwining function from one category to another, = intertwining > meaning (except in the void case), that the function transforms on one = side > according to its domain functor and on the other according to its = codomain functor. From rrosebru@mta.ca Mon Jun 9 11:50:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:50:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNvM-0003Gq-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:47:04 -0300 Date: Sat, 7 Jun 2003 15:18:01 +0100 (BST) From: Ranko Lazic X-Sender: lazic@gem To: categories@mta.ca Subject: categories: PhD studentship In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 36 Dear Colleagues, We would be grateful if you brought this to the attention of potential students. --- Department of Computer Science University of Warwick England PhD studentship Scalable Software Model Checking Based on Game Semantics A three-year PhD studentship funded by the Engineering and Physical Sciences Research Council is available from October 2003. It covers academic fees, and living expenses at the following rates: GBP 9,000 (2003/04), GBP 10,500 (2004/05), GBP 12,000 (2005/06). * Project summary Model checking has been a highly successful approach to verification of hardware and protocols. Recently, model checking of software has become an active and important area of research and application. In contrast to hardware and protocols, software is often highly structured, and contains objects, higher-order computation, complex control mechanisms, pointers, concurrency, and other features. Although impressive tools have been built, a number of substantial challenges remain for software model checking. One of the main breakthroughs in theoretical computer science in the past decade has been the development of game semantics, which has produced the first accurate models for a variety of programming languages and logical systems. Founding software model checking on game semantics has the potential to overcome most of the remaining challenges, because the models are compositional in the style of denotational semantics, yet have clear operational content. We propose contributions to theory and practice of the novel research direction of software model checking based on game semantics. Our main goal is to enable compositional verification of programs and specifications which contain large, polymorphic or infinite data types. This has not been addressed so far, but is necessary for the approach to scale to industrial software. The studentship will be supervised by Dr R Lazic, within the Theory and Practice of Programming research group led by Prof D Peled. Collaboration is planned with the Foundations of Computation research group at Oxford, and with Formal Systems (Europe) Ltd. * Requirements and application You should have at least a II.1 degree in Computer Science or Mathematics, or equivalent. You need to have experience of at least one of: - semantics of programming languages, - automata theory, - process algebra, - category theory. Further information is available at: http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/res/phd.html Informal enquiries by e-mail are welcome: Ranko.Lazic@dcs.warwick.ac.uk You can apply on-line, stating the project title in Question 13: http://www.warwick.ac.uk/study/postgraduate/ Closing date: 11 July 2003. From rrosebru@mta.ca Mon Jun 9 11:50:19 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:50:19 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNwj-0003Ns-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:48:29 -0300 Date: Mon, 9 Jun 2003 10:18:11 +0100 (BST) From: Paul B Levy To: categories@mta.ca Subject: categories: Re: topos logic arising nicely In-Reply-To: <200306051946.VAA19086@fb04305.mathematik.tu-darmstadt.de> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 37 On Thu, 5 Jun 2003, Thomas Streicher wrote: > Hi Paul, > > > "The neglect of sum types is the root of all evil." > > To some extent this may be true for programming languages (but see recent > work of Jim Laird). For logics it is less clear. Actually you mean the > empty type, isn't it? which is the n=0 instance of the n-ary sum connective. So it should be included in even the simply typed setting. Paul > Moreover, sunset types are slightly heavier than > ordinary sum types. Subset types are rather dependent sum types. From rrosebru@mta.ca Mon Jun 9 11:51:40 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:51:40 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNx6-0003QN-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:48:52 -0300 Message-ID: <3EE48CE7.D72A64B0@bangor.ac.uk> Date: Mon, 09 Jun 2003 14:34:31 +0100 From: Ronnie Brown X-Mailer: Mozilla 4.79 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Function composition of natural transformations? References: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 38 There is another way of looking at the strict multiple globular category case, which is to use the monoidal closed structure, as ws established via the cubical case in 116. (A. AL-AGL, R. BROWN and R. STEINER), ``Multiple categories: the equivalence between a globular and cubical approach'', Advances in Mathematics 170 (2002) 71-118. This monoidal closed structure is fairly clear cubically, but is difficult to translate into globular formulae in higher dimensions. If A=END(C), where C is a multiple category (globular or cubical), so that A is one also, then the `enriched composition' is a morphism A \otimes A \to A. In low dimensions this gives left and right whiskering A_0 \times A_1 \to A_1, A_1 \times A_0 \to A_1, and there is also a function say { , }: A_1 \to A_1 \to A_2, which measures the lack of agreement of two possible definitions of compositions, and I think this is what Tom refers to in his email. In the cubical formulation, A_2 consists of `squares', and the sides of the squares are easy to interpret using whiskering. One way round the square is a.g \circ f.v and the other is f.u\circ b.g if f:a \to b, g:u \to v. In the groupoid case, ideas of this type are used in 59. (R. BROWN and N.D. GILBERT), ``Algebraic models of 3-types and automorphism structures for crossed modules'', {\em Proc. London Math. Soc.} (3) 59 (1989) 51-73. and in other papers of Nick Gilbert. The extra structure on a crossed module M (or 2-groupoid, for that matter) of a monoid morphism M \otimes M \to M allows the modelling of homotopy 3-types. However, for calculations of 3-types, crossed squares seem better, because of a Van Kampen Type theorem, not apparently available for the other structures. Ronnie Brown Tom LEINSTER wrote: > > This may be `mere' pedagogy for ordinary categories, but if you try the > same thing for 2-categories then it becomes a `genuine' issue. To put it > another way, the two different but equivalent presentations of a concept > (natural transformation) become, on categorification, significantly > different. > snip... -- Professor Emeritus R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Centre for the Popularisation of Mathematics: http://www.cpm.informatics.bangor.ac.uk/ (reorganised site with new sculpture animations) From rrosebru@mta.ca Mon Jun 9 11:52:10 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Jun 2003 11:52:10 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PNyz-0003bC-00 for categories-list@mta.ca; Mon, 09 Jun 2003 11:50:49 -0300 From: "Jean-Pierre Marquis" To: Subject: categories: RE: Semantic tableaux and intuitionistic logic Date: Mon, 9 Jun 2003 10:05:01 -0400 Message-ID: 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: X-Keywords: X-UID: 39 The following references might be of some interest: Bell, J.L. & DeVidi, D., Solomon, G., 2001, Logical Options, Broadview Press. Marcello D'Agostino, Dov M. Gabbay, Reiner Hahnle, Joachim Posegga, 1999, Handbook of Tableau Methods, Kluwer Academic Pub. Jean-Pierre Marquis -----Message d'origine----- De : cat-dist@mta.ca [mailto:cat-dist@mta.ca]De la part de Thomas Streicher Envoye : 6 juin, 2003 04:14 A : categories@mta.ca Objet : categories: Re: Semantic tableaux and intuitionistic logic > I am only familiar with semantic tableaux for > classical propositional logic (and classical 1st order > logic). It seems that as an inference system it is > based squarely around the law of the excluded middle > because it is essentially reductio ad absurdum. Hence, > as an inference system it can't be simply modified for > intuitionistic propositional calculus?? (Of course, I > am bringing this because the role that Heyting > algebras play in Topos theory). the point is that tableau calculus may be best understood as a search for cut-free proofs in either classical or intuitionistic logic; this fact is systematically overlooked in the literature on tableaux methods like in the logic programming community one hardly ever finds exposed the view that executing a logic program is nothing but unravelling an inductive definition for information on tableau methods from a proof-theoretic point of view see Troelstra & van Dalen's book "Constructivism in Mathematics" vol.2, the chapter on proof theory of intuitionistic logic Best, Thomas From rrosebru@mta.ca Tue Jun 10 19:16:36 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Jun 2003 19:16:36 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PrMI-0004nN-00 for categories-list@mta.ca; Tue, 10 Jun 2003 19:12:50 -0300 From: Thomas Streicher Message-Id: <200306092003.WAA31522@fb04305.mathematik.tu-darmstadt.de> Subject: categories: Re: topos logic arising nicely To: categories@mta.ca Date: Mon, 9 Jun 2003 22:03:51 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (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: X-Keywords: X-UID: 40 Dear Steve, > > Coincidentally, for quite different reasons I have just been looking at > the Fourman/Scott theory as a way to deal with partial functions. > > Scott's system for existence and identity is given a Hilbert style > presentation, and I suppose - I may be wrong - that that is why > Fourman's interpretation makes such heavy use of the higher order > structure of toposes. Do you know of any sequent presentations? I think it is straightforward to give a sequent style formulation of the Fourman/Scott interpretation. BTW one has to take care of inhabitedness of types (in the general case) because variables of type A range over A whereas terms of type A receive there interpretation in \tilde{A}, the partial map clasifier of A. See e.g. Troelstra and van Dalen 2nd Chapter for a traetment of what they call E-logic. Just as example the rules for \forall look as follows \Gamma |- A(x) x \not\in FV(\Gamma) --------------------------------------- \Gamma |- \forall x. A(x) \Gamma |- \forall x. A(x) \Gamma |- t\downarrow ------------------------------------------------------ \Gamma |- A[t/x] where t\downarrow stand for "t defined". What I meant with my remark is that if one allows partial terms then one need not have subtypes. Best, Thomas PS Fourman and Scott exploit higher order aspects already at first order level because \tilde{A} is a subobject of P(A) , namely the subsingletons. From rrosebru@mta.ca Tue Jun 10 19:16:36 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Jun 2003 19:16:36 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PrNf-0004wv-00 for categories-list@mta.ca; Tue, 10 Jun 2003 19:14:15 -0300 Reply-To: From: "Noson Yanofsky" To: "categories@mta. ca" Subject: categories: A paper for people who fear categories. Date: Mon, 9 Jun 2003 17:05:26 -0400 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 41 Dear Esteemed Category Theorists, I have written the following paper for the few people in the world who dread/hate category theory. (I have been told such people exist. Perhaps you know of some.) The paper takes an idea of Lawvere and puts it into a language of sets and functions. Many examples are given to show how one scheme can describe numerous diverse phenomena. The paper should be readable by any undergraduate with a discrete math course. No category theory is used in the paper but the spirit of category theory is employed throughout. Enjoy, Noson Yanofsky =============================== A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points Abstract: Following F. William Lawvere, we show that many self-referential paradoxes, incompleteness theorems and fixed point theorems fall out of the same simple scheme. We demonstrate these similarities by showing how this simple scheme encompasses the semantic paradoxes, and how they arise as diagonal arguments and fixed point theorems in logic, computability theory, complexity theory and formal language theory. Available at: http://xxx.lanl.gov/abs/math.LO/0305282 From rrosebru@mta.ca Tue Jun 10 19:16:36 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Jun 2003 19:16:36 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19PrP1-00053w-00 for categories-list@mta.ca; Tue, 10 Jun 2003 19:15:39 -0300 From: Jpdonaly@aol.com Message-ID: <1d1.b5f6499.2c167d88@aol.com> Date: Mon, 9 Jun 2003 20:17:12 EDT Subject: categories: Re: Function composition of natural transformations? (Pat Don... To: categories@mta.ca 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: X-Keywords: X-UID: 42 Thanks, Jean. As an assiduous student of CWM, I was aware of this and will always wonder why Mac Lane didn't just make the point explicit in his first edition in 1971. The only thing left to realize is that the category of commutative squares which you mention is a subcategory of a product category and thus has a couple of projection functors on it which can be used to follow a functor to get the domain and codomain functors of the natural transformation, so that this version of naturality is much more neatly packaged than the usual diagram. I believe that there is a worker named John Baez (deep apologies for any naive and unforgivable errors here) who says that Mac Lane claimed to be interested not in functoriality so much as naturality when he was coinventing category theory; I wonder when and if he realized that naturality is a brand of functoriality. It would seem that this realization would come very early. In general, if one fixes an argument in a bifunctor, the resulting function is a fully extended intertwining function, and I believe that your point is that every natural transformation arises in this way. So already naturality is an artifact of functoriality. Mitchell notices much of this in his 1965 book. From rrosebru@mta.ca Thu Jun 12 13:02:13 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Jun 2003 13:02:13 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19QUPZ-0006Fn-00 for categories-list@mta.ca; Thu, 12 Jun 2003 12:54:49 -0300 Message-ID: <20030610212350.52749.qmail@web12205.mail.yahoo.com> Date: Tue, 10 Jun 2003 14:23:50 -0700 (PDT) From: Galchin Vasili Subject: categories: re: More Topos questions ala "Conceptual Mathematics" To: categories@mta.ca In-Reply-To: <000701c2d910$a0faa480$39a14244@grassmann> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 43 Hello, I have been reading up on the Curry-Howard isomorphism. In the last chapter of "Conceptual Mathematics" Lawvevre and Schanuel say that the logical connectives are completely analogous to categorical operations x, map object and +. Is this an oblique reference to the Curry-Howard isomorphism? Regards, Bill Halchin --- Stephen Schanuel wrote: > Probably it's easiest to try to define > implication yourself, and then > you'll see that it is just what 'Conceptual > Mathematics' says -- but if you > need more help: > > 'Implication' is supposed to be a binary > operation on Omega, i.e. a map > from OmegaxOmega to Omega. How can we go about > specifying such a map? > > Well, a map from any object X to Omega amounts > (by the universal > property) to a subobject of X, so we're looking for > a subobject of > OmegaxOmega, i.e. a monomorphism with codomain > X=OmegaxOmega. Now how can we > go about specifying a nonomorphism with a given > codomain X? Perhaps the > simplest way is to specify two maps with domain X > and common codomainY; then > the equalizer of these will do. > > See if you can think of two maps from > OmegaxOmega to Omega whose > equalizer seems to capture the intuitive notion of > 'implication'. It might > help to start with a simple case, the category of > sets, where Omega is just > the two-element set with elements called T (true) > and F (false). (If you > have ever seen 'truth tables', you will see that > what you are looking for is > also called the 'truth table for implication', but > if you haven't seen > these, please ignore this remark.) If you succeed in > specifying the pair of > maps, you will have learned much more than you can > by reading further; but > if after trying you are still stuck, then read on. > > The desired two maps from OmegaxOmega to Omega > are: > (1) projection on the first factor, and > (2) conjunction, which was defined in the paragraph > just preceding the one > you're stuck on. > > I hope you managed to find these maps, but even > if you didn't, you can > now have fun by looking at the maps conjunction, > imlication, negation, etc, > in irreflexive graphs (and other simple toposes) and > comparing these with > those in sets; you'll learn why Boolean algebra, so > familiar in sets, needs > to be replaced by Heyting algebra in more general > toposes. > > Good luck in your studies! > > Yours, > Steve Schanuel > ----- Original Message ----- > From: "Galchin Vasili" > To: > Sent: Wednesday, February 19, 2003 7:16 PM > Subject: categories: More Topos questions ala > "Conceptual Mathematics" > > > > > > Hello, > > > > 1) In the very last chapter (Session 33 "2: > Toposes and logic" of > "Conceptual Mathematics" where the authors cover > topoi, they define '=>' > for the internal Heyting algebra of Omega: > > > > "Another logical operation is 'implication', which > is denoted '=>'. This > is also a map Omega x Omega->Omega, defined as the > classifying map of the > subobject S 'hook' Omega x Omega determined by the > all those > in Omega x Omega such that alpha "subset of" beta." > > > > Starting from "subobject S 'hook" ......" I got > totally lost. I am > frustrated because I know this is crucial to > understanding why Omega is an > internal Heyting algebra, so any help would be > appreciated. (I am assuming > that alpha and beta are subojects of Omega???). > > > > 2) In the same Session 33 on pg 350 is a set > "rules of logic". These are > exactly the axioms for a Heyting algebra, yes? > > > > > > > > Regards, Bill Halchin > > > > > > > > > > __________________________________ Do you Yahoo!? Yahoo! Calendar - Free online calendar with sync to Outlook(TM). http://calendar.yahoo.com From rrosebru@mta.ca Thu Jun 12 13:02:13 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Jun 2003 13:02:13 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19QUQu-0006L6-00 for categories-list@mta.ca; Thu, 12 Jun 2003 12:56:12 -0300 Message-ID: <006901c32ff4$dc151240$a0d8f8c1@wanadoo.fr> Reply-To: "jpradines" From: "jpradines" To: References: <1d1.b5f6499.2c167d88@aol.com> Subject: categories: Re: Function composition of natural transformations? (Pat Don... Date: Wed, 11 Jun 2003 10:37:35 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 44 Thank you for your quick answer. I am not sure to understand it quite well. I must confess that I = consider myself much more as a differential geometer than as a = "categoricist", so that I am not at all well informed about categorical = literature. In fact I am often considered as a dissident in both fields, = since my general philosophy is : -first that there is a lot of interesting things to do in Geometry using = categories, an idea with which unfortunately most geometers, save = Ehresmann, disagree ; - secund that most of the classical tools developed by category = theorists, including Ehresmann, are not the best adapted for that = purpose, and I tried to develop some alternative tools (which indeed = most people ignore). It is not the place here to say more on that subject.=20 About the precise point in discussion the main object of my letter was = to emphasize the secund aspect of the definition (functor from I x A to = B or more symmetrically to I x B), which seems less familiar (is it = written somewhere ?) than the first one, and in my opinion the simplest = and the most useful (at least for my personal use). For each arrow f of = A from a to a', the image of I x {a, f, a'}, which may also be regarded = as an image of I x I, gives immediately a commutative square in A and = its diagonal (3 x 3 =3D 9 arrows including the unit ones), where one = reads immediately all the useful aspects of the data, displayed in a = perfectly geometric and symmetric way, in contrast with the usual = definitions, in which the two functors and the naturality arrow seem to = play quite unsymmetrical roles. (Of course all of this is so perfectly = obvious that I am convinced that plenty of people have noticed this, but = I must confess that I have never read (nor heared) it, though in my = opinion it is the best way of describing a natural transformation.)=20 I think also than it would be often useful to consider more frequently = the obvious canonical structure of double category on a product category = and especially on I x A, and I x I. Jean PRADINES ----- Original Message -----=20 From: Jpdonaly@aol.com=20 To: jpradines@wanadoo.fr=20 Cc: categories@mta.ca=20 Sent: Tuesday, June 10, 2003 2:17 AM Subject: Re: categories: Re: Function composition of natural = transformations? (Pat Don... Thanks, Jean. As an assiduous student of CWM, I was aware of this and = will always wonder why Mac Lane didn't just make the point explicit in = his first edition in 1971. The only thing left to realize is that the = category of commutative squares which you mention is a subcategory of a = product category and thus has a couple of projection functors on it = which can be used to follow a functor to get the domain and codomain = functors of the natural transformation, so that this version of = naturality is much more neatly packaged than the usual diagram. I = believe that there is a worker named John Baez (deep apologies for any = naive and unforgivable errors here) who says that Mac Lane claimed to be = interested not in functoriality so much as naturality when he was = coinventing category theory; I wonder when and if he realized that = naturality is a brand of functoriality. It would seem that this = realization would come very early. In general, if one fixes an argument = in a bifunctor, the resulting function is a fully extended intertwining = function, and I believe that your point is that every natural = transformation arises in this way. So already naturality is an artifact = of functoriality. Mitchell notices much of this in his 1965 book.=20 From rrosebru@mta.ca Sat Jun 14 18:43:58 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Jun 2003 18:43:58 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19RIiD-00006H-00 for categories-list@mta.ca; Sat, 14 Jun 2003 18:37:25 -0300 Date: Sat, 14 Jun 2003 12:00:53 +0100 (BST) From: Ronnie Brown X-X-Sender: mas010@publix To: categories Subject: categories: Re: reference: normal categorical subgroup? In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 45 A definition of normal subcrossed module was given by Kathy Norrie in her thesis, (see the references to her work in two papers in the April, 2003, issue of Applied Categorical Structures). Of course crossed modules are equivalent to cat^1-groups, (G,s,t), so it is a nice exercise to do the translation. The expected answer is (H,s',t') such that H is normal in G and invariant under s,t. However categorical groups are different to cat^1-groups, so it is a nice exercise to solve this problem. It would also be good to characterise groupoid objects internal to categorical groups, since these should generalise the congruences for those objects, and hopefully lead to a definition of free groupoid in categorical groups, and so to notions of free resolutions. For cat^1-groups (and crossed modules) there is a nice notion of induced object (see papers by Brown and Wensley in TAC, for example) which is required to compute the 2-type of a mapping cone induced on classifying spaces by a morphism of groups. Best regards Ronnie On Thu, 5 Jun 2003, Marco Mackaay wrote: > To all category theorists, > > I'm looking for a reference to the definition of a normal categorical > subgroup, i.e. the right kind of subgroupoid of a categorical group for > taking the quotient. I know the definition, but I have no reference. Does > anyone know a published origin of the definition? > > Best wishes, > > Marco Mackaay > > > > > > > > Prof R. Brown, School of Informatics, Mathematics Division, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382681 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Centre for the Popularisation of Mathematics Raising Public Awareness of Mathematics CDRom Symbolic Sculpture and Mathematics: http://www.cpm.informatics.bangor.ac.uk/centre/index.html From rrosebru@mta.ca Sun Jun 15 20:04:58 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Jun 2003 20:04:58 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19RgUy-00037U-00 for categories-list@mta.ca; Sun, 15 Jun 2003 20:01:20 -0300 Date: Sun, 15 Jun 2003 18:33:06 -0400 From: Fred E.J. Linton To: Subject: categories: Address change X-Mailer: USANET web-mailer (CM.0402.5.5) Mime-Version: 1.0 Message-ID: <654HFowhg9136S03.1055716386@uwdvg003.cms.usa.net> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 46 Greetings. Those of you who have recorded any variation of the e-mail address <0004142427/FEJLINTON@MCIMAIL.COM> for me (perhaps name only, or number only, with or w/o leading zeros) should become aware that after June 30, 2003, MCI Mail will cease to exist, having been cut off life-support as part of the restructuring of MCI/WorldCom. Instead, please use my university e-mail address, which is , or the secondary, back-up, address: . Many thanks. -- Fred Linton From rrosebru@mta.ca Sun Jun 15 20:04:58 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Jun 2003 20:04:58 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19RgWG-0003Gp-00 for categories-list@mta.ca; Sun, 15 Jun 2003 20:02:40 -0300 Date: Sun, 15 Jun 2003 18:44:48 -0400 From: Fred E.J. Linton To: Subject: categories: CFP: SIPR Calcutta 2004 X-Mailer: USANET web-mailer (CM.0402.5.5) Mime-Version: 1.0 Message-ID: <841HFowSW1472S08.1055717088@uwdvg008.cms.usa.net> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 47 Greetings. Those planning to attend the AMS December 2003 meeting = in Bangalore, India, may wish to plan to stay a bit longer, to participate in a mathematical subsection I have been asked to organize, for a meeting of the Society for = Indian Philosophy and Religion (SIPR) taking place = in early January, 2004, in Calcutta. Further details will post here as they become available. Or, to be included in more direct, personal e-mailings about this event, please express your tentative interest = directly to me at the address below, bearing in mind that summer conference travels may prevent my acknowledging = your interest until early July at the soonest. Thanks. -- Fred E.J. Linton Department of Mathematics, Wesleyan Univ., Middletown, CT 06459 USA From rrosebru@mta.ca Sun Jun 15 20:04:59 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Jun 2003 20:04:59 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19RgY4-0003SQ-00 for categories-list@mta.ca; Sun, 15 Jun 2003 20:04:32 -0300 From: Luca Mauri To: categories@mta.ca Subject: categories: Preprint: Algebraic theories in monoidal categories Date: Sun, 15 Jun 2003 10:49:57 +0200 User-Agent: KMail/1.5 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200306151049.57887.mauri@math.uni-duisburg.de> Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 48 PREPRINT ANNOUNCEMENT Algebraic theories in monoidal categories Luca Mauri Abstract. We define a monoidal semantics for algebraic theories. The basis for the definition is provided by the analysis of the structural rules in the term calculus of algebraic languages. Models are described both explicitly, in a form that generalises the usual definition in sets; and from a category-theoretical point of view, as monoidal functors on suitable classifying categories. The semantics obtained includes as special cases both the semantics of ordinary algebraic theories in Cartesian categories, and the semantics of operads and multicategories over sets. The article is in PDF format (~250 KB, 26 pages) and can be be downloaded using either of the following: "http://128.6.62.2/~mauri/Algebraic theories in monoidal categories" "http://128.6.62.2/~mauri/atmc.pdf" (older browsers) Comments and suggestions are welcome. Luca Mauri mauri@math.uni-duisburg.de From rrosebru@mta.ca Tue Jun 17 16:33:19 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Jun 2003 16:33:19 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19SM8G-0004ms-00 for categories-list@mta.ca; Tue, 17 Jun 2003 16:28:40 -0300 Message-Id: <200306171625.h5HGPNg07087@kira.research.avayalabs.com> To: categories@mta.ca Subject: categories: "twisted" Galois connections? Date: Tue, 17 Jun 2003 12:25:23 -0400 From: Philip Wadler Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 49 Is anything known about the following variation on a Galois connection? Given domains X and A with partial orders, f:X->A and g:A->X constitute a *Galois connection* if the following four conditions hold (1) x <= y implies f(x) <= f(y) (2) a <= b implies g(a) <= g(b) (3) x <= g(f(x)) (4) f(g(a)) <= a (This is equivalent to saying f(x) <= a iff x <= g(a).) The same functions constitute a *twisted Galois connection* if we have conditions (1)-(3) and also (4') a <= f(g(a)) Both Galois connections and twisted Galois connections compose. If f:X->A, g:A->X and h:A->Z, k:Z->A consitute a (twisted) Galois connection, then so do f;h:X->Z, k;g:Z->X. Is there anything in the literature about twisted Galois connections or the corresponding notion of a twisted adjoint, perhaps under a different name? Many thanks, -- P ----------------------------------------------------------------------- Philip Wadler wadler@avaya.com www.research.avayalabs.com/user/wadler Avaya Labs, 233 Mount Airy Road, Basking Ridge, NJ 07920 USA phone +1 908 696 5137 fax +1 908 696 5402 ---------------------------------------------------------------------- "When a Mathematical Reasoning can be had it's as great a folly to make use of any other, as to grope for a thing in the dark, when you have a Candle standing by you." John Arbuthnot, 1692 ---------------------------------------------------------------------- From rrosebru@mta.ca Tue Jun 17 16:33:19 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Jun 2003 16:33:19 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19SM7K-0004hF-00 for categories-list@mta.ca; Tue, 17 Jun 2003 16:27:42 -0300 Message-Id: X-Mailer: Novell GroupWise Internet Agent 6.0.2 Date: Tue, 17 Jun 2003 14:50:29 +1000 From: "Tony Bryant" To: Subject: categories: Categories in Economics Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 50 Dear Categorists, Can anyone supply me with references to uses of category theory and related concepts/arguments in economic theory? Thanks, Tony Bryant Head of Economics MACQUARIE UNIVERSITY From rrosebru@mta.ca Wed Jun 18 19:05:15 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Jun 2003 19:05:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Skyx-0003Tv-00 for categories-list@mta.ca; Wed, 18 Jun 2003 19:00:43 -0300 X-Authentication-Warning: harper.uchicago.edu: cefreer owned process doing -bs Date: Tue, 17 Jun 2003 19:44:46 -0500 (CDT) From: Cameron Freer X-Sender: cefreer@harper.uchicago.edu To: categories@mta.ca Subject: categories: Re: Categories in Economics In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 51 > Dear Categorists, > > Can anyone supply me with references to uses of category theory and > related concepts/arguments in economic theory? > > Thanks, > > Tony Bryant > Head of Economics > MACQUARIE UNIVERSITY I have no idea what else is out there, but Sonnenschein once mentioned the following paper to me: An Axiomatic Characterization of the Price Mechanism Hugo Sonnenschein Econometrica, Vol. 42, No. 3. (May, 1974), pp. 425-434. As of three years ago, I think that he was unaware of any other category-theoretic economics papers. - Cameron From rrosebru@mta.ca Wed Jun 18 19:09:56 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Jun 2003 19:09:56 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Sl7b-00043G-00 for categories-list@mta.ca; Wed, 18 Jun 2003 19:09:39 -0300 Message-id: <13560194@newdancer.Dartmouth.EDU> Date: 18 Jun 2003 13:39:10 EDT From: Andrei.Prokopiw@Dartmouth.EDU (Andrei Prokopiw) Subject: categories: first isomorphism theorem To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-MailScanner: No virus detected by mailhub2.Dartmouth.EDU Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 52 Is there a suitable first isomorphism theorem in category theoretic lan= guage? One barrier for me seems to be the correct notion of an image. W= hat seems best right now would be that given f:X->Y, ker(coker f) =3D c= oker ( ker f). Here the left hand side would represent im f, and the ri= ght hand side X/kerf. If this is the right notion, what are the necessa= ry conditions on the category for it to hold? -Andrei Prokopiw From rrosebru@mta.ca Thu Jun 19 08:00:11 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Jun 2003 08:00:11 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19Sx7c-0006U1-00 for categories-list@mta.ca; Thu, 19 Jun 2003 07:58:28 -0300 Date: Thu, 19 Jun 2003 00:59:18 -0700 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: first isomorphism theorem Message-ID: <20030619075917.GL13356@math-cl-n01.ucr.edu> References: <13560194@newdancer.Dartmouth.EDU> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <13560194@newdancer.Dartmouth.EDU> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 53 Andrei Prokopiw wrote: >Is there a suitable first isomorphism theorem in category theoretic language? >One barrier for me seems to be the correct notion of an image. What seems best >right now would be that given f:X->Y, ker(coker f) = coker ( ker f). Here the >left hand side would represent im f, and the right hand side X/kerf. If this >is the right notion, what are the necessary conditions on the category for it >to hold? I'm not really answering your question, instead addressing the "if". One of the classic examples of the isomorphism theorems is for rings, and the category of rings (with unit) has neither kernels nor cokernels. There are ways around that limitation in this case, such as: * Don't require rings to have units; or * Analyse any specific f in a category of X-modules. But more importantly, I think that much of the point of the theorem is that the image is a purely set-theoretic notion, definable without reference to the algebraic properties of f. In the category of sets, the image is (of course) not realisable as the kernel of the cokernel, but it does exist as the equaliser of the cokernel pair. It seems to me that the essence of the isomorphism theorem is that the forgetful functor from algebras to sets not only preserves limits (which we all know) but also preserves images and coimages (defined as above), even though it does *not* preserve coequalisers or cokernel pairs. The classical form of the theorem is simply a reflection of an inability to speak explicitly about functors' preserving categorical constructions. -- Toby Bartels From rrosebru@mta.ca Thu Jun 19 10:48:58 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Jun 2003 10:48:58 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19SzlA-0004gW-00 for categories-list@mta.ca; Thu, 19 Jun 2003 10:47:28 -0300 Date: Thu, 19 Jun 2003 08:52:03 -0400 (EDT) From: Michael Barr To: categories@mta.ca Subject: categories: Re: first isomorphism theorem In-Reply-To: <20030619075917.GL13356@math-cl-n01.ucr.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 54 Let me just add to this reply (which is certainly one valid answer to the question) the comment that I sent privately to the questioner that exactness is sufficient for the FIT to be meaningful. On Thu, 19 Jun 2003, Toby Bartels wrote: > Andrei Prokopiw wrote: > > >Is there a suitable first isomorphism theorem in category theoretic language? > >One barrier for me seems to be the correct notion of an image. What seems best > >right now would be that given f:X->Y, ker(coker f) = coker ( ker f). Here the > >left hand side would represent im f, and the right hand side X/kerf. If this > >is the right notion, what are the necessary conditions on the category for it > >to hold? > > I'm not really answering your question, instead addressing the "if". > ... From rrosebru@mta.ca Fri Jun 20 13:17:28 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 20 Jun 2003 13:17:28 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19TOUz-0006we-00 for categories-list@mta.ca; Fri, 20 Jun 2003 13:12:25 -0300 Message-Id: <4.1.20030620074844.011a6620@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Fri, 20 Jun 2003 07:49:49 -0400 To: categories@mta.ca From: Charles Wells Subject: categories: My email address Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 55 My correct email address is cwells@oberlin.net My freude.com address was canceled in January and I just found out that my cwru.edu address hasn't been working for a couple of weeks. If anyone has recently sent me messages to those address, please resend them. Thanks Charles Wells Charles Wells professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html genealogical website: http://familytreemaker.genealogy.com/users/w/e/l/Charles-Wells/ NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm From rrosebru@mta.ca Fri Jun 20 13:18:35 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 20 Jun 2003 13:18:35 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19TOai-0007J9-00 for categories-list@mta.ca; Fri, 20 Jun 2003 13:18:20 -0300 Date: Fri, 20 Jun 2003 16:08:14 +0200 Message-Id: <200306201408.h5KE8Eoe003128@urano.sip.ucm.es> To: categories@mta.ca From: alberto@sip.ucm.es Subject: categories: CFP: WRLA 2004 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 56 [[ -- Apologies for multiple copies of this message -- ]] + + + + + WRLA'04 + + + + + CALL FOR PAPERS + + + + + WRLA'04 + + + + + +----------------------------------------------------------+ | | | 5th International Workshop on | | Rewriting Logic and its Applications | | | | W R L A 2004 | | | | Barcelona, Spain, March 27-28, 2004 | | | | http://www.fdi.ucm.es/wrla2004 | +----------------------------------------------------------+ The workshop will be held in conjunction with ETAPS 2004 7th European Joint Conferences on Theory and Practice of Software March 27 - April 4, 2004 http://www.lsi.upc.es/etaps04 IMPORTANT DATES November 24, 2003 Deadline for submission January 15, 2004 Notification of acceptance February 18, 2004 Final version in electronic form March 27-28, 2004 Workshop in Barcelona AIMS AND SCOPE Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas. The topics of the workshop comprise, but are not limited to, * foundations and models of RL; * languages based on RL, including implementation issues; * RL as a logical framework; * RL as a semantic framework, including applications of RL to - object-oriented systems, - concurrent and/or parallel systems, - interactive, distributed, open ended and mobile systems, - specification of languages and systems; * extensions of RL, including - real-time and probabilistic extensions, - tile logic, - rewriting approaches to behavioral specifications; * verification techniques for RL specifications, including - equational and coherence methods, and - verification of properties expressed in modal and temporal logics; * comparisons of RL with existing formalisms having analogous aims, including - rho-calculus, - structural operational semantics, - concurrency calculi, - dynamic algebras. PAST EVENTS Previous WRLA workshops have been organized in - Asilomar, California, September 3-6, 1996, - Pont-a-Mousson, France, September 1-4, 1998, - Kanazawa, Japan, September 18-20, 2000, - Pisa, Italy, September 19-21, 2002. The proceedings of the WRLA workshops have been published as volumes 4, 15, 36, and 71 in the Elsevier ENTCS series, available at http://www.elsevier.nl/locate/entcs Selected papers from WRLA'96 have been published in a special issue of Theoretical Computer Science, Volume 285(2), 2002. LOCATION WRLA 2004 will be held in Barcelona, Spain in March 27-28, 2004. It is a satellite workshop of ETAPS 2004, the European Joint Conferences on Theory and Practice of Software. For venue, registration and suggested accommodation see the ETAPS 2004 web page http://www.lsi.upc.es/etaps04 For information about Barcelona, see among others the city web page http://www.bcn.es/english/ihome.htm PROGRAM COMMITTEE David Basin ETH Zurich Manuel Clavel Universidad Complutense de Madrid Steven Eker SRI International, Menlo Park Kokichi Futatsugi JAIST, Tatsunokuchi Fabio Gadducci Universita di Pisa Alexander Knapp LMU, Muenchen Claude Kirchner INRIA Lorraine & LORIA, Nancy Salvador Lucas Universidad Politecnica de Valencia Narciso Marti-Oliet Universidad Complutense de Madrid (Chair) Jose Meseguer University of Illinois at Urbana-Champaign Ugo Montanari Universita di Pisa Pierre-Etienne Moreau INRIA Lorraine & LORIA, Nancy Grigore Rosu University of Illinois at Urbana-Champaign Carolyn Talcott SRI International, Menlo Park SUBMISSIONS Submissions will be evaluated by the Program Committee for inclusion in the proceedings, which will be available at the time of the workshop and are expected to be published in the Elsevier ENTCS series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. They must be unpublished and not submitted simultaneously for publication elsewhere. Papers (of at most 15 pages) should be submitted electronically, preferably as PDF files, to the workshop email address wrla2004@sip.ucm.es providing also a text-only abstract, and detailed contact information of the corresponding author. The final program of the workshop will also include system demonstrations and two invited presentations by Gilles Dowek Ecole Polytechnique & INRIA, Palaiseau Mario Rodriguez-Artalejo Universidad Complutense de Madrid Based on the quality and interest of the accepted papers, the program committee will study the possibility of preparing a special issue of a scientific journal in the field. ORGANIZING COMMITTEE Narciso Marti-Oliet, Manuel Clavel, and Alberto Verdejo Departamento de Sistemas Informaticos y Programacion Universidad Complutense de Madrid, Spain CONTACT INFORMATION For more information, please contact the organizers wrla2004@sip.ucm.es or visit the workshop web page http://www.fdi.ucm.es/wrla2004 IMPORTANT DATES November 24, 2003 Deadline for submission January 15, 2004 Notification of acceptance February 18, 2004 Final version in electronic form March 27-28, 2004 Workshop in Barcelona + + + + + WRLA'04 + + + + + CALL FOR PAPERS + + + + + WRLA'04 + + + + + From rrosebru@mta.ca Fri Jun 20 17:03:34 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 20 Jun 2003 17:03:34 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19TS4o-00036T-00 for categories-list@mta.ca; Fri, 20 Jun 2003 17:01:38 -0300 Date: Fri, 20 Jun 2003 15:33:51 -0400 (EDT) From: Susan Niefield To: categories@mta.ca Subject: categories: Union College Conference Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-RAVMilter-Version: 8.4.3(snapshot 20030212) (nott.union.edu) Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 57 UNION COLLEGE MATHEMATICS CONFERENCE Saturday and Sunday Schenectady November 8-9, 2003 New York This is a preliminary announcement for the eleventh Union College Mathematics Conference. This year the conference topics are algebraic topology, category theory, and differential geometry. In addition to plenary lectures of interest to the entire Conference audience, there will also be shorter contributed talks in parallel sessions. Anyone interested in giving such a talk should contact one of the organizers. The meeting will begin with an evening reception on Friday, November 7, and end on Sunday afternoon. A more detailed notice will be mailed later this summer. Information will also be available at the Union College Mathematics Department website (www.math.union.edu) in August. Union College is centrally located in New York's capital district about 10 miles from the Albany International Airport, easily accessible by train from NYC, and just 3 to 4 hours by car from NYC, Boston, and Montreal. We hope to see you in November! ORGANIZERS Category Theory Susan Niefield niefiels@union.edu Kimmo Rosenthal rosenthk@union.edu Algebraic Topology Brenda Johnson johnsonb@union.edu Kathryn Lesh leshk@union.edu Differential Geometry Christina Tonnesen-Friedman tonnesec@union.edu From rrosebru@mta.ca Mon Jun 23 13:30:26 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Jun 2003 13:30:26 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19UU8m-0000Ro-00 for categories-list@mta.ca; Mon, 23 Jun 2003 13:26:00 -0300 Date: Mon, 23 Jun 2003 11:03:24 -0400 (EDT) From: F W Lawvere To: categories@mta.ca Subject: categories: Halchin's question re Curry-Howard Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 58 >> I have been reading up on the Curry-Howard isomorphism. >> In the last chapter of Conceptual Mathematics, Lawvere >> and Schanuel say that the logical connectives are >> completely analogous to the categorical operations x, >> map object and +. Is this an oblique reference to the >> Curry-Howard isomorphism? At the 1963 Model Theory conference in Berkeley, I pointed out that an interlocking system of adjoints occurring in set theory and type theory has also as a very special example the one arising in the logic of parts. In Eilenberg and Kelly's 1965 pioneering paper on closed categories, part of my result was cited and it came to be known as the statement that Heyting algebras are cartesian closed categories. In my papers "Adjointness in Foundations"(submitted December 15th 1967), "Equality in Hyperdoctrines...", and "Diagonal Arguments...", I tried to clarify these and related matters. I became aware at some point that Haskell Curry in one of his books had informally pointed out earlier the possible importance of this as an analogy. In the late 1960s, Bill Howard, a student of Mac Lane, began circulating his results which were finally published in 1980; Howard's paper could be described as containing an oblique reference to the closed category theorems. The term "isomorphism" which has emerged in the literature is rather misleading since the map in question is bijective at best at the level of subjective presentations, rather than at the level of objective algebras. That is to say, a symbolic presentation of a particular Heyting algebra can always be construed in many ways as an image of a presentation of a cartesian closed category, but there is the additional draconian rule of inference which says that any two maps with a given domain and codomain are equal. I tried to give a more accurate description of this situation by referring to "an adjunction" rather than to an isomorphism in my paper "Adjointness in and Among Bi-categories" Logic and Algebra, Lecture Notes in Pure and Applied Mathematics, vol. 180, pp 181-189, edited by A. Ursini and P. Agliano', Marcel Dekker, 1996. Bill Lawvere ************************************************************ F. William Lawvere Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************ From rrosebru@mta.ca Mon Jun 23 15:56:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Jun 2003 15:56:04 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19UWOH-0005LU-00 for categories-list@mta.ca; Mon, 23 Jun 2003 15:50:09 -0300 To: categories@mta.ca Subject: categories: Re:first isomorphism theorem Date: Mon, 23 Jun 2003 14:43:36 -0400 From: wlawvere@buffalo.edu Message-ID: <1056393816.3ef74a583a9e7@mail2.buffalo.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 59 Toby Bartels pointed out >>the essence of the isomorphism theorem is that the forgetful functor to >>sets not only preserves limits but also preserves images and coimages >>even though it does not preserve coequalizers and cokernel pairs. In fact, as recent papers of Adamek,Lawvere,& Rosicky, and also of Pedicchio & Wood, have exploited, such forgetful functors do preserve all coequalizers of pairs which admit a reflexivity in the category; the preservation of images is a consequence. From rrosebru@mta.ca Tue Jun 24 10:10:55 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 24 Jun 2003 10:10:55 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19UnX7-0005eD-00 for categories-list@mta.ca; Tue, 24 Jun 2003 10:08:25 -0300 Date: Tue, 24 Jun 2003 05:14:01 -0400 (EDT) From: Thorsten Palm To: Subject: categories: Papers available Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 60 Dear categorists, My Ph.D. dissertation, entitled `Dendrotopic Sets for Weak Infinity-Categories', and a preliminary version of my paper `Dendrotopic Sets' can now be downloaded from the web-page www.math.yorku.ca/Who/Grads/palm . The content of the two works is summarized below, where they are referred to as [A] and [B] respectively. Best regards Thorsten Palm ---------------- In his unpublished paper [1], Makkai defined a notion of _weak infinity-category_ (under the name `multitopic omega-category'). The underlying geometric structures, called _multitopic sets_, are described in the three-part paper [2]. Makkai takes a weak infinity-category to be a multitopic set with the mere property that _compositions_ exist, which are defined as equivalences of certain _coslice_ objects. [A] gives a definition of weak infinity-categories equivalent to Makkai's. While this definition falls into the same two stages, it is considerably shorter and more elementary in each of them. The description of the underlying geometric structures, called _dendrotopic sets_ here, is done purely combinatorially (whereas [2] uses the algebraic machinery of multicategories). A coslice object comes in two guises, in both of which it is a dendrotopic set with mild extra structure in the form of a dendrotopic map (whereas in [1] it is a model for a new signature for Makkai's first-order logic with dependent sorts). [A] also presents an alternative method of introducing composition to a dendrotopic set. Here one has to impose the extra structure of a _universality system_: a subset that behaves in such a way that each member can be thought of as a universal arrow. The main theorem of [A] states that a dendrotopic set containing a universality system is a Makkai weak infinity-category. The concept of a dendrotopic set is defined at a more leisurely pace in [B], where the equivalence to the concept of a multitopic set is, indirectly, established. References: [1] M. Makkai: `The multitopic omega-category of all multitopic omega-categories'; mystic.biomed.mcgill.ca/Makkai [2] C. Hermida, M. Makkai, A. J. Power: `On weak higher dimensional categories'; Journal of Pure and Applied Algebra. Part 1: 154 (2000), pp. 221-246; part 2: 157 (2001), pp. 247-277; part 3: 166 (2002), pp. 83-104 From rrosebru@mta.ca Tue Jun 24 10:13:32 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 24 Jun 2003 10:13:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19UnbS-0005z3-00 for categories-list@mta.ca; Tue, 24 Jun 2003 10:12:54 -0300 Message-ID: <3EF84D09.3070201@bath.ac.uk> Date: Tue, 24 Jun 2003 14:07:21 +0100 Subject: categories: Open positions: Research (Bunched ML); Lectureships. From: David Pym Status: RO X-Status: X-Keywords: X-UID: 61 [Apologies for cross-postings.] Readers of this list may be interested in the following open positions in the (recently established) Department of Computer at the University of Bath, England: 1. One Research Officer position (post-doc) --- UK EPSRC-funded project, "Bunched ML" (roughly, operational and denotational models of ML-like languages with bunched typed systems, based on bunched logic. This project is jointly run by Prof. David Pym at Bath and Profs. Peter O'Hearn and Edmund Robinson at Queen Mary, London. Details below; 2. Two permanent lectureships (roughly, Associate Prof.) --- any area of computer science, though see the reserach areas listed below; 3. One 3-year lectureship (roughly, Assistant Prof.) --- any area of computer science, though see the reserach areas listed below. The University of Bath was placed 5th overall in this year's Times UK University Rankings (6th for CS), see http://www.timesonline.co.uk/section/0,,716,00.html, and is located in a very beautiful city. Official advert follows. UNIVERSITY OF BATH Department of Computer Science: Lectureships (3 posts); Research Officer. Lectureships (Ref: 03/157) The Department of Computer Science seeks to appoint, from as soon as possible, to two lectureships and one fixed-term lectureship (3 years - as a direct result of a Royal Society Industry Fellowship awarded to Professor Pym) The Department is multi-disciplinary and has internationally renowned research. Three main research areas are: Human Computer Interaction, Mathematical Foundations and Applications, Media Technology. We are seeking to appoint in each of the existing main research areas but by exception will also consider well qualified applications in other areas of Computer Science. For teaching purposes we need expertise in mainstream computer science topics. Applicants should normally hold a PhD or have equivalent research experience in Computer Science and show evidence of or the ability to publish in international journals or conferences and to obtain research funding. Salary in the range =A326,270 to =A333,679 (Lecturer Grade B). Informal enquiries to Professor Peter Johnson, Head of Department (P.Johnson@bath.ac.uk; Tel +44(0)1225 383214, Fax +44(0)1225 383493). Research Officer Post (Ref: 03/160) Applications are also invited for the post of Research Officer on the EPSRC-funded project "Bunched ML" under the direction of Prof. David Pym, d.j.pym@bath.ac.uk, http://www.bath.ac.uk/~cssdjp who may be contacted for an informal discussion of the post. This project is funded jointly with Prof. Peter O'Hearn's group at Queen Mary, University of London, and is concerned with the operational and denotational semantics of ML-like programming languages which use bunched typed systems, based on bunched logic. Applicants should have a doctorate in a relevant area of computer science or mathematics and an interest in programming languages with polymorphism, program logics, and their semantics. Programming skills would be advantageous. The post is available for three years from 1 November, 2003 or as soon as possible thereafter. The starting salary is =A321, 125 pa. Applicants should complete an application form and may attach a CV. More information about the Department can be found at: http://www.bath.ac.uk/comp-sci/ Application forms and further particulars for both posts are available from Juliet Hills, Personnel Officer, University of Bath, Claverton Down, Bath, BA2 7AY, (tel. 01225 386873; fax 01225 386559; e-mail adsjf@bath.ac.uk) or e-mail jobs@bath.ac.uk or phone the 24 hour answer-phone service on Bath (01225) 386924, or textphone (01225) 386039 quoting the appropriate reference number. Closing date for applications: Friday 25th July 2003. An equal opportunities employer. --=20 Prof. David J. Pym Telephone: +44 (0)1 225 38 3246 Professor of Logic & Computation Facsimile: +44 (0)1 225 38 3493 University of Bath Email: d.j.pym@bath.ac.uk Bath BA2 7AY, England, U.K. Web: http://www.bath.ac.uk/~cssdjp From rrosebru@mta.ca Thu Jun 26 11:38:29 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Jun 2003 11:38:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19VXZB-0004p4-00 for categories-list@mta.ca; Thu, 26 Jun 2003 11:17:37 -0300 Message-ID: <1056631728.3efaebb036ee2@www.informatics.bangor.ac.uk> Date: Thu, 26 Jun 2003 13:48:48 +0100 From: tporter@informatics.bangor.ac.uk To: categories@mta.ca Subject: categories: job: Research post in Bangor MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 User-Agent: Internet Messaging Program (IMP) 3.1 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 62 Dear All This is an announcement about a forthcoming research position at Bangor. The full announcement will appear on the web at : www.jobs.ac.uk within the next few days. The post is for 10 months only as the funding is for a Pilot project and one of the tasks for the Research Assistant will be to help in the preparation of an extended proposal. Please draw it to the attention of any suitable candidates. Thanks Tim Porter PS. for people outside the U.K. If you don't know North Wales, it is a beautiful area of the U.K. and the School Of Informatics is very near the sea and the mountains!!!! ................... UNIVERSITY OF WALES, BANGOR SCHOOL OF INFORMATICS MATHEMATICS DIVISION Research Officer (Fractafolds, their geometry and topology) Salary: =A318,265 - =A320,311 (on R&A Grade 1A) p.a. Applications are invited for the above Leverhulme funded Pilot Project post available for a period of 10 months. Based in the Mathematics Division of the School of Informatics, you will work on the problem of identifying a class of topological spaces that bear something of the same relationship to certain well structured fractal spaces as manifolds bear to Euclidean spaces. This is a pilot project to evaluate various candidate classes of spaces for =91fractafold=92 status. The candidate spaces are fractal, but also are, in various different ways =91homogeneously fractal=92. The test for success will be indications that a possible fractal analogue of differential geometry can be applied to the study of these spaces. Thus you will study the various classes of candidate spaces to see if the development of such a =91differential geometry=92 on fractals impo= ses extra conditions on them or distinguishes between the different candidate classes. Dependent on the success of this initial testing, it is hoped that a full-scale project lasting a further two years will be awarded. One of your tasks will be to assist the project coordinator in the preparation of full grant applications. You should possess a strong mathematical background (PhD) with research experience in one or more of the following areas: fractals; algebraic, geometric or differential topology; areas of analysis, or differential geometry; category theory; or certain relevant areas of mathematical physics (finite approximation theory, discrete differential manifolds, etc.) or theoretical computer science (digital topology, constructive analysis, etc.). Application forms and further particulars should be obtained by contacting Human Resources, University of Wales, Bangor, Gwynedd LL57 2DG; tel: + 44 (0)1248 382926/388132; e-mail: personnel@bangor.ac.uk Please quote reference number 03-2/231 when applying. Closing date for applications: Friday 25th July, 2003. Interviews will be held in early September, 2003. Informal enquiries can be made by contacting Professor T. Porter, e-mail: t.porter@bangor.ac.uk tel: +44 (0)1248 382492. Committed To Equal Opportunities Name: advert03-2-231.doc advert03-2-231.doc Type: Winword File (application/msword) Encoding: base64 Download Status: Not downloaded with message ----- End forwarded message ----- -------------------------------------------------- School of Informatics, University of Wales, Bangor This mail sent through IMP: http://horde.org/imp/