Previous Up Next
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) |> (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.

Previous Up Next