Re: Applications for Category Theory

Re: Applications for Category Theory

[categories]

Date: Mon, 25 Aug 1997 12:13:34 -0700
From: Michael J. Healy 206-865-3123 <mjhealy@redwood.rt.cs.boeing.com>


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

============================================================================

Re: Applications for Category Theory

[categories]

Date: Thu, 28 Aug 1997 13:29:08 -0700 (PDT)
From: Joseph Goguen <goguen@cs.ucsd.edu>

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")

Re: Applications for Category Theory

[categories]

Date: Thu, 28 Aug 1997 20:47:09 +0000
From: Zinovy Diskin <diskin@fis.lv>

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).

Re: Applications for Category Theory

[categories]

Date: Wed, 27 Aug 1997 14:25:10 +0000
From: Steve Vickers <sjv@doc.ic.ac.uk>

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.

Re: Applications for Category Theory

[categories]

Date: Mon, 25 Aug 1997 08:49:39 -0700
From: Vaughan R. Pratt <pratt@cs.Stanford.EDU>


	 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

Re: Applications for Category Theory

[categories]

Date: Mon, 25 Aug 1997 11:24:40 +0100
From: Don Sannella <dts@dcs.ed.ac.uk>

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

Re: Applications for Category Theory

[categories]

Date: Sat, 23 Aug 1997 13:41:12 -0400 (EDT)
From: F W Lawvere <wlawvere@acsu.buffalo.edu>


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

Applications for Category Theory

[categories]

Date: Fri, 22 Aug 1997 08:54:15 -0500
From: Daniel J. Yoder <dyoder@tazent.com>

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)