re: process algebras

re: process algebras

[Robin Cockett]

Another few papers which may be of interest are:

"Constructing process categories"
J.R,B. Cockett (me!) & D.A. Spooner
TCS 177 (1997) 73-109

"Categories for syncrony and asynchrony"
J.R,B. Cockett & D.A. Spooner
Electronic Notes in Theoretical Computer Science I (1995) 495-520

These papers explore the "combinatorial" representation of processes 
using span categories.  In particular they give an account of
Abramsky's program to model processes (based on a CCS style 
presentation) using span categories.

-robin

Re: process algebras

[dusko]

> Is there any formalization of process algebras in term of categories? I
> would be interested in giving an computational, multi-process semantics
> to certain graphs, and I thought it could be done in terms of a functor
> to a process category (if this concept exists...)
> Is there any literature about this?

around 1995, i had two papers about "convenient categories for process
calculus" and one about "categorical logic of concurrency and
interaction". the simplest way to get them is probably on hypatia, or from
my web page http://www.kestrel.edu/HTML/people/pavlovic/ i am not sure to
which extent is this what you are looking for, but it is surely related.
later samson abramsky and i figured how to deal with process categories
much better, but most of it was never written up. an initial account was
in our CTCS 97 paper (also available, i think, at the same sites.)

-- dusko pavlovic

process algebras

[Anna Labella]

----------
>Da: matthieu amiguet <matthieu.amiguet@info.unine.ch>
>A: categories@mta.ca
>Oggetto: categories: process algebras
>Data: Gio, 20 apr 2000 14:49
>

>Dear categoricians,
>
>Is there any formalization of process algebras in term of categories? I
>would be interested in giving an computational, multi-process semantics
>to certain graphs, and I thought it could be done in terms of a functor
>to a process category (if this concept exists...)
>Is there any literature about this?
>Thank you for your help,
>
>Matthieu Amiguet
>
We have a categorical formalization of process algebras in terms of enriched
category theory. You can see for a general presentation:
S.Kasangian, A.Labella "Observational trees as models for concurrency"
Math. Struct. in Comp.Science (1999) vol.9 pp.687-718

Anna Labella

Osius' set theory

[Paul Taylor]

Elwood Wilkins reminds us that...
> In his 1974 paper Osius showed that there are enough transitive objects
> in the initial topos to define a naive set theory. ...

Gerhard Osius's work was significant in 1974 as one of the ways in which
it was shown that toposes do the same thing as set theory.   In fact Osius's
is, so far as I am aware, the only work that discusses *set* theory -
Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing
as some form of *type* theory.  Of course, it is the latter that
mathematicians actually use when they claim to be using set theory
as foundations, but set theory - epsilontics as Lawvere calls it - is of
some interest in the study of very high powered induction.

Peter Johnstone included a precis of Osius's paper in his book "Topos Theory"
(Academic Press, 1977). Apart from that, I was unable to track down anything
that built significantly on it.  Indeed,  Osius himself didn't seem very
interested when I wrote to him about it (he now does statistics).

The successor to this paper would therefore seem to be my
     "Intuitionistic Sets and Ordinals", J. Symbolic Logic, 61 (1996) 705--744
This develops, in a symbolic way, the notions of "transitive set" and
"ordinal" in the sense of a carrier equipped with an extensional well founded
relation.  Several qualitatively different notions of ordinal arise
intuitionistically.  I also pick up on Osius's set theory and pose some
questions that suggest ways of adapting it to Grothendieck toposes in general.

What remains of considerable interest (once we have agreed that set theory
is wrong, wrong, wrong) is Osius's categorical notion of recursion.

The equation       f(x)  =   r( { f(y) | y in [=element_of] x } )

he writes as the (3=1, not 2=2) commutative square

                            P(f)
  { y | y in x }   P(X)  --------->   P(A)
       ^            ^                  |
       |            |                  |
       |            |                  |
       |            |                  | r
       |            |                  |
       |            |                  |
       -            |        f         v
       x            X  ------------->  A

which we may of course generalise to a "homomorphism" from any P-coalgebra
to any P-algebra, where indeed P may be any functor instead of the covariant
powerset functor.  The coalgebra admits recursion by definition if there is
exactly one such "homomorphism" to any algebra whatever.

The exercises in Chapter VI of my book "Practical Foundations of Mathematics"
(Cambridge University Press, 1999) explore applications of the commutative
square to recursive functional programs.
      http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s6e.html

Osius's 3+1 square is about RECURSION - defining functions or programs -
but I have also considered INDUCTION - proving theorems - categorically.

Again this is a property ("well foundedness") of coalgebras.  See Section 6.3
      http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s63.html
of the book, or my unfinished paper "Towards a Unified Treatment of Induction"
(also known as "On the General Recursion Theorem") which you can get from
my Hypatia page
      http://hypatia.dcs.qmw.ac.uk/author/TaylorP

The final section of the book (s96.html) sketches the way in which this
categorical notion of ordinal can be used to define transfinite iterates of
a functor (for example, internally in a topos).   I hope to use this to
develop categorical notions of the Axiom of Replacement.

Paul Taylor

process algebras

[matthieu amiguet]

Dear categoricians,

Is there any formalization of process algebras in term of categories? I
would be interested in giving an computational, multi-process semantics
to certain graphs, and I thought it could be done in terms of a functor
to a process category (if this concept exists...)
Is there any literature about this?
Thank you for your help,

Matthieu Amiguet

Re: process algebras

[Lindsay Errington]

> Is there any formalization of process algebras in term of categories? I
> would be interested in giving an computational, multi-process semantics
> to certain graphs, and I thought it could be done in terms of a functor
> to a process category (if this concept exists...)
> Is there any literature about this?

I have a CTCS99 paper ``On the semantics of message passing processes'' at
http://theory.doc.ic.ac.uk/~le which may be relevant. As the title
suggests, it looks at categorical semantics for a CSP-like language with
assignment. It is related to the work mentioned by Robin and Dusko. Also,
the conclusions of my thesis discusses representing process networks as
diagrams in a category of processes. This might be related to your comment
above.

Lindsay