Join calculus

The Join-calculus is a process calculus invented by Fournet and Gonthier, as an 'extended subset' of the asynchronous Pi-calculus, making the latter - offering a practically attractive basis for modelling concurrent and distributed systems such as joint input and a locality principle - more amenable to describe distributed systems.

(* In other words, as the Join-calculus is designed be suitable to smoothly describe practical concrrent and distributed systems than Pi-calculus, it is often regarded as a "high-level description language", with contrast to the asynchronous Pi-calculus as "machine language" for the systems.)

As syntactic characterization, the three operators for input, restriction and replication from the Pi-calculus are amalgamated into a single operator called "definition" in the Join calculus :

def u = P in Q 〓 (new u)(!u(v).P | Q) (1)

This compound operator and its extension to admit joint inputs leads to the pleasantly simple grammar of Join calculus:

P, Q ::= u | P|Q | def D in Q

D ::= u | w = P

where D represents the joint definition with u, w called the defined names and v, x called the received namess which are all accessible from within P. The construct def D in Q represents the amalgamated operator that limits the further scope of the defined names of D to Q (see also Equation 1).

This calculus design (i.e., the syntactic design with its formal semantics) renders a more practically attractive basis to describe concurrent and distributed systems. The motivation for Join calculus to depart from the main mobile calculus such as Pi-calculus are as follows.

First, the multiple input device of Join, which is the additional capability to describe the atomic joint reception of values from two different channels, looks more suitable than the single prefix of pi-calculus to smoothly model many orchestration patterns in concurrent and distributed systems. For example, consider the process that must wait for messages on both x and y or in either one of the two. This is coded in Join as " x | tok<> = P1 ∧ y | tok<> = P2 ∧ x | y | tok = P3 "

and by assuring there is a unique message "tok<>", whereas the pi-calculus expression "x(u).P1 +y(v).P2 +x(u).y(v).P3" used, e.g., in [23] is a less faithful encoding, because:

in the third sub-expression multiple inputs must be arbitrarily sequentialised, and
the third alternative can be selected even if a message arrives on x but none arrives on y, causing a deadlock.

Of course one can still use the more precise translation "x(u).(P1 + y(v).P3) + y(v).(x(u).P3 + P2) but it is immediately seen that combinatorial explosion would make the encoding unreadable when larger groups of actions and more complex patterns are considered.

Second, Join adheres to a locality principle ensuring that extruded names cannot be used in input by the process that received them (they can only output values on such ports). This feature is crucial for deploying distributed implementations [10,7] and it is not enforced in the full pi-calculus.

Third, but not last, in [9], Join has been envisaged as some kind of higher-order version of Petri nets, which is another main formalism for concurrent and distributed systems, other than other two framous modeling formalism for concurrency as process algebra and the Actor model.

(*) This article is mostly cited from the following technical papers

Bisimulations in the Join calculus, by Cedric Fournet a Cosimo Laneve
Translating Orc Features into Petri nets and the Join Calculus by Roberto Bruni1, Hern´an Melgratti2, and Emilio Tuosto3