Thomas Given-Wilson

Axel Legay Inria

On the Expressiveness of Joining and Splitting

Keywords: LA, -, -, -, -: InP roc ::= [I] P OutP roc ::= [O] LS, -, -, -, -: InP roc ::= [I] P OutP roc ::= [O] P L-, -, -, -

An ongoing theme of the work of Bernhard Steffen has been the bringing together of different components in a coordinated manner and with a unified language. This paper explores this approach applied to process calculi that account for coordination of different kinds of workflows. Coordination here extends binary interaction to also account for joining of multiple outputs into a single input, and splitting from a single output to multiple inputs. The results here formalise which process calculi can and cannot be encoded into one another, and thus which language has the required expressiveness for given workflow properties. The combination of with other features of interaction allows for the representation of many systems and workflows in an appropriate calculus.

Introduction

An ongoing theme of the work of Bernhard Steffen has been the bringing together of different components in a functional and coordinated manner [START_REF] Steffen | Unifying models[END_REF][START_REF] Naujokat | Tailoring process synthesis to domain characteristics[END_REF][START_REF]Fundamental Approaches to Software Engineering -15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012[END_REF][START_REF] Cassel | A succinct canonical register automaton model[END_REF]. This ranges from early work on unifying models [START_REF] Burkart | Bisimulation collapse and the process taxonomy[END_REF][START_REF] Steffen | Unifying models[END_REF] to bringing together many components [START_REF] Margaria | Middleware: just another level for orchestration[END_REF], to programming environments that combine components and workflows [START_REF] Naujokat | Tailoring process synthesis to domain characteristics[END_REF][START_REF]Fundamental Approaches to Software Engineering -15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012[END_REF]. This theme has as its core finding common languages to express desirable behaviours, and approaches to unify these behaviours and workflows in a single language [START_REF] Burkart | Bisimulation collapse and the process taxonomy[END_REF][START_REF] Steffen | Unifying models[END_REF][START_REF] Margaria | Middleware: just another level for orchestration[END_REF][START_REF] Naujokat | Tailoring process synthesis to domain characteristics[END_REF][START_REF]Fundamental Approaches to Software Engineering -15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012[END_REF][START_REF] Neubauer | Plug-and-play higher-order process integration[END_REF][START_REF] Cassel | A succinct canonical register automaton model[END_REF].

This paper explores languages based on process calculi in the style of πcalculus that focus on coordinating workflows and higher-order process modelling [START_REF] Neubauer | Higher-order process modeling: Productlining, variability modeling and beyond[END_REF][START_REF] Neubauer | Plug-and-play higher-order process integration[END_REF]. The expressiveness of process calculi based upon their choice of communication primitives has been explored before [START_REF] Palamidessi | Comparing the expressive power of the synchronous and asynchronous pi-calculi[END_REF][START_REF] Busi | On the expressiveness of linda coordination primitives[END_REF][START_REF] De Nicola | On the expressive power of klaim-based calculi[END_REF][START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF][START_REF] Van Glabbeek | On the validity of encodings of the synchronous in the asynchronous π-calculus[END_REF]. In [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF] and [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF] this is detailed by examining combinations of four features: synchronism, arity, communication medium, and pattern-matching, and formalising their relations via valid encodings [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]. These four features allow the representation of many languages and many kinds of constraints and typing on interaction [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | An intensional concurrent faithful encoding of turing machines[END_REF]. However, recent work [START_REF] Given-Wilson | On the Expressiveness of Joining[END_REF] has extended binary interaction to joining as a form of coordination that allows a single process to receive input from many workflow producers in a single interaction. This work generalises to also account for splitting where a single process may produce outputs for many workflows in a single interaction (the dual of joining).

Along with the theme or Bernhard Steffen's works, this paper explores the common expressiveness of these languages, and shows which forms of interaction and workflow management can be represented in a single common process calculus. Similarly, the inability to express certain features of interaction is formalised, demonstrating which languages are required for which kinds of interaction and workflow behaviour.

The structure of the paper is as follows. Section 2 introduces the calculi considered here. Section 3 reviews the criteria used for comparing calculi. Section 4 considers encoding synchronism with coordination. Section 5 explores encoding arity via coordination. Section 6 presents results for encoding communication medium into coordination. Section 7 formalises that coordination cannot encode pattern-matching. Section 8 presents that coordination cannot be encoded by other features (i.e. synchronism, channel-names, pattern-matching). Section 9 considers relations between different forms of coordination. Section 10 concludes and discusses future work.

Calculi

This section defines the syntax, operational, and behavioural semantics of the calculi considered here. This relies heavily on the well-known notions developed for the π-calculus and adapts them when necessary to cope with different features. With the exception of the splitting this repeats many prior definitions from [START_REF] Given-Wilson | On the Expressiveness of Joining[END_REF], although there are minor syntactic changes for clarity in this work.

Assume a countable set of names N ranged over by a, b, c, . . .. Name-match patterns (denoted m, n), input patterns (denoted p, q), and terms (denoted s, t) are defined according to the following grammar: m, n ::=

x binding name | a name-match p, q ::= m name-match pattern | p • q (input pattern) compound s, t ::= a name | s • t (term) compound.

The name-match patterns are used for input, with binding names doing binding, and name-matches testing equality. The input patterns generalise the namematch patterns to also include compounds that support structure. The terms are used for output, with names being the base and compounds adding structure. The free names and binding names for input patterns and terms are as expected, taking the union of sub-patterns for compounds. Note that an input pattern is linear if and only if all binding names within the pattern are pairwise distinct. The rest of this paper will only consider linear input patterns.

This paper considers the possible combinations of five features for communication in a language denoted L α,β,γ,δ, where: α = A for asynchronous communication (output only prefoxes the empty process), and S for synchronous communication (output may prefix any process). β = M for monadic data (input or output only a single term), and P for polyadic data (input or output unbounded sequences of terms). γ = D for dataspace-based (interaction without named channels), and C for channel-based communications (interaction uses channel-names). δ = NO for no-matching (inputs can only bind), NM for name-matching (inputs can test equality of names), and I for intensionality (inputs can test name equality and also term structure). = B for binary (one input and one output interact), J for joining (one input may interact with many outputs), and L for splitting communication (one output may interact with many inputs).

For simplicity a dash -will be used when the instantiation of a feature is unimportant. The (parametric) syntax for the languages is: Most of the process forms as as usual: 0 denotes the null process; restriction (νa)P restricts the visibility of a to P ; parallel composition P |Q allows independent evolution of P and Q; and * P represents replication of the process P . The if s = t then P else Q represents conditional equivalence with if s = t then P used when Q is 0 (like the name match of π-calculus, if s = t then P else Q blocks either P when s = t or Q when s = t). The √ is used to represent a success process or state, in other works a specific barb or name has been used, however here by isolating √ as a specific process it is easier to reason about encodings (as also in) [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]. Finally, different languages are obtained by replacing the output OutP roc and input InP roc with the various definitions in Figure 1. The denotation • represents a sequence of the form • 1 , • 2 , . . . , • n and can be used for names, terms, input patterns, etc. (also denote with | • | the size of a set, multiset, or sequence).

As usual (νx)P and [a(. . . , x, . . .)] P and [(x•. . .)] P and [. . . | a(x) | . . .] P bind x in P . Observe that in [a(. . . , b , . . .)] P and [(. . .• b )] P neither a nor b bind in P , both are free. The corresponding notions of free and bound names of a process, denoted fn(P ) and bn(P ), are as usual. Also note that α-equivalence, denoted = α is assumed in the usual manner. Further, an input is linear if all binding names in that input occur exactly once (note that this is already assumed within an input pattern, here this is generalised to whole inputs). This paper shall only consider linear inputs. Finally, the structural congruence relation ≡ is the smallest congruence such that the following hold:

P | 0 ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R P ≡ P if P = α P * P ≡ P | * P (νa)0 ≡ 0 (νa)(νb)P ≡ (νb)(νa)P P | (νa)Q ≡ (νa)(P | Q) if a / ∈ fn(P ) .
Observe that L A,M,C,NO,B , L A,P,C,NO,B , L S,M,C,NO,B , and L S,P,C,NO,B use the communication paradigm of the asynchronous/synchronous monadic/polyadic π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Milner | The polyadic π-calculus: A tutorial[END_REF]. The language L A,P,D,NM ,B uses the communication paradigm of Linda [START_REF] Gelernter | Generative communication in Linda[END_REF]; the languages L A,M,D,NO,B and L A,P,D,NO,B the communication paradigm of the monadic/polyadic Mobile Ambients [START_REF] Cardelli | Mobile ambients[END_REF]; and L A,P,C,NM ,B that of µKlaim [START_REF] De Nicola | KLAIM: A kernel language for agents interaction and mobility[END_REF] or semantic-π [START_REF] Castagna | Semantic subtyping for the pi-calculus[END_REF].

Due to the large number of intensional languages of the form L α,β,γ,I, defined here, many do not match the communication paradigm of well-known calculi. However, the language L S,M,D,I,B is the asymmetric concurrent pattern calculus of [START_REF] Given-Wilson | An intensional concurrent faithful encoding of turing machines[END_REF] and calculi with other communication paradigms that match some of those here have been mentioned in [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF], as variations of Concurrent Pattern Calculus [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF] (with their behavioural theory as a specialisation of [START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF]). Similarly, the language L S,M,C,I,B uses the communication paradigm of Spi calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF][START_REF] Haack | Pattern-matching spi-calculus[END_REF] and Psi calculi (albeit with channel equivalence represented by equality and without the possibility of repeated binding names in patterns) [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF]. There are also similarities between the communication paradigm of L S,M,C,I,B and the polyadic synchronization π-calculus [START_REF] Carbone | On the expressive power of polyadic synchronisation in π-calculus[END_REF], although the intensionality in polyadic synchronization π-calculus is limited to the channel, i.e. inputs and outputs of the form s(x).P and s a .P , respectively.

The joining languages have several similarities to existing calculi. The language L A,P,C,NO,J uses a communication paradigm very close to an asynchronous π-calculus with joint input [START_REF] Nestmann | On the expressive power of joint input[END_REF]. L S,P,C,NO,J uses the communication paradigm of the general rendezvous calculus [START_REF] Bocchi | A process calculus of atomic commit[END_REF], and m-calculus [START_REF] Schmitt | The m-calculus: a higher-order distributed process calculus[END_REF], although the latter has higher order constructs and other aspects that are not captured within the features here. The language L S,M,C,NO,J has a similar communication paradigm to the Quality Calculus [START_REF] Nielson | A calculus for quality[END_REF][START_REF] Nielson | A calculus of quality for robustness against unreliable communication[END_REF], however the Quality Calculus has further conditions upon the inputs that cannot be represented by L S,M,C,NO,J . Despite these similarities to many languages related to Join Calculus, the Join Calculus itself is difficult to capture in the π-calculus based framework here. This is due to Join Calculus combining restriction, replication, and input into a single primitive [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF]. There are no exact connections for the splitting languages. Although one might consider some similarity with broadcast calculus [START_REF] Prasad | A calculus of broadcasting systems[END_REF] and bπ-calculus [START_REF] Ene | A broadcast-based calculus for communicating systems[END_REF] that both allow a single output to communicate with multiple inputs, even the closest splitting language L S,M,C,NO,L has a fundamentally different communication paradigm. The difference is that in the broadcast calculi the number of inputs required to interact with a broadcast is not fixed, while for L S,M,C,NO,L the number of inputs is fixed.

Remark 1. The languages Λ s,a,m,p can be easily partially ordered; in particular L α1,β1,γ1,δ1, 1 is a lesser language than L α2,β2,γ2,δ2, 2 if it holds that α 1 ≤ α 2 and β 1 ≤ β 2 and γ 1 ≤ γ 2 and δ 1 ≤ δ 2 and 1 ≤ 2 , where ≤ is the least reflexive relation satisfying the following axioms:

A ≤ S M ≤ P D ≤ C NO ≤ NM ≤ I B ≤ J B ≤ L .
This can be understood as the lesser language variation being a special case of the more general language. Asynchronous communication is synchronous communication with all output followed by 0. The operational semantics of the languages is given here via reductions as in [START_REF] Milner | The polyadic π-calculus: A tutorial[END_REF][START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF]. An alternative style is via a labelled transition system (LTS) such as [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF]. Here the reduction based style is to simplify having to define here the (potentially complex) labels that occur when both intensionality, and joining/splitting is in play. The LTS style can be used for intensional languages [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF]. Also, for the non-binary languages the techniques used in [START_REF] Boreale | Bisimulations in the join-calculus[END_REF] can be used directly for the no-matching joining languages, and with the techniques of [START_REF] Boreale | Bisimulations in the join-calculus[END_REF][START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF] to extend intensionality and other coordination forms.

Substitutions (denoted σ, ρ, . . .) in non-pattern-matching and name-matching languages are mappings from names to names. For intensional languages substitutions are mappings from names to terms. Note that substitutions are assumed to have finite domain. The application of a substitution σ to a pattern p is defined as follows:

σx = σ(x) x ∈ domain(σ) σx = x x ∈ domain(σ) σ x = (σx) σ(p • q) = (σp) • (σq) .
Where substitution is as usual on names, and on the understanding that (s

• t) def = s • t .
Given a substitution σ and a process P , denote with σP the (captureavoiding) application of σ to P that behaves in the usual manner. Note that capture can always be avoided by exploiting α-equivalence, which can in turn be assumed [START_REF] Urban | Barendregt's variable convention in rule inductions[END_REF][START_REF] Bengtson | Formalising the pi-calculus using nominal logic[END_REF].

The matching of terms t with patterns p is handled in two parts. First, the match rule {t/ /p} of a term t with a pattern p to create a substitution σ:

{t/ /x} def = {t/x} {a/ / a } def = {} {s • t/ /p • q} def =
{s/ /p} ∪ {t/ /q} {t/ /p} undefined otherwise.

Any term t can be matched with a binding name x to generate a substitution from the binding name to the term {t/x}. A single name a can be matched with a name-match for that name a to yield the empty substitution. A compound term s • t can be matched by a compound pattern p • q when the components match to yield substitutions {s/ /p} = σ 1 and {t/ /q} = σ 2 , the resulting substitution is the union of σ 1 and σ 2 . (Observe that, since patterns are linear, the substitutions of components will always have disjoint domain.) Otherwise the match is undefined.

The second part is then the poly-match rule Match( t; p) that determines matching of a sequence of terms t with a sequence of patterns p, defined below.

Match(; ) = {} {s/ /p} = σ 1 Match( t; q) = σ 2 Match(s, t; p, q) = σ 1 ∪ σ 2 .
The empty sequence matches with the empty sequence to produce the empty substitution. Otherwise, when there is a sequence of terms s, t and a sequence of patterns p, q, the first elements are matched by {s/ /p} and the remaining sequences use the poly-match rule. If both are defined and yield substitutions, then the union of substitutions is the result. (Like the match rule, the union is ensured to happen between substitutions with disjoint domain by linearity of inputs.) Otherwise the poly-match rule is undefined, for example when a single match fails, or the sequences are of different arity.

There are now three base reduction rules, one for each of binary, joining, and splitting languages. The binary reduction rule is:

[s t ] P | [s( p)] Q -→ P | σQ Match( t; p) = σ
that states that the split [s t ] P interacts with the join [s( p)] Q to yield P | σQ when the channel name s is the same and the match Match( t; p) is defined and yields σ. Note that P is omitted in the asynchronous languages and the channel names s are omitted in the dataspace-based languages.

The joining reduction rule is:

[s 1 t 1 ] P 1 | . . . | [s i t i ] P i | [s 1 ( p 1 ) | . . . | s i ( p i )] Q -→ P 1 | . . . | P i | σQ Match( t 1 , . . . , t i ; p 1 , . . . , p i ) = σ
that states that i splits [s i t i ] P i can interact with a single join when all of the outputs of the splits s i t i can be matched against the inputs of the join Match( t 1 , . . . , t i ; p 1 , . . . , p i ) to yield a substitution σ, and then reduce to the continuations of the splits P 1 | . . . | P i in parallel with σQ.

The splitting reduction rule is the mirror of the joining rule:

[s 1 t 1 | . . . | s i t i ] P | [s 1 ( p 1 )] Q 1 | . . . | [s i ( p i )] Q i -→ P | σ 1 Q 1 | . . . | σ i Q i Match( t j ; p j ) = σ j j ∈ {1, . . . , i}
where all the outputs of a single split [s 1 t 1 | . . . | s i t i ] P match Match( t j ; p j ) with separate joins [s j ( p j )] Q i to yield σ j and reduce to

P | σ 1 Q 1 | . . . | σ i Q i for all j ∈ {1, . . . , i}.
The general reduction relation -→ for all languages also includes:

P -→ P P | Q -→ P | Q P -→ P (νa)P -→ (νa)P P ≡ Q Q -→ Q Q ≡ P P -→ P s = t P | Q -→ S P | if s = t then Q else R -→ S s = t P | R -→ S P | if s = t then Q else R -→ S .
The reflexive transitive closure of -→ is denoted by =⇒. Lastly, for each language let denote a reduction-sensitive behavioural equivalence for that language. A reduction-sensitive behavioural equivalence is one where it holds that P P and P -→ imply P -→ as in Definition 5.3 of [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] (observe that this rules out weak bisimulations for example). For the nonintensional languages these are mostly already known, either by their equivalent language in the literature, such as asynchronous/synchronous monadic/polyadic π-calculus or Join Calculus, or from [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF]. For the intensional languages the results in [START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF] can be used. For the joining languages that reflect those of the literature the techniques used in [START_REF] Boreale | Bisimulations in the join-calculus[END_REF] apply. For other combinations of joining, and splitting, as well as the addition of intensionality to non-binary languages, adaptations of [START_REF] Boreale | Bisimulations in the join-calculus[END_REF][START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF] should prove adequate.

Encodings

This section recalls the definition of valid encodings as well as some useful results (details in [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]) for formally relating process calculi.

The choice of valid encodings here is to align with prior works [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF][START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF]] and where possible reuse prior results. These valid encodings are those used, sometimes with mild adaptations, in [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF][START_REF] Gorla | A taxonomy of process calculi for distribution and mobility[END_REF][START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Nielsen | Multiparty symmetric sum types[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | A Concurrent Pattern Calculus[END_REF] and have also inspired similar works [START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF][START_REF] Lanese | On the expressive power of primitives for compensation handling[END_REF][START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. However, there are alternative approaches to encoding criteria or comparing expressive power [START_REF] Boudol | Notes on algebraic calculi of processes[END_REF][START_REF] Simone | Higher-level synchronising devices in Meije-SCCS[END_REF][START_REF] Carbone | On the expressive power of polyadic synchronisation in π-calculus[END_REF][START_REF] Parrow | Expressiveness of process algebras[END_REF][START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. Further arguments in favour of, or against, the valid encodings here can be found in [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF][START_REF] Gorla | A taxonomy of process calculi for distribution and mobility[END_REF][START_REF] Peters | Translational expressiveness: comparing process calculi using encodings[END_REF][START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF][START_REF] Given-Wilson | A Concurrent Pattern Calculus[END_REF].

An encoding of a language L 1 into another language L 2 is a pair (

[[ • ]], ϕ [[ ]]
) where [[ • ]] translates every L 1 -process into an L 2 -process and ϕ [[ ]] maps every name (of the source language) into a tuple of k names (of the target language), for k > 0. In doing this, the translation may fix some names to play a precise rôle or may translate a single name into a tuple of names, this can be obtained by exploiting ϕ

[[ ]] .
To aid in the following definition and the results later in the paper, a process P is defined to be at top-level when P may be under any combination of restrictions, conditionals, or replications, but that none of these can prevent reduction or interaction by P . For example, P is top-level in (νn)P and * P and if s = s then P else Q and if s = t then Q else P where s = t and (νn)if s = s then * (P | Q) else R.

Now consider only encodings that satisfy the following properties. Let a kary context C(• 1 ; . . . ; • k ) be a process with k holes. Denote with -→ ω an infinite sequence of reductions. Let P ⇓ mean there exists P such that P =⇒ P and P has an instance of √ at top-level, that is the process P eventually exhibits the success process √ . Moreover, let denote the reference behavioural equivalence. Finally, to simplify reading, let S range over processes of the source language (viz., L 1 ) and T range over processes of the target language (viz., L 2 ) and let the notation of a language L i be subscripted by i, e.g. i , -→ i , etc.

Definition 1 (Valid Encoding). An encoding ([[ • ]], ϕ [[ ]] ) of L 1 into L 2 is valid if it satisfies
the following five properties:

1. Compositionality: for every k-ary operator op of L 1 and for every subset of names N , there exists a k-ary context

C N op (• 1 ; . . . ; • k ) of L 2 such that, for all S 1 , . . . , S k with fn(S 1 , . . . , S k ) = N , it holds that [[ op(S 1 , . . . , S k ) ]] = C N op ([[ S 1 ]]; . . . ; [[ S k ]]
). 2. Name invariance: for every S and substitution σ, it holds that [START_REF] Gorla | A taxonomy of process calculi for distribution and mobility[END_REF]. However, compositionality can be ensured by respecting the below definition of compositional valid encodings. All encodings considered in this paper satisfy this restriction, and therefore are compositional and may be used as such in later proofs.

[[ σS ]] = σ [[ S ]] if σ is injective and [[ σS ]] 2 σ [[ S ]] otherwise where σ is such that ϕ [[ ]] (σ(a)) = σ (ϕ [[ ]] (a)) for every name a ∈ N . 3. Operational correspondence: for all S =⇒ 1 S , it holds that [[ S ]] =⇒ 2 2 [[ S ]]; and for all [[ S ]] =⇒ 2 T , there exists S such that S =⇒ 1 S and T =⇒ 2 2 [[ S ]]. 4. Divergence reflection: for every S such that [[ S ]] -→ ω 2 , it holds that S -→ ω 1 . 5. Success sensitiveness: for every S, it holds that S ⇓ 1 if and only if [[ S ]] ⇓ 2 .

The existence of encodings [[

• ]] 1 from L 1 into L 2 and [[ • ]] 2 from L 2 into L 3 does not ensure that [[ [[ • ]] 1 ]] 2 is a valid encoding from L 1 into L 3

Definition 2 (Compositional Valid Encodings). An encoding ([[

• ]], ϕ [[ ]] ) of L 1 into L 2 is compositional if it satisfies
the properties 1,2,4 and 5 from Definition 1 and the following properties:

-Operational Correspondence revisited: for all S =⇒ 1 S , it holds that [[ S ]] =⇒ 2 [[ S ]] | T , for some T 2 0; and for all [[ S ]] =⇒ 2 T , there exists S such that S =⇒ 1 S and T =⇒ 2 [[ S ]] | T , for some T 2 0. -preserves the equivalence class of 0: for every S 1 0, [[ S ]] 2 0. -is homomorphic w.r.t. |: for every S 1 , S 2 , [[ S 1 | S 2 ]] = [[ S 1 ]] | [[ S 2 ]].
The following three results are here recalled from prior works as they are useful for later proofs.

Proposition 1 (Proposition 5.5 from [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]). The following two results (and a few later in the paper) exploit the notation block(S) that denotes the process (νn)(νm)if n = m then S where n, m ∈ fn(S).

Let [[ • ]] be a valid encoding; then, S -→ / implies that [[ S ]] -→ / .
Proposition 2 (Proposition 5.6 from [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]). Let [[ • ]] be a valid encoding; then for every set of names N , it holds that

C N | (• 1 ,
• 2 ) has both its holes at top-level.

Proof. Fix a set of names N and a process S with fn(S) = N . Now consider

S = √ | block(S). By Proposition 1 it must be that [[ S ]] -→ / , since S -→ / . By compositionality we must have [[ S ]] = C N | ([[ √ ]], [[ block(S) ]]). By success sensitiveness it must be that [[ S ]] ⇓ since S ⇓. All these facts entail that the top- level occurrence of √ in [[ S ]
] is exhibited: either by the translating context and so

C N | (•, •) ⇓; or by [[ √ ]], but this implies that C N | (•, •) has the first hole • at top- level. Indeed, it is not possible that √ is exhibited by [[ block(S) ]] since block(S) ⇓. However, the first case is not possible otherwise [[ block(S) | block(S) ]] ⇓, whereas block(S) | block(S) ⇓. To show that the second hole in C N | (•,
•) is at top-level it suffices to reason in the very same way using S = block(S) | √ .

Proposition 3 (Adapted from Proposition 5.7 from [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]). Let [[ • ]] be a valid encoding; if there exist two processes S 1 and S 2 such that The general way to prove the lack of a valid encoding is as follows. By contradiction assuming there is a valid encoding [[ • ]]. Find a pair of processes P and Q that satisfy Proposition 3 such that

S 1 | S 2 ⇓, with S i ⇓ and S i -→ / for i = 1, 2, then [[ S 1 | S 2 ]] -→. Proof. By success sensitiveness [[ S 1 | S 2 ]] ⇓ and by Proposition 2 C N | ([[ S 1 ]], [[ S 2 ]]) has both [[ S 1 ]] and [[ S 2 ]] at top-level. However, since none of [[ S 1 ]], [[ S 2 ]],
P | Q -→ and [[ P | Q ]] -→. From Q obtain some Q such that P | Q -→ / and [[ P | Q ]] -→.
Conclude by showing this in contradiction with some properties of the encoding or Proposition 1.

The following result is a consequence of the choices of languages and encoding criteria, which corresponds to formalising Remark 1.

Theorem 1. If a language L 1 is a lesser language than L 2 (by the ≤ relation of Remark 1) then there exists a (compositional) valid encoding

[[ • ]] from L 1 into L 2 .
Proof. The encoding [[ • ]] is as described in Remark 1. The proof is then straightforward and ensured by definition of the rule for the base reduction. For a detailed example of the proof technique see Theorem 2.

Coordination and Synchronism

This section considers the relation between coordination and synchronism. It turns out that coordination is unable to encode synchronism unless it could otherwise be encoded by other features.

In general synchronous communication can be encoded into asynchronous communication when the target language includes: channel names; name-matching and polyadicity; or intensionality. Thus it is sufficient to consider the languages L A,M,D,NO,-and L A,P,D,NO,-and L A,M,D,NM ,-since the other asynchronous languages can encode their synchronous joining counterparts in the usual manner [START_REF] Honda | An object calculus for asynchronous communication[END_REF][START_REF] Boudol | Asynchrony and the pi-calculus[END_REF]. This can be adapted in the obvious manner for L S,M,C,NO,J into L A,M,C,NO,J as follows

[[ [n a ] P ]] def = (νz)([n z ] | [z(x)] ([x a ] | [[ P ]])) [[ [n 1 (a 1 ) | . . . | n i (a i )] Q ]] def = (νx 1 , . . . , x i )[n 1 (z 1 ) | . . . | n i (z i )] ([z 1 x 1 ] | . . . | [z i x i ] | [x 1 (a 1 ) | . . . | x i (a i )] [[ Q ]]) .
The idea for binary languages is that the encoded output creates a fresh name synchronises with all the encoded outputs at once, sends the fresh names x j in parallel, and then synchronises on all the a j in the last step. The encoding above is shown for L S,M,C,NO,J into L A,M,C,NO,J and is the identity on all other process forms. This can be proven to be a valid encoding.

Lemma 1. If P ≡ Q then [[P ]] ≡ [[Q]]. Conversely, if [[P ]] ≡ Q then Q ≡ [[P ]]
for some P ≡ P .

Proof. The only non-trivial cases are the join and split as the others are translated homomorphically. The join and split are also straightforward as the only non-trivial parts are the possible renaming of new restricted names introduced in the translation.

Lemma 2. Given a L S,M,C,NO,J join P and split Q then

[[P ]] | [[Q]] -→ if and only if P | Q -→.
Proof. Both parts can be proved by induction on the height of the proof tree for the judgements [[ P | Q ]] -→ and P | Q -→. The base case is ensured by k applications of the poly-match rule when P is of the form [n 1 (x 1 ) | . . . | n k (x k )] P . Note that Lemma 1 is used for structural congruence.

Lemma 3. The translation [[•]

] from L S,M,C,NO,J into L A,M,C,NO,J preserves and reflects reductions. That is: if P -→ P then there exists Q such that

[[ P ]] -→ k Q and Q = [[ P ]]; and if [[ P ]] -→ Q then there exists Q such that Q -→ k-1 Q and Q = [[ P ]]
for some P such that P -→ P .

Proof. Both parts can be proved by straightforward induction on the judgements P -→ P and [[P ]] -→ Q, respectively. In both cases, the base step is the most interesting and follows from Lemma 2, for the second case the step Q -→ Q is ensured by the definition of the translation and match rule. The size of k (the number of target steps required to simulate one source step) in both cases is 2+i where i is the number of inputs of the join involved in P -→ P . The inductive cases where the last rule used is a structural one rely on Lemma 1.

Theorem 2. There is a valid encoding from L S,M,C,NO,J into L A,M,C,NO,J .

Proof. Compositionality and name invariance hold by construction. Operational correspondence (with structural equivalence in the place of ) and divergence reflection follow from Lemma 3. Success sensitiveness can be proved as follows: P ⇓ means that there exists P and k ≥ 0 such that P -→ k P and P has √ at top-level; by exploiting Lemma 3 k times and Lemma 1 obtain that [[P ]] -→ j [[P ]] and P has √ at top-level and where j can be determined from the instantiations of Lemma 3, i.e. that [[P ]] ⇓. The converse implication can be proved similarly.

Splitting can be adapted in a similar manner, e.g. consider the encoding from

L S,M,C,NO,L into L A,M,C,NO,L [[ [n 1 a 1 | . . . | n i a i ] P ]] def = (νz 1 , . . . , z i )([n 1 z 1 | . . . | n i z i ] | [z 1 (x 1 )] . . . [z i (x i )] ([x 1 a 1 | . . . | x i a i ] | [[ P ]])) [[ [a(b)] Q ]] def = (νx)[a(z)] ([z x ] | [x(b)] [[ Q ]])
The use of fresh names z and x is as before. The splitting version is similar except the split synchronises with all the encoded inputs at once, sending fresh names z j in parallel, then collects all the responses with fresh names x j , and then splits sending all the original names a i at once in the last step. The encoding above for L S,M,C,NO,L into L A,M,C,NO,L is the identity on all other process forms. This can similarly be proven to be a valid encoding. Theorem 3. There is a valid encoding from L S,M,C,NO,L into L A,M,C,NO,L .

Proof. The same proof technique as Theorem 2 applies here.

Corollary 1. If there exists a valid encoding from L S,β,γ,δ,B into L A,β,γ,δ,B then there exists a valid encoding from L S,β,γ,δ, into L A,β,γ,δ, .

Proof. Theorems 2 & 3 provide the foundation for all the channel-based results. For the other encodings where channels are not available in the target language, the target language can already encode channel-based communication and so the above results can still be used. For the polyadic and name-matching languages this holds by Proposition 4.1 of [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF], otherwise for the intensional languages this holds by Theorem 6.4 of [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF].

These results confirm that the ability to encode synchronous communication into asynchronous communication is not impacted by changes to coordination. Any encoding that holds from a binary synchronous language into a binary asynchronous language also holds when both languages are instead joining, or splitting. Thus no expressiveness is lost by changing from binary languages to other coordination forms, and existing results can easily be transferred.

The following results formalise that there exist no new encodings from a synchronous languages into an asynchronous languages as a result of shifting from both languages being binary, to both languages being joining or splitting. That is, if there exists no valid encoding from L S,β1,γ1,δ1,B into L A,β2,γ2,δ2,B , then there exists no valid encoding from L S,β1,γ1,δ1, into L A,β2,γ2,δ2, . The impossibility of encoding L S,M,D,NM ,J into L A,M,D,NM ,J is detailed as it illustrates the key proof technique. The other results are either simpler variations (i.e. without name-matching) or straightforward adaptations to consider splitting. ] must include both some n as part of some split, and some ( m ) where m = n (this can be name-matches for any number of names = n, but assume one for simplicity) as part of some join. Otherwise the join must be of the form

[(z 1 ) | . . . | (z j ) | ( n ) | . . . | ( n )] S for k instances of ( n ) and it follows that j + k instances of Q 1 in parallel would reduce when encoded [[ Q 1 | . . . | Q 1 ]] -→ while j +k instances of Q 1 in parallel do not reduce unencoded Q 1 | . . . | Q 1 -→ / violating Proposition 1. Thus, observe that [[ Q ]]
must be able to send at least one name to [[ P ]] via an output d for some d (this could be any number of names sent via different outputs, but assume 1 here for simplicity). Now consider the name d. -

If d is top-level in [[ Q ]] then there exist some k such that k instances of Q 1 in parallel would reduce if encoded [[ Q 1 | . . . | Q 1 ]] -→ while k instances of Q 1 in parallel unencoded do not reduce Q 1 | . . . | Q 1 -→ / and this violates Proposition 1. -If d is not top-level in [[ Q ]], instead d is top-level in some S where [[ P | Q ]] =⇒ S.
Conclude in the same manner as in the first case. Proof. This is proved in a very similar manner to Theorem 4.

If R 1 is a top-level component of [[ Q ]] then [[ Q ]] must also include a top-level join because otherwise if Q = Ω (where Ω is a divergent process) then [[ Q ]]
[ P | σQ | Q ]] -→ R that must be between some component of [[ P ]] and either a component of [[ σQ ]] or [[ Q ]] (because if [[ P ]] was not involved then C N | (C N | ([[ (νn)[( n )] [ b ] 0 ]], [[ σQ ]]), [[ Q ]])
Corollary 2. If there exists no valid encoding from L S,β1,γ1,δ1,B into L A,β2,γ2,δ2,B , then there exists no valid encoding from L S,β1,γ1,δ1, into L A,β2,γ2,δ2, .

Proof. The techniques in Theorems 4 & 5 apply to all monadic joining and splitting languages, respectively. Monadic no-matching languages are simpler variants of the same proof technique, while polyadic no-matching (because polyadic name-matching can encode synchronous communication into asynchronous) is a simple generalisation of the above proofs.

That joining or splitting do not allow for an encoding of synchronous communication alone is not surprising, because there is no control in the input of which outputs are interacting with (without some other control such as channel names or pattern-matching). Thus, being able to consume more outputs or inputs in a single interaction does not capture synchronous behaviours.

This formalizes that there is no change to results within languages grouped by their coordination form. Separation results between coordination forms, and that synchronism and coordination are orthogonal are concluded in Section 8.

Coordination and Arity

This section considers the relation between non-binary coordination and arity. Although there appears to be some similarities in that both have a base case (monadic or binary), and unbounded cases (polyadic or joining/splitting, respectively), these cannot be used to encode arity into coordination unless they could be encoded otherwise.

The interesting results here are the separation results that ensure no new encodings or expressiveness. The proof technique is clearly illustrated by the following result for the joining setting. The splitting result is very similar with only minor adaptations to the proof. Theorem 7. There exists no valid encoding from L A,P,D,NO,B into L A,M,D,NO,L .

Proof. A straightforward adaptation of Theorem 6.

Corollary 3. If there exists no valid encoding from L α1,P,γ1,δ1,B into L α2,M,γ2,δ2,B , then there exists no valid encoding from L α1,P,γ1,δ1, into L α2,M,γ2,δ2, .

Proof. The techniques in Theorems 6 & 7 apply to all joining and splitting languages, respectively. Name-matching requires only a small change of Q = [(x, y)] if a = x then √ to then ensure binding occurs and not only namematching; this is then proved via contradiction name invariance and success sensitiveness like in Theorem 5. The techniques in Theorem 11 more elegantly show that channel-based communication is insufficient, so they are omitted here.

Thus any form of non-binary coordination does not allow for encoding a polyadic language into a monadic language unless it could already be encoded by some other means.

The other main results are to show that existing encodings between binary languages can be reproduced in other forms of coordination. This turns out to be a straightforward adaptation of the usual techniques.

Consider the usual encoding of L S,P,D,NO,B into L S,M,C,NO,B [START_REF] Milner | Communicating and mobile systems -the Pi-calculus[END_REF]:

[[ [ a ] P ]] def = (νc)[n c ] [c a 1 ] . . . [c a n ] [[ P ]] [[ [( x)] Q ]] def = [n(z)] [z(x 1 )] . . . [z(x n )] [[ Q ]]
where c is not in the free names of [ a ] P , and z is not in the free names of [( x)] Q or x. Also n is derived from a since a = a 1 , . . . , a n (and similarly for x). Thus when an output and input agree upon their arity n then they interact with the output sending a fresh name c used for sending the n names a. This can be adapted in the obvious manner, shown below for the encoding of L S,P,D,NO,J into L S,M,C,NO,J .

[

[ [ a ] P ]] def = (νc)[n c ] [c a 1 ] . . . [c a n ] [[ P ]] [[ [( x1) | . . . | ( xk)] Q ]] def = [n1(z 1 ) | . . . | nk(z k )] [z 1 (x1 1 )] . . . [z 1 (x1 n1 )] . . . [z k (xk 1 )] . . . [z k (xk nk )] [[ Q ]]
where the restrictions on z are here extended to distinct z 1 , . . . , z k for each input.

Theorem 8. There is a valid encoding from L S,P,D,NO,J into L S,M,C,NO,J .

Proof. The proof technique is identical to Theorem 2.

This illustrates the key ideas for the following general result, that requires only straightforward adaptations of the proofs in the obvious manner. It is worth noting that all such results rely on the use of a channel-name, or an equivalent pattern match of some form to detect compatible arity and then ensure the right processes communicate. This is clearly available when adding channelbased communication, or when exploiting intensionality. Theorem 9. If there exists a valid encoding from L α1,P,γ1,δ1,B into L α2,M,γ2,δ2,B then there exists a valid encoding from L α1,P,γ1,δ1, into L α2,M,γ2,δ2, .

This confirms that encodings in the binary setting still exist in different coordination settings. Thus no expressiveness differences between languages are lost by changing coordination form, and existing results can be transferred.

Coordination and Communication Medium

This section considers the relation between coordination and communication medium. In general coordination is unable to encode communication medium unless it could otherwise be encoded by other features. This is proved by two main results: that if there is no valid encoding from a channel-based binary language to a dataspace-based binary language then there is no encoding when replacing binary with joining or splitting; and that if there exists a valid encoding from a channel-based binary language into a dataspace-based binary language then there exists an encoding with binary replaced by joining or splitting.

The base result for joining is illustrated in the following theorem, generalised in the corollary that follows.

ing that [[ [a(x)] 0 | [a b 1 , b 2 ] ]] -→ =⇒ [[ [a(x)] 0 | [a b 1 , b 2 ] ]] and so [[ [a(x)] 0 | [a b 1 , b 2 ] ]] -→ ω ).
Thus any form of non-binary coordination does not allow for encoding channels in a dataspace-based language unless it could already be encoded.

The positive encoding results are the typical adaptations of the positive encoding results in the binary setting. The adaptation of the usual encoding for L S,P,C,NM ,J into L S,P,D,NM ,J is the obvious one as below.

[

[ [a c ] P ]] def = [ a, c ] [[ P ]] [[ [a 1 ( x1) | . . . | a k ( xk)] Q ]] def = [( a 1 , x1) | . . . | ( a k , xk)] [[ Q ]]
For the each channel-based output a c the channel name a is moved to the first position of the dataspace-based output a, c in the encoding. The same is done for each channel-based input a( x) becoming a dataspace-based input (a, x).

Theorem 12. There is a valid encoding from L S,P,C,NM ,J into L S,P,D,NM ,J .

Proof. The proof technique is identical to Theorem 2 (albeit simpler since each reduction in the source language corresponds to exactly one reduction in the target language and vice versa). This illustrates the key ideas for the following general result, that requires only straightforward adaptations of the proofs in the obvious manner. Again all such results rely upon the use of pattern-matching, either via name-matching or intensionality, to represent the channel.

Theorem 13. If there exists a valid encoding from L α1,β1,C,δ1,B into L α2,β2,D,δ2,B then there exists a valid encoding from L α1,β1,C,δ1, into L α2,β2,D,δ2, .

This confirms that encodings of channel-based communication into dataspacebased communication in the binary setting still exist in different coordination settings. Thus no expressiveness differences between languages are lost by changing coordination form, and existing results can be transferred.

Coordination and Pattern-Matching

This section considers the relations between coordination and pattern-matching. Intensionality cannot be encoded into a name-matching (or no-matching) language by exploiting joining or splitting. Similarly name-matching cannot be encoded into a no-matching language by exploiting joining or splitting.

To assist with the below theorem, define the maximal interaction patterns mip(P ) of a process P as follows: mip(0) = 0 mip((νa)P ) = mip(P ) mip( * P ) = mip(P ) mip(

√ ) = 0 mip(P | Q) mip(if s = t then P else Q) = mip(P ) if mip(P ) > mip(Q) mip(Q) otherwise mip([ t 1 | . . . | t i ] P ) = j=0,...,i | t j | mip([s 1 t 1 | . . . | s i t i ] P ) = i + j=0,...,i | t j | mip([( p 1 ) | . . . | ( p i )] P ) = j=0,...,i | p j | mip([a 1 ( p 1 ) | . . . | a i ( p i )] P ) = i + j=0,...,i | p j | .
The intuition is that mip(P ) indicates the maximum number of patterns that can be matched by any single split or join of P (i.e. any single OutP roc or InP roc). For the null process, restriction, parallel composition, replication, conditional, and success process this is straightforward, the only non-trivial case is the conditional if s = t then P else Q where both P and Q can be considered (this is to allow flexibility when substitutions may allow either P or Q to be possible). For the splits (resp. joins), when the language is dataspace-based then this is the sum of the arities of all outputs in the split (resp. inputs in the join), and when the language is channel-based the maximum interaction patterns also counts the channel terms (i+ above).

Lemma 4. Given a process P (for any language), for all substitutions σ it holds that mip(P ) = mip(σ(P )).

Proof. The proof is straightforward by induction on the structure of P .

Observe that in name-matching languages, for any process P then mip(P ) is the upper bound on the number of names that can be matched in any split or join of P . For no-matching languages the upper bound is at most mip(P ) 2 (when the maximum arity of any output in a split or input in a join is 1), although this is less significant to the result below. (For intensional languages there is no upper bound, related to mip(P ) or otherwise, however since the goal is to use mip(P ) to reason about non-intensional languages, this is not relevant.)

The first result is to prove that intensionality cannot be encoded by coordination. Recall that since intensionality alone can encode all other features aside from coordination, it is sufficient to consider L A,M,D,I,B . Proof. The same technique as in Theorem 14 can be applied for splitting.

Corollary 5. If there exists no valid encoding from L α1,β1,γ1,I,B into L α2,β2,γ2,δ,B , then there exists no valid encoding from L α1,β1,γ1,I, into L α2,β2,γ2,δ, .

Proof. The joining case is by Theorem 14 and the splitting by Theorem 15.

It follows that any form of coordination cannot represent intensionality in a language that does not have intensionality already (including name-matching or no-matching languages).

The next results show that coordination is insufficient to encode name matching. Unlike Theorem 14, these need to be separated into two results due to the encoding from L A,M,D,NM ,B into L A,M,C,NO,B [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF]. Now if there is no blocking via an if a 1 = a 2 then S 1 else S 2 then this yields a contradiction in the usual manner (see Theorem 4) via either:

[[ P | σQ ]] ⇓ while P | σQ ⇓, or [[ σ(P | Q) ]] ⇓ while σ(P | Q) ⇓.
Therefore there must be a conditional if a 1 = a 2 then S 1 else S 2 that prevents reduction (there may be many, but assume one for simplicity). Further, this must be in [[ Q ]] because otherwise this would violate compositionality and success sensitiveness with

C N | ([[ P ]], •) replacing • with [[ Q ]] or [[ σQ ]]. It must be that a 1 = a 2 in [[ Q ]] because otherwise if a 1 = a 2 then no substitution σ (defined by name invariance σ [[ • ]] = [[ σ(•) ]]
) could make σ a 1 = σ a 2 when a 1 = a 2 . Therefore, it must be that σ a 1 = σ a 2 , however by considering the substitution ρ = {a/c} (and associated ρ from name invariance) it must be that ρ σ

[[ Q ]] [[ Q ]], yet ρ cannot induce inequality in σ a 1 = σ a
P | Q ]] -→ must be of the form [c 1 m 1 ] | . . . | [c i m i ] | [c 1 ( z 1 ) | . . . | c i ( z i )]
R for some c and m and z and i and R . Now consider the substitutions σ = {c/a} and ρ = {d/b} (and their associated substitutions on encoded processes σ and ρ determined by name invariance and validity of the encoding). Observe that because σP

| Q -→ / it follows that C N | (σ [[ P ]], [[ Q ]]) -→ / by Proposition 1.
The reduction can only be prevented by either a conditional or the changing of a channel name via the substitution σ . (Observe that conditionals may introduce or remove splits and joins accounting for missing components or changes in arity, and so the only other possibility for preventing reduction is by changing the channel name.) If the reduction is prevented due to a conditional then contradiction can be achieved as in Theorem 16, so it must be that σ (c j ) = c j for some j ∈ {1, . . . , i}. The same can be shown for ρP | Q and some c k such that ρ (c k ) = c k . Further, by exploiting the inverse substitutions denoted inv(σ) for the inversve of σ (defined in the obvious manner) it must be that j = k, because otherwise inv(σ )ρ (c j ) = c Thus coordination does not allow for encoding name-matching into a nomatching language unless it could already be encoded by some other means.

For the positive results that remain it is straightforward to adapt the existing encodings in the same manner as for Corollary 1, and Theorems 9 & 13.

Theorem 20. If there exists a valid encoding from L α,β,γ,δ1,B into L α,β,γ,δ2,B where δ 1 ≤ δ 2 then there exists a valid encoding from L α,β,γ,δ1, into L α,β,γ,δ2, .

Proof. The same techniques as Corollary 1, and Theorems 9 & 13 can be applied.

Finally, the positive results that preserve encodings when changing the coordination feature can be combined into a single general result.

Corollary 7. If there exists a valid encoding from L α1,β1,γ1,δ1,B into L α2,β2,γ2,δ2,B then there exists a valid encoding from L α1,β1,γ1,δ1, into L α2,β2,γ2,δ2, .

Proof. By combining Corollary 1, and Theorems 9, 13, & 20.

Coordination and Other Features

This section considers the expressive power gained by coordination. It turns out that coordination adds expressive power that cannot be represented by binary languages regardless of other features.

The expressive power gained by joining or splitting can be captured by the concept of the coordination degree of a language L, denoted Cd(L), as the least upper bound on the number of processes that must coordinate to yield a particular reduction in L. For example, all the binary languages L -,-,-,-,B have coordination degree 2 since their reduction axiom is only defined for two processes. By contrast, the coordination degree of the non-binary languages is ∞ since there is no bound on the number of inputs that can be part of a join, or outputs that can be part of a split. The above may not appear intuitive when some implementations of n-ary coordination are achieved by 2-ary coordination. However, the result shows that such implementations must have conditions under which they begin coordination when the coordination cannot be completed and so either: become stuck waiting for further coordination; or must roll-back to a prior state. The first case would here invalidate the encoding by blocking an alternative valid coordination, while the second case would here indicate an infinite reduction sequence again invalidating the encoding. Corollary 8. There exists no valid encoding from L -,-,-,-, into L -,-,-,-,B where = B.

In the other direction the result is ensured by Remark 1. Thus for any languages L α,β,γ,δ, 1 and L α,β,γ,δ, 2 where 1 < 2 then it holds that L α,β,γ,δ, 2 is strictly more expressive than L α,β,γ,δ, 1 . That is, joining or splitting languages are strictly more expressive than binary languages.

Thus coordination turns out to be orthogonal to all other features, since from the prior sections coordination cannot encode any other feature, and here it is proven that other features cannot encode coordination.

Within Coordination

This section considers relations between different forms of coordination. It turns out that there are some encodings from joining languages into splitting languages and vice versa, however most joining and splitting languages are unrelated.

A joining (resp. splitting) language without matching capabilities can be encoded into a splitting (resp. joining) language. For example, consider the encoding from L S,M,C,NO,J to L S,M,C,NO,L that is the identity on all forms except the output and join as follows:

[

[ [a b ] P ]] def = [a(c)] [c b ] [[ P ]] [[ [a 1 (x 1 ) | . . . | a i (x i )] Q ]] def = (ν c)([a 1 c 1 | . . . | a i c i ] [c 1 (x 1 )] . . . [c i (x i )] [[ Q ]])
where c is not b or in the free names of P ; and c does not intersect with a or x or the free names of Q. The key idea is that the direction of communication is reversed; splits become joins (with outputs becoming inputs), and joins become splits (with inputs becoming outputs), a fresh name c is transmitted to be used for then sending the original name b from the output to the encoded join. Thus the requirement that all inputs of a join interact at once is maintained by all the outputs of the split. Observe that this is similar in concept to the encoding of synchrony into asynchrony by Honda & Tokoro [START_REF] Honda | An object calculus for asynchronous communication[END_REF].

Theorem 22. The encoding from L S,M,C,NO,J into L S,M,C,NO,L is valid.

Proof. The proof technique is identical to Theorem 2.

The same approach can be used to encode L S,M,C,NO,L into L S,M,C,NO,J with adjustments to the split and join as follows:

[

[ [a 1 b 1 | . . . | a i b i ] P ]] def = [a 1 (c 1 ) | . . . | a i (c i )] [c 1 b 1 ] . . . [c i b i ] [[ P ]] [[ [a(x)] Q ]] def = (νc)[a c ] [c(x)] [[ Q ]]
c does not intersect b or free names of P ; and c is not a or in free names of Q.

Theorem 23. The encoding from L S,M,C,NO,L into L S,M,C,NO,J is valid.

Proof. The proof technique is identical to Theorem 2.

Interestingly there are encodings that do not require channel names for the language that are dataspace-based and no-matching. Consider the following encoding from L S,M,D,NO,J to L S,M,D,NO,L that is the identity of all forms except the split and join as follows:

[[ [ a ] P ]] def = [(x)] [ a ] [[ P ]] [[ [(x 1 ) | . . . | (x i )] Q ]] def = (ν c)([ c 1 | . . . | c i ] [(x 1 )] . . . [(x i )] [[ Q ]])
where x is not a or in the free names of Proof. The same approach is used as in Theorem 23.

The same techniques can be applied to the asynchronous and polyadic variations of the above languages.

Theorem 26. The languages L -,β,γ,NO,J and L -,β,γ,NO,L can validly encode each other.

Proof. The proof technique is identical to Theorem 2. However there are usually not encodings between joining and splitting languages. This can be illustrated by considering attempts to encode any sort of name-matching from either joining or splitting into the other. Theorem 27. There exists no valid encoding from L A,M,D,NM ,J into L -,-,-,-,L .

Proof. The proof is by contradiction. (Note that the proof assumes channels in the target language as this is more general, they are simply omitted for the data-space based languages.) Consider the processes P = [( a ) | ( b )] P and

Q 1 = [ a ] and Q 2 = [ b ] . Because P | Q 1 | Q 2 -→ √ by instantiating P = √
, then by validity of the encoding and Proposition 3 [

[ P | Q 1 | Q 2 ]] -→, now consider this reduction. It must be between R 1 = [s 1 t 1 | . . . | s i t i ] R 1
and R 2 for some s and t and R 1 and

R 2 such that R 1 | R 2 -→. Observe that R 1 | R 2 cannot be a parallel component of [[ P | Q 1 | 0 ]] or [[ P | 0 | Q 2 ]] or [[ 0 | Q 1 | Q 2 ]] because this would contradict Proposition 1. If R 1 is a top level component of [[ Q 1 ]] or [[ Q 2 ]] then [[ P ]] must exhibit some join [s( p)] R 2 that interacts with R 1 because otherwise [[ 0 | Q 1 | Q 2 ]] -→ which contradicts
[ P | σQ 1 | Q 2 ]] or [[ P | Q 1 | σQ 2 ]] or [[ P | σQ 1 | σQ 2 ]] would reduce in contradiction with Proposition 1. Further, because [s( p)] R 2 must test names from both [[ Q 1 ]] and [[ Q 2 ]] then R 1 must come from only the encoding [[ Q 1 | Q 2 ]]
Q 1 = [( a )] Q 1 and Q 2 = [( b )] Q 2 .
These results show that once name-matching (or intensionality) is in play it is no longer possible for splitting or joining languages to encode one another. Corollary 9. There exists no valid encoding from L A,M,D,I,J into L -,-,-,-,L .

Corollary 10. There exists no valid encoding from L A,M,D,I,L into L -,-,-,-,J .

Thus although there are some languages where a difference only of joining or splitting prove equally expressive, in general different forms of coordination usually indicate differences in expressive power.

Conclusions

In the theme of Barnhard Steffen's work this paper demonstrates expressiveness of different approaches to workflow coordination and their relation to other language features. This paper formalises that increases in coordination always correspond to increases in expressive power: both joining and splitting languages are strictly more expressive than binary languages. However, this expressive power does not allow coordination to encode other aspects of communication; increasing coordination does not allow encoding of other features unless they could already be encoded.

This formalizes that languages using Join Calculus style joins such as general rendezvous calculus, and m-calculus cannot be validly encoded into binary languages, regardless of other features. Although there exist approaches to encoding from these kinds of languages into π-calculus, these often do not meet the criteria for a valid encoding used here. A common approach [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF] Even ordering the channel names to prevent this can be shown to fail under substitutions. However, there are different forms of encodings between such calculi and π-calculi that do not meet the criteria used here [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF][START_REF] Peters | Translational expressiveness: comparing process calculi using encodings[END_REF]. The interesting cases are where joining calculi are encoded into π-calculi. Those in [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF] still suffer the problem above for the criteria used here although they are not an issue for the full abstraction result obtained. In [START_REF] Peters | Translational expressiveness: comparing process calculi using encodings[END_REF] the author asserts the existence of an encoding from Join Calculus into a π-calculus with the same communication paradigm as L A,M,C,N ,B here. However, they choose a different instantiation of Gorla's encoding criteria to here, opting for a non-reduction-sensitive equivalence relation. These different choices in the formal relations mean the results do not quite conflict with those here, instead illustrating the impact of different encoding criteria. This aligns with other results [START_REF] Peters | On distributability in process calculi[END_REF] where it is shown that the communication primitives of joins cannot be encoded into the communication primitives of π-calculi under different definitions of encoding.

That a language with coordination degree n cannot be encoded into a language with coordination degree less than n aligns with some recent results. Laneve and Vitale considered "synchronization" from a perspective that appears similar but is in fact rather different [START_REF] Laneve | The expressive power of synchronizations[END_REF]. They consider languages to have n-join forms where n is the number of inputs a process can have. Thus, [a 1 (x 1 ) | . . . | a i (x i )] P has an i-join. They then show that an n-join language cannot be encoded into an (n -1)-join language, this agrees with the results here. (Indeed, the results here generalise this by considering both joining and splitting.) They further show that if mixed "joins" are allowed that can contain both inputs and outputs (e.g. [a(x) | b c ] P ) then any n-join language can be encoded into a 3-join language. However, in doing this the number of processes that must coordinate to perform the encoded reduction increases, i.e. the coordination degree must increase. This further reinforces the results here.

Fig. 1 .

 1 Fig. 1. Syntax of Languages.

P

  , Q, R ::= 0 | (νa)P | P |Q | * P | if s = t then P else Q | √ | OutP roc | InP roc .

Proof.

  By contradiction, assume that [[ S ]] -→ T , for some S -→ / . By operational correspondence, there exists an S such that S =⇒ S and T =⇒ T [[ S ]]; but the only such S is S itself. Since is reduction-sensitive and since [[ S ]] = [[ S ]] -→, then T -→ T . Again by operational correspondence T =⇒ T [[ S ]], and so on; thus, [[ S ]] -→ T =⇒ T =⇒ T =⇒ T -→ . . ., in contradiction with divergence reflection (since S -→ / implies S -→ / ω ).

  and [[ block(S 1 ) | block(S 2 ) ]] can report success, it must be the case that [[ S 1 | S 2 ]] -→. This can only happen by interaction between [[ S 1 ]] and [[ S 2 ]]. If this was not the case, we would have [[ S 1 | block(S 2 ) ]] -→ or [[ block(S 1 ) | S 2 ]] -→ or [[ block(S 1 ) | block(S 2 ) ]] -→, in violation of Proposition 1: indeed S 1 | block(S 2 ) -→ / because S 1 -→ / , block(S 2 ) -→ / and block(S 2 ) cannot interact with S 1 . Similar reasoning holds for block(S 1 ) | S 2 and block(S 1 ) | block(S 2 ).

  z and sends it to the encoded input. The encoded input creates a fresh name x and sends it to the encoded output along channel name z. The encoded output now knows it has communicated and evolves to [[ P ]] in parallel with the original a sent to the encoded input along channel name x. When the encoded input receives this it can evolve to [[ Q ]]. The joining version is similar except the join

Theorem 4 .

 4 There exists no valid encoding from L S,M,D,NM ,J into L A,M,D,NM ,J . Proof. The proof is by contradiction. Consider two processes P = [(x)] if x = b then √ and Q = [ a ] Q where a = b and Q ⇓. Because P | Q -→ by validity of the encoding and Proposition 3 it follows that [[ P | Q ]] -→ and this must be between some R 1 = [ m ] (for some m) and R 2 . (This can be obtained by induction over the derivation tree for [[ P | Q ]] -→ R.) Observe that R 1 | R 2 cannot be a parallel component of either [[ P ]] or [[ Q ]]because then by Proposition 1 either P or Q would reduce and this is not the case. If R 1 is a top-level component of [[ P ]] then [[ P ]] must also include a join because otherwise there would be no join in [[ P ]] that can bind some name(s) to ϕ [[ ]] x = x and name invariance or success sensitiveness would be shown to fail (i.e. P | Q -→ if a = b then √ | Q and {b/a}if a = b then √ | Q ⇓ while C N | ([[ P ]], [[ Q ]]) =⇒ does no inputs on any part of [[ P ]] and so must always or never succeed regardless of interaction with [[ Q ]]). Because the target language is asynchronous, no output can block any join and so [[ P ]] must contain an unblocked join that must include an input pattern ( n ) for some n = m. Otherwise if the join was only [(x 1 ) | . . . | (x i )] R for some R then [[ P | . . . | P ]] for i instances of P would reduce while P | . . . | P does not, contradicting Proposition 1. It follows that [[ Q ]

1 .

 1 If d = m and d = n then consider [[ P | Q | P ]]. After at least the reduction R 1 | R 2 -→ then d must be available from the reduct R of [[ P | Q ]]. Now consider C N | ([[ P | Q ]], [[ P ]]) after the reduction [[ P | Q ]] -→ R and the two top-level outputs: d available from R, and m from [[ P ]]. Clearly the join that would bind d to some name in x (to be tested in the conditional if x = b) cannot ensure binding to d and could instead bind to m. Conclude because d = m and without the name d being communicated to [[ P ]] the conditional if x = b can be made to be false when it should be true via substitutions such as {a/b} and this contradicts either name invariance or success sensitiveness. 2. If d = n then this fails name invariance or success sensitiveness (by P | Q -→ if a = b then √ | Q and {b/a}if a = b then √ | Q ⇓); or d must be bound to some name in x as in the previous case. 3. If d = m then consider where d appears in [[ Q ]].

  would always diverge or never diverge regardless of interaction with [[ P ]] and this contradicts divergence reflection or operational correspondence. Thus [[ Q ]] must include a top-level join and further it must include an input pattern ( n ) for some n = m (reasoning as above for R 1 in [[ P ]]). Otherwise if the join was only [(z 1 ) | . . . | (z i )] R for some z and R then [[ Q | . . . | Q ]] for i instances of Q would reduce while Q | . . . | Q does not contradicting Proposition 1. Consider when Q = if a = b then Ω and the substitution σ = {b/a}. Clearly P | σQ | Q -→ S where either: S -→ ω and S ⇓; or S -→ / ω and S ⇓. Now consider the reduction [

Theorem 5 .

 5 would reduce which contradicts Proposition 1). If this reduction is the initial one between [[ P ]] and [[ σQ ]] then the output n must now be available in R because otherwise the reduct of [[ σQ ]] would be unable to reduce further and this would contradict operational correspondence (because P | σQ -→ ω while R -→ / ω ). However, this n can now reduce with [[ Q ]] instead of [[ σQ ]], which leads to R ⇓ and R -→ / ω which contradicts operational correspondence via lack of divergence of R . There exists no valid encoding from L S,M,D,NM ,L into L A,M,D,NM ,L .

Theorem 6 .

 6 There exists no valid encoding from L A,P,D,NO,B into L A,M,D,NO,J . Proof. The proof is by contradiction, assume there exists a valid encoding [[ • ]]. Consider the L A,P,D,NO,B processes P = [ a, b ] and Q = [(x, y)] √ . Clearly it holds that P | Q -→ √ and so [[ P | Q ]] ⇓ and [[ P | Q ]] -→ by validity of the encoding and Proposition 3. Now consider the reduction [[ P | Q ]] -→.The reduction must be of some top-level component of[[ P ]] and [[ Q ]] (because of Proposition 2) of the form [ a 1 ] | . . . | [ a i ] | [(x 1 ) | . . . | (x i )]R for some a and x and i and R . Now consider the process whose encoding produces [(x 1 ) | . . . | (x i )] R at top-level, assume Q although the results do not rely on this assumption. Observe that no [ a j ] are also from the encoding of Q because it follows that the encoding of i instances of Q in parallel will reduce,i.e. [[ Q | . . . | Q ]] -→, while Q | . . . | Q -→ /and this yields contradiction. Now consider two fresh processes S = [ c 1 , . . . , c k ] and T = [(z 1 , . . . , z k )] 0 where k = 2. By validity of the encoding, since S | T -→ 0 and S -→ / and T -→ / , it follows that [[ S | T ]] -→ (by Proposition 3) and [[ S ]] -→ / and [[ T ]] -→ / . As above, the reduction [[ S | T ]] -→ must be of the form [ d 1 ] | . . . | [ d k ] | [(z 1 ) | . . . | (z k )] T for some d and z and k and T . Again, assume that [[ T ]] has [(z 1 ) | . . . | (z k )] T at top-level (although the result does not rely on this assumption). Now [[ S ]] must contain at least one [ d j ] (since otherwise [[ T ]] -→ in violation of Proposition 1), and this must be at toplevel by Proposition 2. Conclude by showing that [[ S | . . . | S | Q ]] -→ while S | . . . | S | Q -→ / for i instances of S in contradiction with Proposition 1.

Theorem 10 .Corollary 4 .

 104 There exists no valid encoding from L A,M,C,NO,B into L A,M,D,NO,J . Proof. The proof is by contradiction and uses a very similar to that of Theorem 6. The differences are to use the L A,M,C,NO,B processes P = [a b ] and Q = [a(x)] √ initially, and then S = [c b ] and T = [c(z)] 0 where c = a. Theorem 11. There exists no valid encoding from L A,M,C,NO,B into L A,M,D,NO,L . Proof. The proof is by contradiction and very similar to that of Theorem 7, the main differences are to consider the L A,M,C,NO,B processes P = [a b ] and Q = [a(x)] √ , and then S = [c d ] and T = [c(z)] 0. If there exists no valid encoding from L α1,β1,C,δ1,B into L α2,β2,D,δ2,B , then there exists no valid encoding from L α1,β1,C,δ1, into L α2,β2,D,δ2, .Proof. The technique in Theorems 10 & 11 apply to all monadic languages (the addition of name-matching can be proved using the techniques as in Theorem 4). For the polyadic no-matching setting the results above holds by observing that the arity must remain fixed for an encoding, i.e. [[ [a b 1 , . . . , b i ] ]] is encoded to inputs/outputs all of some arity j. If the arity is not uniform then the encoding fails either Proposition 1 (by showing that the reduction [[ [a(x)] 0 | [a b 1 , b 2 ] ]] -→ must occur) or divergence reflection (by show-

Theorem 14 .

 14 There exists no valid encoding from L A,M,D,I,B into L -,-,-,δ,J where δ = I. Proof. The proof is by contradiction. Assume there exists a valid encoding [[•]] from L A,M,D,I,B into L α,β,γ,δ,J for some α and β and γ and δ where δ = I. Consider the encoding of the processes P = [( a )] P and Q = [ a ] . Because P | Q -→ then by Proposition 3 [[P | Q]] -→. Now define k = mip([[P | Q]]) and define σ = {b 1 • . . . • b k+1 /a}. Observe that σ(P | Q) -→ and so [[σ(P | Q)]] -→ by Proposition 3, and that the reduction [[σ(P | Q)]] -→ can match at most k names because k ≥ the maximum possible patterns of any join in [[σ(P | Q)]] by Lemma 4 and δ = I. Therefore, there must exist at least one name b j (but assume only b j for simplicity here) that is not being tested for equality either by a name match or channel name in the reduction [[σ(P | Q)]] -→. Define P = [ m ] and ρ = {m/b j , b j /m}. Now since b j is not tested for equality in the reduction [[σP | σQ]] -→ it follows that [[ρσP | σQ]] -→. Conclude by showing that * (ρσP | σQ) does not reduce (or diverge) while because [[ρσP | σQ]] -→ it follows that [[ * (ρσP | σQ)]] -→ ω in violation of divergence reflection. Theorem 15. There exists no valid encoding from L A,M,D,I,B into L -,-,-,δ,L where δ = I.

Theorem 16 .

 16 There exists no valid encoding from L A,M,D,NM ,B into L α,β,D,NO,J . Proof. The proof is by contradiction, assume there exists a valid encoding [[ • ]]. Consider the L A,M,D,NM ,B processes P = [ a ] and Q = [( a )] ([ b ] | √ ). Observe that P | Q -→ and P | Q ⇓ and so [[ P | Q ]] -→ and [[ P | Q ]] ⇓ by Proposition 3 and validity of the encoding. Now consider the substitution σ = {c/a}, it follows that P | σQ -→ / and so [[ P | σQ ]] -→ / by Proposition 1.

2

 2 and because no other mechanism can prevent interaction then because [[ P | ρσQ ]] -→ (by Proposition 3) it follows that [[ P | σQ ]] -→ in violation of Proposition 1. Theorem 17. There exists no valid encoding from L A,P,D,NM ,B into L α,β,γ,NO,J . Proof. The proof is by contradiction, assume there exists a valid encoding [[ • ]]. If γ = D then the proof of Theorem 16 applies, so the rest of this proof shall assume γ = C. Consider the L A,P,D,NM ,B processes P = [ a, b ] and Q = [( a , b )] Q . Observe that P | Q -→ and so [[ P | Q ]] -→ by Proposition 3 and validity of the encoding. The reduction [[

Corollary 6 .

 6 j and contradiction could be shown because inv(σ)ρP | Q -→ / . Finally, because the join and all the splits involved in the reductions [[ P | Q ]] -→ must be at top-level by Proposition 2, conclude by observing that [[ σP | ρP | Q | ρσQ ]] -→ because all the components required for interaction are at top-level and because [[ Q | ρσQ ]] provides all the outputs (or inputs) required for the inputs (or outputs) of σP and ρP . However, because σP | ρP | Q | ρσQ -→ / this contradicts Proposition 1. The next two results are the splitting version of the two theorems above. Theorem 18. There exists no valid encoding from L A,M,D,NM ,B into L α,β,D,NO,L .Proof. The same technique as in Theorem 16 can be applied here.Theorem 19. There exists no valid encoding from L A,P,D,NM ,B into L α,β,γ,NO,L .Proof. The same technique as in Theorem 17 can be applied here. If there exists no valid encoding from L α1,β1,γ1,NM ,B into L α2,β2,γ2,δ,B , then there exists no valid encoding from L α1,β1,γ1,NM , into L α2,β2,γ2,δ, .Proof. The joining cases are covered by Theorems 16 & 17 and the splitting byTheorems 18 & 19.

Theorem 21 .

 21 If Cd(L 1 ) > Cd(L 2 ) then there exists no valid encoding[[ • ]] from L 1 into L 2 .Proof. By contradiction, assume there is a valid encoding[[ • ]]. Fix N and pick i processes S 1 to S i where i = Cd(L 2 ) + 1 and N = fn(S j ) for j ∈ {1, . . . , i} such that all these processes must coordinate to yield a reduction and yield success. That is: S 1 | . . . | S i -→ √ but not if any S j (for 1 ≤ j ≤ i) is replaced by block(S j ). By validity of the encoding and Proposition 3 it must be that[[ S 1 | . . . | S i ]] ⇓ and [[ S 1 | . . . | S i ]] -→. By compositionality of the encoding [[ S 1 | . . . | S i ]] = C S = C N | ([[ S 1 ]], C N | (. . . , C N | ([[ S i-1 ]], [[ S i ]]))). Now consider the reduction [[ S 1 | . . . | S i ]] -→ thatcan be at most between i-1 processes by the coordination degree of L 2 . If the reduction does not involve some process [[ S j ]] then it follows that [[ S 1 | . . . | S j-1 | block(S j ) | S j+1 | . . . | S i ]] -→ (by replacing the [[ S j ]] in the context C S with [[ block(S j ) ]]). By construction of S 1 | . . . | S i and Cd(L 2 ) < i there must exist some such S j . However, this contradicts the validity of the encoding since S 1 | . . . | S j-1 | block(S j ) | S j+1 | . . . | S i -→ / . The only other possibility to prevent reduction of [[ S 1 | . . . | S j-1 | block(S j ) | S j+1 | . . . | S i ]] is if [[ block(S j ) ]] blocks the reduction by blocking some [[ S k ]]. This can only occur when [[ S k ]] is either underneath an interaction primitive (e.g. [s t ] [[ S k ]]) or inside a conditional (e.g. if s = t then [[ S k ]] where s = t). Both require that [[ S k ]] not be top-level in C S , which can be proven contradictory by Proposition 2.

Theorem 25 .

 25 [[ P ]]; and c does not intersect the free names of [[ Q ]]. Again the key idea is to reverse the direction of communication, only now no attempt is made to maintain the relation of which encoded process initiated communication with which. This turns out not to be a concern since the split that represents the encoded join ensures sufficient encoded outputs are available before reduction, although the actual binding of names may not match that initial reduction. For example, [[ [ a ] | [ b ] ]] may begin a reduction with [[ [(x) | (y)] P ]], i.e. [[ [ a ] | [ b ] | [(x) | (y)] P ]] -→ S and similarly, [[ [ c ] ]] and [[ [(z)] Q ]] may begin with a reduction [[ [ c ] [(z)] Q ]] -→ T . Despite these initial reductions, it is still possible for S | T =⇒ {b/x, c/y}P | {a/z}Q. This may seem unusual, but despite this lack of control over where the actual names are communicated after the initial reductions of an encoded join, this still meets the criteria for a valid encoding. Theorem 24. The encoding from L S,M,D,NO,J into L S,M,D,NO,L is valid. Proof. The proof technique is identical to Theorem 2. There exists a valid encoding from L S,M,D,NO,L into L S,M,D,NO,J .

Proposition 1 .

 1 Now by Proposition 3 and considering the substitution σ = {c/a, c/b} it must be that [s( p)] R 2 tests equality of some translated names of both ϕ [[ ]] (a) and ϕ [[ ]] (b) because otherwise one of [

  and not from either of [[ Q 1 ]] and [[ Q 2 ]] alone. However, by considering S = [(x)] S 1 | [(y)] S 2 and the fact thatS | Q 1 | Q 2 -→ and S | Q 1 | 0 -→ and S | 0 | Q 2 -→ it follows that either: both [[ Q 1 ]] and [[ Q 2 ]] must exhibit a top-level split, or [[ Q 1 | Q 2 ]] must exhibit more than one top-level split. In both cases this yields a contradiction via [[S | P | Q 1 | Q 2 ]] with S 1 =√ and P = Ω by violating either success sensitiveness or operational correspondence (as in concluding Theorem 4).Therefore, it must be thatR 1 is a top-level component of [[ P ]], so consider the process S = [(z)] S such that Q 1 | S -→ and [[ Q 1 | S ]] -→ (by instantiating S = √ and Proposition 3). Observe that [[ Q 1 ]] interacts with [[ P ]] via some [s j ( p)] Q 1 (there may be many such, but assume one for simplicity because the following can be proved for all of them). Now consider the reduction[[ Q 1 | S ]] -→: -If it is via the same [s j ( p)] Q 1 thatinteracts with [[ P ]] then there must be some [. . . | s j t | . . .] T in [[ S ]] such that Match( t, p) is defined. Observe that this must not rely on equality/matching of any names that depend upon a because otherwise the substitution σ = {c/a} would prevent the reduction of [[ Q 1 | σS ]] yet Q 1 | σS -→ and so this yields contradiction via Proposition 3. However, because no name in [s j ( p)] Q 1 depends upon a it follows that [[ P | σQ 1 | Q 2 ]] -→ which contradicts Proposition 1. -Otherwise it must be that the reduction is via some different input or output in [[ Q 1 ]]. However, then contradiction can be achieved via success sensitive-ness or divergence reflection in a similar manner to the conclusion of Theorem 4 by instantiating P = √ and S = if z = a then Ω and considering [[ P | Q 1 | Q 2 | S | σQ 1 ]].Theorem 28. There exists no valid encoding from L A,M,D,NM ,L into L -,-,-,-,J .Proof. The proof is by contradiction in a similar manner to Theorem 27 by starting with the processes P = [ a | b ] and

  used in such encodings is to encode joins by[[ [m(x) | n(y)] P ]] = m(x).n(y).[[ P ]], however this can easily fail operational correspondence, or success sensitivity. For example considerP 1 = [c 1 (w) | c 2 (x)] √ and P 2 = [c 2 (y) | c 1 (z)] Ω and Q = c 1 a | c 2 b . Together P 1 | P 2 | Q can either report success or diverge, but their encoding [[ P 1 | P 2 | Q ]] can deadlock.

  Monadic communication is polyadic communication with all tuples of arity one. Dataspace-based communication is channel-based communication with all k-ary tuples communicating with channel name k. All name-matching communication is intensional communication with-

out any compounds, and no-matching capability communication is both without any compounds and with only binding names in patterns. Lastly, binary communication is: joining communication with all joining inputs having only a single input pattern, and splitting communication with all splitting outputs having only a single output term.