From MAILER-DAEMON Tue Jul 28 14:17:51 2009 Date: 28 Jul 2009 14:17:51 -0300 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1248801471@mta.ca> X-IMAP: 1235946422 0000000094 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 Sun Mar 1 18:13:18 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Mar 2009 18:13:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LdttO-00060m-Os for categories-list@mta.ca; Sun, 01 Mar 2009 18:12:14 -0400 Date: Sun, 01 Mar 2009 16:23:11 +0100 From: Anders Kock MIME-Version: 1.0 To: categories@mta.ca Subject: categories: beta version of new book available: "Synthetic Geometry of Manifolds" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Anders Kock Message-Id: Status: O X-Status: X-Keywords: X-UID: 1 Dear all, A beta version of my new book "Synthetic Geometry of Manifolds" is available via my homepage, http://home.imf.au.dk/kock/ This book deals with some classical spaces in differential geometry, namely the "prolongation spaces" or "neighbourhoods of the diagonal". These spaces provides a natural way of describing some of the basic constructions in local differential geometry, and in fact, is an inviting gate to differential geometry, and also to some of those differential-geometric notions that exist in algebraic geometry. In the present text, the neighbourhoods of the diagonal are dealt with, and utilized, using the axiomatic method of synthetic differential geometry; this obviates many of those technical difficulties, which till now has made the use of these neighbourhoods rather uninviting. Some of the specific differential geometric theories dealt with here are connection theory (notably affine connections), geometric distributions, differential forms, jet bundles, differentiable groupoids, differential operators, Riemannian metrics, harmonic maps. Anders Kock From rrosebru@mta.ca Tue Mar 3 07:22:28 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Mar 2009 07:22:28 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LeSew-0004Wd-Bx for categories-list@mta.ca; Tue, 03 Mar 2009 07:19:38 -0400 Date: Mon, 2 Mar 2009 23:57:55 +0100 (CET) From: Lutz Strassburger To: categories@mta.ca Subject: categories: Deadline Extension for SD'09 in Bordeaux MIME-Version: 1.0 Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII Sender: categories@mta.ca Precedence: bulk Reply-To: Lutz Strassburger Message-Id: Status: O X-Status: X-Keywords: X-UID: 2 Due to popular demand there will a deadline extension for the workshop "Structures and Deduction 2009" in Bordeaux, July 20-24, 2009. New deadline for submission: Sunday, March 8, 2009 Further details can be found on the webpage Kind regards, Lutz Strassburger From rrosebru@mta.ca Tue Mar 3 07:22:29 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Mar 2009 07:22:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LeSeJ-0004Uv-Sd for categories-list@mta.ca; Tue, 03 Mar 2009 07:18:59 -0400 From: Thorsten Altenkirch To: Categories list Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: PhD positions at Nottingham & Swansea Date: Mon, 2 Mar 2009 15:34:39 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Thorsten Altenkirch Message-Id: Status: O X-Status: X-Keywords: X-UID: 3 Hi, we have two fully funded PhD positions in our project on induction- recursion: one at Swansea (with Anton Setzer) and one at Nottingham (with me). This would be perfect for people who are interested in the foundations of Type Theory. See http://www.cs.nott.ac.uk/~txa/phd.html Please forward this information to talented students who are looking for funding. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. From rrosebru@mta.ca Tue Mar 3 07:22:29 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Mar 2009 07:22:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LeScx-0004Ro-IO for categories-list@mta.ca; Tue, 03 Mar 2009 07:17:35 -0400 From: Guy McCusker To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: PhD studentships in Computer Science at Bath Date: Mon, 2 Mar 2009 15:10:13 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Guy McCusker Message-Id: Status: O X-Status: X-Keywords: X-UID: 4 The studentships advertised below may be of interest to readers of the categories list: note especially that John Power is available to supervise research in category theory, with particular application to computer science. ------- The Department of Computer Science at the University of Bath is currently recruiting PhD research students in the area of Mathematical Foundations. A number of fully-funded studentships are available to cover fees and an annual stipend, subject to eligibility. The Mathematical Foundations group at Bath conducts research in: * logic and semantics of programming languages (Laird, McCusker, Power, Pym) * category theory and proof theory (Guglielmi, Power, Pym) * computer algebra, computational geometry, cryptography, networks and security (Bradford, Davenport, Richardson, Vorobjov) * logic programming, answer-set programming, artificial intelligence and multi-agent systems (De Vos, Nickles, Padget) For more details on our PhD programme, please visit http://www.bath.ac.uk/comp-sci/postgraduate/phd/index.html A complete list of staff members in Mathematical Foundations and their research interests can be found at http://www.cs.bath.ac.uk/department/mathematical-foundations/staff-research-interests.html Informal enquiries may be made to any member of staff in the department. An application form may be downloaded from http://www.bath.ac.uk/prospectus/postgrad/apply/ To be considered for a funded place, applications should normally be received by April 2nd 2009. Further information about the department is available at http://www.bath.ac.uk/comp-sci From rrosebru@mta.ca Thu Mar 5 22:04:52 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Mar 2009 22:04:52 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LfPOw-0002U9-N7 for categories-list@mta.ca; Thu, 05 Mar 2009 22:03:02 -0400 Date: Thu, 5 Mar 2009 14:32:16 +0100 (CET) From: Lutz Strassburger To: Lutz Strassburger Subject: categories: post-doc position at INRIA Saclay (Paris) MIME-Version: 1.0 Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII Sender: categories@mta.ca Precedence: bulk Reply-To: Lutz Strassburger Message-Id: Status: O X-Status: X-Keywords: X-UID: 5 Call for a post-doc position at INRIA Saclay--Ile-de-France =========================================================== Duration: 12 month Starting date: Between 1 Oct 2009 and 1 Dec 2009 Working place: Ecole Polytechnique, LIX, Equipe Parsifal Topic: ------ Canonical proof systems Research Context: ----------------- Traditional proof systems, like sequent calculus, tableaux, or resolution do not provide canonical proofs. The reason is that their syntax allows for many irrelevant rule permutation. Proof nets have been conceived to abstract away from these rule permutation, and thus form a "bureaucracy-free" approach to encoding proofs. But the lack of explicit structure in proof nets makes algorithmic aspects of proofs difficult to describe when the logic reaches a certain expressive power. In other words, they are not suited for proof search. It is an important research problem to design new proof systems that on the one hand provide canonical (i.e., bureaucracy-free) proof objects, and on the other hand provide a rich enough structure for performing proof search. Activities for the Post Doc: ---------------------------- The main task of the successful candidate will be to support the recent research effort within the Parsifal team, in particular the work on focused proofs and proof nets. Concurrently, members of Parsifal have been pushing the notion of "focused proof" to its limit and obtained a "maximally multi-focused" proof system, which yields canonical proof objects for multiplicative additive linear logic without units. It is now important to exhibit the precise relation to proof nets and to see how this can be extended to other logics, in particular, classical logic. Skill required: --------------- The candidate should have a good background in proof theory and related fields. Application: ------------ Applicants should send their application to Lutz Strassburger before 30 April 2009. Further particulars: -------------------- The position is part of the "INRIA Action de Recherche Collaborative" REDO: The position is an INRIA-postdoc position. That means that the candidate must fulfill the formal requirements for INRIA postdocs which can be found at the web-page In particular, the candidate must have held a doctorate or Ph.D. for less than one year before the recruitment date. If the Ph.D. is not defended at the application date, you should cleary point out the defence date and the composition of jury. The salary is 2357.30 euros gross per month. The application process for this position is independent from the INRIA-postdoc campaign. Further details: From rrosebru@mta.ca Thu Mar 5 22:04:52 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Mar 2009 22:04:52 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LfPPq-0002YJ-1S for categories-list@mta.ca; Thu, 05 Mar 2009 22:03:58 -0400 Date: Thu, 5 Mar 2009 16:34:46 +0100 From: Andrew Stacey To: categories@mta.ca Subject: categories: Bi-presheaves MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Andrew Stacey Message-Id: Status: O X-Status: X-Keywords: X-UID: 6 Dear Categorists, I'm interested in looking at the following type of thing: Start with an essentially small category, T, and look at the category whose objects are triples (P,F,c) where: P is a contravariant functor T -> Set, F is a covariant functor T -> Set and c is a natural transformation from P x F to the Hom bi-functor. Morphisms are pairs of natural transformations P_1 -> P_2 and F_2 -> F_1 that intertwine the natural transformations c_1 and c_2. One could also enrich the whole structure. Has this cropped up anywhere before? If so, what is it called and where can I learn about it? If not, what shall I call it? If this is something standard then please pardon my ignorance. I'm fairly new to _real_ category theory and am still just learning the basics. Thanks, Andrew Stacey From rrosebru@mta.ca Thu Mar 5 22:04:52 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Mar 2009 22:04:52 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LfPOI-0002Rj-Tp for categories-list@mta.ca; Thu, 05 Mar 2009 22:02:22 -0400 From: Tom Hirschowitz To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: deadline for french application Date: Wed, 4 Mar 2009 21:20:44 +0100 Sender: categories@mta.ca Precedence: bulk Reply-To: Tom Hirschowitz Message-Id: Status: O X-Status: X-Keywords: X-UID: 7 The deadline for asking a Mcf or Pr position in a French university is Thursday April 2, 2009 at 16:00 (Paris time). All the necessary information can be found at https://extranet.ac-versailles.fr/ensup/galaxie/candidats.html . The list of positions can be found at https://extranet.ac-versailles.fr/ensup/galaxie/emplois_publies.html . Please don't hesitate to contact me for further questions, Tom From rrosebru@mta.ca Thu Mar 5 22:05:01 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Mar 2009 22:05:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LfPQo-0002bB-Id for categories-list@mta.ca; Thu, 05 Mar 2009 22:04:58 -0400 From: Thomas Streicher Date: Thu, 5 Mar 2009 16:40:08 +0100 To: categories@mta.ca Subject: categories: a question of Lubarsky MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 8 Bob Lubarsky has recently asked me a question I could answer only partially. He is not reading this mailing list and so I forward his question (since I am also interested in it). The question is whether for nonisomorphic spaces X and Y one can always find a formula in higher order arithmetic or in the language of set theory which holds in one of the toposes Sh(X), Sh(Y) but not in the other. More concretely he asked about the folowing 4 spaces R (reals) R_{\geq 0} (nonnegative reals) Q (rationals) Q_{\geq 0} (nonnegative rationals) AC_N holds for sheaves over spaces in the second line but not for sheaves over the spaces in the first line. But I couldn't tell him how to logically separate R and R_{\geq 0} or Q and Q_{\geq 0}. The background of Bob's question is his work on "forcing with settling down" (http://www.math.fau.edu/lubarsky/forcing with settling.pdf) providing a model for CZF without Fullness but Exponentiation where, moreover, the Dedekind reals are not a set but a proper class. Thomas From rrosebru@mta.ca Fri Mar 6 19:01:15 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:01:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj17-0006EL-32 for categories-list@mta.ca; Fri, 06 Mar 2009 18:59:45 -0400 Mime-Version: 1.0 (Apple Message framework v753.1) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit From: Ross Street Subject: categories: Re: Bi-presheaves Date: Fri, 6 Mar 2009 16:13:11 +1100 To: Andrew Stacey , categories@mta.ca Sender: categories@mta.ca Precedence: bulk Reply-To: Ross Street Message-Id: Status: O X-Status: X-Keywords: X-UID: 9 Dear Andrew This is what Lawvere told me about once, long ago. I think he called it the Isbell envelope; that is what I've called it ever since. It has nice properties. Lawvere explained that, applied to finite dimensional vector spaces, it fully contains the category of banach spaces and bounded linear maps. (I think I've got that right; it's awhile since I checked it.) Ross On 06/03/2009, at 2:34 AM, Andrew Stacey wrote: > Start with an essentially small category, T, and look at the > category whose > objects are triples (P,F,c) where: P is a contravariant functor T - > > Set, F is > a covariant functor T -> Set and c is a natural transformation from > P x F to > the Hom bi-functor. Morphisms are pairs of natural transformations > P_1 -> P_2 > and F_2 -> F_1 that intertwine the natural transformations c_1 and > c_2. > > One could also enrich the whole structure. > > Has this cropped up anywhere before? If so, what is it called and > where can > I learn about it? If not, what shall I call it? > > If this is something standard then please pardon my ignorance. I'm > fairly new > to _real_ category theory and am still just learning the basics. > From rrosebru@mta.ca Fri Mar 6 19:01:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:01:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj2W-0006Jz-M9 for categories-list@mta.ca; Fri, 06 Mar 2009 19:01:12 -0400 Date: Fri, 6 Mar 2009 09:19:07 +0100 From: Andrew Stacey To: Ross Street , categories@mta.ca Subject: categories: Re: Bi-presheaves MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Andrew Stacey Message-Id: Status: O X-Status: X-Keywords: X-UID: 10 Ross, Thanks for the information. I'm not surprised to hear the name 'Isbell' connected with this (nor Lawvere) as there are hints of this idea in 'Taking Categories Seriously' where Lawvere talks about 'Isbell conjugation' (though in Isbell conjugation one considers the categories of covariant and contravariant functors as separate). Looking up 'Isbell envelope' on MathSciNet came up with nothing whilst 'Isbell conjugation' only came up with two papers (one reviewed by you, I think!). One is about 'total categories', though I've yet to look at it to see if it is relevant. When you say that you call it 'the Isbell envelope', what do you mean? Is the category the 'Isbell envelope of/on the original category' or are the objects 'Isbell envelopes' and we have the category of Isbell envelopes (in/on/of the original category)? Thanks for the quick reply, Andrew On Fri, Mar 06, 2009 at 04:13:11PM +1100, Ross Street wrote: > Dear Andrew > > This is what Lawvere told me about once, long ago. > I think he called it the Isbell envelope; that is what I've called it > ever since. It has nice properties. Lawvere explained that, applied > to finite dimensional vector spaces, it fully contains the category > of banach spaces and bounded linear maps. (I think I've got that > right; it's awhile since I checked it.) > > Ross > > On 06/03/2009, at 2:34 AM, Andrew Stacey wrote: > >> Start with an essentially small category, T, and look at the category >> whose >> objects are triples (P,F,c) where: P is a contravariant functor T -> >> Set, F is >> a covariant functor T -> Set and c is a natural transformation from P x >> F to >> the Hom bi-functor. Morphisms are pairs of natural transformations >> P_1 -> P_2 >> and F_2 -> F_1 that intertwine the natural transformations c_1 and >> c_2. >> >> One could also enrich the whole structure. >> >> Has this cropped up anywhere before? If so, what is it called and >> where can >> I learn about it? If not, what shall I call it? >> >> If this is something standard then please pardon my ignorance. I'm >> fairly new >> to _real_ category theory and am still just learning the basics. >> From rrosebru@mta.ca Fri Mar 6 19:02:59 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:02:59 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj49-0006Qr-8r for categories-list@mta.ca; Fri, 06 Mar 2009 19:02:54 -0400 Date: Fri, 6 Mar 2009 10:22:49 +0000 (GMT) From: "Prof. Peter Johnstone" To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 11 The answer to the general question is surely "no": the sentences which hold in Sh(X + X) are exactly those which hold in Sh(X). Whether one can separate Sh(R) from Sh([0,\infty)) in this way is a more interesting question. Does "Brouwer's continuity theorem" hold in Sh([0,\infty))? The proof that I know for Sh(R) doesn't work over [0,\infty), but that may be because it's not the best proof. Peter Johnstone On Thu, 5 Mar 2009, Thomas Streicher wrote: > Bob Lubarsky has recently asked me a question I could answer only partially. > He is not reading this mailing list and so I forward his question (since I am > also interested in it). > The question is whether for nonisomorphic spaces X and Y one can always find > a formula in higher order arithmetic or in the language of set theory which > holds in one of the toposes Sh(X), Sh(Y) but not in the other. > More concretely he asked about the folowing 4 spaces > > R (reals) R_{\geq 0} (nonnegative reals) > > Q (rationals) Q_{\geq 0} (nonnegative rationals) > > AC_N holds for sheaves over spaces in the second line but not for sheaves > over the spaces in the first line. > But I couldn't tell him how to logically separate R and R_{\geq 0} or > Q and Q_{\geq 0}. > > The background of Bob's question is his work on "forcing with settling down" > (http://www.math.fau.edu/lubarsky/forcing with settling.pdf) providing a model > for CZF without Fullness but Exponentiation where, moreover, the Dedekind > reals are not a set but a proper class. > > Thomas > > > From rrosebru@mta.ca Fri Mar 6 19:04:01 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:04:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj5A-0006Ue-BB for categories-list@mta.ca; Fri, 06 Mar 2009 19:03:56 -0400 Date: Fri, 6 Mar 2009 09:55:28 -0500 (EST) From: Bill Lawvere To: Andrew Stacey , categories@mta.ca Subject: categories: Re: Bi-presheaves MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bill Lawvere Message-Id: Status: O X-Status: X-Keywords: X-UID: 12 Dear Andrew Stacey, When John Isbell introduced this construction in the early 1960's, he called it the 'double envelope', so I often call it the Isbell envelope. You just re-discovered it! Bill Lawvere ************************************************************ F. William Lawvere, Professor emeritus 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 ************************************************************ On Thu, 5 Mar 2009, Andrew Stacey wrote: > Dear Categorists, > > I'm interested in looking at the following type of thing: > > Start with an essentially small category, T, and look at the category whose > objects are triples (P,F,c) where: P is a contravariant functor T -> Set, F is > a covariant functor T -> Set and c is a natural transformation from P x F to > the Hom bi-functor. Morphisms are pairs of natural transformations P_1 -> P_2 > and F_2 -> F_1 that intertwine the natural transformations c_1 and c_2. > > One could also enrich the whole structure. > > Has this cropped up anywhere before? If so, what is it called and where can > I learn about it? If not, what shall I call it? > > If this is something standard then please pardon my ignorance. I'm fairly new > to _real_ category theory and am still just learning the basics. > > Thanks, > > Andrew Stacey > > > > From rrosebru@mta.ca Fri Mar 6 19:05:03 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:05:03 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj66-0006ZG-Lm for categories-list@mta.ca; Fri, 06 Mar 2009 19:04:54 -0400 Date: Fri, 6 Mar 2009 10:01:05 -0500 (EST) From: Bill Lawvere To: Andrew Stacey , categories@mta.ca Subject: categories: Re: Bi-presheaves MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bill Lawvere Message-Id: Status: O X-Status: X-Keywords: X-UID: 13 PS The Isbell envelope arises from the Isbell conjugate pair which is the adjoint pair of functors connecting set^(T^op) and (set^T)^op. It is thus a special case of the general construction in my thesis (TAC Reprints) of the total category with two descriptions which objectifies the notion of adjointness, in order to free it from dependence on enrichments in small sets. (Of course the example depends on enrichments in small sets.) ************************************************************ F. William Lawvere, Professor emeritus 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 ************************************************************ On Thu, 5 Mar 2009, Andrew Stacey wrote: > Dear Categorists, > > I'm interested in looking at the following type of thing: > > Start with an essentially small category, T, and look at the category whose > objects are triples (P,F,c) where: P is a contravariant functor T -> Set, F is > a covariant functor T -> Set and c is a natural transformation from P x F to > the Hom bi-functor. Morphisms are pairs of natural transformations P_1 -> P_2 > and F_2 -> F_1 that intertwine the natural transformations c_1 and c_2. > > One could also enrich the whole structure. > > Has this cropped up anywhere before? If so, what is it called and where can > I learn about it? If not, what shall I call it? > > If this is something standard then please pardon my ignorance. I'm fairly new > to _real_ category theory and am still just learning the basics. > > Thanks, > > Andrew Stacey > > > > From rrosebru@mta.ca Fri Mar 6 19:05:36 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:05:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj6g-0006bz-C7 for categories-list@mta.ca; Fri, 06 Mar 2009 19:05:30 -0400 Date: Fri, 6 Mar 2009 17:49:24 GMT From: Jeremy.Gibbons@comlab.ox.ac.uk To: categories@mta.ca Subject: categories: Fully-funded doctoral studentships in dependently type programming at Oxford and Strathclyde Sender: categories@mta.ca Precedence: bulk Reply-To: Jeremy.Gibbons@comlab.ox.ac.uk Message-Id: Status: O X-Status: X-Keywords: X-UID: 14 FULLY-FUNDED DOCTORAL STUDENTSHIPS IN DEPENDENTLY-TYPED PROGRAMMING AT OXFORD AND STRATHCLYDE A new EPSRC-funded project on Reusability and Dependent Types has just started, as a collaboration between the Functional Programming Laboratory at the University of Nottingham (Thorsten Altenkirch), the Algebra of Programming group at the University of Oxford (Jeremy Gibbons), and the Mathematically Structured Programming group at the University of Strathclyde (Neil Ghani and Conor McBride). We are all familiar with Milner's slogan that "well-typed programs cannot go wrong". Types express properties of programs; more expressive type systems - such as dependent typing - can state properties more precisely, providing stronger guarantees of behaviour and additional guidance in development. However, this expressivity comes at a price: more specific typing can reduce opportunities for code reuse. The goal of this project is to investigate techniques for promoting reuse without sacrificing precision; in particular, how can we layer dependently typed programs, imposing stronger invariants onto more general library code? Two fully-funded doctoral studentships are available to work in this area: one at Oxford (with JG) and one at Strathclyde (with CTM). Each covers stipend, fees (at the home/EU rate), equipment, and travel, and is for three and a half years from October 2009. The closing date for applications is 15th April 2009. For further details, see: http://web.comlab.ox.ac.uk/news/72-full.html http://personal.cis.strath.ac.uk/~conor/phds/ or contact one of the principal investigators on the project: Thorsten Altenkirch (txa@cs.nott.ac.uk) Neil Ghani (ng@cis.strathclyde.ac.uk) Jeremy Gibbons (jg@comlab.ox.ac.uk) Conor McBride (conor@strictlypositive.org) From rrosebru@mta.ca Fri Mar 6 19:06:26 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:06:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj7U-0006fx-6m for categories-list@mta.ca; Fri, 06 Mar 2009 19:06:20 -0400 From: Thomas Streicher Date: Fri, 6 Mar 2009 21:36:05 +0100 To: categories@mta.ca Subject: categories: Re: a question of Lubarsky MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 15 Dear Peter, > The answer to the general question is surely "no": the sentences > which hold in Sh(X + X) are exactly those which hold in Sh(X). Thanks for that explict argument. I told Bob a cardinality axiom. In the languages under consideration there are just countably many formulas but there are class many non-homeomorphic sober spaces. > Whether one can separate Sh(R) from Sh([0,\infty)) in this way > is a more interesting question. Does "Brouwer's continuity theorem" > hold in Sh([0,\infty))? The proof that I know for Sh(R) doesn't > work over [0,\infty), but that may be because it's not the best > proof. I don't know which proof you have in mind. Until recently I was just aware of the argument in the book by MacLane and Moerdijk using a gros topos. But just now I have found that in Troelstra & van Dalen Ch.15 Thm.3.24 says that for any completely regular, first countable space T without isolated points Sh(T) validates Brouwer's Theorem. They attribute it to Grayson. Thus Brouwer's theorem holds in any of the four spaces mentioned. Bob tells me that with his forcing with settling he can distinguish R and [0,\infty) but does not know how to distinguish Q and Q \cap [),\infty). Thomas From rrosebru@mta.ca Fri Mar 6 19:07:08 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Mar 2009 19:07:08 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lfj8C-0006kI-HW for categories-list@mta.ca; Fri, 06 Mar 2009 19:07:04 -0400 Date: Fri, 06 Mar 2009 16:22:57 -0500 To: categories@mta.ca From: "Ellis D. Cooper" Subject: categories: Eilenberg and Automata, Languages and Machines Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Ellis D. Cooper" Message-Id: Status: O X-Status: X-Keywords: X-UID: 16 Was there some kind of community backlash reaction to the work of Samuel Eilenberg on automata, languages and machines? Why did some people feel the way they did about it? What were the pro and con arguments at the time? What is the story to the best of your recollection? Thanks for any help on this merely historical question. Ellis D. Cooper Ellis D. Cooper, Ph.D. 978-546-5228 (LAND) 978-853-4894 (CELL) XTALV1@NETROPOLIS.NET From rrosebru@mta.ca Sat Mar 7 19:40:22 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Mar 2009 19:40:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lg66J-0002UT-8e for categories-list@mta.ca; Sat, 07 Mar 2009 19:38:39 -0400 Mime-Version: 1.0 (Apple Message framework v753.1) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit From: Ross Street Subject: categories: Re: Bi-presheaves Date: Sat, 7 Mar 2009 17:15:29 +1100 To: Andrew Stacey , categories Sender: categories@mta.ca Precedence: bulk Reply-To: Ross Street Message-Id: Status: O X-Status: X-Keywords: X-UID: 17 Given a category A, the Isbell envelope E(A) is the category whose objects are triplets (F_*, F^*, t) where F_* : A --> Set and F^* : A^{op} --> Set are functors and t_{a,b} : F^*(a) x F_*(b) --> A(a,b) is a family natural in a and b in A. The morphisms are as you described. There is a "double Yoneda" A --> E(A) taking c to (A(c,-), A(-,c), composition). ==Ross On 06/03/2009, at 7:19 PM, Andrew Stacey wrote: > When you say that you call it 'the Isbell envelope', what do you > mean? Is the > category the 'Isbell envelope of/on the original category' or are > the objects > 'Isbell envelopes' and we have the category of Isbell envelopes (in/ > on/of the > original category)? From rrosebru@mta.ca Sat Mar 7 19:40:23 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Mar 2009 19:40:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lg64r-0002RX-3f for categories-list@mta.ca; Sat, 07 Mar 2009 19:37:09 -0400 Date: Fri, 6 Mar 2009 19:18:59 -0500 (EST) From: Michael Barr To: "Ellis D. Cooper" , categories@mta.ca Subject: categories: Re: Eilenberg and Automata, Languages and Machines MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Barr Message-Id: Status: O X-Status: X-Keywords: X-UID: 18 Speaking for myself, there was no backlash. I well recall that at the Bowdoin meeting in 1969, Sammy gave some talks and said that the stuff was interesting and had revived his ability to work, which had been in the doldrums. (I think getting rid of Natasha helped too. He said that was expensive but worth every cent.) My attitude was that if revived him, so much the better. Michael On Fri, 6 Mar 2009, Ellis D. Cooper wrote: > Was there some kind of community backlash reaction to the work of > Samuel Eilenberg on automata, languages and machines? Why did some > people feel the way they did about it? What were the pro and con > arguments at the time? What is the story to the best of your recollection? > > Thanks for any help on this merely historical question. > > Ellis D. Cooper > > Ellis D. Cooper, Ph.D. > 978-546-5228 (LAND) > 978-853-4894 (CELL) > XTALV1@NETROPOLIS.NET > > > From rrosebru@mta.ca Sat Mar 7 19:40:58 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Mar 2009 19:40:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lg68U-0002ac-JQ for categories-list@mta.ca; Sat, 07 Mar 2009 19:40:54 -0400 Date: Sat, 7 Mar 2009 14:46:14 -0500 (EST) Subject: categories: Re: a question of Lubarsky From: "Peter LeFanu Lumsdaine" To: "Thomas Streicher" , categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Sender: categories@mta.ca Precedence: bulk Reply-To: "Peter LeFanu Lumsdaine" Message-Id: Status: O X-Status: X-Keywords: X-UID: 19 > Dear Peter, >=20 >> The answer to the general question is surely "no": the sentences which >> hold in Sh(X + X) are exactly those which hold in Sh(X). >=20 > Thanks for that explict argument. I told Bob a cardinality axiom. In th= e=20 > languages under consideration there are just countably many formulas bu= t=20 > there are class many non-homeomorphic sober spaces. The cardinality argument also shows a bit more, I guess. As you've point= ed out, the valid formulas in Sh(X) and Sh(Y) will agree if they have the= same soberification / locale, or if Y is a product of X with some discre= te space. However, even after identifying such spaces, there will still = be (certainly in classical metatheory, and I think in most weaker theorie= s) more than continuum-many classes of spaces; so these "trivial reasons"= can't be the only cases when Sh(X) and Sh(Y) validate the same formulas. -Peter. >> Whether one can separate Sh(R) from Sh([0,\infty)) in this way is a mo= re >> interesting question. Does "Brouwer's continuity theorem" hold in >> Sh([0,\infty))? The proof that I know for Sh(R) doesn't work over >> [0,\infty), but that may be because it's not the best proof. >=20 > I don't know which proof you have in mind. Until recently I was just > aware of the argument in the book by MacLane and Moerdijk using a gros > topos. But just now I have found that in Troelstra & van Dalen Ch.15 > Thm.3.24 says that for any completely regular, first countable space T > without isolated points Sh(T) validates Brouwer's Theorem. They attribu= te > it to Grayson. Thus Brouwer's theorem holds in any of the four spaces > mentioned. >=20 > Bob tells me that with his forcing with settling he can distinguish R a= nd > [0,\infty) but does not know how to distinguish Q and Q \cap [),\infty= ). >=20 >=20 > Thomas >=20 >=20 >=20 >=20 >=20 --=20 Peter LeFanu Lumsdaine Carnegie Mellon University "I shall cast out Wisdom and reject Learning; My thoughts shall wander in the silent Void." -Hsi K'ang From rrosebru@mta.ca Sun Mar 8 20:18:33 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Mar 2009 20:18:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LgSFX-0007dh-JX for categories-list@mta.ca; Sun, 08 Mar 2009 20:17:39 -0300 Date: Sun, 08 Mar 2009 12:25:09 -0700 From: Vaughan Pratt MIME-Version: 1.0 To: categories Subject: categories: Re: Bi-presheaves Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 20 Ross Street wrote: > Given a category A, the Isbell envelope E(A) is the category whose > objects > are triplets (F_*, F^*, t) where F_* : A --> Set and F^* : A^{op} --> > Set are functors > and t_{a,b} : F^*(a) x F_*(b) --> A(a,b) is a family natural in a > and b in A. The > morphisms are as you described. There is a "double Yoneda" A --> E(A) > taking > c to (A(c,-), A(-,c), composition). (For "the morphisms are as you described" to work, unless I'm missing an op somewhere, in the move from (P,F,c) to (F_*,F^*,t), P as the component that "transforms forward" has to be F^*.) I learned about the Isbell envelope from Ross just this January. Ross said he'd learned it from Bill Lawvere, who he said named it that after learning it from Isbell. In the course of some follow-up discussion, Rich Wood pointed out to us the following translation into the language of profunctors of what both Andrew and Ross wrote just now. To avoid having to play favourites by choosing between (P,F,c) and (F_*,F^*,t) I'll pick the neutral (A,X,r), r: A x X --> ? I've been using myself for this stuff, where the early letters A,B,... transform forwards and the late letters X,Y,... transform backwards, just as with Chu spaces. Organize the presheaves A and X as the profunctors A: C^op x 1 --> Set and X: 1^op x C --> Set in the category Prof (Australian: Mod) of profunctors ((bi)modules, distributors) and their natural transformations. In notation more suggestive of how they compose, these become A: 1 -|-> C X: C -|-> 1 r: AX --> 1_C where AX is profunctor composition at 1, and 1_C: C^op x C --> Set is the identity profunctor 1_C: C -|-> C in Prof, aka the homfunctor of C. In general, composition of profunctors entails a left Kan extension, but in this case the composition is taking place at 1, trivializing the composite AX to A x X: C^op x C --> Set (Andrew's P x F). The Isbell envelope being strikingly reminiscent of the Chu construction, it is natural to ask how they're related, which I'll offer an answer to in the rest of this message. A little calculation shows that for the Isbell envelope of the one-morphism category 1 (whose one object I'll denote * in the next paragraph), E(1) is equivalent to Set x Set^op. But this is also Chu(Set,1) where 1 is now the singleton set. What about Chu(Set,2)? The trick here is to take C to be the two-object category 1+1, augmented with two morphisms from what I'll call the positive copy j of 1 to the negative copy \ell, call this C_2 as the category naturally associated to the profunctor 2: 1 -|-> 1 defined by 2(*,*) = 2. I'd been doing this with what I call Dsh(2) below, but Ross pointed out to me (more generally) that Dsh(K) fully embeds in E(C_K) as follows. I'll write it assuming Rich's profunctor typing of A and X as above so that the second argument of A and the first argument of X is always the object * of 1. (In that language Ross's t_{a,b} : F^*(a) x F_*(b) --> A(a,b) becomes t_{a,b} : \int^c F^*(a,c) x F_*(c,b) --> A(a,b) which exposes the left Kan nature of the product, albeit trivial as noted above.) The objects (A,X,r) of E(C_2) now consist of two pairs of sets: A = (A(j,*),A(\ell,*)) and X = (X(*,j),X(*,\ell)). Chu(Set,2) then emerges from E(C) as the full subcategory of E(C_2) for which A(\ell,*) = X(*,j) = {}. In effect A and X behave as though they were single sets A(j,*) and X(*,\ell), the effect we need for (A,X,r) to be an ordinary Chu space. The generalization to Chu(Set,K) simply entails setting C_K(j,\ell) = K, leaving C_K(\ell,j) empty as implicitly assumed above, with |C_K(j,j)| = |C_K(\ell,\ell)| = 1, and with no other change to the description of the full subcategory of E(C_K) constituting Chu(Set,K). In a posting to this list on 9/7/02 with subject line "Presheaves etc. in a uniform way" I described (even more obscurely than my usual postings) a common generalization of presheaves and Chu spaces that can be described far more clearly using the above language. It amounts to a generalization of the Isbell envelope (which as I said I only learned about this January from Ross). Quite independently of Rich and within a day of him, Jeff Egger suggested to me exactly the following typing for A and X in this generalization. In place of the small C parametrizing the Isbell envelope E(C), take two small categories J and L (explaining the j and \ell in the above). Define a *disheaf* (at CT'04 I called these "communes") on a profunctor K: L -|-> J to be a triple (A,X,r) where A: 1 -|-> J and X: L -|-> 1 are profunctors and r: AX --> K: L -|-> J is a natural transformation. By analogy with Chu(Set,K), write Dsh(Set,K) for the category of disheaves on the profunctor K, whose morphisms are just as for the Isbell envelope, which in turn are just as for Chu spaces. The Isbell envelope E(C) = Dsh(Set,1_C). This is the sense in which Dsh generalizes E. (The "Set" parameter is a bad habit arising out of the notation Chu(V,k) adopted around 1992, I forget by whom. It is probably better to write Chu(K) and Dsh(K) and let V be inferred from context as the ambient V in which one is working, which I'll do now.) As pointed out to me by Ross, E(C) generalizes Dsh(K) by taking C to be what Ross called the *cone* C_K of K: J^op x L --> Set (L -|-> J), namely J+L augmented with morphisms from each j to each \ell picked out of the set K(j,\ell) and composed as prescribed by the functoriality of K. (I learned this category representation of profunctors/bimodules the hard way from Robert Seely at CT'04, who kindly said of my "bipartite categories" during my talk, "That's a bimodule!") The generalization is weaker (in some sense) than the other direction, in that Dsh(K) is not E(C_K) itself but only the full subcategory obtained by requiring A(j,*) = X(*,\ell) = 0 for all j in \ob(J) and \ell in \ob(L). I've recently found Dsh(K) very useful as a foundation for ontology (not so much Aristotle as XML, which among other things supplies the Web Ontology Language OWL with its presentation syntax), where it furnishes an extensional conception of the notion of attribute (which the Wikipedia article "Property (philosophy)" helpfully points out doesn't exist), makes sense of C.I. Lewis's highly controversial notion of qualia from the 1920's (philosophers today divide into qualiaphiles and qualiaphobes, see the Wikipedia article on "Qualia") as the elements of K(j,\ell), and offers a mechanism for interaction between the two components in Cartesian dualism, which failed after a century of unconvincing candidates for a meaningful such mechanism (Malebranche's occasionalism, Leibniz's monads, etc.). From a more mathematical standpoint disheaves are even more general than Chu spaces. I can imagine a few raised eyebrows here---after my decade of propaganda on Chu spaces as the ultimate universal framework, the natural question would be, how could anything be more general than a Chu space? It depends on whether you're willing to settle for some full subcategory of some Chu(Set,K) or want your category "on the nose" without the hassle of having to come up with some ad hoc characterization of the desired subcategory (cf. the distinction above between Dsh(K) as a generalization of E(C) and vice versa where only the latter requires the extra step of specifying a full subcategory). Instead one can point to a profunctor K and say that a K-flapdoodle is precisely an object of Dsh(K). For example there is a straightforwardly exhibited K such that Dsh(K) consists essentially of the inelastic acylic graphs, those having invariant path length. No presheaf category consists of these, and Isbell envelopes only contain them as a full subcategory (I don't know if there's a K large enough that Chu(K) does the same job). I have a paper on this in the works, focusing mainly on the ontology application for now and therefore trying (only half successfully I fear) to minimize the deployment of categorical weapons of math destruction in order to make it more accessible to those likely to care at all about ontology, let me know if you're interested. Vaughan Pratt From rrosebru@mta.ca Sun Mar 8 20:18:33 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Mar 2009 20:18:33 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LgSEb-0007Zr-LR for categories-list@mta.ca; Sun, 08 Mar 2009 20:16:41 -0300 From: Thomas Streicher Date: Sun, 8 Mar 2009 12:14:16 +0100 To: Peter LeFanu Lumsdaine , categories@mta.ca Subject: categories: Re: a question of Lubarsky MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 21 > The cardinality argument also shows a bit more, I guess. As you've point= > ed out, the valid formulas in Sh(X) and Sh(Y) will agree if they have the= > same soberification / locale, or if Y is a product of X with some discre= > te space. However, even after identifying such spaces, there will still = > be (certainly in classical metatheory, and I think in most weaker theorie= > s) more than continuum-many classes of spaces; so these "trivial reasons"= > can't be the only cases when Sh(X) and Sh(Y) validate the same formulas. Certainly, yust consider algebraic lattices with their Scott topology. They are all sober and connected. P(\kappa) for all cardinals \kappa provides a class of nonisomorphic such gadgets. BTW Bob suggested to characterise when two sober spaces or locales are logically indistinguishible. I find this a most difficult questions. Reminds me a bit (admittedly somewhat vague analogy) of characterising elementary equivalence of structures. There is an answer by Ehrenfeucht-Fraisse games. But this can't be use for the question at issue. Thomas From rrosebru@mta.ca Tue Mar 10 04:14:31 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Mar 2009 04:14:31 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lgw8L-0005hu-QM for categories-list@mta.ca; Tue, 10 Mar 2009 04:12:13 -0300 Date: Mon, 09 Mar 2009 20:10:29 -0400 From: jim stasheff MIME-Version: 1.0 To: Categories list Subject: categories: [Fwd: Fw: copyright etc] Content-Type: text/plain Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: jim stasheff Message-Id: Status: O X-Status: X-Keywords: X-UID: 22 From: "Ronnie Brown" To: "jim stasheff" Subject: Fw: copyright etc Date: Sat, 7 Mar 2009 17:05:54 -0000 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Hi Jim,=20 perhaps you should do it for the catlist as the bill is a USA congress = issue.=20 But as the email below says, I am urging its discussion here in the THES = and by CASE (Campaign for Science & Engineering); and Steve Harnard = thinks the response to the proposal has been too shrill!=20 It is a good thing to stir things up!=20 Ronnie ----- Original Message -----=20 From: Stevan Harnad=20 To: Richard Poynder=20 Cc: Ronnie Brown ; Nick Hall=20 Sent: Saturday, March 07, 2009 4:40 PM Subject: Re: copyright etc On 7-Mar-09, at 10:34 AM, Richard Poynder wrote: Hi Ronnie, I am copying in Stevan Harnad as he may know whether anyone at the = THES is looking at this. =20 In the meantime these two links may be of interest: = http://www.huffingtonpost.com/lawrence-lessig-and-michael-eisen/is-john-c= onyers-shilling_b_171189.html = http://www.huffingtonpost.com/john-conyers/a-reply-to-larry-lessig_b_1726= 42.html At least Larry Lessig appears to have stung Conyers into responding. Hi Richard, It would certainly be a good idea if THES did a critical article on the = Conyers Bill's attempt to overturn the NIH self-archiving mandate. But I think the letter you attached is a bit too shrill and not = sufficiently well informed to hit the mark and help: "Any bets that the = next step would be defunding arXiv?" The Conyers Bill is about not = allowing NIH to require self-archiving. It has nothing to do with the = spontaneous self-archiving that has been going on in Arxiv and elsewhere = for nearly two decades. Tim Farley's well-meaning piece in Discover Magazine's Bad Astronomy = Blog is also too over the top to be taken seriously: "Conyers wants science to be secret or you will pay." (Secret? Published = journal articles, secret? Even if you have to pay to read them, what has = that to do with being secret?) "...pushing a bill through Congress that will literally ban the open = access of these papers, forcing scientists to only publish in journals." Ban open access? Forcing scientists to publish journal articles is = journals? This kind of scattershot rhetoric does not help any cause, only its = detractors. I've responded to both Larry Lessig's critique and John Conyer's reply, = by the way. Lawrence Lessig's Critique of the Conyers Bill (H.R. 201) to Overturn = the NIH OA Mandate Rep. John Conyers Explains his Bill H.R. 801 in the Huffington Post Chrs, Stevan Cheers, Richard From: Ronnie Brown [mailto:ronnie.profbrown@btinternet.com]=20 Sent: 07 March 2009 15:25 To: richard.poynder@btinternet.com Cc: Nick Hall Subject: Re: copyright etc Hi Richard, Thanks. I just got the attached. It seems to need public discussion! E.g. in = the THES? Can you initiate that? Are there any lengths to which these top publishers will not go to = preserve their cosy domain, battening on the hard work of academics? Ronnie www.bangor.ac.uk/r.brown ----- Original Message ----- From: Richard Poynder To: 'Ronnie Brown' Sent: Saturday, March 07, 2009 2:15 PM Subject: RE: copyright etc Hi Ronnie, Thanks for these links. Yes, these are the kind of issues that = interest me. And I have done a series of interviews discussing these = sort of topics. http://www.bloomsburyacademic.com/Poynder1.htm They recently started to hit the syllabus of some US library arts = colleges e.g. Oberlin. http://www.steword.net/oberlin/soci220/syllabus.html Click on show details under "Intellectual Property & the Web of = Human Creativity" Cheers, Richard From: Ronnie Brown [mailto:ronnie.profbrown@btinternet.com]=20 Sent: 04 March 2009 20:32 To: Richard Poynder Subject: copyright etc Richard, As a result of listening to Laurie Taylor this afternoon I came = across the following and perhaps they are relevant to your concerns. http://www.ft.com/cms/s/2/b46f5a58-aa2e-11db-83b0-0000779e2340.html http://www.thepublicdomain.org/ http://creativecommons.org/licenses/by-nc-sa/3.0/ Best regards Ronnie From rrosebru@mta.ca Tue Mar 10 18:59:18 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Mar 2009 18:59:18 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lh9xO-0003XQ-Gb for categories-list@mta.ca; Tue, 10 Mar 2009 18:57:50 -0300 Date: Tue, 10 Mar 2009 09:50:52 +0100 From: Andrew Stacey To: Categories Mailing List Subject: categories: Bi-presheaves MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Andrew Stacey Message-Id: Status: O X-Status: X-Keywords: X-UID: 23 Many thanks to all those who replied to my question. The replies were extremely useful. I would like to sum up what I've been told to see if I've understood it correctly. 1. What I described is known as the 'Isbell envelope', and has been known about for quite some time - if my reading of Lawvere's emails is correct then the idea dates back to his thesis, after which Isbell worked on the idea and named it the 'double envelope', consequently Lawvere renamed it the 'Isbell envelope'. However, whilst it is known, it is classed as 'folklore' which I interpret to mean 'everyone knows about it, but no-one has written anything particular on it' so there's no easy reference to which I could direct someone (particularly someone like myself not well-versed in the lore of category theory). 2. It is also a special case of a 'profunctor', which also goes by the names 'distributor', 'commune', and 'bimodule'. Rather, what I'm describing is something that can be built out of particular profunctors and natural transformations - the 'lax factorisation' of Jeff's email. 3. They are also related to Chu spaces - something else completely new to me! A quick check on MathSciNet provides me with a reasonable reading list. It seems, at first glance, easier to find information on Chu spaces than profunctors, and certainly easier to find it on profunctors than 'Isbell envelopes'. What I actually intend doing is fairly simple and I suspect that my audience (if any) will be more from the non-categorical side of mathematics so I'm looking more for "here's where this concept has occurred before" rather than "here's where you can find all the theorems that we need". For the record, these came up when looking at the various different categories of "smooth space" that I've encountered. I'm really a differential topologist (I hope that that admission doesn't get me expelled from the list) but I like applying the techniques of differential topology to things that aren't really smooth manifolds. This leads to the question of what they actually are and, as I'm sure everyone here knows, there have been several candidates proposed. In trying to compare them all, I've been looking for a unified way of describing them to make it easier to see the differences. That's where this notion of two functors and a "composition" came up. There's an extra part, which I didn't say originally, in that there are often conditions that these functors have to satisfy. That is, I'm really looking at a full subcategories of the Isbell envelope where some constraints are satisfied. It probably doesn't class as much of a grand project but it is helping me learn a little category theory so I hope you all approve of it in that regard! So many thanks again to all those who replied, and if anyone has any further words of wisdom to impart then I'm happy to learn more. Andrew Stacey From rrosebru@mta.ca Thu Mar 12 17:26:28 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Mar 2009 17:26:28 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LhrSv-0000fW-Fb for categories-list@mta.ca; Thu, 12 Mar 2009 17:25:17 -0300 Date: Wed, 11 Mar 2009 16:42:28 -0700 From: Toby Bartels To: Paul Taylor , Categories list Subject: categories: Re: free algebras in ASD MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 24 Paul Taylor wrote in part: >Toby Bartels asked me: >>My intuition is that polynomials with overt discrete coefficients >>should have overt discrete initial algebras, >>while those with compact Hausdorff coefficients >>should have compact Hausdorff final coalgebras. >>Have you any thoughts about that question? >In fact, what I have to say about this (in the setting of the >existing established theory for locally compact spaces) is little >more than Toby's "intuition". The existence of these spaces >would follow from the limit--colimit coincidence, which is sketched >in Remark 10.16 of > "Geometric and higher-order logic in ASD" > www.PaulTaylor.EU/ASD/loccpct#geohol Yes, there it is! That's what I get for not reading them in order. (^_^) >The symmetry between > => T /\ = some overt discrete free algebra >and <= F \/ != all compact Hausdorff cofree coalgebra >is very strong in this, but not perfect, because > N is overt discrete Hausdorff not compact > 2^N is compact Hausdorff not discrete overt >I have not managed to isolate convincingly the precise point where >the symmetry breaks down. I was about to say that this comparison is not really fair, since N is the initial algebra of X |-> X + 1, while 2^N is the final coalgebra of X |-> 2 x X, but I guess that the final coalgebra of X |-> X + 1 is also overt but not discrete. Perhaps the asymmetry is simply between initial algebras and final colagebras. One is a colimit and the other is a limit; there are already several asymmetries between these, such as that products distribute over sums but not vice versa. Indeed, if final coalgebras preserve "some"s, this might be more than just a bad pun. --Toby From rrosebru@mta.ca Thu Mar 12 17:26:28 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Mar 2009 17:26:28 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LhrRa-0000YL-Lp for categories-list@mta.ca; Thu, 12 Mar 2009 17:23:54 -0300 Mime-Version: 1.0 (Apple Message framework v753.1) Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: Categories list From: Steve Vickers Subject: categories: PhD studentship available: toposes and quantum theory Date: Wed, 11 Mar 2009 16:43:43 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Steve Vickers Message-Id: Status: O X-Status: X-Keywords: X-UID: 25 Dear categories list, I have received EPSRC funding for a project with a PhD studentship attached. If you know of suitably qualified students who might be interested, I would be very please to hear from them. Study would be in the School of Computer Science at Birmingham University, UK, and the preferred start date is October 2009. The project is "Applications of geometric logic to topos approaches to quantum physics". The "topos approaches" referred to are those of Isham and Doering (at Imperial) and Heunen, Landsman and Spitters (at Nijmegen). By working internally in suitable toposes, they are able to find (commutative) Gelfand-Naimark spectra for systems that, externally, are non- commutative. The hope is that this might lead to a style of reasoning about quantum systems that, while logically non-classical, is physically classical. My project will look at trying to keep the intuitionistic, topos- valid, internal reasoning within its geometric part. Insofar as this is possible (and there is mounting evidence that substantial amounts of practical mathematics can be done this way), it enables a language of points, stalks, fibres and bundles for the point-free topology involved. It is hoped that this will allow the topos approach to be conducted in terms that are more conceptually transparent (in particular to physicists), but also make it technically palatable to move from the present presheaf toposes to sheaf toposes. Initial work will focus on the geometric content of the Banaschewski/Mulvey account of Gelfand-Naimark duality. Further information can be found on my web site, at http://www.cs.bham.ac.uk/~sjv/geophysics.php#phd Regards, Steve Vickers. From rrosebru@mta.ca Thu Mar 12 17:26:28 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Mar 2009 17:26:28 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LhrQn-0000Ub-FK for categories-list@mta.ca; Thu, 12 Mar 2009 17:23:05 -0300 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <5144d216929675f329001b33fb3888af@PaulTaylor.EU> Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: free algebras in ASD Date: Wed, 11 Mar 2009 16:13:44 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Status: O X-Status: X-Keywords: X-UID: 26 During the discussion on Dedekind vs Cauchy reals, Toby Bartels asked me > to what extent does ASD have inductive and coinductive objects; > in other words: to what extent do polynomial functors have > initial algebras and final (terminal) coalgebras? > > Of course, N is put in by hand as the initial algebra of X |-> 1 + X. > > And I know that you've constructed Cantor space as 2^N (through > a bit of argument since exponentials don't always exist) and the > proof that this is the final coalgebra of X |-> 2 x X goes through. > > But the final coalgebra of X |-> N x X would be Baire space, > which is not locally compact, so we don't expect that to work. > > My intuition is that polynomials with overt discrete coefficients > should have overt discrete initial algebras, > while those with compact Hausdorff coefficients > should have compact Hausdorff final coalgebras. > Have you any thoughts about that question? In fact, what I have to say about this (in the setting of the existing established theory for locally compact spaces) is little more than Toby's "intuition". The existence of these spaces would follow from the limit--colimit coincidence, which is sketched in Remark 10.16 of "Geometric and higher-order logic in ASD" www.PaulTaylor.EU/ASD/loccpct#geohol I did have in mind (in 2003, largely as a way of avoiding doing any real analysis) to formulate a language for free algebras and cofree coalgebras based on this idea. I then spent half a year on the construction of the free monoid ("set of lists") and free semilattice ("finite powerset") on an overt discrete object, ie writing the paper "Inside every model of ASD lies an arithmetic universe" www.PaulTaylor.EU/ASD/loccpct#insema At no point did this present any insuperable obstacles, but it did keep presenting obstacles, so I got heartily sick of discrete maths in ASD, and was then amenable to being persuaded to do some analysis. The symmetry between => T /\ = some overt discrete free algebra and <= F \/ != all compact Hausdorff cofree coalgebra is very strong in this, but not perfect, because N is overt discrete Hausdorff not compact 2^N is compact Hausdorff not discrete overt I have not managed to isolate convincingly the precise point where the symmetry breaks down. For example, my paper "Computably based locally compact spaces" www.PaulTaylor.EU/ASD/loccpct#comblc investigates the formula phi x = Some n:N. A_n phi /\ beta^n x that captures the way in which locally compact spaces and locales have bases of compact/open pairs. (Note that the spatial and localic cases are different -- in an interesting topological way, not just regarding Choice.) So I thought, "what if" we write down the dual formula phi x = All k:K. A_k phi \/ beta^k x which we think of as a system of overt/closed pairs indexed by a compact Hausdorff space K. (Having used the phrase "dual base" already, I called this a "canopy".) It turns out that every locally compact space has a canopy. This is proved in the notes "Tychonov's theorem in ASD". www.PaulTaylor.EU/ASD/misclc#tyctas which also contain the construction of Cantor space that Toby mentioned. All of this is, as I said, within the existing established theory of locally compact spaces. Extending the theory beyond this is something that has occupied my mind for some time without coming to any satisfactory conclusions. However, the "equideductive logic" that arises in any CCC with all finite limits is very promising as a framework. I have given three lectures about this, www.PaulTaylor.EU/slides/ and described in in the final section of "Foundations for Computable Topology" www.PaulTaylor.EU/ASD/foufct/ Paul Taylor PS The transfer of my website and email to a new hosting company is now complete. (PrimeXeon is a small outfit in Cambridge that provides intelligent helpful personal service for a mere 20 pounds per annum.) There were brief technical and admin problems over the weekend (I didn't understand MX records) that may have resulted in a failure to deliver mail to me. So if you tried to contact me on Sunday or Monday, please send your message again. From rrosebru@mta.ca Thu Mar 12 17:26:45 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Mar 2009 17:26:45 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LhrTW-0000hq-Cw for categories-list@mta.ca; Thu, 12 Mar 2009 17:25:54 -0300 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <2318ad10f8c56195badcc6edad02cd98@PaulTaylor.EU> Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Re: free algebras in ASD Date: Thu, 12 Mar 2009 09:34:39 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Status: O X-Status: X-Keywords: X-UID: 27 Toby Bartels and I have been discussing the relationship between 1-categorical ideas such as free algebras and cofree coalgebras and 2-level ideas such as overt discrete and compact Hausdorff. It does seem to me to be a good question to ask why these relationships hold, and why they break down. Such questions arise in traditional formulations of topology, in which other people may have some intuition. I observed that N is overt discrete Hausdorff not compact 2^N is compact Hausdorff not discrete overt which Toby attributed to the fact that N is the free algebra for +1 whereas 2^N is the cofree coalgebra for a functor that is not directly analogous. I don't think the particular functors are very important, as (some of) these properties hold of free algebras and cofree coalgebras in general. So, a free algebra is - overt because we can enumerate its (raw) terms, - discrete because we can enumerate (proofs of) its equations, - not compact because there are infinitely many raw terms. I don't have much experience of cofree coalgebras, but those that do could probably formulate a similar argument for why they are compact and Hausdorff. N is peculiar in being Hausdorff (ie it has decidable equality). This is because its theory is very simple. Other free algebras (my usual example is "combinatory algebra", with S and K) do not have decidable equality. Likewise, cofree coalgebras are not discrete. ***** Why is Cantor space overt? ***** Do other cofree coalgebras have this property? That would explain these particular failures of symmetry, but ***** Why does this relationship between the 1- and 2-level ideas ***** hold, and why is it this way round? ASD might make things clearer here. Its 1-level theory, like that of an elementary topos, is not self-dual. Toby observed that the symmetry between free algebras and cofree coalgebras is only partial. The ideas have long been well known in category theory, alhough, if you go through the exactness properties of a pretopos, several of them do actually hold for the dual category too. The 2-level theory in ASD is quite interesting before we introduce the axioms that break the duality. These are: - N is overt but not compact - Scott continuity. As I mentioned before, I tried a bit to develop things with dual ideas, in particular starting from Cantor space instead of N. I suspect that there is a dual formulation of Scott continuity, although I couldn't see what it is. So I don't think that that's where the asymmetry lies. I suspect that the symmetry is broken by the "convention" that - N is overt but not compact ie it has a quantifier, and we ("arbitrarily") call this "existential". Paul Taylor From rrosebru@mta.ca Fri Mar 13 22:31:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Mar 2009 22:31:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiIft-0004VE-4J for categories-list@mta.ca; Fri, 13 Mar 2009 22:28:29 -0300 Date: Thu, 12 Mar 2009 11:34:43 +0000 From: Philippa Gardner MIME-Version: 1.0 To: categories@mta.ca Subject: categories: DBPL 2009: The Symposium for Database Programming Languages Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Philippa Gardner Message-Id: Status: O X-Status: X-Keywords: X-UID: 28 [Apologies if you receive many copies of this email]=20 Floris Geerts (Edinburgh, database person working with Peter Buneman) an= d I=20 are organising DBPL 2009 this year. This symposium provides an interface=20 between database and programming language research. I've been to a couple= of=20 meetings and think they're really good. In particular, over the years I h= ave=20 found it invaluable to talk with people from database theory.=20 Following tradition, the meeting is co-located with VLDB in Lyon.=20 As well as the LNCS proceedings, we will be inviting the best papers to be published in the Journal of Computer and System Sciences. I very much encourage people to submit to this lovely meeting, and=20 hope that we will end up with a good showing of programming language pape= rs. Best wishes, Philippa CALL FOR PAPERS 12th International Symposium on Database Programming Languages DBPL 2009 Co-located with VLDB 2009 Lyon, France. August 23-24, 2009. http://workshops.inf.ed.ac.uk/dbpl09/ ----------------------- The 12th Biennial Symposium on Data Base Programming Languages (DBPL 2009), to be held on August 23-24, 2009, in Lyon, France, continues the tradition of excellence initiated by its predecessors in Roscoff, Finistere (1987), Salishan, Oregon (1989), Nafplion, Argolida (1991), Manhattan, New York (1993), Gubbio, Umbria (1995), Estes Park, Colorado (1997), Kinloch Rannoch, Scotland (1999), Marino, Rome (2001), Potsdam, Germany (2003), Trondheim, Norway (2005) and Vienna, Austria (2007). Over the years DBPL has established itself as the main venue for publishing and discussing new ideas at the intersection of database and programming languages research. Many key contributions in query languages for object-oriented data, persistent databases, nested relational data, semistructured data, as well as fundamental ideas in types for query languages have been first announced and discussed at DBPL. Today's emergence of new data management applications like Web services, XML processing, sensor networks and peer to peer data management has lead to a new flurry of creativity in the area lying at the intersection of data management and programming languages, and DBPL is an established destination for such new ideas. Important dates: ----------------------- Submission of paper: May 3, 2009 (midnight GMT) Notification: June 7, 2009. Camera ready: June 14, 2009. DBPL 2009: August 23/24, 2009. Topics of Interest: ----------------------- DBPL 2009 solicits theoretical and practical papers in all areas of Data Base Programming Languages. Papers emphasizing new topics or foundations of emerging areas are especially welcome. Suggested, but not exclusive, topics of interest for submissions include: -Data exchange -Data integration and interoperability -Databases and information retrieval -Databases and the Semantic Web -Database languages in Bioinformatics -Databases in computational linguistics -Declarative data centers -Managing uncertain and imprecise information -Programming language support for databases -Databases in e-commerce -Multimedia databases -Peer-to-peer data management -Stream data processing -Schema mapping and metadata management -Security in data management -Semi-structured data -Spatial and temporal data -Transaction management -Validation, type-checking -Web services -XML processing Submission guidelines: -------------------------------- Papers should be submitted in PDF via the EasyChair submission website: http://www.easychair.org/conferences/?conf=3Ddbpl2009 Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. The proceedings will be published in the Springer Lecture Notes in Computer Science (lncs) series (www.springer.com/lncs). Submissions should be no more than 15 pages long in the format specified by Springer. Papers longer than 15 pages risk rejection without consideration of their merits. It is recommended that each submission begins with a succinct statement of the problem and a summary of the main results. If the authors believe more details are necessary to substantiate the main claims of the paper, they may include a clearly marked appendix to be read at the discretion of the committee. E-mail addresses of the authors should be included on the title page. At least one author of each accepted paper must attend the symposium to present their work. Invitation for the best papers: --------------------------------------- The authors of the best papers will be invited to submit extended versions of their papers to the Journal of Computer and System Sciences. Program co-chairs: -------------------------- Philippa Gardner (Imperial College, UK) Floris Geerts (University of Edinburgh, UK) Program committee: --------------------------- Pablo Barcelo (Universidad de Chile, Chile) Gavin Bierman (Microsoft Research, Cambridge, UK) Jan Chomicki (University at Buffalo, USA) Anuj Dawar (University of Cambridge, UK) J. Nathan Foster (University of Pennsylvania, USA) Philippa Gardner (Imperial College, UK) Floris Geerts (University of Edinburgh, UK) Cosimo Laneve (Universita di Bologne, Italy) Maarten Marx (University of Amsterdam, The Netherlands) Alan Schmitt (Inria, Grenoble, France) Peter Thiemann (University of Freiburg, Germany) Christopher Re (University of Washington, USA) Jerome Simeon (IBM Almaden, USA) Stijn Vansummeren (University of Hasselt, Belgium) Jef Wijsen (Universit=C3=A9 de Mons-Hainaut, Belgium) Limsoon Wong (National University of Singapore, Singapore) From rrosebru@mta.ca Fri Mar 13 22:31:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Mar 2009 22:31:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiIiN-0004bX-DU for categories-list@mta.ca; Fri, 13 Mar 2009 22:31:03 -0300 Date: Fri, 13 Mar 2009 18:01:52 +0100 From: Dave Clarke To: categories@mta.ca Subject: categories: ECOOP 2009 Call for Student Volunteers Sender: categories@mta.ca Precedence: bulk Reply-To: Dave Clarke Message-Id: Status: O X-Status: X-Keywords: X-UID: 29 ECOOP'2009 23rd European Conference on Object Oriented Programming July 6th - 10th 2009, Genova, Italy http://2009.ecoop.org CALL FOR STUDENT VOLUNTEERS ECOOP is pleased to offer a number of opportunities for student volunteers, who are vital to the efficient operation and continued success of the conference each year. The student volunteer program is a chance for students from around the world to participate in the conference whilst assisting us in preparing and running the event. We strongly encourage students to become involved in the ECOOP student volunteer program. Description and Benefits Job assignments include assisting with technical sessions, workshops, tutorials and panels, checking badges at doors, operating the information desk, helping with traffic flow, and general assistance to keep the ECOOP running smoothly. In return for a few hours of their time, student volunteers are granted: * Free registration to the conference * Free access to ECOOP plenary sessions, tutorials, workshops, and demos (duties, space, and specific requirements permitting) Student volunteers should be in Genova two days before the conference, that is from Saturday, July 4th, and help with preparations and with the conference take-down on July 10th. The selection of student volunteers and plan assignment is NOT done on a first come, first served basis. The most important thing is to have an international group of student volunteers. We try to make a balanced decision. Also, we favor students with strong communication skills: being fluent in English is a must. Important Dates and Information Application deadline: April 10, 2009 Notification of acceptance: May 4, 2009 Applicants must be Master students or full-time Ph.D. students. They should send an e-mail to Marco Servetto (servetto@disi.unige.it) with the subject "ECOOP SV", containing the following information: * First name * Last name * Number of years in a Master or Ph.D. program * Group / Department / University * Complete contact information (surface mail) * If you have a driver's license (not necessary) * Languages spoken (at least) fairly well (fairly well means you could survive well in a country speaking this language only; students with TOEFL/TOEIC/DELF-DALF/TCF/TEF/TFI certificates should include their scores). * A short paragraph motivating your application (including possible past experience as a student volunteer) and clarifying your need for financial support. * Supervisor's(s') name(s) and e-mail address(es). Supervisors may be contacted to confirm applicants' suitability. Accommodation and Travel Expenses We will be doing our best to help students find good and cheap accommodation. Sadly, covering the costs of accommodation and travel expenses is not in our budget. In case some funds should be available, precedence will be given to well-motivated requests. Questions and Comments If you have any further questions about volunteering, please feel free to contact Marco Servetto (servetto@disi.unige.it). From rrosebru@mta.ca Fri Mar 13 22:31:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Mar 2009 22:31:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiIhi-0004Zm-Po for categories-list@mta.ca; Fri, 13 Mar 2009 22:30:22 -0300 Date: Fri, 13 Mar 2009 12:29:28 +0100 From: Andrew Stacey To: Categories Mailing List Subject: categories: Functions in programming MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Andrew Stacey Message-Id: Status: O X-Status: X-Keywords: X-UID: 30 Here's a question for those who know about translating between category theory for mathematicians and category theory for computer programmers. In class today I was discussing functions with domain the empty set. The students don't have much background in formal set theory (and none in category theory though I'm doing my best to sneak it in where I can) so they were trying to get to grips with the idea that the _are_ functions from the empty set, but just not very many of them. Afterwards, one student asked about how this related to functions as used in computer programming. It seemed from what he said that he had some understanding of the formal relationship between functions in mathematics and functions in computer programs - beyond them having the same name. He said that a function that takes no input is known as a "constant function" and so wasn't sure how to fit the two notions together. I, on the other hand, am at the level of "Ooo, look! Mathematicians and computer programmers both use the word 'function'. So do biologists and event organisers. Maybe we should organise a function whose function would be to investigate all these different uses.' so I didn't know what answer to give. The best that I could think of was that program functions have a 'hidden' input: the fact that they have been called. So a function defined on the empty set corresponds to a function that can never be called. Can anyone help me straighten this out? Extra kudos for answers that I can just pass on to the student! Thanks, Andrew Stacey From rrosebru@mta.ca Fri Mar 13 22:31:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Mar 2009 22:31:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiIgz-0004Xz-Mw for categories-list@mta.ca; Fri, 13 Mar 2009 22:29:37 -0300 Date: Thu, 12 Mar 2009 22:02:59 -0700 From: Vaughan Pratt MIME-Version: 1.0 To: Categories list Subject: categories: Re: free algebras in ASD Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 31 Paul Taylor wrote: > I observed that > N is overt discrete Hausdorff not compact > 2^N is compact Hausdorff not discrete overt > which Toby attributed to the fact that N is the free algebra for +1 > whereas 2^N is the cofree coalgebra for a functor that is not directly > analogous. As Toby noted, the functor is x2. However it is more than merely analogous, it is the dual of +1 when 2 is taken to be the dual of 1 (as with the original Stone duality for Boolean algebras, more generally distributive lattices, more generally yet Chu(Set,2)), product of course being the dual of sum. > ASD might make things clearer here. Its 1-level theory, like that > of an elementary topos, is not self-dual. By "1-level" do you mean first order? *-autonomous categories constitute a natural elementary notion of abstract Stone duality that is self-dual. What advantage of the elementary fragment of ASD over *-autonomous categories justifies its failure of duality? And how does the *-autonomous abstraction of Stone duality relate to ASD's abstraction of it? Toby Bartels wrote: > Perhaps the asymmetry is simply between initial algebras and final colagebras. > One is a colimit and the other is a limit; > there are already several asymmetries between these, > such as that products distribute over sums but not vice versa. > Indeed, if final coalgebras preserve "some"s, > this might be more than just a bad pun. In general 2 is not the dual of 1. In order to exhibit a duality between N and 2^N, they should be defined in a self-dual category that does make 2 the dual of 1. The most general such that I'm aware of is Chu(Set,2) --- Chu(Set,3) embeds Chu(Set,2) (in 3x2 = 6 ways) but it makes 3 the dual of 1. If you know of another category that makes 2 the dual of 1 that does not embed in Chu(Set,2) I'm all ears. In situations where 2 is not the dual of 1 it's not clear to me why one should expect 2^N to turn out to be dual to N in a way where all properties of one have their dual counterpart of the other; in Chu(Set,K) the natural functor for a final coalgebra dual to N is FX = XxK. In the context of duality the way to think about X in a Chu space (A,X,r) is that it is the dual of A, with the relation r characterizing the particular duality: the dual of (A,X,r) is (X,A,r^) where r^ is the converse of r. The first component constitutes the underlying set while the second can be thought of as a generalized frame of open sets, generalized by dispensing with the traditional frame operations of finite meets and arbitrary sups, with r simply the binary relation of membership of points in open sets. For this reason, absent alternatives to Chu(Set,2) there is no alternative to taking 1 to be the Chu space (1,2) if you want 2 to turn out to be the dual of 1. Note that in doing so 2 becomes the Chu space (2,1), the coarsest possible consistent topology on 2 (thinking of (2,0) as inconsistent). It should be distinguished from discrete 2 = 1+1, which is (2,4). Taking 1 in Chu(Set,2) to be the discrete Chu space (1,2), the initial algebra for +1 is (1,2) + (1,2) + ... = (N,2^N), 2^N being the power set of N, a complete atomic Boolean algebra. The final coalgebra for x2 when 2 = (2,1), as the dual of the initial algebra for +1, is the dual of (N,2^N), namely (2^N,N). Back to Paul: > The symmetry between > => T /\ = some overt discrete free algebra > and <= F \/ != all compact Hausdorff cofree coalgebra > is very strong in this, but not perfect, because > N is overt discrete Hausdorff not compact > 2^N is compact Hausdorff not discrete overt > I have not managed to isolate convincingly the precise point where > the symmetry breaks down. If ASD makes 2 the dual of 1 then it's suspiciously non-abstract. The only framework I know of for analyzing this duality is Chu(Set,K) for K = 2. Any larger K doesn't work, the concreteness of Chu(Set,3) etc. notwithstanding, unless you set things up so that the final coalgebra of the functor XxK is independent of the cardinality of K (which can be done as Bill Lawvere noted long ago, making 3^N equivalent to 2^N, but I'd be very impressed if ASD incorporated Bill's machinery). In Chu(Set,2), if one takes X in (A,X,r) to be the open sets, with r(a,x) membership of a in x, then (N,2^N,r) is discrete (the discrete Chu spaces over 2 being those of the form (A,2^A,r)), Hausdorff (by discreteness), not compact (because infinite and discrete), and overt (because spatial, Elephant C3.1.16). There are two ways of computing which of these four properties (2^N,N,r^) has, depending on whether one applies the elementary definitions of the properties to the "chupology" (taking r^ to be the converse of membership, i.e. a subset of N can "belong" to an element of N), or organizes 2^N as a topological Boolean algebra with the (Stone) topology serving to make it a CABA so that the continuous ultrafilters are all and only the elements of N, in order for the duality to work. Here are the two ways, alongside what Paul claims for comparison. Chupology not compact not Hausdorff not discrete ?~?overt? Stone compact Hausdorff not discrete overt Paul compact Hausdorff not discrete overt (The chupology is not compact because the whole space is not open, in fact {} is not "in" any natural number. It is not Hausdorff because no two opens are disjoint to begin with. And it's obviously not discrete. However unless there's a definition of "overt" meaningful for all chupologies I don't know what "overt" would mean for chupologies whose open sets don't form frames---they do in (N,2^N) but not in (2^N,N).) Interestingly we have perfect agreement between the usual Stone topology one imposes on a Boolean algebra to make it a CABA (to make the duality work) and the topology Paul has in mind for 2^N. Paul, is this because you have in mind the Stone topology, with 2^N obviously being spatial hence overt, or for some other reason? If the former then that is the "precise point where the symmetry breaks down:" you don't take the precise dual of this when dualizing back to (N,2^N), which you leave instead as the original Chu space (N,2^N). This is a perfectly fine discrete, Hausdorff, overt, but not compact space, again in perfect agreement with you. However comparing it with the topology of a topological Boolean algebra is apples to oranges. If the latter however then I have no explanation and the ball is back in your court. Vaughan Pratt From rrosebru@mta.ca Sat Mar 14 11:15:53 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Mar 2009 11:15:53 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiUbV-0000rq-7o for categories-list@mta.ca; Sat, 14 Mar 2009 11:12:45 -0300 MIME-Version: 1.0 Date: Fri, 13 Mar 2009 21:21:43 -0500 Subject: categories: Re: Functions in programming From: Charles Wells To: Andrew Stacey , catbb Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Charles Wells Message-Id: Status: O X-Status: X-Keywords: X-UID: 32 In terms of common mathematical usage, the student was wrong to say that a constant function is a function with no input. A constant function can be defined on any domain; its defining characteristic is that it has the same value for every input. In categorical terms, a constant function is a function that factors through the terminal object. The empty function to an object should be defined as the unique function from the initial object to that object, but I am not claiming that is common usage. Some computer languages do indeed have functions with no inputs. Their output can still vary since the definition may contain global variables. No doubt objects (in the sense of OOP) with global variables can be modeled as objects in a slice category but now I am out of my depth, so I will stop. Charles Wells On Fri, Mar 13, 2009 at 6:29 AM, Andrew Stacey wrote: > Here's a question for those who know about translating between category t= heory > for mathematicians and category theory for computer programmers. > > In class today I was discussing functions with domain the empty set. =A0T= he > students don't have much background in formal set theory (and none in cat= egory > theory though I'm doing my best to sneak it in where I can) so they were > trying to get to grips with the idea that the _are_ functions from the em= pty > set, but just not very many of them. > > Afterwards, one student asked about how this related to functions as used= in > computer programming. =A0It seemed from what he said that he had some > understanding of the formal relationship between functions in mathematics= and > functions in computer programs - beyond them having the same name. =A0He = said > that a function that takes no input is known as a "constant function" and= so > wasn't sure how to fit the two notions together. > > I, on the other hand, am at the level of "Ooo, look! =A0Mathematicians an= d > computer programmers both use the word 'function'. =A0So do biologists an= d event > organisers. =A0Maybe we should organise a function whose function would b= e to > investigate all these different uses.' so I didn't know what answer to gi= ve. > > The best that I could think of was that program functions have a 'hidden' > input: the fact that they have been called. =A0So a function defined on t= he > empty set corresponds to a function that can never be called. > > Can anyone help me straighten this out? > > Extra kudos for answers that I can just pass on to the student! > > Thanks, > > Andrew Stacey > > > --=20 professional website: http://www.cwru.edu/artsci/math/wells/home.html blog: http://sixwingedseraph.wordpress.com/ abstract math website: http://www.abstractmath.org/MM//MMIntro.htm astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.h= tm personal website: http://www.abstractmath.org/Personal/index.html From rrosebru@mta.ca Sat Mar 14 11:15:53 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Mar 2009 11:15:53 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiUci-0000uG-OC for categories-list@mta.ca; Sat, 14 Mar 2009 11:14:00 -0300 MIME-Version: 1.0 Date: Fri, 13 Mar 2009 22:22:34 -0500 Subject: categories: Re: Functions in programming From: Michael Shulman To: Andrew Stacey , Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Shulman Message-Id: Status: O X-Status: X-Keywords: X-UID: 33 Hi Andrew, (Caveat: I'm not an expert in this field, although I find it fascinating, so I hope that the experts who are listening will forgive and correct any misstatements.) I think your answer ("a function defined on the empty set corresponds to a function that can never be called") is almost right. A programming function having n arguments x_1,...,x_n can be represented by a set-theoretic function whose domain is an n-ary cartesian product: A_1 \times ... \times A_n --> B where A_i is the set of values in the type of the variable x_i, and B is the output type of the function. Thus, for instance, a function of two variables with type Int whose output is type Real would be represented by Z \times Z --> R where Z is the set of integers and R the set of real numbers (or maybe the set of floating-point values, depending on what "Real" means to your compiler). Of course, the set-theoretic function is "extensional," meaning it only knows what output results from each list of inputs rather than how that output is computed; thus many different pieces of code will denote the same function. The fancy word for this is "denotational semantics." Now setting n=3D0, we see that a programming function of no arguments is represented by a morphism 1 --> B where 1, a one-element set, is a zero-ary cartesian product. In other words, it is just a constant (global) element of B. The way to represent a function with empty domain in programming is as a function whose input is of a -type- that admits no values. Thus, this function "can never be called" because there is no argument that you can give it. Normal programming languages do not generally come with predefined types that admit no values, since such types are evidently not very useful! You can define a good approximation to such a type in an OO language by writing a class whose only constructor throws a fatal error; thus there will be no possible "values" having that type. Of course, there will then be many different "functions" in the programming sense that you could write whose domain is such a type, but they will all have the same denotation, namely the unique function from the empty set to the set of values of their output type. By the way, this all assumes that your programming functions are "strict" in the "call-by-value" sense that all their arguments must be completely computed before the function is allowed to execute. However, if you allow "lazy" functions which can ignore some of their input, which exist in some programming languages, then there can be plenty of different functions defined on an "empty" type. For instance, in a lazily evaluated language the function with one input of an empty type and defined by "return 3" can still be evaluated and will promptly return 3. Since it never -uses- its input, the lazy language won't even bother trying to figure out what that input is, and hence won't encounter the fatal error that the input doesn't exist. In denotational semantics, this is modeled by working, not in a category of sets, but in a category of a special sort of -posets-. Among other properties, these posets always have bottom elements, which represent the "undefined" value, but the functions between them are not required to preserve the bottom elements. Such a category generally has no initial object; the "empty" type corresponds to the one-element poset, but there are in general many functions out of this object. Best, Mike On Fri, Mar 13, 2009 at 6:29 AM, Andrew Stacey wrote: > Here's a question for those who know about translating between category t= heory > for mathematicians and category theory for computer programmers. > > In class today I was discussing functions with domain the empty set. =A0T= he > students don't have much background in formal set theory (and none in cat= egory > theory though I'm doing my best to sneak it in where I can) so they were > trying to get to grips with the idea that the _are_ functions from the em= pty > set, but just not very many of them. > > Afterwards, one student asked about how this related to functions as used= in > computer programming. =A0It seemed from what he said that he had some > understanding of the formal relationship between functions in mathematics= and > functions in computer programs - beyond them having the same name. =A0He = said > that a function that takes no input is known as a "constant function" and= so > wasn't sure how to fit the two notions together. > > I, on the other hand, am at the level of "Ooo, look! =A0Mathematicians an= d > computer programmers both use the word 'function'. =A0So do biologists an= d event > organisers. =A0Maybe we should organise a function whose function would b= e to > investigate all these different uses.' so I didn't know what answer to gi= ve. > > The best that I could think of was that program functions have a 'hidden' > input: the fact that they have been called. =A0So a function defined on t= he > empty set corresponds to a function that can never be called. > > Can anyone help me straighten this out? > > Extra kudos for answers that I can just pass on to the student! > > Thanks, > > Andrew Stacey > > > From rrosebru@mta.ca Sat Mar 14 11:17:15 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Mar 2009 11:17:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiUe6-0000y4-1t for categories-list@mta.ca; Sat, 14 Mar 2009 11:15:26 -0300 Date: Fri, 13 Mar 2009 23:38:54 -0400 From: "Fred E.J. Linton" To: Andrew Stacey , Subject: categories: Re: Functions in programming Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: "Fred E.J. Linton" Message-Id: Status: O X-Status: X-Keywords: X-UID: 34 Andrew asked (I snip heavily): > Here's a question for those who know about translating between category= theory > for mathematicians and category theory for computer programmers. > = > In class today I was discussing functions with domain the empty set. ..= =2E > ... [One student reported] > that a function that takes no input is known as a "constant function" a= nd so > wasn't sure how to fit the two notions together. I think "constant function" should be reserved for functions that *do* take input, but care not a whit what that input is, always providing the same output regardless what the input. A function with empty domain, on the other hand, never even has a chance of getting called (as you so correctly observe below), = hence has *no* output whatsoever (and is certainly not a = constant function). > The best that I could think of was that program functions have a 'hidde= n' > input: the fact that they have been called. So a function defined on t= he > empty set corresponds to a function that can never be called. Think your student would be able to digest that? If suitably premasticated, perhaps? Cheers, -- Fred = From rrosebru@mta.ca Sat Mar 14 11:18:20 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Mar 2009 11:18:20 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiUf8-00011L-N3 for categories-list@mta.ca; Sat, 14 Mar 2009 11:16:30 -0300 Date: Fri, 13 Mar 2009 23:02:52 -0700 From: Vaughan Pratt MIME-Version: 1.0 To: Categories Mailing List Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 35 > I, on the other hand, am at the level of "Ooo, look! Mathematicians and > computer programmers both use the word 'function'. So do biologists and event > organisers. Maybe we should organise a function whose function would be to > investigate all these different uses.' Even a perfunctory analysis should indicate that the attendees would be likely to come away disfunctional. :) > The best that I could think of was that program functions have a 'hidden' > input: the fact that they have been called. So a function defined on the > empty set corresponds to a function that can never be called. > > Can anyone help me straighten this out? That's easy: just have them visualize a function as a list of its values at the points in its domain enumerated in some fixed order. Programmers can easily see how many lists of length n there are for any given size of codomain of the function (e.g. lists of bits as functions to {0,1}). The empty list should hold no terrors for programmers: in particular they should know it exists, and they should know why there aren't two empty lists. Vaughan Pratt From rrosebru@mta.ca Sat Mar 14 11:20:01 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 14 Mar 2009 11:20:01 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiUgj-00017r-5r for categories-list@mta.ca; Sat, 14 Mar 2009 11:18:09 -0300 Mime-Version: 1.0 (Apple Message framework v753.1) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit From: Luis Barbosa Subject: categories: Re: Functions in programming Date: Sat, 14 Mar 2009 09:51:22 +0000 To: Andrew Stacey , Sender: categories@mta.ca Precedence: bulk Reply-To: Luis Barbosa Message-Id: Status: O X-Status: X-Keywords: X-UID: 36 On 2009/03/13, at 11:29, Andrew Stacey wrote: > > Afterwards, one student asked about how this related to functions > as used in > computer programming. It seemed from what he said that he had some > understanding of the formal relationship between functions in > mathematics and > functions in computer programs - beyond them having the same name. > He said > that a function that takes no input is known as a "constant > function" and so > wasn't sure how to fit the two notions together. A constant function in Haskell, as in Maths, has 1 as a domain. The (isomorphism class of the) singleton set is written as (); so, for example, the function always returning integer 5 is declared as five :: () -> Int and defined by five () = 5 (notice notation () is used to denote both set 1 and its (unique) element) Your student is probably confusing notation () with the empty set. The notation may be a bit unfortunate as () may suggest "no input" ... but, of course functions, in functional programming are just functions. Luis --------------------------------------- Luis S. Barbosa www.di.uminho.pt/~lsb From rrosebru@mta.ca Sun Mar 15 10:34:42 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 10:34:42 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiqQW-0006eP-I3 for categories-list@mta.ca; Sun, 15 Mar 2009 10:30:52 -0300 MIME-version: 1.0 Content-transfer-encoding: 7BIT Content-type: text/plain; charset=us-ascii; format=flowed; delsp=yes From: Steve Stevenson To: Andrew Stacey , Subject: categories: Re: Functions in programming Date: Sat, 14 Mar 2009 10:58:57 -0400 Sender: categories@mta.ca Precedence: bulk Reply-To: Steve Stevenson Message-Id: Status: O X-Status: X-Keywords: X-UID: 37 All us Fortran II survivors know this issue well ... This is the "function" versus "routine" argument: (1) a routine can have no arguments but (2) can't return a value. This where CALL comes from. Sent from my iPhone Steve Stevenson On Mar 13, 2009, at 7:29, Andrew Stacey wrote: > (a lot snipped) > In class today I was discussing functions with domain the empty > set. The > students don't have much background in formal set theory (and none > in category > theory though I'm doing my best to sneak it in where I can) so they > were > trying to get to grips with the idea that the _are_ functions from > the empty > set, but just not very many of them. > > From rrosebru@mta.ca Sun Mar 15 10:34:43 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 10:34:43 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiqRJ-0006gp-6w for categories-list@mta.ca; Sun, 15 Mar 2009 10:31:41 -0300 From: Thorsten Altenkirch To: Andrew Stacey , Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: Re: Functions in programming Date: Sat, 14 Mar 2009 17:39:47 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Thorsten Altenkirch Message-Id: Status: O X-Status: X-Keywords: X-UID: 38 There really shouldn't be a difference between the functions in Mathematics and in Computer Science, especially functional programming. However, there may be some historic differences. Many Mathematicians still use classical set theory, where the set of functions is a derived concept (i.e. a relation which has certain properties) while in constructive theories (such as Type Theory) as in functional programming, functions are a primitive concepts and they are always computable (I like to say that a function which isn't computable doesn't really function :-). Another potential confusion is that functional programming languages allow the definition of partial functions which may not be terminating. However, I think this is an unnecessary complication because non-termination is just a bug and we are really only interested in the total functions anyway. A constant function in functional programming as in set theory is a function which always returns the same value. And clearly there is only one function from the empty set into any set, because any two functions are equal if they agree on all inputs and hence this statement is vaccously true here. The problem in understanding this is the usual trouble in understanding "ex falso quod libet". Cheers, Thorsten On 13 Mar 2009, at 11:29, Andrew Stacey wrote: > Here's a question for those who know about translating between > category theory > for mathematicians and category theory for computer programmers. > > In class today I was discussing functions with domain the empty > set. The > students don't have much background in formal set theory (and none > in category > theory though I'm doing my best to sneak it in where I can) so they > were > trying to get to grips with the idea that the _are_ functions from > the empty > set, but just not very many of them. > > Afterwards, one student asked about how this related to functions as > used in > computer programming. It seemed from what he said that he had some > understanding of the formal relationship between functions in > mathematics and > functions in computer programs - beyond them having the same name. > He said > that a function that takes no input is known as a "constant > function" and so > wasn't sure how to fit the two notions together. > > I, on the other hand, am at the level of "Ooo, look! Mathematicians > and > computer programmers both use the word 'function'. So do biologists > and event > organisers. Maybe we should organise a function whose function > would be to > investigate all these different uses.' so I didn't know what answer > to give. > > The best that I could think of was that program functions have a > 'hidden' > input: the fact that they have been called. So a function defined > on the > empty set corresponds to a function that can never be called. > > Can anyone help me straighten this out? > > Extra kudos for answers that I can just pass on to the student! > > Thanks, > > Andrew Stacey > > This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. From rrosebru@mta.ca Sun Mar 15 10:34:43 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 10:34:43 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiqSB-0006jt-Sk for categories-list@mta.ca; Sun, 15 Mar 2009 10:32:35 -0300 Date: Sat, 14 Mar 2009 15:52:31 -0400 To: categories@mta.ca From: "Ellis D. Cooper" Subject: categories: Re: Functions in programming Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Ellis D. Cooper" Message-Id: Status: O X-Status: X-Keywords: X-UID: 39 To Andrew Stacey - My take on your question is that in programming, functions correspond in mathematics to partially defined functions. A properly coded programming function must either return the result of a computation for given inputs, or return a signal that the programming function is not defined on the inputs provided. The empty mathematical function would correspond to the programming function that returns that "undefined" signal for all inputs whatsoever. Ellis D. Cooper From rrosebru@mta.ca Sun Mar 15 10:34:43 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 10:34:43 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiqPZ-0006bC-86 for categories-list@mta.ca; Sun, 15 Mar 2009 10:29:53 -0300 Message-Id: <67072EDB-6E6F-4033-8AE3-6BD04614BF60@yandex.ru> From: Miguel Mitrofanov To: Michael Shulman , Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: Re: Functions in programming Date: Sat, 14 Mar 2009 17:51:54 +0300 Sender: categories@mta.ca Precedence: bulk Reply-To: Miguel Mitrofanov Status: O X-Status: X-Keywords: X-UID: 40 On 14 Mar 2009, at 06:22, Michael Shulman wrote: > Normal programming languages do not generally come > with predefined types that admit no values, since such types are > evidently not very useful! That's not exactly true. There is a huge area of type-level programming (or metaprogramming, as it's called sometimes), and empty types are useful as some sort of "flags" in this type of programming. Of course, you can allow some values of this types, but this is what makes no sense in this case. From rrosebru@mta.ca Sun Mar 15 19:33:52 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 19:33:52 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiyrZ-0001V6-Mj for categories-list@mta.ca; Sun, 15 Mar 2009 19:31:21 -0300 Date: Sun, 15 Mar 2009 07:35:37 -0800 From: PETER EASTHOPE Subject: categories: Horizontal line notation. To: categories@mta.ca MIME-version: 1.0 Content-type: text/plain; charset=us-ascii Content-language: en Content-transfer-encoding: 7bit Content-disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: PETER EASTHOPE Message-Id: Status: O X-Status: X-Keywords: X-UID: 41 Lawvere & Schanuel use a horizontal line notation. Page 326 for example. X --> 1^T --------- TxX --> 1 This is unfamiliar. Does the line have a name? How is it read? I'll guess either "(X --> 1^T) is equivalent to (TxX --> 1)" or "(X --> 1^T) is isomorphic to (TxX --> 1)". Thanks, ... Peter E. -- http://members.shaw.ca/peasthope/ http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/ From rrosebru@mta.ca Sun Mar 15 19:33:52 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Mar 2009 19:33:52 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LiysS-0001YF-TI for categories-list@mta.ca; Sun, 15 Mar 2009 19:32:16 -0300 Date: Sun, 15 Mar 2009 16:18:41 -0600 From: Robin Cockett MIME-Version: 1.0 To: Categories Mailing List Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Robin Cockett Message-Id: Status: O X-Status: X-Keywords: X-UID: 42 The simple questions ARE the good ones ... and one should certainly not stop the confusing there! If you want to define the initial object in a functional language you should write (say in Haskell): data Initial = deriving (Show) -- so we can display the elements After all clearly the initial object is the (inductive) datatype with zero constructors. Clearly you then should be able to write perfectly good programs such as the identity function and the case on this datatype. idinit:: Initial -> Initial idinit x = x init:: Initial -> a init x = case x of -- well there are no cases! There is one problem, of course: Haskell does not think this is legal as it thinks all datatypes should have at least one constructor. (BTW do any functional languages allow NO constructors? They really should.) No matter we can try to be a little cleverer and cheat the system by having a constructor which we cannot construct anyway ... data Initial = ZZ initial deriving (Show) -- so we can display the elements This has no elements ... just try to inductively construct them. So this works fine as the initial datatype ... or does it? At this stage we belatedly remember we are not quite in the world we expect as initial and final datatypes coincide so we do actually have a perfectly good element in this datatype. forever:: Initial forever = ZZ forever You do have to be patient as it does takes a bit of time to display it ... :-) OK so that did not work!! But now we have remembered that initial and final datatypes are supposed to coincide we have a blinding flash of inspiration: because ()=1 is the final type it must also be the initial object. So constant functions ARE the same as initial functions after all ....... so the student was not confused at all! Or was he? -robin Robin Cockett, Calgary From rrosebru@mta.ca Mon Mar 16 20:45:03 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:45:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMTM-0001P2-KE for categories-list@mta.ca; Mon, 16 Mar 2009 20:43:56 -0300 From: Daniel =?iso-8859-1?q?Sch=FCssler?= To: categories@mta.ca Subject: categories: Re: Functions in programming Date: Mon, 16 Mar 2009 05:25:23 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Daniel =?iso-8859-1?q?Sch=FCssler?= Message-Id: Status: O X-Status: X-Keywords: X-UID: 43 Hello, On Sunday 15 March 2009 23:18:41 Robin Cockett wrote: > There is one problem, of course: Haskell does not think this is legal as > it thinks all datatypes should have at least one constructor. With GHC you can have empty types if you include the {-# OPTIONS -XEmptyDataDecls #-} pragma :) Greetings, Daniel From rrosebru@mta.ca Mon Mar 16 20:45:03 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:45:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMSg-0001L6-87 for categories-list@mta.ca; Mon, 16 Mar 2009 20:43:14 -0300 From: Thorsten Altenkirch To: Robin Cockett . Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: Re: Functions in programming Date: Sun, 15 Mar 2009 23:55:32 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Thorsten Altenkirch Message-Id: Status: O X-Status: X-Keywords: X-UID: 44 > There is one problem, of course: Haskell does not think this is > legal as > it thinks all datatypes should have at least one constructor. (BTW do > any functional languages allow NO constructors? They really should.) Yes, Agda does. > But now we have remembered that initial and final datatypes are > supposed > to coincide we have a blinding flash of inspiration: because ()=1 is > the final type it must also be the initial object. So constant > functions ARE the same as initial functions after all ....... so the > student was not confused at all! > > Or was he? I think it is a common misunderstanding that because you can write non- terminating function that you should. Non-termination is a bug and it is not what functional programming is about. Btw, Agda is total, but you are allowed to ignore the termination checker. Thorsten > > > -robin > > > Robin Cockett, Calgary > > > This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. From rrosebru@mta.ca Mon Mar 16 20:45:03 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:45:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMRV-0001Fv-DF for categories-list@mta.ca; Mon, 16 Mar 2009 20:42:01 -0300 Date: Sun, 15 Mar 2009 22:52:28 -0700 From: Vaughan Pratt MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 45 The categories mailing list is a good one for this sort of discussion: it's hard to make sense of these issues without the abstract framework of categories to interpret statements about the difference if any between a function with no arguments and a function on the empty domain, as the following examples make clear. Steve Stevenson wrote: > All us Fortran II survivors know this issue well ... This is the > "function" versus "routine" argument: (1) a routine can have no > arguments but (2) can't return a value. This where CALL comes from. In both Set and (bottomless) CPO a function (or routine) on the empty domain is typed as 0 --> X, one with no arguments as 1 --> X (1 being the empty product). Andrew, in discussing 0 --> X with your students in the context of ordinary sets and functions (the category Set) you might also want to clarify how it differs from 1 --> X. (Need 1 be identified with Y^0 for any particular Y? I would guess that a specific Y^0 should be different from the empty dependent product but is that the case? Any dependent product experts?) Robin Cockett wrote: > But now we have remembered that initial and final datatypes are supposed > to coincide we have a blinding flash of inspiration: because ()=1 is > the final type it must also be the initial object. So constant > functions ARE the same as initial functions after all ....... so the > student was not confused at all! > > Or was he? Haskell datatypes naively are pointed CPOs (CPPO), in which case one might expect the initial and final CPOs with bottom to coincide as the zero object (0 = 1). In that case the distinction between 0 --> X and 1 --> X would then vanish, in accordance with your story. Without (ultimately) contradicting this, Makoto Hamana's slides at http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf paint a more nuanced picture comparing (bottomless) CPO, CPPO (which *lacks* an initial object), and strict CPPO (all functions preserve bottom, unlike CPPO). Hamana argues for the order-enriched version of the last as the appropriate semantics for Haskell, where 0 = 1 remains the case, in agreement with the intuitions and prior semantics of Haskell. Other languages may vary. Thorsten Altenkirch wrote: > There really shouldn't be a difference between the functions in > Mathematics and in Computer Science, especially functional programming. 1. There should be differences within Mathematics and within Computer Science, and therefore between them. Only in the narrow technical definition of "function" as a morphism of Set should everyone be in agreement as to what a function is. But perhaps what you meant is that mathematics and CS should recognize the same latitude in the conception of function, which is reasonable given the difficulty of defining the boundary between mathematics and CS. 2. One should not assume that mathematics has the answer to every practical problem. Scientists and engineers indeed benefit enormously from the tools of mathematics, in rough proportion to how many of them they have at their fingertips, but when mathematics comes up short the fault does not necessarily lie with the practitioners, who may from time to time be in need of genuinely new mathematical methods. > However, there may be some historic differences. Many Mathematicians > still use classical set theory, where the set of functions is a > derived concept (i.e. a relation which has certain properties) while > in constructive theories (such as Type Theory) as in functional > programming, functions are a primitive concepts and they are always > computable (I like to say that a function which isn't computable > doesn't really function :-). You constructivists can be so judgmental at times. :) > Another potential confusion is that functional programming languages > allow the definition of partial functions which may not be > terminating. However, I think this is an unnecessary complication > because non-termination is just a bug and we are really only > interested in the total functions anyway. Jimmy Treybig made a fortune from his company Tandem's line of NonStop servers, see http://en.wikipedia.org/wiki/NonStop . Computer scientists are confronted with Hobson's Choice of a programming language that includes some partial recursive functions that diverge on some inputs, and one that excludes some (total) recursive functions. No effectively compilable language can capture all and only the recursive functions. If you accept the former in order to avoid the latter, it is unkind to call all the partial ones buggy, especially when the language provides some means of getting useful work out of them. If those programs can't be analyzed as functions then how is functional programming relevant to systems programming? If they can, in what sense do they terminate? > A constant function in functional programming as in set theory is a > function which always returns the same value. And clearly there is > only one function from the empty set into any set, because any two > functions are equal if they agree on all inputs and hence this > statement is vaccously true here. The problem in understanding this is > the usual trouble in understanding "ex falso quod libet". I took Andrew's question to be more about existence of f: 0 --> X than its uniqueness. We could argue against its existence by noting that the empty function diverges on every input and also converges on every input. Hence it is clearly inconsistent and therefore cannot exist. It might seem like a bad joke, but some algebraists actually reason that way to argue that the empty algebra does not exist. We saw at UACT at MSRI in 1993 that the authors of "Algebras, Lattices, Varieties: Volume I" (Volume II still pending) forbid empty algebras because they were unable to come up with a consistent way of quantifying over the empty set. For signatures with no constants, this creates the difficulty that the subalgebras need not be closed under intersection because of the possibility of disjoint nonempty subalgebras. In order to make the set Sub A of subalgebras of an algebra A a lattice under inclusion, the authors of ALV created the notion of a subuniverse as a subalgebra that is allowed to be empty, and define Sub A to be the set of *subuniverses* of A. They spell out this arrangement with admirable clarity in Definition 1.3, and at least one of them insists to this day that maintaining separate notions of subalgebra and subuniverse in order to work around the paradoxes of the empty universe is just fine, with no explanation as to why the inconsistencies supposedly created by empty algebras do not arise for empty subuniverses. One side effect of this algebraic apartheid is that the initial lattice doesn't exist; more generally varieties without constants don't have initial algebras, only free algebras on nonempty sets. Vaughan Pratt From rrosebru@mta.ca Mon Mar 16 20:45:50 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:45:50 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMUZ-0001UK-99 for categories-list@mta.ca; Mon, 16 Mar 2009 20:45:11 -0300 From: Tom Hirschowitz To: Categories Mailing List Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Subject: categories: Re: Functions in programming Date: Mon, 16 Mar 2009 10:27:15 +0100 Sender: categories@mta.ca Precedence: bulk Reply-To: Tom Hirschowitz Message-Id: Status: O X-Status: X-Keywords: X-UID: 46 Dear all, Before asking what the morphisms 0 -> A are, one should probably fix a category. This involves choosing a programming language and a notion of equivalence for programs, and both choices impact on the existence of an initial object. 1) A first possibility consists of choosing a programming language and considering the category where: - objects are types (possibly a single one for untyped languages such as Scheme), - morphisms A -> B are programs of type B with one variable of type A (or variants such as the one proposed by Mike Schulman), considered equivalent up to observational equivalence. Observational equivalence might mean a lot of different things. Let us here put M ~ N : A -> B when for all P : B -> Bool and Q : 1 -> A, PMQ evaluates to true iff PNQ evaluates to true. (If your programming language allows infinite loops, you may replace Bool with 1 and observe termination.) Then, if your programming language has an empty type A, i.e., one without any program 1 -> A, it is initial because M ~ N vacuously holds. An example such programming language is Agda (using an inductive type with no constructor). 2) However, in Haskell, you may define an inhabitant of all types by typing the recursive definition bot = bot . You may also define functions: f x = True and g x = False having all types A -> Bool, which are not equivalent because f bot evaluates to True while g bot evaluates to False. 3) But there are other possible notions of equivalence! For example, one may consider only beta, eta, ... equivalence. Then, even with an empty type A, the functions f x = True and g x = False are different, hence A is not initial. 4) As a final remark, even in a consistent setting like Agda, functions from the empty type are frequently applied (in an open context), typically the canonical function (A * not A) -> B, which looks like f (x, y) = !(y(x)), where !M = match M with {} -- case analysis on zero constructors. Pierre Hyvernat and Tom Hirschowitz -- From rrosebru@mta.ca Mon Mar 16 20:47:00 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:47:00 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMVh-0001d4-RC for categories-list@mta.ca; Mon, 16 Mar 2009 20:46:21 -0300 Date: Mon, 16 Mar 2009 11:37:41 +0000 From: Miles Gould To: Robin Cockett , Subject: categories: Re: Functions in programming Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Miles Gould Message-Id: Status: O X-Status: X-Keywords: X-UID: 47 On Sun, Mar 15, 2009 at 04:18:41PM -0600, Robin Cockett wrote: > If you want to define the initial object in a functional language you > should write (say in Haskell): > > data Initial = > deriving (Show) -- so we can display the elements Unfortunately, this wouldn't be initial in Hask, because of two Haskell features: 1) Every Haskell datatype contains at least one element, namely "undefined", which represents (among other things) non-terminating computations. 2) Haskell is a lazy language, and thus functions are not required to preserve undefinedness. So we can write as many functions Initial -> Int as we please: one :: Initial -> Int one _ = 1 -- The _ means "ignore this input" five :: Initial -> Int five _ = 5 seventeen :: Initial -> Int seventeen _ = -17 -- XXX must get round to renaming this function -- to reflect changed functionality Calling these functions is as easy as Hugs> one undefined 1 Hugs> five undefined 5 Hugs> seventeen undefined -17 [D'oh!] Hope that helps, Miles -- Men occasionally stumble over the truth, but most of them pick themselves up and hurry on as if nothing had happened. -- Winston Churchill From rrosebru@mta.ca Mon Mar 16 20:48:03 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:48:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMWg-0001jP-Br for categories-list@mta.ca; Mon, 16 Mar 2009 20:47:22 -0300 Date: Mon, 16 Mar 2009 11:45:26 +0000 From: Miles Gould To: PETER EASTHOPE Message-Id: Status: O X-Status: X-Keywords: X-UID: 48 On Sun, Mar 15, 2009 at 07:35:37AM -0800, PETER EASTHOPE wrote: > Lawvere & Schanuel use a horizontal line > notation. Page 326 for example. > > X --> 1^T > --------- > TxX --> 1 > > This is unfamiliar. Does the line have a > name? How is it read? It's read "(X --> 1^T)" is the transpose of (TxX --> 1)", but I'm not aware of a name for the line itself. This is reasonably standard notation, by the way. Miles -- Besides, don't think aircraft carrier, think mecha. The type system is a great amplifier of careful reasoning and propagator of intent. If somebody starts muttering about bondage, just tell them "those straps are there so the servos can follow *me*". -- skew, on #haskell From rrosebru@mta.ca Mon Mar 16 20:49:36 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:49:36 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMYA-0001tk-LI for categories-list@mta.ca; Mon, 16 Mar 2009 20:48:54 -0300 From: Tom Hirschowitz To: Categories Mailing List Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: a further bit on functions in programming Date: Mon, 16 Mar 2009 15:28:47 +0100 Sender: categories@mta.ca Precedence: bulk Reply-To: Tom Hirschowitz Message-Id: Status: O X-Status: X-Keywords: X-UID: 49 Dear all, One more remark after my message with Pierre: talking about 'functions' in programming implicitly refers to functional languages, i.e., those where functions are first-class objects. If I'm not mistaken, in the presence of side effects, function types are not exponentials in the corresponding categories of programs (and product types are not products either). Indeed: Consider the following program p: print "founky" ; () where () is the element of type 1. This program prints "founky" and returns (). Considered as a morphism 1 * 1 -> 1, it has too candidate curryings 1 - > 1^1, namely: a) print "founky" ; (x |-> ()) and b) x |-> (print "founky" ; ()). The first program prints "founky" and returns the identity function 1^1. The second directly the function, which, each time it is called, prints "founky" and returns (). It is the case that a () ~ p and b () ~ p. However a and b are not observationally equivalent, as soon as effects are taken into account. Consider q : 1^1 -> 1 defined by: x (); x (). Then the program q a prints "founky" once, while q b prints it twice. A corresponding categorical structure has been proposed by Levy, Power, and Thielecke in their "Modelling environments in call-by-value programming languages" (Information and computation 185 (182-210), 2003. They call it "closed Freyd category". As far as I understand, they observe that requiring the currying to be central (i.e., effect- free) determines the right notion). Am I correct? Tom From rrosebru@mta.ca Mon Mar 16 20:50:15 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 16 Mar 2009 20:50:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjMYp-0001xZ-G3 for categories-list@mta.ca; Mon, 16 Mar 2009 20:49:35 -0300 Date: Mon, 16 Mar 2009 16:12:43 +0100 From: Andrew Stacey To: Categories Mailing List Subject: categories: Re: Functions in programming MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Andrew Stacey Message-Id: Status: O X-Status: X-Keywords: X-UID: 50 Wow! Thanks for _all_ the replies. I certainly learnt a lot very quickly just then. The students seemed to get the basic idea - assuming that I didn't mangle it. One or two seemed to know a bit of category theory and so were able to see a bit further than the others. So thanks again. Particularly, I'm very pleased that I was able to have an answer for the next class. I guess that the time zone helped there but even so it was great to have so many answers so fast. Andrew From rrosebru@mta.ca Tue Mar 17 08:31:56 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Mar 2009 08:31:56 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjXUH-0004zT-L7 for categories-list@mta.ca; Tue, 17 Mar 2009 08:29:37 -0300 From: "David Ellerman" To: Subject: categories: Re: Horizontal line notation. Date: Mon, 16 Mar 2009 19:15:30 -0700 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: "David Ellerman" Message-Id: Status: O X-Status: X-Keywords: X-UID: 51 The horizontal line notation was introduced by Gerhard Gentzen in his logical sequent calculus. If a set of formulas S implies a and b, then S implies a/\b and vice-versa which was written as: S |- a,b ______ S |- a/\b Going from top to bottom was conjunction-introduction, and going in the other direction was conjunction-elimination. After Lawvere noted that these Gentzen rules were simple adjunctions, he started writing all adjunctions using this Gentzen-style notation with the two adjoint transposes on top and on bottom and the arrow replacing the turnstile ( |- ) symbol. The notation caught on. __________________ David Ellerman Visiting Scholar University of California at Riverside Email: david@ellerman.org Webpage: www.ellerman.org View my social science research on my SSRN Author page: http://ssrn.com/author=294049 View my mathematics research at: http://arxiv.org/find/math/1/au:+Ellerman_D/0/1/0/all/0/1 Now out in paperback: Helping People Help Themselves: From the World Bank to an Alternative Philosophy of Development Assistance. University of Michigan Press. 2006. For more information, see the table of contents: http://www.ellerman.org/Davids-Stuff/Books/NEW%20RELEASE%20NOTICE.pdf . Book available at better booksellers online. -----Original Message----- From: categories@mta.ca [mailto:categories@mta.ca] On Behalf Of PETER EASTHOPE Sent: Sunday, March 15, 2009 8:36 AM To: categories@mta.ca Subject: categories: Horizontal line notation. Lawvere & Schanuel use a horizontal line notation. Page 326 for example. X --> 1^T --------- TxX --> 1 This is unfamiliar. Does the line have a name? How is it read? I'll guess either "(X --> 1^T) is equivalent to (TxX --> 1)" or "(X --> 1^T) is isomorphic to (TxX --> 1)". Thanks, ... Peter E. -- http://members.shaw.ca/peasthope/ http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/ From rrosebru@mta.ca Tue Mar 17 08:31:57 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 17 Mar 2009 08:31:57 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LjXVB-00052Q-BP for categories-list@mta.ca; Tue, 17 Mar 2009 08:30:33 -0300 Date: Tue, 17 Mar 2009 00:17:23 -0500 Subject: categories: Re: Functions in programming From: Nathan Bloomfield To: categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Nathan Bloomfield Message-Id: Status: O X-Status: X-Keywords: X-UID: 52 > There is one problem, of course: Haskell does not think this is legal as > it thinks all datatypes should have at least one constructor. This works for me in Hugs: data Void foo :: Void -> () foo _ = () foo undefined = () Although it uses laziness and the fact that undefined is a member of every type. (Apologies Robin; I forgot to reply to the list!) -Nathan Bloomfield, Arkansas From rrosebru@mta.ca Wed Mar 18 09:41:12 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Mar 2009 09:41:12 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ljv32-00049C-M2 for categories-list@mta.ca; Wed, 18 Mar 2009 09:39:04 -0300 Date: Tue, 17 Mar 2009 07:59:49 -0700 From: PETER EASTHOPE Subject: categories: Re: Horizontal line notation. To: categories@mta.ca MIME-version: 1.0 Content-type: text/plain; charset=us-ascii Content-language: en Content-transfer-encoding: 7bit Content-disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: PETER EASTHOPE Message-Id: Status: O X-Status: X-Keywords: X-UID: 53 Apologies for the faulty messages. Eleven replies! Thanks to everyone. Two obvious benefits: a line is easier to type and occupies less space than a vertical arrow. Ross Street wrote, "It means there is a natural bijection. ..." Micah Blake McCurdy wrote, "... The notation itself goes back to Gentzen, I think, but the meaning was not the same there -- he meant that the implication below the line could be deduced from the implication above the line." Andrej Bauer wrote, "In logic ... you put a double horizontal line if you want to emphasize that the rule goes both ways." So in Cat. Th., a single line might represent an arrow while a double line would represent a bijection? Apparently this convention isn't well established. Regards, ... Peter E. -- http://members.shaw.ca/peasthope/ http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/ From rrosebru@mta.ca Wed Mar 18 09:41:13 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Mar 2009 09:41:13 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ljv4K-0004Ho-Ng for categories-list@mta.ca; Wed, 18 Mar 2009 09:40:24 -0300 Date: Tue, 17 Mar 2009 12:36:12 -0700 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: Horizontal line notation. MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 54 David Ellerman wrote in part: >The horizontal line notation was introduced by Gerhard Gentzen in his >logical sequent calculus. If a set of formulas S implies a and b, then S >implies a/\b and vice-versa which was written as: S |- a,b _________ S |- a/\b >Going from top to bottom was conjunction-introduction, and going in the >other direction was conjunction-elimination. But much of sequent calculus is irreversible. If nothing else, structural rules such as weakening: S |- b -------- S:a |- b where S:a is the list or set S followed by a. (Thank all the Haskell recently for making me write it like this.) This is valid downwards, but not upwards. I see sequent-calculus people using a double line if it's good both ways: S |- a=>b =========== S:a |- b (This is a propositional version of the example in the original question.) Incidentally, your first example I would write as S |- a; S |- b ================ S |- a/\b because if you have a set, such as {a,b}, of propositions on the right, then this is interpreted disjunctively (not conjunctively as on the left). But I suppose that you can be lax about this if you agree beforehand that you'll only be doing "intuitionistic" sequents (that is those with only one statement on the right). --Toby From rrosebru@mta.ca Wed Mar 18 09:41:13 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Mar 2009 09:41:13 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ljv23-000449-RN for categories-list@mta.ca; Wed, 18 Mar 2009 09:38:03 -0300 Date: Tue, 17 Mar 2009 05:28:32 -0700 (PDT) From: Jeff Egger Subject: categories: Re: Horizontal line notation. To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: categories@mta.ca Precedence: bulk Reply-To: Jeff Egger Message-Id: Status: O X-Status: X-Keywords: X-UID: 55 Just to set the record straight... > The horizontal line notation was introduced by Gerhard Gentzen in his > logical sequent calculus. If a set of formulas S implies a and b, then S > implies a/\b and vice-versa which was written as: > > S |- a,b > ______ > S |- a/\b That's not quite correct: Gentzen uses a,b,... |- x,y,... to mean "(a and b and ...) entails (x or y or ...)". So what you have written is (if interpreted strictly according to Gentzen's sequent calculus) if "S entails (a or b)" then "S entails (a and b)" which is obviously incorrect. What Gentzen would write is this: S |- a S |- b ------------------- S |- a/\b (if "S entails a" and "S entails b", then "S entails (a and b)"); he would also write (separately) S |- a/\b --------- S |- a (if "S entails (a and b)", then "S entails a") and (again separately) S |- a/\b --------- S |- b (if "S entails (a and b)", then "S entails b"). The point here is that Gentzen did not actually intend his horizontal line notation to represent any sort of bijection. In fact, I rather suspect that he borrowed the line from elementary-school arithmetic: 24 73 92 ---- 189. [The only reason for writing S |- a S |- b ------------------- S |- a/\b instead of S |- a S |- b --------- S |- a/\b is in case you want to append proofs of S |- a and S |- b. In this manner one represents (complete) proofs as trees, where the leaves are axioms, and the root is the theorem being proven.] But I don't think the fact that Gentzen did not intend this horizontal line notation to represent the bijection which is obviously there should stop us from doing it: it's a very convenient way of discussing adjunctions, and there is as little chance of confusing the older use of this symbol with the newer one as confusing either with elementary school arithmetic. Cheers, Jeff. From rrosebru@mta.ca Wed Mar 18 09:41:38 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Mar 2009 09:41:38 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ljv4y-0004Lh-Rs for categories-list@mta.ca; Wed, 18 Mar 2009 09:41:04 -0300 Date: Tue, 17 Mar 2009 17:06:38 -0600 From: Robin Cockett MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Robin Cockett Message-Id: Status: O X-Status: X-Keywords: X-UID: 56 Vaughan Pratt wrote: > The categories mailing list is a good one for this sort of discussion ... So here is some (gentle) push-back for Vaughan ... BTW thank you everyone for pointing out that /everything/ I said was wrong/right! There really are underlying serious pedagogical and practical issue behind this ... typified by the comment. > Thorsten Altenkirch wrote: > > There really shouldn't be a difference between the functions in > > Mathematics and in Computer Science, especially functional programming. > The fact that nothing is quite what it "should be" in what has become the/a leading functional language is bothersome on the one hand for students struggling to develop a (unified) mathematical view and, simultaneously exciting for researchers who now have to find out which (!?!@!) category one is actually working in ... the fact that the answer is not an entirely simple (I do like Vaughan's "nuanced"!) is cause simultaneously for (pedagogical) concern and (researcher) delight. This reflects a general tension between semantics and implementation and the tussle over which is to be the cart and which is to be the horse. As it happens (I recall) one of the motivations behind Haskell was to produce a /lazy/ functional language and so a significant focus was actually on the implementation side ... perhaps at some semantical cost? Vaughan comments: > There should be differences within Mathematics and within Computer > Science, and therefore between them. I confess -- in this context -- what springs (uncalled) to mind is the (modified) comment of Chairman Mao: Computer Science is the continuation of Mathematics by other means! ... and sometimes the balance between what /should/ be done and what /can/ be done is pushed too far. At what stage this becomes a "bug" -- as Thorsten bluntly puts it -- definitely should be up for debate. And there is no doubt in my mind that in making this judgment the clarity of the underlying (categorical) semantics adds an important perspective .... and even should be prescriptive. Semantics does have some "real" effects: the semantics that a programmer has in mind and what is actually implemented by a language/API can be rather different ... and this can become particularly subtle as languages become more abstract (and peculiar) and are built on top of each other. Through these gaps can lie some very unexpected behaviors! Vaughan comments: > 2. One should not assume that mathematics has the answer to every > practical problem. Oft quoted John Arbuthnot commented (some time ago!): "There are very few things which we know, which are not capable of being reduced to a Mathematical Reasoning; and when they cannot it's a sign our knowledge of them is very small and confused; and 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." It really is hard to say more :-) ... but maybe "candle" should be replaced "compact florescent light bulb"? -robin From rrosebru@mta.ca Wed Mar 18 09:42:13 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Mar 2009 09:42:13 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ljv5V-0004Ph-QU for categories-list@mta.ca; Wed, 18 Mar 2009 09:41:37 -0300 Date: Wed, 18 Mar 2009 11:39:11 +0100 From: Carlos Areces Subject: categories: E.W. Beth Dissertation Prize: Extended Deadline Content-type: text/plain To: undisclosed-recipients:; Sender: categories@mta.ca Precedence: bulk Reply-To: Carlos Areces Message-Id: Status: O X-Status: X-Keywords: X-UID: 57 E. W. Beth Dissertation Prize: 2009 call for submissions Since 2002, FoLLI (the European Association for Logic, Language, and Information, www.folli.org) awards the E. W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2008. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of the three fields of Logic, Language, and Computation. Inter-disciplinarity is an important feature of the theses competing for the E. W. Beth Dissertation Prize. Who qualifies. ~~~~~~~~~~~~~~ Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2008 and December 31st, 2008. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2008 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for 2009). Respectively, nominations of full English translations of theses originally written in other language than English and defended in 2007 and 2008 will be accepted for consideration this year, too. Prize. ~~~~~~ The prize consists of: * a certificate * a donation of 2500 euros provided by the E. W. Beth Foundation. * an invitation to submit the thesis (or a revised version of it) to the new series of books in Logic, Language and Information to be published by Springer-Verlag as part of LNCS or LNCS/LNAI. (Further information on this series is available on the FoLLI site) How to submit. ~~~~~~~~~~~~~~ Only electronic submissions are accepted. The following documents are required: 1. the thesis in pdf or ps format (doc/rtf not accepted); 2. a ten page abstract of the dissertation in ascii or pdf format; 3. a letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded; 4. two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree. All documents must be submitted electronically to bethaward2008@gmail.com. Hard copy submissions are not admitted. In case of any problems with the email submission or a lack of notification within three working days after submission, nominators should write to goranko@maths.wits.ac.za or policriti@dimi.uniud.it, with a cc to bethaward2008@gmail.com. Important dates: Extended (strict) deadline for submissions: April 7, 2009. Notification of decision: July 1, 2009. Committee : * Anne Abeill=C3=A9 (Universit=C3=A9 Paris 7) * Natasha Alechina (University of Nottingham) * Wojciech Buszkowski (Adam Mickiewicz University, Poznan) * Didier Caucal (IGM-CNRS) * Nissim Francez (The Technion, Haifa) * Valentin Goranko (chair) (University of the Witwatersrand, Johannesburg= ) * Alexander Koller (Saarland University) * Alessandro Lenci (University of Pisa) * Gerald Penn (University of Toronto) * Alberto Policriti (Universit=C3=A0 di Udine) * Rob van der Sandt (University of Nijmegen) * Colin Stirling (University of Edinburgh) From rrosebru@mta.ca Thu Mar 19 10:08:16 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 10:08:16 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkHwj-0003wj-Cf for categories-list@mta.ca; Thu, 19 Mar 2009 10:06:05 -0300 Date: Wed, 18 Mar 2009 10:26:36 -0700 Subject: categories: Re: Horizontal line notation. From: Mike Stay To: Jeff Egger , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Mike Stay Message-Id: Status: O X-Status: X-Keywords: X-UID: 58 On Tue, Mar 17, 2009 at 5:28 AM, Jeff Egger wrote: > > Just to set the record straight... > >> The horizontal line notation was introduced by Gerhard Gentzen in his >> logical sequent calculus. If a set of formulas S =A0implies a and b, the= n S >> implies a/\b and vice-versa which was written as: >> >> S |- a,b >> ______ >> S |- a/\b > > That's not quite correct: Gentzen uses > =A0a,b,... |- x,y,... > to mean "(a and b and ...) entails (x or y or ...)". > So what you have written is (if interpreted strictly > according to Gentzen's sequent calculus) > =A0if "S entails (a or b)" then "S entails (a and b)" > which is obviously incorrect. > > What Gentzen would write is this: > S |- a =A0 =A0 =A0 S |- b > ------------------- > =A0 =A0 S |- a/\b > (if "S entails a" and "S entails b", then "S entails > (a and b)"); he would also write (separately) > S |- a/\b > --------- > =A0S |- a > (if "S entails (a and b)", then "S entails a") and > (again separately) > S |- a/\b > --------- > =A0S |- b > (if "S entails (a and b)", then "S entails b"). > > The point here is that Gentzen did not actually intend > his =A0horizontal line notation to represent any sort of > bijection. =A0In fact, I rather suspect that he borrowed > the line from elementary-school arithmetic: > =A024 > =A073 > =A092 > ---- > =A0189. > > [The only reason for writing > S |- a =A0 =A0 =A0 S |- b > ------------------- > =A0 =A0 S |- a/\b > instead of > =A0S |- a > =A0S |- b > --------- > S |- a/\b > is in case you want to append proofs of S |- a and > S |- b. =A0In this manner one represents (complete) > proofs as trees, where the leaves are axioms, and > the root is the theorem being proven.] > > But I don't think the fact that Gentzen did not intend > this horizontal line notation to represent the bijection > which is obviously there should stop us from doing it: > it's a very convenient way of discussing adjunctions, > and there is as little chance of confusing the older > use of this symbol with the newer one as confusing > either with elementary school arithmetic. > > Cheers, > Jeff. > The turnstile |- can be viewed as the hom functor (which in a poset is a truth value), while the horizontal bar is a (di)natural transformation. A double bar is a natural isomorphism. An empty "numerator" is the constant bifunctor T:C^op x C -> Set that picks out the one-element set. So, for example, we have ------ (id) X |- X which is a dinatural transformation from T to (X, X); the corresponding commuting hexagon says that the identity is a left and a right unit. Y |- Z X |- Y ----------------- (cut) X |- Z is a transformation that's natural in X, Z and dinatural in Y. The commuting hexagon says that composition is associative. Currying is usually written as two rules, one for introduction of -o (linear implication =3D internal hom) and one for eliminating it. But it's equivalent to use this natural isomorphism: X, Y |- Z =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D (curry) X |- Y -o Z which is an adjunction. --=20 Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com From rrosebru@mta.ca Thu Mar 19 10:08:16 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 10:08:16 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkHvo-0003rl-Vs for categories-list@mta.ca; Thu, 19 Mar 2009 10:05:09 -0300 Date: Wed, 18 Mar 2009 11:34:27 -0400 (EDT) From: Bill Lawvere To: Robin Cockett , categories@mta.ca Subject: categories: Re: Functions in programming MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bill Lawvere Message-Id: Status: O X-Status: X-Keywords: X-UID: 59 Question: Do the various programming languages explicitly implement the indispensible ingredient of categorical semantics, that every map has a unique codomain? I don't know the technical meaning of "lazy"; was it an attempt to avoid the processing speed and ram needed to take account of the composition with inclusion maps, etcetera? Bill ************************************************************ F. William Lawvere, Professor emeritus 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 ************************************************************ On Tue, 17 Mar 2009, Robin Cockett wrote: > Vaughan Pratt wrote: >> The categories mailing list is a good one for this sort of discussion ... > So here is some (gentle) push-back for Vaughan ... > > BTW thank you everyone for pointing out that /everything/ I said was > wrong/right! There really are underlying serious pedagogical and > practical issue behind this ... typified by the comment. > >> Thorsten Altenkirch wrote: >> > There really shouldn't be a difference between the functions in >> > Mathematics and in Computer Science, especially functional programming. >> > The fact that nothing is quite what it "should be" in what has become > the/a leading functional language is bothersome on the one hand for > students struggling to develop a (unified) mathematical view and, > simultaneously exciting for researchers who now have to find out which > (!?!@!) category one is actually working in ... the fact that the answer > is not an entirely simple (I do like Vaughan's "nuanced"!) is cause > simultaneously for (pedagogical) concern and (researcher) delight. > > This reflects a general tension between semantics and implementation and > the tussle over which is to be the cart and which is to be the horse. > As it happens (I recall) one of the motivations behind Haskell was to > produce a /lazy/ functional language and so a significant focus was > actually on the implementation side ... perhaps at some semantical cost? > > Vaughan comments: >> There should be differences within Mathematics and within Computer >> Science, and therefore between them. > I confess -- in this context -- what springs (uncalled) to mind is the > (modified) comment of Chairman Mao: Computer Science is the continuation > of Mathematics by other means! ... and sometimes the balance between > what /should/ be done and what /can/ be done is pushed too far. At what > stage this becomes a "bug" -- as Thorsten bluntly puts it -- definitely > should be up for debate. And there is no doubt in my mind that in > making this judgment the clarity of the underlying (categorical) > semantics adds an important perspective .... and even should be > prescriptive. > > Semantics does have some "real" effects: the semantics that a programmer > has in mind and what is actually implemented by a language/API can be > rather different ... and this can become particularly subtle as > languages become more abstract (and peculiar) and are built on top of > each other. Through these gaps can lie some very unexpected behaviors! > > Vaughan comments: >> 2. One should not assume that mathematics has the answer to every >> practical problem. > Oft quoted John Arbuthnot commented (some time ago!): > "There are very few things which we know, which are not capable of being > reduced to a Mathematical Reasoning; and when they cannot it's a sign > our knowledge of them is very small and confused; and 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." > > It really is hard to say more :-) ... but maybe "candle" should be > replaced "compact florescent light bulb"? > > -robin > > > > From rrosebru@mta.ca Thu Mar 19 10:08:16 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 10:08:16 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkHxe-00041g-MP for categories-list@mta.ca; Thu, 19 Mar 2009 10:07:02 -0300 Date: Wed, 18 Mar 2009 20:32:26 -0600 From: Robin Cockett MIME-Version: 1.0 To: Bill Lawvere , categories@mta.ca Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Robin Cockett Message-Id: Status: O X-Status: X-Keywords: X-UID: 60 I am not sure whether you got a response to this ... here is my attempt. Bill Lawvere wrote: > > Question: Do the various programming languages explicitly > implement the indispensible ingredient of categorical > semantics, that every map has a unique codomain? SO (you are right) the first problem is that usually maps (as a category theorist is thinking of such) are not what is implemented. Functional programming languages, for example, originate from combinatory algebra and the \lambda-calculus ... typing is only really introduced retrospectively as useful sugar on this underlying structure ... what is implemented is application -- or at least a particular rewriting/reduction process of application. A function A -> B is then a just a term which can be typed to be of type A -> B which can be applied to a term of type A to reduce (maybe) to something of type B ... application (as rewriting) is definitely the primitive and typing is retrospective (although very nice and useful). However, at this stage it does /look/ deceptively categorical as one does define f :: A -> B! And, of course that has led people to look at how one might interpret this as actually categorical ... and, of course, thereby hangs a lot of excellent work! However, what emerges is something whose relation to standard mathematical settings is surprisingly remote. Lazy evaluation (mixed with non-termination/partiality) is definitely partly to blame for this ... > > I don't know the technical meaning of "lazy"; was it an > attempt to avoid the processing speed and ram needed to > take account of the composition with inclusion maps, > etcetera? Lazy evaluation is basically a reduction strategy for the lambda calculus. It is a graph reduction strategy (you need a machine model with pointers) which does a "by-name"/"by need" evaluation with sharing of subexpressions which are duplicated in the rewriting process. Sharing arises as in the reduction S x y z => x z (y z) if z is a big structure you don't want to duplicate it so you "share" it ... and this means also you can share any rewriting you do on that structure. In terms of the rewriting steps required on the lambda calculus this reduction strategy is optimal ... however, in storage requirements it is often not optimal (so sometimes a "by-value" reduction will do better under this criterion). One feature of this rewriting technique is that it never looks at subterms which will be eliminated. E.g. in K x y => x the contents of y will never be inspected (as there is apparently no need). Of course, this is all well and good, except, when y had happened to be a term which did not terminate (i.e. had no support) , suddenly now one can produce something very definite from nothing! Of course this is what Miles Gould pointed out with a really simple Haskell program (lovely!). Even if you define the initial type "correctly" you can still write five :: Initial -> Int five _ = 5 and actually get 5 from nowhere! Of course, this really will not seem at all mysterious to a Haskell programmer who will mutter about strictness and bottoms. But it may be a bit of a shock to a mathematician! -robin P.S. Steve Vickers and Stevenson pointed out Chairman Mao plagiarized O:-) : According to the Penguin Dictionary of quotations: Karl von Clausewitz (1780-1831): "War is nothing more than the continuation of politics by other means". From rrosebru@mta.ca Thu Mar 19 10:08:16 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 10:08:16 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkHy3-00043a-Cc for categories-list@mta.ca; Thu, 19 Mar 2009 10:07:27 -0300 MIME-Version: 1.0 Date: Thu, 19 Mar 2009 12:40:18 +0100 Subject: categories: Assemblies without coproducts? From: Andrej Bauer To: categories list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Andrej Bauer Message-Id: Status: O X-Status: X-Keywords: X-UID: 61 This question is mostly for the realizabilitologists on the list. Let A be a PCA. The category of assemblies (or pers) over A has finite coproducts because any PCA contains true, false, and if-then-else. Let now A be a typed PCA (TPCA), according to John Longley. This means we have a non-empty set of types, operations * and -> on types (not necessarily freely generating the types). For each type t we have a set of values A_t. We require the K and S combinators to exist, as well as pairing and projections. We do NOT require that there be a boolean type, or a type of natural numbers. Some examples of TPCAs: - finite sets, with * and -> interpreted as cartesian product and exponential - Goedel's T - countably-based algebraic lattices - any PCA A where the type structure is then trivial and A_t = A. Assemblies over a TPCA are formed like the usual assemblies, except we have to specify underlying types. An assembly (S,t,|=) is a set S with a type t and a realizability relation |= between S and A_t. Now, do assemblies over a tpca A have binary coproducts? If A contains a type which resembles the booleans, we can do it. But I don't see how to do it in general. It's probably a trick involving higher-order functions. Andrej From rrosebru@mta.ca Thu Mar 19 21:59:14 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 21:59:14 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT3W-0001yz-LV for categories-list@mta.ca; Thu, 19 Mar 2009 21:57:50 -0300 Date: Thu, 19 Mar 2009 17:11:15 +0300 From: MigMit MIME-Version: 1.0 To: Robin Cockett , Bill Lawvere , categories@mta.ca Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: MigMit Message-Id: Status: O X-Status: X-Keywords: X-UID: 62 > However, what emerges is something whose relation to standard > mathematical settings is surprisingly remote. Lazy evaluation (mixed > with non-termination/partiality) is definitely partly to blame for this ... Can you elaborate a bit? > Of course, this really will not seem at all mysterious to a Haskell > programmer who will mutter about strictness and bottoms. But it may be > a bit of a shock to a mathematician! Hm-m-m, aren't Haskell (or, in fact, all) programmers just a special sort of mathematicians? From rrosebru@mta.ca Thu Mar 19 21:59:14 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 21:59:14 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT4G-00021E-Eq for categories-list@mta.ca; Thu, 19 Mar 2009 21:58:36 -0300 Subject: categories: Re: Functions in programming To: categories@mta.ca (Categories List) Date: Thu, 19 Mar 2009 11:18:22 -0300 (ADT) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit From: selinger@mathstat.dal.ca (Peter Selinger) Sender: categories@mta.ca Precedence: bulk Reply-To: selinger@mathstat.dal.ca (Peter Selinger) Message-Id: Status: RO X-Status: X-Keywords: X-UID: 63 Hi all, I am surprised that, in answer to one of Andrew Stacey's original questions (i.e., how are mathematical functions related to functions in computer programming), nobody has mentioned Moggi's work. I originally replied to Andrew privately, thinking that surely my reply would be one of dozens of more or less identical ones. Here is what I wrote: > Your wider question, on how functions in mathematics relate to > functions in computing, is an interesting and well-studied question. > In its simplest form, computer functions are the same as math > functions, i.e., they input an argument from a set, and compute an > output from another set. However, computer functions can have > additional behaviors known as "side effects". Here are some examples > of possible side-effects: > > (a) non-termination (loops forever) > (b) non-determinism (can output several possible values on the same input) > (c) probability (can call a random number generator) > (d) input/output (can write stuff to the screen or to a file) > (e) state (can "remember" some information from the last time it was called) > (f) exceptions (can indicate an error condition, to be handled elsewhere) > ... > > Interestingly, all of the above can be dealt with by using category > theory. Each of these notions of side-effect corresponds to a > particular strong monad on the category of sets. Each notion of > function corresponds to a morphism in the corresponding Kleisli > category. This was discovered by Moggi in the 1980's, see the > following paper, and particularly Example 1.1: > > Eugenio Moggi, "Notions of computation and monads". Information And > Computation, 93(1), 1991. > http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf And I may further elaborate, in case it is not obvious, what the monad is in each of the 6 examples of side-effects mentioned above: (a) TX = X+1 (b) TX = powerset(X) (c) TX = probability distributions on X (d) For output: TX = X x Sigma^* For input: TX = X + Sigma->X + Sigma^2->X + ... (Here, Sigma is an alphabet, and Sigma^* the free monoid generated by it). (e) TX = S -> (X x S), where S is a fixed set of states. (f) TX = X + E, where E is a fixed set of exceptions. It is straightforward to equip each of these operations with the structure of a strong monad, and to convince yourself that the Kleisli category in each case is the desired category of side-effecting functions. Of course this is not the end of the story: much further work has been devoted to the question of how to combine several such monads (for example, probability and state, or probability and non-determinism). Also, in the presence of higher-order functions, Set is not always good enough as a base category, and one typically considers other base categories such as a suitable category of DCPOs. So the question is not, as some have put it, whether non-termination (or other side effects) are "good" or "bad" to have in a programming language, but rather, what monad you would like to work with. In response to Bill Lawvere's question: laziness refers to an evaluation strategy where subterms are evaluated only if they are actually needed. For example, an "eager" evaluation of the arithmetic expression 0*(2+3) would first compute 2+3=5, then multiply the result by 0. A "lazy" evaluation would recognize that computing 2+3 is unnecessary. The question is not only one of efficiency, but also one of termination: if instead of 2+3, we use a non-terminating expression, then the lazy evaluation will terminate, whereas the eager one will not. In a lazy language such as Haskell, you can implement a function that computes the first 5 prime numbers as follows: (1) compute the list L of all prime numbers, in increasing order, and (2) take the first 5 elements of L. Since Haskell is lazy, it will automatically only do as much work in step (1) as is actually needed in step (2), i.e., it will not attempt to compute an infinite list. This leads to a quite natural programming style, often reminiscent of mathematical notation. -- Peter Andrew Stacey wrote: > > Here's a question for those who know about translating between > category theory for mathematicians and category theory for computer > programmers. > > In class today I was discussing functions with domain the empty set. > The students don't have much background in formal set theory (and > none in category theory though I'm doing my best to sneak it in > where I can) so they were trying to get to grips with the idea that > the _are_ functions from the empty set, but just not very many of > them. > > Afterwards, one student asked about how this related to functions as > used in computer programming. It seemed from what he said that he > had some understanding of the formal relationship between functions > in mathematics and functions in computer programs - beyond them > having the same name. He said that a function that takes no input > is known as a "constant function" and so wasn't sure how to fit the > two notions together. > > I, on the other hand, am at the level of "Ooo, look! Mathematicians > and computer programmers both use the word 'function'. So do > biologists and event organisers. Maybe we should organise a > function whose function would be to investigate all these different > uses.' so I didn't know what answer to give. > > The best that I could think of was that program functions have a > 'hidden' input: the fact that they have been called. So a function > defined on the empty set corresponds to a function that can never be > called. > > Can anyone help me straighten this out? > > Extra kudos for answers that I can just pass on to the student! > > Thanks, > > Andrew Stacey > > From rrosebru@mta.ca Thu Mar 19 21:59:25 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 21:59:25 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT4z-00023A-EJ for categories-list@mta.ca; Thu, 19 Mar 2009 21:59:21 -0300 MIME-Version: 1.0 Date: Thu, 19 Mar 2009 07:24:55 -0700 Subject: categories: laziness in functional programming From: John Baez To: categories@mta.ca Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: John Baez Message-Id: Status: RO X-Status: X-Keywords: X-UID: 64 Bill Lawvere wrote: I don't know the technical meaning of "lazy"; was it an attempt to avoid the > processing speed and ram needed to take account of the composition with > inclusion maps, etcetera? > No, "lazy evaluation" is a strategy of putting off computations until their results are known to be necessary. The opposite is called "eager evaluation". Laziness is often wiser. For example, a programming statement x:=y calls for the value of x to be set equal to y. A strategy of eager evaluation will do this right away, while lazy evaluation will put off doing it until the variable x is used in some other task. If x is never used, this saves work. I think most functional programming languages either delay evaluation in this way, or give the user the option to do this. Best, jb From rrosebru@mta.ca Thu Mar 19 22:00:34 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 22:00:34 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT66-00027R-9k for categories-list@mta.ca; Thu, 19 Mar 2009 22:00:30 -0300 Subject: categories: Re: Functions in programming To: robin@ucalgary.ca. wlawvere@buffalo.edu, categories@mta.ca Date: Thu, 19 Mar 2009 12:37:58 -0300 (ADT) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit From: selinger@mathstat.dal.ca (Peter Selinger) Sender: categories@mta.ca Precedence: bulk Reply-To: selinger@mathstat.dal.ca (Peter Selinger) Message-Id: Status: RO X-Status: X-Keywords: X-UID: 65 Robin Cockett wrote: > > SO (you are right) the first problem is that usually maps (as a category > theorist is thinking of such) are not what is implemented. Functional > programming languages, for example, originate from combinatory algebra > and the \lambda-calculus ... typing is only really introduced > retrospectively as useful sugar on this underlying structure ... what is > implemented is application -- or at least a particular > rewriting/reduction process of application. A function A -> B is then a > just a term which can be typed to be of type A -> B which can be > applied to a term of type A to reduce (maybe) to something of type B > ... application (as rewriting) is definitely the primitive and typing is > retrospective (although very nice and useful). > > However, at this stage it does /look/ deceptively categorical as one > does define f :: A -> B! And, of course that has led people to look at > how one might interpret this as actually categorical ... and, of course, > thereby hangs a lot of excellent work! > > However, what emerges is something whose relation to standard > mathematical settings is surprisingly remote. Lazy evaluation (mixed > with non-termination/partiality) is definitely partly to blame for this ... Hi all, sorry for writing twice in one day. If I didn't know Robin better, I would think he suggested that something is not categorical just because the functions in question are not morphisms in Set, but in some other category. And that the only "standard mathematical setting" is the category of sets and functions! Of course he didn't say any of these things. It only sounded like he did! Robin's examples: (1) The untyped lambda calculus. It is wrong to say that, in untyped languages, functions have no domain or codomain. What is correct is that there is just a single domain, which serves as the domain and codomain of all functions. So a model of an untyped language is a category with only one object U (but typically lots of morphisms). Now, a non-trivial such category can evidently not be cartesian-closed, because it cannot have an initial object. However, it *can* have binary products, internal function spaces, and even binary coproducts. In other words, it is possible to find one-object categories in which U = U x U, and U = U -> U, and possibly even U = U + U (and a few additional properties). Such categories are models of the untyped lambda calculus. The search for concrete examples of such categories has led to lots of interesting mathematical work, most of which is not category theory per se. However, clearly category theory is the most appropriate language for stating what properties a model has to satisfy. Moreover, the constructions that Robin mentioned, by which one passes from an untyped language to a typed language, are categorical in nature. One such construction is simply to split all idempotents. Even starting from a one-object category such as the above, one ends up with a cartesian-closed category with lots of objects, i.e., a "typed" setting. (2) Lazy languages. Here, an appropriate model is a category of pointed DCPO's (for simplicity, take finite posets with a least element, and monotone functions as the morphisms). Note that we do *not* require the morphisms to preserve the least element. The least element of each poset represents a non-terminating computation in that codomain. Functions that preserve the least element are called "strict", and they correspond to "eager" computations (i.e., they are forced to diverge if one of the inputs diverge). Functions that do not necessarily preserve the least element are "lazy" computations. For example, the "lazy booleans" are the three-element poset Bool={T,F,bot}, where T and F are incomparable, and bot is the bottom element. There are exactly 11 lazy functions from Bool to Bool. 9 of them are eager, and they correspond to every possible function f(bot)=bot, f(T)=a, f(F)=b, where a,b in {T,F,bot}. 2 functions are not eager, and they are the constant T and the constant F function (i.e., f(bot)=f(T)=f(F)=T, and f(bot)=f(T)=f(F)=F). Now clearly this category has a terminal object, namely the one-element poset 1={bot}. It is equally obvious that 1 is not initial, because there are for example 3 different monotone functions from 1 to Bool. And of course, the two non-strict functions from 1 to Bool are exactly the functions that Miles Gould so elegantly expressed in Haskell. It is equally obvious that this category has no initial object (and of course, for the same reason, neither does Haskell have an initial type). None of this is the least bit mysterious, neither mathematically, nor from a programming perspective. Robin mentioned the limit-colimit coincidence, but he forgot that this only applies to directed limits. It is of course false that initial objects and terminal objects always coincide, even in models where the limit-colimit coincidence holds. One may further object that the description of the particular category of DCPO's is not really category theory, that it is ad hoc and not particularly canonical (for example, it is not the free category of any particular kind). And indeed, the devil is in the details and there are many open problems regarding the existence of categories of DCPO's that are suitable for particular purposes. However, there is no question that category theory gives the correct tools for specifying what kind of category one must construct, for discussing alternatives between the different approaches, etc. I hope that these examples help to dispell the view that untyped languages, or lazy languages, are some kind of "practical hack" invented by programmers and implementors that don't really fit any mathematical model. Or, as Robin put it, "whose relation to standard mathematical settings is surprisingly remote". Actually, the contrary is very much true, and category theory is a large part of the reason. [The same cannot, of course, be said for such languages as C, Fortran, Perl, or Visual Basic, which actually *are* practical hacks with no mathematical model. That is precisely why theoreticians study Haskell or ML or Scheme or the lambda calculus or Agda or Charity and so forth.] -- Peter From rrosebru@mta.ca Thu Mar 19 22:01:12 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 22:01:12 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT6j-0002AW-1I for categories-list@mta.ca; Thu, 19 Mar 2009 22:01:09 -0300 Date: Thu, 19 Mar 2009 17:19:59 +0100 Subject: categories: Re: Assemblies without coproducts? From: Andrej Bauer To: categories list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Andrej Bauer Message-Id: Status: O X-Status: X-Keywords: X-UID: 66 On Thu, Mar 19, 2009 at 12:40 PM, Andrej Bauer wrote: > Now, do assemblies over a tpca A have binary coproducts? If A contains > a type which resembles the booleans, we can do it. But I don't see how > to do it in general. It's probably a trick involving higher-order > functions. Following a (private) suggestion by Thomas Streicher, a possible candidate for a TPCA A such that Asm(A) does not have coproducts would be the TPCA whose types are lattices and monotone maps (take countable lattices if you like to worry about size). Note that taking algebraic lattices won't do because those are injective and so they'll allow us to define if-then-else by continuoulsy extending the interesting part of if-then-else (I hope someone will understand what I am saying). Also, I do not see at the moment whether we get coproducts for the TPCA of total continuous functionals over the real numbers. More precisely, let A be the finite type hierachy over the real numbers, as generated in some super- or sub-ccc of topological spaces that contains the reals. Another candidate is the "syntactic" TPCA generated by the simply typed lambda-calculus (with products) over a base type. Perhaps there is a syntactic theorem which tells us that this TPCA does not have "weak" coproducts (which is what is needed to get coproducts at the level of assemblies). Best regards, Andrej From rrosebru@mta.ca Thu Mar 19 22:03:09 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 19 Mar 2009 22:03:09 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT8a-0002Kj-Po for categories-list@mta.ca; Thu, 19 Mar 2009 22:03:04 -0300 Date: Thu, 19 Mar 2009 15:08:02 -0700 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: Horizontal line notation. Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 67 Mac Lane corresponded with Mints nearly three decades ago on the relationship between coherence and proofs. One manifestation of the connection is as the often-mentioned Curry-Howard isomorphism. More recently Kosta Dosen and Zoran Petric have written at length about the relationship in their 2004 book Proof-Theoretical Coherence. I asked Grisha a few questions to see if he felt any of Gentzen's work suggested categorical intuitions, which he answered as follows, essentially in the negative: the connections came much later. (I was surprised by his statement that the sequent calculus is not close to adjunctions, given that the adjoints of the diagonal functor correspond so well to introduction and elimination of logical connectives, and likewise for quantifiers. I'll ask him about that next time I see him, which may be a couple of weeks since we're in Spring break, at which point van Benthem may be here. Grisha's suggestion to ask Prawitz is a good one.) Vaughan -------- Original Message -------- Subject: categories and Gentzen systems Date: Wed, 18 Mar 2009 12:41:56 -0700 (PDT) From: Grigori Mints gmints at stanford edu Hi Vaughan, you may use these comments as you like. > You and Mac Lane had some interaction on this some time ago. > What's > your understanding of what Gentzen had in mind? MacLane's initial understanding of the connection between categories and logic is summarized in the first of two papers below, his summary of our correspondence is in the second paper. MacLane S. Topology and logic as a sourse of algebra, Bull. Amer. Math. Soc. 82, 1976, no 1, 1-40 MacLane S., Why commutative diagrams coincide with equivalent proofs, in: Contemporary Mathematics, v. 13, 1982, 387-401, American Mathematical Society, Providence MacLane was a graduate stuident in Gottingen at the same time as Gentzen. If Gentzen had some ideas very close to categorical treatment of logical deductions, it seems unlikely to me Mac Lane would forget. > Is it just an accident > that the sequent calculus as conceived by Gentzen turned out to be > convenient to express adjunctions, or did Gentzen independently invent > symmetric monoidal categories? I do not see any analogy in Gentzen's writing, even in very recent publication by Jan von Plato of the first vesrion of Gentzen's dissertation containing quite modern normalization proof for natural deduction. By the way, it is not sequent calculus but natural deduction which is close to formulation in terms of adjunctions. Still there is a significant distance between the latter two, bridged in the work by several authors in the years 1970-1980. > Also what was the interaction if any between Goedel's Dialectica > interpretation of S4 and Gentzen's interpretation of his sequent > calculus? Did either man derive any inspiration of this kind from the > other? You mean Godel's Dialectica interpretation of the intuitionistic logic. It is completely unlikely that Gentzen was not aware of the effective (Brouwer-Heyting-Kolmogorov) interpretation of intuitionistic logical connectives, but again I do not see any evidence of this is his writings. His first consistency proof for arithmetic contains game-theoretic semantics, but that is a different matter. Godel certainly derived some inspiration from Gentzen's writings, he comments about this in detail in Zilsel's report. Gentzen's main work was finished long before the ideas of realizability (Dialectica is one of them) which made BHK interpretation explicit became public. > Does Prawitz have > a view on what Gentzen was thinking that got him (Gentzen) to something > so like category theory? Again, no indication in Prawitz' writings, but you can ask him. He certainly is deeply influenced by Gentzen's idea that the meaning of logical connectives is given by introduction-elimination rules. In this formulation the idea is probably due to Prawitz. Best, Grisha From rrosebru@mta.ca Sat Mar 21 10:42:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 21 Mar 2009 10:42:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ll1SI-0006hA-L2 for categories-list@mta.ca; Sat, 21 Mar 2009 10:41:42 -0300 MIME-Version: 1.0 Date: Fri, 20 Mar 2009 11:26:56 -0700 Subject: categories: Re: laziness in functional programming From: Greg Meredith To: John Baez , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Greg Meredith Message-Id: Status: O X-Status: X-Keywords: X-UID: 68 John, et al, The last statement is not true. Laziness is relatively new as the default evaluation strategy in more mainstream functional languages. You can always effect it with "thunks" (wrapping things up in lambdas), but it's not a standard semantic in the dynamic functional languages (Lisp, Scheme, Dylan, ...) nor is it standard in the ML family of the statically typed functional languages (ML, OCaml, F#, ... ). Scala gives a keyword to cause this to be the evaluation strategy. Haskell is fairly unique as a high profile functional language with the property that evaluation is lazy unless forced to be eager. Note that while laziness may be wiser from the point of view of not tripping over potentially divergent computations, it is often very challenging to get lazy code to be memory efficient (because you must pay for the deferred computation in space). Moreover, laziness appears to give very brittle performance characteristics, in the sense that small changes to lazy algorithms can result in dramatic differences in performance characteristics. Unfortunately, there seems to be a "no free lunch" theorem behind this. If ever there were a place where theory could help practice, this is one (hint, hint). Finding good conceptual tools to aid in the design of * appropriately* lazy algorithms for large scale computations would be a real boon. There is no dirth of experience papers of the form "We (computational biologists, computational financiers, machine learning theorists, ...) thought we'd give Haskell a try. We loved the productivity, but we found that there was a significant cost in optimizing our code to meet production level memory and other resource requirements." Best wishes, --greg On Thu, Mar 19, 2009 at 7:24 AM, John Baez wrote: > Bill Lawvere wrote: > > > I don't know the technical meaning of "lazy"; was it an attempt to avoid > the > > processing speed and ram needed to take account of the composition with > > inclusion maps, etcetera? > > > > No, "lazy evaluation" is a strategy of putting off computations until their > results are known to be necessary. The opposite is called "eager > evaluation". Laziness is often wiser. > > For example, a programming statement > > x:=y > > calls for the value of x to be set equal to y. A strategy of eager > evaluation will do this right away, while lazy evaluation will put off > doing > it until the variable x is used in some other task. If x is never used, > this saves work. > > I think most functional programming languages either delay evaluation in > this way, or give the user the option to do this. > > Best, > jb > > > -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com From rrosebru@mta.ca Sat Mar 21 10:42:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 21 Mar 2009 10:42:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ll1Qr-0006eC-KK for categories-list@mta.ca; Sat, 21 Mar 2009 10:40:13 -0300 Date: Fri, 20 Mar 2009 12:11:34 +0000 From: Miles Gould To: categories@mta.ca Subject: categories: Re: laziness in functional programming Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Miles Gould Message-Id: Status: O X-Status: X-Keywords: X-UID: 69 On Thu, Mar 19, 2009 at 07:24:55AM -0700, John Baez wrote: > I think most functional programming languages either delay evaluation in > this way, or give the user the option to do this. It's generally fairly easy to roll your own lazily-evaluated data-structures in any modern language. All you do, instead of returning the value in question, is return a function of no arguments (often called a "thunk", or a "promise") which calculates said value when called. When the value is needed, the thunk is called (and then usually replaced with the value, to save future computation). In languages without first-class functions (functions which can be stored in variables, constructed on-the-fly, etc) you have to do slightly more work to construct the thunk, but this is tedious rather than hard. See http://blog.plover.com/prog/defunctionalization.html for a discussion of how Java programmers work around the lack of first-class functions. At the other end of the scale, some strictly-evaluated languages (Scheme and O'Caml, for example), provide convenient interfaces for constructing lazily-evaluated data-structures, which are implemented using thunks. It's perhaps worth mentioning that lazy evaluation, though often a Very Good Thing, is not all roses: it makes the run-time performance (speed and memory consumption) of a program more complex to predict. Miles -- An extensible program is a double-edged sword, but recent experience has shown that users prefer a double-edged sword to a blunt one. -- Paul Graham From rrosebru@mta.ca Sat Mar 21 10:42:44 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 21 Mar 2009 10:42:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ll1T2-0006j7-8D for categories-list@mta.ca; Sat, 21 Mar 2009 10:42:28 -0300 From: MFPS To: mfpsmail@linus.math.tulane.edu, categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: MFPS 25 Program Date: Fri, 20 Mar 2009 15:20:22 -0500 Sender: categories@mta.ca Precedence: bulk Reply-To: MFPS Message-Id: Status: O X-Status: X-Keywords: X-UID: 70 The Program for MFPS 25 is now posted on the web page http://www.math.tulane.edu/~mfps/mfps25.htm You will also find local information about the meeting and accommodations. There is still time to register and to reserve a room in college (at Univ) or at the Linton Lodge. We are also offering a reduced registration for those who can attend MFPS only for the final two days, Monday, April 6 and Tuesday, April 7. Note that the conference dinner will take place on the evening of the 6th. Mathematical Foundations of Programming Semantics http://www.math.tulane.edu/~mfps From rrosebru@mta.ca Sat Mar 21 10:43:55 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 21 Mar 2009 10:43:55 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ll1UN-0006nk-4M for categories-list@mta.ca; Sat, 21 Mar 2009 10:43:51 -0300 Date: Fri, 20 Mar 2009 15:18:41 -0600 From: Robin Cockett MIME-Version: 1.0 To: Peter Selinger , categories@mta.ca Subject: categories: Re: Functions in programming Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Robin Cockett Message-Id: Status: O X-Status: X-Keywords: X-UID: 71 Peter Selinger wrote: > I hope that these examples help to dispell the view that untyped > languages, or lazy languages, are some kind of "practical hack" > invented by programmers and implementors that don't really fit any > mathematical model. Or, as Robin put it, "whose relation to standard > mathematical settings is surprisingly remote". Actually, the contrary > is very much true, and category theory is a large part of the reason. > [The same cannot, of course, be said for such languages as C, Fortran, > Perl, or Visual Basic, which actually *are* practical hacks with no > mathematical model. That is precisely why theoreticians study Haskell > or ML or Scheme or the lambda calculus or Agda or Charity and so > forth.] > Well I certainly did not intend to imply (or I think say) that lazy functional languages (Haskell) or other strict languages (the ML family) are hacks! Absolutely not -- gosh I would loose my job!!! Clearly I should be clearer on what I did not say! For example I should be clear that things "whose relation to standard mathematical settings is surprisingly remote" can be (in fact usually are) extremely mathematical and important to the development of mathematical thought! When I said that producing something from nothing "may be a bit of a shock to a mathematician" this was not saying that, therefore it is not mathematical: the fact that Fermat's last theorem was proven may also have shocked a good few mathematicians who had not expected it. In this case it is a shock in the sense that naively a mathematician may not have considered carefully what setting he was actually in ... I certainly did want to emphasize the sense in which a program language can be an exploration of a particular perspective (Mathematics by other means). Furthermore, that there is a creative tension between implementation (which, in case anyone thinks otherwise, is -- if done well -- /very/ mathematical: for example in the case of the lambda calculus rests on the now extensive theory of rewriting) and semantics, which I view as prescriptive mathematics (typified by set theory and logic of the 1900s) in which one asserts far reaching axioms hoping madly that they are "right" -- or at least useful. Computer Scientists probably understand this best as simply the difference between a bottom-up and top-down approach -- played out perhaps on a slightly broader canvas -- and would instantly recognize the importance of both (as I am sure would mathematicians). Of course, it is nice if the two approaches meet. (And if I did not know Peter better I might think that he is saying that the whole business is nicely sewn up ... nothing could be further from the truth! Of course he didn't say this. It only may have sounded like he did! ;-) ) If you will now forgive me for being a little colorful to reemphasize a point ... (then that is definitely it from me!) The prescriptive approach, of course, is extremely arrogant: it says "this is what I want" and "this is how the world should be". It was typified by the development of set theory whose the aim was to a pin down exactly what God had intended once and for all. Of course, the real danger to this, much more serious than getting it wrong -- you can always fix that -- is that God is actually playing with a number of settings and hasn't really settled on which one he likes best! The Greeks understood this perfectly 8-) . This is where Category Theory slips into the picture: it is clearly stupid to study just one setting (unless God makes up his mind suddenly) instead lets just study them all! Now in the process of dredging through God's basement (where he keeps his discarded ideas) it would definitely be rather disheartening if we found the lambda calculus (after all that is where HE keeps his discarded ideas)! So let us suppose that this does not happen ... but that we do find ("hiding under the wreckage of set theory" Paul Taylor quickly adds) a really nice implementable category which has a simple axiomatization and resembles the sort of naive mathematics that everyone uses. Wouldn't it just be tempting to pull it out and implement it anyway? ... and, strictly as a market ploy of course, put about that God had had an off day and had made a mistake? The point is that even if there is a base computational reality, we are in the altogether strange situation that we don't actually have to accept it! Computation, just like mathematics, is open to prescription. We can still choose to work in more restrictive settings where getting around (in some ways) may be easier (or safer). And this is a important aspect of programming language and semantics research ... in particular, being Turing complete is /not /an absolute requirement of a programming language (it is certainly something which one can ask about a language!). Far from the semantical/prescriptive approach to computation being dead, it is more alive than ever ... this is not an argument against computability, however, it IS an argument for the important role of Category Theory in Computer Science for helping us to understand the relationship between settings we might want to implement (... on which I think Peter agrees!) -robin From rrosebru@mta.ca Sun Mar 22 10:12:29 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 22 Mar 2009 10:12:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LlNRY-0007cg-Rt for categories-list@mta.ca; Sun, 22 Mar 2009 10:10:24 -0300 Date: Sat, 21 Mar 2009 12:06:25 -0400 (EDT) From: Bill Lawvere To: Robin Cockett , Peter Selinger , categories@mta.ca Subject: categories: Re: Functions in programming MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bill Lawvere Message-Id: Status: O X-Status: X-Keywords: X-UID: 72 Thanks for the several interesting replies. I think I am learning what "lazy" means, but there seems to be embedded in it a presupposition that the order in which new expressions are introduced in a computation is something that one does not carefully plan. It still seems to me to be possible that the developing languages are partly the legacy of an epoch when computational power was qualitatively less than now. I was especially heartened to see the lack of support for St. John's position "in the beginning was the word", especially in view of the recent attempts by physicists to revive that idealist position. Many of us have long instinctively believed that language should fit concepts and concepts should fit reality. Bill ************************************************************ F. William Lawvere, Professor emeritus 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 ************************************************************ On Fri, 20 Mar 2009, Robin Cockett wrote: > Peter Selinger wrote: >> I hope that these examples help to dispell the view that untyped >> languages, or lazy languages, are some kind of "practical hack" >> invented by programmers and implementors that don't really fit any >> mathematical model. Or, as Robin put it, "whose relation to standard >> mathematical settings is surprisingly remote". Actually, the contrary >> is very much true, and category theory is a large part of the reason. >> [The same cannot, of course, be said for such languages as C, Fortran, >> Perl, or Visual Basic, which actually *are* practical hacks with no >> mathematical model. That is precisely why theoreticians study Haskell >> or ML or Scheme or the lambda calculus or Agda or Charity and so >> forth.] >> > Well I certainly did not intend to imply (or I think say) that lazy > functional languages (Haskell) or other strict languages (the ML family) > are hacks! Absolutely not -- gosh I would loose my job!!! > > Clearly I should be clearer on what I did not say! > > For example I should be clear that things "whose relation to standard > mathematical settings is surprisingly remote" can be (in fact usually > are) extremely mathematical and important to the development of > mathematical thought! When I said that producing something from > nothing "may be a bit of a shock to a mathematician" this was not > saying that, therefore it is not mathematical: the fact that Fermat's > last theorem was proven may also have shocked a good few mathematicians > who had not expected it. In this case it is a shock in the sense that > naively a mathematician may not have considered carefully what setting > he was actually in ... > > I certainly did want to emphasize the sense in which a program language > can be an exploration of a particular perspective (Mathematics by other > means). Furthermore, that there is a creative tension between > implementation (which, in case anyone thinks otherwise, is -- if done > well -- /very/ mathematical: for example in the case of the lambda > calculus rests on the now extensive theory of rewriting) and semantics, > which I view as prescriptive mathematics (typified by set theory and > logic of the 1900s) in which one asserts far reaching axioms hoping > madly that they are "right" -- or at least useful. > > Computer Scientists probably understand this best as simply the > difference between a bottom-up and top-down approach -- played out > perhaps on a slightly broader canvas -- and would instantly recognize > the importance of both (as I am sure would mathematicians). > > Of course, it is nice if the two approaches meet. (And if I did not > know Peter better I might think that he is saying that the whole > business is nicely sewn up ... nothing could be further from the > truth! Of course he didn't say this. It only may have sounded like he > did! ;-) ) > > If you will now forgive me for being a little colorful to reemphasize a > point ... (then that is definitely it from me!) > > The prescriptive approach, of course, is extremely arrogant: it says > "this is what I want" and "this is how the world should be". It was > typified by the development of set theory whose the aim was to a pin > down exactly what God had intended once and for all. Of course, the > real danger to this, much more serious than getting it wrong -- you can > always fix that -- is that God is actually playing with a number of > settings and hasn't really settled on which one he likes best! The > Greeks understood this perfectly 8-) . > > This is where Category Theory slips into the picture: it is clearly > stupid to study just one setting (unless God makes up his mind suddenly) > instead lets just study them all! Now in the process of dredging > through God's basement (where he keeps his discarded ideas) it would > definitely be rather disheartening if we found the lambda calculus > (after all that is where HE keeps his discarded ideas)! So let us > suppose that this does not happen ... but that we do find ("hiding > under the wreckage of set theory" Paul Taylor quickly adds) a really > nice implementable category which has a simple axiomatization and > resembles the sort of naive mathematics that everyone uses. Wouldn't it > just be tempting to pull it out and implement it anyway? ... and, > strictly as a market ploy of course, put about that God had had an off > day and had made a mistake? > > The point is that even if there is a base computational reality, we are > in the altogether strange situation that we don't actually have to > accept it! Computation, just like mathematics, is open to > prescription. We can still choose to work in more restrictive settings > where getting around (in some ways) may be easier (or safer). And this > is a important aspect of programming language and semantics research > ... in particular, being Turing complete is /not /an absolute > requirement of a programming language (it is certainly something which > one can ask about a language!). > > Far from the semantical/prescriptive approach to computation being > dead, it is more alive than ever ... this is not an argument against > computability, however, it IS an argument for the important role of > Category Theory in Computer Science for helping us to understand the > relationship between settings we might want to implement (... on which I > think Peter agrees!) > > -robin From rrosebru@mta.ca Mon Mar 23 09:24:25 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Mar 2009 09:24:25 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LljA4-0005p8-Av for categories-list@mta.ca; Mon, 23 Mar 2009 09:21:48 -0300 From: Michael Fourman To: Bill Lawvere , Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 Subject: categories: Re: Re: Functions in programming Date: Sun, 22 Mar 2009 14:22:24 +0000 Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Fourman Message-Id: Status: O X-Status: X-Keywords: X-UID: 73 Dear Bill, It's not primarily a matter of efficiency, but rather of expressiveness. In a lazy language one can define an infinite list, pass it around as a value, and access particular elements of it "on demand". This demand-driven computation can be conceptually much cleaner than trying to carefully plan, in advance, which values should be computed in what order. See, for example: http://www.haskell.org/haskellwiki/Performance/Laziness http://lua-users.org/wiki/HammingNumbersVariant Best, Michael On 21 Mar 2009, at 16:06, Bill Lawvere wrote: > > Thanks for the several interesting replies. > I think I am learning what "lazy" means, but > there seems to be embedded in it a presupposition > that the order in which new expressions are > introduced in a computation is something that > one does not carefully plan. It still seems to > me to be possible that the developing languages > are partly the legacy of an epoch when computational > power was qualitatively less than now. > > I was especially heartened to see the lack of > support for St. John's position "in the beginning > was the word", especially in view of the recent > attempts by physicists to revive that idealist > position. Many of us have long instinctively > believed that language should fit concepts > and concepts should fit reality. > > Bill > > > ************************************************************ > F. William Lawvere, Professor emeritus > 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 Mar 23 09:24:25 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Mar 2009 09:24:25 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LljAs-0005sS-6v for categories-list@mta.ca; Mon, 23 Mar 2009 09:22:38 -0300 Date: Mon, 23 Mar 2009 11:17:24 +0100 (CET) From: Paul-Andre Mellies To: categories@mta.ca Subject: categories: postdoc position in Paris MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Paul-Andre Mellies Message-Id: Status: O X-Status: X-Keywords: X-UID: 74 ====================================================== Postdoctoral position in PPS (CNRS & University Paris 7) Curry-Howard and Concurrency Theory ====================================================== A 12-month postdoctoral position is available within the Laboratory PPS (Preuves Programmes Systemes) located at University Paris 7 Denis Diderot: http://www.pps.jussieu.fr/ The position is supported by the research project Curry-Howard and Concurrency Theory (CHOCO) funded by the French national research agency ANR. http://choco.pps.jussieu.fr/ Important dates: - intention of application (short email) April 15th 2009 - deadline for application: May 31st 2009 - notification: June 15th 2009 - suggested starting date: September 1st 2009 Application procedure. We strongly recommend that potential candidates express their interest in the position by sending an email by April 6th. Full application should be sent before May 31st 2009 including a resume, a short research project (1 page) and two names of possible references. This should be preferably done by email or at the postal address below. For all correspondance use the contact addresses: postdoc-choco@pps.jussieu.fr Paul-Andre Mellies Laboratoire PPS Universite Paris 7 - Denis Diderot Case 7014 75205 Paris Cedex 13 FRANCE The net salary will be around 2000 euro/month before income tax. The starting date for the postdoctoral position is September 2009 although later dates may be also considered. Description The general purpose of the project CHOCO is to investigate the syntactic, semantic and algebraic aspects of proof theory in order to integrate concurrency theory in the Curry-Howard correspondence between proofs and programs. The interdisciplinary nature of the project between proof theory and concurrency theory means that candidates from various scientific horizons are welcome to apply. On the other hand, we will consider with special interest applications by candidates with background in one or several of the fields: - linear logic (proof nets, geometry of interaction) - semantics (game semantics, vectorial semantics) - concurrency theory (process calculi, presheaf semantics) - type theory (realizability, types for process calculi) - rewriting theory (lambda-calculus, diagrammatic rewriting) - category theory (categorical algebra, topos theory) The applicant should hold a PhD or be about to defend his/her PhD thesis by December 2009. The postdoc researcher will work within the laboratory PPS (Preuves, Programmes, Systemes) http://www.pps.jussieu.fr which is internationally recognized as one of the leading research laboratories in mathematics and computer science, with its distinctive proof-theoretic culture. The laboratory PPS is located in Chevaleret, the largest research community of mathematicians in France. The laboratory PPS is also part of the Fondation Sciences Mathematiques de Paris. http://www.sciencesmath-paris.fr Strong interaction of the postdoc researcher with the partner sites of the CHOCO project is also expected: - Laboratoire d'Informatique de Paris Nord. - Laboratoire d'Informatique du Parallelisme, Lyon, - Laboratoire de Mathematiques de l'Universite de Savoie, Chambery - Institut de Mathematiques de Luminy, Marseille, - Laboratoire d'Informatique Fondamentale de Marseille, Further information will possibly be made available from the web page of the project indicated above. From rrosebru@mta.ca Tue Mar 24 14:08:20 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 24 Mar 2009 14:08:20 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LmA3Z-0001Qz-HL for categories-list@mta.ca; Tue, 24 Mar 2009 14:04:53 -0300 Mime-Version: 1.0 (Apple Message framework v753.1) Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed To: Categories list From: =?UTF-8?Q?Jonathan_CHICHE_=E9=BD=90=E6=AD=A3=E8=88=AA?= Subject: categories: Grothendieck's legacy videos Date: Tue, 24 Mar 2009 16:58:29 +0100 Sender: categories@mta.ca Precedence: bulk Reply-To: =?UTF-8?Q?Jonathan_CHICHE_=E9=BD=90=E6=AD=A3=E8=88=AA?= Message-Id: Status: O X-Status: X-Keywords: X-UID: 75 Hello all, The conference devoted to Grothendieck's legacy (or, if you're =20 French: l'h=E9ritage de Grothendieck) held at IHES at the end of =20 January has already been mentioned here. I noticed but a few days ago =20= that videos of the talks are available on the Internet at http://=20 video.google.fr/videosearch?hl=3Dfr&q=3Dihes%=20 20grothendieck&um=3D1&ie=3DUTF-8&sa=3DN&tab=3Dwv# If the link is broken, look for "Grothendieck" at http://=20 www.dailymotion.com. Wilfried Scharlau's talk may be of interest to =20 many members of this list. Jonathan=20= From rrosebru@mta.ca Wed Mar 25 09:33:27 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 25 Mar 2009 09:33:27 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LmSGz-0004WC-Ud for categories-list@mta.ca; Wed, 25 Mar 2009 09:31:57 -0300 MIME-Version: 1.0 Date: Tue, 24 Mar 2009 10:57:48 -0700 Subject: categories: naive questions about sets From: Meredith Gregory To: categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Meredith Gregory Message-Id: Status: O X-Status: X-Keywords: X-UID: 76 Categorical, i have a question about a presentation of sets. The motivation for this question comes from a conversation i had a few years ago with Jamie Gabbay concerning the use of FM-set theory in semantics for 'freshness'. i was arguing that a certain use of 'reflection' gave a canonical (and smallest) set of atoms. Jamie objected that atoms are not allowed to have internal structure in FM-set theory. My question has to do with my response. Because my question has to do with a formulation in categorical language, rather than formulate it in that language, i will formulate it naively. In my view, heavily influenced by computing as it is, i see the basics of set theory as providing some operations for constructing and inspecting, de-structing a data type called set. Very primitively, we have operations for - extensionally constructing sets, '{ ... }' and - operations for intensionally constructing sets '{ ... | ... }' - operations for inspecting sets 'x in ... ' In this view, nothing prevents me from imagining two different versions of this data type. One of which i will call the 'black' version and one of which i will call the 'red' version. Initially, i might imagine these data types as copies of each other; but, we can only construct and inspect 'black sets' with 'black' braces and 'black' in predicate; and likewise for the 'red sets'. So, never the twain shall meet. Now, once we've built such a structure, there's nothing to prevent us from imaginging that the 'atoms' of a 'black' FM-set theory are none other than 'red sets'. Symmetrically, nothing prevents us from imagining that the 'atoms' of a 'red' FM-set theory are none other than 'black sets'. A suggestive use of data type specifications might illustrate the idea - Ordinary sets - Set ::= '{' Set* '}' - Red/black sets - BlackSet ::= '{b|' (BlackSet + RedAtom)* '|b}' - RedSet ::= '{r|' (RedSet + BlackAtom)* '|r}' - RedAtom ::= RedSet - BlackAtom ::= BlackSet Now, my question: is there a topos theoretic characterization of the obvious zoology that results from these musings? Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com From rrosebru@mta.ca Thu Mar 26 09:39:05 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Mar 2009 09:39:05 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lmopr-000144-2T for categories-list@mta.ca; Thu, 26 Mar 2009 09:37:27 -0300 From: Pedro Resende To: Categories list Subject: categories: "Senior postdoc" research positions (5 years) Mime-Version: 1.0 (Apple Message framework v930.3) Date: Thu, 26 Mar 2009 12:19:21 +0000 Content-Type: text/plain;charset=US-ASCII;format=flowed;delsp=yes Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Pedro Resende Message-Id: Status: RO X-Status: X-Keywords: X-UID: 78 Dear categorists, The announcement below may be interesting for some readers of this list. Regards, Pedro. ####### Date: Mon, 23 Mar 2009 13:18:42 +0000 From: Diogo Aguiar Gomes To: Diogo Aguiar Gomes Subject: Post-doctoral positions Dear Colleagues, the UT Austin | Portugal program in the area of Mathematics invites applications for post-doctoral positions under the FCT Ciencia 2008 program. These are five year research positions at one of the Portuguese institutions participating in the UT Austin | Portugal Mathematics program, namely - Universidade de Coimbra - Faculdade de Ciencias e Tecnologia; - Universidade de Lisboa - Faculdade de Ciencias; - Instituto Superior Tecnico; - Universidade Nova de Lisboa - Faculdade de Ciencias e Tecnologia. Candidates should have a PhD Degree in Mathematics, obtained less than 10 years ago and a minimum of 3 year post-doctoral experience. Applicants should send a curriculum vitae, a description of research project and ask that three letters of reference are sent directly to: Joanne Laranjeiro - jlaranj@math.ist.utl.pt before April 20, 2009. From rrosebru@mta.ca Thu Mar 26 09:39:05 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Mar 2009 09:39:05 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lmooe-0000xA-62 for categories-list@mta.ca; Thu, 26 Mar 2009 09:36:12 -0300 Date: Thu, 26 Mar 2009 12:20:10 +0100 From: Jaap van Oosten MIME-Version: 1.0 To: categories@mta.ca, fom@cs.nyu.edu Subject: categories: job opening in Nijmegen Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Jaap van Oosten Message-Id: Status: O X-Status: X-Keywords: X-UID: 79 There is a job opening in Nijmegen. See below. Assistant professor (UD) in the Algebra & Logica group The Algebra&Logic group of IMAPP at Radboud University seeks a tenure-track assistant professor with preference for applicants working in the area between algebra, logic, and computer science. We seek candidates with international experience that have a demonstrable commitment to excellence in both research and teaching. The candidate should be motivated to contribute independently and through collaboration to the research and growth of the group. This includes contributing to the supervision of Master and PhD students and securing of funding for PhD positions through grant applications. The candidate must be a good communicator with experience in as well as enthusiasm for teaching that can contribute across the undergraduate mathematics curriculum as well as at the graduate level in algebra and especially in logic and in the joint research master with computer science. The candidate is expected to contribute the usual share in the management of the group and institute. The accepted candidate is required to master the Dutch language sufficiently to be able to teach in Dutch within two years after the appointment. Radboud University Nijmegen is situated in the oldest city in the Netherlands. It has nine faculties and enrols over 17,500 students in 107 study programmes. The Faculty of Science at Radboud University consists of seven research institutes, including the Institute for Mathematics, Astrophysics, and Particle Physics (IMAPP), and the Institute for Computing and Information Science (ICIS). Research in non-classical logic and its interaction with applications in computer science is strongly represented locally and nationally. The group has close ties with the ICIS research groups in Foundations and in Security of Systems. At the national level the group collaborates with algebraists and logicians, notably in Leiden, Utrecht, at ILLC in Amsterdam, and at CWI. The salary of an assistant professor varies from a minimum of 3.195,-- Euros bruto per month to a maximum of 4.970,-- bruto per month, depending on relevant work experience. (scale 11/12). Female applicants are particularly encouraged to apply. In order to apply please send an application, with reference to vacancy number 18. DE including a full CV, information on research plans and teaching experience, and names and addresses of three references either by e-mail to pz@science.ru.nl or by post to: FNWI Personeel en Organisatie attn. mevr. Marielle Nelemans Postbus 9010 6500 GL Nijmegen The Netherlands Review of applications will begin May 1, 2009. For further information, see http://www.math.ru.nl/~mgehrke/Algebra&LogicUD.htm or contact Mai Gehrke at mgehrke@math.ru.nl **************** Profile: Profile of Algebra&Logic Assistant Professor at IMAPP at the Faculty of Science, Radboud University Nijmegen The Faculty of Science at Radboud University consists of seven research institutes, including the Institute for Mathematics, Astrophysics, and Particle Physics (IMAPP), and the Institute for Computing and Information Science (ICIS). The Mathematics division of IMAPP consists of three groups: Algebra&Logic, Mathematical Physics, and Stochastics. The research of the Algebra&Logic group is focused in the two named areas with a particular focus on interactions of algebra and logic with computer science. Research in non-classical logic and its interaction with applications in computer and information science is strongly represented locally and nationally. The group has close ties with the ICIS research groups in Foundations and in Security of Systems. At the national level the group collaborates with algebraists and logicians, notably in Leiden, Utrecht, at ILLC in Amsterdam, and at CWI. In teaching, the algebra and logic group is part of the Mathematics, Physics, and Astronomy Teaching Institute (WiNSt) and as such it provides high quality teaching of core and service courses in all branches of undergraduate mathematics as well as advanced courses and a Master track in Algebra and Logic. In addition, a new Radboud University Research Master program in the Mathematical Foundations of Computer Science is being set up jointly with computer science. The faculty as a whole and the mathematics department in particular are enthusiastically involved in outreach and actively recruit students through programs with schools. The Algebra&Logic group seeks a tenure track assistant professor with preference for applicants working in the algebra-logic-computer science triangle. We seek candidates with international experience that have a demonstrable commitment to excellence in both research and teaching. The candidate should be motivated to contribute independently and through collaboration to the research and growth of the group. This includes contributing to the supervision of Master and PhD students and securing of funding for PhD positions through grant applications. The candidate must be a good communicator with experience in as well as enthusiasm for teaching that can contribute across the undergraduate mathematics curriculum as well as at the graduate level in algebra and logic, and particularly in the joint research master with computer science. The candidate is expected to contribute the usual share in the management of the group and institute. The accepted candidate is required to master the Dutch language sufficiently to be able to teach in Dutch within two years after the appointment. Female applicants are particularly encouraged to apply. -- Prof.Dr.Mai Gehrke IMAPP Chair of Algebra Radboud Universiteit Toernooiveld 1 6525 ED NIJMEGEN THE NETHERLANDS mgehrke@math.ru.nl http://www.math.ru.nl/~mgehrke/ +31 (0)24 365 3220 (office) +31 (0)24 329 5536 (home) +31 (0)24 365 2986 (secretariat) +31 (0)24 365 2191 (IMAPP fax) From rrosebru@mta.ca Fri Mar 27 19:29:29 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 27 Mar 2009 19:29:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LnKVW-0006Zz-Gw for categories-list@mta.ca; Fri, 27 Mar 2009 19:26:34 -0300 From: Matthew Hennessy To: moca-announce@list.it.uu.se Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: PhD studentships - Dublin Date: Thu, 26 Mar 2009 15:56:17 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Matthew Hennessy Message-Id: Status: O X-Status: X-Keywords: X-UID: 80 Apologies for multiple postings -------------------------------- The Foundations of Global Computing - Trinity College Dublin Two PhD studentships Applications are invited for two PhD studentships within the Software Systems Lab of the Department of Computer Science. The positions are part of a SFI-funded research project, under the direction of Matthew Hennessy, which seeks to establish a firm mathematical and logical basis for the next generation of widely distributed computing environments. The research programme within the project is wide ranging in scope, offering considerable flexibility to the successful candidates to pursue particular research interests. These range from the design and investigation of abstract calculi for describing the behaviour of complex systems, the use of types to enforce security policies, to the development of verification technologies for ensuring properties of mobile agents. Qualification requirements: Applicants should have at least a good honours primary degree in Computer Science or Mathematics, and have a proven aptitude in discrete mathematics and the manipulation of formal systems. Remuneration: 17,000 euros per annum, plus postgraduate fees, for three years, starting in October 2009. Application details: Interested applicants should, in the first instance, send their CV to the address below, together with a statement outlining their suitability for the project and the names of two referees. Applications by email are welcome. Matthew Hennessy Department of Computer Science The O'Reilly Institute Trinity College Dublin 2, Ireland email: matthew.hennessy@cs.tcd.ie tel: +353 (01) 8962634 From rrosebru@mta.ca Fri Mar 27 20:01:24 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 27 Mar 2009 20:01:24 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LnL2f-0000M6-27 for categories-list@mta.ca; Fri, 27 Mar 2009 20:00:49 -0300 MIME-Version: 1.0 Date: Fri, 27 Mar 2009 15:55:05 -0700 Subject: categories: naive questions about sets From: Meredith Gregory To: categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Meredith Gregory Message-Id: Status: O X-Status: X-Keywords: X-UID: 81 Categorical, >From the deafening silence i take it that there is no treatment of these sorts of structures in the topos-theoretic or other categorical literature. The whole area is a very rich vein. On the one hand there is great practical interest in providing a modular semantics for fresh variables and alpha-equivalence and a whole cottage industry has grown up around it. (Jamie Gabbay's homepage is a good place for links.) On the other, 'atoms' of the type in Fraenkel-Mostowski set theory do not occur in an effective nature. An infinite supply of entities with no internal structure, but which support an equality test, takes up way too much room to fit inside a computational device. So, finding a consistent way to keep all the benefits of the FM substitution methodsas they apply to alpha equivalence while staying in an effective theory is of both practical and theoretical interest. Further, the generalization provide lots of structure to explore. One avenue of investigation has to do with what can be contained. i found the construction when teaching my 12 year old daughter set theory. We were using the pedagogical device of set as physical container. Unfortunately, the axiom of extensionality introduces a decidedly non-physical twist to things (not counting quantum mechanical intuitions about what is physical). The example we hit first was the von Neumann encoding for 2 [| 2 |] = { [| 0 |], [| 1 |] } = { [| 0 |], { [| 0 |] } } which puts the same set in two clearly different physical locations. My daughter and i decided that what went into the physical containers were little promisory notes that could be redeemed for actual things. In this version of the construction you only get flat structures, a set never contains a set. That left the problem of the language in which the promisory notes were written. Why not use the language of containers? - Container ::= {c| Note* |c} // BlackSet ::= {b| RedSet* |b} - Note ::= {n| Container* |n} // RedSet ::= {r| BlackSet* |r} This has lots and lots of fun questions regarding how to redeem notes for containers. It turns out that by carefully controlling the computational power of how things are redeemed you never get the Russell paradox. This appears to be related to stratified set theories such as the NF (thanks for the link Paul!), but the circular set up does not show up in the wikipedia article. Another avenue of investigation is the number and kinds of color as there is nothing that requires only two colors. In the spirit of the notation below, we can think of a whole collection of different colored set theories arranged by Set(i) ::= {i| ( \Sigma_{ j != i } Set(j) )* |i} This has interest for generic programming community. Find hereHaskell code that resulted in a conversation i had with Bruno Oliveira regarding using generic programming techniques to take advantage of cyclic symmetry in the different set theories. Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com From rrosebru@mta.ca Sat Mar 28 09:47:01 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 28 Mar 2009 09:47:01 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LnXw4-000264-9f for categories-list@mta.ca; Sat, 28 Mar 2009 09:46:52 -0300 MIME-Version: 1.0 Date: Fri, 27 Mar 2009 18:07:12 -0700 Subject: categories: Re: naive questions about sets From: Meredith Gregory To: Toby Bartels , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Meredith Gregory Message-Id: Status: O X-Status: X-Keywords: X-UID: 82 Toby, Thanks for your note. A longer reply is forthcoming, but in regards to notation, in CS-y conventions it is now standard to separate out the "free" syntax from the relations. So, you're right, of course, that the * denotes a list. (It originates from the Kleene operator.) The standard treatment is to whack this down by what is called a structural equivalence relation. In this case, you have something like n1,n2 = n2,n1 n1,n1 = n1 for the structural relations. This is roughly equivalent to specifying models as algebras, i.e. a free monad plus a a structure map. i find the ghettoization of the CS notations -- which are extremely compact and well aligned with category theoretic sensibilities -- to be a source of unending frustration in communications with the larger mathematical communities. i really need to write a tutorial. Best wishes, --greg On Fri, Mar 27, 2009 at 5:35 PM, Toby Bartels < toby+categories@ugcs.caltech.edu >wrote: > Meredith Gregory wrote in part: > > >My > >daughter and i decided that what went into the physical containers were > >little promisory notes that could be redeemed for actual things. In this > >version of the construction you only get flat structures, a set never > >contains a set. That left the problem of the language in which the > promisory > >notes were written. Why not use the language of containers? > > - Container ::= {c| Note* |c} // BlackSet ::= {b| RedSet* > |b} > > - Note ::= {n| Container* |n} // RedSet ::= {r| BlackSet* > |r} > > Not to denigrate your interesting variation, > but you get a result more like traditional set theory > if you say that each container contains a *single* note > which itself has a list of containers written on it: > - Container ::= {c| Note |c} > - Note ::= {n| Container* |n} > (You could also have a list of notes, each of which has one container.) > > Of course, this is functionally equivalent to > - Container ::= {c| Container* |c} > This is the usual model of what pure sets are like, > but (as you and your daughter noted) this give an unphysical metaphor. > However, you could just as easily do things like this: > - Note ::= {n| Note* |n} > Since {n|...|n} contains things by writing down names for them, > rather than having them physically present as {c|...|c} implies, > there is no physical impossibility here. > > Incidentally, the notation X* suggests to me a list, > where order and repetition matter and only finitely many terms can appear. > Of course, sets are not like this, as you know. > So instead of X* I would write P(X), using "P" for "power". > > This matches how category theorists model pure sets > (the sets that appear in ZF-style set theory). > A _universe of pure sets_ consists of a set U > and a function from U to the power set P(U) of U, > or if you prefer a binary relation E (for 'epsilon') on U, > satisfying a few axioms (extensionality and well-foundedness, > although it's also interesting to consider ill-founded sets). > You get paradoxes like Russell's if you add the axiom > that the function U -> P(U) is invertible. > > Of course, I said "set" above, but there I just meant > an object of the category of sets as category theorists think of it. > That is, simply a collection of atoms that may be equal > but have no other structure (and in particular are not themselves sets). > So this shows how to model ZF-style set theory in categorial set theory. > (I apologise for repetition if you already know all about that.) > > > --Toby > -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com From rrosebru@mta.ca Sat Mar 28 09:47:01 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 28 Mar 2009 09:47:01 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LnXuk-00023d-8X for categories-list@mta.ca; Sat, 28 Mar 2009 09:45:30 -0300 Date: Fri, 27 Mar 2009 17:35:59 -0700 From: Toby Bartels To: Meredith Gregory , categories@mta.ca Subject: categories: Re: naive questions about sets MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 83 Meredith Gregory wrote in part: >My >daughter and i decided that what went into the physical containers were >little promisory notes that could be redeemed for actual things. In this >version of the construction you only get flat structures, a set never >contains a set. That left the problem of the language in which the promisory >notes were written. Why not use the language of containers? > - Container ::= {c| Note* |c} // BlackSet ::= {b| RedSet* |b} > - Note ::= {n| Container* |n} // RedSet ::= {r| BlackSet* |r} Not to denigrate your interesting variation, but you get a result more like traditional set theory if you say that each container contains a *single* note which itself has a list of containers written on it: - Container ::= {c| Note |c} - Note ::= {n| Container* |n} (You could also have a list of notes, each of which has one container.) Of course, this is functionally equivalent to - Container ::= {c| Container* |c} This is the usual model of what pure sets are like, but (as you and your daughter noted) this give an unphysical metaphor. However, you could just as easily do things like this: - Note ::= {n| Note* |n} Since {n|...|n} contains things by writing down names for them, rather than having them physically present as {c|...|c} implies, there is no physical impossibility here. Incidentally, the notation X* suggests to me a list, where order and repetition matter and only finitely many terms can appear. Of course, sets are not like this, as you know. So instead of X* I would write P(X), using "P" for "power". This matches how category theorists model pure sets (the sets that appear in ZF-style set theory). A _universe of pure sets_ consists of a set U and a function from U to the power set P(U) of U, or if you prefer a binary relation E (for 'epsilon') on U, satisfying a few axioms (extensionality and well-foundedness, although it's also interesting to consider ill-founded sets). You get paradoxes like Russell's if you add the axiom that the function U -> P(U) is invertible. Of course, I said "set" above, but there I just meant an object of the category of sets as category theorists think of it. That is, simply a collection of atoms that may be equal but have no other structure (and in particular are not themselves sets). So this shows how to model ZF-style set theory in categorial set theory. (I apologise for repetition if you already know all about that.) --Toby From rrosebru@mta.ca Mon Mar 30 16:54:35 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 30 Mar 2009 16:54:35 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LoNVn-0005Gf-TB for categories-list@mta.ca; Mon, 30 Mar 2009 16:51:12 -0300 Date: Mon, 30 Mar 2009 11:19:15 +0100 From: Monika Seisenberger MIME-Version: 1.0 To: undisclosed-recipients:; Subject: categories: Cfc: CALCO-jnr 2009: CALCO Young Researchers Workshop, Udine, Italy Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Monika Seisenberger Message-Id: Status: O X-Status: X-Keywords: X-UID: 85 [Apologies for multiple copies] !!! PLEASE FORWARD TO PHD STUDENTS AND YOUNG RESEARCHERS !!! *------------------------------------------------------------------* * Call for contributions * * * * CALCO-jnr 2009 * * * * CALCO-jnr: CALCO Young Researchers Workshop * * September 6, 2009, Udine, Italy * * * * part of * * 3rd Conference on Algebra and Coalgebra in Computer Science * * September 6-12, 2009, Udine, Italy * * * *------------------------------------------------------------------* * Abstract submission: May 8, 2009 * * Author notification: May 22, 2009 * * Final abstract due: June 15, 2009 * * Full paper submission: October 15, 2009 * *------------------------------------------------------------------* * http://calco09.dimi.uniud.it/ * *------------------------------------------------------------------* CALCO 2009 will be preceded by the CALCO Young Researchers Workshop, CALCO-jnr, dedicated to presentations by PhD students and young researchers at the beginning of their careers. CALCO brings together researchers and practitioners to exchange new results related to foundational aspects and both traditional and emerging uses of algebras and coalgebras in computer science. The study of algebra and coalgebra relates to the data, process and structural aspects of software systems. This is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). The first and second, very successful CALCO conferences took place 2005 in Swansea, Wales, and 2007 in Bergen, Norway. The third event will take place 2009 in Udine, Italy. The CALCO Young Researchers Workshop, CALCO-jnr, is a CALCO satellite workshop dedicated to presentations by PhD students and by those who have completed their doctoral studies within the past few years. Attendance at the workshop is open to all - it is anticipated that many CALCO conference participants will want to attend the CALCO-jnr workshop (and vice versa). CALCO-jnr presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page abstracts, by the CALCO-jnr PC. A booklet with the abstracts of the accepted presentations will be available at the workshop. After the workshop, the author(s) of each presentation will be invited to submit a full 10-15 page paper on the same topic. They will also be asked to write (anonymous) reviews of papers submitted by other authors on related topics. Additional reviewing and the final selection of papers will be carried out by the CALCO-jnr PC. The volume of selected papers from the workshop will be published as a technical report at Udine. Authors will retain copyright, and are also encouraged to disseminate the results reported at CALCO-jnr by subsequent publication elsewhere. Topics of Interest ------------------ The CALCO Young Researchers Workshop will invite submissions on the same topics as the CALCO conference: reporting results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transition of resulting technologies into industrial practice. In particular, the workshop will encourage submissions included or related to the topics listed below. * Abstract models and logics - Automata and languages, - Categorical semantics, - Modal logics, - Relational systems, - Graph transformation, - Term rewriting, - Adhesive categories * Specialised models and calculi - Hybrid, probabilistic, and timed systems, - Calculi and models of concurrent, distributed, mobile, and context-aware computing, - General systems theory and computational models (chemical, biological, etc) * Algebraic and coalgebraic semantics - Abstract data types, - Inductive and coinductive methods, - Re-engineering techniques (program transformation), - Semantics of conceptual modelling methods and techniques, - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification, - Formal testing and quality assurance, - Validation and verification, - Generative programming and model-driven development, - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra Submission ---------- Submission (pdf-file) is via e-mail to m.seisenberger@swansea.ac.uk. The use of LNCS style (see http://www.springer.de/comp/lncs/authors.html) is strongly encouraged. Important Dates --------------- 8 May 2009 Deadline for 2-page abstract submission 22 May 2009 Notification of abstract selection decision 15 Jun 2009 Final version of abstract due 6 Sep 2009 CALCO Young Researchers Workshop 7-10 Sep 2009 CALCO technical programme 15 Oct 2009 Deadline for 10-15 page paper submission 15 Dec 2009 Notification of paper selection decision 20 Jan 2010 Final version of paper due Programme Committee ------------------- * Magne Haveraaen, University of Bergen, Norway http://www.ii.uib.no/~magne/ * Marina Lenisa, University of Udine, Italy http://sole.dimi.uniud.it/~marina.lenisa/ * John Power, University of Bath, UK http://www.cs.bath.ac.uk/department/contact-department/academic-staff/dr-john-power.html * Monika Seisenberger, Swansea University, UK http://www.cs.swan.ac.uk/~csmona/ -- CALCO-jnr 2009: http://calco09.dimi.uniud.it/calcojnr.html CALCO 2009: http://www.dimi.uniud.it/calco09/ From rrosebru@mta.ca Tue Mar 31 08:55:14 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 31 Mar 2009 08:55:14 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LocWx-0005ev-I9 for categories-list@mta.ca; Tue, 31 Mar 2009 08:53:23 -0300 Date: Mon, 30 Mar 2009 22:26:04 +0100 (BST) From: Bob Coecke To: categories@mta.ca Subject: categories: Quantum Physics and Logic - Oxford April 8-9 MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bob Coecke Message-Id: Status: O X-Status: X-Keywords: X-UID: 86 The program of: The 6th QPL workshop Quantum Physics and Logic April 8-9, 2009, Oxford University, UK http://web.comlab.ox.ac.uk/people/Bob.Coecke/QPL_09.html Is now available from: http://www.comlab.ox.ac.uk/people/bob.coecke/QPL_09_program.html There is no formal registration. There is a non-compulsory small registration fee to cover the coffee breaks, and for a copy of the proceedings. So just show up if you're interested. The location is Lecture Theatre B of Oxford University Computing Laboratory, at the corner of Keble rd and Parks rd. From rrosebru@mta.ca Wed Apr 1 13:51:14 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 01 Apr 2009 13:51:14 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lp3bb-0005Tp-Fq for categories-list@mta.ca; Wed, 01 Apr 2009 13:47:59 -0300 Date: Tue, 31 Mar 2009 14:04:20 +0100 (BST) From: Bob Coecke To: Bob Coecke Subject: categories: Categories, Quanta, Concepts (CQC) at Perimeter Institute MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Bob Coecke Message-Id: Status: O X-Status: X-Keywords: X-UID: 87 WORKSHOP ANNOUNCEMENT: Categories, Quanta, Concepts (CQC) June 1-5, 2009, Perimeter Institute, Waterloo, Canada Organizers: Andreas Doering, Theoretical Physics Group, Imperial College Bob Coecke, Computing Laboratory, Oxford University Lucien Hardy, Perimeter Institute In recent years, more and more mathematical methods and results from the field of category theory have been employed in the foundations of physics. These methods enable us to reconsider conceptual and structural issues in the foundations of quantum theory and possibly beyond, often providing surprising insights and new points of view. The workshop "Categories, Quanta, Concepts" (CQC) will bring together researchers from a variety of backgrounds, physicists, mathematicians, theoretical computer scientists and philosophers, all with a common interest in the foundations of physics. With talks in the morning and workgroups and in-depth sessions in the afternoon, the workshop will provide ample opportunity for interaction between the participants from this emerging community. The workshop also serves as an ideal platform for PhD students to get insight into the field and to discuss their own work. Invited speakers: Samson Abramsky, Wolfson College, Oxford University Harvey Brown, Faculty of Philosophy, Oxford University Howard Barnum, Los Alamos National Laboratory Richard Blute, Dept. Mathematics and Statistics, Ottawa University Keye Martin, U.S. Naval Research Laboratory Prakash Panangaden, School of Computer Science, McGill University Peter Selinger, Mathematics and Statistics, Dalhousie University Mike Stay, University of California at Riverside Webpage: http://www.perimeterinstitute.ca/Events/Categories%2C_Quanta%2C_Concepts/Categories%2C_Quanta%2C_Concepts_%28CQC%29/ From rrosebru@mta.ca Wed Apr 1 13:52:06 2009 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 01 Apr 2009 13:52:06 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lp3fU-0005sc-3y for categories-list@mta.ca; Wed, 01 Apr 2009 13:52:00 -0300 Date: Tue, 31 Mar 2009 17:08:36 -0700 (PDT) From: John MacDonald To: categories@mta.ca Subject: categories: FMCS09 - VANCOUVER MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: John MacDonald Message-Id: Status: RO X-Status: X-Keywords: X-UID: 88 FMCS 2009 17th Workshop on Foundational Methods in Computer Science University of British Columbia, VANCOUVER, Canada MAY 28th - 31st, 2009 SECOND ANNOUNCEMENT * * * FMCS09 now has a website where one can reserve accommodation online. The address is http://www.pims.math.ca/scientific/general-event/foundational-methods-computer-science-2009 I would urge you and your students, if any are attending, to book accommodation early since the housing office will not guarantee booking for our group past April 28. They will, however continue to book if space is available. The third announcement will contain a more complete list of participants so if you are not on the preliminary list of particpants and you will or may attend, then please send email to johnm@math.ubc.ca with subject heading FMCS09 - WILL ATTEND or FMCS09 - MAY ATTEND. Preliminary List of Participants: Robin Cockett, Computer Science University of Calgary Calgary, Alberta Pieter Hofstra, Mathematics University of Ottawa Ottawa, Ontario Mike Johnson, Mathematics and Computer Science Macquarie University Sydney, Australia John MacDonald, Mathematics University of British Columbia Vancouver, British Columbia Ernie Manes, Mathematics University of Massachusetts Amherst, Massachusetts Phil Mulry, Computer Science Colgate University Hamilton, New York Dorette Pronk, Mathematics Dalhousie University Halifax, Nova Scotia Bob Rosebrugh, Mathematics and Computer Science Mount Allison University Sackville, New Brunswick R A G Seely, Mathematics McGill University Montreal, Quebec Peter Selinger, Mathematics Dalhousie University Halifax, Nova Scotia Art Stone, Mathematics Vancouver, British Columbia Hofstra student, Ottawa, Ontario Cockett student(s), Calgary, Alberta The following paragraphs repeat the information from the first announcement. The Department of Mathematics at the University of British Columbia in cooperation with the Pacific Institute of Mathematical Sciences is hosting the Foundational Methods in Computer Science workshop on May 28th - 31st, 2009, on the University of British Columbia Campus in Vancouver, Canada The workshop is an annual informal meeting intended to bring together researchers in mathematics and computer science. There is a focus on the application of category theory in computer science. However, all those who are interested in category theory or computer science are welcome to attend. The meeting begins with a reception at 6pm in the Ruth Blair room in Walter Gage Towers on the UBC campus on Thursday May 28, 2009. The scientific program starts on May 29, and consists of a day of tutorials aimed at students and newcomers to category theory, as well as a day and a half of research talks. The meeting ends at mid-day on May 31. Research talks There will be some invited presentations, but the majority of the talks are solicited from the participants. If you wish to give a talk please send a title and abstract to johnm@math.ubc.ca. Time slots are limited, so please register early if you would like to be considered for a talk. Graduate student participation is particularly encouraged at FMCS. Registration details will appear in the third announcement. Previous meetings Previous FMCS meetings were held in Pullman (1992), Portland (1993), Vancouver (1994), Kananaskis (1995), Pullman (1996), Portland (1998), Kananaskis (1999), Vancouver (2000), Spokane (2001), Hamilton (2002), Ottawa (2003), Kananaskis (2004), Vancouver (2005), Kananaskis (2006), Hamilton (2007), and Halifax (2008). Organizing committee: Robin Cockett (Calgary) John MacDonald (UBC) Phil Mulry (Colgate) Peter Selinger (Dalhousie) Local Organizer: John MacDonald (UBC)