As a refresher for me, and to give some examples to help you guys understand it, I’m going to go through a couple of examples of interesting things you can build with π-calculus. We’ll start with a simple way of building mutable storage.<\/p>\n
<\/p>\n
Before getting started, I’m going to be annoying and change the syntax a bit. Typeset π-calculus uses a channel name by itself for “receive message on channel”, and the channel name with an overbar for “send message on channel”. In yesterdays post, I used the unmarked channel name for receive, and added a “*” prefix for send. Playing with that, I find it very hard to read. So I’m going to start using a prefix for all uses of channel names: “?” for receive, and “!” for send.<\/p>\n
First,we’ll try to build a storage cell. A storage cell is a process that can store a value; and it provides channels that you can use to either receive a copy of its current value, or send it a new value.<\/p>\n
Let’s start with a very naive attempt at a cell.<\/p>\n
\nCell[val]= (νread,write)( !read(val).Cell[val]\n+ ?write(v).Cell[v])\n<\/pre>\nWhat 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 (which means cell writes<\/em> to the channel that others might want to read from), followed by recursively invoking “Cell” on the same value; or it allows a client to update the value by writing a value to its “write” channel (in which case Cell reads<\/em> from the channel and then recursively invokes cell with the new value.)<\/p>\n
So this is a simple updatable storage cell. Almost.<\/p>\n
What’s wrong with it? A couple of things about the channel names:<\/p>\n
\n
- The (νread,write) creates two channels, local to the Cell process<\/em>. That
\nmeans that no one outside of the cell process can see them!<\/em> They’re initially scoped
\nto Cell, and there’s no method inside of Cell to send the channel name outside of its
\nname-scope. So it’s a storage cell, but no one can ever actually read it or write to it.<\/li>\n- The ν that creates the channel is inside<\/em> of the part that is invoked
\nrecursively. So each time that “Cell” is invoked, it creates new channel names<\/em>. <\/li>\n<\/ol>\nSo, how can we fix that? Let’s start by fixing the second problem, and make it always use the same names. We’ll split it into two different definitions: one which creates a new cell (and allocates its channel names), and one which takes the channels that it should use or read and write.<\/p>\n
\nNewCell[val]=(ν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>\nNow we’ve got a cell which creates its channels once, and then just keeps reusing the same channels. That’s a good start. Now, the remaining problem is that we don’t have any way to tell a client what the names o the channels are. To fix that, we’ll just add a parameter to
NewCell<\/code>, which is the name of a channel where we should send the names of the read and write channels.<\/p>\n\nNewCell[creator,initval]=(ν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>\nSo now, we’re in good shape. We can create a storage cell. When we create it, it gets one set of channel names for reading and writing, and it sends those back to whoever created the cell, so that they’ll be able to read from and write to it.<\/p>\n
How would we use it? Let’s just throw together a bit of code.<\/p>\n
\n(ν me)( NewCell[me,0]\n| ?me(r,w).!w(7).?r(x).!out(x) )\n<\/pre>\nThis creates a new cell; receives a message from the cell containing its read and write channels; then it sets the cell contents to 7; reads the cell contents into a variable “x”,
\nand sends the contents it just read to an output channel.<\/p>\n","protected":false},"excerpt":{"rendered":"As a refresher for me, and to give some examples to help you guys understand it, I’m going to go through a couple of examples of interesting things you can build with π-calculus. We’ll start with a simple way of building mutable storage.<\/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-357","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-5L","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/357","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=357"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/357\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=357"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=357"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=357"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}