Ok. So I’m still tweaking syntax, to try to find a way of writing π-calculus in a way that’s
\neasy for me to write in my editor, and for you to read in your browser. Here’s the latest version:<\/p>\n
Process1<\/sub><\/em>.Process2<\/sub><\/em><\/code>.<\/li>\n- Send expressions:
!channel(tuple).Process<\/em><\/code><\/li>\n- Receive expressions:
?channel(tuple).Process<\/em><\/code><\/li>\n- New channel expression
new(name,...) { Process<\/em> }<\/code><\/li>\n- Process duplication expression:
*(Process<\/em>)<\/code><\/li>\n- Parallel composition:
Process1<\/sub><\/em> | Process2<\/sub><\/em><\/code>.<\/li>\n- Choice composition:
Process1<\/sub><\/em> + Process2<\/sub><\/em><\/code>.<\/li>\n- Null process:
∅<\/code><\/li>\n<\/ol>\n So, in this syntax, the final version of the storage cell from yesterdays post
\nis:<\/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 Now, let’s try to use π-calculus to do something that actually involves real concurrency.<\/p>\n
<\/p>\n
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
\nstructure, 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.)<\/p>\n
\nSync[numProc,p]=new(s){!p(s).WaitFor[numProc,s].!p(done).∅ }\nWaitFor[numProc,s]=if(numProc=0) then\n?s(done).WaitFor[numProc-1,s].\n∅.\n<\/pre>\n 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:<\/p>\n
<ul<\/p>\n
- 0=(&lamba;i z.z)<\/li>\n
- 1=(λi z.i z)<\/li>\n
- 2=(λi z.i i z)<\/li>\n
- .. and so on.\n<\/ul>\n
The λ calculus equivalent is:<\/p>\n
\n- \t 0=
?in(p,i,z){!z(p).∅}<\/code><\/li>\n- 1=
?in(p,i,z){!i(p).!z(p).∅}<\/code><\/li>\n- 2=
?in(p,i,z){!i(p).!i(p).!z(p).∅}<\/code><\/li>\n- …<\/li>\n<\/ul>\n
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\tthen sends “p” to “i” N times, followed by sending p to “z” once to say that it’s done.<\/p>\n
Ok. So what’s an adder look like?<\/p>\n
What it should two is take two π-numbers X (which wound send X messages on i, and one on z),
\nand 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.<\/p>\n
\nAdder[x, y, i, z, p]=new(yin) { !x(p, i, yin).∅
\n| ?yin(q).!y(p,i,z) }
\n<\/code><\/p>\n “x” and “y” are the channel names for the two numbers being
\nadded. “i” is the “increment” value, and “z” is the zero value; and p is the value that the
\nmessages need to be sent to. So, what the adder does is first send the message to trigger “x”, but
\ninstead of using the real “z” we created a new channel and used it for z; and in parallel, we have
\na process waiting to receive the “z”-message, and then trigger “y”. That’s in.<\/p>\n
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”:<\/p>\n
(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.)<\/em><\/p>\n\nSub[x,y,i,z,p]= new(ix, iy, zx, zy) {\n!x(ix, zx, p) | !y(iy, zy)\n| ConsumeIsWhileY[ix, zx, iy, zy]\n}\nConsumeIsWhileY[ix, zx, iy, zy, x, z] =\n?iy(p).?ix(p).ConsumeIsWhileY[ix, zx, iy, zx, x, z]\n+ ?zy(p).PassXsWhileX[ix, zx, x, z]\nPassXsWhileX[ix, zx, x, z]\t=\n?ix(p).!x(p).PassXsWhileX[ix, zx, x, z]\n+ ?zx(p).!z(p).∅\n<\/pre>\n 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.<\/p>\n
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 π?<\/p>\n","protected":false},"excerpt":{"rendered":"
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 } […]<\/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-360","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-5O","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/360","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=360"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/360\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=360"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=360"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=360"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}