October 1992 - Categories - categories.org.au

position announcement
by dbenson＠yoda.eecs.wsu.edu 29 Oct '92

29 Oct '92

Dear Colleague, These positions do not appear to be well-publicized and I solicit your cooperation in making these positions more widely known. Please feel free to distribute this position announcment to all who might be interested or might be willing to cooperate in further redistributing this announcement. I believe we have 4 to 6 vacancies we can fill if a good match can be made. We are very interested in making some appointments at the the rank of associate professor and professor. Thank you for your kind assistance, David B. Benson P.S. The chair of the search committee this year is Prof. Raghu Raghavendra, raghu(a)eecs.wsu.edu ----------------------------------------------------------------- Computer Science Faculty Positions School of Electrical Engineering and Computer Science Washington State University The School of Electrical Engineering and Computer Science solicits applications for one or more permanent computer science faculty positions. Responsibilities include initiation and supervision of research programs and instruction at undergraduate and graduate levels. Applicants for assistant professorships should demonstrate the potential for excellence in research. Applicants for associate and full professorships should have proven records of accomplishment in their fields as evidenced by sponsored research programs and publications. We seek outstanding candidates from all areas of computer science. Areas of particular interest include software engineering, artificial intelligence, parallel and distributed computing, database theory, and theoretical computer science. Screening of applications will begin immediately and continue until the positions are filled. Positions start on January 15 and August 15, 1993. Washington State University has offered the Ph.D. in computer science since 1970, and also offers B.S. and M.S. degrees. The School of EECS has over forty faculty (approximately fifteen with primary interests in computer science and engineering), sixty computer science graduate students, and active research groups devoted to parallel and distributed processing, imaging (computer graphics, visualization, image processing, and vision), neural networks, and other areas. Computing facilities in the School of EECS include PCs, graphics workstations, and servers, all with Internet access. WSU has about 16,000 students and is located in Pullman, a quiet university town in the southeast corner of the state (approximately 90 miles south of Spokane). Nearby are some of the nation's most pristine and uncrowded places for outdoor recreation. The Pullman school system is widely acknowledged to be one of the very finest in the Pacific Northwest. Applicants should send a cover letter, a curriculum vita, and the names and addresses of three references qualified to comment on their research and teaching qualifications to Chair, Computer Science Search Committee School of Electrical Engineering and Computer Science Washington State University Pullman, WA 99164-2752 WSU is an EO/AA educator and employer. Protected group members are encouraged to apply. ==============================================================================

2 1

categories of contexts
by Paul Taylor 29 Oct '92

29 Oct '92

Thorsten Altenkirch says > Named variables are a complete redherring. Named variables are the way that human mathematicians have been notating their work for centuries, and human programmers prefer them too. Even categorists give up \pi_1 and \pi_2 shortly after introducing the universal property of products! Thorsten also mentioned alpha conversion. There's an important distinction to be made with alpha conversion which corresponds to that between free (open) and bound (closed) variables. The closed term $\lambda x.x$ is to all intents and purposes the same as $\lambda y.y$ (and with de Bruijn indices *is* the same) but the open terms are quite different. My personal way of formulating this construction is as follows: * the objects are (finite) sets of distinct variable names together with their types, ie contexts; [x1:x1,x2:X2,...,xn:Xn] changing the names gives a different object * the morphisms are substitutions: [y1:=u1,y2:=u2,...,ym:=um] [x1:X1,x2:X2,...xn:Xn] ---------------------------> [y1:Y1,...,ym:Ym] where there's one "assignment" for each variable in the target context and the terms have their variables amongst those in the source. * composition is given right to left by the notationally simple rule [z:=v(y)] o [y:=u(x)] = [z:=v[y:=u]] I missed something out in the definition of morphism: I define *two* categories, one ("raw terms") consisting of closed-alpha equivalence classes, the other ("terms") being its quotient by beta/eta/etc equivalence. Similar constructions may be done for languages other than the simply typed lambda calculus. In fact lambda abstraction is not relevant to the issue. Now we may ask some elementary categorical questions: What are the isomorphisms in the category of *raw* terms? They are exactly the open alpha equivalences. In particular a context with two variables of the same type has a non-trivial automorphism. What do we get from concatenating two contexts which share no variable name? Assuming that the language admits individual variables as terms, allowing omission (weakening) and repetition (contraction), we obtain a product diagram. How can we form the product of contexts which do share variables, in particular the square of a context? We replace one or both by isomorphic copies (along open-alpha equivalences, ie renaming variables) and take the product of those. It seems to me that for any purpose other than the machine implementation of a compiler it is notationally better *not* to adopt a convention for consistently renaming variables in order to provide a canonical product in all cases. The product always *exists*, as I have shown (so long as we have an inexhaustible supply of new variable names), and there is a canonical choice of it, albeit involving an exception. If you're worried about the constructivity of the exception, remember that the variable names must have been chosen from amongst a decidable population, because I began by saying that they were distinct in each context (object). Paul Taylor ==============================================================================

2 1

a question on categories of contexts (CS)
by koslowj＠math.ksu.edu 28 Oct '92

28 Oct '92

This question concerns Bart Jacobs' paper "Simply typed and untyped Lambda Calculus revisited", in "Applications of Categories in Computer Science", Durham Proceedings, London Mathematical Society Lecture Note Series No. 177 In Example 3.2, Bart Jacobs constructs a term model for a certain kind of fibration (or indexed category). The base category has contexts as objects, i.e., finite tuples of type declarations, while morphisms are finite tuples of (beta-eta-equivalence classes of) terms. I have some trouble seeing that this category has finite products, given by concatenation of contexts, as claimed. Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I don't know whether Bart Jacobs has access to the net; maybe someone can forward this question to him? Thank you. regards, J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj(a)math.ksu.edu | Jimi Hendrix (Voodoo Chile) ==============================================================================

3 2

linear logic guide
by andre＠saul.cis.upenn.edu 28 Oct '92

28 Oct '92

A Brief Guide to Linear Logic Andre Scedrov Abstract. An overview of linear logic is given, including an extensive bibliography and a simple example of the close relationship between linear logic and computation. Available by anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/guide.dvi . The bibliography is also available separately from pub/papers/scedrov/LL-bib.bib . ==============================================================================

1 0

tanglerads
by jds＠rademacher.math.upenn.edu 25 Oct '92

25 Oct '92

Operads are a useful way of encoding compositions of maps from n variables to 1, modelled on grafting of trees - root to branchtip and as such appear e.g. in ``classical'' closed string field theory Qunatum corrections require a generalization for which the model should be the category of tangles or some such Any work been done on such a generalization? jim stasheff ==============================================================================

2 1

Atish Bagchi's address
by Charles Wells 22 Oct '92

22 Oct '92

The recent abstract of joint work by Atish Bagchi and me contained an erroneous email address for Atish: It should be axb32(a)po.cwru.edu. However, Atish will not be getting his email for a couple of weeks since he is out of the country. We hope he will return by early November. -- Charles Wells Department of Mathematics, Case Western Reserve University University Circle, Cleveland, OH 44106-7058, USA 216 368 2893 ==============================================================================

1 0

The theorem I didn't talk about at the Octoberfest
by barr＠triples.Math.McGill.CA 21 Oct '92

21 Oct '92

Consider the following situation. An adjoint pair U --| F, U:*A* --> *X*. I assume that *A* is a regular category and U a regular functor. This means roughly that regular epis are pullback stable. It is also supposed that some or all finite limits exist, depending on who you read. Suppose all, for simplicity. Also U preserves regular epis. Let \G denote the resultant cotriple on *A*. Now Beck showed that in all situations that the idea of A-module (A being an object of *A*) had been defined, it had a uniform description as an abelian group object in the slice *A*/A. So we set Mod(A) = Ab(*A*/A). What this does is to identify an A-module with the split extension over A with the module as kernel. If you do that, then for B --> A, the homset in *A*/A of B to M is simply Der(B,M). It therefore makes sense to call an adjoint (if it exists) to the inclusion Mod(A) --> *A*/A the modules of differentials Diff^A(B). I will assume it does exist for each object A. Corresponding to B --> A, there is a functor f_!:*A*/B --> *A*/A and it has a right adjoint f^* = A x_B -. This induces a functor, also called f^*:Mod(A) --> Mod(B) and, under mild conditions, that has a left adjoint f_#. That is usually tensoring with an enveloping object. Next assume given a chain complex functor C_*^A:*A*/A --> Mod(A) for each object A. Suppose that f_# takes C_*^B(C) to C_*^A(C) for an arrow C --> B. (Actually need that assumption only for C = B, but the more general case is what actually happens.) That is all background. Now come the three hypotheses that matter: 1. Assume that C_*(A) is a projective resolution of Diff^A(A). (This is the assumption that fails in the category of commutative algebras.) 2. Assume that UG^nA is projective in *X* for all n >= 0. 3. Assume that for each n >= 0, the functor C_n^A factors through U. More precisely, suppose that there is a functor ~C_n^A:*X*/UA --> Mod(A) such that C_n^A is naturally equivalent to the composite U/A ~C_n^A *A*/A --------> *X*/UA ---------> Mod(A) The conclusion is that the complexes C_*^A(A) is chain homotopic to the cotriple complex that has in degree n the module Diff^A(G^{n+1}A) with boundary induced in the usual way by the simplicial face operators. It is a formidable set of conditions, but of course, they are all readily satisfied in the cohomology theories in Cartan-Eilenberg. 1. essentially defines the C-E theory, 2. is obvious for group and associative algebra cohomology of an algebra projective over its ground ring, and is true (although non-trivially so) for a lie algebra that is projective over its ground ring. 3. has often been remarked and the fact that it plays a role was understood already in the original Barr-Beck paper. It says essentially that the algebra structure is not used in defining the C_n, only in defining the boundary operator. Michael ==============================================================================

1 0

weak toposes
by cxm7＠pop.cwru.edu 16 Oct '92

16 Oct '92

------------- Does anyone have any advice about this following proposed terminology? I think I want to use the term "weak topos" to mean a cartesian closed category with all finite limits and colimits, stable surjections, and a weak power object. By a "weak power object" I mean an object W with a monic M>--->W such that every monic in the category is a pullback of M in at least one way. The reasons for this are that categories of assemblies (including assemblies for extensional or modified realizability) have these properties and: 1) Except for the part about colimits this is just what you need to show the effective reflection is a topos. 2) Using the presence of coequalizers this gives a usable generalization of geometric morphisms. If a functor between weak toposes in this sense has a left exact left adjoint then that adjoint is regular (pres. finite limits and surjections) and the adjunction lifts to a geometric morphism between the toposes. And in fact these arise among categories of assemblies (as is in effect remarked by Pitts and more recently Oosten). Thanks, Colin ==============================================================================

4 4

Graph Based Logic and Sketches
by cfw2＠po.CWRU.Edu 10 Oct '92

10 Oct '92

Graph-based Logic and Sketches Atish Bagchi and Charles Wells October 9, 1992 Extended Abstract Traditional treatments of formal logic provide: 1. A syntax for formulas. The formulas are typically defined recursively by a production system (grammar). 2. An inference relation between sets of formulas. This may be given by structural induction on the syntax for the formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. The semantics may also be given by structural induction on the syntax of the formulas. First order logic, the logic and semantics of programming languages, and the languages that have been formulated for various kinds of categories are all commonly described in this way. The formulas in those logics are strings of symbols that are ultimately modeled on the sentences mathematicians speak and write when proving theorems. Mathematicians with a categorial orientation frequently state and prove theorems using graphs and diagrams (which may be described as graphs labeled coherently by data from some category). The graph, diagrams, cones and other data of a sketch are formal objects that correspond to the graphs and diagrams used by such mathematicians in much the same way as the formulas of traditional logic correspond to the sentences mathematicians use in proofs. The functorial semantics of sketches is sound in the informal sense that it preserves (usually by definition!) the structures given in the sketch. The analogy to traditional model theory is close enough that sketches and their models fit the definition of "institution" (Goguen and Burstall [2]), which is an abstraction of model theory. The content of this paper is to exhibit the structure in sketch theory that corresponds to items 1 and 2 in the description of logic (the deductive structure) and to provide a detailed translation of a particular logic between the string-based version and the sketch-based version. This work is parametrized by the type of categorial theory being considered. We assume given a finite-limit (projective) sketch E of a particular type of category as in [5] or [7]. E presents the type of category as essentially algebraic over the theory of categories. E -categories are then the models of E in Set. The kinds of categories that can be described in this way include categories with finite products, categories with limits or colimits over any particular set of diagrams, cartesian closed categories, regular categories, toposes, and many others. A formula in this setting is a potential factorization (PF) through a subobject of the codomain: formally, a pair consisting of an arrow of E and a subobject of the codomain of the arrow. We will refer to the codomain of the arrow as the codomain of the PF, and the subobject as the "claim" of the PF. Roughly, the PF is "true" if its arrow factors through its claim. Sentences are PF's whose arrows have domain 1. We provide a general recursive construction of the objects and arrows of E (hence of the PF's in particular) which is derived from the similar recursive construction for initial algebras of FLS sketches given by Barr and the second author in [8]. Our thesis is that this recursive definition constitutes the rules of inference corresponding to item 2 above. An E-sketch is a sketch that allows the specification of any kind of construction that can be made in an E-category. This greatly enhances the expressive power of sketches when compared to Ehresmann's original definition. An E-sketch is a global element adjoined freely to E ([5] and [7]). The codomain of this adjoined arrow may be perceived as a description of the graph, diagrams and other constructions of the sketch. Adjoining such an arrow constitutes the axioms of a theory, and the factorization of arrows through subobjects in the polynomial category E[s] obtained by adjoining such an arrow constitute the formulas and sentences that can be inferred from the sketch. The resulting system of inference is sound with respect to models. This type of logic fits some of the abstractions of logic that have been given, such as that of Meseguer in [4] and the formulation in terms of closures given by Tarski [6]. As a kind of worked example, the paper will also contain a detailed description of the relationship between finite-product sketches and multisorted equational logic as given by Goguen and Meseguer [3]. It is intended that this translation be sufficiently algorithmic as to be implementable, for example in Mathematica. The equations of equational logic will be seen to correspond to a specific subset of the set of PF's; indeed, in the classifying topos of E, there is a specific object and subobject that is the common codomain and claim of the all the PF's. We will give explicit proofs of the correctness of the rules of inference given by Goguen and Meseguer in terms of the deductive system described above (the recursive construction of E). References [1]M. Barr and C. Wells, Category theory for computing science. Prentice-Hall International (1990). [2]J. A. Goguen and R. M. Burstall, A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In D. Pitt et al., eds., Category Theory and Computer Programming. Lecture Notes in Computer Science 240, Springer-Verlag (1986), 313-333. [3]J. A. Goguen and J. Meseguer, Completeness of many-sorted equational logic. Technical Report CSL-135, SRI International Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1982). [4]J. Meseguer, General Logics. Report SRI-CSL-89-5, SRI International, Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1989). [5]A. J. Power and C. Wells, A formalism for the specification of essentially-algebraic structures in 2-categories. Mathematical Structures in Computer Science 2 (1992), 1-28. [6]A. Tarski, On some fundamental concepts of metamathematics. In Logic, Semantics, Metamathematics, Oxford University Press, 1956. [7]C. Wells, A generalization of the concept of sketch. Theoretical Computer Science 70 (1990), 159-178. [8]C. Wells and Michael Barr, The formal description of data types using sketches. In M. Main, A. MElton, M. Mislove and D. Schmidt, editors, Mathematical Foundations of Programming Language Semantics, Springer Lecture Notes in Computer Science 298. Springer-Verlag, 1988. Atish Bagchi Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA axb35(a)po.cwru.edu Charles Wells Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA cfw2(a)po.cwru.edu ==============================================================================

1 0

diagrams yet again
by Paul Taylor 09 Oct '92

09 Oct '92

Having criticised (ticked off) certain senior categorists for giving terse and uninformative answers to naive category theory questions, perhaps I ought to give more helpful responses to TeX questions. LaTeX 3 is a general and extensive re-write of LaTeX. I don't fully understand the terms of reference, though they started as making amstex work with LaTeX. Some very amateurish CDs were in amstex, so we may take it that the present objectives are to do (ie make compatible and recommend a package to do) that much, but more professionally. There were CDs in amstex because (presumably) whoever at AMS specified it considered that they were already an important mode of expression IN MATHEMATICS AS A WHOLE. Rectangular diagrams without 2-cells are very commonly found. We all know exactly what the idiomatic usage of such diagrams is and that we would be lost without them. Moreover the fact that Mike Spivak, Steven Smith, Kris Rose and I have put a lot of time into developing the matrix notation of TeXercise 18.46, that Francis Borceux came up with the same idiom without reading the TeXbook, and that large numbers of users have found these five packages convenient are evidence that this is the most appropriate way of rendering such diagrams in machine- (and, of course, user-) readable form. The strings, braids, etc., are a completely different matter. It is not belittling the work done on these topics, in Australia in particular, to say that they are of minority interest, compared to the use of the simpler forms of diagrams. Nor would I be accusing Ross of riding a bandwagon if I suggest that in five years' time he'll probably be interested in something else and drawing a completely different kind of diagram. Meanwhile others on the fringe of the expanding categorical cosmos will only just be learning to use commutative \square's. With such a major piece of programming as CD drawing, "what you see" (type) and "what you get" (see on paper) are completely different things and are to be thought of (designed) separately. For example, the diagrams in my thesis (as submitted to Cambridge in 1986) look pretty horrible, but substituting a recent version of my diagrams package (and, I confess, a little bit of global editting) yields an aesthetically far superior result for (almost) the same input. Later (say post Sept 1989) sources are adapted more easily. I have continued to support the same input language whilst developing the output. With the exception of a few details, the original language design decisions turned out to be good ones. Those who have asked me in person "how do you do this in TeX" will have found that I have tricks up my sleeve which I use in my own papers but am reluctant to explain. Other things have had loud "PROTOTYPE" warning messages in them. This is because any piece of code I give out I have a duty to maintain (in the sense I've mentioned, of continuing to parse the input and producing similar or better output), so until I'm sure that I'm happy with the input language I won't release things. Consequently I sometimes get overtaken. So the short answer to Ross's comment (at the risk of compromising my own typographical principles and contradicting Mike Barr's recent [private] comment to me, "Hell, at least we agree on TeX!" :-) ), is, you're right in sticking to MacDraw for what are for the time being ad hoc diagrams. You can use epsf.sty to import them into LaTeX documents. That is after all the modern equivalent of getting the engraver to do it. When the idiom has become clear, and you've got me sufficiently interested in the subject to want to draw the diagrams myself, then I'll write your macros. Paul ==============================================================================

5 5