Date: Fri, 12 May 1995 10:03:42 -0300 (ADT) Subject: Summer School on SEMANTICS AND LOGICS OF COMPUTATION Date: Thu, 11 May 1995 10:23:31 +0100 From: Andrew Pitts A Newton Institute Summer School SEMANTICS AND LOGICS OF COMPUTATION 25--29 September 1995 Newton Institute, Cambridge, UK in collaboration with the ESPRIT CLICS-II project Second Call for Registration The Summer School on Semantics and Logics of Computation is being held as part of a six-month research programme on Semantics of Computation at the Isaac Newton Institute for Mathematical Sciences, a new international research centre in Cambridge UK. The Summer School is sponsored by the CEC ESPRIT research project "Categorical Logic in Computer Science, II" (CLICS-II). The aim is to present a number of modern developments in semantics and logics of computation in a way that is accessible to graduate-level students. Registrations from postgraduate students will be given priority, but applications by interested academics and industrialists are also welcomed. ===============================COURSES================================ Samson Abramsky (Imperial) "Semantics of interaction" (4 lectures) course content t.b.a. ---------------------------------------------------------------------- Thierry Coquand (Chalmers) "Computational content of classical logic" (4 lectures) I will give an introduction to the problem of extracting constructive content from classical proofs. This problem has an interesting history since it was an important part of Hilbert's program, who wanted to "secure" non-constructive parts of mathematics. It has been revived recently by the discovery of intringuing connections with some concepts in computer science through the work of (among others) C. Murthy, M. Parigot (lambda-mu calculus), J.L. Krivine (connection with imperative programing), Ph. de Groote (connections with exceptions in ML), and S. Berardi (symmetric lambda-calculus). I will try to provide both historical and mathematical background to this problem and to present concrete examples of non-constructive reasoning in mathematics that is constructively problematic. The emphasis will be on the proof-theoretical side, but I hope that this course will motivate and serve as an introduction to the more recent, computer science oriented work cited above (which will be described briefly). A tentative plan is the following Lecture 1: negative (double negation) translation, Friedman's A-translation. An existential statement provable in PA is provable in HA. Lecture 2: Gentzen's sequent calculus, first consistency proof for classical arithmetic. Connection to Novikov's calculus and game-theoretic interpretation. Lecture 3: problem with the combination Axiom of Choice + Excluded Middle. How this problem is solved in C. Murthy's thesis. A realizability interpretation of the negative translation of the Axiom of Choice. Lecture 4: use of formal topology (constructive theory of locales) for extracting constructive content from non-constructive proofs. Application to the topological proof of van der Waerden's theorem on arithmetical progression. ---------------------------------------------------------------------- Martin Hofmann (Edinburgh) "Dependent type theory: syntax, semantics, and applications" (4 lectures) The aim of this course is to familiarise participants with the use of dependent types from the viewpoint of their categorical semantics. Dependent types are types depending on values, for instance lists of a fixed length (arrays), the type of constructive proofs of a fixed proposition, the type of certain algebraic structures over a fixed set, etc. Categorical semantics provides a general framework for formulating and verifying interpretations of dependent types. The course will start with an introduction to theories of dependent types covering Martin-Lof's type theory, the Logical Framework, and the Calculus of Constructions. Guided by syntactic intuition we develop the notion of "categories with families", a simple yet sufficiently general notion of categorical semantics, and define the interpretation of the syntax therein. We then look at some instances such as term models and realisability models and compare to other semantic notions, in particular models based on fibrations. Finally, we treat some larger applications from Computer Science, such as Paulin-Mohring's method of program extraction from proofs, Moggi's work on semantics of modules, and the groupoid interpretation of Martin-Lof's type theory. ---------------------------------------------------------------------- Martin Hyland (Cambridge) "Game Semantics" (4 lectures) course content t.b.a. ---------------------------------------------------------------------- Eugenio Moggi (Genova) "Computational types and applications" (4 lectures) The prerequisites for this course are some knowledge of typed lambda calculus and equational logic. I will avoid use of domain theory as much as possible, because the basic ideas do not rely on it. However, the more sophisticated examples will have to make use of it. Lecture 1: Computational types -- syntax and equations. Lecture 2: Examples of computational types in the category of sets. Lecture 3: Semantics of programming languages via translation into a metalanguage with computational types; examples. Lecture 4: Modular approach to denotational semantics via reinterpretation of computational types. ---------------------------------------------------------------------- Mogens Nielsen & Glynn Winskel (Aarhus) "Models for concurrency" (4 lectures) In these lectures we will highlight a selection of the mathematical structures used in modelling parallel computation, ranging from "interleaving" models like transition systems to models like Petri nets and Mazurkiewicz traces, where concurrency is represented more explicitly by a form of causal independence. The presentation is unified by casting the models in a category-theoretic framework. Category theory is used to provide abstract characterisations of constructions like parallel composition, and broadly applicable definitions of bisimulation, valid throughout a range of different models. In addition, category theory yields formal means for translating between different models. ---------------------------------------------------------------------- Andrew Pitts (Cambridge) "Operationally-based theories for proving program properties" (3 lectures) The aim of the lectures will be to describe recent advances in techniques based on operational semantics for establishing equivalence of programs. The co-inductive characterization of contextual equivalence between functional programs in terms of "applicative bisimulation" will be presented. The use of co-induction for reasoning about lazy datatypes will be illustrated. The extent to which this characterization generalizes to "impure" functional languages will be discussed. ====================================================================== LOCATION The workshop will take place in the Newton Institute's purpose designed building, in a pleasant area in the west of Cambridge, about one mile from the centre of the City. Accommodation for participants will be provided next door to the Newton Institute in the study bedrooms of Girton College's Wolfson Court. The accommodation will be available from the evening of Sunday 24 September until the morning of Saturday 30 September. Fees: general rate: 400 pounds student rate: 250 pounds The fee covers registration, accommodation, meals (breakfast, lunch, supper, tea & coffee breaks), and lecture materials. REGISTRATION There are only a limited number of places available on the Summer School. Intending participants are advised to apply for registration as soon as possible, and in no case later than 30 June 1995. To apply, please send your name and address (including e-mail or fax number, if available) to: Florence Leroy (SEM Summer School) Isaac Newton Institute 20 Clarkson Road Cambridge CB3 0EH Tel: +44 1223 335984 Fax: +44 1223 330508 Email: f.leroy@newton.cam.ac.uk ORGANIZERS For CLICS-II: Peter Dybjer (Chalmers) peterd@cs.chalmers.se For the NIMS Semantics of Andrew Pitts (Cambridge) Computation Programme: ap@cl.cam.ac.uk IMPORTANT DATES (Revised) deadline for registration 30 June 1995 Arrival date 24 September 1995 Scientific programme 25--29 September 1995 Departure date 30 September 1995 --------------------------------------------------------------------------- Date: Sat, 13 May 1995 12:29:37 -0300 (ADT) Subject: CT95 Registration Form and Fourth Announcement Date: Mon, 1 May 1995 22:04:25 -0300 From: Category Theory Conference CT95 REGISTRATION FORM Name: ______________________________________________________ Address: ______________________________________________________ ______________________________________________________ ______________________________________________________ E-mail: ________________________ Phone: _____________________ If known: Date of arrival: ___________________________________ Date of departure: _________________________________ By train: __ Car: __ Plane: __ (Arrival Time: ______________ ( (Arrival Flight #: __________ Staying at: University residence __ Other __ Do not eat: Lobster __ Salmon __ (It is hoped that lobster will be served on the excursion and (salmon at the banquet. If you check one or both of the boxes (above, alternate arrangements will be made for you. Registration fee: General: $ 250 ______ Student: $ 125 ______ Extra tickets for accompanying people: Banquet: $ 40 ______ (Per extra person) Excursion $ 50 ______ (Per extra person) TOTAL PAYMENT $ ______ (Can.) Payment enclosed: __ In $ Can.: __ In $ U.S.: __ (0.8 x Total) = $ ____ or Registration deposit of $50 (Can.) (or $40 (U.S.) with balance to be paid on arrival: __ Notes: 1. At least the registration deposit to be paid before June 1. 2. Cheques to be made payable to CT95; mailed to RJ Wood, Mathematics, Dalhousie, Halifax, NS, B3H 3J5, Canada. 3. No credit cards accepted for registration fee payment. 4. Registration for CT95 is distinct from university accommodation. 5. Extra tickets will be available until Sunday July 9. 6. Abstracts to be sent to pare@cs.dal.ca as soon as possible. Date: Sat, 13 May 1995 12:30:13 -0300 (ADT) Subject: CT95 Fifth message Date: Mon, 8 May 1995 12:27:09 -0300 From: Category Theory Conference CT95 Fifth Message The information about CT95 is now also available on the Web. You can either point to URL http://www.mta.ca/~cat-dist/ct95.html or access through the categories home page. Links to ascii versions of registration forms and regional tourist information are included. It is also possible to contact Tourism Nova Scotia by e-mail. The address is nsvisit@fox.nstn.ca A representative stated the following: ``If people contact us for information, we can forward our Nova Scotia Travel Guide. It is approximately 300 pages and it contains information on attractions, accommodations, events and things to see and do in all of Nova Scotia. We would be pleased to forward information to anyone interested.'' They mean that, upon request by e-mail, they will physically mail you the publication. If you plan to spend some time before or after the meeting seeing Nova Scotia (an excellent idea) then you will find this publication extremely useful. A further enquiry about road maps produced the following: ``We can also provide maps and package information to anyone interested. If people let us know what type of information they are looking for, we can provide packages containing the best information for them. If you are hosting a conference, we can also assist with reservations.Suzanne Morrison from our office can assist in obtaining room blocks and we can actually make reservations on our North American tollfree line to save people making long distance calls directly to the hotels.'' The response time may be a little slow. They probably do not have anybody dedicated to answering e-mail but some of you may still find the service more efficient than physical mail. The North American tollfree line is the one that we mentioned earlier: 1-800-565-0000 The accommodation service in question is quite distinct from the university service that was descibed in the third announcement. Concerning university accommodation for STUDENTS, it should be pointed out that the rate of $20/nightly, $110/weekly, which was advertised for the Category Theory Summer School, is available during CT95 too. Students should declare themselves as such, immediately upon arrival, to obtain this rate. To: CT95 Conference delegates arriving by air Re: transportation to Halifax from Halifax Airport From: Mike Wendt There are two ways to get from the airport to Halifax: BUS. The airport bus departs approximately every half hour from 6am to 12am and costs $11 one way, $18 return. The ride takes about thirty five minutes and the bus stops at various downtown hotels. Of these, the Lord Nelson and the Halifax Holiday Inn are closest to the university. From either, the taxi fare to the university should be about $5. TAXI. The cost of a taxi from the airport to Halifax is approximately $35. We propose that if several people arrive on the same flight, they share a taxi. If you are interested in sharing, please send your flight arrival information (flight number and arrival time) to: wendt@cs.dal.ca We will put people in touch with each other. The airport is not large. A good place to meet is in the domestic baggage claim area, near the exit from international arrivals. International passengers must pass through customs and go through a door which opens on the domestic baggage claim area. Date: Sat, 13 May 1995 12:31:28 -0300 (ADT) Subject: BRICS positions Date: Fri, 21 Apr 1995 15:33:38 +0200 From: Uffe Engberg Postdoctoral positions at BRICS There are several postdoctoral positions at BRICS for a period of one to two years starting this year, 1995. Applications by researchers are welcome in the areas of logic, semantics, algorithms and complexity theory. Applications for positions should preferably be sent by e-mail and include curriculum vitae and two or three names of referees for recommendations as well as the referees' regular mail addresses and, if possible, e-mail addresses (see below). BRICS, a Centre for Basic Research in Computer Science, is funded by the Danish National Research Foundation for the period 1994-1999. Its aim is to establish in Denmark important areas of basic research in the mathematical foundations of Computer Science, notably Algorithmics and Mathematical Logic. The Centre is to develop these areas as a joint effort between the theoretical-computer- science groups at Aarhus University and Aalborg University. The research plan is based on a committment to develop Algorithmics and Logic integrated with existing strong activities in Semantics of Computation, using a combination of long-term efforts and a number of short-term, intensive programmes, within carefully chosen scientific themes. Organizationally, BRICS is an autonomous centre with its own management, and yet with its activities strongly integrated in the existing infrastructure and student environments at the two universities. The scientific planning is the responsibility of the following committee: Glynn Winskel, Professor (Aarhus), Director Mogens Nielsen, Associate Professor (Aarhus), Codirector Erik Meineche Schmidt, Associate Professor (Aarhus), Codirector Uffe Engberg, (Aarhus), Project Manager Kim Guldstrand Larsen, Professor (Aalborg) Peter D.Mosses, Associate Professor (Aarhus) Michael Schwartzbach, Associate Professor (Aarhus) Arne Skou, Associate Professor (Aalborg) Sven Skyum, Associate Professor, Reader (Aarhus) Further information on BRICS can be accessed through World Wide Web (WWW) and anonymous FTP. To connect to the BRICS WWW entry, open the URL: http://www.brics.aau.dk/BRICS/ The BRICS WWW entry contains updated information about activities, courses and researchers as well as access to electronic copies of information material and reports of the BRICS Series (look under Publications). To access the information via anonymous FTP do the following: ftp ftp.daimi.aau.dk cd pub/BRICS get README Addresses: BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark. Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.aau.dk How to apply for a position at BRICS ------------------------------------ Applications for positions should preferably be sent by e-mail and include ^^^^^^ - curriculum vitae and - two or three names of referees for recommendations with the referees' + regular mail addresses and, if possible, + e-mail addresses, as well as - an URL to your WWW home directory if available. The various parts of the application (application letter, CV, etc.) can be sent by e-mail as e.g. uuencoded PostScript, clear ASCII text or if it causes troubles, just as an URL in which case we will try to load the files. /Uffe H. Engberg -- ########### B R I C S | Uffe Henrik Engberg ##### ##### Computer Science Department | engberg@daimi.aau.dk ########### University of Aarhus | +45 8942 3365 ##### ##### Ny Munkegade, Building 540 | ##### ##### DK-8000 Aarhus C | +45 8942 3360 BRICS ##### ##### Denmark | +45 8942 3255 Fax BRICS WWW URL "http://www.brics.aau.dk/BRICS/" Date: Sat, 13 May 1995 12:32:12 -0300 (ADT) Subject: AMAST Date: Tue, 2 May 1995 00:05:56 +0200 From: scollo@cs.utwente.nl (Pippo Scollo) Dear Bob, In view of the frequent (and most welcome!) relevance of contributions from the forum you moderate to the AMAST newsletter, I would appreciate it if you could distribute the enclosed information. Thank you very much, in advance. Regards, Pippo ----------------------------------------------------------------------- [Please accept my apologies if you receive this message more than once. G. Scollo] The AMAST newsletter (the acronym stands for Algebraic Methodology And Software Technology, from the name of a related conference series), called _AMAST Links_, was started last year as an experiment. This has made quite good progress so far, and has now reached some sort of definite shape. Here's some more information about the AMAST newsletter and the related mailing list. _AMAST Links_ is issued monthly and has two forms: plain-text and hypertext. The plain-text form is distributed by e-mail, while both forms are made available on the World-Wide Web (WWW) and by anonymous FTP. In the hypertext form, links to more detailed information, or to information otherwise related to the announcements, are included when available. If you wish to have a look at individual pages of the latest issue of _AMAST Links_, or to previous issues, and if you have access to the WWW, then please open either of the following: WWW URL: http://www.cs.utwente.nl/data/amast/links/AL-Index.html FTP URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/links/AL-Index.html whereby you should get to a page which provides you with links to all the issues of the AMAST newsletter appeared so far. A more general index to all the AMAST information maintained on the WWW- and FTP- servers at the University of Twente (in The Netherlands) is available at either of the following URL: WWW URL: http://www.cs.utwente.nl/data/amast/Index.html FTP URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/Index.html If you do not have access to the WWW, you may get a detailed outline of that information by FTP from host: ftp.cs.utwente.nl username: anonymous (please give your e-mail address as password) directory: pub/doc/amast/ file (plain ASCII text): README In addition to the newsletter, AMAST subscribers may receive (if they wish so) e-mail messages sent to the list by other subscribers. This communication form is neither direct nor immediate, however. Messages sent to the list communication address amast@cs.utwente.nl are collected into a digest, which is distributed at a frequency not higher than fortnightly. Because of the availability of _AMAST Links_ to host announcements and the like, the digest usually has a very modest size. Subscription to _AMAST Links_ and/or to the AMAST e-mail digest is free of charge, and is obtained by sending a message to the list management address amast-request@cs.utwente.nl where a subscription option may be specified. The following options are available: S1: (default) full newsletter and e-mail digest, S2: full newsletter, but no e-mail digest, S3: ToC-only option (no e-mail digest, by default), S4: ToC-only option, but with e-mail digest as well. In particular, the ToC-only version of each issue of AMAST Links only contains the first and the last page of that issue, which respectively list the page titles and the contributors to that issue. The ToC-only option is thus well-suited for those who wish to receive a low-volume, summary information by e-mail, and then access the items of interest by FTP or on the WWW. For more information, please send a message to the list information address amast-info@cs.utwente.nl specifying your request. Date: Sat, 13 May 1995 12:32:47 -0300 (ADT) Subject: cocomplete toposes having no small set of generators From: Thomas Streicher Date: Fri, 05 May 1995 16:14:50 MESZ One possible very concise definition of GROTHENDIECK topos is as an elementary topos E such that 1) E is locally small 2) E has small sums 3) E has a small set of generators One knows that a lex category B satisfies 1) and 2) iff the global sections functor Gamma : B -> Set has a lex left adjoint Delta. For an elemenatry topos E satisfying 1) and 2) the condition 3) is equivalent to the requirement that any object X of E is a SUBQUOTIENT of a Delta(I). Now may question is WHAT IS THE STATUS of LOCALLY SMALL COCOMPLETE ELEMENTARY TOPOSES Are there natural examples ?? Locally small cocomplete elementary toposes are sufficient for interpreting set theory. Can they - maybe - characterised via this property ? Do there exist models of set theory giving rise to cocomplete topoi which don't have a small set of generators ? The background of my question is that elementary toposes as such don't provide models of IZF (how should one simulate the Goedel-Bernays-Neumann hierarchy ?). It would be nice iff cocomplete topoi were the precise analogon of IZF ! But maybe that's hoping too much ? Grateful for any hints, Thomas Streicher Date: Sat, 13 May 1995 12:33:09 -0300 (ADT) Subject: Re: cocomplete toposes having no small set of generators Date: Tue, 9 May 95 22:43:59 EDT From: Michael Barr What about small G-sets, where G is a LARGE group. This was the classic example of an equational category that isn't varietal, that is lacks free algebras. A classic example, anyway. Michael Date: Sat, 13 May 1995 12:33:24 -0300 (ADT) Subject: announcement of paper Date: Wed, 10 May 1995 20:24:52 +1000 (EST) From: C. Barry Jay A Semantics for Shape ===================== by C. Barry Jay is now available by anonymous ftp at ftp.socs.uts.edu.au in the file users/cbj/shape_semantics.ps.Z Abstract -------- Shapely types separate data, represented by lists, from shape, or structure. This separation supports shape polymorphism, where operations are defined for arbitrary shapes, and shapely operations, for which the shape of the result is determined by that of the input, permitting static shape checking. The shapely types are closed under the formation of fixpoints, and hence include the usual algebraic types of lists, trees, etc. They also include other standard data structures such as arrays, graphs and records. End of returned message Date: Sat, 13 May 1995 12:33:49 -0300 (ADT) Subject: Re: cocomplete toposes having no small set of generators Date: Wed, 10 May 1995 07:43:07 -0400 From: Peter Freyd Thomas Streicher asks about cocomplete topoi that aren't Grothendieck. The standard example is as follows: an object is a "base set," B, together with an "operator set," C, with an action a:B x C -> B such that for every c:C it is the case that \b.abc is a permutation. One uses the convention that abc = b for all c not in C. (So one may think of this as a set on which the entire universe acts, the action "having small support".) Given a second such object B', C', a', a map from the first to the second is a function f:B -> B' such that f(abc) = a'(fb)c all b:B and c:(C union C'). This yields a topos and the forgetful functor to the cat of sets is logical (which tells one how to construct power-sets). If one drops the "\b.abc is a permutation" condition the resulting cat is not a topos but satisfies the Giraud definition except for the generating set. The Fourman interpretation of IZF arising from a cocomplete topos (I can't find Fourman's paper in MathSci -- look at my paper in the Mac Lane Festschrift, JPAA Vol 19, 1980) only refers to its "well-founded part." One needs "ur elements," that is, one needs IZFA, to get out of the well-founded part. Date: Sat, 13 May 1995 12:34:06 -0300 (ADT) Subject: cocomplete toposes having no small set of generators Date: Wed, 10 May 1995 12:32:33 -0400 From: Peter Freyd The standard example is to be found in 1.96(10) in Cats and Allegators. As for the connection with IZF take a look at the Mac Lane Festschrift, JPAA Vol 19 (1980), for papers by Fourman and me. IZF without ur-elements is not enough. One needs IZFA. Date: Sat, 13 May 1995 12:34:58 -0300 (ADT) Subject: re: cocomplete toposes having no small set of generators Date: Thu, 11 May 1995 12:41:57 +1000 From: street@macadam.mpce.mq.edu.au (Ross Street) >Date: Tue, 9 May 95 22:43:59 EDT >From: Michael Barr > >What about small G-sets, where G is a LARGE group. This was the classic >example of an equational category that isn't varietal, that is lacks >free algebras. A classic example, anyway. A reference for this classic example in the topos context is my paper Notions of topos, Bulletin Australian Math. Soc. 23 (1981) 199-208; MR83a:18014. Regards, Ross Date: Sun, 14 May 1995 23:02:25 -0300 (ADT) Subject: Fourman's paper Date: Sun, 14 May 1995 13:17:42 -0400 From: Peter Freyd For some reason the other day I couldn't find on MathSci Mike's paper on the connection between cocomplete topoi and Zermelo-Fraenkel. It's in plain sight: AU Fourman, Michael P. TI Sheaf models for set theory. SO J. Pure Appl. Algebra (Journal of Pure and Applied Algebra) 19 (1980), 91--101. DT Journal AB ``Set theory'' means Zermelo-Fraenkel set theory, with atoms, formulated in intuitionistic logic. ``Sheaf model'' means an interpretation in a locally small, complete topos. If A is an object in such a topos {script}E, the cumulative hierarchy V{sub} alpha (A), with A as the object of atoms, is defined in the expected way, with power objects at successor stages and direct limits at limit stages, and with the membership relation on V{sub} alpha (A) and the embedding of V{sub} beta (A) in V{sub} alpha (A) for beta < alpha being defined by induction simultaneously with V{sub} alpha (A). Formulas of set theory in which all quantifiers are bounded by V{sub} alpha (A)'s have a well-known interpretation in {script}E, since they are formulas of the internal logic of {script}E. The completeness and local smallness of E enable the author to interpret unbounded quantifiers as well. The truth value of ({all} x) phi (x) is the infimum of the truth values of the approximations ({all} x{in}V{sub} alpha (A)) phi (x) and existential quantifiers are handled similarly. The main theorem asserts that the axioms of set theory, as well as the axioms and rules of the underlying intuitionistic logic, are correct for this interpretation; if {script}E is Boolean then classical logic is also correct. The author gives three sorts of examples; (a) Fraenkel- Mostowski models, (b) Boolean-valued extensions, and (c) symmetric extensions. The main novelty here is in (a). If A is a set of atoms, G a group of permutations of A, {script}F a normal filter of subgroups of G, and M the associated Fraenkel-Mostowski model, then ordinary truth in M is the same as the author's interpretation in the Grothendieck topos {script}E of continuous G- sets, i.e. G-sets each of whose points has its stabilizer in {script}F. This is true despite the fact that {script}E is only a part of the (non- Grothendieck) topos of sets and functions of M. The latter topos, which we also call M, contains sets on which not G, but only some subgroup in {script}F, acts. These sets are not objects of {script}E, but they are elements of such objects (specifically of the V{sub} alpha (A)'s) and so contribute to the interpretation of set-theoretic formulas. (Reviewer's remark: M is obtainable from {script}E by making supports split; it is the direct limit, in the sense of logical morphisms, of the slice topoi {script}E/(G/H) where H ranges over {script}F. This sort of construction was used by P. J. Freyd [Bull. Austral. Math. Soc. 7 (1972) 1 - 76; MR 53#576; corrigenda, ibid. 7 (1972), 467 - 480; MR 54#7571].) In connection with (b), the author mentions the unpublished result of Higgs that the topos of sets and functions of a Boolean-valued model V{sup}B is equivalent to the topos of sheaves on B for the canonical topology, and he indicates that his interpretation, with A={empty}, coincides with the usual interpretation in V {sup}B. Finally, he shows that symmetric extensions can be obtained as the pure part (i.e. A=0) of Boolean extensions of Fraenkel-Mostowski models. (As far as the reviewer knows, this approach to symmetric extensions was first used by P. Vopenka and P. Hajek [Theory of semisets, Academia, Prague, 1972; MR 56#2824].) Date: Tue, 16 May 1995 18:24:31 -0300 (ADT) Subject: MathSci Date: Tue, 16 May 1995 07:08:05 -0400 From: Peter Freyd Several have asked me about MathSci. It is not, as far as I know, available to everyone on the internet. I think you have to talk your library into subscribing. The version at Penn is accessible only to people it recogognizes as being from Penn. It is described as follows: MathSci, produced by the American Mathematical Society (AMS), provides coverage of the world's literature on mathematics, statistics, and computer science and their applications in a wide range of disciplines, including econometrics, operations research, engineering, physics, biology, and many related fields. MathSci consists of eight subfiles: Mathematical Reviews. 1940-. Updated monthly, MR consists of evaluative reviews and abstracts of the mathematical research literature of the world. Current Mathematical Publications, 1985-. Updated monthly, CMP contains approximately 3000 newly published titles in advance of being reviewed. Current Index to Statistics, 1975-. Updated quarterly, produced jointly by the American Statistical Association and the Institute of Mathematical Statistics, CIS provides comprehensive coverage on the literature of Statistics. Eugene Strens Recreational Mathematics Collection contains over 4,000 mathematical books, journals, manuscripts, and puzzles archived by the University of Calgary Libraries. Index to Statistics and Probability, 1910-1968, compiled by John W. Tukey and Ian C. Ross, is an historical statistics subfile of over 25,000 entries. ACM Guide to Computer Literature, 1981-1989. Produced by the Association for Computing Machinery (ACM), GCL is a comprehensive index to the computing literature covering over 500 periodicals including books, conference proceedings and report literature. Computing Review, 1984-July 1990. Produced by the Association for Computing Machinery (ACM), CR consists of evaluative reviews of the research in computer science and its applications. Technical Reports in Computer Science, 1954 -. Updated quarterly, the Stanford collection consists of over 40,000 records of technical reports acquired from more than 135 academic and corporate institutions. * * * Some titles and abstracts/reviews will have TeX encoding, a formatting software system. You must have the TeX software with AMSFonts in order to restore the encoded records to the typeset form i.e. correctly formatted. Instructions for obtaining the software are available by accessing e-math via the AMS web ( http://e-math.ams.org) or via telnet ( e-math.ams.org logon: e-math password: e-math ). Date: Wed, 17 May 1995 00:57:37 -0300 (ADT) Subject: Announcement of papers Date: Wed, 17 May 95 10:40:41 +1000 From: Sjoerd Crans Dear people, The following papers are now available by anonymous ftp from ftp.maths.usyd.edu.au, in the directory sydcat/papers/crans. Hardcopies are also available, requests for this can be sent to the address below. thcms.ps Sjoerd E. Crans Quillen closed model structures for sheaves, to appear in {\em Journal Pure Appl. Algebra} 100 (1995). Abstract: In this paper I give a general procedure of transferring closed model structures along adjoint functor pairs. As applications I derive from a global closed model structure on the category of simplicial sheaves closed model structures on the category of sheaves of 2-groupoids, the category of bisimplicial sheaves and the category of simplicial sheaves of groupoids. Subsequently, the homotopy theories of these categories are related to the homotopy theory of simplicial sheaves. thpp.ps Sjoerd E. Crans Pasting presentations for $\omega$-categories. Abstract: The pasting theorem showed that pasting schemes are useful in studying free $\omega$-categories. It was thought that their inflexibility with respect to composition and identities prohibited wider use. This is not the case: there is a way of dealing with identities which makes it possible to describe $\omega$-categories in terms of generating pasting schemes and relations between generated pastings, \ie{}, with pasting presentations. In this paper I develop the necessary machinery for this. The main result, that the $\omega$-category generated by a pasting presentation is universal with respect to respectable families of realizations, is a generalization of the pasting theorem. thten.ps Sjoerd E. Crans Pasting schemes for the monoidal biclosed structure on $\omega\mbox{-} \bf Cat$. Abstract: Using the theory of pasting presentations, developed in the previous paper, I give a detailed description of the tensor product on $\omega$-categories, which extends Gray's tensor product on $2$-categories and which is closely related to Brown-Higgins's tensor product on $\omega$-groupoids. Immediate consequences are a general and uniform definition of higher dimensional lax natural transformations, and a nice and transparent description of the corresponding internal homs. Further consequences will be in the development of a theory for weak $n$-categories, since both tensor products and lax structures are crucial in this. Sjoerd Crans School of Mathematics and Statistics University of Sydney NSW 2006 Australia email: crans_s@maths.usyd.edu.au Date: Mon, 22 May 1995 11:18:27 -0300 (ADT) Subject: The effective topos. Date: Mon, 22 May 1995 13:22:11 +0100 From: Justin Pearson Dear All, A question for people who know about the effective topos. I'm just feeling my way, so be gentle. In the effective topos (and any other realizability topos I assume, but I don't know since I haven't got hold of the tripos paper yet), one can make internal the combinators S and K. I assume that you define the functional relations: G_s(n,n') = {n'} if Sn = n' \emptyset otherwise. G_k(n,n') = {n') if Kn = n' \emptyset otherwise. (In all this S refers to the combinator S not the successor function). Now here is the bit I'm not sure about, if we stipulate in a category, that there must be an object N with a unique pair of maps S and K such that: for all x,y K;x;y = x for all x,y,z S;x;y;z = x;z;(y;z) Further every map from N to N can be factored into S and K, and for good measure that N is actually the natural number object to avoid degeneracy. Does this characterize N in the effective topos? and hence the modest sets? Regards Justin Pearson Date: Mon, 22 May 1995 11:16:12 -0300 (ADT) Subject: WADT11/COMPASS-8, 2nd CFP (ASCII & Latex) Date: Mon, 22 May 1995 11:27:27 +0200 From: Magne.Haveraaen@ii.uib.no Please distribute. This reminder contains some new information, such as a list of invited speakers and some tourist information. Magne %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%ASCII%%%%%%%%%%%%%%%%%%%%%%%%% 11th ADT Workshop and 8th General Compass Meeting September 19 1995 -- September 23 1995 2nd Call for Participation Workshop on Specification of Abstract Data Types and ESPRIT Compass Meeting --------------------------------------------------------------------------- The two joint events will take place at Holmenkollen in Oslo. The workshop starts just after lunch-time Tuesday September 19, and lasts till Saturday evening September 23. Before the workshop a meeting of the IFIP WG 14.3 (Foundations of Systems Specifications) will be held the same place starting just after lunch-time Monday September 18. The workshop will provide an opportunity to meet colleagues, to present recent and ongoing work and to discuss new ideas and future trends. The workshop is organised by Olaf Owe and Ole-Johan Dahl from the University of Oslo, and Magne Haveraaen from the University of Bergen. The topics of the workshop include, but are not limited to: - algebraic specifications; - other approaches to formal specification; - specification languages and methods; - term rewriting and proof systems; - specification development systems (concepts, tools, etc.). As this is the final COMPASS year we have searched for invited speakers who may put the area of algebraic methods in a wider perspective, assess its practical value, and hopefully indicate possible future directions and links to related areas. The invited speakers include: - E. Astesiano (Universita di Genova, Italy) - R. Burstall (University of Edinburgh, United Kingdom) - H. Ehrig (Technische Universitdt Berlin, Germany) - C.A.R. Hoare (Oxford University, United Kingdom) - J. Horning (DEC Systems Research Center, Palo Alto, Ca, USA) - B. Krieg-Bruckner (Universitdt Bremen, Germany) - P. Lescanne (CRIN, Nancy, France) In addition there will be many prominent speakers from within the COMPASS project. The proceedings, consisting of a selection of the presented talks through the usual referee process, will be published after the workshop, probably in the Lecture Notes series of the Springer-Verlag (see e.g. the Recent Trends in Data Type Specifications series, no. 332, 534, 655, 785, ...). Please note: as there is a limited number of slots for talks, REGISTER NOW! We will accept speakers essentially in the order of arrival date of their registrations (a corrective mechanism is organised in order to guarantee visibility to every site). So if you plan to have a talk please let us know as soon as possible (communication via e-mail or WWW is suggested). Location -------- The workshop will be held at the Soria Moria Conference Center at Holmenkollen in Oslo, just 12 km from downtown and 14 km from the airport. The centre is located on the top of a hill, Voksenkollen, 500 m above sea level, overlooking the Oslo Fjord. It is bordering "Nordmarka", the Oslo forest national park, covering a huge area with lakes, forest and hills. Whereas September is too early for skiing, it is a good time for hiking, with trees in fall colours. For sporty participants we plan a hiking excursion to an old-fashioned log-cabin serving homemade food. An alternative excursion will show some of the interesting places in Oslo, such as the Viking ship museum (with authentic viking ships), the old stave church, the Vigeland sculpture park, Aker brygge (a fjord-front shopping and restaurant area with new and old architecture), the Munch Museum and the Holmenkollen ski jump national monument. Depending on the number of accompanying persons, and their interests, we will try to improvise some additional informal sightseeing. Also, one may take a suburban train to downtown Oslo in 30 minutes and visit the center (around Karl Johans gate) with museums, shops, and walking streets, all close together. For those interested in seeing more of Norway, such as the famous west coast fjords, the mountains, or the north of Norway, we will provide information about trips taking a few days or more. We especially recommend the Norway-in-a-nutshell trip, which includes the famous train ride from the mountains down to Flem and a boat tour on the Sognefjord. It is possible to make this tour starting from Oslo in the morning and returning to Oslo by night-train, or extend the trip to include a visit to Bergen. Accommodation ------------- According to tradition, the workshop is planned on a residential base, so participants are required to stay at the Soria Moria hotel. It is a modern hotel with excellent conference facilities, including swimming pool and sauna. Normal arrival is expected Tuesday September 19 after lunch, and departure on Sunday September 24 after breakfast, with the possibility of extending the stay in both directions. Participants to the IFIP WG 14.3 meeting are expected to arrive Monday September 18 after lunch. We have reserved a number of rooms, both single and double, and expect to be able to accommodate everybody registering {\bf before June 15}. We will try to accommodate people registering by July 31, depending on room availability. Please note: the single rooms will be assigned essentially following a FIFO principle; thus if you want a single room, book it now. Prices ------ We have an agreement with the hotel for a special price for full board during the workshop. For a single room this amounts to 880 NOK per day, and to 620 NOK per day per person in a double room. For the whole workshop the prices in Norwegian Crowns (NOK) amount to: ! WADT/COMPASS (Tue-Sun) ! WG14.3/WADT/COMPASS (Mon-Sun) -----------------+-------------------------+------------------------------ single room ! 4400 NOK (ca. 530 ECU) ! 5280 NOK (ca. 640 ECU) double room, p.p.! 3100 NOK (ca. 375 ECU) ! 3720 NOK (ca. 450 ECU) -----------------+-------------------------+------------------------------ Note that the prices in ECU are obtained at the current rate (which can be different in September). As usual a reasonable registration fee will be charged, to cover expenses like proceedings publication, social events and so on. The precise amount has still to be established, depending on the real costs and the funds that can be raised to cover them, but we expect it to be no more than 200 ECU. Some support may be available for participants from countries with soft currencies. Applications for support must be received by the registration deadline. Travel Information ------------------ The Soria Moria hotel is easily reachable by bus and taxi from downtown Oslo or directly from the Fornebu Airport in Oslo, with direct flight connections from most major European cities. Intercontinental travel is usually via Copenhagen, but some direct connections exist. The dates for the events have been chosen so that participants can make use of reduced airfares (PEX, APEX). There are also direct ferry conections to Kiel and Copenhagen. Other information ----------------- More organisational details will follow, and registered participants will be kept informed. Updated information will also be available on the World-Wide Web (WWW) at URL: http://www.ifi.uio.no/~adt95/ AS THERE IS A LIMITED NUMBER OF PLACES AVAILABLE FOR THE WORKSHOP, REGISTER EARLY! We will accept participants in the order of date of arrival of the enclosed registration form +---------------------------------------------------+ ! DEADLINE FOR REGISTRATION IS THE 15TH OF JUNE '95 ! +---------------------------------------------------+ Please return the registration form (by e-mail or surface mail) to the following address. Registration using WWW is also possible. ADT'95 Organisation Institutt for informatikk e-mail: adt95@ifi.uio.no Postboks 1080 Blindern phone: +47 22 85 24 10 0316 OSLO fax: +47 22 85 24 01 Norway WWW: http://www.ifi.uio.no/~adt95/ ------------------------------------------------------------------------ 11th ADT Workshop and 8th General Compass Meeting Registration form One form for each participant, please! Family Name ........................................................ Christian Name ........................................................ Institution ........................................................ Mailing address ........................................................ ........................................................ ........................................................ ........................................................ ........................................................ E-mail ........................................................ Fax ........................................................ Telephone ........................................................ I will attend to the workshop ... yes ... no I intend to give a talk ... yes ... no If yes, provisional title .............................................. ........................................................ ........................................................ I prefer ... single room ... double room I would like to share the room with ................................ Special meal requirements (please specify): ............................ I will arrive .......................... I will depart .......................... I am a member of IFIP WG 14.3 ... yes ... no Name of accompanying non-participants .................................. for which I need ...... additional single rooms and ...... additional double rooms Signature ............................................................. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%LATEX%%%%%%%%%%%%%%%%%%%%%%%%% \documentstyle{article} \topmargin - 21mm \oddsidemargin -11mm \evensidemargin -11mm \textheight 256mm \textwidth 180mm \renewenvironment{itemize}{\renewcommand{\item}{\\\hspace*{\parindent}$\bullet$\hspace*{\labelsep}}}{\\} \catcode`\<=\active\global\chardef~126 \pagestyle{empty} \begin{document} \begin{center} {\LARGE\bf 11th ADT Workshop and 8th General Compass Meeting}\\[1ex] {\Large\bf September 19 1995 -- September 23 1995}\\[1ex] {\large\bf 2nd Call for Participation} \end{center} \thispagestyle{empty} \subsection*{Workshop on specification of Abstract Data Types and ESPRIT Compass Meeting} The two joint events will take place at Holmenkollen in Oslo. The workshop starts just after lunch-time Tuesday September 19, and lasts till Saturday evening September 23. Before the workshop a meeting of the IFIP WG 14.3 (Foundations of Systems Specifications) will be held the same place starting just after lunch-time Monday September 18.\\ The workshop will provide an opportunity to meet colleagues, to present recent and ongoing work and to discuss new ideas and future trends. The workshop is organised by Olaf Owe and Ole-Johan Dahl from the University of Oslo, and Magne Haveraaen from the University of Bergen. The topics of the workshop include, but are not limited to: \begin{itemize} \item algebraic specifications; \item other approaches to formal specification; \item specification languages and methods; \item term rewriting and proof systems; \item specification development systems (concepts, tools, etc.). \end{itemize} As this is the final COMPASS year we have searched for invited speakers who may put the area of algebraic methods in a wider perspective, assess its practical value, and hopefully indicate possible future directions and links to related areas. The invited speakers include: \begin{itemize} \item E. Astesiano (Universit\'a di Genova, Italy) \item R. Burstall (University of Edinburgh, United Kingdom) \item H. Ehrig (Technische Universit\"at Berlin, Germany) \item C.A.R. Hoare (Oxford University, United Kingdom) \item J. Horning (DEC Systems Research Center, Palo Alto, Ca, USA) \item B. Krieg-Bruckner (Universit\"at Bremen, Germany) \item P. Lescanne (CRIN, Nancy, France) \end{itemize} In addition there will be many prominent speakers from within the COMPASS project. The proceedings, consisting of a selection of the presented talks through the usual referee process, will be published after the workshop, probably in the Lecture Notes series of the Springer-Verlag (see e.g.\ the Recent Trends in Data Type Specifications series, no. 332, 534, 655, 785, \ldots). \noindent{\bf Please note:} as there is a limited number of slots for talks, {\large\em register now!} We will accept speakers essentially in the order of arrival date of their registrations (a corrective mechanism is organised in order to guarantee visibility to every site). So if you plan to have a talk please let us know as soon as possible (communication via e-mail or WWW is suggested). \subsection*{Location} The workshop will be held at the Soria Moria Conference Center at Holmenkollen in Oslo, just 12 km from downtown and 14 km from the airport. The centre is located on the top of a hill, Voksenkollen, 500 m above sea level, overlooking the Oslo Fjord. It is bordering ``Nordmarka'', the Oslo forest national park, covering a huge area with lakes, forest and hills. Whereas September is too early for skiing, it is a good time for hiking, with trees in fall colours. For sporty participants we plan a hiking excursion to an old-fashioned log-cabin serving homemade food. An alternative excursion will show some of the interesting places in Oslo, such as the Viking ship museum (with authentic viking ships), the old stave church, the Vigeland sculpture park, Aker brygge (a fjord-front shopping and restaurant area with new and old architecture), the Munch Museum and the Holmenkollen ski jump national monument. Depending on the number of accompanying persons, and their interests, we will try to improvise some additional informal sightseeing. Also, one may take a suburban train to downtown Oslo in 30 minutes and visit the center (around Karl Johans gate) with museums, shops, and walking streets, all close together. For those interested in seeing more of Norway, such as the famous west coast fjords, the mountains, or the north of Norway, we will provide information about trips taking a few days or more. We especially recommend the {\em Norway-in-a-nutshell} trip, which includes the famous train ride from the mountains down to Fl{\aa}m and a boat tour on the Sognefjord. It is possible to make this tour starting from Oslo in the morning and returning to Oslo by night-train, or extend the trip to include a visit to Bergen. \subsection*{Accommodation} According to tradition, the workshop is planned on a residential base, so participants are required to stay at the Soria Moria hotel. It is a modern hotel with excellent conference facilities, including swimming pool and sauna. Normal arrival is expected Tuesday September 19 after lunch, and departure on Sunday September 24 after breakfast, with the possibility of extending the stay in both directions. Participants to the IFIP WG 14.3 meeting are expected to arrive Monday September 18 after lunch. We have reserved a number of rooms, both single and double, and expect to be able to accommodate everybody registering {\bf before June 15}. We will try to accommodate people registering by July 31, depending on room availability. \\ \noindent{\bf Please note:} the single rooms will be assigned essentially following a {\tt FIFO} principle; thus if you want a single room, {\em book it now}. \subsubsection*{Prices} We have an agreement with the hotel for a special price for full board during the workshop. For a single room this amounts to 880 NOK per day, and to 620 NOK per day per person in a double room. \noindent For the whole workshop the prices in Norwegian Crowns (NOK) amount to: \smallskip \begin{center} \begin{tabular}{|l|c|c|}\hline & Just WADT/COMPASS (Tue-Sun) & IFIP WG 14.3 \& WADT/COMPASS (Mon-Sun) \\ \hline single room & 4400 NOK ($\approx$ 530 ECU) & 5280 NOK ($\approx$ 640 ECU) \\ %\hline double room, p.p. & 3100 NOK ($\approx$ 375 ECU) & 3720 NOK ($\approx$ 450 ECU) \\ \hline \end{tabular} \end{center} Note that the prices in ECU are obtained at the current rate (which can be different in September). \smallskip As usual a reasonable registration fee will be charged, to cover expenses like proceedings publication, social events and so on. The precise amount has still to be established, depending on the real costs and the funds that can be raised to cover them, but we expect it to be no more than 200 ECU. Some support may be available for participants from countries with {\em soft currencies}. Applications for support must be received by the registration deadline. \subsection*{Travel Information} The Soria Moria hotel is easily reachable by bus and taxi from downtown Oslo or directly from the Fornebu Airport in Oslo, with direct flight connections from most major European cities. Intercontinental travel is usually via Copenhagen, but some direct connections exist. The dates for the events have been chosen so that participants can make use of reduced airfares (PEX, APEX). There are also direct ferry conections to Kiel and Copenhagen. \subsection*{Other information} More organisational details will follow, and registered participants will be kept informed. Updated information will also be available on the World-Wide Web (WWW) at URL: \begin{center} http://www.ifi.uio.no/~adt95/ \end{center} \begin{center} \Large As a limited number of places are available for the workshop, register early! \end{center} \noindent We will accept participants in the order of date of arrival of the enclosed registration form \medskip \begin{center} \large\bf \fbox{Deadline for registration is the 15th of June '95} \end{center} \medskip \noindent Please return the registration form (by e-mail or surface mail) to the following address. Registration using WWW is also possible. \begin{center} \begin{tabular}{lcll} ADT'95 Organisation &\makebox[3cm]{}& \\ Institutt for informatikk &&e-mail: &adt95@ifi.uio.no \\ Postboks 1080 Blindern &&phone: &+47 22 85 24 10 \\ 0316 OSLO &&fax: &+47 22 85 24 01 \\ Norway &&WWW: &http://www.ifi.uio.no/~adt95/ \end{tabular} \end{center} \begin{center} \pagebreak {\Large\bf 11th ADT Workshop and 8th General Compass Meeting} \smallskip {\Large\bf Registration form} {\bf One form for each participant, please!} \end{center} \addtolength{\baselineskip}{0.3cm} \bigskip \noindent \makebox[3cm][l]{Family Name} \ \dotfill\ \\ \makebox[3cm][l]{Christian Name} \ \dotfill\ \\ \makebox[3cm][l]{Institution} \ \dotfill\ \\ \makebox[3cm][l]{Mailing address} \ \dotfill\ \\ \makebox[3cm]{} \ \dotfill\ \\ \makebox[3cm]{} \ \dotfill\ \\ \makebox[3cm]{} \ \dotfill\ \\ E-mail \dotfill\qquad Fax \dotfill\qquad Telephone \dotfill\\ \bigskip \noindent \begin{tabular}{lll} I will attend to the workshop & $\Box$ yes & $\Box$ no\\ I intend to give a talk & $\Box$ yes & $\Box$ no\\ \end{tabular} \hspace{1cm}If yes, provisional title \dotfill\\ \makebox[3cm]{}\dotfill\\ \bigskip \noindent I prefer\hspace{2cm} $\Box$ single room\hspace{2cm}$\Box$ double room\\ \hspace{1cm}I would like to share the room with\ \dotfill\\ \bigskip \noindent Special meal requirements (please specify): \dotfill\\ \bigskip \noindent I will arrive \dotfill\\ I will depart \dotfill\\ I am a member of IFIP WG 14.3 \ \ \ $\Box$ yes \ \ $\Box$ no\\ \bigskip \noindent \begin{tabular}{@{}lll}\multicolumn{3}{@{}l@{}}{\hspace*{\textwidth}}\\[0em] Name of accompanying non-participants &\multicolumn{2}{l@{}}{\dotfill} \\ \multicolumn{1}{r}{for which I need} &\ldots\ldots\ldots& additional single rooms and \\ &\ldots\ldots\ldots& additional double rooms \end{tabular} \vfill \noindent \begin{tabular}{|l|}\hline {\bf Mail to:} \\ ADT'95 Organisation \\ Institutt for informatikk \\ Postboks 1080 Blindern \\ 0316 OSLO \\ Norway \\\hline \end{tabular}\\*[-2.5ex]\hspace*{5cm}Signature \dotfill \end{document} Date: Tue, 23 May 1995 00:44:53 -0300 (ADT) Subject: question about bounded toposes Date: Mon, 22 May 95 19:09:45 +0300 From: Zinovy Diskin Topos theoretic concepts are implicitly in the focus of semantic modeling -- an active subarea of the DataBase research. The corresponding theory developed in the DB community is a diverse collection of awkward pseudo-formal constructs, semi-formal correct specifications (whose precise counterparts are however known in Category Theory long ago), and also deep insights elaboration of which seems can contribute to CT itself. In particular, the following categorial construct which I'd call a {\em bounded power-object} is extremely useful in DB theory and my question is whether it was explored by anybody before. DEFINITION 1. A category ${\cal C}$ is said to have {\em bounded power-objects} if any jointly monic pair (relation), f:R-->a, g:R-->B, can be extended to the following commutative diagram (PDiag): B===B where the square (r,s,n,f) is pull-back ^ ^ and (s,e) is jointly monic. e| | s | | P<---E |g ^ ^ | r| |n | | | | A<---R===R f In addition, this augmentation enjoys the following universal property: for any other similar augmentation of (f,g): (PDiag') with P',E',r' etc instead of P,E,r etc. there are uniquely determined arrows u1:P-->P' and u2:E-->E' commuting the entire diagram (PDiag)+(PDiag'). It is easy to prove that bounded power-objects are unique up to isomorphism. So, given an object B, there is no the universal power-object of the object B, ${\bf P}B $, but for any relation R=(f,g) with B a domain there is the R-specific power-object ${\bf P}_{R}B $. Thus, B has many power-objects indexed by relations to B. Of course, if ${\cal C}$ is cocomplete they can be joined into the universal power-object of B but unbounded cocompleteness is just the property we wish to avoid. DEFINITION 2. {\em A bounded topos} is a category with finite limits and finite colimits which has bounded power-objects for all jointly monic pairs of arrows. REMARK 1. I do not familiar with Mikkelsen's proof that finite limits and power-objects imply finite colimits so I do not know to what extent the finite colimits condition can be relaxed. REMARK 2. The concept of bounded topos constitutes a natural universe for computationally feasible set theory. Indeed, bounded power-sets are tractable (ie, within the polynomial time computability) in contrast to intractability of finitary yet unbounded powersets. QUESTION: What is known about bounded toposes? What is known about complexity evaluations of topos-theoretic operations? CONCLUDING REMARK. The interplay between computational and descriptional complexities is one of the most nice and exciting hot topics of the modern model theory. It seems that exploring the interplay between two hierarchies when the descriptional one is specified in the language of graph-based topos-theoretic operations will be of equal beaty but simultaneously of a much more immediate practical impact. Grateful for any comments and remarks, Zinovy Diskin Date: Tue, 23 May 1995 00:53:07 -0300 (ADT) Subject: Combinators in the effective topos Date: Mon, 22 May 1995 14:55:23 -0400 From: Peter Freyd I'm having trouble interpreting the question posed by Justin Pearson. If N is the natural numbers object then it certainly has a fixed-point-free self-map, which gives me trouble in figuring out what's meant by "every map from N to N can be factored into S and K." Date: Tue, 23 May 1995 00:54:57 -0300 (ADT) Subject: [Q] Modified notion of epi Date: Mon, 22 May 1995 12:50:01 -0700 From: Andrew Ensor In any category the pullback of a monic is monic, but this does not hold for epis. However in the category Sets (or in an abelian category) the pullback of a surjective function is surjective. Is there another notion of "epi" for categories that is preserved by pullbacks, and that is surjectivity in the category Sets? Andrew Ensor. Date: Tue, 23 May 1995 09:40:47 -0300 (ADT) Subject: Diskin's question Date: Tue, 23 May 95 10:01 BST From: Dr. P.T. Johnstone I don't have a direct answer to Diskin's question, but here are a few immediate comments about it. 1. I'm not happy with the terms `bounded power-objects' and `bounded topos', because `bounded' has another meaning in topos theory (bounded geometric morphisms) and I sense that this could lead to confusion. It seems to me that something like `local power-objects' would be a better name for the concept Diskin describes ... but of course `local' is also a word which is already heavily used by topos-theorists. 2. I presume that the universal property of the bounded/local power-object, as described by Diskin, is the wrong way round: that is, one wants (P,E) to be terminal rather than initial in the category of diagrams of the form (PDiag). (If you ask for an initial object, then the problem always has a trivial solution: take P = A and E = R.) 3. Assuming I'm right about (2), then the condition that an object B has bounded power-objects is equivalent to saying that the functor Rel(-,B) is multi-representable in the sense of Diers (rather than representable, as it would be in a topos). There is a considerable literature (much of it written by Diers, but some by other people including myself) about multi-representability, multi-limits and the like; but I don't think any of it addresses the multi-representability of this particular functor. 4. I'd find it a lot easier to think about the problem if I had a simple example of a category (other than a topos) with this property, on which to test my ideas. Does Diskin (or anyone else) have such an example? Peter Johnstone Date: Tue, 23 May 1995 09:42:35 -0300 (ADT) Subject: APCS questionnaire Date: Tue, 23 May 95 10:05 BST From: Dr. P.T. Johnstone I thought I should let people know that, a few days ago, I received a paper to referee for Applied Categorical Structures -- and it came without that stupid questionnaire! So: thanks to all those who took the trouble to send messages to Kluwer; they did have an effect. Peter Johnstone Date: Tue, 23 May 1995 09:44:59 -0300 (ADT) Subject: Re: [Q] Modified notion of epi Date: Tue, 23 May 1995 09:38:33 +0000 From: Steve Vickers >Is there another notion of "epi" for categories that is preserved >by pullbacks, and that is surjectivity in the category Sets? Effective descent morphisms. (See Carboni, Janelidze, Kelly and Pare, "On localization and stabilization for factorization systems".) p: A -> B in C (with finite limits) is effective descent iff the pullback functor between slice categories, p*: C/B -> C/A, is monadic. In any topos, effective descent = epi. Steve Vickers. Date: Wed, 24 May 1995 00:12:38 -0300 (ADT) Subject: the other short answer Date: Tue, 23 May 1995 10:31:04 -0400 From: Peter Freyd Mike Barr writes: The short answer is that only split epis (those with a right inverse) are preserved under pullbacks in "all" categories. Well, yeah. But there is another short answer. I didn't know how to answer the original note without sounding stupid. I still don't. But there have been those who have given names to just those epis that are preserved under pullback, the most popular being "stable epis." So: The short answer is that only stable epis (those preserved by pullbacks) are preserved under pullbacks. Sorry about this. Anyway: split implies stable. Date: Wed, 24 May 1995 10:52:02 -0300 (ADT) Subject: Re: [Q] Modified notion of epi Date: Wed, 24 May 1995 12:42:30 +1000 From: Ross Street >>Is there another notion of "epi" for categories that is preserved >>by pullbacks, and that is surjectivity in the category Sets? Of course, split epis (= retractions) will answer this if Set has choice. --Ross Date: Wed, 24 May 1995 17:51:24 -0300 (ADT) Subject: Re: question about bounded toposes Date: Wed, 24 May 95 18:41:47 +0300 From: Zinovy Diskin Dear All, I must apologize: the universal property of (PDiag) described in my previous definition of bounded power-object is evidently not suitable (thanks to Peter Johnstone) and terminality of (P,E) is also not suitable: take for P' a superobject of A and for E' a relation from A' to B which is a "conservative" expansion of R -- then there are no canonical arrows from P' to P (and from P to P' too). So, actually the question is open which universal property of (PDiag) provides intended semantics of the construction. Zinovy Diskin Date: Thu, 25 May 1995 17:45:27 -0300 (ADT) Subject: Effective topos. Date: Thu, 25 May 1995 14:55:29 +0100 From: Justin Pearson Some people have been confused by my question. This probally reflects a confusion on my part. There are two seperat parts. i)In the effective topos, given the internal defn. of S and K on N. Can every map form N to N be written as arbitary (fintie) words over S and K. I.E. given f:N -> N, can f be writen as some word f=S^a;K^b;S^c;K^d ... for a,b,c,d, ... > 0? ii) If (i) is true, then can we turn it around on its head and use it as a definition of the natural number object N in Eff? But as Rosolini pointed out there is a problem, do I mean every PARTIAL map can be factored? Hope this helps, sorry about the confusion, but as I have said it is all probally due to me. Regards Justin Pearson Date: Fri, 26 May 1995 11:00:17 -0300 (ADT) Subject: S,K,N Date: Thu, 25 May 1995 22:19:00 -0400 From: Peter Freyd With respect to the question from Justin Pearson, my point remains. Since the 1930's it has been the case that if every function from A to A can be written as a combination of S's and K's then every function from A to A has a fixed point. (Note the word "combination" not just the special case thereof, "word".) Date: Fri, 2 Jun 1995 09:50:50 -0300 (ADT) Subject: garbled paper Date: Wed, 31 May 95 13:44:12 EDT From: Michael Barr It has just come to my attention that my paper, *-Autonomous categories and linear logic, that appeared in Vol 1 of MSCS got garbled. Virtually all occurrences of ^\bot appear to have been changed to ~\bot so that instead of V^\bot, you get V \bot (with extra space). The only exceptions occur when the ^\bot immediately follows a close parenthesis. I had sent them a TeX file, so there is no excuse for this change, which was doubtless made by an editorial assistant because they thought they were improving the paper. What it does is make it almost impossible to make sense of. I am astonished that in five years, nobody brought it to my attention. The corrected paper (with one or two cosmetic changes to kill overfull boxes) is about to be posted on my ftp directory. Note also that the theorem numbering scheme has changed, back to what it was in the original, but they no longer conform to the printed version. Michael Date: Fri, 2 Jun 1995 09:49:36 -0300 (ADT) Subject: Dana Scott receives Honorary Degree from Edinburgh Date: Wed, 31 May 1995 13:06:40 +0100 From: mikef@dcs.edinburgh.ac.uk Apologies if you've already seen this... > > +++++++++++++++ > + Dana Scott + > +++++++++++++++ > > Celebration of Honorary D.Sc. > ============================= > > Edinburgh, 13th - 14th July 1995 > > Invitation > ========= > > The University of Edinburgh will honour Prof. Dana Scott, > of Carnegie Mellon University, USA, with the Honorary Degree of > Doctor of Science, on 12th July 1995. > > We take great pleasure in inviting friends and colleagues to join > in an informal celebration of this award, which we will hold in Dana's > honour on 13th and 14th July 1995. > > Lectures and reception will be held in the James Clerk Maxwell > Building on the Science Campus (King's Buildings) of > The University of Edinburgh, > Edinburgh > EH9 3JZ. > > For further information please reply with > full postal address to tlc@dcs.ed.ac.uk. We regret that we will be unable to make any financial contributions towards travel and accommodation. For making accommodation arrangements please refer to http://www.dcs.ed.ac.uk/lfcsinfo/miscellaneous/accommodation-list.html ------------------------------------------------------------------------------- Prof. Michael P. Fourman, Laboratory for Foundations of Computer Science, University of Edinburgh, King's Buildings, Mayfield Road, Edinburgh EH9 3JZ Scotland, UK. email : Michael.Fourman@ed.ac.uk Tel: (+44)131-650-5197 Fax : (+44)131-667-7209