From cat-dist Fri Aug 1 14:49:37 1997 Received: by mailserv.mta.ca; id AA21329; Fri, 1 Aug 1997 14:48:43 -0300 Date: Fri, 1 Aug 1997 14:48:43 -0300 (ADT) From: categories To: categories Subject: My posting Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 31 Jul 1997 21:33:58 -0400 From: Michael Barr I regret that my recent posting on Pratt's construction should not have been sent to categories. He sent me privately a construction showing that A -o A has at least 2^K dinatural endomorphisms (that is the diagonalization of the functor that takes A,B to A -o B) in chu(Set,K) and I mistakenly thought it had come off the categories bulletin board. But it had been sent to me privately. In any case, the claim is correct and my description for K = 2 is too. Sorry for the mixup. Michael From cat-dist Fri Aug 1 14:51:58 1997 Received: by mailserv.mta.ca; id AA22307; Fri, 1 Aug 1997 14:51:51 -0300 Date: Fri, 1 Aug 1997 14:51:51 -0300 (ADT) From: categories To: categories Subject: JOB OPENING: two post-doc positions rewriting and semantics Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 01 Aug 1997 13:34:15 +0900 From: KINOSHITA Yoshiki The Semantics Group of the Computer Science Division of ETL seeks applicants for two postdoctoral positions in Rewriting and Programming Semantics which are expected to become available from October 15th, 1997. The positions are initially for one and half year (until March 31, 1999) with a possibility of extension to two and half year. The salary will be according to STA (Science and Technology Agency, which offers the budget for these positions) standards, depending on age and experience. The research interests of the group lies in Rewriting and Programming Semantics. Current topics are infinite rewriting and categorical semantics for data refinement. Applications, including a letter of interest, curriculum vita, e-mail address, and the names of at least three references, should be sent to our secretary: Ms Mariko Fujikubo, Computer Science Division, ETL, mailbox 1503 1-1-4 Umezono, Tsukuba, Ibaraki 305 JAPAN. To ensure full consideration, applications should be received by August 25, 1997, but we will accept applications until the positions are filled. Research facilities of the Semantics group are good: the research library and computer equipment are up-to-date. The semantics group currently enjoys support of a COE-grant (centre of excellence) by the Science and Technology Agency of Japan, which allows for invitation of visitors and research trips. The group has strong international connections and is active in organisation of and participation in in various regional and national workshops in Japan. Right now, there are three members: Dr. Yoshiki Kinoshita, Koichi Takahashi and Dr. Fer-Jan de Vries. The 106 year old Electrotechnical Laboratory (ETL) is a large governmental research institute. Research is performed in electronics and informatics; about one fourth of its 529 researchers do research in computer science, artificial intelligence and robotics. ETL is situated in Tsukuba Science City. Tsukuba is located about 50 km North-East of Tokyo with good connections to Tokyo and Narita international airport. For more details see (partly in Japanese) http://www.etl.go.jp/outline.html (on ETL) http://www.etl.go.jp/etl/etlclu/~semantics (on Semantics group) http://www.etl.go.jp/~yoshiki http://www.etl.go.jp/~ferjan Further enquiries can be made to Yoshiki Kinoshita (yoshiki@etl.go.jp) or Fer-Jan de Vries (ferjan@etl.go.jp). -- Yoshiki Kinoshita Computer Language Section, Electrotechnical Laboratory 1-1-4, Umezono, Tsukuba-shi, Ibaraki, 305 Japan phone: +81-298-54-5859 FAX: +81-298-50-3914 e-mail: yoshiki@etl.go.jp From cat-dist Wed Aug 6 08:48:21 1997 Received: by mailserv.mta.ca; id AA19424; Wed, 6 Aug 1997 08:46:35 -0300 Date: Wed, 6 Aug 1997 08:46:35 -0300 (ADT) From: categories To: categories Subject: Preprints available Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 5 Aug 1997 17:19:51 -0400 From: Walter Tholen The following two preprints (joint work with George Janelidze) are available as postscript files from my home page at http://www.math.yorku.ca/Who/Faculty/Tholen/menu.html For titles and abstracts, see below. Walter Tholen -------------------------------------------------------------------------- "Functorial Factorization, Well-pointedness and Separabilty" Abstract: A functorial treatment of factorization structures is presented, under extensive use of well-pointed endofunctors. Actually, so-called weak factorization systems are interpreted as pointed lax indexed endofunctors, and this sheds new light on the correspondence between reflective subcategories and factorization systems. The second part of the paper presents two improtant factorization structures in the context of pointed endofunctors: concordant-dissonant and inseparable-sepaprable. "Extended Galois Theory And Dissonant Morphisms" Abstract: For a given Galois structure on a category C and an effective descent morphism p: E --> B in C we describe the category of so-called weakly split objects over (E,p) in terms of internal actions of the Galois (pre)groupoid of (E,p) with an additional structure. We explain that this generates various known results in categorical Galois theory and in particular two results of M. Barr and R. Diaconescu. We also give an elaborate list of examples and applications. From cat-dist Thu Aug 7 14:13:28 1997 Received: by mailserv.mta.ca; id AA05940; Thu, 7 Aug 1997 14:12:31 -0300 Date: Thu, 7 Aug 1997 14:12:31 -0300 (ADT) From: categories To: categories Subject: preprint Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 7 Aug 1997 15:43:23 +1000 From: Michael Batanin The preprint " Finitary monads on globular sets and notions of computad they generate " is available as postscript files at http://www-math.mpce.mq.edu.au/~mbatanin/papers.html Abstract Consider a finitary monad on the category of globular sets. We prove that the category of its algebras is isomorphic to the category of algebras of an appropriate monad on the special category (of computads) constructed from the data of the initial monad. In the case of the free $n$-category monad this definition coincides with R.Street's definition of $n$-computad. In the case of a monad generated by a higher operad this allows us to define a pasting operation in a weak $n$-category. It may be also considered as the first step toward the proof of equivalence of the different definitions of weak $n$-categories. From cat-dist Fri Aug 8 17:19:58 1997 Received: by mailserv.mta.ca; id AA20976; Fri, 8 Aug 1997 17:19:01 -0300 Date: Fri, 8 Aug 1997 17:19:01 -0300 (ADT) From: categories To: categories Subject: Workshop on Internet Programming Languages: Call For Papers Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 7 Aug 1997 15:00:20 -0500 (CDT) From: Christopher Colby (Apologies for multiple postings of...) CALL FOR PAPERS Workshop on Internet Programming Languages In conjunction with the IEEE Computer Society 1998 International Conference on Computer Languages (http://www.math.luc.edu/iccl98) Loyola University Chicago, USA, 13 May, 1998 The Internet has long provided a global computing infrastructure but, for most of its history, there has not been much interest in programming languages tailored specifically to that infrastructure. More recently, the Web has produced a widespread interest in global resources and, as a consequence, in global programmability. It is now commonplace to discuss how programs can be made to run effectively and securely over the Internet. This workshop will provide a forum for the discussions of all aspects of computer languages for wide-area systems, including specification languages, programming languages, semantics, implementation technologies, and application experience. Papers are sought that describe theoretical results, language designs, implementation techniques, and experiences. Areas of particular interest include, but are not limited to: * Models of mobile computation * Semantic Frameworks * Programming constructs * Implementations * Run-time systems * Internet Models SUMBISSIONS Two categories of papers are requested: presentation papers and poster papers. Presentation papers should be at most 6 double-spaced pages (10 pt on 16 pt) in length. Poster papers should be at most 2 double-spaced page summaries (10 pt on 16 pt). Electronic submissions should be sent to wil98@eecs.tulane.edu. The submissions must be in Postcript form and must be viewable with Ghostview and printable on USletter. The deadline for submission is NOV 10, 1997. Authors will be notified by FEB 18, 1998. Participation in the workshop will be limited to only those who submit papers. ORGANIZING COMMITTEE Henri Bal Vrije Univ, The Netherlands bal@cs.vu.nl Boumediene Belkhouche Tulane Univ, USA bb@eecs.tulane.edu Luca Cardelli Digital SRC, USA luca@pa.dec.com From cat-dist Fri Aug 8 17:19:58 1997 Received: by mailserv.mta.ca; id AA11702; Fri, 8 Aug 1997 17:19:56 -0300 Date: Fri, 8 Aug 1997 17:19:56 -0300 (ADT) From: categories To: categories Subject: ICCL'98 Call For Papers Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 7 Aug 1997 15:00:15 -0500 (CDT) From: Christopher Colby (Apologies for multiple postings of...) CALL FOR PAPERS IEEE Computer Society 1998 International Conference on Computer Languages Loyola University Chicago, USA, 14-16 May, 1998 (http://www.math.luc.edu/iccl98) Sponsored by the IEEE Computer Society Technical Committee on Computer Languages, in cooperation with ACM Special Interest Group on Programming Languages. This is the sixth in a series of conferences devoted to all aspects of computer languages, serving to bring together people broadly interested in machine processable descriptions. The hallmarks of ICCL are diversity, openness to a wide range of linguistic research, and international representation. The focus is on new ideas in languages and language technology which are innovative or experimental in nature. Papers are sought that describe significant new theoretical or experimental results in the design, evaluation or implementation of programming/specification languages. Areas of particular interest include but are not limited to: * Implementation/optimization * Theory/semantics * Abstract interpretation/Flow Analysis * Partial evaluation * Parallel/distributed languages * Object-oriented languages * Functional/logic languages * Multiparadigm languages * Real-time/fault-tolerant languages * Requirements/design/specification languages * Internet programming languages * Domain-specific languages Papers should be at most 20 double-spaced pages in length, should have an abstract of approximately 250 words, and a separate cover page indicating the title, authors, and a list of keywords. Papers will be judged on the basis of their relevance, significance, originality, correctness, and clarity. Accepted papers will appear in a full proceedings published by the IEEE Computer Society Press, for which authors will be expected to sign a copyright release form. Papers may be submitted electronically by sending an e-mail containing a platform-independent postscript file (which can be printed on A4 and/or on 8.5"x11" paper) to the address iccl98@csc.ncsu.edu, or by sending 5 copies of papers to Purush Iyer, program committee co-chair, at the address below. Submissions should be accompanied by a cover letter that includes a return mailing address, telephone number and email address. The papers are due by OCT 1, 1997. Authors will be notified of acceptance or rejection by JAN 20, 1998. Camera ready versions of accepted papers will be due FEB 15, 1998. On the day prior to the Conference, a workshop on internet programming languages is being planned by Henri Bal (bal@cs.vu.nl) and Boumediene Belkhouche (bb@eecs.tulane.edu); details for this and other pre-Conference activities will be publicized in a separate announcement and are also available at http://www.math.luc.edu/iccl98. PROGRAM COMMITTEE CO-CHAIRS Purush Iyer Young-il Choo Dept of Computer Science Gifford-Fong Associates North Carolina State University yic@gfa-genesis.com Raleigh, NC 27695-8206 +1 919-515-7291, purush@csc.ncsu.edu Fax: +1 919-515-2878 CONFERENCE CHAIR David Schmidt Computing and Info. Sciences Dept. Nichols Hall 234 Kansas State University Manhattan, KS 66506 +1 913-532-6350, schmidt@cis.ksu.edu Fax: +1 913-532-7353 PROGRAM COMMITTEE Henri Bal (Vrije University, NL) Boumediene Belkhouche (Tulane University, US) Young-il Choo (Gifford-Fong Associates, US) Radhia Cousot (CNRS & Ecole Polytechnique, FR) Pascal Fradet (IRISA, FR) Dan Friedman (Indiana University, US) Rajiv Gupta (University of Pittsburgh, US) Laurie Hendren (McGill University, CA) Fritz Henglein (DIKU, DK) Purush Iyer (NC State University, US) Joxan Jaffar (National University of Singapore, SG) Kim Marriott (Monash University, AU) Martin Odersky (Univ of South Australia, AU) Jens Palsberg (Purdue University, US) Uday Reddy (Univ of Illinois, Urbana, US) John Reppy (AT&T Research, US) Tom Reps (Univ of Wisconsin, US) Jeremy Gibbons (Oxford Brookes University, UK) Dave Schmidt (Kansas State University, US) Bernhard Steffen (Univ of Passau, DE) LOCAL ARRANGEMENTS CHAIR Konstantin Laufer Loyola University Chicago, IL STEERING COMMITTEE Joseph Urban (Chair), Arizona State Univ., USA Boumediene Belkhouche, Tulane University, USA Pei Hsia, University of Texas, Arlington, USA From cat-dist Sun Aug 10 16:29:22 1997 Received: by mailserv.mta.ca; id AA00363; Sun, 10 Aug 1997 16:28:18 -0300 Date: Sun, 10 Aug 1997 16:28:18 -0300 (ADT) From: categories To: categories Subject: alg-geom daily 9708010 received (over 1354 served) 976 Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 8 Aug 1997 08:27:18 -0400 (EDT) From: James Stasheff has this already made it to your newsletter? ************************************************************ Until August 10, 1998, I am on leave from UNC and am at the University of Pennsylvania Jim Stasheff jds@math.upenn.edu 146 Woodland Dr Lansdale PA 19446 (215)822-6707 Jim Stasheff jds@math.unc.edu Math-UNC (919)-962-9607 Chapel Hill NC FAX:(919)-962-2568 27599-3250 ---------- Forwarded message ---------- Date: Fri, 8 Aug 1997 01:14:18 -0600 (MDT) From: send mail ONLY to alg-geom Reply-To: alg-geom@eprints.math.duke.edu To: alg-geom daily title/abstract distribution Subject: alg-geom daily 9708010 received (over 1354 served) 976 ALGEBRAIC GEOMETRY E-PRINTS DAILY MAILING received from Thu 7 Aug 97 00:00:10 GMT to Fri 8 Aug 97 00:00:11 GMT ------------------------------------------------------------------------------ \\ Paper: alg-geom/9708010 From: carlos@picard.ups-tlse.fr (Carlos Simpson) Date: Thu, 7 Aug 1997 16:31:55 +0000 (59kb) Title: Limits in $n$-categories Author: Carlos Simpson (CNRS, Universit\'e Paul Sabatier, Toulouse, France) Notes: Approximately 90 pages \\ We define notions of direct and inverse limits in an $n$-category. We prove that the $n+1$-category $nCAT'$ of fibrant $n$-categories admits direct and inverse limits. At the end we speculate (without proofs) on some applications of the notion of limit, including homotopy fiber product and homotopy coproduct for $n$-categories, the notion of $n$-stack, representable functors, and finally on a somewhat different note, a notion of relative Malcev completion of the higher homotopy at a representation of the fundamental group. \\ ( alg-geom/9708010 , 59kb) %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%- %%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%%--%% %%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%---%%%--- The most recent addition to the conference page, at http://eprints.math.duke.edu/conferences/alg-geom.html is an announcement of the Opening Workshop of the Symplectic Geometry Year 1997/98, to be held at the University of Warwick, 1-12 September 1997. USEFUL INFORMATION ABOUT THIS SERVER Never `reply' to NO-reply@eprints.math.duke.edu; send all mail to alg-geom@eprints.math.duke.edu, with commands in the SUBJECT LINE. Use a single `get' to request multiple papers, `list macros' for available macro packages, and `help' for a list of available commands and other info. Information about submitting papers can be found at http://eprints.math.duke.edu/archive/alg-geom/submission.html and a list of conferences in algebraic geometry is at http://eprints.math.duke.edu/conferences/alg-geom.html From cat-dist Sat Aug 23 12:42:57 1997 Received: by mailserv.mta.ca; id AA23991; Sat, 23 Aug 1997 12:41:31 -0300 Date: Sat, 23 Aug 1997 12:41:31 -0300 (ADT) From: categories To: categories Subject: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Aug 1997 08:54:15 -0500 From: Daniel J. Yoder My name is Daniel Yoder. I am very interested in learning about Category Theory -- I have in fact purchased a little booklet by a Benjamin C. Pierce entitled "Basic Category Theory for Computer Scientists" -- as part of a software engineering project I am working on. The project started out as an attempt to address my frustrations with existing commercial object-oriented programming tools, like those for Smalltalk and C++. I had been developing the outlines of a "methodology" for describing logical domain models, which could perhaps be loosely compared to an (explicitly) object-oriented version of the Z language. I say loosely because my formal algebra background is very weak. At any rate, eventually I began translating these abstractions into a C++ library and I wanted to see if there wasn't a more formal basis to proceed from. This idea was particularly compelling because I am dealing with a synthesis of functional programming abstractions, a rich object model (which includes my own conception of a category which appears to be vaguely related to the formal one), and graphs (which I was using for representing the model). Presently, my goals are quite modest but I have found it difficult to develop an approach based on existing research because I lack the appropriate mathematical background. So the question is: are there any attempts to map category theory (or type theory or set theory -- I am not sure where the boundaries are) to applications (versus theory per se), roughly analagous to Z or VDM, that might be comprehensible to somewhat without the formal framework? If not, is there a sequence of study you would recommend for proceeding? I have an undergraduate degree and have done some reading about formal algebra and category theory, but I am not sure of the path from the former to the latter, or if that is, in fact, the appropriate path. Any assistance would be greatly appreciated. Thank you for your consideration. - Dan (founder of Tazent Software) From cat-dist Mon Aug 25 11:08:43 1997 Received: by mailserv.mta.ca; id AA07350; Mon, 25 Aug 1997 11:07:42 -0300 Date: Mon, 25 Aug 1997 11:07:42 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Sat, 23 Aug 1997 13:41:12 -0400 (EDT) From: F W Lawvere This is a partial reply to the inquiry by Dan Yoder of Tazent Systems. To create a more engineering-friendly mathematics has been one of the goals of category theory (at least for me since 1959).That of course doesn't prevent some people who know a little about it to claim that it can be enjoyed as "mysticism" and that applied mathematics has no place in it.The fact is that this goal is taking several workers several years of work to achieve; but it is in sight. It must be emphasized that "reading about" algebra will never suffice to understand its applications. Indeed no mathematical science can be "comprehensible to someone without the formal framework".At least a few conscious acts on the part of the individual to learn by participating in the actual scientific reasoning are necessary. As an attempt to provide he interested reader with the materials for doing just that,(1) Steve Schanuel and I prepared a text, CONCEPTUAL MATHEMATICS which will be available from Cambridge University Press after September 2. It is based on a course we gave for freshmen at Buffalo several times in the early 90's, and aims to provide the reader having no previous advanced mathematics with a non-watered-down grasp of some of the basic concepts and examples of categories. We tried to do this without shrinking from correct proofs or precise definitions (as too many books do on the basis of the absurd theory that actual understanding would be incompatible with intuition). In 1987 I prepared for those having a basic understanding of categories,(2) an introduction to the method used in nearly all mathematical applications of categories, namely the systematic use of categories of actions (="presheaves"or A-sets) and natural maps (=homogeneous or equivariant or intertwining or.. maps) between them as the first approximation to modelling any category of situations. This text was written with computer science specifically in mind, and was published as the second section of my paper "Qualitative distinctions between toposes of generalized graphs" in volume 92 of the American Mathematical Society's series CONTEMPORARY MATHEMATICS I would much appreciate to learn opinions on the two questions: a) Is (1) sufficient background for the student who undertakes a serious study of (2) ? and b) Are the applications alluded to in (2) sufficiently suggestive to those who want to use that method ? Further examples of the kind in (2) are in my "Kinship and mathematical categories" which will appear in a volume edited by Jackendoff and Wynn in memory of John Macnamara ( who worked to apply categorical logic to psychology). Although that paper is directed to a problem in anthropology, computer scientists will quickly recognize the kinship with concurrency and other problems of interest to them. Of course there are many writings by other authors with much the same purpose, but I take this opportunity to suggest that (1) followed by (2) may be an approximation to a reasonable course for self-study. Bill Lawvere From cat-dist Mon Aug 25 11:08:50 1997 Received: by mailserv.mta.ca; id AA07391; Mon, 25 Aug 1997 11:08:44 -0300 Date: Mon, 25 Aug 1997 11:08:44 -0300 (ADT) From: categories To: categories Subject: Is cut semantical? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Sun, 24 Aug 1997 08:10:45 -0700 From: Vaughan R. Pratt Cut-free proofs correspond more or less to dinatural transformations, suitably strengthened to require invariance under logical relations when necessary. Is there a semantical counterpart in this sense to proofs with cut? Or is the chaotic nature of cut incompatible with this sort of syntax-semantics correspondence? Vaughan Pratt From cat-dist Mon Aug 25 11:09:51 1997 Received: by mailserv.mta.ca; id AA07485; Mon, 25 Aug 1997 11:09:49 -0300 Date: Mon, 25 Aug 1997 11:09:49 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Mon, 25 Aug 1997 11:24:40 +0100 From: Don Sannella Daniel Yoder wrote: > [...] are there any attempts to map category theory > (or type theory or set theory -- I am not sure where the boundaries are) > > to applications (versus theory per se), roughly analagous to Z or VDM, > that might be comprehensible to somewhat without the formal framework? > If not, is there a sequence of study you would recommend for proceeding? Maybe you will find the following paper useful: D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, to appear (1997). Abstract: The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than new results, and to focus on the basic motivation behind the technicalities presented elsewhere. http://www.dcs.ed.ac.uk/home/dts/pub/concepts.{dvi,ps,pdf} The presentation is intended to be accessible to "ordinary" computer scientists. If you find the approach attractive and want to look at the technical details, follow the many references given in the paper (most of the papers by me are available electronically in http://www.dcs.ed.ac.uk/home/dts/pub/). These details are phrased in terms of simple concepts from category theory, universal algebra and logic. Regards, Don Sannella Univ. of Edinburgh dts@dcs.ed.ac.uk From cat-dist Mon Aug 25 16:47:08 1997 Received: by mailserv.mta.ca; id AA23347; Mon, 25 Aug 1997 16:46:10 -0300 Date: Mon, 25 Aug 1997 16:46:10 -0300 (ADT) From: categories To: categories Subject: Chair in Computing Science at Uppsala University Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Mon, 25 Aug 97 15:00:47 +0200 From: Bengt Jonsson Could you please post the following announcement on the Category Theory Mailing list? Thank you Bengt Jonsson Uppsala University **************************************************************** UPPSALA UNIVERSITY invites applications for a tenured CHAIR (FULL PROFESSOR) IN COMPUTING SCIENCE at the Faculty of Science and Technology. Ref no. 3603/97 Applicants must demonstrate scientific excellence and pedagogical proficiency. The successful candidate is expected to pursue an active research program, perform graduate and undergraduate teaching, and supervise graduate students. The chair is placed in the division for mathematics and computer science, which is nicely located on a campus area for mathematics and information technology (http://www.mic.uu.se/) at Uppsala University. The campus houses chairs and graduate programs in areas including automatic control, computerized image analysis, computer systems, computing science, mathematical logic, mathematical statistics, mathematics, numerical analysis, signal processing, and systems analysis. Information about computer science in the division can be found at the home page of the department of computing science (http://www.csd.uu.se/datalogi/), of computer systems (http://www.docs.uu.se/), or of scientific computing (http://www.tdb.uu.se/). For additional information about the position, consult the dean of mathematics and computer science, prof. Ewert Bengtsson, tel no +46-18-183467 (after June 28 +46-18-4714367), e-mail Ewert.Bengtsson@cb.uu.se. Prospective candidates must contact the office of the faculty in order to receive the full announcement with instructions on how to apply. Please use fax no +46-18-181999 (after June 28 +46-18-4711999), e-mail: Christina.Lindberg@uadm.uu.se, or retrieve the announcement from http://www.csd.uu.se/datalogi/positions97/chair.shtml. Applications must be received on September 10, 1997, at the latest. The faculty wishes to establish a more equal proportion amongst female and male professors, and applications from women are encouraged. From cat-dist Mon Aug 25 16:47:09 1997 Received: by mailserv.mta.ca; id AA23344; Mon, 25 Aug 1997 16:47:00 -0300 Date: Mon, 25 Aug 1997 16:47:00 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory (Yoder) Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 25 Aug 1997 10:47:09 -0400 From: Philip Wadler You might find Burstall and Rydeheard's book useful -- they implement much of category theory in Standard ML. It's published by Prentice Hall, in the series edited by Tony Hoare. -- P From cat-dist Mon Aug 25 16:47:30 1997 Received: by mailserv.mta.ca; id AA22662; Mon, 25 Aug 1997 16:47:29 -0300 Date: Mon, 25 Aug 1997 16:47:28 -0300 (ADT) From: categories To: categories Subject: Re: Is cut semantical? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 25 Aug 1997 08:46:46 -0700 From: Vaughan R. Pratt Just to clarify, my question was about proofs with cut, not about cut itself, whose semantics is perfectly clear. (I received a couple of replies from people who merely answered the question in the subject line, apparently without reading the message.) The difficulty is that the standard semantics of cut as composition is not injective, in that it erases the information as to the location of the cut, as a nasty side effect of associativity. I therefore do not see how to attach semantical significance to proofs with cut, as opposed to their cut-free counterparts where the situation is much clearer. This issue arises not just for the denotational semantics of proof but its operational semantics as well. In theorem-proving, proofs with cut are in principle attractive because they can be quite short in comparison to their cut-free counterparts. In practice the difficulty when backchaining of deciding where to put cuts, and what formula to cut on, seems to make it much harder to find proofs with cut than without. Good decision methods are much easier to find for cut-free logics. Granted that making algorithmic sense of cut (in the context of a proof) is hard enough, can one even make semantic sense of it *in that context*? That is, is there any bijection between proofs with cut and some reasonable class of mathematical objects? Presumably the class will not be closed under composition, at least not of the associative kind. Far from being the answer to my problem, composition is its root. Vaughan Pratt From cat-dist Mon Aug 25 16:48:18 1997 Received: by mailserv.mta.ca; id AA23376; Mon, 25 Aug 1997 16:48:17 -0300 Date: Mon, 25 Aug 1997 16:48:17 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 25 Aug 1997 08:49:39 -0700 From: Vaughan R. Pratt are there any attempts to map category theory (or type theory or set theory -- I am not sure where the boundaries are) to applications (versus theory per se), roughly analagous to Z or VDM, that might be comprehensible to somewhat without the ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ formal framework? ^^^^^^^^^^^^^^^^ This last condition is the kicker. Applying category theory without a grasp of the formal framework is like operating a car without a grasp of how to drive. So I would say a definite "not". If not, is there a sequence of study you would recommend for proceeding? It would be interesting to have some comparison of the effectiveness of the various texts and articles that are aimed at computer scientists and set at a reasonably elementary level. There are quite a few of these, some easily identifiable from their titles. I have no idea which ones work best in practice for beginners. But there are first steps to category theory that one can take that do not require any category text. How comfortable are you with graphs and partially ordered sets (definable as transitive acyclic graphs)? If not very, then this is an excellent place to start. Graphs and posets are more fundamental than categories, in the respective senses that a graph is a basic underlying structure of a category while a poset is a primitive kind of category. Moreover they are versatile and useful concepts that will stand you in good stead in many areas of computer science and elsewhere. Once you are comfortable with graphs and posets the conceptual passage to categories becomes easier. What goes on in categories is for the most part a complicated generalization of what goes on in graphs and posets. The complications arise from the composition law for a category, which amounts to a means for tracking which path one is following in a graph. When there is more than one way to get from A to B, the mathematics of keeping track of those ways gets very interesting. This is what is going on down in the engine room of category theory. Up on the bridge the ship is steered with natural transformations. Both of these levels have their counterparts in poset theory and poset-based logic respectively, and make much more sense when understood in that light. Vaughan Pratt From cat-dist Mon Aug 25 16:49:02 1997 Received: by mailserv.mta.ca; id AA23520; Mon, 25 Aug 1997 16:49:01 -0300 Date: Mon, 25 Aug 1997 16:49:01 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 25 Aug 1997 12:13:34 -0700 From: Michael J. Healy 206-865-3123 So the question > is: are there any attempts to map category theory > (or type theory or set theory -- I am not sure where the boundaries are) > > to applications (versus theory per se), roughly analagous to Z or VDM, > that might be comprehensible to somewhat without the formal framework? > If not, is there a sequence of study you would recommend for proceeding? > > I have an undergraduate degree and have done some reading about formal > algebra and category theory, but I am not sure of the path from the > former to the latter, or if that is, in fact, the appropriate path. Any > assistance would be greatly appreciated. Thank you for your > consideration. > > - Dan (founder of Tazent Software) > I started a project here at The Boeing Company three years ago whose approach is a categorical methodology for software synthesis from specifications. We are using The Kestrel Institute's Specware system, which implements category theory, for this purpose. The Web site for Kestrel is http://www.kestrel.edu/, and click on Projects, then Modular Construction of Very large Knowledge Bases. Quite a bit is being done to translate category theory into terminology more manageable for the non-mathematician, making Specware accessible to a wider audience. Please note that the description here is mine only. I just want to share this because we have had quite a bit of success in our project, and it has put category theory on the map in our little corner of industry. Our most direct application at present is for a separate project that is developing neutral representations for knowledge- based engineering (KBE) systems, which are seeing increasing use. Our specific example at present is the representation of engineering knowledge, and the refinement of it into code, for a program that produces a kind of airplane part design given its overall size and some sizing constraints. The program was synthesized by first developing a colimit of specifications of simple theories about part geometry, materials, manufacturing processes, and a representation of real numbers. The specifications make visible the design and manufacturing rationale---the knowledge---that constitutes the constraints on the specific design. Given sizing values, the layout for a specific design can be calculated. The knowledge is re-usable because of its abstract nature, the use of diagrams and colimits in several categories to build complex specifications from simple components, and a way of implementing functorial program construction from specifications (or better yet, from diagrams). A colleague and I have an initial attempt at a paper in a poster session at the upcoming Automated Software Engineering conference (ASE`97) this November. We also have a paper to appear in the Journal of Intelligent Manufacturing and an associated technical report. A good overall background is a paper by the original developers of the approach: Jullig, R. and Srinivas, Y. V. (1993). Diagrams for Software Synthesis, in Proceedings of KBSE `93: The Eighth Knowledge-Based Software Engineering Conference, IEEE Computer Society Press, pp. 10-19. -- =========================================================================== e Michael J. Healy A FA ----------> GA (425)865-3123 | | FAX(425)865-2964 | | Ff | | Gf c/o The Boeing Company | | PO Box 3707 MS 7L-66 \|/ \|/ Seattle, WA 98124-2207 ' ' USA FB ----------> GB e "I'm a natural man." michael.j.healy@boeing.com B -or- mjhealy@u.washington.edu ============================================================================ From cat-dist Tue Aug 26 12:18:31 1997 Received: by mailserv.mta.ca; id AA16955; Tue, 26 Aug 1997 12:17:06 -0300 Date: Tue, 26 Aug 1997 12:17:06 -0300 (ADT) From: categories To: categories Subject: Re: Is cut semantical? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 26 Aug 1997 09:19:07 -0400 From: Michael Barr Maybe I am being naive, but I always thought that cuts were equivalent to composing arrows. The fact that in getting an arrow A --> B, you could take arbitrary paths A --> C --> B corresponds to the unbounded nature of proofs with cut. Of course, if you can calculate Hom(A,B) directly, this is all irrelevant. Mike From cat-dist Tue Aug 26 12:18:31 1997 Received: by mailserv.mta.ca; id AA15512; Tue, 26 Aug 1997 12:18:12 -0300 Date: Tue, 26 Aug 1997 12:18:12 -0300 (ADT) From: categories To: categories Subject: Re: Is cut semantical? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 26 Aug 1997 09:41:49 -0400 From: Michael Barr I should clarify. Proofs with cuts correspond to composable paths. If you like, to proofs in the graph (or free category) of a category. Michael From cat-dist Wed Aug 27 10:32:20 1997 Received: by mailserv.mta.ca; id AA20652; Wed, 27 Aug 1997 10:31:46 -0300 Date: Wed, 27 Aug 1997 10:31:46 -0300 (ADT) From: categories To: categories Subject: Re: Is cut semantical? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 26 Aug 1997 09:25:31 -0700 From: Vaughan R. Pratt From: Michael Barr I should clarify. Proofs with cuts correspond to composable paths. If you like, to proofs in the graph (or free category) of a category. Yes, the free thing on the syntax you're trying to model usually does the job, e.g. the Lindenbaum algebra. But is there any mathematical object arising in nature that works like proofs with cut, the way natural transformations do for cut-free proofs? It is somewhat magical that natural transformations match proofs in this way when they do, and reassuring when they don't: they're letting you know they're alive and require maintenance, unlike free things which are dead and therefore maintenance-free. Vaughan From cat-dist Wed Aug 27 10:32:31 1997 Received: by mailserv.mta.ca; id AA02163; Wed, 27 Aug 1997 10:32:27 -0300 Date: Wed, 27 Aug 1997 10:32:27 -0300 (ADT) From: categories To: categories Subject: e-address change Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 26 Aug 1997 13:19:03 -0500 (CDT) From: J. R. Otto Dear People, My e-address has changed from otto@triples.math.mcgill.ca to quant@mcs.com Thanks, Jim Otto From cat-dist Wed Aug 27 16:34:16 1997 Received: by mailserv.mta.ca; id AA05741; Wed, 27 Aug 1997 16:33:39 -0300 Date: Wed, 27 Aug 1997 16:33:39 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 27 Aug 1997 14:25:10 +0000 From: Steve Vickers Here are a couple of styles of application. 1. The main style is "modularization" - ignoring the internal structure of objects in favour of their external relationship with other objects (specification instead of implementation). Category theory shows how to do this starting from morphisms as basic units of inter-object relationship: given those, objects can then be characterized as products, exponentials etc. A basic method then is to describe morphisms to make a category out of your objects, and use that to give abstract specifications of constructions that are implemented in terms of concrete internal structure. The thesis is that that is better, because it describes the constrction in terms of what you get out of it rather than how it is achieved. The paradigm is sets: internal structure = collection of elements, morphism = function. Look at the early chapters of Goldblatt's book "Topoi" to see how set-theoretic constructions get turned into categorical characterizations. Some applications in computer science are - * types in functional programming (probably in Pierce's book) * work here at Imperial, by Tom Maibaum and myself and others, for specification languages: in crude Z terms, schema connectives (or better-behaved substitutes) can be characterized in a presentation-independent way as products, pullbacks etc. once we know what schema morphisms are. It has to be born in mind that the categorical structure has a quite specific form that prima facie might be insufficient or inappropriate for describing the relationship between objects in particular cases. Nonetheless, in practice it is very often good or a good starting point. Sometimes extra "2-categorical" structure is needed. Again, sometimes you get different kinds of relationship, e.g. terminating computations v. possibly non-terminating ones; or computations with or without side-effects. The structure of Moggi's "Computational Monads" aims to capture this and has been applied by Phil Wadler in functional programming. A pattern of relationship between objects that is very uncategorical is that of "nearness" or "neighbourhoods" as you see in topology. (The two patterns, the categorical and the topological, are combined in a remarkable way in the idea of "topos as generalized topological space". The objects are then the points of a topos instead of the objects of a category.) 2. (Less widespread) Synthetic reasoning for engineer friendliness. This is a kind of inverse to modularization: having ignored concrete internal structure and reduced objects to their categorical relationship with the others, they can seem rather austerely abstract. There is often a formal trick by which an artificial internal structure can be reinvented, and the objects talked about as though they were set-like things, collections of elements. This is intended to make the categories more "engineer-friendly", at a cost of restricting the logical ways one can reason about the collections, and is not unlike the use of infinitessimals as though they were real numbers for doing calculus. Categorical logic studies the interplay between the category theory and the logic. The paradigm example is that of objects in a topos, for which the so-called "Mitchell-Benabou" language enables one to prove theorems about them in a style that ostensibly refers to their elements. (The logical reasoning must be intuitionistic - no proofs by contradiction.) The programme of "synthetic domain theory" has similar ambitions for the domains of denotational semantics, which could be applied to the types of functional programming. I'm working on something of the same kind for contexts where the objects (technically, the points of locales or toposes) also have topological relationships, the corresponding logic being the so-called "geometric logic". Steve Vickers. From cat-dist Thu Aug 28 09:21:08 1997 Received: by mailserv.mta.ca; id AA26018; Thu, 28 Aug 1997 09:20:21 -0300 Date: Thu, 28 Aug 1997 09:20:21 -0300 (ADT) From: categories To: categories Subject: Reviews of books on category theory in c.s. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 27 Aug 1997 17:32:45 -0400 From: Charles Wells A year or two ago someone wrote a comparative review of several books in the area of category theory in computer science. I would appreciate finding out where it is available. Thanks, Charles Wells, Department of Mathematics, Case Western Reserve University, 10900 Euclid Ave., Cleveland, OH 44106-7058, USA. EMAIL: charles@freude.com. OFFICE PHONE: 216 368 2893. FAX: 216 368 5163. HOME PHONE: 440 774 1926. HOME PAGE: URL http://www.cwru.edu/artsci/math/wells/home.html "In theory, there is no difference between theory and practice, but in practice, there is." From cat-dist Thu Aug 28 13:20:01 1997 Received: by mailserv.mta.ca; id AA04522; Thu, 28 Aug 1997 13:19:23 -0300 Date: Thu, 28 Aug 1997 13:19:23 -0300 (ADT) From: categories To: categories Subject: Re: Reviews of books on category theory in c.s. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 28 Aug 1997 09:24:42 -0400 (EDT) From: F W Lawvere Probably Charles is thinking of David Benson's review of five books in COMPUTING REVIEWS Nov 1993, 577-579 under the title "Comparative Review" # 9311-0833. On Thu, 28 Aug 1997, categories wrote: > Date: Wed, 27 Aug 1997 17:32:45 -0400 > From: Charles Wells > > A year or two ago someone wrote a comparative review of several books in > the area of category theory in computer science. I would appreciate > finding out where it is available. Thanks, > > > > > > Charles Wells, Department of Mathematics, Case Western Reserve University, > 10900 Euclid Ave., Cleveland, OH 44106-7058, USA. > EMAIL: charles@freude.com. OFFICE PHONE: 216 368 2893. > FAX: 216 368 5163. HOME PHONE: 440 774 1926. > HOME PAGE: URL http://www.cwru.edu/artsci/math/wells/home.html > > "In theory, there is no difference between theory and practice, > but in practice, there is." > > From cat-dist Thu Aug 28 15:45:06 1997 Received: by mailserv.mta.ca; id AA05351; Thu, 28 Aug 1997 15:44:28 -0300 Date: Thu, 28 Aug 1997 15:44:28 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 28 Aug 1997 20:47:09 +0000 From: Zinovy Diskin For last several years I try to marry category theory (CT, a rather strict and refined lady) and software engineering (SE, a rich gentleman) via (i) building some software theories (semantic modeling, modeling OO databases, metadata modeling) on categorical foundations, (ii) demonstrating the power and relevance of CT in managing some actual practical problems in SE (object-oriented-relational database design, heterogeneous schema integration, structuring schema repositories) and (iii) conducting here, at Frame Inform Systems, a project on implementing a new generation CASE-tool based on categorical principals. During this time I had a few occasions to discuss perspectives of applying CT with experts in SE (together with presenting them a prototype of our CASE-tool), and now could summarize these discussions as follows. Each expert side has (let's suppose) a good knowledge of its subject and a rather fuzzy notion of the opposite subject, correspondingly, each expert's opinion about possibilities of CT-applications is necessarily fuzzy. Nevertheless, up to my feeling of SE and, on the other hand, up to SE experts' understanding of my explanations of the (essence of the) CT-approach, both sides had agreed that CT-applications in SE seem to be extremely promising and just to the point, and both sides were somewhat excited by this coordination of abstract mathematics and practical matters. My colleagues' and my experience in this field is summarized in a declarative document "The Arrow Manifesto: Towards software engineering based on comprehensible yet rigorous graphical specifications" (on ftp: //ftp.cs.chalmers.se/pub/users/diskin/MANIFEST/arrfest.ps); the presentation is intended for software people who are seeking for a universal specification language suitable for SE (and allow the possibility of practically useful theory, these two restrictions single out a limited but definitely non-empty set). The present discussion in categories mailing list is a one more justification of the remarkable coordination mentioned above. Let me continue with a somewhat diverse set of distinct replies (to, mainly, Dan Yoder's and Vaughan Pratt's messages). > are there any attempts to map category theory (or type > theory or set theory -- I am not sure where the boundaries > are) to applications (versus theory per se), roughly > analogous to Z or VDM, that might be comprehensible to > somewhat without the > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > formal framework? > ^^^^^^^^^^^^^^^^ > > This last condition is the kicker. Applying category theory without > a grasp of the formal framework is like operating a car without a > grasp of how to drive. So I would say a definite "not". > The situation is not so hopeless. During my studies of the area of information modeling (or else conceptual modeling, or semantic modeling) I found that the community is, in fact, trying to deal implicitly with topos-theoretic concepts. Of course, all is utterly intermixed -- there are neither a consistent conceptual framework nor even a consistent terminology -- but it turned out to be not very difficult to explain what is the topos SET to qualified practitioners in information modeling . Now I can assert that the SET-specialization of topos-theoretic concepts can be explained to any qualified software man familiar with entity-relationship diagrams, or with object class-reference schemas used in OO-software design, or with any other of similar notations (of course, this does not mean that the notion of abstract topos can be easily explained but this notion is not so important for what I'd call engineering CT, see below). Another software subcommunity well prepared for grasping categorical ideas is that of object-oriented programming. OO is a way of thinking of the world rather than merely a technique for software design. One corner stone of this way is to view the world as consisting of object classes -- nodes, and references between them -- arrows, which is essentially the categorical view. Another corner stone of OO is the so called encapsulation -- accessing objects only via explicitly defined interfaces to them. Note however that this is nothing but the basic CT idea that objects have no internal structure other than that embodied into arrow diagrams adjoint to objects (Lawvere perfectly phrased this as "objectify means to mappify"). In other words, the most fundamental OO-principle of encapsulation can be well seen as a software realization of the fundamental CT principle of mappifying. (Of course, it would be too strong to say that OO is CT-modulated programming but saying "CT is OO-mathematics" seems to be a reasonable thesis). Nevertheless, in spite of good preconditions, the problem of applying CT for SE is extremely hard. It is determined by inherited, genetic gaps between mathematics and engineering. A special case of this general problem is that of teaching CT to software people. > > If not is there a sequence of study you would > recommend for > proceeding? > > It would be interesting to have some comparison of the effectiveness > of the various texts and articles that are aimed at computer > scientists and set at a reasonably elementary level. There are > quite a few of these, some easily identifiable from their titles. I > have no idea which ones work best in practice for beginners. > > But there are first steps to category theory that one can take that > do not require any category text. How comfortable are you with > graphs and partially ordered sets (definable as transitive acyclic > graphs)? If not very, then this is an excellent place to start. > Graphs and posets are more fundamental than categories, in the > respective senses that a graph is a basic underlying structure of a > category while a poset is a primitive kind of category. Moreover > they are versatile and useful concepts that will stand you in good > stead in many areas of computer science and elsewhere. > In contrast to Vaughan, I do not believe that a software person is able to grasp CT as a mathematical theory by tracing some mathematical way how well adapted it would be (via graphs, or posets, or toposes). Normally, a mathematician and an engineer are humans of different cultures of thinking for which not only criteria of well formed intellectual construction are different but their very notions of reasonable intellectual construction differ too. However, I do believe that a software person is quite able to grasp the basic ideas of CT if the latter are explained in software terms and on the ground of this person special professional intuition (like, e.g., it was in my experience of explaining Makkai's sketches as a generalization of ER-diagrams). Of course, such an explanation will not present CT as a formal mathematical theory but hopefully will make it possible to proceed -- to use categorical ideas in software design and development. So, I'd advise Daniel Yoder to invite a mathematician trained in CT, to pay her or him enough money to motivate going into details of software problems Dan tries to manage, and then I believe the mathematician will explain to the employer the essence of CT-approach to employer's problem in terms quite clear and transparent to him. (One of possible answers to the traditional question "What is mathematics needed for?" is "Mathematics is necessary to generate mathematicians"). To summarize, let us return to the initial point: .... > VDM, that might be comprehensible to somewhat without the > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > formal framework? > ^^^^^^^^^^^^^^^^ > > This last condition is the kicker. Applying category theory without > a grasp of the formal framework is like operating a car without a > grasp of how to drive. So I would say a definite "not". I would not take the responsibility to say a definite "yes" but I am sure enough to state a definite "not" on Vaughan's definite "not" (maybe, a specialist in modal logic would infer more from this data :-) Relations between CT and software applications is a special case of general problem of relating mathematics and engineering. To my mind, discussion of such questions needs to involve the notion of what I would call engineering mathematics (e-mathematics) to distinguish it from mathematics of mathematicians (m-mathematics). Mathematicians are inclined to identify mathematics with m-mathematics but this is a too puristic and actually poor view. Consider, for example, the situation with engineering being of analysis. In fact, engineers are familiar with operational rules of differentiation and integration but have a rather fuzzy notion of their denotational semantics. I mean that usually engineers have a rather fuzzy notion of the precise definitions of differentiation and especially integration but successfully use these constructs in their everyday work. (And before inventing the non-standard analysis by A. Robinson, the intersection of e-analysis and m-analysis was not too large). Back to CT: what I want to say in this respect is that the field of CT-applications in SE will hopefully grow and as this process goes a new discipline of *engineering CT* ( e-CT) will begin to emerge. Though it is difficult to predict at present what discipline e-CT will be, some important points can be seen already today. More accurately, what can be seen today is some aspects of me-CT -- a subsystem of m-CT which could serve as a mathematical foundation of e-CT (like the non-standard analysis is a foundation of e-analysis). First of all, the very notion of category is not very important in applications. What an engineer actually needs is an effective and comprehensible presentation of a category (and an additional structure on the top of it). In contrast, categorists prefer to work with closed structures rather than their presentations: categories instead of graphs, monads instead of terms and equations, classifying categories instead of formulas and axioms. So, development of presentation-centered specification machinery within CT should be a must for e-CT (and me-CT supporting it). Two main techniques for specifying presentations were developed in CT. One is to use internal logic (the Mitchell-Benabou language) -- this is suitable for theoretical and teaching purposes but is not satisfactory for applications as the advantages of the graphical CT-syntax are lost in this approach. The other technique is associated with the concept of Ehresmann's sketches which were directly intended for graphical yet formalized presentation of complex strucrtures (but note, complex in the m- rather than e-sense). However, these sketch specifications are based on a very special kind of logic -- the logic of universal diagram properties whereas applications need a much more flexible logic where signatures would be user-defined like, e.g., in the first-order logic, FOL. (Analogously, the possibility to derive all Boolean operations from a single one -- Sheffer's stroke -- is a nice result but it is hardly useful for everyday practical work and applications.) What would be desirable for SE is a graph-based logic and algebra combining the flexibility of the internal logic approach and graph-basedness of sketches. A suitable framework is described in my TechReport "Generalized sketches ..." (on ftp: //ftp.cs.chalmers.se/pub/users/diskin/REPORTS/tr9703.ps). It is based on the constructs of diagram predicate and diagram operation treated as a direct generalization of the ordinary (string-based) predicates and operations considered in FOL. Surprisingly, but the elementary treatment of the elementary notions of diagram predicate and diagram operation was somehow missed in CT. (Of course, some reservations to this statement are needed. As for diagram predicates, they are considered by Makkai in his generalized sketches framework but his presentation hides (i) the elementary nature of these notions and (ii) their parallelism with ordinary string-based predicates. As for diagram operations, they were invented by Burroni but, again, his presentation has a drawback (ii) and, in addition, Burroni's operations produce only one item (arrow or node) while it is quite natural and practically useful to consider diagram operations producing diagrams from diagrams. In addition, there are non-elementary versions of these constructs where too many things are internilized and considered abstract object rather than sets ) . In contrast, the presentation in the TechReport constitutes an elementary treatment of graph-based logic and algebra (and augments it with e-CT-oriented sentiments :-). Maybe, some details would be relevant. As it was said, diagram predicates/operations defined in the report appear as an *immediate* generalization of their ordinary (string-based) counterparts considered in FOL. A diagram predicate is a predicate symbol coupled with a graph of place-holders -- the shape of the predicate, while an ordinary predicate has a set (arrow-free graph) of place-holders. A diagram operation is a diagram predicate whose shape has an additional structure -- a designated subgraph of the input place-holders. The direct string-based counterpart is a set of ordinary operations whereas a single such operation has a set of place-holders in which only one element is not among the input place-holders. A natural next step is to consider shapes (graphs of place-holders) which carry some diagram predicates and operations defined on previous stages, i.e., to consider shapes which are not graphs but generalized operational sketches. When one considers only diagram predicates (operations are absent), this is just Makkai's setting. This framework is quite natural but I'm not aware of its explicit formulation. This is the more surprising as categorists actually use the constructs described above in their everyday work when they draw and chase diagrams. In addition, an accurate formalization of these everyday graphical images leads not to ordinary sketches as it is usually thought but to a bit different constructs which I call *visual sketches*. The latter are based on visual graphs: a visual graph is a surjective graph morphism g: G_v --> G_n where G_v is to be thought of as a graph-as-it-is-drawn (the visual presentation of g) and G_n is to be thought of as a graph of names (the name graph of g). In particular, the shape of the identity arrow predicate is the evident mapping from the graph [ o-->o ] to the loop [ o<----- ]. |___| These considerations give rise to a consistent framework of generalized visual sketches (close to Makkai's generalized sketches but in our setting there are else diagram operations, and they are important ). I believe that nice and practically useful mathematics could be developed along these lines, it should be attributed (in my terminology) to me-CT. Let me finished with a nice imaginary picture. In some (short?) time some engineering discipline, e-CT, will emerge and then CT will be understood as an amalgamation of m-CT and e-CT. This new e-CT under the name of CT will be a basic discipline in the standard undergraduate course of software engineer, a lot of (good and poor) textbooks on CT (actually teaching students to e-CT) will appear, in all advanced software companies there will be a position of CT-consultant and so on. Now the first question is whether this CT-paradise is good for m-CT -- I believe that it is. If so, the second question is must mathematicians work hardly to speed up appearance of this paradise or it is more wise to wait while it will grow up itself of efforts of software engineers? Thank you for your attention, Zinovy Diskin P.S. I'm indebted to Ilya Beylin for comments on a preliminary version of this message (and many occasional discussions of the subject). From cat-dist Fri Aug 29 13:14:52 1997 Received: by mailserv.mta.ca; id AA17522; Fri, 29 Aug 1997 13:13:37 -0300 Date: Fri, 29 Aug 1997 13:13:37 -0300 (ADT) From: categories To: categories Subject: Re: Applications for Category Theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 28 Aug 1997 13:29:08 -0700 (PDT) From: Joseph Goguen Im enjoying the discussion of CT and CS or SWE, although it seems to me to be a bit theoretical. Id like to mention three tools, real implemented software systems that have been and are being used in real software engineering: SpecWare \cite{specware}, LILEANNA \cite{traczth,tracz93}, and TOOR \cite{toor}. All are based on a category theoretic module system called parameterized programming \cite{ppp}. The idea is that specs are theoires and that putting specs together is just colimit; this goes back to work on general systems theory from the late 1960s \cite{gst} and work of Clear from the late 1970s \cite{bg77,bg80sh}. SpecWare actually has colimit as a top level command, but it fails to provide all the module operations which make parameterized programming so powerful. However, it can generate code from sufficiently detailed specs, and has very good documentation, a good user base, and a verification capability. It is produced by Kestrel Inst. LILEANNA fully implements parameterized programming and can compose Ada modules, but it only generates glue code. It was built at Martin-Marietta, and has been used for helicopter navigation software. TOOR supports requirements evolution and full parameterized programming, without verification, but with a good user interface. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @incollection(bg77, title = "Putting Theories together to Make Specifications", author = "Rod Burstall and Joseph Goguen", booktitle = "Proceedings, Fifth International Joint Conference on Artificial Intelligence", editor = "Raj Reddy", publisher = "Department of Computer Science, Carnegie-Mellon University", year = 1977, pages = "1045--1058") @incollection(bg80sh, author = "Rod Burstall and Joseph Goguen", title = "The Semantics of {C}lear, a Specification Language", booktitle = "Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification", editor = "Dines Bjorner", note = "Lecture Notes in Computer Science, Volume 86", publisher = "Springer", pages = "292--332", year = 1980) @techreport(specware, title = "Spec{W}are Language Manual, Version 2.0", author = "Y.V.\ Srinivas and Richard J{\"u}llig", institution = "Kestrel", year = 1996) @inproceedings(tracz93, author = "Will Tracz", title = "{\sc lileanna}: a Parameterized Programming Language", booktitle = "Proceedings, Second International Workshop on Software Reuse", month = "March", year = 1993, note = "Lucca, Italy", pages = "66--78") @phdthesis(traczth, title = "Formal Specification of Parameterized Programs in {\sc lilleanna}", author = "William Joseph Tracz", school = "Stanford University", year = 1997) @incollection(gst71, title = "Mathematical Representation of Hierarchically Organized Systems", author = "Joseph Goguen", year = 1971, editor = "E. Attinger", booktitle = "Global Systems Dynamics", publisher = "S. Karger", location = "Basel", city = "Basil", pages = "112--128") @incollection(gst73, title = "Categorical Foundations for General Systems Theory", author = "Joseph Goguen", booktitle = "Advances in Cybernetics and Systems Research", editor = "F. Pichler and R. Trappl", year = 1973, publisher = "Transcripta Books", location = "London", pages = "121--130") @article(toor, title = "An Object-Oriented Tool for Tracing Requirements", author = "Francisco Pinheiro and Joseph Goguen", journal = "IEEE Software", note = "Special issue of papers from ICRE '96", year = "March 1996", pages = "52--64") @incollection(ppp, title = "Principles of Parameterized Programming", author = "Joseph Goguen", booktitle = "Software Reusability, Volume {I}: Concepts and Models", editor = "Ted Biggerstaff and Alan Perlis", publisher = "Addison Wesley", year = 1989, pages = "159--225")