Pi Calculus | Hacker News Reader

Pi Calculus

en.wikipedia.org

12 pointsimb7 comments

To give this some context and some application today:

The Pi Calculus is a form of Process Calculus which is a Mathematical tool for modelling concurrent systems. (One might argue that concurrency is still a hard problem in Computer Science - but I'll leave that to the reader):

http://en.wikipedia.org/wiki/Process_calculus

This led to Robin Milners work on the Calculus of Communicating Systems (CCS). (Milner was trying to invent an automated theorem prover - and invented ML (Haskell precursor) and CCS along the way). Milner rocks.

https://en.wikipedia.org/wiki/Calculus_of_Communicating_Syst...

CCS Lead to the PI Calculus (which is what is linked).

Communicating Sequential Processes (CSP) also came out of the Process Calculi. (Philip Wadler described CSP as the 'moral equivalent' of CCS).

http://en.wikipedia.org/wiki/Communicating_Sequential_Proces...

The great thing about CSP is that they're used in modern programming languages today to solve concurrency problems in async operations. We see this with the C# compiler and the Async primitive:

http://msdn.microsoft.com/en-au/vstudio/jj573641.aspx

What is even more interesting is that CSP is used in Clojure in core.async. core.async is a macro that writes a state machine around blocking macros. (Similar in function to the C# compiler primitive). The benefit for this for ClojureScript is that you can write concurrent blocking operations that run in a single threaded environment. All this is done not with compiler changes, but with a deep walking macro written by Rich Hickey and Timothy Baldridge.

http://www.slideshare.net/borgesleonardo/intro-to-clojures-c...

http://swannodette.github.io/2013/08/02/100000-processes/

So is the Pi Calculus interesting and relevant to today? Yes! (But you have to jump a few links to understand why.)

CSP ideas have been used in Erlang, Scala (and you say Clojure). But CSP is earlier the pi-calculus. So that's not a good argument for the value of the pi-calculus.

Compared to CCS and CSP, the pi-calculus allows for natural transmission of communication links (think object references in java RMI for instance), and it uses an elegant formalism to do so (scope extrusion). At least, I would say that pi-calculus ideas are useful to give a formal semantics to certains concurrent or distributed languages, which in turns open the door to program verification.

It has also been used for protocol verification.

Thanks - that's a helpful clarification. I agree there isn't a direct link - it's more like you have to "widen the lense" within a field of related ideas to get from pi-calculus to CSP.

It's a nice model of concurrency that had been extensively studied by researchers but (I believe) never really had much practical impact.

Basically, it's a very small programming or modeling language based on concurrent message passing with a simple formal semantics. Pretty much in the same way that the lambda calculus is a small language based on functions.

There's no mainstream programming language based on it, unlike the lambda calculus that inspired LISP, ML and so on...

Interestingly, many evolutionary biology-related papers use p-calculus for their models. It's a shame most of them are typical science papers (they're written to seem complex and deep instead of trying to give a clear explanation of the model).

That's true. I think what happens is that researchers sometimes believe they need enough material for their papers to be published. For instance, they prove mathematical properties of their models which obfuscate the message and aren't necessarily relevant.

Also the target audience are other specialists in the same narrow field.

I read the whole article and didn't understand anything.

Reply on news.ycombinator.com