The n-Category Café

As it happened, I was reading up on concurrent computation and the pi-calculus myself, yesterday. I’ve had “The pi-calculus: A Theory of Mobile Processes” by Sangiorgi and Walker standing on my bookshelf for some years, but never started reading as seemed to require a deeper understanding of concurrent computation than I possesed. In fact, in the introduction they suggest “Communicating and Mobile Systems: the pi-Calculus” by Robin Milner as a good introduction into the field of concurrent computation and hope their book will form a good complement.

Sangiorgi and Walker also note that neither the pi-calculus, nor currently any other process calculus, forms a complete theory of mobile systems (like lambda-calculus is for sequential computation), but is only a stepping-stone on the road to a more fundamental theory.

They assume something basic underlies the various theories. It would be interesting to see if category theory could help in shedding some light on this currently unknown theory.

Since you’re familiar with some of Paul-André Melliès’s work, you might find his take on concurrency interesting. For example, a relatively recent paper with Samuel Mimram, “Asynchronous games: innocence without alternation”.

Hello John,

I think you should have a look at Milner’s most recent work, Bigraphs. Bigraphs are a generalization of Milner’s earlier work on CCS and the Pi-calculus, enriched with categorical ideas and a nice graphical formalism. Milner explicitly states that he hopes to investigate links with natural sciences, including physics.

A recent book offers a gentle introduction to the theory. An electronic version was previously available on Milner’s web-page ; copies could still be available somewhere on the internet (Google or e-mail me for more).

One way to understand Pi-calculus is to compare and contrast Pi-calculus composition with categorical composition.

Categories are about things (morphisms and their attached domain and codomain) and how to compose them. If we compose

   f : A -> B 

   g : B -> C

  
   (g o f) : A -> C

Pi-calculus is also about composition, this time of processes. A process is a thing with a finite number of connection points (like domain and codomain for morphisms, except that there can be any finite number of connection points, including 0). Let’s write P(x1, …, xn) for a process with n connection points x1, …, xn. Composing say

   P(abcx)

   
   Q(axyz)

   P|Q

This is also what happens when you connect your computer with Google’s by making a search query: the parallel composition of your machine with Google does not prevent others from also interacting with Google.

Of course sometimes we want to prevent further composition at some composition points. The Pi-calculus enables this by providing an explicit hiding operation (nu x): given P(abc), the process

   (nu a)P

So in some sense this aspect of Pi-calculus can be seen as decomposing the usual functional/categorical composition into two distinct parts: the pure connection aspect and the hiding aspect, both of which are given as one basic operation in category theory.

A paper that looks at this generalised form of composition in some detail is Elementary structures in process theory (1) by K. Honda.

This is not the full story of the Pi-calculus, because processes have dynamics, they evolve over time, and the connection structure can change over time.

I don’t recommend the Sangiorgi, Walker book as an introduction to the field. Good as it is, it’s too full of technical detail for an introduction.

Good, you’re getting into process algebras. That should increase the chances of my understanding them. I have had some contact with systems biology people in Kent, and I know there’s some interest there. We read an introduction by Luca Cardelli. Certainly an ambitious program.

Mind you, Samson Abramsky is looking to physics rather than biology for inspiration.

Neat. Another tantalizing subject I wish I understood.

This one, i.e. process calculus, seems particularly close to my heart because, from my very naive understanding, it seems similar in spirit to what I was trying to do with discrete calculus.

The intersecting theme I guess is physics as a process of computation.

Claude Shannon sharpened the notion of building reliably systems from unreliable components. I’ve been working for some time on the model theory of systems of intelligent agents (not a spacial model) who are all interconnected in that any “announcement” is a public announcement that all agents can hear. The problem is how can one prove theorems about the way that agents revise their belief sets as they determine that certain other agents are certain kinds of liars. First, I have formally proved some of Raymond Smullyan’s (verbal) examples of Knights and Knaves. More importantly, what if there are conspiracies of strategic liars? There is some dispute in the Logic and Philosophy literature as to what is the proper definition of “lying and deception.” I recommend: The Definition of Lying and Deception, James Edwin Mahon. As the Global Recession suggests, markets of “intelligent agents” behave differently if some agents are trying to defraud others. This is a process logic issue, but I’m not clear how Pi Calculus refines the approach. My coauthor and I have been pushing for about 7 years to extend Information Theory into Disinformation Theory.

A paper on encoding knots in the $\pi$-calculus – Knots as processes: a new kind of invariant, by L. G. Meredith and David F. Snyder.

We exhibit an encoding of knots into processes in the $\pi$-calculus such that knots are ambient isotopic if and only their encodings are weakly bisimilar.

Dear John,

One of the principal challenges of finding good categorical models of calculi like Milner’s π-calculus (and even to some extent the lambda calculus) is that the packaging of structure and function is quite different in these formalisms.

If you think about vector spaces, they just sit there. There’s all this algebraic structure, but nothing “going on”, so to speak, no dynamics until you add morphisms. All the dynamics are in the maps. In process calculi (and other similar systems) the dynamics are packaged *with* the algebraic structure.

Specifically, process calculi can be presented in terms of a triple (G,E,S) where G is a grammar that freely generates the terms (this is really just some combination of monads); E is a structural equivalence whacking down terms that are syntactically different but not essentially different (this is a lot like the relations part of a generators (like G) and relations presentation of an algebra); S is a set of reduction rules, i.e. the operational semantics of the calculus. The (G,E) pair is a lot like a standard presentation of some algebraic structure. The S is the odd bit. It packages up dynamics over G/E.

This new packaging has some really interesting consequences. On the one hand it provides some nice ways to reason compositionally about dynamics that modify structure – compare this to Panagaden’s questions about dynamic topologies. On the other it makes it really challenging – right at the beginning – to say what a morphism might be in a category of such widgets (G,E,S). Specifically, morphisms need to encapsulate an understanding of what is preserved under mapping. It’s difficult to say what of S is or ought to be preserved. Lack of clarity on this point has been part of the difficulty in constructing a convincing categorical view.

Another interesting point is that process calculi have been presented without a compositional theory of process calculi. A given calculus presents a compositional account of concurrent behavior. No one really has a fully convincing account of how to compose (and hence decompose) process calculi as widgets themselves. Milner’s bi-graphs were an attempt to provide a basis for this. But, it’s hard to say how successful this proposal is without a decent competitor against which to evaluate it.

It turns out that this is really a practical matter. When i was at a certain large software company in the pacific northwest we built a π-calculus “chip” on an FPGA. We got interested in tiling the chip across the FPGA. This lead to an an interesting observation/question: how would we farm work out to the different chips? This lead to a proposed architecture in which we had a tree-like structure with ambient calculi at branches (because they are slightly better at farming out work than π-calculus) and π-calculi at leaves. Such an architecture begs the question of the global dynamics of such a composite “chip”. This would be more easily addressed by a compositional theory of calculi.

Best wishes,

–greg

Hello,

is there some kind of conclusion to this question yet, besides the option of using bigraphs?

Greetings,
Chris

Hi

I recently revised CCS and my understanding is that the transition tree of “a.P|a’.Q” agent is:

Tree(a.P|a’.Q) = ({a, Tree(P|a’.Q)},{aa’,Tree(P|Q)},{a’,Tree(a.P|Q)})

where aa’ (tau) is the internal action (agent a.P communicating with agent a’.Q)

I need to understand why the transition tree should not be the following:

Tree(a.P|a’.Q) = ({aa’,Tree(P|Q)})

I thought that when an agent execute the action a (send to channel a) it blocks until the action a’ (receive from channel a) is ready and inversely.

Kind regards
–Taoufik

I found the following article that has not been mentioned above Pi-Calculus in Logical Form by M. Bonsangue, and A Kurtz that ties this to coalgebras.

Abramsky's logical formulation of domain theory is extended
to encompass the domain theoretic model for picalculus
processes of Stark and of Fiore, Moggi and Sangiorgi.
This is done by defining a logical counterpart of
categorical constructions including dynamic name allocation
and name exponentiation, and showing that they are
dual to standard constructs in functor categories. We show
that initial algebras of functors defined in terms of these
constructs give rise to a logic that is sound, complete, and
characterises bisimilarity. The approach is modular, and
we apply it to derive a logical formulation of pi-calculus.
The resulting logic is a modal calculus with primitives for
input, free output and bound output.

I am only just learning about coalgebras and pi calculus, so I only just have a very superficial understanding of this….