Ok. So I’m still tweaking syntax, to try to find a way of writing π-calculus in a way that’s
easy for me to write in my editor, and for you to read in your browser. Here’s the latest version:
- Sequential Composition:
Process1.Process2. - Send expressions:
!channel(tuple).Process - Receive expressions:
?channel(tuple).Process - New channel expression
new(name,...) { Process } - Process duplication expression:
*(Process) - Parallel composition:
Process1 | Process2. - Choice composition:
Process1 + Process2. - Null process:
∅
So, in this syntax, the final version of the storage cell from yesterdays post
is:
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])
Now, let’s try to use π-calculus to do something that actually involves real concurrency.
One thing that comes up often is the need for some kind of synchronization. You create N different worker processes, and then you need to wait until all N of them are done, and then you can go continue. One little cheat that I’m going to use is tossing in an if/then control
structure, and I’m going to use integers. (There’s a way to do both of those in π-calculus, which I’ll get to later, but for now, let’s just take them as a given.)
Sync[numProc,p]=new(s){!p(s).WaitFor[numProc,s].!p(done).∅ }
WaitFor[numProc,s]=if(numProc=0) then
?s(done).WaitFor[numProc-1,s].
∅.
Ok. So, to make that work, we needed some numbers. How can do we numbers in π-calculus? We’re going to borrow the basic idea of Church numerals from λ calculus. Remember in lambda calculus, we do numbers using lambda expressions:
<ul
The λ calculus equivalent is:
- 0=
?in(p,i,z){!z(p).∅} - 1=
?in(p,i,z){!i(p).!z(p).∅} - 2=
?in(p,i,z){!i(p).!i(p).!z(p).∅} - …
A number N is a process that that takes two channel names “i” (for increment), and z (for zero), and one value called “p”. It then sends “p” to “i” N times, followed by sending p to “z” once to say that it’s done.
Ok. So what’s an adder look like?
What it should two is take two π-numbers X (which wound send X messages on i, and one on z),
and Y (which would send Y messages on i, and one on z), and produce a process which will X+Y messages on i, followed by only one on z.
Adder[x, y, i, z, p]=new(yin) { !x(p, i, yin).∅
| ?yin(q).!y(p,i,z) }
“x” and “y” are the channel names for the two numbers being
added. “i” is the “increment” value, and “z” is the zero value; and p is the value that the
messages need to be sent to. So, what the adder does is first send the message to trigger “x”, but
instead of using the real “z” we created a new channel and used it for z; and in parallel, we have
a process waiting to receive the “z”-message, and then trigger “y”. That’s in.
How about a subtracter? To keep things easy, we’ll assume that when we do “x-y”, that “x>=y”. So then, what we’ll want to do is “eat” the first “y” p’s send by “x”:
(The following was originally very screwed up, due to a stupid editing error. I write my posts in an editor called TextMate, and then paste them into MoveableType for posting. I pasted an incomplete copy to check the MT preview, then went back to Textmate, finished the post, and posted the version that was in MT… Stupid, stupid, stupid! Sorry about that! In addition, there were some inconsistencies in the use of “[]”s versus “()”s, as pointed out in the comments. That had nothing to do with editing errors, just with my own inconsistency. I think those have all been fixed.)
Sub[x,y,i,z,p]= new(ix, iy, zx, zy) {
!x(ix, zx, p) | !y(iy, zy)
| ConsumeIsWhileY[ix, zx, iy, zy]
}
ConsumeIsWhileY[ix, zx, iy, zy, x, z] =
?iy(p).?ix(p).ConsumeIsWhileY[ix, zx, iy, zx, x, z]
+ ?zy(p).PassXsWhileX[ix, zx, x, z]
PassXsWhileX[ix, zx, x, z] =
?ix(p).!x(p).PassXsWhileX[ix, zx, x, z]
+ ?zx(p).!z(p).∅
In any real programming, we’re obviously not going to use these π-church numerals. But it’s a useful exercise to understand how to write π-calculus processes for doing simple some simple controlled iteration.
Now, as an exercise, if you’re so inclines: the implementation of subtract is very similar to how you’d implement a less-than-or-equal comparison. What would less-than-or-equal look like in π?
I am five kinds of confused by this post. I admit that the pi-calculus (and lambda calculus) is still quite unintuitive to me, but I’m trying me best to wrap my head around it. That section, though, just doesn’t make a damn lick of sense to me. Please enlighten me, perhaps with an example of use. ^_^
First, the Sync/WaitFor construction. How does it know what processes to sync? Would you compose the Sync bit into the child processes you spawned? Into the parent process?
Second, the Adder. I understand how numerals work, but how does the !x(p,i,z) process know to act like a numeral? I suspect you may be doing this in a meta-language, but I’m not sure. Isn’t a numeral a process that reads off of the input channel to find its p, z, and i values?
Now that I’m looking at numerals some more, I think I understand how they should work, because as written they don’t seem to make much sense. You can’t start throwing around {} until you lay down a new operater to declare some new channel names.
As well, I’m still confused about your usage of () versus []. It seems like the ‘functions’ in the latter half of your post should be using [] to fence off their variable names.
I’m not trying to be a jerk, just trying to understand! >_
Xanthir:
The trick for the numerals is that they’re a lot like church numerals. If you remember Church numerals, they use two function-values to represent a number: a zero-functions, and an increment function; you do it that way because in λ-calculus, the only things that really exist are functions.
In π-calculus, there are two kinds of things: processes, and channel names. Channel names are really the only thing that can be treated as a value – they’re the only things that can be passed, compared, or manipulated by processes.
In Lambda calculus, we represent a number N by a function that invokes the increment function N times on the zero function. In π-calculus, we represent N by a process that sends a message N times to its “increment” channel, followed by once to its “zero” channel, to indicate that it’s finished.
And you’re right to be confused about “[]”s versus “()”s; I was inconsistent about them. I’ll go fix that.
Xanthir:
You have very good reason to be confused; I accidentally posted an incomplete version of the post. Hopefully, between my previous answer, correcting the inconsistency about “[]” versus “()”, and getting the proper complete post up, it will be clearer.
Xanthir:
Forgot one thing: the whole sync/wait for. It’s set up to
just wait for “N” pings. The idea is that the parent process would spawn off N sub-processes in parallel, and then waits for them to complete. Since the parent process provides the channel that will be used for the sync, there’s no way for anything except the subprocesses to have access to the channel name used for the synchronization – so it doesn’t need to know anything except the number of subprocesses. So it just listens on that unique channel for N pings, and when it gets them, it signals the parent process to continue.
You might want to add the pi-calculus tag to the first pi-calculus post.
Cheers!
Chris
WaitFor[numProc,s]=if(numProc=0) then ?s(done).WaitFor[numProc-1,s].∅.
Should that be numProc!=0? And is that trailing period intentional?
All right, so I understand the way numerals work. What I’m still a little confused about is how you’re using them, such as in Adder. Let me elaborate.
Adder[x, y, i, z, p]=new(yin) { !x(p, i, yin).∅ | ?yin(q).!y(p,i,z) }
1=?in(p,i,z){!i(p).!z(p).∅}
So, say that x is the name of the number. That would mean that, if x was 1, then the definition would actually be:
?x(p,i,z){!i(p).!z(p).0}
When Adder evaluates the !x(p,i,yin) process, that triggers the numeral that is waiting, with baited breath, for something to show up on its input channel.
How does this add arbitrary numbers, though? It seems like you have to predefine each number before it can be used, or else you’re just throwing values on a channel that won’t ever get read. Is it assumed that all numbers exist beforehand?
I think this is my fundamental confusion here. If I gloss over this, then the rest of the post makes sense.
First, I’d like to check my understanding of Sync. done is an external variable. Sync assumes that there is a process waiting with a ?p(s). That process then uses s in spawning numProc parallel processes which all issue a !s(done) when they are done.
If all the above is correct, would example program would use it like this:?
new(p){Sync[2, p] | ?p(s).(work_1(s) | work_2(s)).?p(done).∅)}
If all the above is correct, it would seem to me to make more sense to write Sync just like WaitFor (with jag’s correction):
Sync[numProc,s]=if(numProc!=0) then
?s(done).WaitFor[numProc-1,s].
∅.
Then the example program would look like:
new(s){work_1(s) | work_2(s) | Sync[2, s].∅}
Of course, there’s a good chance I’m completely backward on all this. I suppose the aboves is simpler, but has less encapsulation. I guess I’m curious about design decisions. I also think I’ve spotted some typos in Sub. Modifications are marked with an @.
Sub[x,y,i,z,p]= new(ix, iy, zx, zy) {
!x(ix, zx, p) | !y(iy, zy@)
| ConsumeIsWhileY[ix, zx, iy, zy@]
}
ConsumeIsWhileY[ix, zx, iy, zy, x, z@] =
?iy(p).?ix(p).ConsumeIsWhileY[ix, zx, iy, zx@, x, z@]
+ ?zy(p).PassXsWhileX[ix, zx, x, z@]
PassXsWhileX[ix, zx, x, z@] =
?ix(p).!x(p).PassXsWhileX[ix, zx, x, z]
+ ?zx(p).!z(p).∅
should be, I believe:
Sub[x,y,i,z,p]= new(ix, iy, zx, zy) {
!x(ix, zx, p) | !y(iy, zy, p)
| ConsumeIsWhileY[ix, zx, iy, zy, x, z, p]
}
ConsumeIsWhileY[ix, zx, iy, zy, x, z, p] =
?iy(p).?ix(p).ConsumeIsWhileY[ix, zx, iy, zy, x, z, p]
+ ?zy(p).PassXsWhileX[ix, zx, x, z, p]
PassXsWhileX[ix, zx, x, z, p] =
?ix(p).!x(p).PassXsWhileX[ix, zx, x, z]
+ ?zx(p).!z(p).∅
Interesting to read your posts on π-calculus, as I have been going through papers on Piccola which is based on πL-calculus. A difference being that arguments are passed as extensible records called “forms” instead of tuples.
I like the theoretical background but a bit of my engineering background tends to kick in. For λ-calculus a practical implementation would make use of number, boolean and string primitives. For π-calculus would an implement at a low level use co-routines and perhaps scale to threads, process and distributed workloads?
Translation into blog-English desired [JVP: I presume he means “category” even though writing “actegory” twice] for:
The logic of message passing
Authors: J. R. B. Cockett, Craig A. Pastro
Comments: 47 pages
Subj-class: Category Theory; Logic in Computer Science
http://arxiv.org/abs/math.CT/0703713
Message passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the term calculus borrows heavily from the (synchronous) pi-calculus. The cut elimination procedure for the system provides an operational semantics.
Just a dumb comments about symbol for send or receive, perhaps >>| or |>> might be more intuitive (at least for me :P).