Process Declarations in Pica

Sorry for the slow pace of things around here lately; life interferes sometimes. I've mentioned my fathers illness before; things took a drastic change for the worse a week ago, which made things more than a little bit crazy. Of course, life wouldn't be life in things happened one at a time; so naturally, my asthma picked now to act up as well, so I've been coughing my lungs out. It's been a fun week, really.

Anyway, I've been wanting to look a bit more at Pica. I've been thinking about how a
named process definition looks, and what it does. The type part of a definition is
relatively straightforward: a process is defined by a set of externally visible channels; each channel is defined by a type. In a named definition, there are two types of channels to think about. One is a set of channels supplied to the process when it's created; the other is a set of channels created by the process, but which are 'exported': that is, made visible to other processes. The type of a process is a tuple of all of the channels which
the process exports the outside world.

Of course, there's always a hitch, right? Nothing is ever simple. One of the defining characteristics of the π-calculus is mobility: channels can be moved around. A process can send a channel to another process, and no longer retain any ability to use it; or it can receive a channel via a message from some other process, effectively adding an externally visible channel; and finally, it can create a new channel via "new", and then
send that channel via a message to another process, effectively adding a new externally visible channel.

For the purposes of declaring a process and its channels, we'll adopt the
following rules:

1. A process type declares a set of fundamental channels for the process. Identifiers for a processes fundamental channels are treated as being immutable variables
   associated with a process instance.
2. A process may have more channels associated with it than its fundamental
   channels - but those channels do not affect its static type.

The basic syntax of processes is the following pattern:

    proc Name[pchannels...] shows [echannels...] does
       process-body-stuff
    end

where:

• pchannels is a set of fundamental channels associated
  with the process, and which are supplied to the process as parameters when a process
  instance is created; and
• echannels is a set of fundamental channels associated with
  the process, and which are created by an implicit "new" when a process instance is
  created.

So, for example, let's bring back the old storage cell example from an earlier post.
We wrote that in π-calculus syntax as:

    NewCell[creator,initval]≡new(read,write).{Cell[read,write,initval]
                                              | !creator(read,write) }
    Cell[read,write,val]≡{!read(val).Cell[read,write,val]
                          + ?write(v).Cell[read,write,v]}

In Pica syntax, that would be:

    proc Cell[init:Val] shows [read:Val,write:Val] does
         !read(init).Cell[init]
      || ?write(v).Cell[v]
    end

It looks a lot simpler than the π-calculus version, but the differences are pretty much all syntactic sugar. One of the syntax tricks that I've used for the Pica version is creating a syntactic distinction between "invoking" a process definition, and instantiating a process. In the π-calculus version, we didn't have that distinction. The split between "NewCell" and "Cell" in the π-calculus version, and the existence of "read" and "write" as parameters of "Cell" are all artifacts of that - we needed to explicitly separate the process invocation that would create a new cell. For Pica, when we just refer to a process by name, we'll treat that as an in-place invocation of the named processes behavior in the current process. So recursively invoking "Cell" inside of "Cell" just continues "Cell", re-using its exported channels. So just invoking "Cell" won't create new copies of its fundamental exported channels. To really create a new process with new channels, you'd need to invoke it via "spawn Cell[v]".

Creating this distinction does, of course, introduce some trouble. Since new channels aren't created unless you do a spawn, what does the following mean?

    proc A[] shows [x:X,y:Y] does
          something.B[]
    end

    proc B[] shows [a:X,b:X] does
      something
    end

When "A" invokes the behavior of "B", what's the value of the "a" channel of B? Or the "b" channel of B? We need some more syntax to allow us to say how to assign name bindings
of fundamental channels when we invoke a processes behavior without spawning it. The easiest part of that is that we'll just say that if "A" invokes "B", and B has a fundamental channel which matches a fundamental channel of "A" in both name and type, the matches channels will be unified. For other channels, we'll steal some syntax from the reduction rules:

    proc A[] shows [x:X,y:Y] does
         something.B[][x/a,y/b]
    end

    proc B[] shows [a:X,b:X] does
      something
   end

So when we invoke a process as a behavior, if its channel names don't match, then we can add a second set of "[]"s which specify how to match the names.

One last thing for today. Suppose we have an instantiated process P, with visible channels [a:X,b:Y]. To reference process P's channel "a", you'd use the syntax "P::a".