January 2000 - Categories - categories.org.au

Grad positions available
by Richard Blute 01 Feb '00

01 Feb '00

The Logic Team at the Math Department of the University of Ottawa announces that it anticipates having one or more openings in its graduate program beginning in September. These would be at either the Master's or Ph. D. level, and would come with funding in the form of tuition and an additional stipend. The team is run by Phil Scott and Rick Blute, and specializes in the following areas: -linear logic -categorical logic and proof theory -category theory, especially monoidal categories -logic and foundations of computer science We have close affiliations with the University of Ottawa School of Information Technology and Engineering, as well as the Category Theory Research Centre in Montreal, and our students have many opportunities to interact with the members of these institutions. The Math Department at the University of Ottawa has a wide range of research interests and provides an excellent environment for graduate study. Students here also have the advantage of living in one of the most beautiful cities in Canada, and the national capital. For further information, please visit our website at www.science.uottawa.ca/mathstat, or contact Rick Blute at rblute(a)mathstat.uottawa.ca or Phil Scott at phil(a)mathstat.uottawa.ca.

1 0

2 on terminology (fwd)
by James Stasheff 29 Jan '00

29 Jan '00

.oooO Jim Stasheff jds(a)math.unc.edu (UNC) Math-UNC (919)-962-9607 \ ( Chapel Hill NC FAX:(919)-962-2568 \*) 27599-3250 http://www.math.unc.edu/Faculty/jds ---------- Forwarded message ---------- Date: Fri, 28 Jan 2000 12:26:36 EST From: DON DAVIS <dmd1(a)lehigh.edu> To: toplist <Distribution.List(a)lehigh.edu> Subject: 2 on terminology Two similar responses regarding simplicial terminology.....DMD ______________________________________________________ Date: Fri, 28 Jan 2000 08:56:36 -0600 (CST) From: Peter May <may(a)math.uchicago.edu> Subject: "Delta sets" Once upon a time, people doing category theory and algebraic topology overlapped with people doing geometric topology and algebraic topology. There is a large literature of $\triangle$-sets, or $\delta$-sets, which are precisely simplicial sets without degeneracy operations. I believe the term was introduced in the pair of papers listed in MathSciNet as "$\triangle$-sets. I II", by Colin Rourke and Brian Sanderson. Both papers were published in 1971, in the Quarterly Journal of Mathematics. The main point is that use of delta sets is essential to the theory of block bundles and thus to PL topology. Peter May ______________________________________________________________ Date: Fri, 28 Jan 2000 15:12:58 GMT From: Brian Sanderson <bjs(a)maths.warwick.ac.uk> Subject: Re: terminology. Delta sets. J. Stasheff wrote: >Has terminology settled down? >I can recall seeing various terms for >``simplicial object without degeneracies'' Colin Rourke and I called these sets Delta sets. Unfortunately you might have to look for "$\triangle" to find them. Prior to the two papers below they were a neglected curiosity. We needed them when block bundles emerged. I don't know how current the terminology is now. Brian Sanderson [7] 45 #9328 Rourke, C. P.; Sanderson, B. J. $\triangle $-sets. II. Block bundles and block fibrations. Quart. J. Math. Oxford Ser. (2) 22 (1971), 465--48 5. (Reviewer: E. B. Curtis) 55F60 [8] 45 #9327 Rourke, C. P.; Sanderson, B. J. $\triangle $-sets. I. Homotopy theory. Quart. J. Math. Oxford Ser. (2) 22 (1971), 321--338. (Reviewer: E. B. Curtis) 55F60 (55D99)

1 0

integrals
by Peter Freyd 29 Jan '00

29 Jan '00

Let I be a closed interval and let C(X) denote the bipointed midpoint algebra of continuous functions from a space X to I. I would not have guessed the following: 1. Any map from C(X) to C(Y) that preserves midpoints, top, and bottom is monotonic and preserves constant functions. The order preservation is an immediate consequence of: f =< g iff there exists h such that f|top = g|h If we specialize to the case that X and Y are single points, the order preservation implies the only map from I to I that preserves midpoints, top and bottom, is the identity map (after first noticing that it must have a dense subset of fixed points corresponding to the dyadic rationals). Let I -> C(X) be the "K-map" that assigns constant maps. For any y:Y let C(Y) -> I be its evaluation map. Then for any map C(X) -> C(Y) that preserves midpoints, top, and bottom we have that I -> C(X) -> C(Y) -> I is the identity map. And from that we can easily conclude that C(X) -> C(Y) preserves constant maps. In a 22 Dec posting I said that the "mean-value" function M:C(I) -> I can be characterized from its order preservation together with what it does to constant functions and MxM C(I v I) --> C(I + I) --> C(I) x C(I) ---> I x I C(F) | | m v v M C(I) -----------------------------------> I where F:I -> I v I is the coalgebra structure and m is the midpoint operation. I went on to say that if C(F) is inverted then this diagram can be read as a fixed-point definition of M: "It's the unique fixed-point of an operator acting on the set of all those order-preserving maps from C(I) to R that do the right thing on constant functions." It's much better to change the R to I and say just that it's acting on the set of bipointed midpoint-algebra homomorphisms. To recapitulate (using \ for lambda, T for top, B for bottom): 2. The mean-value operator, M:C(I) --> I, is the unique map such that: M(\x.B) = B M(\x.T) = T (Mf)|(Mg) = M(\x.(fx)|(gx)) Mf = (M(\x.f(B|x)))|(M(\x.f(x|T))) No inequalities, no limits, only equations. Let me take the occasion to do a little clean-up. In a 31 Dec posting I gave a curse-of-analysis proof for: 3. Midpoint-preserving functions between intervals are monotonic. Here's a much better proof. Monotonicity is equivalent to the preservation of betweenness. Suppose f is a midpoint-preserving map between intervals. It's conceptually useful to take the target to be, instead, the real line and show that a failure to preserve betweenness forces the values of f to be unbounded. So let a,b,c be points in the source interval with b between a and c which fact will be denoted as {a.b.c} and suppose that fb is not between fa and fc. Without loss of generality we can assume that {fa.fc.fb}. There exists {a.b'.c} such that either b = a|b' or b = c|b'. Each of the equations fb = fa|fb' and fb = fc|fb' implies {fa.fc.fb'}. So {a.b'.c} is still an example but the first equation implies that the distance from fc to fb' is twice -- and the second equation implies it is _at least_ twice -- the distance from fc to fb. By iteration we may thus increase that distance beyond any bound. A point that the previous proof didn't really cover is dispatched by this corollary: 4. Midpoint-preserving functions between intervals are either one-to-one or constant. Suppose a and c are distinct but fa = fc. If there's c' such that c = a|c' then we may infer that fa = fc'. By replacing c with c' in this manner as long as possible we may assume that a and c are such that there is no solution to the equation c = a|x and from that we may infer that if c' is chosen to be the endpoint such that {a.c.c'} then there is {a,b,c} such that c = b|c'. By the last result we have fa = fb = fc hence fc = fb = fc'. Thus we may assume that a and c are distinct with fa = fc and c an endpoint. Similarly we may assume that a is an endpoint and finish by applying, once again, the last result. Besides injectivity we have this corollary on surjectivity obtained by combining 1 and 3: 5. The image of any midpoint preserving function between intervals is a closed interval. PS >>From the proof of 1 it is clear that order preservation doesn't require preservation of bottom. A similar proof uses preservation of bottom instead of top, but if both conditions are dropped the map needn't even be monotonic. Let I = [-1,1] and let C(I) -> I be the map that sends f to f(-1)|(-f1). It sends all constant functions to 0, it sends the identity map to -1 and it sends the negating map to 1.) The proof of 3 suggests that if the target interval is replaced by the reals then there do exist midpoint-preserving maps that are not monotonic. And that is, indeed, the case in the presence of the axiom of choice: view the reals as a rational vector-space and count the number of endomorphisms (each of which preserves midpoints) to find that there are 2^{2^N} of them. But there are only 2^N monotonic self maps (midpoint preserving or not). Do we need the axiom of choice? If, instead, we add the axiom of measurability, then the counterexamples disappear: let f be a measurable midpoint-preserving map from R to R; we can easily specialize to the case that f0 = 0, hence f is a measurable group endomorphism; for any real a consider the induced group homomorphism from R/aZ to R/(fa)Z; any measurable group character is continuous and that's enough to force f to be continuous.

1 0

ETAPS 2000 - Call for Participation
by Doris Faehndrich 29 Jan '00

29 Jan '00

(Sorry, if you receive multiple copies of this Call. Doris Faehndrich) ----------------------------------------------------------------- ETAPS 2000 - EUROPEAN JOINT CONFERENCES ON THEORY AND PRACTICE OF SOFTWARE Technical University of Berlin, March 25 - April 2, 2000 -------------------- CALL FOR PARTICIPATION ------------------------- Welcome to Berlin, welcome to ETAPS, the European Joint Conferences on Theory and Practice of Software, the european forum for academic and industrial researchers working on these topics! For 9 days you will be able to choose between 5 conferences with more than 120 regular papers and tool demonstrations covering a wide range of topics from theory and practice, 7 invited lectures, 10 tutorials, and 5 satellite events. -------------------------------------------------------------------- Please, check for details http://iks.cs.tu-berlin.de/etaps2000/ Use the option of online registration or one of the downloadable registration forms! -------------------------------------------------------------------- EARLY REGISTRATION UNTIL FEBRUARY 29, 2000 -------------------------------------------------------------------- Main Conferences, March 27 - March 31 ------------------------------------- CC 2000 International Conference on Compiler Construction Chair: David Watt (University of Glasgow, UK) ESOP 2000 European Symposium on Programming Chair: Gert Smolka (Saarland University, D) FASE 2000 Fundamental Approaches to Software Engineering Chair: Tom Maibaum (King's College London, UK) FOSSACS 2000 Foundations of Software Science and Computation Structures, Chair: Jerzy Tiuryn (University of Warsaw, PL) TACAS 2000 Tools and Algorithms for the Construction and Analysis of Systems, Chair: Susanne Graf (VERIMAG, Grenoble, F) Invited Speakers ---------------- Abbas Edalat (Imperial College, London, UK) ``A Data Type for Computational Geometry and Solid Modelling'' David Harel (The Weizmann Institute of Science, Rehovot, IL) ``From play-in scenarios to code: an achievable dream'' Martin Odersky (EPF Lausanne, CH) ``Functional nets'' Richard Mark Soley (OMG Object Management Group, USA) ``Memex isn't Enough'' Wladyslaw M. Turski (University of Warsaw, PL) ``An essay on software engineering at the turn of century'' Reinhard Wilhelm (Saarland University, D) ``Shape analysis'' Pierre Wolper (University of Liege, B) ``On the representation of constraints by automata in the verification of infinite systems'' Panel: ``Standard Components of the Shelf - Do they carry and need a (Formal) Standard Semantics?'' Chair: Herbert Weber (TU Berlin, D) Satellite Events ---------------- GRATRA - Joint APPLIGRAPH/GETGRATS Workshop on Graph Transformation Systems, Contact: Hartmut Ehrig (TU Berlin, D) March 25 - March 27 Invited Lecture by Grzegorz Rozenberg (University of Leiden, NL) ``DNA Computing in vivo and graph transformation'' (open for all ETAPS participants) CMCS - Workshop on Coalgebraic Methods in Computer Science Contact: Horst Reichel (TU Dresden, D) March 25 - March 26 CBS - International Workshop on Communication-Based Systems Contact: Guenter Hommel(TU Berlin, D) March 31 - April 1 INT - Integration of Specification Techniques with Applications in Engineering, Contact: Martin Grosse-Rhode(TU Berlin, D) March 31 - April 1 CoFI - Common Framework Initiative for Algebraic Specification and Development of Software Contact: Don Sannella (University of Edinburgh, UK) April 1 - April 2 Tutorials --------- XML for Software Engineers Andrea Zisman, Anthony Finkelstein (University College London, UK) March 25, p.m., half-day A tutorial on Maude Narciso Marti Oliet (Universidad Complutense, Madrid, E), Jose Meseguer (SRI International, USA) March 25, p.m., half-day Rigorous Requirements for Safety-Critical Systems: Fundamentals and Applications of the SCR Method Constance L. Heitmeyer (Naval Research Laboratory, USA) March 26, full-day Multi-Paradigm Programming Michael Hanus (RWTH Aachen, D) March 26, a.m., half-day Query-based Automated Debugging Mireille Ducasse (IRISA/INSA, F) March 26, p.m., half-day The Unified Modelling Language Perdita Stevens (University of Edinburgh, UK) April 1, full-day Swinging Types Peter Padawitz (University of Dortmund, D) April 1, a.m., half-day Tables and computation A.J.Wilder (University of Wales, UK) April 1, p.m., half-day SDL 2000 Joachim Fischer (HU Berlin, D), Andreas Prinz (Research Digital Media Systems GmbH, D), Eckhardt Holz (HU Berlin, D) April 2, full-day Software Metrology Basis Hans-Ludwig Hausen (GMD Bonn, D) April 2, a.m., half-day ------------------------------------------------------------------ ETAPS Steering Committee Don Sannella (Chairman, UK), Egidio Astesiano (I), Jan Bergstra (NL), Pierpaolo Degano (I), Hartmut Ehrig (D), Jose Luiz Fiadeiro (P), Marie-Claude Gaudel (F), Susanne Graf (F), Furio Honsell (I), Heinrich Hussmann (D), Stefan Jaehnichen (D), Paul Klint (NL), Tom Maibaum (UK), Tiziana Margaria (D), Ugo Montanari (I), Hanne Riis Nielson (DK), Fernando Orejas (E), Andreas Podelski (D), David Sands (S), Gert Smolka (D), Bernhard Steffen (D), Wolfgang Thomas (D), Jerzy Tiuryn (PL), David Watt (UK), Reinhard Wilhelm (D) Organizing Chairs: Bernd Mahr, Hartmut Ehrig, Peter Pepper, Stefan Jaehnichen, Radu Popescu-Zeletin Conference Address: ETAPS 2000, TU Berlin, Sekr. FR 6-10, Franklinstr. 28/29, D-10587 Berlin Germany Tel: ++49 30 314 -73540, Fax: -73622 Email: etaps2000(a)iks.cs.tu-berlin.de http://iks.cs.tu-berlin.de/etaps2000/ Registration Address: BWO Marketing Service GmbH Mohrenstr. 63-64 D-10117 Berlin-Mitte Germany Fax: ++49 30 22 66 84-64 Email: Etaps2000(a)BWO-Berlin.de -=-=-=-==-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Doris FÃ¤hndrich: TU Berlin FB-13 Sekr. FR 5-6, Franklinstr. 28/29, 10587 Berlin, Tel: 030/31473436 -=-=-=-==-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

1 0

slogans
by Al Vilcius 29 Jan '00

29 Jan '00

As a bit of a fun project, I would like to put together a collection of slogans, and am asking for contributions. Such a collection may or may not turn out to be "useful", but at least it will be amusing. I'm thinking of a slogan (apart from being a Scottish Highland war-cry) as a pithy little phrase or saying or motto or truism ..., just short of being poetry, that can tweak the neural pathways to follow a previously traveled path of understanding. Slogans tend to be little gems, often found in the folklore, but sometimes published, such as the 5 slogans in Jim Lambek & P. Scott's "Intro to higher order categorical logic" - these are: I: many objects of interest in mathematics congregate in concrete categories. II: many objects of interest to mathematicians are themselves small categories. III: many objects of interest to mathematicians may be viewed as functors from small categories to Sets. IV: many important concepts in mathematics arise as adjoints, right or left, to previously known functors. V: many equivalence and duality theorems in mathematics arise as an equivalence of fixed subcategories induced by a pair of adjoint functors. I think there are many more such gems; I like (and use) the one that says: the arrows always go through the limit. - I attribute this one to Armin Frei circa 1971 at UBC. Another really good one is: adjoints are the unity and identity of opposites. - I attribute this one to Bill Lawvwere Here are a couple more, from the physics of information: * there is no information without representation. * there is no processing without a process. - attributed to Benjamin Schumacher of Kenyon College. Each slogan can explode into rich and meaningful ideas, sort of the "url's of the mind" (if you like that kind of cyber-geek talk). Anyway, I hope the intention is clear, and that everyone will contribute their favourites as well. Please either post a response or send to me directly (no flames please), along with appropriate credit if known; I will assemble, and depending on how it goes, make the collection available. Could be fun and interesting - I look forward to your responses. Best regards to all .... Al /\ / Al R. Vilcius, Canada / \ / mailto:al.r@vilcius.com /--->\ / Tel./FAX (905) 854-3342 /3371 / \/ web site: http://www.VILCIUS.com

3 2

abcd=cba
by James Stasheff 28 Jan '00

28 Jan '00

The pentagon relation abc=de occurs all over the place. I've just come across abcd = cba for the first time. Look familiar? .oooO Jim Stasheff jds(a)math.unc.edu (UNC) Math-UNC (919)-962-9607 \ ( Chapel Hill NC FAX:(919)-962-2568 \*) 27599-3250 http://www.math.unc.edu/Faculty/jds

1 0

terminology
by James Stasheff 28 Jan '00

28 Jan '00

Has terminology settled down? I can recall seeing various terms for ``simplicial object without degeneracies'' .oooO Jim Stasheff jds(a)math.unc.edu (UNC) Math-UNC (919)-962-9607 \ ( Chapel Hill NC FAX:(919)-962-2568 \*) 27599-3250 http://www.math.unc.edu/Faculty/jds

3 3

Freyd's couniversal characterization of [0,1]
by Martin H. Escardo 27 Jan '00

27 Jan '00

It would be interesting to test Freyd's couniversal characterization of the unit interval in many other categories. Here I test it in Top, the category of topological spaces and continuous maps, and various full subcategories, where one would hope to get the unit interval with the Euclidean topology. ---------------------------------------------------------------------- Summary of the outcome of some tests: (1) In Top, the final coalgebra for Freyd's functor exists. Its underlying object, however, is an indiscrete space (unsurprisingly). (2) In the category of T0 spaces, it doesn't exist. (3) In the category of normal spaces it does exist, and, as one would hope, its underlying object is indeed the unit interval with the Euclidean topology. See remark below for weakening normality in (3) as much as possible. ---------------------------------------------------------------------- Arguments follow. We work with the category BiTop of bipointed topological spaces, whose objects are topological spaces with two distinct distinguished points and whose morphisms are continuous maps that preserve the two distinguished points. Given a bipointed topological space x0,x1:1->X, one constructs a bipointed topological space FX as in the diagram below, where the square is a pushout. inr x1 FX <--------- X <---------- 1 ^ ^ | | inl | | x0 | | X <---------- 1 ^ x1 | x0 | | 1. Thus, FX is the quotient of the coproduct of two copies of X that identifies two points (x1 of the first copy with x0 of the second). It is clear how F extends to morphisms producing a functor BiTop->BiTop. (1)----------------------------------------------------------------- Is there a final coalgebra d:I->FI in BiTop? In BiSet, Freyd argued, one can take I=[0,1] with distinguished points 0 and 1 and structure map d defined by d(x) = inl(2x) if x<=1/2 inr(2x-1) if x>=1/2 Notice that for x=1/2 one gets inl(1)=inr(0), as one should. [[Incidentally, see M.H. Escardo and Th. Streicher. "Induction and recursion on the partial real line with applications to Real PCF", TCS 210(1999) 121-157. There, essentially the same definition gives a final coalgebra whose inverse is an initial algebra, but the underlying category is that of continuous Scott domains.]] By general trivial reasons, the same construction works in BiTop if one endows X with the indiscrete topology: Uniqueness and existence of a set-theoretic map follow by Freyd's argument, and any map with values in an indiscrete space is continuous. (2)------------------------------------------------------------------ Now consider the category of T0 spaces. For the sake of contradiction, assume that there is a final coalgebra d:X->FX where X has distinguished points x0 and x1. Let S be the space with two points 0 and 1 such that {1} is open but {0} is not (Sierpinski space). We use the facts that 0<=1 in the specialization order (every neighbourhood of 0 is also a neighbourhood of 1) and that continuous maps preserve the specialization order. Let A be S with distinguished points 0 and 1 (in this order). Then FA has points 0,1/2,1 with distinguished points 0 and 1. So there is a unique morphism A->FA. By the alleged finality of d:X->FX there is a unique homomorphism h:A->X. Since h(0)=x_0 and h(1)=x_1, by continuity of h we conclude that x0<=x1 in the specialization order. By swapping the order of the distinguished points of S, we also conclude that x1<=x0. Thus, x0 and x1 have the same neighbourhoods. By the T0 property, they are equal, which contradicts the definition of a bipointed topological space. (3)------------------------------------------------------------------ Now consider the category of normal spaces. We use Urysohn's Lemma and Banach's Fixed Point Theorem to show that Freyd's construction works here if one endows I=[0,1] with the Euclidean topology. First, d:I->FI as defined by above is clearly a homeomorphism with inverse c:FI->I given by c(inl(x))=x/2 c(inr(x))=(x+1)/2. (NB. "d" stands for "destructor" and "c" for "constructor".) Thus, if D:X->FX is a coalgebra, to say that h:X->I is a coalgebra homomorphism is the same as saying that h = c o Fh o D We thus consider the obvious functional H:C(X,I)->C(X,I) where C(X,I) is the set of continuous maps from X to I, namely H(h) = c o Fh o D. (I know, the domain and codomain of H should consist of BiTop morphisms rather than continuous maps; this (co)restriction will be performed very shortly). We endow C(X,I) with the sup-metric, which is well-defined as I is bounded. It is well-known that this is a complete metric space with limits of Cauchy sequences computed pointwise. We consider the subspace B(X,I) of BiTop morphisms. First, it is non-empty by Urysohn's Lemma. And this is where the assumption of normality is used (albeit not in its full strength). Second, it is a complete subspace, as limits are computed pointwise. Third, H trivially (co)restricts to a functional H:B(X,I)->B(X,I). Thus, in order to obtain the desired conclusion, all we have to do is to show that H:B(X,I)->B(X,I) is contractive. For every x in X, we have that D(x) is of one of the forms inl(y) or inr(z), for which we respectively get that, for any h in B(X,I), H(h)(x)= c o Fh o inl(y)=h(y)/2 or H(h)(x)= c o Fh o inr(z)=(h(z)+1)/2. Hence in each case we respectively get that |H(h)(x)-H(g)(x)|=|h(y)/2-g(y)/2| =|h(y)-g(y)|/2 or |H(h)(x)-H(g)(x)|=|(h(z)+1)/2-(g(z)+1)/2|=|h(z)-g(z)|/2 By definition of the sup-metric, the distance from H(h) to H(g) is the sup of |H(h)(x)-H(g)(x)| over all x. By the above argument this is smaller than the sup of |h(t)-g(t)|/2 over all t (because the sup of a larger set is bigger), which is half the distance from h to g. Therefore H is contractive. Q.E.D Remark --------------------------------------------------------------- Normality in (3) can be generalized to the requirement that for any two distinct points there is a function into the unit interval that maps one of the points to 0 and the other to 1 (weak normality). This is stronger than Hausdorffness and weaker than normality by Urysohn's Lemma. But this definition uses the very object that we want to "construct". Does anyone know a characterization of weak normality that doesn't refer to real numbers? It is easy to see that the assumption that the unit interval with the Freyd's structure is final in BiC for some subcategory C of Top implies that all spaces of C are weakly normal. Thus, the largest full subcategory of Top for which the Euclidean unit interval with Freyd's structure map is a final coalgebra consists precisely of the weakly normal spaces. ---------------------------------------------------------------------- Question: What does one get in full subcategories of locales and of equilogical spaces? ---------------------------------------------------------------------- mailto:mhe@dcs.st-and.ac.uk http://www.dcs.st-and.ac.uk/~mhe/ ----------------------------------------------------------------------

1 1

call for participation: ASM2000, March 19th - March 24th
by Application Asm 27 Jan '00

27 Jan '00

-> We apologize if you received multiple copies <- ______________________________________________________________ _______ _______ _______ Call for Participation, Preliminary Program _______ _______ _______ _______ ASM2000 _______ _______ _______ _______ http://www.tik.ee.ethz.ch/~asm/2000 _______ _______ Monte Verita, Switzerland _______ _______ March 19th - 24th 2000 _______ ______________________________________________________________ In March 2000, an Abstract State Machine (ASM) Workshop will be held at Monte Verita, Switzerland. The aim of the workshop is to bring together domain-experts using ASMs as practical specification formalisms and theore- ticians using ASMs as formal starting point for their investi- gations, as well as people generally interested in ASMs. See http://www.eecs.umich.edu/gasm for more info on ASMs. The technical program consists of invited lectures, tutorials, presentations of refereed papers, and software demonstrations. A significant part of the time will be devoted to discussions. Arrival is on Sunday afternoon, June 19th, and the workshop program will end on Friday noon, June 24th. A limited number of grants covering registration and part of travel costs are available for undergraduate students. Applications shall include a short CV and resumee of scientific interests. ______________________________________________________________ _______ _______ _______ Important Dates _______ ______________________________________________________________ Grant applications deadline : February 15th Registration deadline : March 1st Earlier registrants get nicer rooms with view over lake and mountains! ASM2000 is just before ETAPS'2000 (Berlin, March 25-April 2,2000) so that attendance to both events can be suitably combined. ______________________________________________________________ _______ _______ _______ Location _______ ______________________________________________________________ Monte Verita served for over hundred year as a boiling meeting place for a variety of movements, ranging from naturalism, over anarchism, to various artistic tendencies. (see http://http://www.csf-mv.ethz.ch/Official/MonteVerita/History.html) The workshop takes place in the newly restored historic Bauhaus buildings, situated in a scenic park with a marvelous view onto the lake Lago Maggiore and the mountains. A 10 minutes walk away the participants can take advantage of Ascona, a picturesque medieval village on the shore of a splendid and sunny bay. (see http://www.ascona.ch/etale.htm) Ascona and the Monte Verita are situated in the heart of Europe, easily accessible from Milano, Italy and Zurich, Switzerland. For travel instructions see http://www.csf-mv.ethz.ch/Official/Additional/Additional.html _______________________________________________________________ _______ _______ _______ Registration Form _______ _______________________________________________________________ Please fill out the registration form below and send it until March 1st to Monica Fricker at the address on the form (regular mail only, no e-mail or fax) to register for the workshop. =============================================================== Send to: Monica Fricker (e-mail/fax not acceptable) Institut TIK ETH Zentrum Gloriastrasse 35 CH-8092 Zurich Switzerland ph: +41-1-632-7035 fax: +41-1-632-1035 EMail: fricker(a)tik.ee.ethz.ch Please Print or Type: Name:__________________________________________________________ Last/Family First MI Affiliation:___________________________________________________ Address:_______________________________________________________ _______________________________________________________ City:_________________________ State or Region:________________ Zip/Postal code:___________________ Country:___________________ Daytime Phone:_____________________ Fax Number:________________ Email:_________________________________________________________ Do you have any special needs?_________________________________ (special meals, access, etc.) Please circle appropriate fee * Workshop Registration, Accommodation, and Full Board: Student Regular Dollar $ 310 $ 510 Swiss Francs CHF 465 CHF 765 Charges: (please fill out) Total Enclosed: ________ (Swiss Francs (CHF)) PAYMENT MUST BE ENCLOSED: BANK-TO-BANK-TRANSFER (INTERNATIONAL MONEY ORDER) MUST BE DRAWN ON THE FOLLOWING BANK ACCOUNT: SCHWEIZERISCHE NATIONALBANK, BERN BC: 110 Acc.#: 1530-5-30-ETHZ Credit: ASM97 1-67-234-97 E_MAIL REGISTRATIONS CANNOT BE ACCEPTED BECAUSE WE NEED TO HAVE SIGNATURES ON FILE. CHECKS NOT ACCEPTED. Method of Payment ______ BANK-TO-BANK-TRANSFER ______ VISA ______ MASTERCARD ______ AMERICAN EXPRESS ______ DINERS CLUB Credit Card Number:____________________________________________ Exp. Date:____________________ Cardholder Name: ______________________________________________ Exactly as it is printed on the card Date:___________Signature:_____________________________________ We will have to bill no-show registered persons in full. Sorry, we cannot accept cancellations after March 1st, and refunds for cancellations before March 1st may take several months to process. _______________________________________________________________ _______ _______ _______ Program _______ _______________________________________________________________ Discussion sessions, ad hoc meetings, .... Invited Talks: -------------- Andreas Blass, Univ. of Michigan "Pure Mathematics and ASM's." Egon B�rger, Univ. of Pisa "Composition and Structuring Principles for ASMs" Gerhard Goos, Univ. of Karlsruhe title to be anounced Martin Odersky, EPFL Lausanne "Functional Nets as a Composition Method for ASM's" Wolfgang Reisig, Humbold Univ. Berlin "Towards a Distributed ASM Thesis" Natarajan Shankar, SRI International "Symbolic Analysis of Transition Systems" Tutorials: ---------- Tutorials include tool-demonstrations and hands-on experience with the used tools. Infrastructure includes 12 SUN-workstations. Uwe Glaesser, Giuseppe del Castillo "Specifying Concurrent Systems with ASMs" The ASM-workbench is introduced and used for experiments with concurrent systems. Harald Ruess, ... , Natarajan Shankar "Verifying ASMs with PVS" The basic features of the PVS proof development system are introduced and demonstrated. Matthias Anlauff, Philipp Kutter, Alfonso Pierantonio "Developing Domain Specific Languages" The Gem-Mex system is used to prototype and visualize small domain specific languages with ASM semantics. Industrial Applications: ------------------------ Peter Paeppinghaus and Joachim Schmid, Siemens AG "Report about a practical application of ASMs in Software Design" Wolfram Schulte, Microsoft Research "ASM applications in industrial research and development" Presentations: -------------- M. Anlauff "Xasm - An Extensible, Component-Based Abstract State Machines Language" D. Beauquier and A. Slissenko "Verification of Timed Algorithms: Gurevich Abstract State Machines versus First Order Timed Logic" A. Blass, Y. Gurevich and J. Van den Bussche "Abstract state machines and computionally complete query languages" E. Boerger, A. Cavarra, and E. Riccobene "An ASM semantics for UML Activity Diagrams and UML State Machines" S.C. Cater and J.K. Huggins "An ASM Dynamic Semantics for Standard ML" J. Cohen and A. Slissenko "On Verification of Refinements of Timed Distributed Algorithms" R. Eschbach, U. Glaesser, R. Gotzhein, A. Prinz "The Semantics of Programming Languages: A transformational operational approach using Abstract State Machines" V.O. Di Iorio, R. da Silva Bigonha, and M. Maia "A Self-Applicable Partial Evaluator for ASM" A. Gargantini and E. Riccobene "Encoding Abstract State Machines in PVS" Y. Gurevich and D. Rosenzweig "Partially Ordered Runs: a Case Study" Y. Gurevich, W. Schulte, and C. Wallace "Investigating Java concurrency using Abstract State Machines" A. Heberle, W. Loewe, and W. Zimmermann "On Modular Definitions and Implementations of Programming Languages using Order-Sorted Partial Abstract State Machines" J.K. Huggins and W. Shen "The Static and Dynamic Semantics of C" B. Intrigila, G.D. Penna, and D. Ciccomartino "Extending Boerger's JVM Model to Compile Safe C++ Code: 1. The Pointers' Problem" J.W. Janneck and P.W. Kutter "Mapping Automaton - Simple Abstract State Machines" C. Pahl "Towards an Action Refinement Calculus for Abstract State Machines" H. Rust "Hybrid Abstract State Machines: Using the Hyperreals for Describing Continuous Changes in a Discrete Notation" J. Teich, P.W. Kutter, and R. Weper "Description and Simulation of Microprocessor Instruction Sets Using ASMs" K. Winter "Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study" M. Spielmann "Model Checking Abstract State Machines and Beyond" A.V. Zamulin "Specifications In-the-large by Typed ASMs" A.V. Zamulin "Generic Facilities in Object-Oriented ASMs" _______________________________________________________________ _______ _______ _______ Organization _______ _______________________________________________________________ The workshop is sponsored by the Swiss Federal Institute of Technology, Microsoft Research, and BlueCapital. Organizers: Yuri Gurevich, Microsoft Research, Redmond, Washington Philipp W. Kutter, Federal Institute of Technology, Z�rich Martin Odersky, Federal Institute of Technology, Lausanne Lothar Thiele, Federal Institute of Technology, Z�rich

1 0

Re: Freyd's couniversal characterization of [0,1]
by Andrej Bauer 27 Jan '00

27 Jan '00

"Martin H. Escardo" <Martin.H.Escardo(a)ens.fr> writes: > It would be interesting to test Freyd's couniversal characterization > of the unit interval in many other categories. > > Here I test it in Top, the category of topological spaces and > continuous maps, and various full subcategories, where one would hope > to get the unit interval with the Euclidean topology. > > ---------------------------------------------------------------------- > Summary of the outcome of some tests: > > (1) In Top, the final coalgebra for Freyd's functor exists. Its > underlying object, however, is an indiscrete space (unsurprisingly). > > (2) In the category of T0 spaces, it doesn't exist. > > (3) In the category of normal spaces it does exist, and, as one > would hope, its underlying object is indeed the unit interval with the > Euclidean topology. > > See remark below for weakening normality in (3) as much as possible. > ---------------------------------------------------------------------- > Arguments follow. > > [text deleted] >> ---------------------------------------------------------------------- > Question: What does one get in full subcategories of locales and of > equilogical spaces? I can answer this for equilogical spaces. The functor F: Bi[Equ] ---> Bi[Equ] has a final coalgebra. It is the equilogical space (C, ~) where C is the Cantor space C = 2^N = infinite sequences of 0's and 1's and ~ is the equivalence relation defined by a ~ b iff r(a) = r(b) where r: C --> [0,1] is defined by r(a) = \sum_{k=0}^\infty a_k / 2^{k+1} (This equivalence relation can easily be defined without reference to the closed interval [0,1].) Thus, the final coalgebra is the _(unsigned) binary digit representation_ of the closed interval [0,1]. The structure map d: (C,~) ---> F(C,~) is induced by the canonical isomorphism C ---> C + C = 2 x C. Unfortunately, this closed interval is not what we would hope for. Ideally, we would want the _signed_ binary digit representation of the interval [-1,1], i.e., the space ({-1,0,1}^N, :=:) where :=: is defined by a :=: b iff s(a) = s(b) s(a) = \sum_{k=0}^\infty a_k / 2^{k+1} We want this because the real numbers object in Equ is the built from the _signed_ representation of reals. I do not see how to adapt the construction so that it yields the signed representation. We would have to "glue" more than just a couple of points. But how do we say what should be glued, without reference to [0,1] or C? Let me explain briefly why (C, ~) is the final coalgebra. In Equ, in the pushout 1 -------> X | | | | | | | | V V X -------> FX the underlying space of FX is |FX| = |X| + |X|. This is a "small" but crucial difference between Top and Equ. We can first find the final coalgebra in Top_0 for the functor A --> A + A, which is the Cantor space C, and then compute the equivalence relation on C. In this case it is easy to verify that all the continuous maps obtained from the coalgebraic structure of C actually preserve the equivalence relations. By the way, the two distinguished points of (C, ~) are 0^\infty and 1^\infty, of course (and it doesn't matter, since C is homogeneous). -- Andrej Bauer

2 1