A Cross-encodings to the join calculus

In the join calculus of [10], each definition binds one or several channel names that can be passed independently whereas, in the objective join calculus of Section 2, each definitions binds a single object. This difference is not very deep; we briefly present cross-encodings between these two variants. We recall a syntax for the join calculus:
 P ::= 0 | x(u) | P & P | defD in P D ::= M |> P | D or D M ::= x(u) | M & M

Join calculus processes can be encoded by introducing single-label forwarder objects and passing those object names instead of channel names. (The encoding given below works for non-recursive definitions in the join calculus; recursive definitions can easily be eliminated beforehand [9].)
 [[0]] = 0 [[x (u)]] = x.send (u) [[P1 & P2]] = [[P1]] & [[P2]] [[ defD in P]] = obj o = [[D]] in obj x1 = send (u1) |> o.m1 (u1) in ... obj xn = send (un) |> o.mn (un) in [[P]]
where we assume that D defines the channel names x1, ..., xn. Accordingly, we encode channel reaction rules and patterns as follows:
 [[D1 or D2]] = [[D1]] or [[D2]] [[M1 & M2]]- = [[M1]]- & [[M2]]- [[M |>P]] = [[M]]-|> [[P]] [[x (u)]]- = mx(u)

Conversely, one can encode objective join processes into a join calculus enriched with records. Join calculus values then consist of both names and records, written {li = xi}i Î I; we use   #  for record projection. The encoding substitutes explicit records of channels for defined objects.
 [[0]] = 0 [[x.l (u)]] = x   # l (u) [[P1 & P2]] = [[P1]] & [[P2]] [[ obj x = D \ init P1 in P2]] = ( def[[D]]x in [[P1 & P2]]) {x ¬ {l = xl, l Î dl(D)}}
 [[D1 or D2]]x = [[D1]]x or [[D2]]x [[M1 & M2]]x = [[M1]]x & [[M2]]x [[M |> P]]x = [[M]]x |> [[P]] [[l (u)]]x = xl(u)
The encoding above treats all methods as public; it can be refined to preserve the scope of private labels using two records of channels instead of a single one.