*mbx* 42cf5ab000000000 7-Jan-2005 11:11:48 -0400,5415;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 07 Jan 2005 11:11:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cmvhl-0001f6-00 for categories-list@mta.ca; Fri, 07 Jan 2005 11:07:09 -0400 Date: Fri, 7 Jan 2005 14:48:38 +0100 To: paola.bruscoli@inf.tu-dresden.de From: Paola Bruscoli Subject: categories: CFP: Structures and Deduction Workshop - ICALP '05 Satellite Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Message-Id: ICALP Workshop-Lisbon July 16-17, 2005 STRUCTURES AND DEDUCTION The quest for the essence of proofs This meeting is about new algebraic and geometric methods in proof theory, with the aim of expanding our ability to manipulate proofs, eliminate bureaucracy from deductive systems, and ultimately provide: 1) a satisfying answer to the problem of identity of proofs and 2) tools for improving our ability to implement logics. Stimulated by computer science, proof theory is progressing at fast pace. However, it is becoming very technical, and runs the risk of splitting into esoteric specialties. The history of science tells us that this has happened several times before, and that these centrifugal tendencies are very often countered by conceptual reunifications, which occur when one is looking at a field after having taken a few steps back. Some emerging ideas are showing their unifying potential. Deep inference's atomization of deductions simplifies and unifies the design of deduction systems; it provides unprecedented plasticity to proofs and has injected new impetus into the theory of proof nets. New proof nets, and new associated semantics, are giving surprising insight about the very subtle relationship between categories and proofs, for example in the formerly intractable case of classical logic. The field of deduction modulo, which turns out to be very much in the spirit of deep inference, decreases our dependency on the syntactic presentation of functional objects, and brings us closer to their intrinsic nature, even from the computational point of view. After studying all those trees for years we at last have the impression of looking at the forest. The core topics are organised along the axis: algebraic semantics deduction of proofs deep inference modulo game semantics operads and specification <--> structads <--> proof nets proof search calculus of deductive structures implementations proof nets This workshop aims at being a meeting point for all those who are interested in decreasing the dependency of logic from low-level syntax. The list of topics above is not exhaustive: if you feel you can contribute to the discussion along the broad lines outlined above, please submit your contribution. SUBMISSION, IMPORTANT DATES AND PUBLICATION Contributions such as work in progress, programmatic/position papers, tutorials, as well as regular papers are more than welcome. We will favor the former over regular papers that seem to us to be minor contributions, although we will definitely not reject major contributions! Submissions should be formatted with the LNCS LaTeX style, and should not exceed fifteen pages, to allow the committee to assess their merits with reasonable effort. This limit can be relaxed for the versions that will be presented at the workshop, depending on the total bulk of the accepted contributions. Contributions should be submitted electronically; details will be provided soon. submission: 15.4.2005 notification: 22.5.2005 final version: 10.6.2005 The selected papers will be made public on the web for downloads. It goes without saying that authors will be able to keep their copyrights. The issue of printed proceedings is still under discussion. INVITED SPEAKERS Martin Hyland (Cambridge) Claude or Helene Kirchner (LORIA & INRIA Lorraine, Nancy) Dale Miller (INRIA Futurs and LIX, Paris) David Pym (Bath and HP Labs) PROGRAM COMMITTEE Paola Bruscoli (Dresden) Pietro Di Gianantonio (Udine) Gilles Dowek (LIX & Ecole Polytechnique, Paris) Roy Dyckhoff (St Andrews) Rajeev Gore' (NICTA and ANU, Canberra) Francois Lamarche (LORIA & INRIA Lorraine, Nancy) -- Chair Luke Ong (Oxford) Prakash Panangaden (McGill) Michel Parigot (CNRS, Paris) Charles Stewart (Dresden) Thomas Streicher (Darmstadt) LOCATION Lisbon, July 16-17, 2005; the workshop is a satellite of the ICALP 2005 conference. HOW TO REGISTER A registration fee for attending the workshop will be paid to the ICALP Workshop general chair; no fee for participating in the main conference should be necessary, while participation in both conference and workshop should entitle to special discounts. Please visit the ICALP web site for up-to-date, precise information: ORGANISERS Paola Bruscoli (Dresden) Francois Lamarche (LORIA & INRIA Lorraine, Nancy) -- Chair Charles Stewart (Dresden) 7-Jan-2005 11:11:48 -0400,2548;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 07 Jan 2005 11:11:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cmvft-0001Vu-00 for categories-list@mta.ca; Fri, 07 Jan 2005 11:05:13 -0400 Date: Wed, 5 Jan 2005 23:02:48 -0500 (EST) From: Phil Scott To: categories@mta.ca Subject: categories: Research Fellow/Postdoc (UOttawa) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Research Fellow/Postdoc positions in Logic and Computation, University of Ottawa The Logic Group in the Department of Mathematics and Statistics at the University of Ottawa is looking to hire at least one (maybe more) research fellows/postdocs beginning in July, 2005. The positions are in any area of category theory, categorical logic, and theoretical computer science. Research fellows / postdocs will participate in the activities of the Logic and Foundations of Computation Group. This group includes faculty and students from several different Ottawa-area universities. In the Math Department, the Logic Group currently includes 3 faculty members (R. Blute, P. Scott, P. Selinger), 3 postdocs, and 8 graduate students. For more information about our team, see http://www.mathstat.uottawa.ca/lfc/ The research fellowships/postdocs are initially for one year, with a possible renewal for a second year. Duties include research and the teaching of two one-semester courses. Potential applicants should contact one of us: Philip Scott (phil@site.uottawa.ca) Richard Blute (rblute@mathstat.uottawa.ca) Peter Selinger (selinger@mathstat.uottawa.ca) immediately by email to indicate their interest. They should then also send a curriculum vitae, a research plan, and arrange for three confidential letters of recommendation, with one addressing teaching, to be sent to Professor Mayer Alvo, Chairman, Department of Mathematics and Statistics, University of Ottawa, Ottawa, ON Canada, K1N 6N5. Applicants are also encouraged to include up to three copies of their most significant publications. Those who have already applied for a position will of course be considered and do not have to re-send an application. These positions depend upon a competition for limited funds, so early application is essential. P. Scott, R. Blute, and P. Selinger 9-Jan-2005 15:22:39 -0400,2411;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 09 Jan 2005 15:22:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CniWJ-0001J9-00 for categories-list@mta.ca; Sun, 09 Jan 2005 15:14:35 -0400 Message-ID: <41E0C2E5.9090200@cs.stanford.edu> Date: Sat, 08 Jan 2005 21:36:37 -0800 From: Vaughan Pratt Reply-To: pratt@cs.stanford.edu Organization: Stanford University User-Agent: Mozilla Thunderbird 0.9 (Windows/20041103) X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Coordinated names for two Boolean algebras Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Is there a coordinated pair of names for the Boolean algebra arising as the double-negation retract of a Heyting algebra H, and that arising as the completion of H to a Boolean algebra? I've been thinking of them as the interior and exterior Boolean algebras of H, but if there's a pair of names already in use, either specifically for this situation or for a situation that this is an instance of, established notation would be preferable provided it isn't too much longer than interior and exterior. Actually I only care about complete Heyting algebras, in fact profinite distributive lattices, in case that makes any difference. The Boolean algebra completing a profinite distributive lattice is clearly a CABA; unless I'm overlooking something it looks like the double-negation retract should be the powerset of the set of maximal filters of H and so a CABA too. If so, is there some principle that shows that both Boolean algebras have to be CABAs without a separate argument for each, assuming H is profinite? A quick skim through the Handbook of Boolean Algebras, Sikorski, and the Elephant, didn't turn up anything, but these things are easy to miss when you don't have Google to search them. While I'm on the question of names, here's a really elementary question I don't know the answer to. How acceptable is it to write \sum_J:C^J\to C instead of Colim:C^J\to C when J is not discrete? Is \sum always understood to connote discrete sum or is the usage \sum_J excusable? Seems like context should make the meaning clear when J is a category. Vaughan Pratt 9-Jan-2005 15:22:39 -0400,1631;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 09 Jan 2005 15:22:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CniXU-0001Lr-00 for categories-list@mta.ca; Sun, 09 Jan 2005 15:15:48 -0400 From: J=FCrgen Koslowski Message-Id: <200501091431.j09EVBO21544@lxt5.iti.cs.tu-bs.de> Subject: categories: potentially interesting link To: categories@mta.ca (categories list) Date: Sun, 9 Jan 2005 15:31:11 +0100 (CET) X-Mailer: ELM [version 2.5 PL6] MIME-Version: 1.0 Content-Type: text/plain; charset=3Dus-ascii X-Scanned-By: MIMEDefang 2.37 Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Dear colleagues, By accident I stumbled upon the thesis of Ralph Kroemer (in German) Die Kategorienetheorie: ihre mathematischen Leistungen, ihre erkentnistheoretischen Implikationen dated May 6, 2004. Some of you probably know this work, since you are explicitly mentioned in the Acknowledgements ;-) Some others with sufficient knowledge of German may be interested as well: http://www.univ-nancy2.fr/poincare/perso/kroemer/these-kroemer.pdf (445 pages). From my initial impression, this may be an important contribution. Best regards, and all the best for 2005 -- Juergen Koslowski --=20 Juergen Koslowski If I don't see you no more on this world ITI, TU Braunschweig I'll meet you on the next one koslowj@iti.cs.tu-bs.de and don't be late! http://www.iti.cs.tu-bs.de/~koslowj Jimi Hendrix (Voodoo Child, SR) 11-Jan-2005 13:05:22 -0400,4507;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:05:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPQH-0003av-00 for categories-list@mta.ca; Tue, 11 Jan 2005 13:03:13 -0400 Message-ID: <41E2DA74.10300@cs.stanford.edu> Date: Mon, 10 Jan 2005 11:41:40 -0800 From: Vaughan Pratt Reply-To: pratt@cs.stanford.edu Organization: Stanford University User-Agent: Mozilla Thunderbird 0.9 (Windows/20041103) X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Coordinated names for two Boolean algebras References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Dear Peter, Thanks for your very thought-provoking example. I'm having difficulty coming up with a direct description of the Booleanization of H. Is it the finite unions of principal filters no two of which are siblings? And which Boolean algebra is it? The free countably generated one? Vaughan Prof. Peter Johnstone wrote: > On Sat, 8 Jan 2005, Vaughan Pratt wrote: > > >>Is there a coordinated pair of names for the Boolean algebra arising as >>the double-negation retract of a Heyting algebra H, and that arising as >>the completion of H to a Boolean algebra? > > > I see no harm in calling the Ba of \neg\neg-stable elements the > Booleanization of H, since it is entirely analogous to the > Abelianization of a group. However, I'm not sure what Vaughan > means by "the completion of H to a Boolean algebra", since there > are several possible candidates for that title, and they don't > agree in general. > > If Vaughan is thinking of some construction that returns H itself > when H is already Boolean (for example, the Boolean algebra freely > generated by H qua lattice), then "completion" is a bad word to > use since such algebras won't in general be complete, even if H is. > For example, if H is a profinite distributive lattice, represented > as the poset of upper subsets of some poset P (Stone Spaces, VII > 3.4), then the corresponding Boolean algebra B consists of all > subsets of P which are (finite) lattice-theoretic combinations > of upper and lower sets, and this is in general not complete > (though it is atomic, since all singletons are in B). For example, > if P is the real line with its usual ordering, then B consists of > all subsets which are finite unions of intervals (using the word > "interval" in its broadest sense, to include singletons), and the > set of all singletons {q} with q rational has no least upper bound. > > Vaughan's comments suggest that he is thinking of a construction > which, when H = upper sets of P, returns the full power-set of > P. I'm not sure whether there is any such construction on > arbitrary (not necessarily complete) Heyting algebras, but for > complete Heyting algebras (frames) H one could take the Booleanization > of the assembly of H. Is that what Vaughan was thinking of? > > >>Actually I only care about complete Heyting algebras, in fact profinite >>distributive lattices, in case that makes any difference. The Boolean >>algebra completing a profinite distributive lattice is clearly a CABA; >>unless I'm overlooking something it looks like the double-negation >>retract should be the powerset of the set of maximal filters of H and so >>a CABA too. > > > No, it isn't: take H = upper sets of P, where P is the poset of finite > sequences of 0's and 1's, ordered by p \leq q iff p is an initial > segment of q. For this H, each principal upper set \uparrow(p) is > \neg\neg-stable, and there are no atoms in the Booleanization of H. > >>While I'm on the question of names, here's a really elementary question >>I don't know the answer to. How acceptable is it to write >>\sum_J:C^J\to C instead of Colim:C^J\to C when J is not discrete? >>Is \sum always understood to connote discrete sum or is the usage \sum_J >>excusable? Seems like context should make the meaning clear when J is a >>category. >> > > I wouldn't do it myself (any more than I'd use the product sign for > limits of non-discrete diagrams), but I don't have strong objections. > > Peter Johnstone > > 11-Jan-2005 13:05:22 -0400,8440;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:05:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPOt-0003U6-00 for categories-list@mta.ca; Tue, 11 Jan 2005 13:01:47 -0400 Message-ID: <41E296DC.8060605@swan.ac.uk> Date: Mon, 10 Jan 2005 14:53:16 +0000 From: Markus Roggenbach User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3.1) Gecko/2003042= Bcc: 5 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Final CFP: CALCO 2005 Content-Type: text/plain; charset=3DISO-8859-1; format=3Dflowed Content-Transfer-Encoding: 8bit X-SA-Exim-Mail-From: M.Roggenbach@swansea.ac.uk Sender: cat-dist@mta.ca Precedence: bulk We apologise if you receive multiple copies. *--------------------------------------------------------------------* * Final Call for Papers * * * * CALCO 2005 * * * * =091st Conference on Algebra and Coalgebra in Computer Science * * * * September 3-6, 2005, Swansea, Wales, UK * * * *--------------------------------------------------------------------* * Abstract submission : January 21, 2005 * * Technical paper submission: January 31, 2005 * * Author notification: April 11, 2005 * *--------------------------------------------------------------------* * http://www.cs.swan.ac.uk/calco/ * *--------------------------------------------------------------------* With the support of IFIP WG 1.3 on Foundations of System Specification CMCS - the International Workshop on Coalgebraic Methods in Computer Science, and WADT - the Workshop on Algebraic Development Techniques, are joining their forces and reputations into a new high level bi-annual conference. Starting in 2005, CALCO will bring 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. CALCO 2005 will be preceded by a CALCO Young Researchers Workshop, CALCO-jnr, dedicated to presentations by PhD students and by those who completed their doctoral studies within the past few years (see www.cs.swan.ac.uk/calco-jnr/ for details). Topics of Interest ------------------ We invite submission of technical papers that report 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 practise. We encourage submissions in topics included or related to those in the lists below. Algebras and coalgebras as mathematical objects: Automata and languages Categorical semantics Hybrid, probabilistic, and timed systems Inductive and coinductive methods Modal logics Relational systems and term rewriting Algebras and coalgebras in computer science: Abstract data types Algebraic and coalgebraic specification Calculi and models of concurrent, distributed, mobile, and context-aware computing Formal testing and quality assurance General systems theory and computational models (chemical, biological, etc) Generative programming and model-driven development Models, correctness and (re)configuration of hardware/middleware/architectures Re-engineering techniques (program transformation) Semantics of conceptual modelling methods and techniques Semantics of programming languages Validation and verification Submission Guidelines --------------------- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Proceedings will be published in the Springer LNCS series. Final papers will be no more than 15 pages long in the format specified by Springer. It is recommended that submissions adhere to that format and length (see at http://www.springer.de/comp/lncs/authors.html). Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Paper submissions will be made electronically at he conference web site. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of Theoretical Computer Science consisting of extended versions of selected papers will be produced after the conference if there are enough good papers that can be extended and revised to the standards of this journal. Invited Speakers ---------------- The so-far confirmed invited speakers for CALCO 05 are: * Samson Abramsky, Christopher Strachey Professor of Computer Science, University of Oxford, UK. * Vladimiro Sassone, Professor of Informatics, University of Sussex, UK. Important Dates (all in 2005) ----------------------------- Jan 21 Abstract submission due Jan 31 Technical paper submissions due April 11 Author notification May 30 Camera ready due Sept 3-6 CALCO technical programme Programme Committee ------------------- Jose Fiadeiro, University of Leicester, UK (co-chair) Jan Rutten, CWI & Free University Amsterdam, NL (co-chair) Luca Aceto, Aalborg University, DK, and Reykjav=EDk University, IS Jiri Adamek, University of Braunschweig, D Christel Baier, University of Bonn, D Michel Bidoit, CNRS, Cachan, F Jules Desharnais, Laval University, CAN Marie-Claude Gaudel, LRI-CNRS, Paris, F Reiko Heckel, University of Leicester, UK H.Peter Gumm, Philipps University, Marburg, D Ugo Montanari, University of Pisa, I Larry Moss, Indiana University, Bloomington, USA Peter Mosses, University of Wales Swansea, UK Fernando Orejas, Politechnical University Catalunia, Barcelona, E Francesco Parisi-Presicce, George Mason University, Fairfax, USA John Power, University of Edinburgh, UK Horst Reichel, Technical University Dresden, D Eugene Stark, Stony Brook University, New York, USA Andrzej Tarlecki, Warsaw University, PL John Tucker, University of Wales Swansea, UK Martin Wirsing, Ludwig-Maximilian University, Muenchen, D Steering Committee ------------------ Jiri Adamek, Nakagawa Ataru, Michel Bidoit, Jose Fiadeiro (co-chair), H.Peter Gumm, Bart Jacobs Hans- Jorg Kreowski, Ugo Montanari, Larry Moss, Peter Mosses, Fernando Orejas, Francesco Parisi-Presicce, John Power, Horst Reichel, Markus Roggenbach, Jan Rutten (co-chair), Andrzej Tarlecki Organising Committee -------------------- Neal Harman and Markus Roggenbach, University of Wales Swansea, UK Location and Organisation ------------------------- The City of Swansea dates from the 10th Century AD and is currently an expanding centre for high tech. industry. Swansea is located at the centre of the South Wales coastline, next to the Gower peninsula, renowned for its dramatic coastal scenery and beaches. The conference will be held on the Swansea University campus overlooking the sea. Accommodation will be available in newly built halls of residence and also in a small selection of good quality hotels. A full social programme drawing on the culture of the area will complement the scientific event. This CFP version dated: 10th January 2005. --=20 ------------------------------------------------------------------- Markus Roggenbach Phone +44-1792-51-3578 Dept. of Computer Science Fax +44-1792-295708 University of Wales Swansea M.Roggenbach@Swan.ac.uk Singleton Park http://www.cs.swan.ac.uk/~csmarkus Swansea SA2 8PP, United Kingdom -------------------------------------------------------------------- 11-Jan-2005 13:05:22 -0400,4227;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:05:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPRU-0003gN-00 for categories-list@mta.ca; Tue, 11 Jan 2005 13:04:28 -0400 Date: Tue, 11 Jan 2005 10:49:41 +0000 (GMT) From: "Prof. Peter Johnstone" To: Categories mailing list Subject: categories: Free Heyting semilattices Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-DPMMS-Scan-Signature: 3014769432642ca802df8a5b59fc1046 Sender: cat-dist@mta.ca Precedence: bulk Does anyone know of any work on the question: is the free Heyting semilattice (i.e. the free cartesian closed poset) on a finite set of generators always finite? Or, to put an equivalent question in terms more familiar to logicians: is the Lindenbaum algebra for the pure implicational calculus, with a finite number of primitive propositions, always finite? (Note that the two questions are equivalent, though not the same: although we have the operation of conjunction (= meet) as well as implication in a Heyting semilattice, any Heyting-semilattice term is expressible as a finite conjunction of terms involving only implication.) Of course, free Heyting algebras are wildly infinite; but the wildness seems to derive from the (lack of) interaction between disjunction and implication, so things ought to be better-behaved if you leave out the operation of disjunction. I have explicitly calculated the free Heyting semilattice on two generators: it turns out to have 18 elements, which is a lot smaller than I'd expected. (Even more bizarrely, it turns out to be self-dual as a poset: I append its Hasse diagram below, for anyone who's interested.) However, it seems fairly clear that the corresponding calculation with three generators is too large to be done by hand, and I can't see any "pattern" emerging from the two-generator one which might indicate why they should all be finite. It seems quite likely that someone has considered the problem before; so I'd be very grateful for any pointers to relevant literature. Peter Johnstone Here is the Hasse diagram for the free Heytng semilattice on {x,y}. Conventions: implication is denoted by juxtaposition, and binds more strongly than conjunction (denoted &). Iterated implications are associated from left to right -- that is, pqr denotes ((p => q) => r) -- unless otherwise parenthesized. (Interestingly, with these conventions there is only one element whose description requires the use of parentheses: it may be equivalently described as xy(yxx), xy(yxy), yx(xyx) or yx(xyy).) 1 /|\ / | \ / | \ / | \ / | \ / | \ yxyy xy(yxx) xyxx /|\ / \ /|\ / | \ / \ / | \ / | \/ \/ | \ / | /\ /\ | \ / | / \ / \ | \ / |/ \ / \| \ yx xyy yxyy&xyxx yxx xy |\ / \ /|\ / \ /| | \ / \ / | \ / \ / | | \/ \/ | \/ \/ | | /\ /\ | /\ /\ | | / \ / \ | / \ / \ | |/ \ / \|/ \ / \| xyx xyyx xyy&yxx yxxy yxy \ |\ / \ /| / \ | \ / \ / | / \ | \/ \/ | / \ | /\ /\ | / \ | / \ / \ | / \|/ \ / \|/ x xy&yx y \ | / \ | / \ | / \ | / \ | / \|/ x&y 11-Jan-2005 13:05:23 -0400,3879;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:05:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPO9-0003Q2-00 for categories-list@mta.ca; Tue, 11 Jan 2005 13:01:01 -0400 Date: Mon, 10 Jan 2005 11:58:52 +0000 (GMT) From: "Prof. Peter Johnstone" Reply-To: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Coordinated names for two Boolean algebras In-Reply-To: <41E0C2E5.9090200@cs.stanford.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk On Sat, 8 Jan 2005, Vaughan Pratt wrote: > Is there a coordinated pair of names for the Boolean algebra arising as > the double-negation retract of a Heyting algebra H, and that arising as > the completion of H to a Boolean algebra? I see no harm in calling the Ba of \neg\neg-stable elements the Booleanization of H, since it is entirely analogous to the Abelianization of a group. However, I'm not sure what Vaughan means by "the completion of H to a Boolean algebra", since there are several possible candidates for that title, and they don't agree in general. If Vaughan is thinking of some construction that returns H itself when H is already Boolean (for example, the Boolean algebra freely generated by H qua lattice), then "completion" is a bad word to use since such algebras won't in general be complete, even if H is. For example, if H is a profinite distributive lattice, represented as the poset of upper subsets of some poset P (Stone Spaces, VII 3.4), then the corresponding Boolean algebra B consists of all subsets of P which are (finite) lattice-theoretic combinations of upper and lower sets, and this is in general not complete (though it is atomic, since all singletons are in B). For example, if P is the real line with its usual ordering, then B consists of all subsets which are finite unions of intervals (using the word "interval" in its broadest sense, to include singletons), and the set of all singletons {q} with q rational has no least upper bound. Vaughan's comments suggest that he is thinking of a construction which, when H = upper sets of P, returns the full power-set of P. I'm not sure whether there is any such construction on arbitrary (not necessarily complete) Heyting algebras, but for complete Heyting algebras (frames) H one could take the Booleanization of the assembly of H. Is that what Vaughan was thinking of? > Actually I only care about complete Heyting algebras, in fact profinite > distributive lattices, in case that makes any difference. The Boolean > algebra completing a profinite distributive lattice is clearly a CABA; > unless I'm overlooking something it looks like the double-negation > retract should be the powerset of the set of maximal filters of H and so > a CABA too. No, it isn't: take H = upper sets of P, where P is the poset of finite sequences of 0's and 1's, ordered by p \leq q iff p is an initial segment of q. For this H, each principal upper set \uparrow(p) is \neg\neg-stable, and there are no atoms in the Booleanization of H. > > While I'm on the question of names, here's a really elementary question > I don't know the answer to. How acceptable is it to write > \sum_J:C^J\to C instead of Colim:C^J\to C when J is not discrete? > Is \sum always understood to connote discrete sum or is the usage \sum_J > excusable? Seems like context should make the meaning clear when J is a > category. > I wouldn't do it myself (any more than I'd use the product sign for limits of non-discrete diagrams), but I don't have strong objections. Peter Johnstone 11-Jan-2005 13:05:23 -0400,1339;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:05:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPMc-0003HW-00 for categories-list@mta.ca; Tue, 11 Jan 2005 12:59:26 -0400 Date: Sun, 09 Jan 2005 17:24:19 -0800 From: Vaughan Pratt Reply-To: pratt@cs.stanford.edu Organization: Stanford University User-Agent: Mozilla Thunderbird 0.9 (Windows/20041103) X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories list Subject: categories: Re: Coordinated names for two Boolean algebras References: <200501091431.j09EVBO21544@lxt5.iti.cs.tu-bs.de> In-Reply-To: <200501091431.j09EVBO21544@lxt5.iti.cs.tu-bs.de> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: (In case it wasn't clear from context, by "maximal filters of H" in > the double-negation retract should be the powerset of the set of > maximal filters of H and so a CABA too. I meant "maximal complete filters," in order to keep the topology discrete. That viewpoint incidentally makes the exterior Boolean algebra simply a matter of dropping "maximal".) Vaughan Pratt 11-Jan-2005 13:08:21 -0400,8206;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Jan 2005 13:08:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CoPV3-000417-00 for categories-list@mta.ca; Tue, 11 Jan 2005 13:08:09 -0400 Reply-To: From: "Iman Hafiz Poernomo" To: Subject: categories: CFP: CLASE at ETAPS deadline extension Date: Tue, 11 Jan 2005 13:09:52 -0000 Organization: Department of Computer Science, King's College London MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Dear colleague, I draw your attention to the following workshop at ETAPS 2005 in Edinburgh: Constructive Logic for Automated Software Engineering http://www.dcs.kcl.ac.uk/events/clase/ Please find the CFP attached. The title of the workshop sounds rather specific, but we are open to any kind of type theoretic/categorical/logic-based theories/methodologies/tools that could help make software construction more reliable. Due to several requests, it has been decided to move to paper submission deadline for CLASE to February 11th. This also gives you a chance to submit something! Long papers and abstracts can be submitted. After the workshop, papers will be published in a volume of Elsevier's ENTCS (abstracts can be extended for publication in this also). Publication of best papers is also expected to be given in a special issue of a major logic journal -- so it is well worth putting something in. The workshop promises to be an interesting one and we are lucky to have Alan Bundy as invited speaker -- so please forward this CFP to any colleagues who might be interested. Best wishes and happy New Year, Iman -------------- Iman Poernomo Lecturer Department of Computer Science King's College London iman@dcs.kcl.ac.uk CALL FOR PAPERS Constructive Logic for Automated Software Engineering (CLASE 2005) http://www.dcs.kcl.ac.uk/events/clase/ Satellite event of ETAPS 2005, Edinburgh, 3rd April 2005 Scope This workshop will provide an avenue for work that extends traditional methods that derive from constructive logic for synthesizing complex software. After more than 30 years of research, program synthesis using constructive logic constitutes a mature field with an established theory and set of best practices. Recent years have seen an interest in providing analogous results to other logical systems and programming languages. This workshop will bring together researchers and practitioners to share ideas on the foundations, techniques, tools, and applications of constructive logic and its methods to automated software engineering technology. This workshop will provide an avenue for work that extends traditional methods that derive from constructive logic for synthesizing complex software. Software engineering is concerned with processes and techniques for analysis, design, implementation, testing, and maintenance of software systems. Automated software engineering is concerned with computational techniques to automate these tasks (at least partially) in order to aid reliability, trustworthiness and productivity of code and of the engineering process itself. The application of constructive logic to small-scale functional program synthesis is well known. One pervasive idea is that the constructive content of a proof of a formula can be transformed into a functional program that satisfies the formula when the latter is regarded as a specification. Such work, based upon the Curry-Howard isomorphism and higher-order type theory, constitutes the area referred to as the proofs-as-programs paradigm. Other areas that are susceptible to the use of constructive logic include ? Type theory in general, ? Proof planning, ? Constructive tableaux, ? Labelled Deductive systems and hybrid logics in general, ? Deductive logic programming. The advantage of proofs-as-programs techniques is that the task of programming a function is reduced to reasoning with domain knowledge, transforming constructive proofs to a commonly used functional programming language that can encode a simply typed lambda calculus, such as SML, Scheme or Haskell. After more than 30 years of research, proofs-as-programs constitutes a mature field with an established theory and set of best practices. Recent years have seen an interest in providing analogous results to other logical systems and programming languages. This workshop will bring together researchers and practitioners to share ideas on the foundations, techniques, tools, and applications of constructive logic and its methods to automated software engineering technology. Topics We encourage submissions on techniques that involve constructive reasoning, analysis and synthesis for complex software engineering. Examples include: ? proofs-as-programs adapted to logics other than intuitionistic logic (e.g., linear logic, Hennesy-Milner specification systems, modal logic, temporal logic) ? proofs-as-programs for program synthesis in complex programming paradigms (e.g., distributed, object-oriented, component-based or embedded systems), ? constructive logics for semantic foundations of modelling and requirements languages, ? integration of ideas from constructive logic into software engineering process design, ? evaluative case studies of constructive methods for large scale system development, ? industrial strength, constructive synthesis, system implementations. Guest Speaker Alan Bundy, School of Informatics, University of Edinburgh, UK. Dates Submission deadline: 11th February 2005 Notification of acceptance/rejection: 21st February 2005 Final version: 28th February 2005 Submissions There are two kinds of submission accepted: short (no longer than 2 pages) and long (no longer than 10 pages) papers. Submissions should include author's full name(s), affiliation(s) and address(es), phone- and fax-number(s) and email address(es). Papers in PS or PDF-format should be emailed to the address iman 'at symbol' = dcs.kcl.ac.uk, with the subject heading "CLASE submission". All valid submissions will = be reviewed by at least two members of the program committee. Publication Final versions of accepted full papers are to be published in a special issue of the Electronic Notes in Computer Science (ENTCS). Authors of accepted short papers will have the opportunity to submit expanded versions of their papers for a second round of review for publication in the special issue. Organizing Committee Stuart F. Allen, sfa 'at symbol' cs.cornell.edu, Department of Computer Science, Cornell University, USA John Crossley, John.Crossley 'at symbol' infotech.monash.edu.au, School of Computer Science and Software Engineering, Monash University, Australia Kung-Kiu Lau, kung-kiu 'at symbol' cs.man.ac.uk, Department of Computer Science, University of Manchester, UK Iman Poernomo, iman 'at symbol' dcs.kcl.ac.uk, Department of Computer Science, King's College London, UK Program Committee Stuart F. Allen, Cornell University, USA Ulrich Berger, University of Wales Swansea, UK James Caldwell, University of Wyoming, USA Karl Crary, Carnegie Mellon University, USA John Crossley, Monash University, Australia Ewen Denney, University of Edinburgh, UK Raj Gore, Australian National University, Australia Douglas J. Howe, Carleton University, Canada Kung-Kiu Lau, University of Manchester, UK Mihhail Matskin, Royal Institute of Technology, Sweden Mario Ornaghi, Universita' degli studi di Milano, Italy Christine Paulin-Mohring, Universit=E9 Paris Sud, France Iman Poernomo, Monash University, Australia Anton Setzer, University of Wales Swansea, UK Alex Simpson, University of Edinburgh, UK Martin Wirsing, Ludwig-Maximilians Universit=E4t, Germany ------=_NextPart_000_073A_01C4F7DE.E8604480-- 12-Jan-2005 12:21:18 -0400,4350;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Jan 2005 12:21:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ColCK-0002LY-00 for categories-list@mta.ca; Wed, 12 Jan 2005 12:18:16 -0400 From: Todd Wilson Message-ID: <16868.7506.5762.455946@localhost.localdomain> Date: Tue, 11 Jan 2005 10:39:14 -0800 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: Categories mailing list Subject: categories: Re: Free Heyting semilattices In-Reply-To: References: X-Mailer: VM 7.17 under 21.4 (patch 14) "Reasonable Discussion" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk On Tue, 11 Jan 2005, Prof. Peter Johnstone wrote: > Does anyone know of any work on the question: is the free Heyting > semilattice (i.e. the free cartesian closed poset) on a finite set > of generators always finite? Yes, and the answer is yes. Algebras satisfying all of the implications true for Heyting algebras have been called "Hilbert algebras", and their local finiteness was first shown in A. Diego, "Sur les algebres de Hilbert", Gauthier-Villars, Paris, 1966, although there is also an apparently earlier article in Spanish that I have not been able to get, A. Diego, "Sobre algebras de Hilbert", Notas de Logica Mathematica 26, Instituto de Matematica, Universidad Nacional del Sur, Bahia Blanca, 1965, that may be the same, or very similar. Better bounds on the size of free Hilbert algebras and a better construction of them can be found in A. Urquhart, "Implicational formulas in intuitionistic logic", JSL 39 (4), 1974, p. 661-664. Rasiowa discusses these algebras, under the name "positive implication algebras", in her book H. Rasiowa, An algebraic approach to non-classical logics, Studies in Logic and the Foundations of Mathematics, V. 78, North-Holland, 1974, referring to Diego and proving his representation theorem that every Hilbert algebra is a subalgebra of the Hilbert algebra of open sets of a topological space (the points are the binary-intersection-irreducible filters, appropriately defined). She also refers to J. C. Abbott, "Semi-boolean algebras", Matematicki Vesnik, 4 (1967), pp. 177-198. for the theory of "implication algebras" (all the implications true in Boolean algebras). Another important reference is the technical report N. G. De Bruijn, "Exact finite models for minimal propositional calculus over a finite alphabet." TR 75-WSK-02, Technological University Eindhoven, Netherlands, Department of Mathematics, February 1975. which deals with Heyting semilattices. De Bruijn also cites Diego and Urquhart, commenting: It was only after the completion of this paper that the author learned that proofs for the finiteness of the number of classes had been given by [Diego, Urquhart]. Both authors showed the finiteness for the case without conjunction, but the finiteness of the case with conjunction is a simple consequence. The present approach is very different; as a matter of fact our treatment shows that it is profitable to study the case of implication plus conjunction, since this reveals so much more of the structure. De Bruijn shows that free finitely generated Heyting semilattices are finite topological spaces (thus Kripke models), and he displays the cases n = 1,2,3 explicitly (with 1, 5, and 61 points), and calculates their cardinalities: |HS(1)| = 2 |HS(2)| = 18 |HS(3)| = 623,662,965,552,330 The general case is handled by a recursive construction. He says, of the sequence of cardinalities, a_1, a_2, a_3, ..., that "It can be expected that log a_(n+1) is of the order of a_n", so their sizes, though finite, become incomprehensible quite quickly. -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh 12-Jan-2005 12:21:18 -0400,2592;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Jan 2005 12:21:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ColEP-0002Tl-00 for categories-list@mta.ca; Wed, 12 Jan 2005 12:20:25 -0400 Date: Wed, 12 Jan 2005 15:26:43 +0100 Message-Id: <200501121426.j0CEQhMA018987@mercurio.srv.dsi.unimi.it> X-Sender: ghilardi@pop.dsi.unimi.it X-Mailer: QUALCOMM Windows Eudora Pro Versione 4.0.1 Data: Wed, 12 Jan 2005 15:29:49 +0100 To: categories@mta.ca From: Silvio Ghilardi Subject: categories: Re: Free Heyting semilattices In-Reply-To: Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk >Does anyone know of any work on the question: is the free Heyting >semilattice (i.e. the free cartesian closed poset) on a finite set >of generators always finite? Or, to put an equivalent question in >terms more familiar to logicians: is the Lindenbaum algebra for the >pure implicational calculus, with a finite number of primitive >propositions, always finite? (Note that the two questions are >equivalent, though not the same: although we have the operation of >conjunction (=3D meet) as well as implication in a Heyting semilattice, >any Heyting-semilattice term is expressible as a finite conjunction >of terms involving only implication.) > The answer is yes, it is Diego-McKay theorem: semilattices with implication (usually called Brouwerian semilattices) are a locally finite variety; in other words, there are only finitely many intuitionistically non-equivalent propositional formulas built up from finitely many propositional letters, conjunction and implication. For a quick algebraic proof of this fact, see p.107 in P. Kohler "Brouwerian semilattices", Trans. Amer. Math. Soc., vol. 268, n.1, (1981), pp.103-126 The same paper describes a duality for finite brouwerian semilattices and gives some cardinality=20 information on p.118 for n-generated free algebras (bounds are very large: on 3 generators there are 623, 662, 965, 552, 330 elements !!!!! ).=20 silvio ghilardi Silvio Ghilardi Professor in Logic Dipartimento di Scienze dell'Informazione Universit=E0 degli Studi di Milano via Comelico 39 20135 Milano, Italy e-mail: ghilardi@dsi.unimi.it tel: +39/0250316217 fax:+39/0250316373 web-page: http://homes.dsi.unimi.it/~ghilardi/ 12-Jan-2005 12:21:18 -0400,1744;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Jan 2005 12:21:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ColDY-0002QT-00 for categories-list@mta.ca; Wed, 12 Jan 2005 12:19:32 -0400 Date: Tue, 11 Jan 2005 18:09:09 -0800 From: Vaughan Pratt Reply-To: pratt@cs.stanford.edu Organization: Stanford University User-Agent: Mozilla Thunderbird 0.9 (Windows/20041103) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Categories mailing list Subject: categories: Re: Free Heyting semilattices References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: > However, it seems > fairly clear that the corresponding calculation with three generators > is too large to be done by hand, and I can't see any "pattern" > emerging from the two-generator one which might indicate why they > should all be finite. I see a pattern that very strongly inclines me to the conjecture that they are all finite. Peter's poset is simply the product of three chains, 2 x 3 x 3. One rarely sees that kind of regularity in a combinatorial enumeration that blows up to infinity at some finite point. The one-generator chain being simply 2 (1 and x), the question then becomes, what's the next element in the sequence 2, 2 x 3 x 3, ...? I'd like to see one more term before going out on a limb here. :) Vaughan Pratt 12-Jan-2005 12:21:18 -0400,2004;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Jan 2005 12:21:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ColCs-0002Nq-00 for categories-list@mta.ca; Wed, 12 Jan 2005 12:18:50 -0400 Date: Tue, 11 Jan 2005 15:30:39 -0500 (EST) From: Peter Freyd Message-Id: <200501112030.j0BKUdNX011125@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Re: Free Heyting semilattices Sender: cat-dist@mta.ca Precedence: bulk Yes, finitely generated Heyting semilattices are finite. My proof is recorded in the dissertation of one Samuel Johnson from the 70s. I suspect that it had many earlier proofs. My proof is as follows: For any equational theory (with a finite number of primitive operations) to show that the free algebra on n generators is finite it suffices to show that there is a (finite) upper bound on the size of subdirectly irreducible algebras on n generators. For HSLs, subdirect irreducibility is equivalent to a unique maximal element below 1. I'll denote the element M. I like to call these "local HSLs". (For examples, take any non-trivial topological space and any point x therein; identify open sets if they are locally equivalent at x, that is if their intersections with an open nhbd of x are equal; the HA of equivalent class is local -- M is named by the complement of the closure of {x}). If we remove M from a local HSL, the result is still an HSL (clearly M is not the meet of two things in the complement, and -- perhaps not quite so clearly -- M is not the result of x -> y for x and y in the complement, indeed M = x -> y iff x = 1 and y = M). Hence if a local HSL is generated by n of its elements, then its complement is necessarily generated by n-1 of its elements. Hence a a local HSL has at most K+1 elements where K is the number of elements in the free HSL on n generators. Done. 12-Jan-2005 12:21:18 -0400,1002;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Jan 2005 12:21:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ColAq-0002De-00 for categories-list@mta.ca; Wed, 12 Jan 2005 12:16:44 -0400 Mime-Version: 1.0 (Apple Message framework v612) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <3904A28A-63F6-11D9-B7BA-000393DAA298@pps.jussieu.fr> Content-Transfer-Encoding: 7bit From: Curien Pierre-Louis Subject: categories: Goedel prize 2005 Date: Tue, 11 Jan 2005 18:28:35 +0100 To: concurrency@cwi.nl, categories@mta.ca, types@cis.upenn.edu Sender: cat-dist@mta.ca Precedence: bulk I'd like to draw your attention on the call for nominations for GOEDEL Prize 2005 (deadline January 31) All information on the nomination process can be found on the following url: http://sigact.acm.org/prizes/godel/ Best regards, Pierre-Louis 13-Jan-2005 14:16:16 -0400,2674;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Jan 2005 14:16:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cp9Oz-0004xA-00 for categories-list@mta.ca; Thu, 13 Jan 2005 14:08:57 -0400 Date: Wed, 12 Jan 2005 13:21:11 -0500 (EST) From: Peter Freyd Message-Id: <200501121821.j0CILAjD014038@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Re: Free Heyting semilattices Sender: cat-dist@mta.ca Precedence: bulk Since we're on the subject, say that a Heyting semi-lattice (sometimes Hilbert algebra) is LINEAR if it satisfies the further equation: ((x -> y) -> z) ^ ((y -> x) -> z) = z The prime examples are totally ordered sets (where, necessarily, x -> y = if y < x then y else 1). One may prove that every linear HSL is isomorphic to a subalgebra of a cartesian product of totally ordered HSLs. One may then prove that every linear HSL is, in fact, a Heyting algebra: the join operation is constructible as: ((x -> y) -> y) ^ ((y -> x) -> x) The proof is easy: first verify that this term yields the join of x and y in any totally ordered HSL; second realize that it therefore necessarily satisfies the axioms for a join operation (with respect to the given meet operation) in every totally ordered HSL; third note that the representation theorem says that such must be the case in every linear HSL. There's a nice converse: a variety of HSLs all of whose members are Heyting algebras is necessarily a variety of linear HSLs. (And it's not hard to find all such varieties.) Anyway, it is possible to count the number of elements in free linear HSLs. You can find the following on Neil Sloane's Encyclopedia of Integer Sequences: ID Number: A067765 URL: http://www.research.att.com/projects/OEIS?Anum=A067765 Sequence: 1,2,18,370386,143436460933743129632865858558642 Name: Order of linear Heyting semi-lattice on n points. References P. J. Freyd, On the size of Heyting semi-lattices, preprint, 2002. Formula: a(0)=1; for n>0, a(n) = product((1+a(r))^binomial(n,r),r=0..n-1). Maple: A067765 := proc(n) option remember; if n=0 then 1 else mul((1+A067765(r))^binomial(n,r),r=0..n-1); fi; end; See also: Sequence in context: A059783 A066361 A007184 this_sequence A086367 A059706 A096481 Adjacent sequences: A067762 A067763 A067764 this_sequence A067766 A067767 A067768 Author(s): Peter Freyd (pjf(AT)saul.cis.upenn.edu), Feb 07 2002 Extension: The next term is too large to include. 18-Jan-2005 13:32:32 -0400,1956;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Jan 2005 13:32:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cqx7A-0000k9-00 for categories-list@mta.ca; Tue, 18 Jan 2005 13:26:00 -0400 Date: Mon, 17 Jan 2005 15:28:56 +0000 From: Oliver Kullmann To: categories@mta.ca Subject: categories: elementary facts on categories of categories and functors?! Message-ID: <20050117152856.GB23434@cs-wsok.swansea.ac.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.6i Sender: cat-dist@mta.ca Precedence: bulk Hello, considering the category of categories, either with functors or with natural transformations as morphisms, or categories of functors with natural transformations as morphisms, it seems very likely to me that the basic questions like: -- what are the mono's, epi's, extreme mono's, extreme epi's etc. ? -- constant morphisms, initial and terminal objects etc. ? -- existence of limits and colimits ? have all been answered for these categories. But in the books known to me only very few facts are given. I started answering these questions myself, but some (like the characterisation of monomorphic functors or monomorphic natural transformations) seem not completely trivial to me. So my question: Could somebody tell me about sources regarding these basic considerations?! (I'm an outsider to category theory, and perhaps there are sources known to everybody in the list, but not to me; I would be glad for any help. Especially I would like to see any kind of an encyclopaedic source for category theory.) Thanks for your help in any case! Oliver -- Dr. Oliver Kullmann Computer Science Department University of Wales Swansea Faraday Building, Singleton Park Swansea SA2 8PP, UK http://cs-svr1.swan.ac.uk/~csoliver/ 18-Jan-2005 13:32:32 -0400,1108;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Jan 2005 13:32:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cqx8f-0000qL-00 for categories-list@mta.ca; Tue, 18 Jan 2005 13:27:33 -0400 Date: Tue, 18 Jan 2005 13:08:51 +0000 (GMT) From: "Prof. Peter Johnstone" To: Categories mailing list Subject: categories: Re: Heyting semilattices again In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-DPMMS-Scan-Signature: cd92b554eb07c34b23e8fc4651166fdf Sender: cat-dist@mta.ca Precedence: bulk Apologies: I've just rechecked my working and found a mistake. The actual number of Mal'cev operations in the theory of Heyting semilattices is 603 = 3 x 201. So the appearance of the prime 163 was illusory (and it wasn't Eddington's favourite prime anyway: that was 137). Peter Johnstone 18-Jan-2005 13:32:33 -0400,1608;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Jan 2005 13:32:33 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1Cqx89-0000nh-00 for categories-list@mta.ca; Tue, 18 Jan 2005 13:27:01 -0400 Date: Tue, 18 Jan 2005 12:24:54 +0000 (GMT) From: "Prof. Peter Johnstone" To: Categories mailing list Subject: categories: Heyting semilattices again Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-DPMMS-Scan-Signature: 6f1923d5823a84ebbf9364e906eb30a5 Sender: cat-dist@mta.ca Precedence: bulk Many thanks to the people who pointed me in the direction of the literature on free Heyting semilattices. With its help, I have now managed to answer the question that led me to think about them in the first place: There are exactly 489 different Mal'cev operations in the theory of Heyting semilattices. (There are infinitely many in Heyting algebras, and I had idly wondered whether the same might be true if you leave out disjunction.) Note that 489 = 3 x 163: this is not a coincidence, though why Eddington's favourite prime appears in this context I don't know. Rather to my surprise, there is only one Pixley operation (that is, a Mal'cev operation p satisfying the additional equation p(x,y,x) = y). There are many different ways of describing it, but they all turn out to be equal as members of the free Heyting semilattice HS(3). Peter Johnstone 20-Jan-2005 15:07:43 -0400,2069;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Jan 2005 15:07:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CrhaZ-0003yj-00 for categories-list@mta.ca; Thu, 20 Jan 2005 15:03:27 -0400 From: Organization: FernUniversitaet To: categories@mta.ca Date: Thu, 20 Jan 2005 11:57:48 +0200 MIME-Version: 1.0 Content-type: text/plain; charset=ISO-8859-1 Content-transfer-encoding: Quoted-printable Subject: categories: Re: A question for topos theorists. Message-ID: <41EF9CBC.31471.CC2533@localhost> Sender: cat-dist@mta.ca Precedence: bulk Datum: Mon, 27 Dec 2004 19:06:52 +0100 Betreff: categories: A question for topos theorists. Von: jean benabou An: Categories > I have recently come across a question, which seems to me natural, and > before trying to solve it, I wanted to know if an answer was already > known. > > If E is a category with pullbacks so is the category Cat(E) having as > objects the internal categories of E and and as maps the internal > functors F: A ---> B. I shall say that such an F is a "Pi-functor" if > the pullback functor: Cat(E)/B --->Cat(E)/A has a right adjoint Pi/F: > Cat(E)/A---->Cat(E)/B > > When E=3DSet there is a well known Conduch=E9-Giraud condition > characterizing such functors. Is there such a characterization when E > is an (elementary) topos? If there is, what is the condition and where > can it be found? > > Best wishes to all, Jean > > > Dear Jean, Let me draw your attention to the the paper by Phil Heath and myself P.R.Heath, K.H.Kamps Lifting colimits of (topological) groupoids and (topological) categories. Categorical topology and its relations to analysis, algebra and combinatorics : Proceedings, Prague 1988, World Sci. Publishing, Teaneck, NJ, 54-88 (1989). where a related problem on Pi-functors has been dealt with. With best wishes, Heiner. 20-Jan-2005 15:07:43 -0400,1221;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Jan 2005 15:07:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CrhXo-0003kt-00 for categories-list@mta.ca; Thu, 20 Jan 2005 15:00:36 -0400 To: vardi@cs.rice.edu Subject: categories: A Special Programme on Logic and Algorithm Message-Id: <20050119143105.7390C4AB58@cs.rice.edu> Date: Wed, 19 Jan 2005 08:31:05 -0600 (CST) From: vardi@cs.rice.edu (Moshe Vardi) X-Virus-Scanned: by amavis-20030616-p7 at cs.rice.edu X-Spam-Status: No, hits=- tagged_above=-999.0 required=6.9 WHITELISTED Sender: cat-dist@mta.ca Precedence: bulk The Isaac Newton Institute for Mathematical Science in Cambridge, UK (http://www.newton.cam.ac.uk/) will hold a Special Programme on Logic and Algorithms (LAA) during the first half of 2006. A brief statement on the programme's focus areas can be seen at http://www.newton.cam.ac.uk/programmes/LAA/. For a list of workshops, see http://www.newton.cam.ac.uk/programmes/LAA/ws.html. To receive further announcements on LAA events, see instructions at http://www.newton.cam.ac.uk/programmes/LAA/list.html. Anuj Dawar and Moshe Y. Vardi 20-Jan-2005 15:07:43 -0400,959;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Jan 2005 15:07:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CrhYG-0003n0-00 for categories-list@mta.ca; Thu, 20 Jan 2005 15:01:04 -0400 Date: Wed, 19 Jan 2005 15:18:20 +0000 (GMT) From: Bob Coecke To: Subject: categories: Quantale workshop this Friday in Oxford. Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk For those of you in the Oxford, London, English midlands area, or elsewere, there will be a workshop this Friday (the 21st) on Logic from Quantales in Oxford. Please check: http://se10.comlab.ox.ac.uk:8080/InformaticPhenomena/LogicfromQuantales_en.html for the program, directions etc. Best wishes, Bob. 25-Jan-2005 11:57:36 -0400,4861;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 25 Jan 2005 11:57:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CtSy8-0001ne-00 for categories-list@mta.ca; Tue, 25 Jan 2005 11:51:04 -0400 Mime-Version: 1.0 (Apple Message framework v619) Message-Id: Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Renaud Marlet Subject: categories: CFP Student session LACL 2005 Date: Tue, 25 Jan 2005 10:15:31 +0100 X-Mailer: Apple Mail (2.619) To: undisclosed-recipients: ; X-Virus-Scanned: amavisd-new at u-bordeaux1.fr Sender: cat-dist@mta.ca Precedence: bulk Call for papers ***************************************************** Student Session - LACL'2005 Logical Aspects of Computational Linguistics ***************************************************** Deadline : March 15, 2005 LACL'2005 is the 5th edition of a series of international conferences on logical and formal methods in computational linguistics. It addresses in particular the use of proof theoretic and model theoretic methods for describing natural language syntax and semantics, as well as the implementation of natural language processing software relying on such models. *** STUDENT SESSION *** For the first time, LACL'2005 will feature a student session. Students (not having defended yet their PhD thesis or defending it in 2005) are invited to submit short papers (2 or 3 pages) on the same topics as LACL. Submitted papers may present only partial but promising work. This student session offers a good opportunity for students to acquaint themselves with the world of research : digest writing exercise, feedback from the program committee, oral presentation exercise, feedback from LACL attendants. Students whose articles will be selected for the student session will benefit from reduced registration fees for the LACL conference. *** PAPER SELECTION *** Submitted articles will be reviewed by a program committee made of a a group of experienced researcher as well as a group of chosen PhD students. Each article will be reviewed by at least one experienced researcher and one of these PhD students. *** PAPER PRESENTATION *** Students whose papers will be selected will present their work in a poster session at the LACL conference. The papers will also be grouped and edited as an INRIA research report. *** TOPICS *** Computer scientists, linguists, mathematicians and philosophers are invited to present their work on the use of logical methods in computational linguistics and natural language processing, in natural language analysis, generation or acquisition. * LOGICAL FOUNDATIONS OF SYNTACTIC FORMALISMS: - categorial grammars, - minimalist grammars, - dependency grammars, - tree adjoining grammars, - model theoretic syntax, - formal language theory for natural language processing, - data-driven approaches, * LOGIC FOR SEMANTICS OF LEXICAL ITEMS, SENTENCES, DISCOURSE AND DIALOG: - discourse representation theory, - Montague semantics, - compositionality, - dynamic logic, - game semantics, - situation semantics, - generative lexicon, * APPLICATIONS OF THESE MODELS TO NATURAL LANGUAGE PROCESSING: - software for natural language analysis, - software for acquiring linguistic resources, - software for natural language generation, - software for information extraction, - question answering and human computer interaction in natural language, - evaluation and scalability *** SUBMISSION FORMAT *** Papers are be 2 to 3 pages long, including bibliography and possible figures and appendices. Articles, in PDF format, should be sent by email to lacl@labri.fr, with the keywords "student session" in the mail subject. *** IMPORTANT DATES *** - Paper submission deadline : March 15th, 2005 - Notification of acceptance : March 31st, 2005 - Camera-ready papers due : April 15th, 2005 - Student session : during LACL (April 28-30th, 2005) *** SCIENTIFIC INQUIRIES *** - Philippe Blache, blache@lpl.univ-aix.fr - Edward Stabler, stabler@ucla.edu *** PRACTICAL INQUIRIES *** - Renaud Marlet, marlet@labri.fr - Maxime Amblard, amblard@labri.fr *** PROGRAM COMMITTEE *** Ph. Blache, E. Stabler (chairs), members of the LACL 2005 program committee, group of chosen PhD students (in the course of being defined). *** ORGANIZING COMMITTEE *** R. Marlet, M. Amblard, J. Busquets, R. Moot *** MORE DETAILS *** http://lacl.labri.fr/student-session (at work) 25-Jan-2005 11:57:37 -0400,4662;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 25 Jan 2005 11:57:37 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CtSxG-0001iu-00 for categories-list@mta.ca; Tue, 25 Jan 2005 11:50:10 -0400 Date: Mon, 24 Jan 2005 16:12:50 +0000 (GMT) From: Andrzej Murawski To: Andrzej Murawski Subject: categories: CSL'05 - Second Call for Papers Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=X-UNKNOWN Content-Transfer-Encoding: QUOTED-PRINTABLE Sender: cat-dist@mta.ca Precedence: bulk CALL FOR PAPERS CSL'05, University of Oxford, 22-25 August 2005 http://web.comlab.ox.ac.uk/oucl/conferences/CSL05/ THE EVENT Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The 14th Annual Conference (and 19th International Workshop), CSL2005, will take place in the week 22 - 25 August 2005; it will be organised by the Computing Laboratory at the University of Oxford. SCOPE The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested topics of interest include: automated deduction and interactive theorem proving, constructive mathematics and type theory, equational logic and term rewriting, modal and temporal logic, model checking, logical aspects of computational complexity, finite model theory, computational proof theory, logic programming and constraints, lambda calculus and combinatory logic, categorical logic and topological semantics, domain theory, database theory, specification, extraction and transformation of programs, logical foundations of programming paradigms, linear logic, higher-order logic. INVITED SPEAKERS Matthias Baaz (U. of Technology, Vienna) Ulrich Berger (U. of Wales, Swansea) Maarten Marx (U. of Amsterdam) Anatol Slissenko (Universit=E9 Paris 12) SUBMISSION The proceedings will be published in the Springer Lecture Notes in Computer Science. Papers accepted by the Programme Committee must be presented at the conference by one of the authors, and final copy prepared according to Springer's guidelines. Submitted papers must be in Springer's LNCS style and of no more than 15 pages, presenting work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. The PC chair should be informed of closely related work submitted to a conference or journal by 1 April 2005. Papers authored or coauthored by members of the Programme Committee are not allowed. Submitted papers must be in English and provide sufficient detail to allow the programme committee to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewer's discretion. The title page must contain: title and author(s), physical and e-mail addresses, identification of the corresponding author, an abstract of no more than 200 words, and a list of keywords. IMPORTANT DATES Deadline for abstracts 25 March, 2005 Deadline for papers=09 1 April, 2005 Notification=09=09 15 May, 2005 Final versions due=09 1 June, 2005 ACKERMANN AWARD The EACSL Board has decided to launch the Ackermann Award: The EACSL Outstanding Dissertation Award for Logic in Computer Science. The first awards will be presented to the recipients at CSL'05. Further details of the Award can be found at =09 http://www.dimi.uniud.it/~eacsl/award.html PROGRAMME COMMITTEE Albert Atserias (Universitat Polit=E8cnica de Catalunya) David Basin (Eidgen=F6ssische Technische Hochschule Z=FCrich) Martin Escardo (U. of Birmingham) Martin Grohe (Humboldt-Universitat zu Berlin) Ryu Hasegawa (U. of Tokyo) Martin Hofmann (Ludwig-Maximilians-Universit=E4t M=FCnchen) Ulrich Kohlenbach (Darmstadt U. of Technology) Orna Kupferman (Hebrew U. of Jerusalem) Paul-Andre Mellies (CNRS / Universit=E9 Paris 7) Aart Middeldorp (U. of Innsbruck, Austria) Dale Miller (INRIA / Ecole Polytechnique) Damian Niwinski (U. of Warsaw) Peter O'Hearn (Queen Mary, U. of London) Luke Ong (U. of Oxford, Chair) Alexander Rabinovich (U. of Tel Aviv) Thomas Schwentick (Philipps-Universit=E4t Marburg) Alex Simpson (U. of Edinburgh) Nicolai Vorobjov (U. of Bath) Andrei Voronkov (U. of Manchester) 26-Jan-2005 11:48:51 -0400,1731;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 26 Jan 2005 11:48:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CtpIj-0007DK-00 for categories-list@mta.ca; Wed, 26 Jan 2005 11:41:49 -0400 Date: Wed, 26 Jan 2005 13:41:36 +0100 From: Jiri Rosicky To: categories@mta.ca Subject: categories: PhD positions Message-ID: <20050126124136.GA31813@queen.math.muni.cz> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-2 Content-Disposition: inline User-Agent: Mutt/1.4.1i X-Muni-Envelope-From: rosicky@math.muni.cz X-Muni-Virus-Test: Clean Sender: cat-dist@mta.ca Precedence: bulk The Department of Algebra and Geometry at the Masaryk University, Brno, Czech Republic, announces free PhD positions. The scholarships are available for three years, beginning in October 2005. They cover modest living expenses and are supported by the project `Algebra and geometry: the reunion and trends in current Mathematics' of the Grant Agency of the Czech Republic. The research topics are: category theory, algebraic number theory, semigroups and languages, differential geometry, global analysis, algebraic topology. Possible supervisors include: J.Rosicky, R.Kucera, L.Polak, J.Slovak, M.Cadek, J.Janyska. The closing date for applications is April 15, 2005. The study will begin in September 2005. Further basic information on the project is available at www.math.muni.cz/~slovak/phd-grant, the web pages of the Masaryk University are at http://www.muni.cz/to.en/, or http://www.muni.cz/to.en/misc/about.html (including a short Euro News profile http://wwwdata.muni.cz/to.en/media/video_mu.avi). 28-Jan-2005 17:09:36 -0400,5292;000000000000-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Jan 2005 17:09:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CudFy-0004OE-00 for categories-list@mta.ca; Fri, 28 Jan 2005 17:02:18 -0400 Mime-Version: 1.0 (Apple Message framework v619.2) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: Content-Transfer-Encoding: 7bit From: Michael Mislove Subject: categories: MFPS Final Call for Papers Date: Fri, 28 Jan 2005 12:53:11 -0600 To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Dear Colleagues, Below is the Final Call for Papers for MFPS 21, which will take place at the University of Birmingham, UK from Wednesday, May 18 through Saturday, May 21, 2005. Best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== Final Call for Papers MFPS XXI Twenty-first Conference on the Mathematical Foundations of Programming Semantics University of Birmingham Edgbaston, Birmingham UK May 18 - May 21, 2005 Partially Supported by US Office of Naval Research The Twenty-first Conference on the Mathematical Foundations of Programming Semantics will take place at the University of Birmingham, UK from Wednesday, May 18 through Saturday, May 21, 2005. The invited speakers for MFPS XXI are Samson Abramsky, Oxford Andrej Bauer, IMFM, Slovenia Roberto Gorrieri, Bologna Cliff Jones, Newcastle Catuscia Palamidessi, INRIA Gordon Plotkin, Edinburgh John Reynolds, CMU In addition to the invited addresses, there will be three special sessions: o Special Session on Quantum Computing organized by Samson Abramsky, Michael Mislove (Tulane) and Prakash Panangaden (McGill). o Special Session on Security organized by Catherine Meadows (NRL) o Special Session on Domain Theory and Topology, organized by Martin Escardo and Achim Jung (Birmingham). The remainder of the program will be composed of papers selected by the Program Committee from submissions received in response to this Call for Papers. The Program Committee is being chaired by Martin Escardo (Birmingham). It also includes: o Ulrich Berger, Swansea o Lars Birkedal, ITU, Denmark o Stephen Brookes, CMU o Thierry Coquand, Goteberg o Pierre-Louis Curien, LIAFA, Paris VII o Vincent Danos, Paris o Marcelo Fiore, Cambridge o Achim Jung Birmingham, U.K. o Catherine Meadows, NRL o Michael Mislove, Tulane o Luke Ong, Oxford o Prakash Panangaden, McGill o Brigitte Pientka, McGill o Phil Scott, Ottawa o Roberto Segala, Verona o Alex Simpson, Edinburgh o James Worrell, Tulane o Steve Zdancewic, Penn Submissions should consist of original work that has not been published elsewhere. Submissions should be no longer than 12 pages, and they should be in the form of either PostScript or pdf files that can be printed on a standard printer. They can be made using the link that is available on the MFPS 21 Home Page http://www.math.tulane.edu/~mfps/mfps21.htm Submissions must be received by midnight, Pacific Standard Time on Friday, February 15, 2005. Authors will be notified of acceptance by March 25, 2005. The conference Proceedings will appear as a volume of the Electronic Notes on Theoretical Computer Science. Information about proper formatting of submissions for the Proceedings will accompany the notices of acceptance. Information about ENTCS is available at http://www.elsevier.com/locate/entcs The MFPS conferences are devoted to those areas of mathematics, logic and computer science which are related to the semantics of programming languages. The series particularly has stressed providing a forum where both mathematicians and computer scientists can meet and exchange ideas about problems of common interest. We also encourage participation by researchers in neighboring areas, since we strive to maintain breadth in the scope of the series. The Organizing Committee for MFPS consists of Stephen Brookes (CMU), Achim Jung (Birmingham), Catherine Meadows (NRL), Michael Mislove (Tulane) and Prakash Panangaden (McGill). The local arrangements for MFPS XXI are being overseen by Achim Jung. In addition to supporting the conference overall, the support we anticipate from the Office of Naval Research makes funds available to help offset expenses of graduate students. Women and minorities also are encouraged to inquire about possible support to attend the meeting. Participation Information Further information about MFPS XXI can be found at the URL http://www.math.tulane.edu/~mfps/mfps21.htm Registration information will be available at these sites shortly after the list of accepted papers is available. If you have problems accessing the link above, then send email to mfps@math.tulane.edu. 30-Jan-2005 16:49:19 -0400,24236;000000000001-00000000 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 30 Jan 2005 16:49:19 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1CvLsK-0001sr-00 for categories-list@mta.ca; Sun, 30 Jan 2005 16:40:52 -0400 Message-Id: <200501300006.j0U06mM16668@math-cl-n03.ucr.edu> Subject: categories: Gerbes To: categories@mta.ca (categories) Date: Sat, 29 Jan 2005 16:06:47 -0800 (PST) From: "John Baez" X-Mailer: ELM [version 2.5 PL6] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Dear Categorists - I thought some of you might enjoy the material here on Larry Breen's conference, and on gerbes. Best, jb ...................................................................... Also available at http://math.ucr.edu/home/baez/week210.html January 25, 2005 This Week's Finds in Mathematical Physics - Week 210 John Baez As you've probably heard, the Huygens probe has successfully landed on Saturn's moon Titan and is sending back pictures: 1) Huygens Probe Descent http://saturn.jpl.nasa.gov/news/events/huygensDescent/index.cfm Titan averages a chilly -180 degrees Celsius, and its smoggy orange atmosphere is thicker than the Earth's, mostly nitrogen but 6 percent methane, together with substantial traces of all sorts of other hydrocarbons. The orange color may come from "tholins": polymers made by irradiating a mix of nitrogen and methane. Some other icy moons in the outer solar system are covered with this goop, but Titan is the only moon in the Solar System to have a substantial atmosphere. It even has clouds. As the Huygens probe parachuted to the surface, it photographed what look like twisty riverbeds flowing into a large lake! People have long suspected that Titan has lakes of made of methane and/or ethane, but now we may be seeing them. And when Huygens landed, its sensors reported that it broke through a crusty surface and sunk about 20 centimeters into something mushy: probably methane mud! The first color photo of the surface looks disappointingly like Mars at first sight. But, the surface is pumpkin-colored due to tholins or something, not rust red. The sky is orange too! The "rocks" could be water ice. And they've detected hints of volcanos that spew molten water and ammonia! So, it's a strange new world. Back here on Earth, there was a conference in December in honor of Larry Breen's 60th birthday: 2) Arithmetic, Geometry and Topology: Conference on occasion of Larry Breen's sixtieth birthday, http://www-math.univ-paris13.fr/~lb2004/ It was in Paris. This was my first visit to that city, but luckily I got to stay there an extra week after the conference, so I could focus on the math while it was going on. But I can't resist a digression! Paris won my heart, despite my suspicions that it had somehow been hyped all along. First of all, it's beautiful. Second, it's nice to be someplace where people take simple foods like bread, cheese, fruits and vegetables really seriously, and don't settle for the tasteless crud we so often eat in the US. None of this came as a surprise, of course. What surprised is that I've never seen a city with so many bookstores - and good ones, too! They're clustered thick near the Sorbonne, but the Latin Quarter is dotted with them, and there are even lots along the Boulevard St-Germain, which is the biggest most fashionable shopping street. I don't think there's any place in the English speaking world with so many bookstores. Not London, not New York... Cambridge Massachusetts used to have lots near Harvard Square, back when I was a grad student, but the high rents have long since squeezed them out, replacing bohemian diversity with clothing shops for boring rich people, like Abercrombie and Fitch. Somehow in Paris fancy clothing and books coexist. Umm, but what about the conference? Well, Breen's work is mainly on algebraic geometry a la Grothendieck, with a strong emphasis on category theory. Beautiful stuff, and lately it's it's begun to find applications to string theory - especially his work on gerbes. People at his conference spoke on all sorts of topics, most of which I didn't understand very well - some heavy-duty number theory, for example. I understood a few well enough to really enjoy them, like Mike Hopkins' talk on derived algebraic geometry, Clemens Berger's talk on geometric Reedy categories, and Ieke Moerdijk's talk on the homotopy theory of operads. But I won't try to explain these - I want to explain what a "gerbe" is, so I have my work cut out for me. One way to get going on the idea of gauge theory is to start with electromagnetism, where the concept of "phase" turns out to play a crucial role. If you move a charged particle through an electromagnetic field, its wavefunction gets multiplied by a unit complex number, or "phase" - and it turns out, rather wonderfully, that all effects of electricity and magnetism on charged particles is due to this! However, phases are funny. You can't actually measure the phase of a charged particle - at least, there's no such thing as a "phasometer" where you stick in a particle and the dial on the meter points to a unit complex number. Of course a unit complex number is just a fancy name for a point on the circle, and a dial is precisely the right shape for that... but you just can't build this machine. Instead, you can only measure the *change* in phase of a particle as it goes around a loop. Or, equivalently, the *difference* in phases when a particle takes two different paths from here to there. See, in quantum mechanics you can play tricks like the "double slit experiment", where you coax a particle's wavefunction to smear out and take two routes from here to there... and then when it arrives, it interferes with itself, and if you're smart you can see by these interference effects what the relative phase of the two paths is. Pretty weird, eh? I'm so used to this that it seems completely normal to me, but I should admit that this way of understanding the electromagnetic field came fairly late. Weyl had a hint of it in 1918 when he invented the term "gauge theory" in his quest to unify electromagnetism and gravity, but he was mixed up in some crucial ways that only got sorted out quite a bit later. For more details, try O'Raiferteagh's book "The Dawning of Gauge Theory", which I discussed in "week116". Anyway, the concept of relative phase, or difference in phase, is nicely captured by the concept of a "torsor". A unit complex number is a point on the unit circle in the complex plane. This circle is a group since we can multiply unit complex numbers and get unit complex numbers back. This group is called U(1). Like a dial, U(1) has standard names for all the points on it - and it has one god-given special point, the identity element, namely the number 1. A "U(1) torsor" is a lot like U(1), but subtly different. It's a circle where the points aren't given these standard names... but where you can still tell measure angles, and tell the difference between clockwise and counterclockwise. You can't get an element of U(1) from *one* point on a U(1) torsor. But, if you have *two* points on a U(1) torsor, you can say how much rotation it takes to get from one to the other, and this give an element of U(1). In other words, you can describe the "difference in phase" between these two points. For more on torsors, try this: 3) John Baez, Torsors made easy, http://math.ucr.edu/home/baez/torsors.html Anyway, the real idea behind electromagnetism is that sitting over each point in spacetime is a U(1) torsor. If a particle is sitting at some point in spacetime, its phase is not really a numbers: it's an element of the U(1) torsor sitting over that point! To get a *number*, we have to carry the particle around a loop! Its phase will change when we do this, so we get *two* points in a U(1) torsor, and their difference is an element of U(1). So while it sounds far-out, the key mathematical structure in electromagnetism is a bunch of U(1) torsors, one over each point in spacetime. This is called a "principal U(1) bundle" or sometimes just a "U(1) bundle" for short. If we wanted to describe some force other than electromagnetism, we could take this whole setup and replace U(1) with some other group. In fact, this idea works great: it's the main idea behind gauge theories, which do an excellent job of describing all the forces in nature. To set up a gauge theory, the first thing you need to do is pick a group G and pick a "principal G-bundle" over spacetime. Spacetime will be some manifold X. A principal G-bundle over X is gadget that assigns a G-torsor to each point of X. A G-torsor is a space where if you pick two points in it, you get an element of G which describes their "difference". I'm being fairly sloppy here, so don't take these as precise definitions! I give a precise definition of a G-torsor in the above webpage, and any decent book on differential geometry will give you a definition of a principal G-bundle. However, only rather highbrow books define principal G-bundles with the help of G-torsors... which is sad, because it's not that hard, and rather enlightening. Anyway, in gauge theory the forces of nature are described by "connections" on principal G-bundles. Let's say we have a principal G-bundle P which assigns to each point x of our manifold a G-torsor P(x). Then a "connection" on P is a gadget that says how any path from x to y gives a map from P(x) to P(y). If G is U(1), for example, this gadget says how the phase of a charged particle changes as we move it along any path from x to y. Now suppose we have a loop that starts and ends at x. Then our connection gives a map from P(x) to itself. If we start with a point in P(x), and apply this map, we get another point in P(x). Since P(x) is a G-torsor, these two points determine an element of G. This is how we get group elements from loops in gauge theory! Now let me sketch how gerbes enter the game. First I'll do the case where the group G is abelian, for example U(1). It's the nonabelian gerbes that really interest me... but the abelian case is a lot easier. The reason is that when G is abelian, the group element we get in the previous paragraph doesn't depend on the choice of a point of P(x). Gerbes show up when we try to invent a kind of "higher gauge theory" that describes how not just point particles but 1-dimensional objects transform when you move them around. For example, the strings in string theory, or the loops in loop quantum gravity. This leads to a mind-boggling self-referential twist, which is just the kind of thing I love: As we've seen, a connection describes how a point particle transforms when you carry it along a path: f x------------>-----y a path f from the point x to the point y: we write this as f: x -> y Now we need a gadget that'll describe how a *path* transforms when you carry it along a PATH OF PATHS: f ----------->----- / || \ x ||F y a path-of-paths F from the path f to the path g: \ \/ / we write this as F: f => g ----------->----- g To do this, we need to boost our level of thinking a notch, working not with "G-torsors" and "principal G-bundles" but instead with "G-2-torsors" and "G-gerbes". Here's how it goes: We start by picking an abelian group G and a manifold X. Then we pick a "G-gerbe" over M, say P. What's that? It's a thing that assigns to each point x of X a "G-2-torsor", say P(x). What's that? Well, it's a thing where if you pick two points in it, you get a G-TORSOR describing their difference! Get it? This is the beginning of a story that goes on forever: Two points in a G-torsor determine an element of G; two points in a G-2-torsor determine a G-torsor; two points in a G-3-torsor determine a G-2-torsor; . . . But, you'll probably be relieved to know we won't go beyond G-2-torsors today. Next, we pick a "connection" on P. What's that? Well, it's a gadget that for each path from x to y gives us a map from the G-2-torsor P(x) to the G-2-torsor P(y). If we call the path f: x -> y then we call this map P(f): P(x) -> P(y) Moroever, this sort of connection also gives a "map between maps" for each path-of-paths! So, from F: f => g it gives P(F): P(f) => P(g) I haven't explained enough stuff to say yet what these "maps between maps" are, so let's just see what happens if we have a loop f: x -> x and then a loop-of-loops F: f => f Our connection assigns a map to the loop f: x -> x, like this: P(f): P(x) -> P(x) If we start with a point in P(x), and apply this map, we get another point in P(x). Since P(x) is a G-2-torsor, these two points determine a G-torsor. This G-torsor doesn't depend on our initial choice of point. So, we can think of P(f) as being a G-torsor, if we like. Our connection also assigns a map to the loop-of-loops F: f => f, like this: P(F): P(f) => P(f) If we start with a point in P(f), and apply this map, we get another point in P(f). Since P(f) is a G-2-torsor, these two points determine an element of G. This element of G doesn't depend on our initial choice of point. So, we can think of P(F) as being an element of G, if we like. In short, the machinery functions just as you'd hope, giving a group element that describes how a loop of string "changes phase" as you carry it around a loop-of-loops! So far I've been strenously avoiding the language of categories and 2-categories, but if you're at all familiar with that language, you'll have guessed that it's precisely what we need to make everything I'm saying precise. It's actually incredibly beautiful... but I'm getting lazy, so I'll explain it very tersely now, in a way that only true lovers of abstraction will enjoy: If G is a group, it acts on itself by left translation. So, it becomes a left G-set. Any left G-set isomorphic to this one is called a "G-torsor". There's a category G-Tor whose objects are G-torsors and whose morphisms are maps compatible with the action of G. Since all G-torsors are isomorphic, and the automorphism group of any one is just G, this category G-Tor is equivalent to G (regarded as a 1-object category). If G is abelian, every left G-set becomes a right G-set too. This allows us to define a "tensor product" of G-sets. The tensor product of G-torsors is a G-torsor, so G-Tor becomes a monoidal category. In fact, it's a "2-group": a monoidal category where all the objects and morphisms are invertible. This allows us to iterate what we've just done: Since G-Tor is a 2-group, it acts on itself by left translation. So, it becomes a "left G-category". Any left G-category isomorphic to this one is called a "G-2-torsor". There's a 2-category G-2-Tor whose objects are G-2-torsors, whose morphisms are functors compatible the action of G, and whose morphisms are natural transformations compatible with the action of G. Since all G-2-torsors are isomorphic, and the automorphism 2-group of any one is just G-Tor, this 2-category is equivalent to G-Tor (regarded as a 1-object 2-category). And so on! This infinite hierarchy only works when G is abelian; when G is nonabelian we need a different hierarchy, which uses "bitorsors", where G acts on both left and right, instead of "torsors". To learn more about this stuff, here are some references. I'll stick to ones I didn't already list in "week71" and "week151". First, for physicists, some work on the role of gerbes and 2-gerbes in string theory and M-theory: 4) Paolo Aschieri, Luigi Cantini and Branislav Jurco, Nonabelian bundle gerbes, their differential geometry and gauge theory, available as hep-th/0312154. 5) Paolo Aschieri and Branislav Jurco, Gerbes, M5-brane anomalies and E8 gauge theory, available as hep-th/0409200. Second, for mathematicians, some classic works by Breen: 6) Lawrence Breen, Bitorseurs et cohomologie non-abelienne, in The Grothendieck Festschrift, eds. P. Cartier et al, Progress in Mathematics vol. 86, Birkhauser, Boston, 1990, pp. 401-476. 7) Lawrence Breen, Theorie de Schreier superieure, Ann. Sci. Ecole Norm. Sup. 25 (1992), 465-514. 8) Lawrence Breen, Classification of 2-stacks and 2-gerbes, Asterisque 225, Societe Mathematique de France, 1994. 2-gerbes are what you get if you climb the hierarchy one more step. They should be good for describing the parallel transport of 2-dimensional surfaces, or "2-branes" - and indeed they make an appearance in Aschieri and Jurco's paper for precisely that reason. Another key reference is Breen's paper with Messing about connections on nonabelian gerbes: 9) Lawrence Breen and William Messing, The Differential Geometry of Gerbes, available as math.AG/0106083. and Breen's lecture notes from the IMA workshop on higher categories: 10) Larry Breen, n-Stacks and n-gerbes: homotopy theory. Notes available at http://www.ima.umn.edu/categories/#thur I've been working on this stuff myself lately, from a somewhat different viewpoint. So far I've written papers with Aaron Lauda and Alissa Crans about 2-groups and Lie 2-algebras: 11) John Baez and Aaron Lauda, Higher-dimensional algebra V: 2-groups, Theory and Applications of Categories 12 (2004), 423-491. Available online at http://www.tac.mta.ca/tac/volumes/12/14/12-14abs.html or as math.QA/0307200. 12) John Baez and Alissa Crans, Higher-dimensional algebra VI: Lie 2-algebras, Theory and Applications of Categories 12 (2004), 492-528. Available online at http://www.tac.mta.ca/tac/volumes/12/15/12-15abs.html or as math.QA/0307263. Aaron Lauda was getting a masters degree in physics at UCR when we started our paper on 2-groups. Now he's a grad student in math at the University of Cambridge, working on things related to topological quantum field theory with the category theorist Martin Hyland. Alissa Crans did her PhD in math at UCR, and our paper on Lie 2-algebras contains a lot of stuff from her thesis. Now she has a job at Loyola Marymount University, in Los Angeles. I've had a huge amount of fun working with both of them! Luckily Alissa lives nearby, and I visit Cambridge most summers. So, we can all keep working on other projects together - and we are. I also have some gerbe-related projects going on with my grad student Toby Bartels, Danny Stevenson (who is teaching at UCR now) and Urs Schreiber, a fellow moderator of sci.physics.research who will soon be a postdoc at Hamburg with Christoph Schweiger. Urs will be visiting UCR for two weeks in February, and we plan to figure a lot of stuff out. So, I've got gerbes on the brain, and I'll probably be saying more about them in the future, unless I burn up all my expository energy writing papers. In fact, one of the best places to learn about the differential geometry of abelian gerbes and 2-gerbes is Danny's thesis: 13) Danny Stevenson, The geometry of bundle gerbes, Ph.D. thesis, University of Adelaide, 2000. Available as math.DG/0004117. He's also written lots of other papers on gerbes, which you can find on the arXiv. Physicists may find these the most interesting: 14) Michael K. Murray and Danny Stevenson, Higgs fields, bundle gerbes and string structures, Comm. Math. Phys. 236 (2003), 541-555. Also available as math.DG/0106179. 15) Alan L. Carey, Stuart Johnson, Michael K. Murray, Danny Stevenson and Bai-Ling Wang, Bundle gerbes for Chern-Simons and Wess-Zumino-Witten models, available as math.DG/0410013. Toby is doing his thesis on categorified bundles, or "2-bundles", and you can already get a preview here: 16) Toby Bartels, Categorified gauge theory: 2-bundles, available as math.CT/0410328. 2-bundles are meant to be an alternative to gerbes: although I've done my best to hide it above, a gerbe is really more like a categorified *sheaf* than a bundle. And, just as a bundle has a sheaf of sections, we're hoping that a 2-bundle has a stack of sections, which in certain cases will be a gerbe. That's one of the things we need to figure out, though. And, while I'm listing the papers of the gerbe gang, I should admit that Urs and I have written a paper about connections on 2-bundles. But, I want to polish this paper a bit before talking about it here. As for 2-groups, various people have been studying their representations lately, and this should become an important part of higher gauge theory, just as group representations are crucial in gauge theory: 17) Magnus Forrester-Barker, Representations of crossed modules and cat^1-groups, Ph.D. thesis, Department of Mathematics, University of Wales, Bangor, 2004. Available at http://www.informatics.bangor.ac.uk/public/mathematics/research/ftp/theses/forrester-barker.pdf 18) John Barrett and Marco Mackaay, Categorical representations of categorical groups, available as math.CT/0407463. 19) Josep Elgueta, Representation theory of 2-groups on finite dimensional 2-vector spaces, available as math.CT/0408120. Hendryk Pfeiffer's papers on higher gauge theory are also very interesting. Since he works on lattice gauge theory and spin foam models, the first two papers here develop higher gauge theory on a discrete spacetime, and then compare it to higher gauge theory on a manifold: 20) Hendryk Pfeiffer, Higher gauge theory and a non-Abelian generalization of 2-form electrodynamics, Annals Phys. 308 (2003), 447-477. Also available as hep-th/0304074. 21) Florian Girelli and Hendryk Pfeiffer, Higher gauge theory - differential versus integral formulation, Jour. Math. Phys. 45 (2004), 3949-3971. Also available as hep-th/0309173. 22) Hendryk Pfeiffer, 2-groups, trialgebras and their Hopf categories of representations, available as math.QA/0411468. The third one partially fulfills an old dream of Crane and Frenkel - a dream I vaguely hinted at way back in "week50". Their dream was to find a concept of "trialgebra" such that a trialgebra has a Hopf category of representations, which in turn can have a monoidal 2-category of representations of its own. This is a kind of aggravated version of a pattern already familiar in algebra, where a Hopf algebra (or bialgebra) has a monoidal category of representations. Pfeiffer doesn't define general trialgebras, but only "cocommutative trialgebras" and "commutative cotrialgebras". A cocommutative trialgebra is a category in the category of cocommutative Hopf algebras, while a commutative cotrialgebra is a category in the opposite of the category of commutative Hopf algebras. Zounds - say that three times fast! He shows you can get these two gadgets from 2-groups in analogy to how you get cocommutative or commutative Hopf algebras from groups, by taking the group algebra or the algebra of functions on a group. He also proves a Tannaka- Krein theorem that lets you reconstruct commutative cotrialgebras from their Hopf categories of representations. Really cool stuff! ----------------------------------------------------------------------- Previous issues of "This Week's Finds" and other expository articles on mathematics and physics, as well as some of my research papers, can be obtained at http://math.ucr.edu/home/baez/ For a table of contents of all the issues of This Week's Finds, try http://math.ucr.edu/home/baez/twf.html A simple jumping-off point to the old issues is available at http://math.ucr.edu/home/baez/twfshort.html If you just want the latest issue, go to http://math.ucr.edu/home/baez/this.week.html