Date: Wed, 1 Jun 1994 21:22:27 +0500 (GMT+4:00) Subject: limits and colimits of enriched categories Date: Tue, 31 May 94 22:31:33 PDT From: john baez In Kelly's book on enriched category theory, he seems to claim that it would be easy to prove that if K is a symmetric monoidal closed category in which all small diagrams have limits and colimits, then in the category of small K-categories it is also true that all small diagrams have limits and colimits, but he does not actually prove this. Does anyone know a reference for a proof of this fact? John Baez Date: Thu, 2 Jun 1994 16:48:09 +0500 (GMT+4:00) Subject: Name change for PSSL? Date: Thu, 2 Jun 94 10:33:00 BST From: John Power Dear Colleagues, I have been inundated with mail about a proposed name change for the "Peripatetic Seminar on Sheaves and Logic". I would like to make two points: 1 several people seem to be pressing a "reply" button and thereby communicating their response with the rest of the world. I suggest you send them only to me unless you specifically want them distributed worldwide: I will acknowledge receipt of each, and I am collecting them all to pass to Dana in due course for a decision. 2 so far, the great majority of replies want to retain the current name. I humbly submit that some may not be taking the concern sufficiently seriously. I organized the last meeting, and some intelligent, very interesting people in closely related areas felt the meeting would be irrelevant to them because of the name. Of those, I convinced some to attend, but even then, they did so skeptically. Others evidently thought I misrepresented the nature of the meeting and did not come. Presumably, others did not attend but did not tell me their concerns. It seems to me that it is of fundamental importance that such a seminar welcome new intelligent interesting people in closely related areas: so if we are not to change the name, I suggest people send alternative suggestions to resolve the problem. All the best, John. Date: Thu, 2 Jun 1994 16:46:40 +0500 (GMT+4:00) Subject: Re: Name change Date: Thu, 2 Jun 1994 10:43:12 +1000 From: Murray Adelman I would like to go on record as suggesting the same name for the PSSL. I think "logic" covers a lot of ground and don't like the idea of replacing part of a name on the grounds that it will "put some people off". Personally I think "sheaves" in the general context it is used in the name of the seminar is relevant to computer science. Regards, Murray Date: Thu, 2 Jun 1994 16:50:36 +0500 (GMT+4:00) Subject: Re: limits and colimits of enriched categories Date: Thu, 02 Jun 94 08:50:03 PDT From: Ross Casley Date: Tue, 31 May 94 22:31:33 PDT From: john baez In Kelly's book on enriched category theory, he seems to claim that it would be easy to prove that if K is a symmetric monoidal closed category in which all small diagrams have limits and colimits, then in the category of small K-categories it is also true that all small diagrams have limits and colimits, but he does not actually prove this. Does anyone know a reference for a proof of this fact? John Baez I wrote out the proof for limits in my dissertation. (Ross Casley. On the Specification of Concurrent Systems. Department of Computer Science, Stanford University. Feb 1991. Technical Report STAN-CS-91-1355.) The existence of colimits is shown in a somewhat more general setting in the following: @Article( BCSW83, Author="Betti, R. and Carboni, A. and Street, R. and Walters, R.", Title="Variation Through Enrichment", Journal="Journal of Pure and Applied Algebra", Volume=29, Pages="109-127", Year=1983) -Ross Casley Date: Fri, 3 Jun 1994 15:36:16 +0500 (GMT+4:00) Subject: Re: limits and colimits of enriched categories Date: Thu, 02 Jun 94 15:11:28 PDT From: pratt@CS.Stanford.EDU Date: Thu, 02 Jun 94 08:50:03 PDT From: Ross Casley From: john baez if K is a symmetric monoidal closed category in which all small diagrams have limits and colimits, then all small diagrams [in K-Cat] have limits and colimits. Does anyone know a reference for a proof of this fact? I wrote out the proof for limits in my dissertation. (Ross Casley. On the Specification of Concurrent Systems. Department of Computer Science, Stanford University. Feb 1991. Technical Report STAN-CS-91-1355.) Ross is too modest, the theorem he proves there is a tad stronger: if K has all J-limits for a small diagram J then so does K-Cat. K should be symmetric monoidal but need not be closed and needs no limits or colimits beyond those implied by the existence of all J-limits. Vaughan Pratt Date: Fri, 3 Jun 1994 15:38:02 +0500 (GMT+4:00) Subject: Re: Name change Date: 2-JUN-1994 18:15:04.63 From: "Fred E.J. Linton" Open letter to John Power , and the readers of CATEGORIES, with the hope it will be forwarded to Dana Scott, adjudicator: , How about "Peripatetic CSAPL Seminar"? People can read what they wish into the initials -- Computer Science and Programming Languages -- Categories, Sheaves and Presheaves, Logic -- Combinatorics, Sets and Posets, Linguistics -- Computer Systems, Applied Physics, Lazy [evaluation] -- ... . , I'd pronounce CSAPL hungarian-style: approximately "chapel" ("choppel" for the purists, if they take to omitting that "accent aigue" over the A ). Then, of course, each meeting would need its own special preacher for the Sunday morning sermon, but we've never been at a loss for a suitable candidate before ... :-) . Some may even be pleased to see the initials APL (and the programming language for which it stands) resuscitated within the formation CSAPL . But please don't let that influence your decision, as many more may not be. Cheers. -- Fred Fred E.J. Linton Wesleyan U. Math. Dept. 649 Sci. Tower Middletown, CT 06459 E-mail: ( or ) Tel.: + 1 203 776 2210 (home) or + 1 203 347 9411 x2249 (work) Date: Sat, 4 Jun 1994 12:14:39 +0500 (GMT+4:00) Subject: Re: limits and colimits of enriched categories Date: Sat, 4 Jun 1994 16:16:02 +1000 From: Max Kelly I see that Casley has answered the query of Baez on the completeness and cocompleteness of V-Cat by giving the reference to the Betti, Carboni, Strret, Walters paper "Variation through enrichment" in JPAA 29 (1983), 109-127. That is a fine reference, and everyone should read that paper; but it was of course not my reason for believing the result at the time of writing my book, published in 1982 but available earlier as a preprint. The result that V-Cat is complete and cocomplete when V is so is much older, and is due to Harvey Wolff, J.Pure Appl. Algebra 4 (1974), 123-135. The paper of Betti et al. does indeed mention this reference - but some y younger colleagues may be unaware of the details of Wolff's contribution. Max Kelly. Date: Sat, 4 Jun 1994 12:17:44 +0500 (GMT+4:00) Subject: Re: limits and colimits of enriched categories Date: Fri, 3 Jun 1994 15:04:51 -0500 From: John Gray I would have thought that the standard reference to the cocompleteness of V-Cat was Harvey Wolff, V-cat and V-graph, J. Pure and Applied Alg, 4(1974) 123-135. He shows that if V is cocomplete, then so is V-cat, by showing that V-cat is monadic over V-graph, that V-graph is cocomplete and then quoting a result of Linton in F. E. J. Linton, Coequalizers in categories of algebras, in Lecture Notes in Math. 80, Springer-Verlag 1969, 75-90. His main application is the existence of localizations in the V case. Wolff assumes that V is a symmetric monoidal closed category. The existence of the free functor from V-graph to V-cat requires that tensor commute with coproducts, and the existence of coequalizers in V-cat seems to require that tensor commute with coequalizers, so closedness apparently is essential, at least for this form of the argument. He doesn't say anything about the existence of limits in V-cat. John W. Gray Date: Tue, 7 Jun 1994 10:15:08 +0500 (GMT+4:00) Subject: two ftp-able papers Date: Mon, 06 Jun 94 15:30:34 EDT From: SCPSG@acadvm1.uottawa.ca The following announcement of two ftp-able papers was made on the TYPES mailing list. The first paper on syntactic dinatural transformations may be of some interest to categorists. The second paper is aimed at concurrency theorists and logicians. Phil Scott ------------------------------------------------------------- Dear Colleagues: Due to some requests, the following two papers are available for anonymous ftp from Imperial College, Department of Computer Science (theory.doc.ic.ac.uk), in: papers/Scott. They also will shortly be available on the WorldWideWeb, at: http://www.csi.uottawa.ca/~phil/extra/papers . 1. "Normal Forms and Cut-Free Proofs as Natural Transformations", by J-Y. Girard, A. Scedrov, and P. J. Scott. This paper appeared in MSRI Publications (Logic from Computer Science), Y. Moschovakis, ed., Vol.21 (Springer-Verlag), 1992, pp. 217-241. Due to an error by Springer-Verlag, appropriate sizes of LateX fonts (for mathematics symbols) were not loaded into the printer for this volume (ours was not the only paper affected). Hence the published version of the above paper is almost unreadable in critical places. This is the complete original paper, with the authors' addresses updated. In brief, the paper is about parametricity, composition of definable dinatural transformations, and Wadler's equations. 2. "On the \pi-Calculus and Linear Logic" by G. Bellin and P. J. Scott. To appear in Theoretical Computer Science (1994), Proceedings Mathematical Foundations of Programming Semantics 8 (MFPS 8). This is a considerably revised version of the original ftp-able preprint and LFCS report. Sincerely, Philip Scott Dept. of Mathematics University of Ottawa Ottawa, Ont. Canada e-mail: scpsg@acadvm1.uottawa.ca or phil@csi.uottawa.ca Date: Sun, 12 Jun 1994 23:51:43 +0500 (GMT+4:00) Subject: New release of XY-pic diagram drawing macros Date: Thu, 9 Jun 1994 17:42:43 +0200 From: kris@diku.dk Dear fellow diagram drawers and TeX users! This is to announce the release of a new version of my DIAGRAM DRAWING PACKAGE, XY-pic: version 2.9. In particular this version represents the stage where XY-pic 3 has left ALPHA test (and entered BETA confidence test) and the kernel should be stable. The release is mainly a BUG FIX RELEASE fixing several problems reported in version 2.7 and 2.8 by users; in addition it ADDS THESE NEW FEATURES: * The speed of diagram typesetting has been increased back closer to the version 2.6 speed, faster for very large diagrams. * The set up of the style of \arrow command must now be clearly marked. * It is possible to `compile' large diagrams (with some restrictions) to a file such that retypesetting is faster still. * Options can now be loaded safely in any order. * The bug that required removal of \\ before \enddiagram has been fixed. * The PostScript backend by Ross Moore has been greatly enhanced and now supports varying line thickness, colour, rotation, and scaling. * There is a new feature by Ross Moore: \xyoption{2cell} loads special commands typesetting pairs and triples of curved arrows like categorical two-cells. Below I have attached the TRAILER of the package that gives some more details and explains how to obtain it; the version packaged specially for the Apple Macintosh by Ross Moore will be available shortly. Regards, Kristoffer Rose (.signature at end of TRAILER) -*-text-*- $Id: TRAILER,v 2.9 1994/06/09 14:53:07 kris Exp $ ====================================================================== TRAILER: ANNOUNCING the XY-pic version 2.9 DIAGRAM TYPESETTING PACKAGE ====================================================================== XY-pic is a package for typesetting a variety of graphs and diagrams within TeX that works with most formats (including LaTeX 2.09, LaTeX2e, AMS-LaTeX, AMS-TeX, and plain TeX). In particular XY-pic is provided as a LaTeX2e `package'. NOTE: version 2.9 is a final BETA CONFIDENCE TEST release of XY-pic 3 in the sense that it is likely to contain minor bugs in both documentation and code but should be stable. If you are a user of an earlier version of XY-pic then PLEASE TEST this release with your existing diagrams and REPORT PROBLEMS you encounter to the authors! The intention remains to maintain full backwards compatibility with XY-pic 2 but we need feed-back from users in order to achieve this goal (see `The future and backwards compatibility' in the User's Guide for the unavoidable exceptions). Version 2.9 is the final result of the effort this springs to outline XY-pic 3 in collaboration with Ross Moore while visiting Macquarie U, Sydney: The package has been restructured and extended into a kernel and several orthogonal modules and is now ready for the implementation of several independent `specialist' modes for convenient typesetting of Graphs and Trees, 2-cells, String and braid diagrams, etc. (some are already under construction). Below I discuss the main features of XY-pic and how it is available. ---------------------------------------------------------------------- VERSION 2.9 FEATURES ---------------------------------------------------------------------- XY-pic version 2.9 provides two modes of specifying drawings: * A matrix-like mode where the dimensions of the drawing are automatically computed by aligning diagram entries in rows and columns (this is also the `version 2 compatibility mode'). * A general `turtle graphic' drawing language for specifying graphs with objects and connections between them in a manner independent of orientation. Both modes support the following specific features: + Positions can be given in variety of formats (extendable) including user defined coordinates (x,y) and relative to previous positions, objects, object edges, and points on connections. + Objects may be circular or rectangular (more shapes can be added) and adjusted in several ways. + Large library of objects with mnemonic names. + Objects that orient themself along a connection when placed relative to it, e.g., `\dir{|-}' is like \vdash but thus oriented; new such objects can be defined in a convenient way. + Includes circle segments and arbitrary TeX text. + Connections are aligned between the reference points of objects but start and end on the edges. + Any object can be used to build a connection (using `diagonal filling'); library objects provide common line types. + Special notation for drawing arrows with tail, stem, and head build from any object(s). Special support for arrows that cross each other, arrows that `go by' other entries, combined arrows, and arrows with n/8 bends. + Library of frames. + NEW: Special notation for rotation, scaling, colour, and line thickness. The correct typesetting of these features requires a backend that supports it (i.e., PostScript) but even when PostScript is not available XY-pic tries to approximate what is requested. + Output can use PostScript for drawing (several \special formats are supported: dvips, dvitops, Textures, and OzTeX -- more are being added continuously: contact Ross Moore for the current list). Notation for inclusion of literal PostScript. ---------------------------------------------------------------------- AVAILABILTY ---------------------------------------------------------------------- XY-pic can be retrieved by anonymous ftp from at least the following locations (given as `site : directory'): ftp.diku.dk : /diku/users/kris/TeX ftp.mpce.mq.edu.au : /pub/maths/TeX as well as (unpacked) on CTAN in macros/generic/diagrams/xypic. The following distribution files should be available in the above two locations but check the `README' file in each case: xy29.TRAILER These release notes xy29run.tar.Z XY-pic 2.9 `ready to run' distribution for un*x and similar systems xy29src.tar.Z XY-pic 2.9 complete sources xy29mac.sit.hqx XY-pic adapted for the Macintosh (Textures and OzTeX) by Ross Moore xyguide.ps.Z User's Guide and Reference Manual preformatted xyrefer.ps.Z for a 300dpi PostScript printer Please note that XY-pic is `copyleft' under the terms of the GNU General Public License. ---------------------------------------------------------------------- This is the end of the TRAILER. I hope you will enjoy XY-pic! -- Kristoffer Ho/gsbro ROSE Internet: kris@diku.dk DIKU, U of Copenhagen, Universitetsparken 1, 2100 Ko/benhavn O/, DANMARK phone: +45 35321400 direct: +45 35321420 fax: +45 35321401 -- World Wide Web URL: file://ftp.diku.dk/diku/users/kris/WWW/home.html Date: Sun, 12 Jun 1994 23:56:24 +0500 (GMT+4:00) Subject: CFP: State in Programming Languages (SIPL '95) Date: Sat, 11 Jun 94 12:18:34 EDT From: ohearn@top.cis.syr.edu Call for Papers The Second ACM SIGPLAN Workshop on STATE in Programming Languages (SIPL) Jan 22, 1995 San Francisco Held in conjunction with POPL '95 Programming languages have been state-based since their inception. After a period of relative unpopularity, when research focused on declarative languages, interest in the treatment of state has been renewed. Research is increasingly devoted to finding a symbiotic relationship between the semantic foundations of declarative languages and the pragmatic handling of state in more conventional languages. This workshop brings together researchers from various areas, interested in the common issues of state manipulation in high-level programming languages. The first workshop in this series (SIPL '93) was held in Copenhagen in conjunction with FPCA '93. The proceedings are available as a Yale technical report YALEU/DCS/RR-968. A special issue of the Journal of Lisp and Symbolic Computation is being published as a follow-up to SIPL '93. Submissions are invited for the second workshop to be held in conjunction with POPL '95 in San Francisco. The workshop addresses the fundamental issues of expressing, manipulating, and reasoning about state in high-level programming languages. The range of topics includes operational and denotational models of state, assignment and references, semantics of object- oriented programming, calculi of state and methods to reason about state. Novel methods for expressing and controlling state- manipulation such as linear type systems, effect systems, and monads are also of interest. Formal presentations of results, research in progress, tutorials, and topical discussions are among the possible venues for interaction. Program Committee: Stephen Brookes, Carnegie-Mellon University Kim Bruce, Williams College John Launchbury, Glasgow University and Oregon Graduate Institute Ian Mason, Stanford University Peter O'Hearn, Syracuse University Andrew Pitts, Cambridge University Uday Reddy, University of Illinois (Chair) Mads Tofte, University of Copenhagen POPL General Chair: Ron Cytron, Washington University Submission: We solicit submissions on original research not submitted or published elsewhere. Authors should submit 8 copies of a detailed summary not to exceed 5000 words (approximately 10 pages) to the program chair by Sep 30, 1994. The cover page should include a return postal address and an electronic mail address (if possible). Please follow the same guidelines as for writing summaries for the POPL conference. These are available by anonymous FTP from directories ftp.cs.cmu.edu:/user/petel/popl95 and cs.uiuc.edu:/pub/reddy/sipl Authors will be notified of acceptance of their paper by Nov 15, 1994. Final versions of accepted papers are due on Dec 22, 1995. Accepted papers will appear in a technical report to be distributed at the workshop. Correspondence should be sent to: Prof. Uday Reddy SIPL '95 Department of Computer Science University of Illinois 1304 W. Springfield Avenue Urbana, IL 61801 U.S.A. E-mail: sipl@cs.uiuc.edu Date: Thu, 16 Jun 1994 13:50:35 +0500 (GMT+4:00) Subject: Birkhoff variety theorem Date: Thu, 16 Jun 1994 18:10:51 +0200 (MET DST) From: Paul Johnson I have a vague idea that Michael Barr has a result which answers the following question: that being to give characterization to that situation when a composite of functors A0 -----> A -----> X is tripleable, assuming A -----> X is, and that A0 -----> A is the inclusion of a subcategory. Perhaps the result reads like ``if and only if there exists a Horn clause....''. Might anyone give me a reference? Date: Fri, 17 Jun 1994 13:59:02 +0500 (GMT+4:00) Subject: ANNOUNCE: Kock-Moerdijk preprint Date: Fri, 17 Jun 1994 08:40:31 +0200 From: kock@mi.aau.dk Preprint "Spaces with local equivalence relations, and their monodromy" available. The final version of Kock and Moerdijk's work on this topic is now available by ftp at theory.doc.ic.ac.uk (login: anonymous, directory: papers/Kock, file: km-ler.dvi). Compared to the 1991 preprint, it has more emphasis on topology, less on toposes (the topos theoretic aspects are dealt with in our article published in JPAA 82 (1992)). A paper version (Aarhus Preprint 1994 No. 8) is also available, on request. From kris@diku.dk Ukn Jun 15 11:16:25 1994 Date: Wed, 15 Jun 1994 16:27:02 +0200 From: kris@diku.dk To: CATEGORIES@mta.ca Subject: ANNOUNCE: XY-pic version 2.10 released... Dear CATEGORY THEORY COMMUNITY, [You are on my XY-pic user list because you have once written to me about XY-pic. If you do wish to receive news about XY-pic (or get this message twice) then I apologise and ask you to tell me so by sending an E-mail to kris@diku.dk. And now the NEWS:] This is to announce a BUG FIX release of my DIAGRAM DRAWING PACKAGE, XY-pic: version 2.10. It fixes the following user visible bugs in version 2.9: * Very high of wide labels were not placed correctly on diagonal arrows by the `arrow' feature and in compatibility mode (thanks to Clemens Beckstein for finding this). * Colouring of labels (using the `color' extension) now works! I'm sorry for releasing so soon after the last release but the bugs were classed `important'. Please retrieve the new version by anonymous ftp from ftp.diku.dk : /diku/users/kris/TeX ftp.mpce.mq.edu.au : /pub/maths/TeX or the CTAN `macros/generic/diagrams/xypic' mirror which will be up to date in a day or so. Regards, Kristoffer Rose -- Kristoffer Ho/gsbro ROSE Internet: kris@diku.dk DIKU, U of Copenhagen, Universitetsparken 1, 2100 Ko/benhavn O/, DANMARK phone: +45 35321400 direct: +45 35321420 fax: +45 35321401 -- W3 home From streiche@informatik.uni-muenchen.de Ukn Jun 15 10:54:41 1994 Date: Wed, 15 Jun 94 16:04:02 +0200 From: Thomas Streicher To: categories@mta.ca Subject: McCarty = Eff Recently in a discussion with J. Lipton there came up the question whether the full and faithful embedding of D. McCarty's realisability model of IZF into the effective topos Eff is actually an equivalence. More concretely that means whether any object of the effective topos is really isomorphic to an object of the McCarty topos. I think the problem is highly nontrivial as the equality predicate on an object of the McCarty topos is derived form its inductive presentation. I would be pleased in any comments. Thanks in advance, Thomas Streicher Date: Mon, 20 Jun 1994 18:41:29 +0500 (GMT+4:00) Subject: Topology: a geometric account of general topology, homotopy types and the fundamental groupoid, published 1988, by Ronald Brown Date: Mon, 20 Jun 1994 14:28:33 +0100 From: "Prof R. Brown" The publishers have just informed informed me that the above book has been out of print since sept, 1993, that no stock is available, and that the copyright reverts to me. I would consider getting some loose page copies printed and sold if this seemed economic, and/or if for example there was a desire to use part or all for course adoption. For the latter I could supply a top copy and allow for copying to students at a moderate fee per student. Offers welcomed. The aim is to get the book available and read. The publisher's previous distribution at 50 pounds sterling discouraged this. This book has material on groupoids, homotopy types, fundamental groupoid of orbit spaces, etc. not available elsewhere. Ronnie Brown Prof R. Brown Tel: +44 248 382474 School of Mathematics Fax: +44 248 355881 Dean St email: mas010@uk.ac.bangor University of Wales Bangor Gwynedd LL57 1UT UK Date: Wed, 22 Jun 1994 22:34:53 +0500 (GMT+4:00) Subject: in case you hadn't heard Date: Tue, 21 Jun 94 11:51:50 -0400 From: jds@math.upenn.edu available on the hep-th list server is a paper by V. Lychagin Calculus and quantizations over Hopf algebras hep-th 9406097 It includes ``a general notion of quantization in monoidal cats'' which `deforms all natural algebraic and differential objects''. This occurs in Section 3 p. 31 + so skim rapidly if this is the part that interests you. [Note from moderator: th poster provided the following information on accessing hep-th server] This bulletin board for string/conformal field theory/2d gravity preprints, hepth@xxx.lanl.gov, described in an earlier message is now turned on. For the first week or so, replies to messages received during the day will be sent out only during the evening (so that potential bugs can be identified and corrected under actual combat conditions). A (subscribe all / cancel all) option has been added that allows automatic receipt of the full text of each paper on day of receipt. This is recommended only for large groups where a single such account could be used for general distribution or posting in a preprint library. Commands to the system, entered in the Subject: field of messages, are get # returns to requester the paper specified by # put submit paper (body of message in format described below*) paper is assigned #, and added to listing replace # replace paper specified by # with revised version (only original submitter can do this). listing returns title/author list of all papers currently held find (keyword) search title/author list for keyword (either authorname or word in title) to recall # subscribe add new username to distribution list (email address automatically extracted from return address) cancel remove username from distribution list subscribe all automatically receive full text of all papers cancel all return to receipt only of authors/titles/abstracts distribution returns full list of email addresses on distribution list comment forwards mail message for human perusal help returns this list of commands Date: Thu, 23 Jun 1994 14:21:04 +0500 (GMT+4:00) Subject: Domain Theory and Partial Maps Date: Thu, 23 Jun 1994 17:47:33 +0000 From: Marcelo Fiore My thesis (Axiomatic Domain Theory in Categories of Partial Maps) is available by anonymous ftp from ftp.dcs.ed.ac.uk directory pub/mf files thesis.dvi.Z and thesis.ps.Z. Marcelo Fiore P.S. The abstract follows: ------------------------------------------------------------------------ Axiomatic Domain Theory in Categories of Partial Maps Marcelo P. Fiore Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King's Buildings Edinburgh EH9 3JZ, Scotland Phone: + 44 31 650 5145. Fax: + 44 31 667 7209. June 1994 Synopsis This thesis is an investigation into axiomatic categorical domain theory as needed for the denotational semantics of deterministic programming languages. To provide a direct semantic treatment of non-terminating computations, we make partiality the core of our theory. Thus, we focus on categories of partial maps. We study representability of partial maps and show its equivalence with classifiability. We observe that, once partiality is taken as primitive, a notion of approximation may be derived. In fact, two notions of approximation, contextual approximation and specialisation, based on testing and observing partial maps are considered and shown to coincide. Further we characterise when the approximation relation between partial maps is domain-theoretic in the (technical) sense that the category of partial maps Cpo-enriches with respect to it. Concerning the semantics of type constructors in categories of partial maps, we present a characterisation of colimits of diagrams of total maps; study order-enriched partial cartesian closure; and provide conditions to guarantee the existence of the limits needed to solve recursive type equations. Concerning the semantics of recursive types, we motivate the study of enriched algebraic compactness and make it the central concept when interpreting recursive types. We establish the fundamental property of algebraically compact categories, namely that recursive types on them admit canonical interpretations, and show that in algebraically compact categories recursive types reduce to inductive types. Special attention is paid to Cpo-algebraic compactness, leading to the identification of a 2-category of kinds with very strong closure properties. As an application of the theory developed, enriched categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined and two abstract examples of models, including domain-theoretic models, are axiomatised. Further, FPC is considered as a programming language with a call-by-value operational semantics and a denotational semantics defined on top of a categorical model. Operational and denotational semantics are related via a computational soundness result. The interpretation of FPC expressions in domain-theoretic Poset-models is observed to be representation-independent. And, to culminate, a computational adequacy result for an axiomatisation of absolute non-trivial domain-theoretic models is proved. ------------------------------------------------------------------------ Date: Sun, 26 Jun 1994 15:48:11 +0500 (GMT+4:00) Subject: Third Announcement of Tempus Summer School in Budapest Date: Sun, 26 Jun 1994 20:35:42 +0200 From: cora@ludens.elte.hu ************************************** * WE CAN STILL ACCEPT REGISTRATIONS! * ************************************** ************************************************************* > < > Third Announcement & Program of the Summer School < > < > ALGEBRAIC LOGIC and the METHODOLOGY OF APPLYING IT, < > < > July 11-17, 1994, Budapest, < > < > which is part of the TEMPUS Summer School series for < > Algebraic and Categorial Methods in Computer Science. < > < ************************************************************* This will be the third one in the above mentioned series of summer schools, attached to the TEMPUS project entitled "Algebraic and Categorial Methods in Computer Science". The summer school is sponsored by the European Community TEMPUS office. The summer school received support from IQSoft Budapest, too. ORGANIZING COMMITTEE: Hajnal Andreka, Miklos Ferenczi, Istvan Nemeti and Ildiko Sain ORGANIZING SECRETARY: Corinna Farkas ADDRESSES: Please send your correspondence to BOTH of the following two e-mail addresses: cora@ludens.elte.hu and h1468sai@ella.hu, or to the following mailing address: Ildiko Sain, Mathematical Institute, Budapest, Pf. 127, H-1364, Hungary. Fax: (36-1) 117-7166 (indicate: To Ildiko Sain). If you intend to participate, please, fill in & send back the REGISTRATION FORM attached to the end of this announcement (if you haven't done so yet). -------------------------------------------------------------------------- S C I E N T I F I C P R O G R A M Courses: ________________________________________________________________ | | | WILLEM BLOK and DON PIGOZZI: General Algebraic Logic | | | | VAUGHAN PRATT: Chu Spaces: Complementarity and Uncertainty in | | Rational Mechanics | | | | YDE VENEMA: Boolean Algebras with Operators & Modal Logic | | | | ISTVAN NEMETI and HAJNAL ANDREKA: Algebras of Relations of | | Various Ranks & their Applications | | | | WORKSHOP GIVEN BY YOUNG RESEARCHERS: Decidability issues and | | logics related to the dynamic trend | | | | UNIVERSAL ALGEBRA TUTORIAL | |________________________________________________________________| Talk: ANTONINO SALIBRA (joint work with Don Pigozzi): The Abstract Variable-binding Calculus ABSTRACTS OF COURSES: Willem Blok and Don Pigozzi: GENERAL ALGEBRAIC LOGIC "General algebraic logic" can be characterized as the process of reducing logical deduction, in its broadest sense, to equational logic, the particularly simple form of logical deduction that underlies most of modern algebra. In these lectures we investigate the precise method by which this reduction can be either completely or partially effected. We show how this leads to close connections between logical systems and suitable classes of algebras, enriched with a predicate when the reduction is only partial. We outline the theory of algebraization in a very general context, illustrating the ideas with numerous examples. Having isolated a precise notion of algebraizable logic, we show how it provides the proper framework for studying algebraic equivalents of metalogical properties as, for example, the property of "possessing a deduction theorem". --------------- Vaughan Pratt: CHU SPACES: COMPLEMENTARITY AND UNCERTAINTY IN RATIONAL MECHANICS "Rational mechanics" captures mind-body duality for autonomous agents in essentially the same way that quantum mechanics captures momentum-position duality for physical systems, with Chu spaces in place of Hilbert spaces. Chu spaces expose a Heisenberg-like uncertainty principle as a previously unnoticed yet prominent feature of Stone duality. --------------- Yde Venema: BOOLEAN ALGEBRAS WITH OPERATORS & MODAL LOGIC Formalisms related to Modal Logic play an important role in theoretical computer science: think of examples like epistemic logic, dynamic logic or relational algebra. Such formalisms can be treated in a nice algebraic way via the theory of Boolean Algebras with Operators (BAO's). The course will be centered around two themes: (1) the duality between BAO's and Relational (Kripke) Structures, and (2) modal/algebraic languages to describe these structures. We will review some important and elegant theorems, like automatic completeness results for a large class of logics. --------------- Istvan Nemeti and Hajnal Andreka: ALGEBRAS OF RELATIONS OF VARIOUS RANKS & THEIR APPLICATIONS Theories of relations (binary ones, ternary relations, n-ary ones etc.) play an essential role both in Computer Science and in Logic. Besides quantifier logics, they are important for e.g. logics of the dynamic trend, resource-sensitive logics, substructural logics, logics of actions etc. We will study algebras whose elements are relations. Research in this area has been going on for 140 years, hence its theory is powerful and profoundly applicable. The goal of the course is to make this rich theory accessible, to provide insight into why and how it works, and to highlight the main directions in which it is "moving". --------------- Agnes Kurucz and Ildiko Sain: UNIVERSAL ALGEBRA TUTORIAL Algebras, subalgebras, homomorphisms, congruences, Cartesian products. Subdirect decomposition, simple and subdirectly irreducible algebras. Birkhoff's subdirect decomposition theorem. Ultraproducts, Los theorem. Birkhoff's variety characterization theorem, quasi-variety characterization theorem. Discriminator varieties. We will give only a brief survey of the above broad material, concentrating on theorems frequently used in algebraic logic. Theorems will be stated and explained but usually not proved. A detailed lecture notes containing full proofs will accompany the lectures. --------------- ABSTRACT OF TALK: Antonino Salibra (joint work with Don Pigozzi): THE ABSTRACT VARIABLE-BINDING CALCULUS In this talk we illustrate how the algebraizations of classical and nonclassical logics fit into a general framework of variable-binding and variable-substitution that includes such diverse variable-binding operations as lambda abstraction, definite Riemann integration, universal and existential quantification (in both classical and intuitionistic logic), and various notions of generalized quantification. The main conceptual devices used are the abstract variable-binding calculus (VB-calculus) and the variety of polyadic VB-algebras. We show that every locally finite polyadic VB-algebra is isomorphic to a functional polyadic VB-algebra that is obtained from some model of the VB-calculus by a natural coordinatization process. As an application of this result, we present a strong completeness theorem for the VB-calculus that specializes to give a completeness theorem for every VB-theory. In particular, this result specializes to a completeness theorem for the familiar formal systems above specified. --------------- ABSTRACTS OF WORKSHOP LECTURES: Viktor Gyuris: FINITE SCHEMA AXIOMATIZABLE ALGEBRAIZATION OF FIRST-ORDER LOGIC The algebraic counterparts of first-order logic obtained so far (e.g. representable cylindric algebras, representable polyadic algebras, representable relation algebras) are not axiomatizable even with a finite schema of equations. This negative property has lead to serious difficulties of various kinds. Here we present an algebraic counterpart of first-order logic which is axiomatizable by a simple finite schema of equations. The key step is to choose the operations suitably on algebras whose elements are relations of higher ranks. --------------- Agnes Kurucz: DECIDABLE & UNDECIDABLE VARIETIES OF BAO'S AND LOGICS TOUCHED BY THE DYNAMIC TREND We shall map the landscape of logics of the so called dynamic paradigm from the point of view of decidability and undecidability. We will see what this "map" means for decidability issues about the equational theories of the algebraic counterparts of these logics. As a byproduct, we will get a "systematic" answer to the question "Which varieties of Boolean algebras with operators are decidable?". Proof methods will be discussed, too. --------------- Maarten Marx: ARROW LOGICS: A PARADIGM FOR LOGICS TOUCHED BY THE DYNAMIC TREND Research in areas such as Computer Science, Linguistics, Artificial Intelligence and Cognitive Science gave birth to a new paradigm for doing logic which for brevity we will call the dynamic paradigm. Logics of this paradigm include dynamic logic, action logic(s), dynamic semantics, resource sensitive logics such as linear logic and its fragments and Lambek Calculus, process logics and algebras, various temporal logics etc. The theory of Arrow Logics is both (i) the common backbone of all these new logics, and (ii) an explicit formulation of the new paradigm. One of the purposes of Arrow Logic is to give insight into the common essence of all these logics or, in other words, into "what makes them tick". --------------- Szabolcs Mikulas: A TECHNOLOGY FOR OBTAINING WELL-BEHAVED & STRONG ALGEBRA OF RELATIONS There are many well-investigated and useful logics that do not behave nicely in certain respects. Such examples are the undecidability of classical first-order logic, FOL, incompleteness of its finite variable fragment, Ln, and the incompleteness and undecidability of the strongest versions of logics of dynamics and action or resource sensitive logics etc. Following the ideas of van Benthem and Nemeti, we will discuss how to "tame" logics so that they behave in a nice way, and at the same time, remain strong (expressive) or become even stronger. That is, using the powerful methods of algebraic logic, we will reformulate several logics and show that these new versions (i) have desirable properties such as completeness, decidability etc., and at the same time (ii) their expressive powers remain great or become even greater. --------------- Szabolcs Mikulas and Andras Simon: METHODOLOGY OF APPLYING ALGEBRAIC LOGIC TO LOGIC This talk aims at improving understandability and usefulness of the Andreka-Nemeti (AN) lectures as well as the rest of the workshop lectures. The algebraic investigations in the AN lectures are applied in the workshop talks, among others, to logics originating from computer science, linguistics, cognitive science. The present talk explains the methodology of these and other applications, putting both the AN lectures and the workshops in perspective. We present a methodology of translating purely logical problems to algebra, then solving them by the strong machinery available in algebra, and then translating the result back to logic. The AN lectures as well as the workshops will occasionally refer to the material covered in the present talk. --------------- A TENTATIVE schedule of the programme is in the chart below. Abbreviations: UA tuto = Universal Algebra Tutorial A-N = Andreka-Nemeti B-P = Blok-Pigozzi M-S = Mikulas-Simon W = Workshop +---------+---------+---------+---------+---------+---------+ | Monday | Tuesday |Wednesday|Thursday | Friday |Saturday | |=======|=========|=========|=========|=========|=========|=========| | 8- 9 | | UA tuto | | | | | |-------|---------|---------|----W----|---------|----W----|----W----| | 9-10 | Pratt | UA tuto | M-S | Pratt | Mikulas | M-S | |-------|---------|---------|---------|---------|---------|----|----| | 10-11 | Pratt | B-P | Pratt | B-P | B-P |A-N |Ven.| cons. |-------|---------|---------|---------|---------|---------|----|----| | 11-12 | UA tuto | B-P | Pratt | B-P | B-P |B-P | | cons. |-------|---------|---------|---------|---------|---------|----|----| | 12-13 | | | | | | | |-------|---------|---------|---------|---------|---------|---------| | 13-14 | | | | | | | |-------|---------|---------|---------|---------|---------|---------| | 14-15 | A-N | Venema | A-N | Venema | A-N | E | |-------|---------|---------|---------|---------|---------|---------| | 15-16 | A-N | Venema | A-N | Venema | Venema | X | |-------|---------|---------|---------|---------|---------|---------| | 16-17 | | Salibra | Marx | Kurucz | Gyuris | C | |-------|---------|---------|----W----|----W----|----W----|---------| | 17-18 | | | | | | U | |-------|---------|---------|---------|---------|---------|---------| | 18-19 | | | | | | R | |-------|---------|---------|---------|---------|---------|---------| | 19-20 | party | | | | | S | |-------|---------|---------|---------|---------|---------|---------| | 20-21 | party | | | | | ION | +-------+---------+---------+---------+---------+---------+---------+ LECTURE NOTES: Every registered participant will receive basic lecture notes for courses indicated in the program. Besides these notes, scientific papers for further reading and extra copies of the lecture notes will be sold throughout the summer school. --------------------------------------------------------------------------- G E N E R A L I N F O R M A T I O N ACCOMMODATION: In double bedrooms for 14 DM/day, or in single bedrooms for 18 DM/day, in Summer Hotel Hill. The lectures will be in the same building. Address: Budapest, district XI, Menesi street 5. MEALS: Continental breakfast for 4 DM/day, lunch for 5,3 DM/day in Summer Hotel Hill. The Drink Bar of Summer Hotel Hill is open from 7 a.m. until late at night. Many restaurants are available in the neighborhood of Summer Hotel Hill. REGISTRATION: All participants are requested to register and to pay the conference fee and charges as appropriate, at the Reception Desk on Sunday, July 10: 6 p.m. - 10 p.m. or on Monday, July 11: 8 a.m. - 9 a.m. or 12 a.m. - 14 p.m. or 16 p.m. - 18 p.m. The Reception Desk is located close to the entrance of Summer Hotel Hill. REGISTRATION FEE: 120 DM for participants 50 DM for accompanying persons. EXCHANGE OF CURRENCY: Foreign currency can be brought into Hungary without restriction and there is no obligation for exchanging currency. However, in general, you have to use Hungarian currency (HUF called Forints in Hungarian) in shops. Exchange bureaux are available at the airport, in bigger hotels, in banks and other places. TRAVEL: Budapest has two airport terminals, Ferihegy I and Ferihegy II. >From both terminals you have the same possibilities to come to the center. The most convenient way is offered by the Minibus-Service at very reasonable price. They take you to any address in Budapest with their comfortable 8-seaters, for 600 Forints (equivalent to 10 DM) per person. Tickets are available at the Airport passenger service counters. You can also choose to use buses called "Centrum Airport Service" as well. These buses leave every 30 minutes to Erzsebet square in central Budapest for 200 Forints (equivalent to 3,3 DM), from where you can take tram no.49 or no.47 to "Moricz Zsigmond korter", the nearest square to your accommodation (Summer Hotel Hill, Menesi street 5), which is at 5 minutes walking distance from the tram station at Moricz Zsigmond korter. For using public transportation in Budapest (trams, buses, Metro or trolley buses), tickets must be purchased in advance, for 25 Forints (0.5 DM) each trip. One can buy tickets from slot machines (there are some slot machines at the airport terminal bus stations), at Metro stations, or from some of the small shops selling newspaper or tobacco. Taxi from Ferihegy to central Budapest costs about 2000 Forints (equivalent to 33 DM). From Nyugati palyaudvar (Western Railway Station) you can reach Moricz Zsigmond korter by tram no.4 or no.6. From Keleti palyaudvar (Eastern Railway Station) to Moricz Zsigmond korter take bus no.7 or no.red 7, from Deli palyaudvar (Southern Railway Station) tram no.61. RENT A CAR: This service is at your disposal at Ferihegy Airport and all larger hotels. We can offer leaflets on them. SPORT FACILITIES in the Summer Hotel Hill: 25m swimming pool and sauna will be open from Monday to Friday: 6 a.m. - 9 p.m., during weekend: 8 a.m. - 6 p.m. One ticket costs 220 HUF, a ticket for 6 occasions (usable once a day) costs 600 HUF. Tickets can be bought at the reception of Summer Hotel Hill. The rent of the Fitness room is 120 HUF for one hour. The rent of the Drill Hall is 2200 HUF for one hour; here you can play tennis, basketball, volley ball, football. You have to take care of rackets and balls yourself. SOCIAL PROGRAMS: Reception on Monday evening and an excursion on Saturday afternoon. See also "Final notes" below. BOOK FAIR: From Tuesday (12th of June) to Thursday (14th) there will be a display and fair of books relevant to the Summer School, by Springer-Verlag and perhaps by Oxford University Press as well. MUSEUMS: Most museums are open from 10 a.m. to 6 p.m. All museums are closed on Monday. SHOPPING HOURS: Shopping hours are generally 10 a.m. to 6 p.m. on weekdays. On Saturday the majority of shops are closed, the rest close early afternoon. In shops you have to use Hungarian currency. (There are some exceptional places where foreign currency is accepted.) WEATHER: Hungary has a continental climate. The weather in July is generally dry and warm, with average temperatures between 24 and 30 centigrade. ---------------------------------------------------------------------- We hope this small map will help you to find Summer Hotel Hill in Budapest: / st. / / / 1: Bus stop no.7 from center | | | ************** / B. / 2: Bus stop no.7 to the center | | | |Summer Hotel| | / / 3: Tram stop no.4 and 6 ____| |_| |___Hill_____| | / k / 4: Tram stop no.47 to the center ____ __ Menesi st.___ \ / o / 5: Tram stop no.47 from center |H| \ \/ t / 6: Tram stop no.49 to the center |i| \ r / |m| / a / 2 This big crossing is called: |f| _/ B /______ "Moricz Zsigmond korter" ____|y|_______________/ _____ \____________________ _ / \ Villanyi st. /1/ 6 / Park | Karinthy Frigyes st. ___________________/_/ / 4/ ___________________ | /_______ / | / ____5__ / 3 / / \ Feher| / / | vari | | sreet| --------------------------------------------------------------------------