---

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 x₁, ..., x_n. 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 {l_i = x_i}^{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.

---