We here rephrase the traditional presentation of the core
join-calculus , where names are
the only value. Thus, we ignore the issue of system primitives and
names provide sufficient expressive power for our purpose of
describing our implementation of pattern-matching (However we use
primitives and constants in our examples).
We slightly change the syntax of , in order to
match the one of
the join programming language.
We use x to denote a name in general.
x(xii ∈ 1… p)
P | P
x(xii ∈ 1… p)
J | J
A process P is either a message, a defining process, or a parallel
composition of processes (note that names are polyadic, meaning that
messages may be made of several values);
a definition D consists of one or several clauses J = P that
associate a guarded process P to a specific message pattern J;
a join-pattern J consists of one or several messages in parallel. We
say that the pattern J = … x(xii ∈ 1… p)…
defines the name x and that a definition defines the set of the names
defined by its patterns.
Moreover, patterns are linear, i.e. names may appear at most once in
a given pattern.
Processes and definitions are known modulo renaming of bound
variables, as substitution performs α-conversion to avoid
This semantics is specified as a reflexive chemical abstract machine
(RCHAM) (see ). The state of the computation
is a chemical soupD ⊩ P that consists of two
multisets: active definitions D and running processes P.
The chemical soup evolves according to two families of rules: Structural rules ↔ are reversible (→ is heating,
← is cooling); they represent the syntactical rearrangement of
terms (heating breaks terms into smaller ones, cooling builds larger
terms from their components). Reduction rules ⇒
consume specific processes present in the soup, replacing them by some
others; they are the basic computation steps.
We present simplified chemical rules
(see [4, 5] for
the complete set of rules).
Following the chemical tradition, every rule applies on any matching
sub-part of the soup, non-matching sub-parts of the soup being left
⊩ P1 | P2
⊩ P1, P2
⊩ ϕ (J)
⊩ ϕ (P)
Two of the rules above have side conditions:
the names defined in D must not appear anywhere
in solution but in the reacting process and definition D and P.
This condition is global; in combination with α-renaming it
enforces lexical scoping.
(R-β) ϕ (·) substitute actual names for
the received variables in J and P.
Additionally, we only consider well-typed terms and reductions.
See  for details on a rich polymorphic type system
for the join calculus. Here, this mostly amounts to assuming that
message and name arity always agree.
In this paper, we take particular interest in the reduction (R-β).
Informally, when there are messages pending on all the names defined
in a given join-pattern, then the process guarded by this join-pattern
may be fired. When firing is performed, we say that a matching occurs.
On the semantics level, there is a message (xii ∈ 1… p) pending
on a name x when there is an active molecule
x(xii ∈ 1… p) in the chemical soup.
Thus, we may define the reactivity status of a given chemical soup as
the multiset of the active molecules in it.
Later on in this paper, we shall consider various abstractions of this
Apart from primitives, join-languages support synchronous
names, which the core join-calculus does not provide directly.
Synchronous names send back results, a bit like functions.
However synchronous names may engage in any kind of
join-synchronization, just as asynchronous names do.
A program written using synchronous names can be translated
into the core join-calculus alone.
The translation is analogous to continuation passing style
transformation in the λ-calculus.
In our implementation, as far as pattern-matching is concerned,
a synchronous name
behave like it was asynchronous and carried one additional continuation
argument. All implementation difficulties concentrate in managing this extra
argument, whose presence had no effect on pattern-matching itself.
The join language  is our first prototype. All
examples in this paper are in join syntax. The system consists
in a bytecode compiler and a bytecode interpreter. Both compiler and
interpreter are Objective Caml  programs and it
is easy to lift Objective Caml data types and functions into join abstract data types and primitives. For instance, join
programs easily draw graphics, using the graphics Objective Caml
library. As a consequence, join can be seen either as a
language of its own, featuring many primitives, or as a distributed
layer on top of Objective Caml. Continuations are encoded using
ad hoc threads, which are created and scheduled by the join
The jocaml system is our second implementation. In jocaml,
all join-calculus constructs for concurrency, communication,
synchronization and process mobility are directly available as
syntactical extensions to Objective Caml. On the runtime environment
side, we have supplemented the original Objective Caml runtime system
(which already provides a thread library) with a special “join”
library and a distributed garbage collector . On the
compiler side, the Objective Caml compiler has been extended to
translate join-calculus source code into functions calls to the
“join” library. However, we also introduced a few new instructions
to Objective Caml bytecode, but only to handle code mobility, a
feature orthogonal to pattern-matching. The jocaml system is
currently available as a prototype version .