Subj: linear logic guide Date: Tue, 27 Oct 92 10:50:52 EST From: andre@saul.cis.upenn.edu (Andre Scedrov) 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 . ============================================================================== Subj: What mathematicans can learn from c.s. Date: Wed, 11 Nov 92 12:13:13 AST From: Charles Wells A revised version of my paper, "What mathematicians can learn from computer science", is now available by ftp from ftp.cwru.edu Here is how you get it in detail: 1. ftp to ftp.cwru.edu 2. Login as "anonymous"; give your email address as the password. 3. Change directories to /math/wells cd /math/wells 4. Set file type to BINARY: binary 5. Transfer the file: get wmclfcs.dvi 6. Quit: bye I will be happy to supply printed copies to anyone who asks. The other paper I wrote this spring, "Varieties of mathematical prose" has gained Atish Bagchi as a co-author and should be available during the spring of 1993. -- Charles Wells Department of Mathematics, Case Western Reserve University University Circle, Cleveland, OH 44106-7058, USA 216 368 2893 ============================================================================== Subj: Additional structure on representing objects From: "Allen Knutson" Date: Mon, 16 Nov 92 22:34:21 EST The object representing a functor from a category C to Set is well understood, being unique if it exists up to unique isomorphism and all that. In the only case I'm familiar with, functors from k-Alg to Grp, the representing objects can be given a Hopf algebra structure with which to determine the group structure. Is there a general theory on how to give representing objects additional structure, when one is interested in functors to other categories than Set (of which the above example would be a particular case)? In the case I'm dealing with in particular, the terminal category has as objects affine spaces. If this is well covered in the literature, please forgive the question and just point me to a reference. Thanks very much! Allen K. ============================================================================== Subj: Sconing and Relators Date: Tue, 17 Nov 92 17:39:31 EST From: andre@saul.cis.upenn.edu (Andre Scedrov) NOTES ON SCONING AND RELATORS John Mitchell and Andre Scedrov ABSTRACT. A semantics of typed lambda calculi based on relations is described. The main mathematical tool is a category-theoretic method of sconing, also called glueing or Freyd covers. Its correspondence to logical relations is also examined. In the case of polymorphic types, a central role is played by relators, i.e., maps that take objects to objects and relations to relations. Sconing may be used to express relators as functors, indeed, as certain object maps on an appropriate category. These notes are intended to be accessible to readers with minimal background in category theory. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/rel.dvi or pub/papers/scedrov/rel.ps . ============================================================================== Subj: Re: Additional structure on representing objects(twice) Date: Tue, 17 Nov 92 10:07:03 EST From: pjf@saul.cis.upenn.edu (Peter Freyd) Affine spaces over a give field are easily seen to be algebras of a particular equational theory. Hence the answer to Allen Knutsun's question: Is there a general theory on how to give representing objects additional structure, when one is interested in functors to other categories than Set? In the case I'm dealing with in particular, the terminal category has as objects affine spaces. can be found in the ancient work: Algebra-valued functors in general and tensor products in particular, Colloquium Mathematicum, XIV, 1966. ++++++++++++++++++++++++++++++++++++++++++++++++++ Date: Wed, 18 Nov 92 10:29:51 +1100 From: kelly_m@maths.su.oz.au (Max Kelly) There are many references. See e.g. Foltz, Lair, Kelly, JPAA 17 (1980), 171 - 177. Max Kelly. ============================================================================== Subj: Re: Fibration of categories Date: Wed, 18 Nov 1992 05:45:50 -0500 From: rkieboom@tena2.vub.ac.be (Rudger Kieboom) I am interested in fibrations of categories.Being a homotopy theoreticist I got acquainted with this subject through Ronnie BROWN's paper on fibrations of groupoids (1970). Can anyone help me to find recent papers on this subject ? Thanks for the trouble. Rudger Kieboom (Brussels). ============================================================================== Subj: Categories with faithful functors to a group Date: Wed, 18 Nov 1992 10:15:16 -0500 (EST) From: D_FELDMAN@UNHH.UNH.EDU Have categories that are equipped with a faithful functor to some group (or perhaps monoid) ever been singled out as objects of study? I am especially interested in the use they might be put to as a categorical framework for quasiperiodicity. Here is the sort of thing I have in mind. Consider the Euclidean plane decorated with a particular Penrose tiling. For definiteness, regard the tiling as the characteristic function of the union of the edges of all the tiles. Consider the category C whose objects are non-empty open subsets of the plane such that given objects U and V, Hom(U,V) consists of functions f:U --> V which are restrictions of rigid motions of the plane and which commute with the tiling. Then there is a forgetful functor from C to the group of rigid motions of the plane. David Feldman Department of Mathematics University of New Hampshire ============================================================================== Subj: Re: Fibration of categories From: Kirill Mackenzie Date: 18 Nov 92 16:16:36 GMT > I am interested in fibrations of categories.Being a homotopy theoreticist > I got acquainted with this subject through Ronnie BROWN's paper on > fibrations of groupoids (1970). Can anyone help me to find recent papers > on this subject ? Thanks for the trouble. > Rudger Kieboom (Brussels). The paper by P. J. Higgins and myself, "Fibrations and quotients of differentiable groupoids", J. London Math. Soc.(2) {\bf 42} (1990) 101--110. characterizes fibrations in Brown's sense in terms of the congruences they determine, and shows that a 'First Isomorphism Theorem' can be given for fibrations provided one extends the notion of normal subgroupoid. This paper is written in differentiable terms, but (as far as we know) the results were new also for the underlying algebra. They can be regarded as a kind of descent construction. Kirill Mackenzie ============================================================================== Subj: Re: Fibration of categories From: piggy@hilbert.maths.utas.edu.au (La Monte Yarroll) Date: Thu, 19 Nov 92 13:59:31 EST > > Date: Wed, 18 Nov 1992 05:45:50 -0500 > From: rkieboom@tena2.vub.ac.be (Rudger Kieboom) > > I am interested in fibrations of categories.Being a homotopy theoreticist > I got acquainted with this subject through Ronnie BROWN's paper on > fibrations of groupoids (1970). Can anyone help me to find recent papers > on this subject ? Thanks for the trouble. > > Rudger Kieboom (Brussels). This may be a little outside your realm of interest, but it is very recent. Du\u{s}ko Pavlovi\'{c}'s thesis, "Predicates and Fibrations" includes a nice chapter on fibrations as variable categories. From the introduction to that chapter: ... The theory of fibrations, or fibered categories, is just category theory relative to a bse category. Ordinary categories can be viewed as fibered over 1. ============================================================================== Subj: Re: Categories with faithful functors to a group Date: Thu, 19 Nov 92 10:25:28 +1100 From: street@macadam.mpce.mq.edu.au >Date: Wed, 18 Nov 1992 10:15:16 -0500 (EST) >From: D_FELDMAN@UNHH.UNH.EDU > >Have categories that are equipped with a faithful functor to some group (or >perhaps monoid) ever been singled out as objects of study? One reference is: A. Froehlich & C.T.C. Wall "Graded monoidal categories" Compositio Matematica Vol 28 Fasc 3 (1974) 229-285 (graded here is wrt a group; and the applications they had in mind were equivariant Brauer group, representations of groups by automorphisms of algebraic structures, theory of quadratic & Hermitian forms). Fibrations into groupoids are very important. The only reference that comes to mind (but I hope other people can remember more) is the recent Memoir of the AMS by R. (Bob) Gordon, and here is my review: Review of: "G-Categories" by Gordon The literature of algebraic topology and representation theory is sparsely sprinkled with ad hoc results about categories on which a group G acts; here called G-categories. Category theory has a lot to say about G-categories because they are special cases of many structures: for example, categories internal to a presheaf topos, G-graded categories, categories fibred over G (or G-indexed categories), categories with homs enriched in a (non-symmetric) biclosed monoidal category, algebras for a doctrine. Yet, it is precisely this diversity of views that makes it worthwhile beginning a systematic theory as done in the present memoir. All the peculiarities of G-categories are explained by no single view, and some by none. The author is motivated, it seems, by the prospect of applications to modules over G-graded algebras. There is particular value in having this work done by someone whose speciality is outside category theory. Limits, representability, adjointness and cotripleability are all adapted to the G-context. The author is interested in the control the stable subcategory has over its ambient G-category. However, the reviewer believes stability considerations entered too strongly into the choice to consider only conical limits (= Kan extensions along the unique functor into the trivial G-set), and that a more versatile notion would have been Kan extension along functors into the G-set G (acting on itself by multiplication); this would have been discovered had a formula for Kan extensions been included. For the variant of the Yoneda Lemma, a special G-category Par(G-Set) is introduced to receive the hom functors of G-categories. It is interesting to observe that this does actually come out of the viewpoint of G-sets as presheaves on G (as a one-object category). The gross internal full subcategory of the category of presheaves on C in the sense of the reviewer ["Cosmoi of internal categories", Transactions of the American Mathematical Society 258 (1980) 271-318] was shown to be the category-valued presheaf on C whose value at u C is the category of presheaves on C/u; it can be checked that this is equivalent to Par(G-Set) when C = G. Indeed, the G-groupoid C/u is used by the author to discuss systems of isomorphisms and stably closed G-categories. There is a section on "transversals". Transversaled functors between G-categories arise, for a category theorist, from the view that G-categories are categories fibred over G; they are then the appropriate morphisms (more general than G-functors). Alternatively, they are pseudonatural transformations between category-valued functors on G. Because of the inverses in G, the author is able to prove that, if one of the functors in an adjunction is a G-functor, then the other admits a transversal, but is generally not a G-functor. The memoir is written for algebraists with a basic knowledge of category theory, yet there is much to stimulate the expert. ---------------------- Regards, Ross ============================================================================== Subj: Object-speak --> Sets ? From: Al Vilcius Date: Tue, 24 Nov 1992 23:14:01 -0500 For various reasons, I find myself needing to know something about object-oriented programming and seek help from my learned friends and acquaintances in understanding what it is all about in categorical terms. "Object-speak" is the terminology used in the so called object- oriented technology, implemented in the (now ten year old) programming language C++ and in other languages as well. It uses terms (taken here from David A. Taylor's "Object- Oriented Technology" Addison-Wesley 1990) such as: object: a software packet that contains a collection of related data (in the form of variables) and methods for operating on that data. method: a procedure contained within an object that is made available to other objects. message: a signal from one object to another that requests the receiving object to carry out one of its methods. class: a template for defining the methods and variables for a particular type of object; can contain subclasses which are special cases. instance: refers to an object that belongs to a particular class. inheritance: a mechanism whereby classes can make use of the methods and variables defined in all classes above them on their branch of the class hierarchy. encapsulation: a technique in which data is packaged together with its corresponding procedures. In object- oriented technology, the mechanism for encapsulation is the object. data abstraction: the process of defining new higher-level data types. polymorphism: the ability to hide different implementations behind a common interface to simplify communications among objects. What does all this really mean? Does all this structure lead to (or arise from) a theory? Is there an interpretation of "object-speak" in a category (with what properties ?) so that it might be understood in category theoretic terms? Are there any references that explicitly make such a connection? Al Vilcius, Toronto ============================================================================== Subj: Some idle questions From: "Allen Knutson" Date: Wed, 25 Nov 92 23:05:32 EST Are there famous results that can be stated as "Every functor from category A to concrete category B is representable"? Or at least "Every functor from this class that would a priori seem to be too large is representable"? I don't have any use for such a result, I just want to have more feeling for representability vs nonrepresentability. A more specialized question: the representing object for a representable functor from k-Alg to Grp gets a natural commutative Hopf algebra structure. This can be generalized in two ways: lose representability, and just have a functor, or lose commutativity, and just have a noncommutative Hopf algebra. Has anyone ever seen an example where it was desirable to lose both, somehow? Allen K. ============================================================================== Subj: ! as comonad or adjunction? Date: Thu, 26 Nov 92 01:45:43 PST From: Vaughan Pratt Can anyone give me a good reason for taking ! literally as a comonad when defining the notion of "model of linear logic"? The problem I have with it is that it seems to force either the co-Kleisli or co-Eilenberg-Moore category on you. I have two objections to this. First, correct me if I'm wrong but I was under the impression that co-Eilenberg-Moore categories were hard to determine. Second, again correct me if I've misunderstood this, but if you have a particular adjunction in mind and F is not comonadic, then when you plug FU into the definition it won't give your F and U back. Instead it will go into convulsions trying to find some comonadic adjunction that you didn't want in the first place. The alternative I have in mind is that the notion of model should be defined so as to permit you to specify an adjunction F -| U such that ! = FU. This allows you to use whatever nice adjunction you had in mind in place of the canonical one determined by FU. One might require that U be monadic, but I don't see any compelling reason to require this. I've been doing just this for the past couple of years, but it occurs to me that the notion of "model of linear logic" might need to be standardized at some point, in which case it would be a pity if it got this detail wrong. Vaughan Pratt ============================================================================== Subj: Re: Object-speak --> Sets ? Date: Thu, 26 Nov 92 12:43:15 -0800 From: Jose Meseguer Regarding the question by Al Vilcius, the most direct correspondence with category theory that I am aware of is in my recent work on the foundations of object-oriented programming using rewriting logic. Two relevant refences are: "Conditional Rewriting Logic as a Unified Model of Concurrency," Theoretical Computer Science, 96, 73-155, 1992. "A Logical Theory of Concurrent Objects and its Realization in the Maude Language," Technical Report SRI-CSL-92-08, Comp. Sci. Lab., SRI International, July 1992. The first paper focuses more on the logic and the categorical foundations but contains also a discussion of object-oriented programming and of other models. The second treats in much more detail the foundations of object-oriented programming. The report can be obtained free of charge by writing or sending email to: Mrs. Judith Burgess Computer Science Laboratory 333 Ravenswood Avenue Menlo Park CA 94025, USA (burgess@csl.sri.com) Jose Meseguer ============================================================================== Subj: Re: Some idle questions Date: Fri, 27 Nov 92 11:38:25 EST From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic) >Are there famous results that can be stated as "Every functor from category >A to concrete category B is representable"? Or at least "Every functor >from this class that would a priori seem to be too large is representable"? One version of the Giraud theorem says: A category E is Grothendieck topos if and only if every contravariant functor from E to Set, which takes colimits to limits, is representable. This is somewhere in expose IV of SGA4 (Springer LNM 269); also in the appendix of Barr's Exact Categories (Springer LNM 236)... The questions of this kind were studied more in the early days of category theory. There are several propositions in the form which interests you in Lambek's book on completions (Springer LNM 24). Regards, Dusko ============================================================================== Subj: Re: ! as comonad or adjunction? Date: Thu, 26 Nov 92 21:44:28 PST From: Vaughan Pratt In asking my previous question about comonads vs. adjunctions in linear logic I had assumed a negative answer to the following question: Need the Kleisli category be the only CCC among the adjunctions defining a Girard comonad !:D->D (one with !(AxB)^!(A)@!(B), !(1)^I)? What is the truth of the matter? Under the proposed definition of ! (just a comonad, no specification of the intended adjunction) a counterexample to the above would be ruled out as a model of linear logic in the sense that abstracting the adjunction to a comonad in effect replaces the intended CCC by the (distinct) Kleisli CCC. Vaughan Pratt ============================================================================== Subj: Re: Object-speak --> Sets ? From: Joseph A Goguen Date: Thu, 26 Nov 92 18:00:45 AST Dear Al Vilcius, Yes, I have done some work along the lines that you query, using theories and models from hidden sorted equational logic to explicate classes and objects. You can find details in @incollection(tpasth, title = "Types as Theories", author = "Joseph Goguen", booktitle = "Topology and Category Theory in Computer Science", editor = "George Michael Reed and Andrew William Roscoe and Ralph F. Wachter", publisher = "Oxford", year = 1991, pages = "357--390", note = "Proceeding of a Conference held at Oxford, June 1989") As a general orienting remark (pun intended), existing languages tend to have been designed from an ad hoc, partial instantiation of the relevant concepts. For example, C++ was constrained to be an extension of C, and hence inherits all of its faults and limitations, with the result that it cannot realise the full potential of the object paradigm. Also, I do not quite agree with all of the definitions that you quote. In particular, it is significant that "objects" have actual dedicated local storage; hence, they are not just software; they are run-time entities. And "polymorphism" as usually understood in computing has to do with overloading operations; perhaps this is intended to be a reference to what is usually called "dynamic binding"? If so, it is unnecessarily oblique and obscure. The definition of "data abstraction" is not much better. Yours, Joseph Goguen &&&&&&&&&&&&&&&&&&&&&&&&&&&&& Signature File &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&& Joseph A. Goguen, Professor of Computing Science, Programming Research Group, University of Oxford, 11 Keble Road, Oxford OX1 3QD, United Kingdom. email: Joseph.Goguen@prg.ox.ac.uk [internet] -- usually also works in the UK, but if not, try Joseph.Goguen@uk.ac.ox.prg phone: 272567 [my office]; 272568 [secy]; 273838 [PRG office]; 273839 or 272582 [FAX]. From USA, dial 011-44-865-...; from UK, dial (0865)-... ============================================================================== 1aug92-1jan93, sabbatical: Technical University of Nova Scotia School of Computer Science P.O.Box 1000, Halifax, Nova Scotia, Canada B3J 2X4 phone: (902)420-7776 [direct]; (902)420-7718 [sec]; (902)420-7858 [fax] email: goguenja@newton.ccs.tuns.ca [email to goguen@prg.ox.ac.uk should also be forwarded] Our home address is: 5742 Victoria Rd, Halifax, Nova Scotia B3H 1N2 Canada phone: (902)422-1361 ============================================================================== Subj: Re: ! as comonad or adjunction? Date: Fri, 27 Nov 92 19:50:42 EST From: barr@triples.Math.McGill.CA (Michael Barr) One answer to Vaughan's question is that if the original category has equalizers, then the Eilenberg-Moore category is also a CCC. With equalizers too, which makes it, by my estimation, a better model. A CCC that does not have equalizers is not much of a model of classical logic, since without equalizers, you cannot form predicates, at least not freely. Are there other CCCs? There is not reason why not, although I don't any example offhand. Michael ============================================================================== Subject: Re: Object-speak --> Sets ? From: John C. Mitchell Date: Fri, 27 Nov 92 14:18:45 -0800 I think we've been through this before, on another forum, and I do not want to sound overly polemical or partisan, but I do want to put in my two-cents worth (or whatever currency is appropriate wherever you are reading this). While I like what Goguen and Meseguer have done, separately and in collaboration, I think there are many important aspects of object-oriented programming that their work does not address. This is true of my work as well, although I think for different reasons. I believe that there are aspects of object-oriented programming that are important to programming practicianers (the kind that go to object-oriented programming conferences, not the ones with big DARPA contracts) that have not been adequately characterized in a mathematical way by any of us. For those interested in applying their favorite mathematical theory to a practical (and relatively abstract) problem, I would advocate attempting to formalize aspects of object-oriented programming. Did I offend anyone? I hope not. I just don't think the answers are in yet. John Mitchell ============================================================================== Subj: ! Date: Sat, 28 Nov 92 14:09:47 EST From: barr@triples.Math.McGill.CA (Michael Barr) I would like to add something to what I said about the !. Jim Otto pointed this out to me a year ago. If you take modules over a commutative ring it is closed monoidal category. It is a model for a fragment of linear logic, missing negation. Define !M as the free module generated by the underlying set of M. Then !(M x N) is !M tensor !N and so is ostensibly a cofree functor. The Eilenberg-Moore category is the category of sets and the Kleisli category is the full subcategory whose objects are the sets underlying modules. To me this seems to mean that unless the ! has some sensible relation to the linear logic of the category, there is really no content to the claim that you have a model of classical logic inside the linear logic. The only models that seem to fill that requirement are the cofree coalgebras, assuming they exist. Michael ============================================================================== Subj: Re: Object-speak --> Sets ? Date: Sat, 27 Dec 86 17:01:13 -0800 From: Jose Meseguer I welcome John Mitchell's message, although unfortunately I am leaving for a two week trip to Europe Monday morning and will not have a chance to participate in further discussions in this forum while I am travelling. First let me point out the obvious, namely that neither my message nor Goguen's contain in my view the slightest hint of having solved all the problems of object-oriented programming. My own answer was quite restrictive and tried only to provide some information on the question of connections between object-oriented programming and category theory. It turns out that in my recent work the appropriate models not only form a category, but are themselves categories, so the connections in my case are very strong and direct. Regarding object-oriented programming, I cannot think of a better topic for discussion at the present time than that suggested by John Mitchell's message. This is due to the fact that, indeed, a lot remains to be done and that a comparison of what different approaches have done so far may be very helpful. I am, however, not sure whether this forum is the best for this kind of discussion but remain very open and willing to a dialogue of this kind. What might be useful is some articulation on Mitchell's part of what important aspects of object-oriented programming are not addressed by my own work or by Goguen's. In Section 9 of the Technical Report SRI-CSL-92-08 that I mentioned, I discuss related work, including type theory approaches and Mitchell's work in particular, so I have already payed my dues to some extent. One last point. Although Joseph Goguen and I have worked together in the past on the semantics of object-oriented programming and the FOOPS language (see our "Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics" in B. Shriver and P. Wegner (eds.) "Research Directions in Object-Oriented Programming," MIT Press, 1987, pp. 417-477) and share a good deal of ideas on the matter, in the past few years each of us has explored different semantic foundations--logics with hidden sorts in his case, as pointed out in his message to Vincius, and rewriting logic in mine--and it is probably confusing the matter to group our current positions together, because they are different. Sincerely, Jose Meseguer