January 1998 - Categories - categories.org.au

sad news
by Peter Freyd 01 Feb '98

01 Feb '98

Sammy Eilenberg died today. He had been unconscious since June. Knowing it was inevitable doesn't really help.

2 1

Friedman's challenge, and the ordinals
by Paul Taylor 01 Feb '98

01 Feb '98

Date: Mon Jan 26 21:40:18 1998 Subject: Friedman's challenge The reason why 1970s topos theorists did a "slavish translation" of well-pointedness, choice, etc is quite simple: it is known in computer science and engineering as "reverse compatibility". We (ie Lawvere, Tierney and others) needed to show that whatever you could allegedly do with set theory, you could do with elementary toposes too. Now that reverse compatibility has been achieved, the old methods are obsolete, and we should be able to move on from there. We show that the new methods (by which I mean category theory in general, not necessarily elementary toposes) are more idiomatic for the old purposes and more powerful for new ones. For example we would never have got anywhere with domain models of polymorphism, or with synthetic domain theory, without category theory as our guide. I'm sure that most of the readers of "categories" can add examples from their own interests. I have a personal reason for bitterly resenting ever being taught set theory. (I don't want anybody to interpret that as resentment towards the particular people in Cambridge who did the teaching - the problem is with the mathematical community as a whole which has perpetuated this pernicious theory.) For several years I was trying to prove (in an elementary topos, in particular without excluded middle, or the axiom of collection, which seems to me to be set-theoretic hocus pocus): Let (X, <=) be a poset with least element and directed joins, and s:X->X a monotone (not necessarily Scott continuous) function. Then s has a least fixed point. I talked about my attempts at this at at least two international category meetings and several other project meetings and conferences. Because of my set-theoretic indoctrination, much as I rebelled against it, I set about defining ordinal iterates of the function s and its values at the least element. The intuitionistic theory of ordinals is complicated, and there are several flavours of them, but there is no doubt that ordinals as big as you please exist in any elementary topos. See JSL 61 (1996) 703-742. Always with traditional applications of ordinals, the problem is knowning when to stop. The textbook solution is due to Friedrich Hartogs, 1917. Basically, you take a pair of scissors ... . Andre Joyal and Ieke Moerdijk have a pair of scissors which make a cleaner cut (by our standards in category theory), but they too still chop off the standard sequence. (Maybe someone would like to write a PhD thesis which uses their methods to eliminate the set theory from the "alpha-presentable" versions of Gabriel-Ulmer duality.) In fact this result has now been proved, by a Georgian called Dimitri Pataraia. (I haven't met him, or been able to find out much about him, despite now sharing an office with another Georgian). Pataraia's solution is pure order theory. You could teach it to a third year undergraduate class in a course on lattices or domain theory. There is not an ordinal in sight. In fact, looking more closely at his solution, there *are* ordinals in it. [My version of] his proof looks remarkably like Zermelo's second proof of Choice => well ordering. It may seem strange that such an infamously classical result should contain a the essence of an intuitionistic argument, but in fact [Zermelo's version of] Choice occurs in the first line of the argument and never again. Zermelo manufactures the required ordinal structure out of the given object, whereas the subsequent orthodox approach, due to Hartogs 9 years later, is based on a single monolithic system, which has to be chopped off in a rather unceremonious fashion. Ordinals similar to Zermelo's, though only satisfying the induction scheme for a restricted class of predicates, and not satisfying any recursion scheme I can find, are also to be found in Pataraia's proof. Throughout my (personally unsuccessful) study of this problem, whenever I sought intuition from set theory it took me in the WRONG direction. I cannot think of any other branch of mathematics, with the exception of infinitessimal calculus before it was reformed, which I would condemn so utterly. In fact, 18th century calculus did give a lot of right answers, and at least its wrong ones were interesting and provoked good research. In answer to Harvey Friedman, I *don't* advocate topos theory as foundations. It still reeks of set theory (sorry, Bill). Paul Taylor =================================== Part II (it seems that I originally sent the above to the wrong email alias) I didn't properly spell out my philosophical conclusions about ordinals. What I mean is that a [not "the"] system of ordinals *ought* to have a top element (a fixed point for successor). In other words, I am contradicting the usual interpretation of the Burali-Forti paradox, and discarding the tradition of chopping the monolithic system of ordinals off, as Hartogs, Joyal/Moerdijk and many others have done (including me). The notion of cardinality is clearly stupid from a categorical point of view (we know better than to classify objects up to isomorphism, without even any regard to their automorphism groups) and, as an atheist, I find Cantor's theologically motivated notion of "size" utterly incomprehensible. While I'm at it, I don't accept the argument in either Russell's paradox (re the set {x:x not in x}) or Cantor's theorem that P(X) =/= X. It's not that I am particularly keen to have a set of all sets (though such a thing is probably to be expected from the right logical principles in much the same way as a universal Turing machine is in recursion theory), but that I do not consider that these classic arguments ought to be valid. Andy Pitts and I traced Russell's paradox to a particular quantifier (in fact in a locally cartesian closed category) - see our paper in Studia Logica 1989 p 387. It is this quantifier which I reject. In fact he and I independently had models which had a type of types, and achieved this by restricting the quantifiers which could be interpreted. The Burali-Forti paradox goes away too if the class of predicates for which the induction scheme is valid (in the definition of an ordinal) is retricted. For example, the domain of increasing natural numbers plus a fixed point is such an ordinal for Scott-continuous predicates (the Crole-Pitts FIX object). I think I may be able to adjust the notion of elementary topos (I prefer to think in these terms than in symbolic logic) to a useful fragment in which Cantor's theorem fails. (Sorry to be so vague, but I haven't got very far with this, and currently have a head full of perl programming.) Paul

2 1

Generic Programming Workshop: Final Call
by Roland Backhouse 31 Jan '98

31 Jan '98

Final Call for Papers Workshop on Generic Programming June 18th 1998, Marstrand, Sweden (In Conjunction with Mathematics of Program Construction Conference) ---------------------------------------------- Deadline for submissions: 16th February, 1998. ---------------------------------------------- Generic programming is about making programs more adaptable by making them more general. A generic program embodies some sort of polymorphism; ordinary programs are obtained from it by suitably instantiating its parameters. The parameters may be other programs, types or type constructors, or even programming paradigms. Generic programming techniques have always been of interest, both to practitioners and theoreticians, but to date have rarely been a specific focus of research. Recent developments in functional and object-oriented programming lead the organizers of this workshop to believe that there is sufficient interest to warrant the organisation of a one-day workshop on the theme of generic programming. The workshop will be on June 18th, 1998, following on from the Mathematics of Program Construction conference. The goal of the workshop is to inventorise the full diversity of research activities in the area of generic programming, both theoretical and applied, by attracting as wide a spectrum of participants as possible to the workshop. The results of the workshop will be published in the form of a detailed summary of all presentations, prepared by the organizers and made available on internet. We cordially invite all those with an active interest in this important new area to submit a short position paper on their work to Roland Backhouse (rolandb(a)win.tue.nl) The position paper should outline your current research activities in this area and include references to published papers and/or web links to technical reports where more information can be found. The recommended length is approximately three pages. The deadline for submission is 16th February, 1998. Notification of acceptance will be on or before 15th March, 1998. The organizers are as follows: Roland Backhouse (Cochair), Netherlands Tim Sheard (Cochair), USA Robin Cockett, Canada Barry Jay, Australia Johan Jeuring, Sweden Karl Lieberherr, USA Oege de Moor, UK Bernhard Moeller, Germany Jose Oliveira, Portugal Fritz Ruehr, USA For further details on the Mathematics of Program Construction and this workshop please consult: http://www.md.chalmers.se/Conf/MPC98/

1 0

Challenge from Harvey Friedman
by Vaughan Pratt 31 Jan '98

31 Jan '98

I'm taking the liberty of forwarding to the categories mailing list the following challenge posted by Harvey Friedman to Steve Simpson's Foundations of Mathematics mailing list. This is the latest in a long-running engagement about sets vs. categories on the latter list, recent postings to which can be read at http://www.math.psu.edu/simpson/fom/postings/9801.html Postings with "categor{y,ical}" in their subject lines are the relevant ones. Information about the fom list (how to subscribe etc.) can be found at http://www.math.psu.edu/simpson/fom/fom-info As we were fond of saying quarter of a century ago, Peace Vaughan Pratt ------- Forwarded Message Date: Fri, 23 Jan 1998 00:54:20 +0100 To: fom(a)math.psu.edu From: Harvey Friedman <friedman(a)math.ohio-state.edu> Subject: FOM: Set Theory Axioms The point of this posting is to give some entirely conventional axioms for set theory that are a bit simpler than many that are normally given. They are fully formal. By comparison, look at the axioms of elementary topoi that are given in MacLane/Moerdijk, Sheaves in Geometry and Logic, A first Introduction to Topos Theory, Springer-Verlag, 1994, on p. 163. The difference in complexity is strikingly grotesque. I challenge anyone to write down their favorite fully formal axioms for topoi that are sufficient to do real analysis, so we can compare them side by side with the fully formal axioms I write down here. Topos theory with natural number object is insufficient to develop undergraduate real analysis - although many fom postings conceal this fact. One has to add to topoi: natural number object, well pointedness, and choice. The latter two are nothing more than slavish translations of set theory into the topos framework. The "idea" is to take a fatally flawed foundational idea and force it to "work" by transporting important ideas from set theoretic foundations. But the axioms of elementary topoi are already incomparably more complicated than the axioms for set theory presented here. Let me start with the dramatically simple axioms of finite set theory. These amazingly simple axioms are tremendously powerful. We work in the usual classical predicate calculus with equality and one binary relation symbol epsilon - which we abbreviate here by "in." It is also useful to use the constant symbol 0 (for the empty set), the unary function symbol { } (for singletons), and the binary function symbol U (for pairwise union). Note that axioms 2-4 amount to the most trivial of definitions. 1. (forall x)(x in a iff x in b) implies a = b. 2. (forall x)(not(x in 0)). 3. x in {a} iff x = a. 4. x in a U b if and only if (x in a or x in b). 5. [phi(0) & (forall x,y)((phi(x) & phi(y)) implies phi(x U {y}))] implies phi(x). Here phi(x) is any formula in the language in which y is not free. That's all! One ***derives*** pairing, union, power set, foundation, replacement, and choice, from these axioms alone!!! Also, when appropriately formalized, "every set is finite" and things like "every set has a transitive closure." These axioms are "practically" complete - an informal concept that I have alluded to before on the fom. Now for ZFC. We take a different tack and only use epsilon. 1. (forall x)(x in a iff x in b) implies a = b. 2. (therexists x)(a in x & b in x). 3. (therexists x)(forall y in a)(forall z in y)(z in x). 4. (therexists x)(forall y)((forall z in a)(z in y) implies y in x). 5. (forall x,y)(x in y implies (therexists z in y)(forall w in z)(w notin y)). 6. (therexists x,y)(x in y & (forall z in y)(therexists w in y)(z in w)). 7. (therexists x)(forall y)(y in x iff (y in a & phi)), where phi is any formula in the language in which x is not free. 8. (forall x in a)(therexists y)(phi) & (forall x,y,z)((phi(x,z) & phi(y,z)) implies x = y) implies (therexists w)(forall x in a)(therexists unique y in w)(phi), A novelty is the axiom of infinity, 6, is simpler than usual; and also choice and replacement are combined nicely by 8. This allows such a simple axiomatization in purely primitive notation. Try to right down the axioms of a topos with natural number object, well pointed, and choice, in simple primitive notation!! Good luck. As is well known, ZFC is "practically" complete. The version in the book on p.163 - which does not even include natural number object, well pointedness, or choice - requires a very substantial amount of preliminary abbreviations in order to formalize. ------- End of Forwarded Message

10 10

Insights: adjunctions and languages
by Jonathan Burns 31 Jan '98

31 Jan '98

Hello and goodwill Now that I have my PhD dissertation submitted, I've had a while to stand back from the material, and consider the categorial territory that I stumbled into in the last year or so. Although I'm acquainted with a mere fraction of the crucial concepts here, what I have found seems to contain really elegant insights into computer languages, and I want to clarify these to myself, as a philosophical basis for future study. It may well be that it will all be old news here, but the introductory texts don't spell things out in quite the way I perceive them. (My reading started out wide, but narrowed down mainly to MacLane, Barr and Wells, and articles by Ridenour in some S-V workshop proceedings some years back. Asperti and Longo has been good too.) To cut to the chase, consider Cartesian closure. If we leave out matters of storage, scoping and other time-related resources, a Lisp-family language is lambda-calculus with a reduction policy - that is, a set of decisions that one expression form is to be replaced by another. (For Lisp, the policy is to do beta- and eta-reduction in some order until no more redexes can be found.) And lambda is a CCC with name binding - as opposed to expressing everything with projectors. But more: a CCC is defined by adjunctions: unique-terminal, diagonal- product, product-exponential. These adjunctions define isomorphisms between expression forms: f = n (F g) g = (G f) u where u and n are unit and counit. In other words, the isomorphisms are determined by natural transformations, of a very simple and intuitive kind: if you can have one of a thing, you can have two of them; if you can have one thing and another, you can have both together in a product; if you have a product expression, then you can have a product expression constructor (exponential) with one term curried out. These natural transformations are universal structural operators; inherently polymorphic or domain-free, in programming terms. And using only a handful of them, you can define these isomorphisms, which then constitute an equational theory for a language - in the sense that lambda is the equational theory behind Lisp. Whatever can be defined by adjunctions is what they call "referentially transparent": equals are substituted only for equals. It's stronger than that, in fact, because with an adjunctive system like this, an expression can be substituted for another only when there is also a rule for the reverse substitution. E.g. x * x = square x The referentially-transparent equational theory stands by itself. But on top of it, we may now impose reduction policies, ("games") of various kinds: 1. We can substitute equals for equals by hand: "just doing algebra". 2. We can specify an algorithm for substitutions: intepreters. 3. We can extend this to interpreters where we introduce new reduction rules as we go along: symbolic algebra systems. 4. We can specify a data-directed backtracking algorithm, which is allowed to apply a reduction rule in either order: equational logic systems. 5. We can specify a data-directed heuristic backtracking algorithm: dunno quite what we call these, maybe constraint systems. 6. We can specify systems which not only use backtracking and heuristics, but assert and retract additional rules as we go along: traditional AI. "Extending the rules" is a dangerous game, of course; you have the responsibility for maintaining referential transparency. Nobody I've read has hinted at the possibility of automating the definition of equational rules by adjunction. Even if such a thing could only be done in a very restrained sense, though, it would still be very powerful. Vaguely, I think the rubric has to be: OK, here's the kind of data we want to work on - regular expressions, perms and coms, machine code, whatever - now, what are the equivalences we see in these domains, and are they isomorphisms? And if so, _why_ are they isomorphisms, and what natural transformations might possibly define them by adjunction? The key insight for me, the thing that categories has revealed, is that reduction polices for equational theories are _the_ bridge between the declarative and the procedural; and equational theories can be built by adjunction from universal constructors. It's so beautiful I just want to sit and gaze at it. It's one of those obvious things that you see side-on for years, and then suddenly you see it directly. More later. Jonathan Burns | burns(a)latcs1.lat.oz.au| A student approached Susskind, in hopes Computer Science Dept | of understanding the lambda-nature... La Trobe University |

2 1

Announcement of PhD Positions in Computing Science at Chalemrs
by Mary Sheeran 28 Jan '98

28 Jan '98

The Department of Computing Science at the Chalmers University of Technology and G�teborgs University announces free PhD positions. The major research topics at the department are programming logic and type theory, functional programming, concurrency, fault tolerant distributed systems, formal methods, cognition technology, and algorithms and discrete optimisation, but research is also carried out in a number of other topics. More information about the research at the department can be found on the WWW on page: http://www.cs.chalmers.se/ComputingScience/Research Most PhD positions are five year scholarships. The PhD student will spend about 80 percent of his or her time on graduate studies, and about 20 percent on teaching. Applicants must have an undergraduate degree in Computer Science with excellent results. The department tries to increase the number of female employees, and especially welcomes female applicants. At the moment the scholarships consists of 15400 (18000) SEK per month in the first (last) year. Usually a foreign PhD student does not teach in his or her first year in Sweden, and as a consequence the scholarship is of a slightly smaller size. More information about the graduate programmes can be found on the WWW on page: http://www.cs.chalmers.se/Cs/Grad/gradinfo/gradinfo.html To apply, send us a letter in English, covering 1 data about yourself; 2 a copy of an official paper giving grades from your undergraduate degree(s); 3 a statement about your main interests and your plans for research; 4 some letters of recommendation from people that know you as a student or as an employee; 5 any scientific papers you have written. Send your application to Director of Graduate Studies Department of Computing Science Chalmers University of Technology 412 96 G�teborg Sweden Furthermore, send an email containing the data about yourself to ms(a)cs.chalmers.se The last date for your application to arrive is March 2, 1998. A decision about to whom we will offer the PhD positions will be taken before June 1, 1998.

1 0

Terminology for Kan extensions
by Ronnie Brown 28 Jan '98

28 Jan '98

There seems some confusion as to whether Left Kan extensions are right Kan extensions and conversely, and it seems different authors use different conventions. What do people think of using a terminology analogous to limits and colimits, i.e. Kan extensions and Kan coextensions? In particular, what Carmody and Walters call left Kan extensions would here be Kan coextensions, which can be constructed as coends (as in Mac Lane, CFTWM). This point has come from Anne Heyworth, where left Kan extensions use right rewriting, if you write composition in a category in the algebraic rather than functional way. Any other ideas? Ronnie Prof R. Brown, School of Mathematics, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382475 fax: +44 1248 383663 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ New article: Higher dimensional group theory Symbolic Sculpture and Mathematics: http://www.bangor.ac.uk/SculMath/ Mathematics and Knots: http://www.bangor.ac.uk/ma/CPM/exhibit/welcome.htm

1 0

67th PSSL
by Jaap van Oosten 27 Jan '98

27 Jan '98

FIRST ANNOUNCEMENT Dear friends and colleagues, We plan to organize the 67th meeting of the Peripatetic Seminar on Sheaves and Logic in Utrecht over the weekend of 30-31 May, 1998. As usual we welcome talks on sheaves, logic and related areas. In order to register, please fill in the form below and return (preferably by email) to Jaap van Oosten (jvoosten(a)math.ruu.nl, or to the address below). We'd be obliged if you could register before half May. Postal address: Dept. of Mathematics, P.O.Box 80.010 3508 TA Utrecht, The Netherlands --------------------------------------------------------------- Name _____________________________ Address _____________________________ _____________________________ _____________________________ _____________________________ email I wish to give a talk entitled__________________________________ ________________________________________________________ I wish to reserve accomodation for the following nights: (single/double)_______________________ ---------------------------------------------------------------- Looking forward to meeting you in Utrecht, Carsten Butz, Ieke Moerdijk and Jaap van Oosten

1 0

The Friedman/Flagg paper
by Peter Freyd 27 Jan '98

27 Jan '98

91f:03111 03E99 03B30 03F99 68Q25 Friedman, H.(1-OHS); Flagg, R. C.(1-SME) A framework for measuring the complexity of mathematical concepts. (English) Adv. in Appl. Math. 11 (1990), no. 1, 1--34. _________________________________________________________________ This paper presents a system $\scr F\sb 0(\scr B)$ that is intended to allow practical computation of the complexity of mathematical concepts. $\scr F\sb 0(\scr B)$ is an untyped theory of sets and partial functions in a first-order free logic with equality and a description operator. Its language $\scr L\sb 0(\scr B)$ contains many primitive operations, such as $n$-tuples, lambda abstraction, comprehension terms, finite set and Cartesian product formation, and definition by cases. $\scr B$ denotes a set of "descriptive forms" that are patterns according to which new constants, functions, and predicates can be defined. After a rigorous presentation of the syntax of $\scr L\sb 0(\scr B)$, standard programming language procedures yield parsing and recognition algorithms. A precise semantics for $\scr L\sb 0(\scr B)$ is given, followed by a deductive system $\scr F\sb 0(\scr B)$ that is shown to be complete by means of a Henkin-style proof. Finally, the authors introduce the notions of definition sequence, definition dag (directed acyclic graph), and definition tree. On the basis of these notions, they promise that, in a future paper, they will develop measures of complexity of definitions that will make possible practical calculation of the complexity of concepts in a large part of current mathematical practice. Reviewed by E. Mendelson

1 0

Immodest proposal
by John R Isbell 26 Jan '98

26 Jan '98

Contemplating Harvey Friedman's Challenge, I asked myself 'Aren't there more important problems around?' And of course there are. Moreover, I believe I have solved one of them. P. What should we call the ancient substitute for e-mail? S. Why not m-mail? Snappy; memorable; unmistakable; and m=e\over {c^2} gives the value. John Isbell

1 0