I feel like a bit of a change of pace, and trying a bit of an experiment.<\/p>\n
Re-reading Backus’s old FP work reminds me of what I was doing the last time I read it, which
\nwas back in grad school. At the time, I was working on some stuff involving parallel computation,
\nand I discovered Robin Milner’s π-calculus as a tool for describing parallel computation. You
\ncan think of π-calculus as being a sort of parallel (pun intended) for the λ-calculus: in
\nsequential, single-threaded computation, λ-calculus can be a great tool for describing what
\nthings mean. But λ-calculus has absolutely no way of describing the concept of multiple
\nthings happening at once. π-calculus is fundamentally built on the concept of multiple threads
\nwhich can only share information by passing messages.<\/p>\n
There’s a reason that reading Backus made me think of this, beyond just the temporal coincendence of the fact that I was working with π-calculus the last time I read Backus’s So my experiment, such as it is, is to see if I can work through how to create an actual, useful, non-pathological programming language based on the π-calculus; and not just do that, <\/p>\n The obvious starting place is with a quick overview of what π-calculus is. Today, I’llgive you a quick overview of it; and then in another post, I’ll dive into a bit of semantics – but only as much semantics as is really relevant to building a language out of it.<\/p>\n π-calculus is really remarkably simple. The idea is that you describe a set of Computations in π-calculus is described in terms of a fundamental reduction rule, →, which is read “reduces in one step” (think of → as the π-calculus version of β-reduction): “ To clarify the what this means in the context of the other constructs, we also usually say the following, although strictly speaking, they should be derivable from the syntax and the basic reduction rule:<\/p>\n Suppose that “out” is a communication channel that prints to a standard output. Then We can walk through a quick reduction of that:<\/p>\n I feel like a bit of a change of pace, and trying a bit of an experiment. Re-reading Backus’s old FP work reminds me of what I was doing the last time I read it, which was back in grad school. At the time, I was working on some stuff involving parallel computation, and I […]<\/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":[33,54],"tags":[],"class_list":["post-355","post","type-post","status-publish","format-standard","hentry","category-logic","category-programming"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-5J","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/355","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=355"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/355\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=355"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=355"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=355"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nFP paper. One of the major points that Backus made was how poorly the vonNeumann model was
\nat describing many computations; that has become far<\/em> more true in recent years. Even my laptop now has multiple processors; computation just isn’t single-threaded anymore. But most programming languages are basically deeply single-threaded. Even Haskell, for all of its functional
\npurity, isn’t particularly good at multi-threaded execution. But I’ve always thought it would be
\na great idea to build a language around π-calculus the way that ML is built around λ-calculus.<\/p>\n
\nbut do it publicly, here on the blog.<\/p>\n
\nprocesses<\/em> using the syntax of the calculus, and then there are a set of reduction rules
\nthat describe how the computation actually executes. Syntactically, there are really only six
\nconstructs in λ-calculus; and some of those can be viewed as “compounds”. The basic
\nconstructs are:<\/p>\n\n
P|Q<\/code>” is a process which runs “P” and “Q” in parallel.<\/li>\n
\nwhich will be non-deterministically transformed into either “P” or “Q”, but not both.<\/li>\n
\n“x” is an identifier, then then “c(x).P<\/code>” waits for a message to be received
\non channel “c”, binds the contents of that message to the identifier “x”,
\nand then becomes process P. This is very much like the π-calculus version of
\na λabstraction.<\/li>\n*c(x).P<\/code>” sends the value “x” as a message on channel “c” and then proceeds with process “P”. (In standard π-calculus syntax, this would be written a c with an overbar, but that’s very awkward in HTML, so I’m using “*” as an alternative.) <\/li>\n!P<\/code>” is a process consisting of an arbitrary
\nnumber of copies of P. “!P<\/code>” is syntactically equivalent to “P|!P<\/code>“. You can think of “!P” as being something like an HTTP service: no matter
\nhow many times you send an HTTP request to a server, there’s always an HTTP listener waiting
\nto receive your request.<\/li>\n
\nthen “(νx)P” creates a new communication channel bound to the identifier “x”, and
\nthen proceeds with process P (where the new identifier is in scope.)<\/li>\n
\nused to describe process termination: when a process P become 0, it halts.<\/li>\n<\/ol>\n*x(z).P | x(y).Q→P|(Q[z\/y])<\/code>“, where Q[z\/y] means “Q with z replacing y”. <\/p>\n\n
\nthe following is a little “program” in π-calculus which prints hello world.<\/p>\n\n(νin)( (!(in(x).*out(x).0))\n| (*in(hello).*in(world).0) )\n<\/pre>\n
\n(νin)( (!(in(x).*out(x).0))\n| (*in(hello).*in(world).0) )\n= (νin)( (in(x).*out(x).0|!(in(x).*out(x).0))\n| (*in(hello).*in(world).0) ) [! expansion]<\/em>\n→ (νin)( *out(hello).0|!(in(x).*out(x).0))\n| (*in(world).0) ) [one → step on channel \"in\"]<\/em>\n→ (νin)( !(in(x).*out(x).0))\n| (*in(world).0) ) [one → step with the \"invisible\" standard out process step]<\/em>\n= (νin)( (in(x).*out(x).0|!(in(x).*out(x).0))\n| (*in(world).0) ) [Another \"!\" expansion]<\/em>\n→ (νin)( *out(world).0|!(in(x).*out(x).0))\n| (0) ) [→ on \"in\"]<\/em>\n→ (νin)(!(in(x).*out(x).0)) [→ with standard out process on \"out\".]<\/em>\n<\/pre>\n","protected":false},"excerpt":{"rendered":"