Message Boards

GROUPS:

Staff Picks Computer Science Graphics and Visualization Graphs and Networks Wolfram Language Wolfram High School Summer Camp

Rohan Mehta

[WSC21] Investigating the pi calculus and Petri nets

Rohan Mehta, Moravian Academy Upper School

Posted 6 months ago

1242 Views

1 Reply

6 Total Likes

Follow this post

enter image description here

Investigating the pi calculus and Petri nets
by Rohan Mehta

I first heard mention of the π -calculus a few years ago, and it really piqued my interest . After all, everyone’ s heard of the λ-calculus, but the π -calculus? For me, at least, it was completely new. Unfortunately, any information I could find about it online was basically impossible to understand, buried under so much math and notation that I soon gave up my search. However, when it came up as a potential project idea, I felt an itch to try and understand it again, this time armed with the powerful computational tools of the Wolfram Language. I wanted to create a visual and intuitive way to understand what it was really saying, and hopefully connect it to other forms of concurrent computation, like Petri Nets, on a visual (rather than mathematical) level. While my intuitions about how all of these ideas fit together are still somewhat in flux, I think I have discovered a rather compelling visual alternative to how these structures are traditionally understood .

π-calculus 101

The π-calculus is the slightly more esoteric (and yet, far more practical!) cousin to the well-known λ-calculus (which is itself rather aptly described as the more theoretically-inclined twin of the Turing Machine). However, instead of describing sequential computation (like the λ-calculus), the π-calculus specializes in concurrent computation. It can represent systems in which potentially infinitely many agents are communicating with one another along potentially infinitely many channels. In other words, everything from a client querying a server, to the innumerable interactions between the proteins in our cell's biological pathways, fall within its reach. And just like in the λ-calculus, all this expressive power comes from composing almost suspiciously simple (and, in hindsight, extremely obvious) operations together. In fact, the most basic π-calculus programs boil down to nothing more than three things:

◼

Names (the most obfuscating aspect of the π-calculus, names act simultaneously as communication channels and data; I like to think of them as addresses; they can refer to a physical place that data can be sent to, or a piece of information used to locate that place)

◼

Send commands (pretty self-explanatory, a Send command sends a name to another name)

◼

Receive commands (again, not too cryptic: a Receive command receives a name from another name)

A "Mild" π-Calculus Program


A "Medium" π-Calculus Program


A "Spicy" π-Calculus Program


Evaluating a π-calculus Program

Now that we've expressed the syntax we will be using, it's time to consider how we might evaluate a π-calculus program. It's actually surprisingly straightforward. The first thing to notice is that for most π-calculus programs, there won' t be a single, definitive order in which to evaluate all the processes that the program consists of. For example, if two proceses start off by sending some information along the same channel, then one has to go before the other, since a single channel can't accommodate two pieces of information at the same time . But while it would be equally valid to evaluate either of these processes first, choosing to evaluate one before the other might lead to a different eventual outcome .

But what if two processes don't interfere with one another? What if they send information along two separate channels, or replicate themselves? Then they can be executed concurrently. For our purposes, though, it won't be necessary to actually evaluate a given π-calculus program in parallel – we will get the same result even if we evaluate the program one process at a time . Obviously the whole point of π-calculus programs is that they are supposed to be executed in parallel, over a network of devices (not just on a single machine like we're doing now) . What we're doing here is somewhat more pedagogical, not exactly trying to build a useful program in the π-calculus, but instead considering how they work, how we might be able to better visualize and understand them, and, in a NKS-like spirit, trying to see whether even simple π-calculus programs are still capable of exhibiting complicated behavior.

Choosing a Process to Evaluate


Sending and Receiving


Updating the Program


Let's Evaluate Some π-calculus Programs!

Now can finally try our hand at evaluating a π-calculus program!

In[]:=

simplePrograms = {mildProgram, mediumProgram};

Reduce our terminating programs

reductionRule/@simplePrograms

Out[]=

{{{{PiSend[z,x],PiTerminate[]},{PiReceive[y,x],PiSend[x,y],PiReceive[y,x],PiTerminate[]},{PiReceive[v,z],PiSend[v,v],PiTerminate[]}},{{PiSend[x,z],PiReceive[z,x],PiTerminate[]},{PiReceive[v,z],PiSend[v,v],PiTerminate[]}},{{PiReceive[z,x],PiTerminate[]},{PiSend[x,x],PiTerminate[]}}},{{{{PiSend[x,b]}||{PiSend[x,e]},PiTerminate[]},{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiReceive[x,e],PiSend[x,f1],PiTerminate[]},{{PiReceive[x,f1]}||{PiReceive[x,f2]},PiSend[x,g],PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]},{PiReceive[x,g],PiSend[x,h2],PiTerminate[]},{{PiReceive[x,h1]}||{PiReceive[x,h2]},PiSend[x,i],PiTerminate[]}},{{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiSend[x,f1],PiTerminate[]},{{PiReceive[x,f1]}||{PiReceive[x,f2]},PiSend[x,g],PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]},{PiReceive[x,g],PiSend[x,h2],PiTerminate[]},{{PiReceive[x,h1]}||{PiReceive[x,h2]},PiSend[x,i],PiTerminate[]}},{{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiSend[x,g],PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]},{PiReceive[x,g],PiSend[x,h2],PiTerminate[]},{{PiReceive[x,h1]}||{PiReceive[x,h2]},PiSend[x,i],PiTerminate[]}},{{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]},{PiSend[x,h2],PiTerminate[]},{{PiReceive[x,h1]}||{PiReceive[x,h2]},PiSend[x,i],PiTerminate[]}},{{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]},{PiSend[x,i],PiTerminate[]}},{{PiReceive[x,b],PiSend[x,c],PiTerminate[]},{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]},{PiReceive[x,d],PiSend[x,h1],PiTerminate[]}}}}

Reduce our non-terminating program by 100 steps

In[]:=

reductionRule[spicyProgram, 100]

Out[]=

{{PiReplicate[{{PiSend[x,b]}||{PiSend[x,e]},PiTerminate[]}],PiReplicate[{PiReceive[x,b],PiSend[x,c],PiTerminate[]}],PiReplicate[{PiReceive[x,c],{PiSend[x,d]}||{PiSend[x,f2]},PiTerminate[]}],PiReplicate[{PiReceive[x,e],PiSend[x,f1],PiTerminate[]}],PiReplicate[{{PiReceive[x,f1]}||{PiReceive[x,f2]},PiSend[x,g],PiTerminate[]}],PiReplicate[{PiReceive[x,d],PiSend[x,h1],PiTerminate[]}],PiReplicate[{PiReceive[x,g],PiSend[x,h2],PiTerminate[]}],PiReplicate[{{PiReceive[x,h1]}||{PiReceive[x,h2]},PiSend[x,i],PiTerminate[]}]},

⋯99⋯

,{PiReplicate[{{PiSend[x,b]}||{PiSend[x,e]},PiTerminate[]}],

⋯32⋯

,{PiReceive[x,b],

⋯1⋯

}}}

large output

show less

show all

set size limit...

Converting to Canonical π-Calculus Syntax

Well....it looked like everything worked, but the result is pretty impossible to parse. There must be a better way to visualize what's really happening here. While the syntax we've chosen is very intuitive, it's also quite verbose, and pretty difficult to work with in large quantities. As such, it may be worthwhile to convert from our custom syntax to the more concise, canonical π-calculus syntax, so that we can visualize things a bit more succinctly.

To do this, we need to map the various elements of our syntax to their representations in the canonical π-calculus syntax. In other words, our versions of "Send", "Receive", "Choice", etc. need to get converted to their canonical counterparts. Thanks to the Wolfram Language's powerful pattern matching, this is actually pretty easy!

Convert custom π-calculus syntax to canonical syntax for a single process

processPrettyPrint[process_] := Module[{replicateConvert, orConvert, sendConvert,receiveConvert, converted}, replicateConvert = PiReplicate[{a__}] :> "!"<>"("<>processPrettyPrint[{a}]<>")"; orConvert = a__||b__ :> (processPrettyPrint[a]<>"+"<>processPrettyPrint[b]); sendConvert = PiSend[sent_, to_]:>(ToString@to<>"〈"<> ToString@sent <>"〉"); receiveConvert = PiReceive[received_, at_]:> (ToString@at<>"("<>ToString@received<>")"); converted = process /.{sendConvert, receiveConvert, orConvert,replicateConvert, PiTerminate[]->"0"}; If[converted[[0]]===List, StringRiffle[converted, "."], converted]]

Convert custom π-calculus syntax to canonical syntax for an entire program, and then style it

In[]:=

processesPrettyPrint[processes_, color_] := Framed[Column[ Style[Framed[processPrettyPrint[#]<>"|"],Background->color] &/@processes]]

In[]:=

lightColorList =

ListIcon

;

Now we can see what the output of our π-calculus interpreter looks like in the canonical π-calculus syntax! Note that what is shown here is either irreducible, or reduces to nothing. If the expression reduces to nothing, then technically it has not be fully evaluated. But if we did fully evaluate it, there would be nothing to visualize!

Display the fully-evaluated form of our first two programs in the canonical syntax

In[]:=

processesPrettyPrint[#[[-1]], RandomChoice@lightColorList]&/@reductionRule/@simplePrograms // Row[#, " "]&

Out[]=

x(z).0|

x〈x〉.0|

b(x).c〈x〉.0|

c(x).d〈x〉+f2〈x〉.0|

d(x).h1〈x〉.0|

Much better! We can do the same thing with our non-terminating program, too. Let's see what it looks like after five reductions!

Display the fully-evaluated form of our third, non-terminating program in the canonical syntax

In[]:=

processesPrettyPrint[#[[-1]], RandomChoice@lightColorList]&@reductionRule[spicyProgram, 5]

Out[]=

!(b〈x〉+e〈x〉.0)|

!(b(x).c〈x〉.0)|

!(c(x).d〈x〉+f2〈x〉.0)|

!(e(x).f1〈x〉.0)|

!(f1(x)+f2(x).g〈x〉.0)|

!(d(x).h1〈x〉.0)|

!(g(x).h2〈x〉.0)|

!(h1(x)+h2(x).i〈x〉.0)|

d(x).h1〈x〉.0|

f1(x)+f2(x).g〈x〉.0|

While our first two programs appear to have contracted in size, eventually reaching some smaller irreducible state, our third, non-terminating program, seems to have expanded in size. This is, obviously, due to the fact that it includes a replication operator (multiple of them, actually), while our simpler programs do not. We can even animate the evolution of our programs as they're being evaluated to see these two opposite trends in action.

Convert custom π-calculus syntax to canonical syntax after each reduction step

In[]:=

visualizeEvolution[processes_, stepCount_: 0] := Module[{randomColor}, randomColor=RandomChoice@lightColorList; (processesPrettyPrint[#, randomColor]&/@reductionRule[processes, stepCount])]

In[]:=

dynamicallyVisualizeEvolution[processes_, stepCount_: 0] := FoldList[Row[{#1,#2}," ⟶ "]&, visualizeEvolution[processes, stepCount]] // ListAnimate[#, Alignment  {Left,Center}]&

Visualize the contracting evolution of our first two program in the canonical syntax

In[]:=

dynamicallyVisualizeEvolution/@simplePrograms // Column

Out[]=

x〈z〉.0|

x(y).y〈x〉.x(y).0|

z(v).v〈v〉.0|

⟶

z〈x〉.x(z).0|

z(v).v〈v〉.0|

⟶

x(z).0|

x〈x〉.0|

b〈x〉+e〈x〉.0|

b(x).c〈x〉.0|

c(x).d〈x〉+f2〈x〉.0|

e(x).f1〈x〉.0|

f1(x)+f2(x).g〈x〉.0|

d(x).h1〈x〉.0|

g(x).h2〈x〉.0|

h1(x)+h2(x).i〈x〉.0|

Visualize the expanding evolution of our third, non-terminating program in the canonical syntax

dynamicallyVisualizeEvolution[spicyProgram, 4]

Out[]=

!(b〈x〉+e〈x〉.0)|

!(b(x).c〈x〉.0)|

!(c(x).d〈x〉+f2〈x〉.0)|

!(e(x).f1〈x〉.0)|

!(f1(x)+f2(x).g〈x〉.0)|

!(d(x).h1〈x〉.0)|

!(g(x).h2〈x〉.0)|

!(h1(x)+h2(x).i〈x〉.0)|

So this is what's really happening underneath the hood of our interpreter! But while these visualizations are definitely a step up from before, they're still missing a dimension to the reduction process. Each of these reductions implicitly carries with it a choice made by the interpreter – a choice to evaluate one process instead of the other. Therefore the outcome we're seeing here may not be the only possible outcome (that's the nondeterminism of the π-calculus in action)! How can we tell if there are multiple possible outcomes for a given π-calculus program, and if possible, visualize them all at once?

Visualizing the Multiway System of Reductions

Enter the idea of a Multiway System. We can express these systems as graphs, where each node in the graph represents our system's state, and each edge represents a possible transformation from the current state to a future state. Any path within this graph represents a possible way our system could evolve over time, although which one it chooses to take, is , ultimately, random. To generate such a graph we can't just evaluate our program for a single ordering of its constituent processes, but for every possible ordering of them!

Generate all possible evaluation outcomes for a given π-calculus program and turn them into the connections of a graph

In[]:=

allPossible[processes_] := updateStep[processes,#, True, True]&/@(activeProcesses@processes)

In[]:=

helper1[processes_] := ((allPossible/@#[[1]][[2]])&/@processes) // Flatten[#,2]&helper2[processes_] := (processes[[1]][[1]]->#)->Placed[processes[[2]][[1]],3/4]&/@processes[[1]][[2]]helper3[processes_] := helper2[#]&/@processes

generateConnections[processes_, stepCount_:-1] := If[stepCount==-1, (helper3/@NestWhileList[DeleteDuplicates@*helper1, allPossible@processes,#1!=#2&, 2]), (helper3/@NestList[DeleteDuplicates@*helper1, allPossible@processes,stepCount])] // Flatten[#,2]&

Graph these connections, and build up the Multiway System

In[]:=

graphMultiwaySystem[connections_, small_:True]:= Module[{newConnections}, newConnections = (# /. ((a_ -> b_) -> c_) :> ((Column@(processPrettyPrint/@(a)) -> Column@(processPrettyPrint/@(b))) -> c)&/@connections); Graph[((#[[1]])&/@(newConnections)) // DeleteDuplicates, VertexLabelsIf[small,Placed["Name",Tooltip],None],EdgeLabelsIf[small,newConnections,None],EdgeLabelStyleIf[small,Directive[Black,Bold,FontSizeScaled[0.0032],FontFamily"Courier",BackgroundRandomChoice[lightColorList]],None]]]

In[]:=

generateMultiwaySystem[processes_, stepCount_:-1, small_:True]:= processes//generateConnections[#,stepCount]&//graphMultiwaySystem[#,small]&

In[]:=

generateMultiwaySystem@mildProgram

Out[]=

Woah! Now we can finally see what's really going on. This diagram shows us that our first program is actually deterministic. It's Multiway System is just a linear chain. It can only ever evolve in one way. But what about our second program?

In[]:=

generateMultiwaySystem@mediumProgram

Out[]=

As we might expect, its a good deal more complicated! Its Multiway System has three distinct paths, each of which leads to a distinct end result (a distinct program state!). In particular, each split in the graph represents the existence of a Choice operation (although it's important to note that a π-calculus program can still be non-deterministic even without a Choice operator, for example, if there are multiple processes that start with a Send or Replicate command).

=Just as before, we can visualize how these graphs are built up over time with a little animation.

In[]:=

dynamicallyGenerateMultiwaySystem[processes_, stepCount_:0, small_:True]:= graphMultiwaySystem[#, small]&/@Table[generateConnections[processes, i], {i,0,stepCount}] // ListAnimate[#, Alignment  Center]&

In[]:=

dynamicallyGenerateMultiwaySystem[mediumProgram, 5, True]

Out[]=

How about our final program though? The one that includes Replication operators. What do you think it might look like? Well, let's try and animate the evolution of its Multiway Graph for three time-steps (remember, we can't render the full graph, because the program never terminates).

In[]:=

dynamicallyGenerateMultiwaySystem[spicyProgram, 3, False]

Out[]=

Wow! It almost looks like a snowflake. That's an interesting thing to note about π-calculus programs that have all their processes wrapped in Replication commands. They often tend to very closely mirror some symmetrical shape. That's because each process can always split out and Replicate itself. If this was the only thing they could do, then the graph would be perfectly symmetrical, but sometimes instead of replicating, our interpreter might choose to evaluate one of the processes, which introduces a few irregularities into their overall shape. We can also notice some other interesting motifs within these Multiway Graphs. For instance, consider the topology of the second stage graph of our program above. It contains a loop: a place where our π-calculus program can actually revert back to a previous state! What's happening here?

Well, if we turn on the labeling feature for our graph’s edges (the result is pretty ugly since everything is packed together so tightly, so I won’t show it here) we’ll see that the operation carrying the program state away is a replication operation, and the operation carrying it back to its initial state is an evaluation of the operation that was replicated (in this case, a Send). Since there are no receivers (all of them are still waiting to be replicated), evaluating the Send equates to doing nothing, and returns the program to its initial state. While they’re more difficult to pick out, we can notice these same motifs in the third- and fourth-stage graphs too!

"Mining the Computational Universe" of Simple π-calculus Programs

So we discovered some pretty cool structures in the Multiway Graphs of our three programs! But our sample size was severely limited. To try and get a better sense of the diversity of Multiway Graph topologies that π-calculus programs can generate, we can try and "mine the computational universe" of π-calculus programs by randomly generating programs within certain parameters.

Generating a Random π-calculus Expression


Experiments Without Replication

Let's start out simple, and just try to generate 2x2 π-calculus programs. For simplicity, we won't include any replication operators for right now. Using our syntax-conversion scheme, we can visualize the evolution of 10 random 2x2 programs in the canonical π-calculus syntax.

Visualize the evolution of 10 2x2 programs

In[]:=

randomlyVisualizeEvolution/@Table[randomlyGenerateProcesses[2,2], {n,10}]

Out[]=



b〈c〉.b(b).0|

c(a).b(c).0|

,

b〈a〉.c(c).0|

a〈c〉.c(c)+c(b).0|

b〈a〉.c(c).0|

c(c)+c(b).0|

c(c).0|

c(c)+c(b).0|

,

c〈a〉.a〈b〉.0|

c〈b〉+c(a).a(b).0|

a〈b〉.0|

a(b).0|

,

b〈c〉.a(c).0|

a(c).c〈c〉.0|

a(c).0|

a(c).c〈c〉.0|

,

b〈a〉.c〈a〉.0|

a(c).a(a).0|

c〈a〉.0|

a(c).a(a).0|

,

c〈c〉.b〈a〉.0|

c(b).a〈c〉.0|

b〈a〉.0|

a〈c〉.0|

,

c〈b〉.a(a)+b〈a〉.0|

b(b).c〈b〉.0|

a(a)+b〈a〉.0|

b(b).c〈b〉.0|

c〈a〉.0|

,

c〈a〉.b(c)+a(a).0|

a(a).b〈b〉.0|

b(c)+a(a).0|

a(a).b〈b〉.0|

,

a〈a〉.b〈c〉.0|

a(a)+b〈c〉.a(b)+b(b).0|

,

a〈c〉.c(a).0|

b(c).c(a).0|

c(a).0|

b(c).c(a).0|



Ok, so we have confirmed that we can indeed generate random π-calculus programs, and ones that have multiple evaluation steps! Let's see what the graphs of 50 2x2 π-calculus programs look like.

Generate 50 2x2 π-calculus programs and graph their Multiway Systems

makeExperiment[2,2,False,50]

Out[]=

There's a lot to take in here! First of all, there is a much richer variety of structure than in our three test programs. Some programs have Multiway Graphs that diverge at one point but later converge, while others exhibit some more exotic loops. One interesting thing to note is that most graphs have many more intermediate states than end states, and that its rare for (at least a 2x2) program to have more than three distinct end states. Here are some of my favorite Multiway Graphs for this class of programs:

Out[]=

Now we can do the same thing with 3x3 and 4x4 π-calculus programs!

makeExperiment[3,3,False,50]

Out[]=

makeExperiment[4,4,False,50]

Out[]=

Wow, some of those got very big very quickly – so big sometimes that their graphs can't even be rendered! One interesting phenomena we might notice is that we often see really simple graphs right next to complex ones. This is because we are generating programs at random, and so sometimes the ones we generate will be completely useless, like an agent sending out information with no one to receive it. In general though, we get some very sophisticated structures. Here are some of my favorites:

Out[]=

Experiments With Replication

We can also try to visualize 5 steps of non-terminating programs. These programs grow even more steeply, so we can only experiment with 2x2 and 3x3 programs.

Visualize the evolution of 10 2x2 programs (with replication)

In[]:=

randomlyVisualizeEvolution/@Table[randomlyGenerateProcesses[2,2,True],{n,3}]

Out[]=



c〈a〉.a〈b〉.0|

c(b).a〈c〉.0|

a〈b〉.0|

a〈c〉.0|

,

!(c〈c〉.a(c).0)|

!(b〈b〉.c〈c〉.0)|

[WSC21] Investigating the pi calculus and Petri nets

π-calculus 101

A "Mild" π-Calculus Program

A "Medium" π-Calculus Program

A "Spicy" π-Calculus Program

Evaluating a π-calculus Program

Choosing a Process to Evaluate

Sending and Receiving 

Updating the Program

Let's Evaluate Some π-calculus Programs!

Converting to Canonical π-Calculus Syntax

Visualizing the Multiway System of Reductions

"Mining the Computational Universe" of Simple π-calculus Programs

Generating a Random π-calculus Expression

Experiments Without Replication

Experiments With Replication

A "Mild" π-Calculus Program


A "Medium" π-Calculus Program


A "Spicy" π-Calculus Program


Choosing a Process to Evaluate


Sending and Receiving


Updating the Program


Generating a Random π-calculus Expression
