Re:Encoding pi calculus in Calculus of Structures

Hello,

I have a few comments and questions about Alwen's message. I started 
thinking about the problem he proposes and it looks like I'm arriving 
at his same conclusion. Perhaps it's not bad, for the people 
interested, to have a rather extensive account of this matter, so 
here it is. I hope something good can come out of this stuff, it 
looks like it's possible.

I should perhaps say about my point of view on proof theory and 
concurrency. Very simply: we know that in concurrency there is a 
duality sender/receiver; then, proof theory should help in the design 
of process algebras that fully exploit the duality.

Clearly, theorems like cut elimination and Craig's interpolation are 
sort of ultimate tests about the good design wrt duality. Deductive 
systems enjoying these properties are then amenable to extensive 
manipulation and enjoy combinatorial properties (especially in deep 
inference) that people exploit for practical purposes like 
verification.

So, I think that:

1) It's important to try to capture process algebras, like CCS and 
the pi-calculus, in a proof theoretic setting with cut elimination 
etc.

2) This does not mean that we have fully to respect the process 
algebras we want to capture: on the contrary, I'd expect proof theory 
to provide feedback for making them better.

3) The actual logic used for the capture is rather irrelevant, 
provided we get good combinatorial properties.

Point 3 is important, let me comment a bit about that. I've heard 
several times that `we better stick to very well-know logics', like 
classical logic and perhaps linear logic. I believe that this might 
be wrong, and the reason is that we don't have universally accepted 
and well-studied semantics of proofs for these and other formalisms, 
*with an obvious relevance to concurrency*.

In other words, what matters is understanding the combinatorics of 
proofs that closely correspond to computations, and this has nothing 
to do with the semantics of formulae, which usually is what drives 
the proponents of classical logic. Yes, we can express everything in 
classical logic, but what does this tell us? (This reminds me of the 
mantra of logic programming, where people are proud of `having a 
clear semantics' and then nobody uses it, because in fact it's no use)

Instead, there are now two broad research efforts about semantics of 
proofs (in whatever logics) and semantics of concurrent computation 
that could very well join forces in the near future. I'm thinking 
here, of course, to the use of algebraic topology methods; I think 
this is our future.

Sorry, this message is getting long. Please tell me what you think 
about the previous opinions, am I wrong? Anyway, let's get to the 
point of Alwen's message, which is about capturing scoping mechanisms 
in deductive systems.

Basically, I'd like to understand the problem better; please consider 
that I'm no expert at all. For the notation, I'm going to use that of 
Robin Milner's `Communicating and Mobile Systems: The Pi-calculus' 
(it's a very nice book which I recommend, especially to students).

I will also use some deep inference/CoS notation. Most of the 
background for this can be found in Paola Bruscoli's paper 
<http://iccl.tu-dresden.de/~paola/bvl/bvl.pdf>, where she makes the 
correspondence between a subset of CCS and CoS system BV.

We have to distinguish two scoping mechanisms, and I believe they 
should be dealt with separately, at least initially.


RESTRICTION
-----------

The *restriction*

    new a P

construct, intuitively, simply means that the name a is private in P, 
and so the action a cannot be observed from outside P. Examples:

    new a (a | -a | b) | a | -b   -->   new a b | a | -b   and
           -   --
    new a (a | -a | b) | a | -b   -->   new a (a | -a) | a
                    -        --

are valid transitions, both labeled by tau (se they also are 
reactions), and I underscored the relative redexes. A non-valid 
transition would be going

    from   new a (a | -a | b) | a | -b   to   new a (a | b) | -b ,

because the a external to the leftmost process in the | cannot see 
the -a, which is protected by new a.

This mechanism is common to CCS and the pi-calculus (it can also be 
denoted by the nu operator and by the /_ suffix).

How can we capture its behaviour? In deep inference, the fact that -> 
is a congruence is already taken care of by deep inference itself, so 
we basically just need a rule that states that names are private:

    S{P[a/b]}
    ---------- ,   b not free in S{ } .
    S{new a P}

This rule is not very much in the spirit of CoS, but this is not the 
biggest problem  (actually, if it worked it wouldn't be a problem at 
all).

The problem is answering the question: what is the dual of new? The 
natural thing that comes to mind is to consider new self-dual. After 
all, why not? Scoping should be just a matter of bookkeeping like 
contraction and weakening, and they do are self-dual!

However, if we take R = new a a, then we have that -R = new a -a. 
Clearly, [R,-R] should be provable, but this would mean that there is 
a transition

    from   new a a | new a -a   to   0 ,

which is of course impossible, because R and -R actually cannot 
communicate on any channel.

So, if new is not self-dual, what is the behaviour of its dual? An 
experiment could be the following:
a) consider new a kind of `universal' quantification;
b) introduce its dual, call it `wen';
c) take quantification as is done in Kai Bruennler's thesis 
<http://www.iam.unibe.ch/~kai/Papers/phd.pdf>, and remove every 
equation and every rule for quantifiers from system SKS, except for 
the core rule, which we need.

Then, we only have the rule

          S{new a[R,T]}
    u_ ------------------- ,
       S[new a R, wen a T]

which corresponds to a tau-transition (or, if you like, reaction)

    new a R | wen a T   -->   new a (R | T) .

This would solve the problem mentioned above, because new a a | wen a 
-a should be reducible to 0.

Does it make any sense in concurrency? It looks strange to me, it's 
sort of a way of tapping into private communication channels (by 
simply knowing their names), or, if you prefer, to dynamically update 
a certain network configuration, boh? An interesting property seems 
to be the following. Consider

    R = wen a R' ,
    T = new a T' ,
    U = new a U' ;

two reactions are possible:

    R | T | U   -->   new a (R' | T') | U   and
    R | T | U   -->   T | new a (R' | U') .

So, it looks like the wen construct allows a process (R) to be part 
of the `internal network' of any process whose private channel it 
knows the name, and then, once one of the processes is chosen (T or 
U), then R commits and cannot escape anymore. In this sense of 
choice, wen looks appropriate as an existential-like quantification. 
Maybe it does make some `mobility' sense after all... What do you 
think?

Anyway, one can go on with the experiment by adding u_ to system BV 
and then seeing whether cut elimination can work, presumably by 
building on my splitting proof (you find this stuff in my paper `A 
System of Interaction and Structure' 
<http://iccl.tu-dresden.de/~guglielm/p/SystIntStr.pdf>). It might be 
necessary to introduce new laws (equations, maybe) about new/wen, and 
this would give more information on the nature of the quantifier. It 
might be worthy to have a look at this, I don't know. If you do, 
please let me know, I'm very interested.


INPUT/OUTPUT
------------

This is a place where the pi-calculus seems to need improvement. In 
CCS, communication is perfectly symmetric:

    a | -a   -->   0 ,

and this of course corresponds to a nice rule in CoS:

         S{0}
    ai_ ------- .
        S[a,-a]

This is not the case with the pi-calculus (unless I'm not able to see 
it). Here, you have the constructs

    a(x)    (receive x along a)   and
    -a<x>   (send x along a) ;

in addition, a(x).P binds the name x in P, while this is not the case 
for -a<x>.P.

This is already an asymmetry, and then there's the reaction rule

    a(x).P | -a<y>.Q   -->   P[x/y] | Q .

Clearly, this reaction cannot be taken as a basis for a rule 
(contrary to the CCS case), rather, it should perhaps be the final 
outcome of several derivation steps. For example, something like (I 
guess this is exactly what Alwen was proposing in his last message):

                [P[x/y],Q]
    ai_ ---------------------------
        < [a_y,-a_y] ; [P[x/y],Q] >
     q_ ----------------------------
        [ <a_y;P[x/y]>  , <-a_y;Q> ]
      = ----------------------------
        [ <a_x;P>[x/y]  , <-a_y;Q> ]
     n_ ---------------------------- .
        [ wen x.<a_x;P> , <-a_y;Q> ]

Here, I make a number of hypotheses:

1) We use BV (or BVL, as in Paola's paper).

2) a(x).P is expressed as wen x.<a_x;P>.

3) -a<y>.Q is expressed as <-a_y;Q>.

4) a_x is to be intended as a normal unary predicate a(x), I don't 
use this notation because it conflicts with the rest.

5) Like any good existential quantification, wen is subject to the n_ rule:

       S{P[x/Q]}
    n_ ---------- ,
       S{wen x P}

where Q is any process (we have to be careful here, of course we are 
doing some sort of second order propositional logic).

We have to test negation, so take process a(x); its dual is then new 
x -a<x>. Is

    a(x) | new x -a<x>   -->   0

a valid reaction? YES, it is (unless I'm horribly mistaken)! By the 
way (if I'm not double-horribly mistaken), this should be the so 
called phenomenon of `scope extrusion' in the pi-calculus.

The dual of -a<y> is simply a_y, in BV notation, and it does not have 
a correspondence in the pi-calculus, but it could be naturally 
interpreted as an input prefix which doesn't bind y. We can of course 
use it for a synchronisation that carries no value, as in

    -a<y>.P | a<y>.Q   -->   P | Q ,

where I use a<y> for the non-binding version of a(y).

So, it looks like there is some room for maneuvering here, and I'd 
like to hear your opinions.

One more point. Clearly, after introducing n_, one should ask whether 
what the proof theory can do is still sound wrt the pi-calculus. In 
other words, don't we derive more than just what corresponds to the 
computation we want?

Clearly, n_ poses a problem, in that any process a(x).P can 
spontaneously decay into P[x/Q] for any Q. How should we interpret 
this fact? If we only go for computation that terminate in 0, then 
the answer should be straightforward (albeit perhaps technically 
challenging): Q can only instantiate x if later in the computation 
some communication is actually able to match Q.

This would be nothing really new, it entails coming up with a lazy 
version of BV + {u_,n_} which only applies n_ together with ai_, 
i.e., it ties instantiation with actual communication. One should 
then prove that the lazy system and the normal one are equivalent 
over provability.

By the way, this is exactly what happens between Paola's BVL and BV, 
where BVL is the lazy version of BV (wrt to inferring on sequential 
constructs). Proving the equivalence can be very challenging, and, as 
a matter of fact, it's still open whether BVL and BV are equivalent 
(Paola gets away with it by resorting to a further, harmless 
restriction, for which she can more easily get the correspondence).

So, if what I wrote above is not total crap, there should be actually 
the possibility of some exciting developments. So far, the problem 
with asymmetric communication in the pi-calculus looked very nasty to 
me, but perhaps this is just a matter of breaking it into smaller 
pieces (old story...).

By the way, I've updated the part related to language design in the 
current topics page <http://alessio.guglielmi.name/res/cos/crt.html>. 
Please react.

Ciao,

-Alessio