As I did with my first attempt at explaining π-calculus, I think that before getting into any of the deep semantics, it’s good to look at a few examples of things you can build with π-calculus. But before getting to the meat of the post, I’ll give you the answer the puzzle I left in the last post. What’s wrong with the example I gave for “Hello world” yesterday?<\/p>\n
As a reminder, the question was: Assume “out” is the name for a channel that is read by a process that prints whatever it receives to the standard output. What’s wrong with the following process as an implementation of “Hello World”?<\/p>\n
\nnew(in).{ *(?in(x).!out(x).∅)\n| !in(hello).!in(world).∅ }\n<\/pre>\n<\/p>\n
As one commenter correctly answered, there is no guarantee that “hello” will be printed before “world”. Let’s first do the two reduction in the non-replicated subprocess. Then we’ll end up with:<\/p>\n
\nnew(in).{ !out(hello).∅ | !out(world).∅ | *(?in(x).∅) }\n<\/pre>\n Now, we can do a reduction with either<\/em> of the two processes trying to send to out. There’s no guarantee that “!out(hello)<\/code>” will get reduced before “!out(world)<\/code>“.<\/p>\n The correct way to do it is to explicitly synchronize things: don’t let the message “world” get sent, until after you know “hello” has been printed out:<\/p>\n
\nnew(in,sync).{ *(?in(x).!out(x).!sync().∅)\n| !in(hello).?sync().!in(world).?sync().∅ }\n<\/pre>\n
\n I’m going to use the syntax I introduced in the previous post, with
\none<\/em> addition: named process definitions.<\/p>\n A named process definition is really just a shorthand. A recursive named-process
\ndefinition is really just sugar for a replication expression; and a non-recursive one is
\nobviously just shorthand for a textual replacement of the process name with the process
\ndefinition assigned to it. Similarly, when a process definition takes parameters, there’s a
\ntranslation of that into messages. I’m not going to explain the expansion of recursive
\nprocess definitions or parameters in this post – but I will<\/em> come back to it in a
\nfuture post when we start getting into the detailed semantics. The way that I’ll write a
\nnamed process definition is “Name[params]≡Process<\/em><\/code>“; and for
\nclarity, I’ll always use names starting with an uppercase letter for processes, and names
\nstarting with a lowercase character for channel names and variables.<\/p>\n One very useful thing to have if we’re going to write real programs using π-calculus is mutable storage cells. In terms of π-calculus, a mutable storage cell is a process
\nwith two channels: one for reading the value of the cell, and one for writing a new value into the cell.<\/p>\n
To update the cell, a client will send<\/em> a message to the cell’s “write” channel containing the new value; to read the value of the cell, a client will receive<\/em> a message from channel’s “read” channel. Based on that description, here’s a process definition which would be most peoples first attempt at defining Cell:<\/p>\n\nCell[val]≡new(read,write).{?write(v).Cell[v]\n+!read(val).Cell[val]}\n<\/pre>\n What that says is: “Cell” is a shorthand for a process expression which is parametric in a value, called “val”. Cell introduces its own read and write channels, and then either allows a client to read the value in the cell, or update the value in the cell. There’s a bit of trickiness for people who aren’t used to process calculi: writing to replace the value inside the cell is done by reading<\/em> a message: ?write(v)<\/code> a client needs to send<\/em> a message containing a value to update the cell; and for clients to read the value from the cell, the cell has to write<\/em> to the read channel: !read(val) – sending a message to<\/em> the client containing the value in the cell. “read” and “write” are from the perspective of the client; they’re backwards from the perspective of the cell.<\/p>\n This cell implementation is close, but it isn’t correct, and the reason why illustrates some of the subtleties of π-calculus. What’s wrong with it? There are problems with channel naming – and channel naming and the subtleties of managing them are at the heart of how things work in π-calculus.<\/p>\n
\n- The “
new(read,write)<\/code>” creates two channels, scoped locally<\/em> to the Cell process. That means that no one outside of the cell process can see them! They’re initially scoped to Cell, and there’s no method inside of Cell to send the channel name outside of its name-scope. So it’s a storage cell, but no one can ever actually read it or write to it.<\/li>\n- The “new” that creates the channel is inside of the part that is invoked recursively. So each time that “Cell” is invoked, it creates new channel names. So even if some client had access to the channel names of the cell at some point in time, any time that the cell was read or written, it would allocate new names, and the client would no longer be able to access it.<\/li>\n<\/ol>\n
To fix it, we need to do two things. First, we need to change the cell definition so that it only allocates its read and write channel names once, and then reuses them. And second, we need to provide some way of making those channel names available to a client.<\/p>\n
To remove the allocation of the channel names from the recursive part of the process, we’ll split the process definition into two parts: one which will only be executed once, and one which executes recursively:<\/p>\n
\nNewCell[val]≡new(read,write)Cell[read,write,val]\nCell[read,write,val]≡{!read(val).Cell[read,write,val]\n+ ?write(v).Cell[read,write,v]}\n<\/pre>\n Fixing the other problem is also easy. We want to make the names of the
\ncell’s read and write channels available to a client. How do we do that in π-calculus? There’s only one way of moving values around in a π-calculus process: message passing. So when someone wants to create a cell, they’ll send a message to
\na cell factory process containing an initial value for the cell, and the name of
\na channel where the new cell’s read and write channel names should be sent:<\/p>\n
\nNewCell[creator,initval]≡new(read,write).{Cell[read,write,initval]\n| !creator(read,write) }\nCell[read,write,val]≡{!read(val).Cell[read,write,val]\n+ ?write(v).Cell[read,write,v]}\n<\/pre>\n To create and use a cell, the client process just invokes NewCell, passing it
\na message containing a channel name where it wants to receive the read and write channels of the cell:<\/p>\n
\nnew(self).{ NewCell[self,0]\n| ?(cellread,cellwrite).(...) }\n<\/pre>\n So, for example, we can write a process which allocates a cell, prints out its initial value, updates the cell value, and then prints out the new value like this:<\/p>\n
\nnew(self).{NewCell[self,0]\n| ?(cellread,cellwrite).?cellread(v).!out(v).!cellwrite(7).?cellread(w).!out(w)}\n<\/pre>\n","protected":false},"excerpt":{"rendered":"As I did with my first attempt at explaining π-calculus, I think that before getting into any of the deep semantics, it’s good to look at a few examples of things you can build with π-calculus. But before getting to the meat of the post, I’ll give you the answer the puzzle I left in […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[50],"tags":[],"class_list":["post-387","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-6f","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/387","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=387"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/387\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=387"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=387"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=387"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}