{"id":389,"date":"2007-04-18T08:00:00","date_gmt":"2007-04-18T08:00:00","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2007\/04\/18\/numbers-using-processes-and-messages-part-1-addition\/"},"modified":"2007-04-18T08:00:00","modified_gmt":"2007-04-18T08:00:00","slug":"numbers-using-processes-and-messages-part-1-addition","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2007\/04\/18\/numbers-using-processes-and-messages-part-1-addition\/","title":{"rendered":"Numbers Using Processes and Messages: Part 1, Addition"},"content":{"rendered":"<p> Given a calculus, one of the things that <em>I<\/em> always want to see is how it can do<br \/>\nsome kind of meaningful computation. The easiest way to do that is to start building numbers and basic arithmetic.<\/p>\n<p><!--more--><\/p>\n<p> To be able to do this, we&#8217;re going to need one more bit of<br \/>\nsyntax. What we want to do is specify a condition. There is, of course, a way to do<br \/>\nthat in &pi;-calculus, but I don&#8217;t want to go into detail about how to do that yet. So what I&#8217;m going to do is allow, is a message receive operation, to specify a specific value<br \/>\nfor the received message; and say that in the reduction rules, a message send will match with a message receive if <em>either<\/em> the receive uses an unbound variable name,<br \/>\n<em>or<\/em> the receive specifies a concrete value which is identical to the value in the send:<\/p>\n<ul>\n<li><b>Syntax:<\/b> Our concrete receive will just place the value in quotes: <code>?in(\"v\")<\/code>.<\/li>\n<li><b>Reduction rule:<\/b> <code>?a(\"x\").P|!a(y).Q &rarr; P|Q<\/code> if &#8220;x&#8221;==y.<\/li>\n<\/ul>\n<p> The way that we do numbers in &pi;-calculus is based on the way that we do numbers in &lambda;-calculus. So we&#8217;ll start by reviewing the basics of how we do numbers in &lambda;-calculus: it&#8217;s called <em>church numerals<\/em>. <\/p>\n<p> Church numerals represent numbers are functions with two parameters, &#8220;s&#8221; and &#8220;z&#8221;. A number N is a function which applies its &#8220;s&#8221; parameter to its &#8220;z&#8221; parameter N times &#8211; you can think of it as N copies of &#8220;s&#8221; followed by one copy of &#8220;z&#8221;.  So:<\/p>\n<ul>\n<li> 0 &equiv; <code>&lambda;s z. z<\/code><\/li>\n<li> 1 &equiv; <code>&lambda;s z. s z<\/code><\/li>\n<li> 2 &equiv; <code>&lambda;s z. s (s z)<\/code><\/li>\n<li> 3 &equiv; <code>&lambda;s z. s (s (s z))<\/code><\/li>\n<li>&#8230;<\/li>\n<\/ul>\n<p> So now, we want to translate that basic concept into &pi;-calculus. In &lambda;, the basic single-step operation is function application, and the basic values are all functions. In &pi;-calculus, the basic single-step operation is messaging, and the basic values are all communication channel names. So what we&#8217;ll do is translate church numerals into processes. A number N will be a process which <em>sends<\/em> N &#8220;s&#8221; messages, followed by one &#8220;z&#8221; message. We need to add one extra parameter in &pi;-calculus: the place to send the message <em>to<\/em><\/p>\n<ul>\n<li> 0 &equiv; <code>?in(t,s,z).!t(z).&empty;<\/code><\/li>\n<li> 1 &equiv; <code>?in(t,s,z).!t(s).!t(z).&empty;<\/code><\/li>\n<li> 2 &equiv; <code>?in(t,s,z).!t(s).!t(s).!t(z).&empty;<\/code><\/li>\n<li> 3 &equiv; <code>?in(t,s,z).!t(s).!t(s).!t(s).!t(z).&empty;<\/code><\/li>\n<li> &#8230; <\/li>\n<\/ul>\n<p> Now, suppose we want to write an adder. An adder will be a process which takes an input message containing the &#8220;in&#8221; ports of two numbers X and Y, and then behaves the same as<br \/>\nthe process &#8220;X + Y&#8221;.<\/p>\n<p> The first part is easy: it needs to receive a message containing the in ports of &#8220;X&#8221; and &#8220;Y&#8221;:<\/p>\n<pre>\nAdder&equiv;?in(x,y).<em>???<\/em>\n<\/pre>\n<p> After it gets X and Y, it should <em>look<\/em> exactly like a number process. Each number process starts by receiving a message on its input channel, which contains a tuple of three values: t, s, and z.<\/p>\n<pre>\nAdder&equiv;?in(x,y).?in(t,s,z).<em>???<\/em>\n<\/pre>\n<p> Once it&#8217;s got its channels, the sum process should send (X+Y) &#8220;s&#8221;s, followed by one &#8220;z&#8221; to &#8220;t&#8221;. The way that we&#8217;ll make it to that is to use three parts:<\/p>\n<ol>\n<li> First, we need to invoke X (that is, send its &#8220;(t,s,z)&#8221; message to its input channel). But we can&#8217;t just have it send its &#8220;s&#8221; and &#8220;z&#8221; messages to &#8220;t&#8221; &#8211; because then, it would send &#8220;z&#8221; after only X &#8220;s&#8221;s. So we create a new port, &#8220;xt&#8221;, and invoke x, using the new &#8220;xt&#8221; in place of t.<\/li>\n<li> Next, we add a replicated process in parallel, which takes any &#8220;s&#8221; messages sent to &#8220;xt&#8221;,<br \/>\nand forwards them to &#8220;t&#8221;. So now, the two processes together give us a process<br \/>\nwhich sends X &#8220;s&#8221; messages to &#8220;t&#8221;. But after X &#8220;s&#8221; messages have been sent,<br \/>\nand &#8220;X&#8221; sends its &#8220;z&#8221;, that won&#8217;t get forwarded: the replicated process will<br \/>\nonly forward &#8220;s&#8221;s.<\/li>\n<li> Finally, we add a process in parallel with the other two which receives a &#8220;z&#8221; message from &#8220;xt&#8221;. When it<br \/>\ndoes, it invokes Y, using &#8220;(t,s,z)&#8221;. So now, the three processes together<br \/>\nwill send X &#8220;s&#8221;s to &#8220;t&#8221;; then the &#8220;z&#8221; on &#8220;xt&#8221; will cause Y &#8220;s&#8221;s to be sent to &#8220;t&#8221;, followed by one &#8220;z&#8221;. So it sends X+Y &#8220;s&#8221;s, followed by 1 &#8220;z&#8221; &#8211; which is exactly the behavior of a the process for the number &#8220;X+Y&#8221;.<\/li>\n<\/ol>\n<p> So, our completed adder is:<\/p>\n<pre>\nAdder&equiv;?in(x,y).?in(t,s,z).new(xt).{!x(xt,s,z).&empty;\n| *(?xt(\"s\").!t(s).&empty;)\n| ?xt(\"z\").!y(t,s,z).&empty; }\n<\/pre>\n<p> An exercise for interested people: try writing multiplication. Since multiplication<br \/>\nis just repeated addition, it shouldn&#8217;t be too hard &#8211; it&#8217;s just re-applying the<br \/>\nsame tricks I just showed for addition.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Given a calculus, one of the things that I always want to see is how it can do some kind of meaningful computation. The easiest way to do that is to start building numbers and basic arithmetic.<\/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-389","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-6h","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/389","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=389"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/389\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=389"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=389"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=389"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}