February 2001 - Categories - categories.org.au

2nd announcement: meeting at Stanford
by Rick Jardine 01 Mar '01

01 Mar '01

Second Announcement: Conference on Algebraic Topological Methods in Computer Science Department of Mathematics Stanford University July 30 - August 3, 2001 The application of algebraic topological methods in areas related to Computer Science is an emerging field that is of interest to both pure and applied mathematical scientists. The aim of this conference is to describe recent advances, and define the fundamental open problems in the field through a mixture of expository and technical lectures. There will be twenty-one main lectures, on a variety of topics in the area. This meeting has been funded by grants from Hewlett-Packard and the National Science Foundation. The following mathematical scientists have agreed to speak: John Baez (Math, UC Riverside) Marshall Bern (Xerox PARC) Anders Bjorner (Royal Institute of Technology, Stockholm) Tamal Dey (CS, Ohio State) Herbert Edelsbrunner (CS, Duke) David Eppstein (CS, UC Irvine) Michael Freedman (Microsoft) Philippe Gaucher (CNRS, Strasbourg) Eric Goubault (Commissariat a l'Energie Atomique, France) Jean Goubault-Larrecq (ENS Cachan) Marco Grandis (Dip. di Mat., Genova) Jeremy Gunawardena (HP BRIMS) John Harer (Math, Duke) Joel Hass (Math, UC Davis) Maurice Herlihy (CS, Brown) Reinhard Laubenbacher (Math, NMSU) Laszlo Lovasz (Microsoft) Vaughan Pratt (CS, Stanford) Christian Reidys (Los Alamos National Lab) Bernd Sturmfels (Math, UC Berkeley) Noson Yanofsky (CS, Brooklyn College) The organizers for this meeting are: Gunnar Carlsson, gunnar(a)math.stanford.edu Rick Jardine, jardine(a)uwo.ca We ask that all participants register for the meeting. The latest information and all registration forms are available at the Stanford Conference Web Site (http://math.stanford.edu/atmcs/index.htm) A limited amount of time at the meeting will be devoted to short talks by conference participants. If you would like to give a short presentation, please send an abstract to gunnar(a)math.stanford.edu. There will be a volume of proceedings for the conference, to appear in the journal "Homology, Homotopy and Applications", with Gunnar Carlsson as senior editor. Submissions for this volume should be set in LATEX and should be sent to gunnar(a)math.stanford.edu, to arrive by Friday, August 17. We are interested in expository papers on particular areas of application of topology, as well as research papers. There will be housing for conference participants on the Stanford campus, at the rate of about 50.00 US per night for single accomodation: a reservation form is available at the Stanford Conference Web Site. There are also several hotels in the area - see the Stanford site for a list. Limited financial support may be available for travel and housing: please make your request when registering.

1 0

connectedness/intuitionistic logic
by paolo torrini 28 Feb '01

28 Feb '01

I am looking for information about work on the representation of topological properties (esp. connectedness) using intuitionistic logic. I presently know about definitions of connectedness in "Sheaves and Logic" (Fourman-Scott 79) and "Formal spaces" (Fourman-Grayson 82). I would be interested in knowing whether there has been more work, esp. whether there is something that may have some relation with discrete geometry. Thank you for your help, Paolo -- Paolo Torrini School of Computing Leeds 0113 233 5684

1 0

CALL FOR REGISTRATION: ESSLLI 2001 (Helsinki, Finland)
by Ahti Pietarinen 27 Feb '01

27 Feb '01

- Apologies for multiple copies - If you want to receive detailed information including the ESSLLI 2001 poster please send us (esslli(a)helsinki.fi) your complete address. !!!!!!!!!!!!!!!!!!!!!!!!!! CALL FOR REGISTRATION !!!!!!!!!!!!!!!!!!!!!!!! 13th European Summer School in Logic, Language and Information ESSLLI 2001 University of Helsinki FINLAND August 13-24, 2001 http://www.helsinki.fi/esslli ** Early registration deadline: 30 April 2001 ** GENERAL INFORMATION The 13th European Summer School in Logic, Language and Information (ESSLLI'01) will take place at the University of Helsinki, Helsinki, Finland, during two weeks in August, from August 13 until 24. The ESSLLI Summer Schools are organised under the auspices of FoLLI (http://www.folli.uva.nl) the European Association for Logic, Language and Information. The main focus of the European Summer Schools is the interface between linguistics, logic and computation. Foundational, introductory and advanced courses, workshops and special events cover a wide variety of topics within six areas of interest: * Logic * Language * Computation * Logic and Language * Logic and Computation * Language and Computation The number of courses offered is over 50. Previous summer schools have been highly successful, attracting around 500 students from Europe and elsewhere. The school has developed into an important meeting place and forum for discussion for students, researchers and IT professionals interested in the interdisciplinary study of Logic, Language and Information. In addition to courses, workshops and evening lectures there will be a Student Session and a social program. COURSE PROGRAM The full scientific program can be found at our home page. Evening Lectures are given by * Edward L. Keenan "Spinoza Lecture" (UCLA) * Yannis Moschovakis "Vienna Circle Lecture" (UCLA) * Keith Devlin (Saint Mary's College, California) * Jaakko Hintikka (Boston & Helsinki) * Bonnie Webber (Edinburgh) WORKSHOPS There are currently several Calls for Workshop Papers. Please visit our home page for detailed information. TRAVEL AND LOCAL INFORMATION By plane to Helsinki airport and then a 30-minute nonstop coach or taxi service to the main railway station. From the railway station 5-minute walk to the university. A gateway between East and West, the city of Helsinki (population 1M) is the capital of Finland and one of the nine European Cities of Culture for the millennium. It is located at the warm and sunny south coast of Finland, within an easy reach from the main airports worldwide, or inside Europe by car or regular train services, or using the ferry services operating within the Baltic region. The scientific program of ESSLLI'01 will be held in the University Main Building, located on the University city campus at the very centre of Helsinki. The accommodation will be arranged at the University Summer Hotel close to the city campus. The accommodation includes sauna and breakfast. REGISTRATION ESSLLI 2001 is now open for registration. The registration fee for students is just ECU 190, for scholars ECU 350, and for industrial affiliates ECU 600. Please visit our home page for the on-line registration form and detailed instructions. ** Early registration deadline: 30 April 2001 ** All participants will get a letter of invitation to facilitate the procedure of getting a visa. GRANTS There will be a limited number of grants available, to partially support travel, registration and accommodation for ESSLLI'01. Instructions for grant applications are found at our home page. ** Deadline for grant applications: 31 May 2001 ** SPEACIAL EVENTS During ESSLLI, special "Finnish for Foreigners" language courses will be organised, as well as various excursions and other social events. Helsinki Summer School (http://summerschool.helsinki.fi) will offer special deals for ESSLLI participants who want to choose some of their courses and earn credits. SATELLITE EVENTS The Association for the Mathematics of Language will stage its annual meeting (MoL7) in conjunction with ESSLLI'01 in Helsinki, in the weekend preceding ESSLLI in August 10-12, and the affiliated Formal Grammar Conference will be held in conjunction with the Mathematics of Language Conference. ESSLLI participants are entitled to reduced registration fees. PROGRAM COMMITTEE Marcus Kracht (Chair) <kracht(a)math.fu-berlin.de> Jouko VÃ¤Ã¤nÃ¤nen (Logic) Bonnie Webber (Language) Claude Kirchner (Computation) Michael Moortgat (Logic and Language) Steffen HÃ¶lldobler (Computation and Logic) Claire Gardent (Language and Computation) CONTACT ADDRESSES Please visit ESSLLI'01 Home Page http://www.helsinki.fi/esslli for updated information concerning the scientific program, registration fees and procedures, grants, accommodation, satellite events, and other practical information. For further enquiries concerning ESSLLI'01, please contact the Organising Committee at <esslli(a)helsinki.fi>, or write to ESSLLI 2001 Secretariat C/o Department of Philosophy P.O. Box 24 00014 Helsinki University Finland ESSLLI'01 is organised by the Department of Philosophy (coordinator), the Department of Mathematics, the Department of General Linguistics, and the Department of Computer Science at the University of Helsinki. ORGANISING COMMITTEE Gabriel Sandu (Chair, Philosophy) Jouko VÃ¤Ã¤nÃ¤nen (Mathematics) Fred Karlsson (General Linguistics) Ilkka Niiniluoto (Philosophy) Martti Tienari (Computer Science) Ahti Pietarinen (Philosophy, secretariat) <esslli(a)helsinki.fi> ================================================================================

1 0

job: Postdoc available
by Mark D Ryan 27 Feb '01

27 Feb '01

[apologies for multi-post] Dear Colleague, I would be very grateful if you would forward this email to finishing or recently-finished PhD students. The University of Birmingham, UK, has a post-doctoral position to offer involving Applications of formal logic, in particular temporal logic, to problems in telecommunication systems. The job would suit someone with a PhD in formal methods or logic, who is interested in developing and applying verification techniques in a setting of industrial relevance and importance. We offer a good research environment, and the job can be moulded to suit your preference in terms of theory vs applications. Informal enquiries welcome. ===== THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Postdoctoral Research Fellow Applications are invited for a Postdoctoral Research Fellow to work on the project `The Feature Construct in Programming and Specification Languages', funded by EPSRC and British Telecom, coordinated by Dr. Mark Ryan and Dr. Marta Kwiatkowska. Applicants should have a PhD in Computer Science and ideally have some knowledge of one or more of the following areas: model checking, temporal logic, and/or program semantics. The successful applicant may be expected to contribute to teaching in the School up to a maximum of two hours per week on average. More information about the project, the research group and the School can be obtained from the URLs: www.cs.bham.ac.uk/~mdr/fc www.cs.bham.ac.uk The starting salary will be up to 19,482 pounds per year. The post is for three years from 1 April 2001 or as soon as possible thereafter. Application forms and further particulars available from: The Director of Personnel Services The University of Birmingham Edgbaston, Birmingham, B15 2TT tel: + 44 (0)121 414 6486 (24 hours) email: h.h.luong(a)bham.ac.uk Application forms are available from the WWW, at www.bham.ac.uk/personnel/app.htm Please quote reference S35522/01. The closing date for applications is Monday 19th March 2001. Late applications will be considered if the selection process has not advanced too far. Informal enquiries are welcome, and should be addressed to: Mark Ryan, tel: +44 (0)121 414 7361, email: M.D.Ryan(a)cs.bham.ac.uk. The University of Birmingham is working towards equal opportunities. ------- end -------

1 0

Re: Mike Healy's question about AI and math
by zdiskin 26 Feb '01

26 Feb '01

The discussion around the question in Re:above is expired but it seems not too much was said that might be directly related to problems in the applied domains in question and, thus, be really understood and appreciated by the corresponding part of the audience. Bill Lawvere is of course right in his << strong advice to actually learn some category theory, rather than resting content with slinging back and forth ill-defined epithets like "set theory", "contingency", etc >> but still there are no King's ways in math, and learning CT, as any other rich math discipline, needs efforts and time. Well, efforts and time is not a problem for students but a working specialist will reasonably require a certain motivation and justification for investing his resources into CT-studies. No doubts, the best justification is a host of examples of real successful applications ("success stories"), and in a discussion in this list in 1997 few were described. However, the NCDoms (Newly Created Domains as Lawvere called them) is an enormous territory and a few discrete example in particular areas do not set enough motivation/justification for the entire region. What is needed is a representative net of examples but still we have no it. So, for a while, a discrete set of new examples, and substantial conceptual / theoretical considerations too, would not be useless and a few were presented in the discussion. I'm afraid however that for a non-CT-part of the audience the arguments may seem far too general and/or too abstract, and we again come to the same issue at the beginning of the posting... There is a general problem of applying math to engineering domains and, correspondingly, of interaction between mathematicians and engineers. The former must respect a lot of formal details (in order to exist, the construction has to be formally consistent) and hence must go into the depth of consistent formalization. The latter must respect a lot of obstacles of the real world (to exist, the construction has to work) and hence must go into the width of functioning in the real world. Amalgamation of math depth with engineering width is a non-trivial task that needs working out a spacious array of details (every mathematician who ever tried to work in an industrial environment knows it) but at the end you have some kind of 3D vision beneficial for the both sides. (This general opposition "depth vs. width" in the case of "Math vs. NSDs" has some quite concrete technical aspects, see below). In these terms, an overall picture appeared in the discussion so far is somewhat like a discrete collection of bore-pits (well, they are connected at a depth, but it's hardly visible from the surface). To get a presentation more relevant for NCDs, I've tried to write a text integrating these pits into something wider ("a foundation pit" :). That is, I've tried (i) to trace some of the lines appeared in the discussion and add a bit of engineering width to them, (ii) to integrate them into an observable picture, (iii) to make some details a bit more understandable for the "foreign" part of the audience (and probably annoying for the "native" part so that my head is on the two platters simultaneously), and finally (iv), to explain something for myself. The resulting text turned out very bulky and can be found on http://www.cs.kuleuven.ac.be/~frank/Diskin.ps (thanks to Frank Piessens for hospitality). Below is a brief summary of the text and the table of contents to look thru before starting, or not starting, the tour. Regards, --Zinovy Diskin BRIEF SUMMARY (I) OBSERVATION. In many newly created domains (NCDs) they deal with a stuff in much similar to that managed in mathematics. Like a mathematician, an NCD-specialist deals with design (definition), presentation and reasoning about structures modeling a piece of reality (material, informational, "computeral") in an abstract way, suppressing some details (irrelevant for the model) and explicating others (important but often residing in intuition / default assumptions and therefore implicit). Hence, to look for a suitable math framework(s) for NCDs, one should look at *meta*mathematics -- a part of mathematics aimed at modeling mathematics by mathematical means. (II) OBSERVATION. Category theory (CT) is, in essence, a consistent *meta*mathematical framework where relations, manipulations and transformations of / between math structures are considered in an abstract and precise way. In a sense, CT is a discipline and framework for mathematical structure engineering. It is abstract enough to provide an extreme flexibility and simultaneously concrete enough to discover CT- structures in applications in a quite immediate way. In addition, this framework is essentially algebraic (and in some precise sense too), well structured itself and hence is quite manageable and effective. (III) It follows from (I) and (II) that CT appears to be a good candidate for an integral math framework, and effective machinery too, for applications in NCDs. Of course, in each particular context suitable CT-patterns should be found and adjusted, and their match with NCDs-structures to be managed should be checked. An example (rough sketch) of such an activity for the case of software engineering is presented below. (IV) OBSERVATION: CT vs. SE (software engineering in a wide sense including business modeling and knowledge representation). It appears that some of major mechanisms invented (and implemented!) in SE to manage the complexity of structures involved -- object orientation, set orientation, graphic notations, multi-level system architectures -- are based on ideas very close to those developed in CT. To wit: object and set orientations together appear as a kind of SE-realization of the arrow thinking underlying CT, and graph-based syntax and multi-level organization of the CT-stuff are evident and speak for themselves. (V) SPECULATION. While the theoretical part of the NCDs community is discussing whether CT is relevant or not, the (software) engineering part is already using categorical, in essence, ideas in a implicit way. Nothing surprising: the same goal of building a framework where complex structures (computational and specificational) could be managed in a systematic and effective way has led engineers and mathematicians to close results. Making this implicit partnership explicit would benefit the both sides. END OF SUMMARY CT as a mathematical framework for software engineering, AI, cognitive science, and other newly created domains (NCDoms). http://www.cs.kuleuven.ac.be/~frank/Diskin.ps Table of contents. 1 About NCDoms. 1.1 NCDoms as mathematics. 1.2. Peculiarities of NCDoms' mathematics: length and width vs. depth. 1.3 SE's mechanisms to manage complex structures. 2 CT in a SE-View: Object-Oriented, Setwise And Graph-Based Mathematics with Multi-Level Architecture. 2.1 CT as OO-language: Math structures via arrows. 2.2 CT as a setwise language. Toposes. 2.3 CT as a graphic language. Sketches. 2.4 CT as a language for multi-level specifying architectures. 3 CT vs. SE. 3.1 Graphic notation and sketches. 3.2 CT as an integral specification framework. 3.3 Three final remarks. REFERENCES Appendix O. MODELING AND MATHEMATICAL MODELING O.1 General schema of modeling (something by something) O.2 Examples O.3 Some peculiarities of applying math to natural sciences O.3.1. Semi-formal deduction. O.3.2 "Unreasonable effectiveness". Appendix A. MECHANISMS FOR MANAGING NCDs' STRUCTURES A.1 Object orientation. A.2 Set orientation. A.3 Graphic syntax of specification languages: Notational Babylon A.4 Multi - level specification architectures. A.5 The challenge of integration. Appendix B. ABOUT METAMATHEMATICS B.0 "Business structure" of meta-mathematics. B.1 Metamath I: CatST vs. FrmST. B.2 Metamath II: CatLogic vs. Tarskian MetaMath. B.3 Metamath III: abstract mathematical structures engineering. B.A(ppendix): Bourbakian way of setting math structures and CT. Appendix C. CT vs. SE: EXAMPLES C.1 Relations: Categorical vs. Element-oriented treatment C.2. Semantic database theory: Toposes and Database design. C.3 Whether schema integration is an associative operation?

1 0

job: Research job in model checking application
by Mark D Ryan 22 Feb '01

22 Feb '01

Job opportunity * Model checking * flexible balance of theory/applications, to suit applicant * good research environment * ability more important than relevant experience * informal enquiries welcome THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Postdoctoral Research Fellow Applications are invited for a Postdoctoral Research Fellow to work on the project `The Feature Construct in Programming and Specification Languages', funded by EPSRC and British Telecom, coordinated by Dr. Mark Ryan and Dr. Marta Kwiatkowska. Applicants should have a PhD in Computer Science and ideally have knowledge of one or more of the following areas: model checking, temporal logic, and/or program semantics. The successful applicant may be expected to contribute to teaching in the School up to a maximum of two hours per week on average. More information about the project, the research group and the School can be obtained from the URLs: www.cs.bham.ac.uk/~mdr/fc www.cs.bham.ac.uk The starting salary will be up to 19,482 pounds per year. The post is for three years from 1 April 2001 or as soon as possible thereafter. Application forms and further particulars available from: The Director of Personnel Services The University of Birmingham Edgbaston, Birmingham, B15 2TT tel: + 44 (0)121 414 6486 (24 hours) email: h.h.luong(a)bham.ac.uk Application forms are available from the WWW, at www.bham.ac.uk/personnel/app.htm Please quote reference S35522/01. The closing date for applications is Friday 9th March 2001. Late applications will be considered if the selection process has not advanced too far. Informal enquiries are welcome, and should be addressed to: Mark Ryan, tel: +44 (0)121 414 7361, email: M.D.Ryan(a)cs.bham.ac.uk. The University of Birmingham is working towards equal opportunities.

1 1

Book Announcement: Galois Theories
by Cathy Siddiqi 21 Feb '01

21 Feb '01

I would like to post the following annoucement for your category theorists. Galois Theories by Francis Borceux and George Janeldize Starting from the classical finite-dimensional Galois theory of fields, this book develops Galois theory in a much more general context. The authors first formalize the categorical context in which a general Galois theorem holds, and then give applications to Galois theory for commutative rings, central extensions of groups, the topological theory of covering maps and a Galois theorem for toposes. The book is a hardback, 360 pages, and costs $74.95 (50.00 in UK). For more information about the book, or to order a copy, please visit www.cambridge.org. Please let me know if you need additional information from me Thanks, Cathy -- Cathy Siddiqi Marketing Associate Cambridge University Press 40 West 20th Street New York, NY 10011 212-924-3900 x323 212-691-3239 fax

1 0

Jon Beck's thesis
by Michael Barr 21 Feb '01

21 Feb '01

Does anyone have a copy of Jon Beck's thesis? I have received a request from a Georgian mathematician (the editor and founder of Homology, Homotopy and Applications) who has no access to foreign exchange for a copy. I have looked and I do not have one, although I must have once. Actually, I don't have a copy of my own thesis (and they have disappeared from the Penn library). Michael

1 0

toposes vs. sets - another aspect
by Thomas Streicher 20 Feb '01

20 Feb '01

I want to take up the discussion on ``toposes vs. sets'' from another point of view. Over the years a few questions have accumulated and I'd be interested in the opinion of the experts. As Bill Lawvere has pointed out in his reply to the original question there are several meanings in which one can understand the relation ``toposes vs. set theory''. One such distinction is static sets vs. variable sets and one can hardly deny that the latter are of enormous importance for understanding modern mathematics from a conceptual point of view. That's probably what most categorists have in mind when they defend categories as superior to traditional set theory. Another argument probably is that the official language of axiomatic set theory is most inconvenient for actual formalisation of mathematics. One knows that in principle one always can eliminate function symbols in favour of relation symbols but that leads to an explosion of length of formulas and ends in something fairly uncomprehensible.Thus, categorists and also quite a few logicians are in favour of formal systems based function application and predication instead of using just one single relation \epsilon besides equality because function application and predication are the basic constitutents of actual mathematical statements and, moreover, appear most naturally from the categorical notion of topos. In the end this amounts to the point of view that HAH (Higher Order Arithmetic), the internal language of the free topos with NNO, is the formal system which is most suitable for formalizing mathematics (if one wants to embark on such an endeavour at all). Well, but there are some reasons why HAH may be considered as non-sufficient at least from a logical point of view. As Zermelo-Fraenkel set theory ZF(C) and, actually, already Zermelo's Set Theory Z(C) prove the consistency of HAH and accordingly they are non-conservative extensions of HAH. Well, one might argue that this lack of conservativity only affects "meta-statements" and not ``real mathematical statements''. Even hard boiled set theorists would admit that "99% of modern mathematics can be formalised in HAH" (such a statement for Zermelo's Z(C) instead of HAH can be found e.g. in Kunen's monograph on set theory). However, there do exists natural mathematical statements which can be formulated in the language of HAH but proved only in ZF though they are fairly different in character from ``meta-statements''. A typical such example is Borel Determinacy (BD) saying that for every Borel set X in Baire space either player or opponent has a winning strategy for the game G_X where in each step each player plays a natural number and in the end (after \omega steps) player has won if and only if the resulting sequence of numbers lies in X. >>From this point of view I think one can hardly insist that HAH is the ultima ratio as it prevents us from proving meaningful statements which can be formulated in HAH. Of course, one might still have in mind an open-ended axiomatization of HAH where one adopts an axiom, as e.g. BD, whenever convenient. This seems to be the attitude for example in SDG where one postulates by need axioms ensuring the existence of particular functions such as cos and sin instead of constructing them via some series. It seems to me that such an attitude is absolutely ok as long as one is interested only in appropriate formalism for expressing mathematical facts and not in the strength of axiomatizations. However, if one wants to arrive at a formal system which allows one to derive (in principle) "all current mathematics" then I think one has to accept that HAH is not satisfactory simply because it is too weak. On the other hand it still is the case that traditional syntax of ZF is not very convenient as a formalisation of mathematical practice. Therefore, it might be worthwhile to look for formal systems of a type-theoretic character equiconsistent to ZF(C) and including ZF(C) via translation. Well, such a language is available, namely the so-called "Calculus of Inductive Constructions" an impredicative type theory with an infinite hierarchy of universes. This is described in Werner, Benjamin Sets in types, types in sets. Theoretical aspects of computer software (Sendai, 1997), 530--546, Lecture Notes in Comput. Sci., 1281, Springer, Berlin, 1997. ftp://ftp.inria.fr/INRIA/Projects/coq/Benjamin.Werner/zfc.ps.gz where one also can find (sketches of) proofs of the meta-theoretic properties mentioned above. The reason why systems like the "Calculus of Inductive Constructions" are as strong as ZF(C) is that they allow one to define FAMILIES of TYPES by structural recursion. which is precisely what the set theoretic axiom of replacement is good for. However, type theoretic language does bring this to the point more clearly than the set-theoretic axiom of replacement which is often used in mathematical practice to formulate the image of a function f : A -> B namely as { f(a) | a \in A} which certainly has to be considered as sort of an overkill because this can be formulated in HAH as well. The real strength of the axiom of replacement is used when defining `images of functions without a codomain' as e.g. families of sets indexed by some inductive type (e.g. an ordinal). The very purpose of type-theoretic universes is to provide a codomain for such `functions without codomain'. According to these observations I get the impression that what topos logic is missing is a concept of universe which allows one to define by recursion not only families of objects but also families of types. I want to conclude my remarks with a pointer to a recent paper by Alex Simpson on Solving Domain Equations in Models of Intuitionistic Set Theory (to be found at http://www.dcs.ed.ac.uk/home/als/Research/rde.ps.gz) where in the last paragraph of section 5 (p.12) he gives a counterexample to the claim that in a topos satisfying the usual axioms of SDT (Synthetic Domain Theory) one always can solve domain equations. The reason is that the topos considered there doesn't allow one to construct certain N-indexed families. (This is a style of argument well-known from the usual proofs in set theory showing that Z(C) is weaker than ZF(C)!) I hope that it has got clear from my formulations that I am not at all ``anti-category''. However, I always found it most confusing when in some texts on toposes I read the statement that the logic of toposes coincides with intuitionistic set theory. I think that most classically trained logicians get immediately puzzled by such statements because they know very well that set theory is stronger than type theory and, therefore, feel sort of repelled by such oversimplifying statements. Moreover, during the 90ies there have been developed fascinating categorical accounts of constructive set theory by Joyal, Moerdijk, Simpson, Butz and Palmgren. I think it would be an interesting question to clarify the relation between this account and the one by universes. Thomas Streicher

1 0

statecharts and categories
by Amiguet Matthieu 19 Feb '01

19 Feb '01

Dear Categoricians, I'm wondering if there has been any work in formalizing statecharts [1] in categorical terms. If not, do you know of an other algebraic description of this specification language? Also, it seems to me that the operationnal semantic STATEMATE of Statecharts as described in [2] is very coalgebraic in nature. Did anybody write something about this? Thank you for any information or pointer, Matthieu REFERENCES: [1] Harel, D. (1987) Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231--274. [2] Harel, D. and Naamad, A. (1996) The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology, 5(4), 293--333

2 1