{"id":385,"date":"2007-04-16T08:05:00","date_gmt":"2007-04-16T08:05:00","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2007\/04\/16\/back-to-calculus-a-better-introduction\/"},"modified":"2007-04-16T08:05:00","modified_gmt":"2007-04-16T08:05:00","slug":"back-to-calculus-a-better-introduction","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2007\/04\/16\/back-to-calculus-a-better-introduction\/","title":{"rendered":"Back to &#960;-Calculus: a better introduction"},"content":{"rendered":"<p> Now that things are settling down a little bit, I wanted to get back to the stuff I was writing about &pi;-calculus. But looking back at what I&#8217;ve already written, I think I did a terrible job of introducing it. So I&#8217;m going to start over, and try to be more clear. <\/p>\n<p> I&#8217;ll start with a basic refresher of what &pi;-calculus is for, and a bit of history for where it came from.<\/p>\n<p><!--more--><\/p>\n<p> When computer networks first appeared and came into relatively widespread use, one of the problems that smart people recognized quite quickly is that communicating systems are fundamentally different from the kinds of computing systems that most of us are familiar with. The tools that we use to model conventional computing systems fail to capture many of the relevant properties of computation in a distributed world; and in fact, worse than just not capturing things, they often get things actively wrong.<\/p>\n<p> So &#8211; some people started looking at more useful and\/or realistic ways of describing<br \/>\ncommunicating systems &#8211; things called <em>process calculi<\/em>. The first major process calculus that I know of that&#8217;s still used today is CSP (Communicating Sequential Processes), first described in 1978 by C. A. R. Hoare. CSP became the basis of a<br \/>\nsystem called the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Transputer\">transputer<\/a>, and its programming language, <a href=\"http:\/\/www.wotug.org\/occam\/\">Occam<\/a>. <\/p>\n<p> Just two years later, in 1980, Robin Milner proposed something similar<br \/>\nto CSP called CCS &#8211; the calculus of communicating systems. The CCS had a stronger formal<br \/>\nbasis than CSP, and was somewhat more flexible in some ways. It was a very widely respected and widely used tool &#8211; in particular, it became the basis of a major tool for the formal description of network communication protocols, called <a href=\"http:\/\/wwwtios.cs.utwente.nl\/lotos\/\">LOTOS<\/a>. But it had one<br \/>\nmajor problem: it was limited to <em>static communication structures<\/em>. What that means<br \/>\nis that it described communication over a specific, static network of communication<br \/>\nchannels. Using the CCS, you could not add channels, remove channels, or rearrange the<br \/>\ninterconnections of communication channels in a system.<\/p>\n<p> The &pi;-calculus is an extension of the CCS that addresses that limitation, by<br \/>\nreplacing static communication channels with <em>channel names<\/em>. Instead of using a<br \/>\npredefined network of communication channels, the &pi;-calculus introduced the notion of a<br \/>\ndynamic system of named channels, and communication instructions in the &pi;-calculus work<br \/>\nin terms of channel <em>names<\/em>, not specific channels. Channel names can be created<br \/>\ndynamically, assigned to variables, and passed in messages. With the addition of channel<br \/>\nnames, &pi;-calculus could be used to describe many more kinds of communicating systems<br \/>\nmuch more easily than could be done in the systems that preceded it.<\/p>\n<p> So, finally, let&#8217;s get down to some syntax. There are only a small number of<br \/>\nbasic forms in &pi;-calculus. I&#8217;m not going to use Milner&#8217;s syntax &#8211; it&#8217;s too hard to write in HTML. But I&#8217;m going to try to be more consistent than last time around. A &pi;-calculus expression is called a <em>process<\/em>. Processes are written using the following forms:<\/p>\n<dl>\n<dt><b>Send Message:<\/b> <code>!<em>name<\/em>(<em>values<\/em>).<em>Process<\/em><\/code><\/dt>\n<dd> If there is a matching receiver waiting, send the values as a message on the channel named by the value of the <em>name<\/em>.<\/dd>\n<dt><b>Receive Message:<\/b> <code>?<em>name<\/em>(<em>values<\/em>).<em>Process<\/em><\/code><\/dt>\n<dd> If there is a matching sender, receive the values that it&#8217;s sending as a message on the channel named by the value of <em>name<\/em>.<\/dd>\n<dt>Create Name: <\/b> <code>new(<em>vars<\/em>).<em>Process<\/em><\/code><\/dt>\n<dd> Create a new channel set of channel name, and assign them to the variables. The variables names are <em>scoped<\/em> to the rest of the process definition. <\/dd>\n<dt><b>Parallel Composition: <\/b><code><em>Process<sub>1<\/sub><\/em> | <em>Process<sub>2<\/sub><\/em><\/code><\/dt>\n<dd>Run both <em>Process<sub>1<\/sub><\/em> and <em>Process<sub>2<\/sub><\/em> at the same<br \/>\ntime.<\/dd>\n<dt> <b>Choice Composition:<\/b><code><em>Process<sub>1<\/sub><\/em> + <em>Process<sub>2<\/sub><\/em><\/code><\/dt>\n<dd>Non-deterministically choose to run <em>either<\/em> <em>Process<sub>1<\/sub><\/em> or <em>Process<sub>2<\/sub><\/em>. <\/dd>\n<dt> <b>Replication:<\/b> <code>*(<em>Process<\/em>)<\/code><\/dt>\n<dd>Spawn as many copies of a process as necessary. &#8220;<code>*(P)<\/code>&#8221; is equivalent to &#8220;<code>P | *(P)<\/code>&#8220;. <\/dd>\n<dt> <b>Null<\/b>: <code>&empty;<\/code><\/dt>\n<dd> An empty process. The null process is mainly used to express process termination.<\/dd>\n<\/dl>\n<p> In addition to those basic structures, I&#8217;ll also use &#8220;{}&#8221;s for grouping.<\/p>\n<p> As usual for a calculus, we also need to look at <em>reduction rules<\/em>, the rules by which steps in a &pi;-calculus process get evaluated. In &pi;-calculus, reduction is written using &rarr;: &#8220;A&#8221; is reducible to &#8220;B&#8221; in one step is written &#8220;A &rarr; B&#8221;. The reduction rules are:<\/p>\n<ul>\n<li> <b>The Fundamental Rule:<\/b> <code>( !x(z).P | ?x(y).Q ) &rarr; P|(Q[z\/y])<\/code>. This rule basically says that given a matching pair of message send and message receive in parallel processes, both the send and the receive can be executed in one step, and the values in the message replace the parameters named in the receiver. (Q[z\/y] means &#8220;The process Q with every reference to name &#8220;z&#8221; replaced with a reference to name &#8220;y&#8221;.)<\/li>\n<li> <b>The Choice Rule:<\/b> If <code>P&rarr;Q<\/code>, then <code>(P+R)&rarr;Q<\/code>. This one is a little bit tricky. What it says is: if you have a choice between either process P or process R, and there is a one-step reduction of P to Q, then you can choose P, and do that reduction.<\/li>\n<li> <b>The Parallelism Rule:<\/b> If <code>P&rarr;Q<\/code>, then <code>(P|R)&rarr;(Q|R)<\/code>. All this says is that if there&#8217;s two processes running in<br \/>\nparallel, you can do a one-step reduction of one of the parallel processes without<br \/>\naffecting the other.<\/li>\n<li> <b>The Replication Rule<\/b>: If <code>P&rarr;Q<\/code>, then <code>*(P)&rarr;Q|*(P)<\/code>. This is just a restatement of what I said earlier about the<br \/>\nmeaning of replication.<\/li>\n<li> <b>Name Binding Rule<\/b>: If <code>P&rarr;Q<\/code>, then <code>new(x).P&rarr;new(x).Q<\/code>. This just says that introducing a new name around<br \/>\na process doesn&#8217;t change the reduceability of the processes inside of it.<\/li>\n<\/ul>\n<p> For today, we&#8217;ll just do one simple example. Suppose that we&#8217;ve got a communication channel named &#8220;out&#8221;, and any message received by &#8220;out&#8221; is printed to the standard output. Then we can write a hello world process:<\/p>\n<pre>\nnew(in).( *(?in(x).!out(x).&empty;)\n| !in(hello).!in(world).&empty; )\n<\/pre>\n<p> There are two processes composed in parallel. One is a replicated process &#8211; so there are conceptually an infinite number of copies of this instantiated. Each instantiated copy receives one message on the channel named &#8220;in&#8221;, and then sends it to out. The other process in here sends two messages to &#8220;in&#8221;: &#8220;hello&#8221;, and &#8220;world&#8221;.<\/p>\n<p> Here&#8217;s an exercise for interested readers. What&#8217;s wrong with this process?<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Now that things are settling down a little bit, I wanted to get back to the stuff I was writing about &pi;-calculus. But looking back at what I&#8217;ve already written, I think I did a terrible job of introducing it. So I&#8217;m going to start over, and try to be more clear. I&#8217;ll start with [&hellip;]<\/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-385","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-6d","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/385","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=385"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/385\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=385"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=385"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=385"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}