Subj:	linear logic guide
Date: Tue, 27 Oct 92 10:50:52 EST
From: andre@saul.cis.upenn.edu (Andre Scedrov)



                    A Brief Guide to Linear Logic  

                            Andre Scedrov 


      Abstract.  An overview of linear logic is given, including 
      an extensive bibliography and a simple example of the close 
      relationship between linear logic and computation.

      Available by anonymous ftp from host ftp.cis.upenn.edu and 
      the file pub/papers/scedrov/guide.dvi . The bibliography is 
      also available separately from pub/papers/scedrov/LL-bib.bib . 

==============================================================================
Subj:	What mathematicans can learn from c.s.
Date:        Wed, 11 Nov 92 12:13:13 AST
From: Charles Wells <cfw2@po.cwru.edu>

A revised version of my paper, "What mathematicians can learn
from computer science", is now available by ftp from

ftp.cwru.edu

Here is how you get it in detail:

1. ftp to ftp.cwru.edu

2. Login as "anonymous"; give your email address as the password.

3. Change directories to /math/wells

      cd /math/wells

4. Set file type to BINARY:

      binary

5. Transfer the file:

      get wmclfcs.dvi

6. Quit:

      bye

I will be happy to supply printed copies to anyone who asks.

The other paper I wrote this spring, "Varieties of mathematical
prose" has gained Atish Bagchi as a co-author and should be
available during the spring of 1993.


--
Charles Wells
Department of Mathematics, Case Western Reserve University
University Circle, Cleveland, OH 44106-7058, USA
216 368 2893

==============================================================================
Subj:	Additional structure on representing objects
From: "Allen Knutson" <aknaton@math.Princeton.EDU>
Date: Mon, 16 Nov 92 22:34:21 EST

The object representing a functor from a category C to Set is well 
understood, being unique if it exists up to unique isomorphism and 
all that. In the only case I'm familiar with, functors from k-Alg to 
Grp, the representing objects can be given a Hopf algebra structure
with which to determine the group structure.

Is there a general theory on how to give representing objects additional
structure, when one is interested in functors to other categories
than Set (of which the above example would be a particular case)?

In the case I'm dealing with in particular, the terminal category has
as objects affine spaces.

If this is well covered in the literature, please forgive the question
and just point me to a reference. Thanks very much!		Allen K.
==============================================================================
Subj:	Sconing and Relators
Date: Tue, 17 Nov 92 17:39:31 EST
From: andre@saul.cis.upenn.edu (Andre Scedrov)


                      NOTES ON SCONING AND RELATORS  

                     John Mitchell and Andre Scedrov


      ABSTRACT. A semantics of typed lambda calculi based on relations 
      is described. The main mathematical tool is a category-theoretic 
      method of sconing, also called glueing or Freyd covers.  Its 
      correspondence to logical relations is also examined. In the case 
      of polymorphic types, a central role is played by relators, i.e., 
      maps that take objects to objects and relations to relations.  
      Sconing may be used to express relators as functors, indeed, as 
      certain object maps on an appropriate category. These notes are 
      intended to be accessible to readers with minimal background in 
      category theory.  

  Available using anonymous ftp from host ftp.cis.upenn.edu and the file 
  pub/papers/scedrov/rel.dvi  or  pub/papers/scedrov/rel.ps .  
==============================================================================
Subj:	Re: Additional structure on representing objects(twice)
Date: Tue, 17 Nov 92 10:07:03 EST
From: pjf@saul.cis.upenn.edu (Peter Freyd)

Affine spaces over a give field are easily seen to be algebras of a
particular equational theory.  Hence the answer to Allen Knutsun's question:

 Is there a general theory on how to give representing objects additional
 structure, when one is interested in functors to other categories
 than Set?  In the case I'm dealing with in particular, the terminal 
 category has as objects affine spaces.

can be found in the ancient work:

  Algebra-valued functors in general and tensor products in particular,
     Colloquium Mathematicum, XIV, 1966.
++++++++++++++++++++++++++++++++++++++++++++++++++
Date: Wed, 18 Nov 92 10:29:51 +1100
From: kelly_m@maths.su.oz.au (Max Kelly)

There are many references. See e.g. Foltz, Lair, Kelly, JPAA 17 (1980), 171 - 177.
Max Kelly.
==============================================================================
Subj:	Re: Fibration of categories
Date:	Wed, 18 Nov 1992 05:45:50 -0500
From:	rkieboom@tena2.vub.ac.be (Rudger Kieboom)

I am interested in fibrations of categories.Being a homotopy theoreticist
I got acquainted with this subject through Ronnie BROWN's paper on
fibrations of groupoids (1970). Can anyone help me to find recent papers
on this subject ? Thanks for the trouble.

Rudger Kieboom (Brussels).
==============================================================================
Subj:	Categories with faithful functors to a group
Date:    Wed, 18 Nov 1992 10:15:16 -0500 (EST)
From:    D_FELDMAN@UNHH.UNH.EDU

Have categories that are equipped with a faithful functor to some group  (or
perhaps monoid) ever been singled out as objects of study?   I am especially
interested in the use they might be put to as a categorical framework for
quasiperiodicity.  

Here is the sort of thing I have in mind. Consider the Euclidean plane
decorated with a particular Penrose tiling.  For definiteness, regard the
tiling as the characteristic function of the union of the edges of all the
tiles.  Consider the category  C  whose objects are non-empty open subsets 
of the plane such that given objects U and V,  Hom(U,V) consists of functions
f:U --> V which are restrictions of rigid motions of the plane and which 
commute with the tiling.  Then there is a forgetful functor from C to
the group of rigid motions of the plane.

David Feldman
Department of Mathematics
University of New Hampshire

==============================================================================
Subj:	Re: Fibration of categories
From: Kirill Mackenzie <K.Mackenzie@sheffield.ac.uk>
Date: 18 Nov 92 16:16:36 GMT

> I am interested in fibrations of categories.Being a homotopy theoreticist
> I got acquainted with this subject through Ronnie BROWN's paper on
> fibrations of groupoids (1970). Can anyone help me to find recent papers
> on this subject ? Thanks for the trouble.

> Rudger Kieboom (Brussels).

The paper by P. J. Higgins and myself,

"Fibrations and quotients of differentiable groupoids",
J. London Math. Soc.(2) {\bf 42} (1990) 101--110.

characterizes fibrations in Brown's sense in terms of the congruences they
determine, and shows that a 'First Isomorphism Theorem' can be given for
fibrations provided one extends the notion of normal subgroupoid. This paper
is written in differentiable terms, but (as far as we know) the results were
new also for the underlying algebra. They can be regarded as a kind of
descent construction.
                      Kirill Mackenzie
==============================================================================
Subj:	Re: Fibration of categories
From: piggy@hilbert.maths.utas.edu.au (La Monte Yarroll)
Date: Thu, 19 Nov 92 13:59:31 EST

> 
> Date:	Wed, 18 Nov 1992 05:45:50 -0500
> From:	rkieboom@tena2.vub.ac.be (Rudger Kieboom)
> 
> I am interested in fibrations of categories.Being a homotopy theoreticist
> I got acquainted with this subject through Ronnie BROWN's paper on
> fibrations of groupoids (1970). Can anyone help me to find recent papers
> on this subject ? Thanks for the trouble.
> 
> Rudger Kieboom (Brussels).

This may be a little outside your realm of interest, but it is very
recent.

Du\u{s}ko Pavlovi\'{c}'s thesis, "Predicates and Fibrations" includes
a nice chapter on fibrations as variable categories.  From the
introduction to that chapter:

	... The theory of fibrations, or fibered categories, is just
	category theory relative to a bse category.  Ordinary
	categories can be viewed as fibered over 1.
==============================================================================
Subj:	Re: Categories with faithful functors to a group
Date: Thu, 19 Nov 92 10:25:28 +1100
From: street@macadam.mpce.mq.edu.au

>Date:    Wed, 18 Nov 1992 10:15:16 -0500 (EST)
>From:    D_FELDMAN@UNHH.UNH.EDU
>
>Have categories that are equipped with a faithful functor to some group  (or
>perhaps monoid) ever been singled out as objects of study?
   
One reference is: A. Froehlich & C.T.C. Wall "Graded monoidal categories"
Compositio Matematica Vol 28 Fasc 3 (1974) 229-285 (graded here is wrt a
group; and the applications they had in mind were equivariant Brauer group,
representations of groups by automorphisms of algebraic structures, theory
of quadratic & Hermitian forms).

Fibrations into groupoids are very important. The only reference that comes
to mind (but I hope other people can remember more) is the recent Memoir of
the AMS by R. (Bob) Gordon, and here is my review:

Review of: "G-Categories"    by Gordon

	       The literature of algebraic topology and representation theory is
sparsely sprinkled with ad hoc results about categories on which a group  G
 acts; here called G-categories. Category theory has a lot to say about
G-categories because they are special cases of many structures: for
example, categories internal to a presheaf topos, G-graded categories,
categories fibred over  G  (or G-indexed categories),  categories with homs
enriched in a (non-symmetric) biclosed monoidal category, algebras for a
doctrine. Yet, it is precisely this diversity of views that makes it
worthwhile beginning a systematic theory as done in the present memoir. All
the peculiarities of G-categories are explained by no single view, and some
by none.  The author is motivated, it seems, by the prospect of
applications to modules over G-graded algebras. There is particular value
in having this work done by someone whose speciality is outside category
theory. 
	       Limits, representability, adjointness and cotripleability are all
adapted to the G-context. The author is interested in the control the
stable subcategory has over its ambient G-category. However, the reviewer
believes stability considerations entered too strongly into the choice to
consider only conical limits (= Kan extensions along the unique functor
into the trivial G-set), and that a more versatile notion would have been
Kan extension along functors into the G-set G (acting on itself by
multiplication); this would have been discovered had a formula for Kan
extensions been included.
	       For the variant of the Yoneda Lemma, a special G-category 
Par(G-Set)  is introduced to receive the hom functors of G-categories. It
is interesting to observe that this does actually come out of the viewpoint
of G-sets as presheaves on  G  (as a one-object category). The gross
internal full subcategory of the category of presheaves on  C  in the sense
of the reviewer ["Cosmoi of internal categories", Transactions of the
American Mathematical Society 258 (1980) 271-318] was shown to be the
category-valued presheaf on  C  whose value at  u C  is the category of
presheaves on  C/u;  it can be checked that this is equivalent to 
Par(G-Set)  when  C = G.  Indeed, the G-groupoid  C/u  is used by the
author to discuss systems of isomorphisms and stably closed G-categories.
	       There is a section on "transversals". Transversaled functors
between G-categories arise, for a category theorist, from the view that
G-categories are categories fibred over  G;  they are then the appropriate
morphisms (more general than G-functors). Alternatively, they are
pseudonatural transformations between category-valued functors on  G. 
Because of the inverses in  G,  the author is able to prove that, if one of
the functors in an adjunction is a G-functor, then the other admits a
transversal, but is generally not a G-functor. 
	       The memoir is written for algebraists with a basic knowledge of
category theory, yet there is much to stimulate the expert. 

----------------------

Regards,
Ross 


==============================================================================
Subj:	Object-speak --> Sets ?
From:	Al Vilcius <vilcius@mathstat.yorku.ca>
Date:	Tue, 24 Nov 1992 23:14:01 -0500

For various reasons, I find myself needing to know something
about object-oriented programming and seek  help from my learned
friends and acquaintances in understanding what it is all about
in categorical terms.

"Object-speak" is the terminology used in the so called object-
oriented technology, implemented in the (now ten year old) 
programming language C++ and in other languages as well.
It uses terms (taken here from   David A. Taylor's  "Object-
Oriented Technology" Addison-Wesley 1990) such as:

object:   a software packet that contains a collection of 
          related data (in the form of variables) and methods 
          for operating on that data.

method:   a procedure contained within an object that is made
          available to other objects.

message:  a signal from one object to another that requests the
          receiving object to carry out one of its methods.

class:    a template for defining the methods and variables for 
          a particular type of object; can contain subclasses
          which are special cases.

instance: refers to an object that belongs to a particular class.

inheritance:   a mechanism whereby classes can make use of the
               methods and variables defined in all classes above
               them on their branch of the class hierarchy.

encapsulation: a technique in which data is packaged together
               with its corresponding procedures. In object-
               oriented technology, the mechanism for
               encapsulation is the object.

data abstraction:   the process of defining new higher-level 
                    data types.

polymorphism:  the ability to hide different implementations
               behind a common interface to simplify
               communications among objects.

What does all this really mean?
Does all this structure lead to (or arise from) a theory?
Is there an interpretation of "object-speak" in a category (with
what properties ?) so that it might be understood in category
theoretic terms?
Are there any references that explicitly make such a connection?

Al Vilcius, Toronto
==============================================================================
Subj:	Some idle questions
From: "Allen Knutson" <aknaton@math.Princeton.EDU>
Date: Wed, 25 Nov 92 23:05:32 EST

Are there famous results that can be stated as "Every functor from category
A to concrete category B is representable"? Or at least "Every functor
from this class that would a priori seem to be too large is representable"?

I don't have any use for such a result, I just want to have more feeling
for representability vs nonrepresentability.

A more specialized question: the representing object for a representable
functor from k-Alg to Grp gets a natural commutative Hopf algebra structure.
This can be generalized in two ways: lose representability, and just have
a functor, or lose commutativity, and just have a noncommutative Hopf
algebra. Has anyone ever seen an example where it was desirable to lose
both, somehow?							Allen K.
==============================================================================
Subj:	! as comonad or adjunction?
Date: Thu, 26 Nov 92 01:45:43 PST
From: Vaughan Pratt <pratt@cs.stanford.edu>

Can anyone give me a good reason for taking ! literally as a comonad
when defining the notion of "model of linear logic"?

The problem I have with it is that it seems to force either the
co-Kleisli or co-Eilenberg-Moore category on you.  I have two
objections to this.  First, correct me if I'm wrong but I was under the
impression that co-Eilenberg-Moore categories were hard to determine.
Second, again correct me if I've misunderstood this, but if you have a
particular adjunction in mind and F is not comonadic, then when you
plug FU into the definition it won't give your F and U back.  Instead
it will go into convulsions trying to find some comonadic adjunction
that you didn't want in the first place.

The alternative I have in mind is that the notion of model should be
defined so as to permit you to specify an adjunction F -| U such that
! = FU.  This allows you to use whatever nice adjunction you had in
mind in place of the canonical one determined by FU.

One might require that U be monadic, but I don't see any compelling
reason to require this.

I've been doing just this for the past couple of years, but it occurs
to me that the notion of "model of linear logic" might need to be
standardized at some point, in which case it would be a pity if it got
this detail wrong.

Vaughan Pratt
==============================================================================
Subj:	Re:  Object-speak --> Sets ?
Date: Thu, 26 Nov 92 12:43:15 -0800
From: Jose Meseguer <meseguer@csl.sri.com>

Regarding the question by Al Vilcius, the most direct correspondence with
category theory that I am aware of is in my recent work on the foundations
of object-oriented programming using rewriting logic.  Two relevant refences
are:

 "Conditional Rewriting Logic as a Unified Model of Concurrency," Theoretical
  Computer Science, 96, 73-155, 1992.

 "A Logical Theory of Concurrent Objects and its Realization in the Maude
  Language," Technical Report SRI-CSL-92-08, Comp. Sci. Lab., SRI 
  International, July 1992.

The first paper focuses more on the logic and the categorical foundations but
contains also a discussion of object-oriented programming and of other models.
The second treats in much more detail the foundations of object-oriented
programming.

The report can be obtained free of charge by writing or sending email to:

 Mrs. Judith Burgess
 Computer Science Laboratory
 333 Ravenswood Avenue
 Menlo Park
 CA 94025, USA

 (burgess@csl.sri.com)

Jose Meseguer

==============================================================================
Subj:	Re:  Some idle questions
Date: Fri, 27 Nov 92 11:38:25 EST
From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic)

>Are there famous results that can be stated as "Every functor from category
>A to concrete category B is representable"? Or at least "Every functor
>from this class that would a priori seem to be too large is representable"?

One version of the Giraud theorem says:
	A category E is Grothendieck topos if and only if every
	contravariant functor from E to Set, which takes colimits to
	limits, is representable. 
This is somewhere in expose IV of SGA4 (Springer LNM 269); also in the
appendix of Barr's Exact Categories (Springer LNM 236)... 

The questions of this kind were studied more in the early days of
category theory. There are several propositions in the form which
interests you in Lambek's book on completions (Springer LNM 24).

	Regards,
	Dusko
==============================================================================
Subj:	Re: ! as comonad or adjunction?
Date: Thu, 26 Nov 92 21:44:28 PST
From: Vaughan Pratt <pratt@cs.stanford.edu>

In asking my previous question about comonads vs. adjunctions in linear
logic I had assumed a negative answer to the following question:

Need the Kleisli category be the only CCC among the adjunctions
defining a Girard comonad !:D->D (one with !(AxB)^!(A)@!(B), !(1)^I)?

What is the truth of the matter?

Under the proposed definition of ! (just a comonad, no specification of
the intended adjunction) a counterexample to the above would be ruled
out as a model of linear logic in the sense that abstracting the
adjunction to a comonad in effect replaces the intended CCC by the
(distinct) Kleisli CCC.

Vaughan Pratt
==============================================================================
Subj:	Re: Object-speak --> Sets ?
From: Joseph A Goguen <goguenja@newton.ccs.tuns.ca>
Date: Thu, 26 Nov 92 18:00:45 AST

Dear Al Vilcius,

Yes, I have done some work along the lines that you query, using theories and
models from hidden sorted equational logic to explicate classes and objects.
You can find details in

 @incollection(tpasth,
 title = "Types as Theories",
 author = "Joseph Goguen",
 booktitle = "Topology and Category Theory in Computer Science",
 editor = "George Michael Reed and Andrew William Roscoe and Ralph F. Wachter",
 publisher = "Oxford",
 year = 1991,
 pages = "357--390",
 note = "Proceeding of a Conference held at Oxford, June 1989")

As a general orienting remark (pun intended), existing languages tend to have
been designed from an ad hoc, partial instantiation of the relevant concepts.
For example, C++ was constrained to be an extension of C, and hence inherits
all of its faults and limitations, with the result that it cannot realise the
full potential of the object paradigm.

Also, I do not quite agree with all of the definitions that you quote.  In
particular, it is significant that "objects" have actual dedicated local
storage; hence, they are not just software; they are run-time entities.  And
"polymorphism" as usually understood in computing has to do with overloading
operations; perhaps this is intended to be a reference to what is usually
called "dynamic binding"?  If so, it is unnecessarily oblique and obscure.
The definition of "data abstraction" is not much better.

Yours,
Joseph Goguen
&&&&&&&&&&&&&&&&&&&&&&&&&&&&& Signature File &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Joseph A. Goguen, Professor of Computing Science, Programming Research Group,
University of Oxford, 11 Keble Road, Oxford OX1 3QD, United Kingdom.

email: Joseph.Goguen@prg.ox.ac.uk [internet] -- usually also works in the
  UK, but if not, try Joseph.Goguen@uk.ac.ox.prg

phone: 272567 [my office]; 272568 [secy]; 273838 [PRG office]; 273839
  or 272582 [FAX].  From USA, dial 011-44-865-...; from UK, dial (0865)-...

==============================================================================
1aug92-1jan93, sabbatical:

    Technical University of Nova Scotia
    School of Computer Science
    P.O.Box 1000, Halifax, Nova Scotia, Canada B3J 2X4
    phone: (902)420-7776 [direct]; (902)420-7718 [sec]; (902)420-7858 [fax]
    email: goguenja@newton.ccs.tuns.ca
      [email to goguen@prg.ox.ac.uk should also be forwarded]

Our home address is:

    5742 Victoria Rd, Halifax, Nova Scotia B3H 1N2 Canada
    phone: (902)422-1361

==============================================================================
Subj:	Re: ! as comonad or adjunction?
Date: Fri, 27 Nov 92 19:50:42 EST
From: barr@triples.Math.McGill.CA (Michael Barr)

One answer to Vaughan's question is that if the original category has
equalizers, then the Eilenberg-Moore category is also a CCC.  With
equalizers too, which makes it, by my estimation, a better model.
A CCC that does not have equalizers is not much of a model of
classical logic, since without equalizers, you cannot form predicates,
at least not freely.

Are there other CCCs?  There is not reason why not, although I don't
any example offhand.

Michael
==============================================================================
Subject: Re:  Object-speak --> Sets ?
From: John C. Mitchell <jcm@cs.stanford.edu>
Date: Fri, 27 Nov 92 14:18:45 -0800


I think we've been through this before, on another forum, and I do
not want to sound overly polemical or partisan, but I do want to
put in my two-cents worth (or whatever currency is appropriate wherever
you are reading this). While I like what Goguen and Meseguer have done,
separately and in collaboration, I think there are many important
aspects of object-oriented programming that their work does not
address. This is true of my work as well, although I think for different
reasons. I believe that there are aspects of object-oriented programming
that are important to programming practicianers (the kind that go to 
object-oriented programming conferences, not the ones with big DARPA
contracts) that have not been adequately characterized in a mathematical
way by any of us. For those interested in applying their favorite mathematical 
theory to a practical (and relatively abstract) problem, I would advocate
attempting to formalize aspects of object-oriented programming.

Did I offend anyone? I hope not. I just don't think the answers are in yet.

John Mitchell
==============================================================================
Subj:	!
Date: Sat, 28 Nov 92 14:09:47 EST
From: barr@triples.Math.McGill.CA (Michael Barr)

I would like to add something to what I said about the !.  Jim Otto
pointed this out to me a year ago.  If you take modules over a
commutative ring it is closed monoidal category.  It is a model for
a fragment of linear logic, missing negation.  Define !M as the free
module generated by the underlying set of M.  Then !(M x N) is !M
tensor !N and so is ostensibly a cofree functor.  The
Eilenberg-Moore category is the category of sets and the Kleisli
category is the full subcategory whose objects are the sets
underlying modules.  To me this seems to mean that unless the !  has
some sensible relation to the linear logic of the category, there is
really no content to the claim that you have a model of classical
logic inside the linear logic.  The only models that seem to fill
that requirement are the cofree coalgebras, assuming they exist.  

Michael

==============================================================================
Subj:	Re:  Object-speak --> Sets ?
Date: Sat, 27 Dec 86 17:01:13 -0800
From: Jose Meseguer <meseguer@csl.sri.com>

I welcome John Mitchell's message, although unfortunately I am leaving for a
two week trip to Europe Monday morning and will not have a chance to
participate in further discussions in this forum while I am travelling.

First let me point out the obvious, namely that neither my message nor
Goguen's contain in my view the slightest hint of having solved all the
problems of object-oriented programming.

My own answer was quite restrictive and tried only to provide some information
on the question of connections between object-oriented programming and
category theory.  It turns out that in my recent work the appropriate models
not only form a category, but are themselves categories, so the connections in
my case are very strong and direct.

Regarding object-oriented programming, I cannot think of a better topic for
discussion at the present time than that suggested by John Mitchell's message.
This is due to the fact that, indeed, a lot remains to be done and that a
comparison of what different approaches have done so far may be very helpful.
I am, however, not sure whether this forum is the best for this kind of
discussion but remain very open and willing to a dialogue of this kind.

What might be useful is some articulation on Mitchell's part of what important
aspects of object-oriented programming are not addressed by my own work or by
Goguen's.  In Section 9 of the Technical Report SRI-CSL-92-08 that I
mentioned, I discuss related work, including type theory approaches and
Mitchell's work in particular, so I have already payed my dues to some extent.

One last point.  Although Joseph Goguen and I have worked together in the past
on the semantics of object-oriented programming and the FOOPS language (see
our "Unifying Functional, Object-Oriented and Relational Programming with
Logical Semantics" in B.  Shriver and P. Wegner (eds.) "Research Directions in
Object-Oriented Programming," MIT Press, 1987, pp. 417-477) and share a good
deal of ideas on the matter, in the past few years each of us has explored
different semantic foundations--logics with hidden sorts in his case, as
pointed out in his message to Vincius, and rewriting logic in mine--and it is
probably confusing the matter to group our current positions together, because
they are different.

Sincerely,

 Jose Meseguer


