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.<\/p>\n
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.<\/p>\n
<\/p>\n
Of course, there’s always a hitch, right? Nothing is ever simple. One of the defining characteristics of the π-calculus is mobility<\/em>: 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.<\/p>\n For the purposes of declaring<\/em> a process and its channels, we’ll adopt the following rules:<\/p>\n The basic syntax of processes is the following pattern:<\/p>\n where:<\/p>\n So, for example, let’s bring back the old storage cell example from an earlier post. We wrote that in π-calculus syntax as:<\/p>\n In Pica syntax, that would be:<\/p>\n 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<\/em> 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<\/em> 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 “ 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?<\/p>\n 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:<\/p>\n 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.<\/p>\n 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”.<\/p>\n","protected":false},"excerpt":{"rendered":" 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 […]<\/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-417","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-6J","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/417","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=417"}],"version-history":[{"count":2,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/417\/revisions"}],"predecessor-version":[{"id":2991,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/417\/revisions\/2991"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=417"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=417"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=417"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n
\nchannels – but those channels do not affect its static<\/em> type.<\/li>\n<\/ol>\n\nproc<\/b> Name[pchannels...] shows<\/b> [echannels...] does<\/b>\nprocess-body-stuff end<\/b>\n<\/pre>\n
\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\nproc Cell[init:Val] shows [read:Val,write:Val] does\n !read(init).Cell[init]\n|| ?write(v).Cell[v]\nend\n<\/pre>\n
spawn Cell[v]<\/code>“.<\/p>\n\nproc A[] shows [x:X,y:Y] does\n something<\/em>.B[]\nend\n\nproc B[] shows [a:X,b:X] does\n something<\/em>\nend\n<\/pre>\n
\nproc A[] shows [x:X,y:Y] does\n something<\/em>.B[][x\/a,y\/b]\nend\n\nproc B[] shows [a:X,b:X] does\n something<\/em>\nend\n<\/pre>\n