Thomas Given-Wilson

Axel Legay

On the Expressiveness of Joining

The expressiveness of communication primitives has been explored in a common framework based on the π-calculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channel-based), and pattern-matching (binding to a name vs testing name equality vs intensionality). Here another dimension coordination is considered that accounts for the number of processes required for an interaction to occur. Coordination generalises binary languages such as π-calculus to joining languages that combine inputs such as the Join Calculus and general rendezvous calculus. By means of possibility/impossibility of encodings, this paper shows coordination is unrelated to the other features. That is, joining languages are more expressive than binary languages, and no combination of the other features can encode a joining language into a binary language. Further, joining is not able to encode any of the other features unless they could be encoded otherwise.

Introduction

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 picalculi[END_REF][START_REF] Busi | On the Expressiveness of Linda Coordination Primitives[END_REF][START_REF] De | 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]. 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, namely: synchronism, asynchronous versus synchronous; arity, monadic versus polyadic; communication medium, shared dataspaces versus channels; and pattern-matching, purely binding names versus name equality versus intensionality. These features are able to represent many popular calculi [START_REF] Gorla | Comparing Communication Primitives via their Relative Expressive Power[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF] such as: asynchronous or synchronous, monadic or 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]; Linda [START_REF] Gelernter | Generative communication in Linda[END_REF]; Mobile Ambients [START_REF] Cardelli | Mobile Ambients[END_REF]; µKlaim [START_REF] De | KLAIM: A Kernel Language for Agents Interaction and Mobility[END_REF]; semantic-π [START_REF] Castagna | Semantic Subtyping for the Pi-calculus[END_REF]; and asymmetric concurrent pattern calculus [START_REF] Given-Wilson | An Intensional Concurrent Faithful Encoding of Turing Machines[END_REF]. Also the intensional features capture significant aspects of Concurrent Pattern Calculus (CPC) [START_REF] Given-Wilson | Concurrent Pattern Calculus[END_REF][START_REF] Given-Wilson | A Concurrent Pattern Calculus[END_REF] and variations [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | An Intensional Concurrent Faithful Encoding of Turing Machines[END_REF]; and Psi calculi [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF] and sorted Psi calculi [START_REF] Borgström | A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract)[END_REF].

Typically interaction in process calculi is a binary relation, where two processes interact and reduce to a third process. For example in π-calculus the interaction rule is m a .P | m(x).Q -→ P | {a/x}Q .

Here the processes m a .P and m(x).Q interact and reduce to a new process P | {a/x}Q. However, there are process calculi that are not binary with their interactions. For example, Concurrent Constraint Programming (CCP) has no direct interaction primitives, instead interactions are a single process and the constraint environment [START_REF] Saraswat | The Semantic Foundations of Concurrent Constraint Programming[END_REF]. In the other direction Join Calculus [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF], 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] allow any number of processes to join in a single interaction.

This paper abstracts away from specific calculi in the style of [START_REF] Gorla | Comparing Communication Primitives via their Relative Expressive Power[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF] to provide a general account of the expressiveness of the coordination of communication primitives. Here coordination can be either binary between an explicit input and output (as above), or joining where the input may interact with unbounded outputs (but at least one). For example, consider the reduction

m a .P 1 | n b .P 2 | (m(x) | n(y)) ⊲ Q -→ P 1 | P 2 | {a/x, b/y}Q
where the join ⊲ interacts when the two outputs m a and n b can match the two parts of the input m(x) and n(y), respectively.

By adding the dimension of coordination, the original 24 calculi of [START_REF] Gorla | Comparing Communication Primitives via their Relative Expressive Power[END_REF][START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF] are here expanded to 48. This paper details the relations between these calculi, with the following key results.

Joining cannot be encoded into a binary language. This is formalised via the coordination degree of a language that is the least upper bound on the number of processes required to yield a reduction. In general a language with a greater coordination degree cannot be encoded into a language with a lesser coordination degree. That is, the joining languages with ∞ coordination degree cannot be encoded into the binary languages with coordination degree 2.

Synchronous languages that can be encoded into asynchronous languages in the binary setting can also do so in the joining setting. In the other direction synchronous languages cannot be encoded into asynchronous languages that differ only by the addition of joining over binary communication.

Polyadic languages that cannot be encoded into monadic languages in the binary setting cannot be encoded into monadic languages simply with the addition of joining. Indeed, coordination is unrelated to arity despite being similar in having a base case (monadic/binary) and an unbounded case (polyadic/joining).

Channel-based languages cannot be encoded into dataspace-based languages by the addition of joining unless they could be encoded already. In the other direction, the addition of channels does not allow a joining language to be encoded into a binary language.

Intensionality cannot be encoded by joining regardless of other features, this result mirrors the general result that intensionality cannot be represented by any combination of the first four features [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF]. Name-matching cannot be encoded by joining into a language without any name-matching, despite the possibility of matching unbounded numbers of names via joining on an unbounded number of channels.

Overall, the results of this paper prove that joining is orthogonal to all the other features, and that joining languages are strictly more expressive than binary languages.

The structure of the paper is as follows. Section 2 introduces the 48 calculi considered here. Section 3 revises the criteria used for encoding and comparing calculi. Section 4 defines the coordination degree of a language and formalises the relation between binary and joining languages. Section 5 considers the relation between synchronism and coordination. Section 6 relates arity and coordination. Section 7 presents results contrasting communication medium with coordination. Section 8 formalises the relation between pattern-matching and coordination. Section 9 concludes, discusses future and related work, and provides some motivations for intensional calculi.

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 (the reference framework) and adapts them when necessary to cope with different features. With the exception of the joining constructs this is a repetition of prior definitions from [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF].

Assume a countable set of names N ranged over by a, b, c, . . .. Traditionally in π-calculus-style calculi names are used for channels, input bindings, and output data. However, here these are generalised to account for structure. Then, define the terms (denoted with s, t, . . .) to be s, t ::= a | s • t. Terms consist of names such as a, or of compounds s • t that combines two terms into one. The choice of the • as compound operator is similar to Concurrent Pattern Calculus, and also to be clearly distinct from the traditional comma-separated tuples of polyadic calculi.

The input primitives of different languages will exploit different kinds of input patterns. The nonpattern-matching languages will simply use binding names (denoted x, y, z, . . .). The name-matching patterns, denoted m, n, o, . . . and defined by m, n ::= x | a consist of either a binding name x, or a name-match a . Lastly the intensional patterns (denoted p, q, . . .) will also consider structure and are defined by p, q ::= m | p • q. The binding names x and name-match a are contained in m from the name-matching calculi, the compound pattern p • q combines p and q into a single pattern, and are left associative. The free names and binding names of name-matching and intensional patterns are as expected, taking the union of sub-patterns for compound patterns. Note that an intensional pattern is well-formed if and only if all binding names within the pattern are pairwise distinct. The rest of this paper will only consider well-formed intensional patterns.

The (parametric) syntax for the languages is:

P, Q, R ::= 0 | OutProc | InProc | (νa)P | P|Q | if s = t then P else Q | * P | √ .
The different languages are obtained by replacing the output OutProc and input InProc with the various definitions. The rest of the process forms are as usual: 0 denotes the null process; restriction (νa)P restricts the visibility of a to P; and parallel composition P|Q allows independent evolution of P and Q.

The if s = t then P else Q represents conditional equivalence with if s = t then P used when Q is 0.

The * P represents replication of the process P. Finally, the √ is used to represent a success process or state, exploited for reasoning about encodings as 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]. This paper considers the possible combinations of five features for communication: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (dataspacebased vs channel-based), pattern-matching (simple binding vs name equality vs intensionality), and coordination (binary vs joining). As a result there exist 48 languages denoted as Λ s,a,m,p,b whose generic element is denoted as L α,β,γ,δ,ǫ where:

• α = A for asynchronous communication, and α = S for synchronous communication.

• β = M for monadic data, and β = P for polyadic data.

• γ = D for dataspace-based communication, and γ = C for channel-based communications.

• δ = NO for no matching capability, δ = NM for name-matching, and δ = I for intensionality.

• ǫ = B for binary communication, and ǫ = J for joining communication. For simplicity a dashwill be used when the instantiation of that feature is unimportant.

Thus the syntax of every language is obtained from the productions in Figure 1. The denotation • represents a sequence of the form • 1 , • 2 , . . . , • n and can be used for names, terms, and input patterns.

As usual a(. . . , x, . . .).P and (ν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. Lastly, an input is well-formed if all binding names in that input occur exactly once. This paper shall only consider well-formed inputs. Finally, the structural equivalence relation ≡ is defined by: 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 align with the communication primitives 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 aligns with 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 with the monadic/polyadic Mobile Ambients [START_REF] Cardelli | Mobile Ambients[END_REF]; and L A,P,C,NM,B with that of µKlaim [START_REF] De | KLAIM: A Kernel Language for Agents Interaction and Mobility[END_REF] or semantic-π [START_REF] Castagna | Semantic Subtyping for the Pi-calculus[END_REF]. The intensional languages do not exactly match any well-known calculi. However, the language L S ,M,D,I,B has been mentioned in [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF], as a variation of Concurrent Pattern Calculus [START_REF] Given-Wilson | Concurrent Pattern Calculus[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF], and has a 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 is very similar to pattern-matching Spi calculus [START_REF] Haack | Pattern-matching Spi-calculus[END_REF] and Psi calculi [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF], albeit without the assertions or the possibility of repeated binding names in patterns. There are also similarities between L S ,M,C,I,B and the polyadic synchronous π-calculus of [START_REF] Carbone | On the Expressive Power of Polyadic Synchronisation in π-calculus[END_REF], although the intensionality is limited to the channel, i.e. inputs and outputs of the form s(x).P and s a .P respectively. For the joining languages, L A,P,C,NO,J represents Join Calculus [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF], 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.

P | 0 ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R if s = t then P else Q ≡ P s = t if s = t then P else Q ≡ Q s t P ≡ P ′ if P = α P ′ (νa)0 ≡ 0 (
Remark 2.1. The languages Λ s,a,m,p,ǫ can be easily ordered; in particular

L α 1 ,β 1 ,γ 1 ,δ 1 ,ǫ 1 can be encoded into 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 .
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.

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 without any compounds, and nomatching 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.

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 is in play. However, 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], and indeed captures many1 of the languages here [START_REF] Given-Wilson | Pattern Matching and Bisimulation[END_REF]. For the joining languages the techniques used in [START_REF] Boreale | Bisimulations in the Join-Calculus[END_REF] can be used for the no-matching joining languages, with the techniques of [START_REF] Given-Wilson | Pattern Matching and Bisimulation[END_REF] used to extend intensionality 2 .

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

σ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 the name-match syntax can be applied to any term as follows

x def = x and (s • t) def = s • t .
Given a substitution σ and a process P, denote with σP the (capture-avoiding) 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 | Barendregts Variable Convention in Rule Inductions[END_REF].

Interaction between processes is handled by matching some terms t with some patterns p, and possibly also equivalence of channel-names. This is handled in two parts, the match rule {t//p} of a single term t with a single pattern p to create a substitution σ. This is defined as follows:

{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 unification of σ 1 and σ 2 . Observe that since patterns are well-formed, the substitutions of components will always have disjoint domain. Otherwise the match is undefined.

The general case is then the poly-match rule Match( t; p) that determines matching of a sequence of terms t with a sequence of patterns p, that is 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 {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 disjoint domain by well-formedness of inputs.) Otherwise the poly-match rule is undefined, for example when a single match fails, or the sequences are of unequal arity.

Interaction is now defined by the following axiom for the binary languages:

s t .P | s( p).Q -→ P | σQ Match( t; p) = σ
and for the joining languages:

s 1 t 1 .P 1 | . . . | s k t k .P k | (s 1 ( p 1 ) | . . . | s k ( p k )) ⊲ Q -→ P 1 | . . . | P k | σQ σ = {i∈1...k} Match( t i ; p i ) .
In both axioms, the Ps are omitted in the asynchronous languages, and the s's are omitted for the dataspace-based languages. The axioms state that when the poly-match of the terms of the output(s) t match with the input pattern(s) of the input p (and in the channel-based setting the output and input pattern(s) are along the same channels) yields a substitution σ, then reduce to (P(s) in the synchronous languages in parallel with) σ applied to Q.

The general reduction relation -→ includes the interaction axiom for the language in question as well as the following three rules:

P -→ P ′ P | Q -→ P ′ | Q P -→ P ′ (νa)P -→ (νa)P ′ P ≡ Q Q -→ Q ′ Q ′ ≡ P ′ P -→ P ′ .
The reflexive transitive closure of -→ is denoted by =⇒.

Lastly, for each language let ≃ denote a reduction-sensitive reference behavioural equivalence for that language, e.g. a barbed equivalence. For the non-intensional 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 other joining languages the techniques used in [START_REF] Boreale | Bisimulations in the Join-Calculus[END_REF] can be used for the no-matching joining languages, with the techniques of [START_REF] Given-Wilson | Pattern Matching and Bisimulation[END_REF] used to extend intensionality3 .

Encodings

This section recalls the definition of valid encodings as well as some useful theorems (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 validity of such criteria in developing expressiveness studies emerges from the various works [START_REF] Gorla | Comparing Communication Primitives via their Relative Expressive Power[END_REF][START_REF] Gorla | A Taxonomy of Process Calculi for Distribution and Mobility[END_REF][START_REF] Gorla | Towards a Unified Approach to Encodability and Separation Results for Process Calculi[END_REF], that have also recently 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].

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. The translation [[ • ]] turns every term of the source language into a term of the target; 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 ϕ

[[ ]] .
Now consider only encodings that satisfy the following properties. Let a k-ary context C(• 1 ; . . . ; • k ) be a term where k occurrences of 0 are linearly replaced by the holes {• 1 ; . . . ; • k } (every one of the k holes must occur once and only once). Denote with -→ i and =⇒ i the relations -→ and =⇒ in language L i ; denote with -→ ω i an infinite sequence of reductions in L i . Moreover, let ≃ i denote the reference behavioural equivalence for language L i . Also, let P ⇓ i mean that there exists P ′ such that P =⇒ i P ′ and P ′ ≡ P ′′ | √ , for some P ′′ . 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 ).

Valid Encoding An encoding ([[

• ]], ϕ [[ ]] ) of L 1 into L 2 is
] = σ ′ [[ S ]] if σ is injective and [[ σS ]] ≃ 2 σ ′ [[ S ]] otherwise where σ ′ is such that ϕ [[ ]] (σ(a)) = σ ′ (ϕ [[ ]] (a)
) for every name a.

Operational correspondence:

• for all

S =⇒ 1 S ′ , it holds that [[ S ]] =⇒ 2 ≃ 2 [[ S ′ ]]; • for all [[ S ]] =⇒ 2 T ,

Joining vs Binary

This section considers the expressive power gained by joining. It turns out that joining adds expressive power that cannot be represented by binary languages regardless of other features. The expressive power gained by joining 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 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 joining languages is ∞ since there is no bound on the number of inputs that can be part of a join.

. . | S j-1 | 0 | S j+1 | . . . | S i -→.

The only other possibility is if [[ 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 ]]). Both require that [[ S k ]

] not be a top level is C S , which can be proven contradictory by i -1 applications of Proposition 3.2.

Corollary 4.2.

There exists no valid encoding from L α,β,γ,δ,J into L α,β,γ,δ,B .

In the other direction the result is ensured by Remark 2.1. Thus for any two languages who differ only by one being binary and the other joining, the joining language is strictly more expressive than the binary language.

Joining and Synchronicity

This section considers the relation between joining and synchronicity. It turns out that the two are orthogonal and do not influence the other's expressiveness.

It is sufficient to consider the languages L A,M,D,NO,J and L A,P,D,NO,J and L A,M,D,NM,J . The other asynchronous joining languages can encode their synchronous joining counterparts in the usual manner [START_REF] Honda | An object calculus for asynchronous communication[END_REF]. For example, the encoding from L S ,M,C,NO,B into L A,M,C,NO,B given by

[[ n a .P ]] def = (νz)(n z | z(x).(x a | [[ P ]])) [[ n(a).Q ]] def = (νx)n(z).(z x | x(a).[[ Q ]])
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 . The joining version is similar except the join 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 5.1. Given a L S ,M,C,NO,J input P and output Q then

[[P]] | [[Q]] -→ if and only if P | Q -→. Lemma 5.2. If P ≡ Q then [[P]] ≡ [[Q]]. Conversely, if [[P]] ≡ Q then Q = [[P ′ ]
] for some P ′ ≡ P. Proof. Theorem 5.4 applies directly for all channel-based languages. The only other cases can encode channels and so use encodings of the channel-based solution above. 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].

The following results complete the formalisation that coordination is orthogonal synchronicity.

Theorem 5.6. 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 Ω (where Ω is a divergent process) and ] must also include a top level join since otherwise there would be no join in [[ P ]] that can bind some name to x and name invariance or divergence reflection would be shown to fail (i.e. ] is not able to discriminate and thus that there exist two possible reductions

Q = a .Q ′ . Since P | Q -→
P | Q -→ if a = b then Ω | Q ′ and {b/a}if a = b then Ω | Q ′ -→ ω while C N | ([[ P ]], [[ Q ]]) =⇒
[[ P | σQ | Q ]] -→ R ′ to an R ′
where either: R ′ -→ ω and R ′ ⇓; or R ′ -→ ω and R ⇓; both of which contradict divergence reflection and success sensitiveness.

Theorem 5.7. There exists no valid encoding from L S ,β,D,NO,J into L A,β,D,NO,J .

Proof. This is proved in the same manner as Theorem 5.6.

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

Joining and Arity

This section considers the relation between joining and arity. It turns out that these are orthogonal. Although there appear to be some similarities in that both have a base case (monadic or binary), and an unbounded case (polyadic or joining, respectively), these cannot be used to encode one-another. This is captured by the following result.

P | Q ]] -→.
If the reduction is of the form m | ((z)) ⊲ T ′ for some m and z and T ′ then consider the origin of

R 1 = m and R 2 = ((z)) ⊲ T ′ . If R 1 | R 2 is a reduct of [[ P ]] or [[ Q ]] then it follows that [[ P | 0 ]] or [[ 0 | Q ]]
would reduce which contradicts that P -→ and Q -→. Therefore, it must be that R 1 arises from P and R 2 from Q (or with P and Q swapped, but the result holds either way). Now replace Q with some S = (w). Otherwise if the reduction is of the form

m 1 | . . . | m i | ((z 1 ) | . . . | (z i )) ⊲ T ′
for some m and z and i and T ′ . Now consider the process whose encoding produces ((z 1 ) | . . . | (z i )) ⊲ T ′ , assume Q although the results do not rely on this assumption. If any m j are also from the encoding of Q then it follows that the encoding of i instances of Q in parallel will reduce, i.e. Corollary 6.2. If there exists no valid encoding from L α,P,γ,δ,B into L α,M,γ,δ,B , then there exists no valid encoding from L α,P,γ,δ,-into L α,M,γ,δ,J .

[[ Q | . . . | Q ]] -→, while Q | . . . | Q -→.
Proof. The technique in Theorem 6.1 applies to all dataspace-based languages (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 then proved via contradiction of name invariance and success sensitiveness like in Theorem 5.6). The techniques in Theorem 7.1 can more elegantly show that channel-based communication cannot solve the situation than adding them to the proof above.

Thus joining does not allow for encoding polyadicity in a monadic language unless it could already be encoded by some other means. In the other direction, the inability to encode joining into a binary language is already ensured by Corollary 4.2.

Joining and Communication Medium

This section considers the relation between joining and communication medium. Again joining turns out to be orthogonal to communication medium and neither can encode the other. The key to this is captured in the following result. ) must be able to do both of these initial reductions in any order. Now consider the process R that has performed both of these initial reductions. By operational correspondence it must be that R

= ( a 1 • . . . a i-1 • m • a i+1 . . . a k+2 ). a i . Now consider the context C N | ([[ S 2 ]], [[ • ]]) = [[ S 2 | • ]] where N = { a ∪ m}. Clearly neither C N | ([[ S 2 ]], [[ 0 ]]) -→ nor C N | ([[ S 2 ]], [[ S 4 ]]) -→
=⇒≃ [[ m | m ]] since S 2 | S 0 | S 3 =⇒ m | m .
Therefore, R must be able to roll-back the initial step with combined arity j; i.e reduce to a state that is equivalent to the reduction not occurring. (Or the initial step with arity k, but either one is sufficient as by operational correspondence R =⇒≃ [[ m | S 3 ]].) Now consider how many names are being matched in the initial reduction with combined arity j. If j < k the technique of differing on one name used in the case of j = k can be used to show that this would introduce divergence on the potential roll-back and thus contradict a valid encoding. Therefore it must be that j > k. Finally, by exploiting name invariance and substitutions like {(b 1 • . . . • b j )/a 1 } applied to S 2 and S 3 it follows that either j > k + j or both S 2 and S 3 must have infinitely many initial reductions which yields divergence.

• If the combined arity is not k then proceed like the second case above. Corollary 8.2. If there exists no valid encoding from L α,β,γ,I,B into L α,β,γ,δ,B , then there exists no valid encoding from L α,β,γ,I,-into L α,β,γ,δ,J .

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

The next result shows that name matching is insufficient to encode joining. Thus joining does not allow for encoding name-matching into a no-matching language unless it could already be encoded by some other means. In the other direction, the inability to encode joining into a binary language is already ensured by Corollary 4.2.

Conclusions and Future Work

Languages with non-binary coordination have been considered before, although less often than binary languages. It turns out that increases in coordination degree correspond to increases in expressive power. For example, an intensional binary language cannot be encoded by a non-intensional joining language. However, encodings from lower coordination degree languages into higher coordination degree languages are still dependent upon other features.

This formalises that languages like the Join Calculus, general rendezvous calculus, and m-calculus cannot be validly encoded into binary languages, regardless of other features. Despite the existing encodings from (for example) Join Calculus into π-calculus [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF] Future work along this line can consider coordination to not merely be binary or joining. Indeed, a splitting language could be one where several output terms can be combined into a split (m a | n b ) ⊲ P while inputs remain of the form m(x).Q. Further, languages could support both joining and splitting primitives for full coordination.

  νa)(νb)P ≡ (νb)(νa)P P | (νa)Q ≡ (νa)(P | Q) if a fn(P) * P ≡ P | * P . L A,-,-,-,-: OutProc ::= OUT L S ,-,-,-,-: OutProc ::= OUT.P L -,-,-,-,B : InProc ::= IN.P L -,-,-,-,J : InProc ::= (I) ⊲ P I ::= IN | I | I L -,M,D,NO,-: IN ::= (x) OUT ::= a L -,M,D,NM,-: IN ::= (m) OUT ::= a L -,M,D,I,-: IN ::= (p) OUT ::= t L -,M,C,NO,-: IN ::= a(x) OUT ::= a b L -,M,C,NM,-: IN ::= a(m) OUT ::= a b L -,M,C,I,-: IN ::= s(p) OUT ::= s t L -,P,D,NO,-: IN ::= ( x) OUT ::= a L -,P,D,NM,-: IN ::= ( m) OUT ::= a L -,P,D,I,-: IN ::= ( p) OUT ::= t L -,P,C,NO,-: IN ::= a( x) OUT ::= a b L -,P,C,NM,-: IN ::= a( m) OUT ::= a b L -,P,C,I,-: IN ::= s( p) OUT ::= s t Figure 1: Syntax of Languages.

Theorem 4 . 1 .

 41 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 [[ • ]]. Pick i processes S 1 to S i where i = Cd(L 2 ) + 1 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) isreplaced by the null process 0. By validity of the encoding it must be that [[ S 1 | . . . | S i ]] -→ and [[ S 1 | . . . | S i ]] ⇓. By compositionality of the encoding [[ S 1 | . . . | S i ]] = C S where C S must be of the form C N | ([[ S 1 ]], C N | (. . . , C N | ([[ S i-1 ]], [[ S i ]]) . . .)). Now consider the reduction [[ S 1 | . . . | S i ]] -→ that can 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 | 0 | S j+1 | . . . | S i ]] -→ (by replacing the [[ S j ]] in the context C S with [[ 0 ]]). 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 | .

  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 ]]

Lemma 5 . 3 .Corollary 5 . 5 .

 5355 The translation[[•]] from L S ,M,C,NO,J into L A,M,C,NO,J preserves and reflects reductions.Theorem 5.4. 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 5.3. Success sensitiveness can be proved as follows: P ⇓ means that there exists P ′ and k ≥ 0 such that P -→ k P ′ ≡ P′′ | √ ; by exploiting Lemma 5.3 k times and Lemma 5.2 obtain that [[P]] -→ j [[P ′ ]] ≡ [[P ′′ ]] | √ where j can be determined from the instantiations of Lemma 5.2, i.e. that [[P]] ⇓. The converse implication can be proved similarly. If there exists a valid encoding from L S ,β,γ,δ,B into L A,β,γ,δ,B then there exists a valid encoding from L S ,β,γ,δ,J into L A,β,γ,δ,J .

  does no inputs on any part of [[ P ]] and so must always or never diverge regardless of interaction with [[ Q ]]). Thus [[ P ]] must include a top level join and further it must include an input pattern ( n ) for some n m since otherwise if the join was only ((z 1 ) | . . . | (z i ))⊲R ′ for some z and R ′ then [[ P | . . . | P ]] for i instances of P would reduce while P | . . . | P does not contradicting Proposition 3.1. It follows that [[ Q ]] must include ( m ) as part of some join under which there must be an output that is able to send at least 1 name to [[ P ]] via an output d for some d (this could be any number of names, but assume 1 here for simplicity). Now consider the name d. If d = m then [[ P ]] -→ and this contradicts validity of the encoding since P -→. If d = n then n is not bound in [[ P ]] and so it can be shown that either: this fails name invariance or divergence reflection (again by P | Q -→ if a = b then Ω | Q ′ and {b/a}if a = b then Ω | Q ′ -→ ω ); or there must be a further input in [[ P ]] that is binding as in the next case. If d m and d n then it can be shown that [[ P | Q | P ]] can reduce such that the input under consideration interacts with the m from the other [[ P ]] and this ends up contradicting operational correspondence. If R 1 arises from [[ Q ]] then it can be shown that [[ Q ]] must also include a top level join since otherwise when Q ′ = Ω then [[ Q ]] would always diverge or never diverge regardless of interaction with [[ P ]] and this contradicts divergence reflection. Thus [[ Q ]] must include a top level join and further it must include an input pattern ( n ) for some n m since 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 3.1. Now 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 ⇓. However it can be shown that the top level join in [[ Q ]

Theorem 6 . 1 .

 61 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. Now consider the reduction [[

  0 and consider [[ P | S ]]. If [[ P | S ]] -→ then this contradicts the encoding since P | S -→. Define a process T = c , it follows that S | T -→ and T | T -→. Now [[ S ]] must exhibit either an input or output since otherwise [[ S | T ]] would not reduce (or [[ T | T ]] would reduce, but this contradicts validity of the encoding). If [[ S ]] has an output then [[ S | Q ]] would reduce, contradicting that S | Q -→. Therefore, [[ S ]] must be of the form ((w 1 ) | . . . | (w i )) ⊲ S ′ for some w and i and S ′ . Conclude by showing that [[ S | P | . . . | P ]] for i instances of P reduces, while S | P | . . . | P does not.

  Now consider two fresh processes S and T such that S | T -→ with some arity that is not 2 and S -→ and T -→. It follows that [[ S | T ]] -→ (and [[ S ]] -→ and [[ T ]] -→) and [[ S | T ]] must include at least one n to do so. This n must arise from either [[ S ]] or [[ T ]], and conclude by showing that the encoding of i instances of either S or T in parallel with Q reduces, while the un-encoded processes do not.

Theorem 7 . 1 . 2 def= a 1 • 3 def= ( a 1 •

 712131 There exists no valid encoding from L A,M,C,NO,B into L A,M,D,NO,J . encoding of the processes S 0 = ((x)) ⊲ m and S 1 = a . Clearly [[S 0 | S 1 ]] -→ since S 0 | S 1 -→. There exists a reduction [[S 0 | S 1 ]] -→ that must be between a join and some outputs that have combined maximal arity k. (The combined arity is the sum of the arities of all the input-patterns of the join involved, e.g. ((a, b) | (c)) ⊲ 0 has combined arity 3.) Now define the following processes S . . . • a 2k+1 and S . . . • a 2k+1 ). m where S 2 outputs 2k + 1 distinct names in a single term, and S 3 matches all of these names in a single intensional pattern. Since S 2 | S 0 -→ it must be that [[S 2 | S 0 ]] -→ for the encoding to be valid. Now consider the maximal combined arity of the reduction [[S 2 | S 0 ]] -→. • If the arity is k consider the reduction [[S 2 | S 3 ]] -→ with the combined maximal arity j and that must exist since S 2 | S 3 -→. Now consider the relationship of j and k.

  as this would contradict Proposition 3.1. However, since S 3 and S 4 differ only by the position of one name whose tuple ϕ[[ ]] (•) does not appear in the reduction [[ S 2 | S 3 ]] -→, it follows that the reason C N | ([[ S 2 ]], [[ S 4 ]]) -→ must be due to a structural congruence difference between C N | ([[ S 2 ]], [[ S 3 ]]) and C N | ([[ S 2 ]], [[ S 4 ]]).Further, by compositionality of the encoding the difference can only be between [[ S 3 ]] and [[ S 4 ]]. Since Proposition 3.1 ensures that [[ S 3 ]] -→ and [[ S 4 ]] -→, the only possibility is a structural difference between [[ S 3 ]] and [[ S 4 ]]. Now exploiting σ = {m/a i , a i /m} such that σS 4 = S 3 yields contradiction. 2. If j k then obtain that [[ S 2 ]] must be able to interact with both combined arity k and combined arity j. That is, [[S 2 | •]] = C N | ([[S 2 ]], [[•]]) where N = { a ∪ m} and that C N | ([[S 2 ]], [[S 0 ]]) reduces with combined arity k and C N | ([[S 2 ]], [[S 3 ]]) reduces with combined arity j. Now it is straightforward, if tedious, to show that since S 0 | S 3 -→ that C N | ([[S 2 ]], [[S 0 | S 3 ]]) can perform the same initial reductions as either C N | ([[S 2 ]], [[S 0 | 0]]) or C N | ([[S 2 ]], [[0 | S 3 ]]) by exploiting operational correspondence and Proposition 3.1. Thus, it can be shown that C N | ([[S 2 ]], [[S 0 | S 3 ]]) can perform both the k combined arity reduction of [[S 2 | S 0 ]] -→ and the j combined arity reduction of [[S 2 | S 3 ]] -→. Now by exploiting the structural congruence rules it follows that neither of these initial reductions can prevent the other occurring. Thus, C N | ([[S 2 ]], [[S 0 | S 3 ]]

Theorem 8 . 3 .•Corollary 8 . 4 .

 8384 There exists no valid encoding from L A,M,D,NM,B into L α,β,γ,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 | √ ). Clearly it holds that P | Q -→ and P | Q ⇓ and so [[ P | Q ]] -→ and [[ P | Q ]] ⇓ by validity of the encoding. Now consider γ. • If γ = D then consider the substitution σ = {a/b, b/a}, it is clear that P | σQ -→ and so [[ P | σQ ]] -→, however the only possibility that this holds is when [[ σQ ]] is blocked from interacting. It is then straightforward if tedious to show that any such blocking of reduction would either imply [[ σ(P | Q) ]] -→ or σ(P | Q) -→ and thus contradict validity of the encoding. Otherwise it must be that γ = C. Now consider the reduction [[ P | Q ]] -→ that must be from the form c 1 m 1 | . . . | c i m i | (c 1 ( z 1 ) | . . . | c i ( z i )) ⊲ T 1for some c and m and z and i and T 1 . Again consider the substitution σ = {a/b, b/a}, it is clear that σP | Q -→ and so [[ σP | Q ]] -→. The only way this can occur without contradicting validity of the encoding (as in the previous case) is when there is at least one c k in the domain of some σ ′ where σ ′ (c k ) c k and [[ σP ]] ≃ σ ′ [[ P ]] by definition of the encoding. Now consider the process S = (x).S ′ , clearly P | S -→ and so [[ P | S ]] -→ as well. The reduction [[ P | S ]] -→ must be from the form d 1 n 1 | . . . | d j n j | (d 1 ( w 1 ) | . . . | d j ( w j )) ⊲ T 2 for some d and n and w and j and T 2 . Now if i = j it follows that for each k ∈ {1 . . . i} then c k = d k . However, this contradicts the validity of the encoding since there is some c k in the domain of σ ′ such that σ ′ (c k ) c k and σP | S -→ while [[ σP | S ]] -→. Otherwise it must be that i > j (otherwise if i < j then [[ P | S ]] -→) and that c k ∈ {c j+1 , . . . , c i }. Now consider when S ′ = if x = a then Ω, clearly P | S -→≡ Ω and σP | S -→≡ 0 and so [[ P | S ]] diverges and [[ σP | S ]] =⇒≃ 0. Now it can be shown that P | σP | S | Q -→ -→≡ √ while [[ P | σP | S | Q ]] ⇓ and diverges since [[ σP ]] can satisfy the first j input patterns of [[ Q ]] and [[ σP ]] the remaining ij, leaving the first j input patterns of [[ P ]] to interact with [[ S ]] and yield divergence. The only other possibility is that [[ P | σP | S | Q ]] ⇓, however this requires that T 1 check some name equivalent to if z l = a then √with l ≤ j which can be shown to contradict validity by adding another instance of P. If there exists no valid encoding from L α,β,γ,NM,B into L α,β,γ,δ,B , then there exists no valid encoding from L α,β,γ,NM,-into L α,β,γ,δ,J .

  these turn out not to meet the criteria for a valid encoding. Their general approach is to encode joins by[[ (m(x) | n(y)) ⊲ P ]] = m(x).n(y).P, however this can easily fail operational correspondence, divergence reflection, or success sensitivity. For example(c 1 (w) | c 2 (x)) ⊲ √ | (c 2 (y) | c 1 (z)) ⊲ Ω | c 1 a | c 2 bwill either report success or diverge, but its encoding can deadlock. Even ordering the channel names to prevent this can be shown to fail under substitutions.

  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

[[ σS ]

  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 . Now recall two result concerning valid encodings that are useful for later proofs. Proposition 3.1 (Proposition 5.5 from [21]). Let [[ • ]] be a valid encoding; then, S -→ / 1 implies that [[ S ]] -→ / 2 . Proposition 3.2 (Proposition 5.6 from [21]). 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.

  by validity of the encoding [[ P | Q ]] -→ and this must be between some R 1 = m for some m and R 2 . Observe that R 1 | R 2 cannot be a reduct of either [[ P ]] or [[ Q ]] since then one of them would reduce while neither P nor Q reduce and this would contradict Proposition 3.1. If R 1 arises from [[ P ]] then it can be shown that [[ P ]

  1. If j = k then the upper bound on the number of names that are matched in the reduction is 2k (when each name is matched via a distinct channel). Since not all 2k + 1 tuples of names from ϕ [[ ]] (a i ) can be matched in the reduction then there must be at least one tuple ϕ [[ ]] (a i ) for i ∈ {1, . . . , 2k + 1} that is not being matched in the interaction [[S 2 | S 3 ]] -→. Now construct S 4 that differs from S 3 only by swapping one such name a i with m: S 4 def

Perhaps all of the binary languages here, although this has not been proven.

This has not been proven as yet, however there appears no reason it should not be straightforward albeit very tedious.

This has not been proven as yet, however there appears no reason it should not be possible, and the results here rely upon the existence of an equivalence relation, not any particular one.

Acknowledgments. We would like to thank the reviewers for their constructive and helpful criticism.

Proof. The proof is by contradiction, assume there exists a valid encoding [ If the reduction is of the form m | ((z)) ⊲ T ′ for some m and z and T ′ then consider the origin of

would reduce which contradicts that P -→ and Q -→. Therefore, it must be that R 1 arises from P and R 2 from Q (or with P and Q swapped, but the result holds either way). Now replace Q with some S = c(w). Proof. The technique in Theorem 7.1 applies to all monadic languages (the addition of name-matching can be proved using the techniques as in Theorem 5.6). For the polyadic no-matching setting the result above holds by observing that the arity must remain fixed for an encoding, i.e. [[ a b 1 , . . . , b i ]] is encode to inputs/outputs all of some arity j. If the arity is not uniform then the encoding fails either operational correspondence (i.e. [[ a(x).0 | a b 1 , b 2 ]] -→) or divergence reflection as in sub-case (2) of Theorem 8.1 except here with arity instead of number of names.

Thus joining does not allow for encoding channels in a dataspace-based language unless it could already be encoded by some other means. In the other direction, the inability to encode joining into a binary language is already ensured by Corollary 4.2.

Joining and Pattern-Matching

This section considers the relations between joining and pattern-matching. The great expressive power of name matching [START_REF] Gorla | Comparing Communication Primitives via their Relative Expressive Power[END_REF] and intensionality [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF] prove impossible to encode with joining. In the other direction, joining cannot be encoded by any form of pattern-matching.

The first result is to prove that intensionality cannot be encoded by joining. Recall that since intensionality alone can encode all other features aside from joining, it is sufficient to consider L A,M,D,I,B . Theorem 8.1. There exists no valid encoding from L A,M,D,I,B into L -,-,-,δ,J where δ I.

Proof. The proof is by contradiction and similar to Theorem 7.1 of [START_REF] Given-Wilson | On the Expressiveness of Intensional Communication[END_REF]. 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


¸ois Fillastre
email: francois.fillastre@u-cergy.fr

AND Ivan Izmestiev
email: izmestiev@math.fu-berlin.de

Giona Veronelli
email: veronelli@math.univ-paris13.fr

HYPERBOLIZATION OF CUSPS WITH CONVEX BOUNDARY

We prove that for every metric on the torus with curvature bounded from below by -1 in the sense of Alexandrov there exists a hyperbolic cusp with convex boundary such that the induced metric on the boundary is the given metric. The proof is by polyhedral approximation.

This was the last open case of a general theorem: every metric with curvature bounded from below on a compact surface is isometric to a convex surface in a 3-dimensional space form.

1. Introduction 1.1. Statement of the results. Let T denote the 2-dimensional torus. A hyperbolic cusp C with convex boundary is a complete hyperbolic manifold of finite volume, homeomorphic to T × [0, +∞[, and such that the boundary ∂C = T × {0} is geodesically convex. By the Buyalo convex hypersurface theorem [START_REF] Alexander | An optimal lower curvature bound for convex hypersurfaces in Riemannian manifolds[END_REF], the induced inner metric on ∂C has curvature bounded from below by -1 in the sense of Alexandrov -in short, the metric is CBB(-1), see Section 2.1. In the present paper, we prove that all the CBB(-1) metrics on the torus are obtained in this way.

Date: May 15, 2015 v1.

Theorem 1.1. Let m be a CBB(-1) metric on the torus. Then there exists a hyperbolic cusp C with convex boundary such that the induced metric on ∂C is isometric to m.

Throughout the paper, by induced metric we mean an intrinsic metric. Examples of CBB(-1) metrics on the torus are distances defined by Riemannian metrics of curvature ≥ -1. Using classical regularity results of Pogorelov (see below), Theorem 1.1 implies the following.

Theorem 1.2. Let g be a smooth Riemannian metric of curvature > -1 on the torus. Then there exists a hyperbolic cusp C with smooth strictly convex boundary such that the induced Riemannian metric on ∂C is isometric to g.

Another examples of CBB(-1) metrics on the torus are hyperbolic metrics with conical singularities of positive curvatures. Recall that the (singular) curvature at a cone singularity is 2π minus the total angle around the singularity. The proof of Theorem 1.1 will be done by polyhedral approximation, using the following result.

Theorem 1.3 ([FI09]

). Let m be a hyperbolic metric with conical singularities of positive curvature on the torus. Then there exists a hyperbolic cusp C with convex polyhedral boundary such that the induced inner metric on ∂C is isometric to m.

Actually it is proved in [START_REF] Fillastre | Hyperbolic cusps with convex polyhedral boundary[END_REF] that the cusp C in the statement of Theorem 1.3 is unique. One can hope a uniqueness result in Theorem 1.1 (that would also imply uniqueness in Theorem 1.2). This should be the subject of a forthcoming paper.

The above statements were the last steps in order to get the following general statement.

Theorem 1.4. Let m be a CBB(k) metric on a compact surface. Then m is isometric to a convex surface S in a Riemannian space of constant curvature k. Moreover

• if m is a metric of curvature k with conical singularities of positive curvature, then S is polyhedral, • if m comes from a smooth Riemannian metric with curvature > k, then S is smooth and strictly convex.

In the rest of the introduction we will recall all the results leading to Theorem 1.4. The proof of Theorem 1.1 is based on a general result of polyhedral approximation that is recalled in Section 2.1 (Theorem 2.2). Going to the universal cover, boundaries of convex hyperbolic cusps are seen as convex surfaces of the hyperbolic space invariant under the action of a group of isometries acting cocompactly on a horosphere. Such surfaces are graphs of horoconvex functions defined on the horosphere. They are introduced in Section 2.2. They can be written in terms of convex functions on the plane, hence they will inherit strong properties from convex functions.

Then we prove Theorem 1.1 in Section 3. Theorem 1.3 and Theorem 2.2 give a sequence of polyhedral surfaces in H 3 . One shows that this sequence converges to a convex surface, invariant under the action of a group Γ. The main point is to check that the induced metric on the quotient of the surface by Γ is isometric to the metric m (Section 3.4). 1.2. Hyperbolization of products manifolds. The notion of metric space with non-negative curvature was introduced by A.D. Alexandrov in order to describe the induced metric on the boundary of convex bodies in R 3 . He proved that this property characterizes the convex bodies in the following sense.

Theorem 1.5 [START_REF] Alexandrov | selected works[END_REF]). Any CBB(0) metric on the sphere is isometric to the boundary of a convex body in R 3 .

The hyperbolic version is as follows.

Theorem 1.6 ( [START_REF] Alexandrov | selected works[END_REF]). Any CBB(-1) metric on the sphere is isometric to the boundary of a compact convex set in H 3 .

Let us mention the following general local result, obtained from Theorem 1.6 and a gluing theorem.

Theorem 1.7 ([Ale06]). Each point in a CBB(-1) surface has a neighbourhood isometric to a convex surface in H 3 .

Forgetting the part of the hyperbolic space outside of the convex body, one derives from Theorem 1.6 the following hyperbolization theorem for the ball.

Theorem 1.8. Let m be a CBB(-1) metric on the sphere. Then there exists a hyperbolic ball M with convex boundary such that the induced metric on ∂M is isometric to m.

Actually Theorem 1.8 also implies Theorem 1.6, because in this case the developing map is an isometric embedding [CEG06, Proposition I.1.4.2.]. Theorem 1.6 and Theorem 1.8 are proved by polyhedral approximation. For example Theorem 1.6 is proved from the following particular case.

Theorem 1.9. Let m be a hyperbolic metric with conical singularities of positive curvature on the sphere. Then there exists a hyperbolic ball M with convex polyhedral boundary such that the induced metric on ∂M is isometric to m.

The following regularity result roughly says that if the metric on a convex surface in H 3 is smooth, then the surface is smooth.

Theorem 1.10 ([Pog73, Theorem 1, chap. V 8]). Let S be a surface with a C k , k ≥ 5, Riemannian metric of curvature > -1. If S admits a convex isometric embedding into H 3 , then its image is a C k-1 surface.
See [START_REF] Chang | The Weyl problem with nonnegative Gauss curvature in hyperbolic space[END_REF] for more precise results if S is homeomoprhic to the sphere, in particular if the curvature is ≥ -1. Theorem 1.10 and Theorem 1.6 immediately give the following.

Theorem 1.11. Let g be a smooth Riemannian metric with curvature > -1 on a the sphere. Then there exists a hyperbolic ball M with smooth convex boundary such that the induced metric on ∂M is isometric to g.

For metrics on a compact (connected) surface S of genus > 1, the following result was recently proved.

Theorem 1.12 ( [START_REF] Slutskiy | Compact domains with prescribed convex boundary metrics in quasi-Fuchsian manifolds[END_REF][START_REF] Slutskiy | Polyhedral metrics on the boundaries of convex compact quasi-Fuchsian manifolds[END_REF]). Let M be a compact connected 3-manifold with boundary of the type S × [1, 1]. Let m be a CBB(-1) metric on ∂M . Then there exists a hyperbolic metric in M with a convex boundary such that the induced metric on ∂M is isometric to m.

The proof of Theorem 1.12 goes by smooth approximation. The smooth version of Theorem 1.12 is included in the following more general result.

Theorem 1.13 [START_REF] Labourie | Métriques prescrites sur le bord des variétés hyperboliques de dimension 3[END_REF]). Let M be a compact manifold with boundary (different from the solid torus) which admits a structure of a strictly convex hyperbolic manifold. Let g be a smooth metric on ∂M of curvature > -1. Then there exists a convex hyperbolic metric on M which induces g on ∂M .

See also [START_REF] Schlenker | Hyperbolic manifolds with convex boundary[END_REF], which contains a uniqueness result. Of course one can take for metrics m in the statement of Theorem 1.12 hyperbolic metrics on S with conical singularities with positive curvature. But the boundary of the solution is not necessarily of polyhedral type. This is because the boundary may meet the boundary of the convex core of M . If M is Fuchsian, that is if its convex core is a totally geodesic surface, this cannot happen. Actually we have the following.

Theorem 1.14 [START_REF] Fillastre | Polyhedral realisation of hyperbolic metrics with conical singularities on compact surfaces[END_REF]). Let m be a hyperbolic metric with conical singularities with positive curvature on a compact surface S of genus > 1. Then there exists a Fuchsian hyperbolic manifold S × [-1, 1] with polyhedral convex boundary such that the induced metric on the boundary components is isometric to m.

The smooth analogue was known for a long: Theorem 1.15 [START_REF] Gromov | Partial differential relations, volume 9 of Ergebnisse der Mathematik und ihrer Grenzgebiete (3)[END_REF]). Let g be a smooth Riemannian metric with curvature > -1 on a compact surface S of genus > 1. Then there exists a Fuchsian hyperbolic manifold S × [-1, 1] with smooth convex boundary such that the induced metric on the boundary components is isometric to g.

Using Theorem 1.15 instead of Theorem 1.13, the proof of Theorem 1.12 leads to the following. Theorem 1.16. Let m be a CBB(-1) metric on a compact surface S of genus > 1. Then there exists a Fuchsian hyperbolic manifold S ×[-1, 1] with convex boundary such that the induced metric on the boundary components is isometric to m.

Let us put all these statements together. Cutting in a suitable way the hyperbolic manifolds given in theorems 1.6, 1.11, 1.9, 1.1, 1.2, 1.3, 1.16, 1.15, 1.14, we obtain the following result.

Theorem 1.17. Let m be a CBB(-1) metric on a compact surface S. Then the manifold S × [-1, 1] admits a hyperbolic metric, such that S × {-1} is convex and isometric to m for the induced inner metric, and S × {1} has constant curvature. Moreover • if m is a hyperbolic metric with conical singularities of positive curvature, then S × {-1} is polyhedral,

• if m comes from a smooth Riemannian metric with curvature > -1, then S × {-1} is smooth and strictly convex.

Note that in the case of genus > 1, we have chosen the Fuchsian solution, but the quasi-Fuchsian Theorem 1.12 gives many choices for the realization of the prescribed metric. Actually all the cases in Theorem 1.17 share the same property: the holonomy of their developing map fixes a point (the point may not be in the hyperboic space, see for example the beginning of Section 3).

In the case of CBB(-1) metrics on the torus, we could also consider a hyperbolic metric with convex boundary on a full torus. In this direction, only the smooth case is known.

Theorem 1.18 [START_REF] Schlenker | Hyperbolic manifolds with convex boundary[END_REF]). Let g be a smooth Riemannian metric of curvature > -1 on the torus T . Then there exists a (unique) hyperbolic metric on the full torus such that the metric on the boundary is smooth, strictly convex and isometric to g.

Another question is to realize CBB(-1) metrics on compact surfaces of genus > 1 as the convex boundary of more general compact hyperbolic manifold, analogously to Theorem 1.13.

We cited Theorem 1.5 about realization of CBB(0) metrics on the sphere in the Euclidean space. There is also an analogue result about realization of CBB(1) metrics on the sphere in the 3 dimensional sphere [START_REF] Alexandrov | selected works[END_REF], as well as the polyhedral and smooth counterparts. Theorem 1.17 gives all the possibilities for a CBB(-1) metric on a compact surface of genus > 1. Moreover it is obvious that any flat metric on a torus T can be extended to a flat metric on T × [-1, 1]. Lemma 2.1 says that we have exhausted all the possibilities. Theorem 1.4 follows.

A question is to know if the constant curvature metric on S × [-1, 1] is unique. Due to the work of Pogorelov, the answer is positive is S is the sphere [START_REF] Pogorelov | Extrinsic geometry of convex surfaces[END_REF]. As we already mentioned, in the torus case this is work in progress. As the only unsolved case there would remain that of Fuchsian hyperbolic manifolds with convex boundary. 1.3. Smooth variational approach? As we said, Theorem 1.5 was proved by polyhedral approximation. It is based on the following seminal theorem, proved in the 1940's.

Theorem 1.19 ([Ale06]

). Let m be a flat metric with conical singularities of positive curvature on the sphere. Then there exists a convex polyhedron in Euclidean space with inner induced metric m on the boundary.

The proof of Theorem 1.19 is done by a continuity method, based on topological arguments, in particular the Domain Invariance theorem. Some years ago, a variational proof of Theorem 1.19 was given in [START_REF] Bobenko | Alexandrov's theorem, weighted Delaunay triangulations, and mixed volumes[END_REF]. The functional is a discrete Hilbert-Einstein functional. It was then used in [START_REF] Izmestiev | A variational proof of Alexandrov's convex cap theorem[END_REF], and later in [START_REF] Fillastre | Hyperbolic cusps with convex polyhedral boundary[END_REF] to prove Theorem 1.3. A long-standing question is to use the smooth Hilbert-Einstein functional to give a variational proof of the smooth version of Theorem 1.19 (known as Weyl problem) [START_REF] Blaschke | Über die Verwirklichung einer geschlossenen Fläche mit vorgeschriebenem Bogenelement im Euklidischen Raum[END_REF][START_REF] Izmestiev | Infinitesimal rigidity of smooth convex surfaces through the second derivative of the Hilbert-Einstein functional[END_REF]. It would be interesting to give a variational proof of Theorem 1.2 as well. There are reasons to think that the functional will have good properties in the case of a hyperbolic cusp. 1.4. Acknowledgement. The authors thank Stephanie Alexander, Thomas Richard, Joël Rouyer, Dima Slutskiy for useful conversations.

The first author was partially supported by the ANR GR-Analysis-Geometry and by the mathematic department of the Universidade Federal do Rio de Janeiro and this research has been conducted as part of the project Labex MME-DII (ANR11-LBX-0023-01). A part of this work was done during his stay at the Universidade Federal do Rio de Janeiro. He thanks this institution for its hospitality.

The second author was supported by by the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013)/ERC Grant agreement no. 247029-SDModels.

The third author was partially supported by the Gruppo Nazionale per l'Analisi Matematica, la Probabilità e le loro Applicazioni (GNAMPA).

Background

2.1. CBB metrics on compact surfaces. We follow [START_REF] Burago | A course in metric geometry[END_REF] for basic definitions and results about metric geometry. See also [START_REF] Bridson | Metric spaces of non-positive curvature, volume 319 of Grundlehren der Mathematischen Wissenschaften[END_REF] and [AKP]. Let m be a metric on a compact surface S (by this we imply that the topology given by m is the topology of S). We suppose that m is intrinsic, that is for any x, y ∈ S, m(x, y) is equal to the infimum of the length of the continuous curves between x and y. By the Hopf-Rinow theorem, there always exists a shortest path between x and y.

The metric m is CBB(k) if every point has a neighbourhood U such that any triangle contained in U is thicker than the comparison triangle in the model space of constant curvature k (see the references above for precise and equivalent definitions). By the Toponogov globalization theorem, this property is actually true for any triangle in (S, m).

A shortest path between two points in a CBB(k) space may not be unique, as show the example of a disc of curvature k with a sector removed and the two resulting sides identified. But shortest paths in CBB(k) do not branch.

Let (S, m) be a polyhedral CBB(k) metric, that is a metric of constant curvature k with singular curvatures k i (the k i have to be positive [BBI01, 10.9.5]). It has to satisfy the Gauss-Bonnet formula

2πχ(S) = k area(S) + k i i.e. 2πχ(S) ≥ k area(S)
with equality if and only if m is a smooth constant curvature metric (no conical singularities). Now let (S, m) be any CBB(k) metric. By a theorem of Alexandrov and Zalgaller, (S, m) can be decomposed into non-overlapping geodesic triangles. Replacing each triangle by a comparison triangle in the space of constant curvature k, we obtain a polyhedral CBB(k) metric on S see [START_REF] Richard | Ricci flow without upper bounds on the curvature and the geometry of some metric spaces[END_REF][START_REF] Itoh | Moderate smoothness of most Alexandrov surfaces[END_REF] for details. In particular, we obtain the following.

Lemma 2.1. A compact surface S can be endowed with a CBB(k) metric if and only if

• if S is a sphere, k ∈ R,
• if S is a torus, k = 0 and the metric is a flat Riemannian metric or k < 0, • otherwise, k < 0.

Actually, Alexandrov and Zalgaller proved much more, but in a different context. Roughly speaking, the triangulation of the CBB(-1) can be chosen as fine as wanted. If the perimeter of the triangles goes to 0, then the sequence of polyhedral metrics obtained by replacing the triangles by comparison triangles converge to (S, m) in the Gromov-Haussdorff sense [START_REF] Richard | Ricci flow without upper bounds on the curvature and the geometry of some metric spaces[END_REF][START_REF] Itoh | Moderate smoothness of most Alexandrov surfaces[END_REF].

Theorem 2.2. Let d be a CBB(-1) metric on a compact surface. Then there exists polyhedral CBB(-1) sequence of metric m n on the torus Gromov Hausdorff converging to m.

At the end of the day, in the case of the torus, it is not hard to conclude from Theorem 1.1 and Proposition 3.5 that the convergence can be taken uniform in Theorem 2.2.

Let us mention the following results about Gromov-Hausdorff convergence that we will use in the sequel. 2.2. Horoconvex functions. We identify R 2 with a given horosphere H ⊂ H 3 , with center ∞. We get coordinates (x, t) on H 3 = H × R, where t is the signed distance from a point to H: it is positive if and only if the point is in the exterior of the horoball bounded by H. Note that it is the length of the segment between x and its orthogonal projection onto H, and that the line from x to ∞ is orthogonal to H.

Let u : R 2 → R. The horograph of u is the subset (x, u(x)) ∈ H 3 for those coordinates. The horograph is said to be convex if the surface is convex in H 3 in the sense that it bounds a geodesically convex set. In the Klein projective model, this corresponds to the affine notion of convexity.

Remark 2.5. In the upper half plane model, if the horosphere H is the horizontal plane at height 1, then the horograph of u is the graph of e -u .

We have the following characterization of horographs. It was already known in the smooth case [START_REF] Guan | Hypersurfaces of constant curvature in hyperbolic space[END_REF]. Let us also mention that the Darboux equation related to Theorem 1.2 is studied in [START_REF] Rosenberg | On the existence of convex hypersurfaces of constant Gauss curvature in hyperbolic space[END_REF].

Proposition 2.6. The horograph of u : R 2 → R is a convex surface if and only if the function

x → e -2u(x) + x 2 is convex, with • the Euclidean norm.

In particular, e -2u is semi-convex, or lower-C ∞ , compare with 10.33 and 13.27 in [START_REF] Rockafellar | of Grundlehren der Mathematischen Wissenschaften[END_REF]. We will call horoconvex a function satisfying the hypothesis of the proposition.

Proof. As above, consider coordinates (x, t) H on H 3 = H × R. The horograph of u is convex in H 3 if and only if at each point (x 0 , u(x 0 )) H there exists a totally geodesic surface Σ containing the point (x 0 , u(x 0 )) H and such that Σ ⊂ {(x, y) H : y ≥ u(x)}. Now, consider on the Poincaré halfspace model the standard Euclidean coordinates (y, s) E ∈ R 2 × (0, ∞). Without loss of generality we can assume that the horosphere H is the plane at heigh 1 in this model. Then we have (x, t) H = (x, e -t ) E . In this system, Σ has to be a half-sphere with center (c, 0) E on the plane at infinity R 2 × {0}. In particular every such a half-sphere containing the point (x 0 , u(x 0 )) H is given by {(x, s) E : e -2u(x 0 ) + c -

x 0 2 = x -c 2 + s 2 } .
Coming back to (, ) H coordinates, we have obtained that the horograph of u is convex if and only if for all

x 0 ∈ R 2 there exists a point c ∈ R 2 such that u(x) ≤ - 1 2 ln e -2u(x 0 ) + c -x 0 2 -c -x 2 , that is, (1) e -2u(x) -e -2u(x 0 ) ≥ c -x 0 2 -c -x 2 = -x -x 0 2 + 2 G, x -x 0 ,
where

G := c -x 0 ∈ R 2 . Since x ∈ R 2 is arbitrary, (1) is equivalent to (2) e -2u(x 0 +v) + x 0 + v 2 -e -2u(x 0 ) -x 0 2 ≥ 2(x 0 + G), v , ∀v ∈ R 2 .
In turn, (2) means that if G ∈ R 2 is such that (1) is satisfied, then at each point x 0 ∈ R 2 the graph of the function e -2u(x) + x 2 has the planar graph of v → 2(x 0 + G), v + e -2u(x 0 ) + x 0 2 as a support plane. Hence e -2u(x) + x 2 is a convex function on R 2 if and only if the horograph of u is convex in H 3 . Remark 2.7. Suppose that x = x 0 + th for some unitary vector h ∈ R 2 and t > 0. Then (1) reads (3) 1 t e -2u(x 0 +th) -e -2u(x 0 ) ≥ -t|h| 2 + 2 G, h .

If u ∈ C 1 (R 2 ), taking the limit as t → 0 we get that grad x 0 e -2u , h ≥ 2G, h , and since the latter inequality holds for both h and -h we have necessarily that G is unique and G = 1 2 grad x 0 e -2u = -e -2u(x 0 ) grad x 0 u .

Corollary 2.8. Let u be horoconvex and > 0. Then u + is horoconvex.

Proof. By Proposition 2.6, one has to see that e -2 e -2u(x) + x 2 is convex, that is equivalent to the convexity of e -2u(x) + e 2 x 2 . Let f + g be convex, g convex and λ > 1. Then f + λg = (f + g) + (λ -1)g is convex as a sum of two convex functions.

Example 2.9. In one dimension, the function t → cos(t)/20 is horoconvex, see Figure 1. More generally, any function C 2 close to a constant function is horoconvex. But t → cos(t) is not horoconvex. This example shows that u horoconvex does not imply λu horoconvex.

Figure 1. Graphs of t → e -cos(t)/10 and t → e -2 cos(t) .

Horoconvex functions inherit strong properties from convex functions.

Corollary 2.10. Any sequence of uniformly bounded horoconvex functions is equi-Lipschitz on any compact set of R 2 . Moreover, up to extracting a subsequence, the sequence converges uniformly on any compact set to a horoconvex function.

Proof. Let C ⊂ R 2 be a compact set and (u n ) a sequence of uniformly bounded horoconvex functions. Let F n (x) = e -2un(x) + x 2 , which is convex by Proposition 2.6. By [START_REF] Rockafellar | Convex analysis[END_REF]10.4], there exists an > 0 such that for any x, y ∈ C

|F n (x) -F n (y)| ≤ max C F n -min C F n x -y .
As the u n are uniformly bounded, F n are uniformly bounded on C, hence there exists a number A satisfying

|F n (x) -F n (y)| ≤ A x -y .
Using again that the u n are uniformly bounded, and that

x 2 -y 2 ≤ 2 sup C x x -y ,
we thus obtain that

|u n (x) -u n (y)| ≤ A x -y for some A = A (C) > 0 independent of n. So the sequence is equi-Lipschitz on C.
Up to extract a subsequence, the sequence of convex functions (F n ) converge (uniformly on compact sets) to a convex function F [Roc97, Theorem 10.9]). As the u n are uniformly bounded, there exists a positive constant c such that

F n ≥ c + • 2 , so F > • 2 , hence the function u = - 1 2 ln(F -• 2 )
is well defined and horoconvex by definition. As (F n ) converges to F uniformly on compact sets, it follows easily that u n converges to u uniformly on compact sets.

In particular, a horoconvex function is Lipschitz on any compact set. By Rademacher theorem, it is differentiable almost everywhere.

2.3. Induced metric. The length of a curve c in H 3 is the supremum of the length of all the broken lines of H 3 with vertices on c. Equivalently [BBI01, Theorem 2.7.6], if c is Lipschitz (in H 3 ), then

L(c) = c H 3 .
Let S be a convex surface in H 3 . The (intrinsic) induced metric on S between two points a, b of S is the infimum of all the Lipschitz curves of finite length between a and b.

Let u be a horoconvex function. Let du be the intrinsic metric induced on the horograph of u. For simplicity, we will look at metrics onto R 2 rather than on the surfaces: for (x, y) ∈ R 2 , d u (x, y) := du x, e -u(x) , y, e -u (y) .

Note that, in the upper half space model, notions of locally Lipschitz are equivalent for the metric of H 3 and R 3 . As the projection onto the horizontal plane is contracting, a locally Lipschitz curve of H 3 is projected onto a locally Lipschitz curve of R 2 .

Let c : [a, b] → R 2 be a Lipschitz curve. Let c u be the corresponding curve in the horograph of u i.e. on the graph of e -u :

c u = c e -u•c . As u is Lipschitz, c u is a Lipschitz curve of H 3 .
Let us denote by L u (c) the length of c u for the metric du on S u . Using the half-space model metric

L u (c) = b a c u R 3 (c u ) 3 = b a e u•c c 2 + Du(c ) 2 e -2(u•c) 1/2 i.e. ( 4
) L u (c) = b a e 2u•c c 2 + Du(c ) 2 1/2 .
Lemma 2.11. Let (u n ) be a uniformly bounded sequence of horoconvex functions. Then on any compact set K, d un are uniformly Lipschitz equivalent to the Euclidean metric: ∃λ 1 , λ 2 > 0 such that

λ 1 d R 2 ≤ d un ≤ λ 2 d R 2 .
Moreover, for any Lipschitz curve c contained in K,

λ 1 L R 2 (c) ≤ L un (c) ≤ λ 2 L R 2 (c) .
Proof. By construction, for any x, y ∈ K, d un (x, y) is not less than the distance in H 3 between the corresponding points on the horograph of u. As K is compact and the u n uniformly bounded, the corresponding horographs above K in R 3 are contained in a hyperbolic ball. There exists a constant λ 1 such that on this ball, d

H 3 ≥ λ 1 d R 3 , and clearly d R 3 ≥ d R 2 .
As the length of a Lipschitz curve for d un is the supremum of the length of broken shortest paths [BBI01, 2.3.4,2.4.3] it follows that for any curve c in K,

λ 1 L R 2 (c) ≤ L un (c).
On the other hand, for any curve c in K, it follows from (4)

L un (c) ≤ b a e -un c + |Du n (c )|
and as the u n are uniformly bounded on K by assumption, as well as grad u n when it exists by Corollary 2.10, then there exists λ 2 such that

L un (c) ≤ λ 2 L R 2 (c) .
The proof of the following lemma mimics the one for convex bodies in Euclidean space [BBI01, p. 358].

Lemma 2.12. Let u, v be horoconvex such that u ≤ v and

δ = sup R 2 (v -u) is finite. Then d u ≤ d v + 2δ .
Proof. Recall that the Hyperbolic Busemann-Feller Lemma, [BH99, II.2.4] says that the orthogonal projection onto a convex set in H 3 is contracting. u ≤ v implies that the horograph of v is in the exterior of the convex set bounded by the horograph of u, so the orthogonal projection is well defined from the horograph of v onto the horograph of u. For a ∈ R 2 , let p ⊥ (a) be the vertical projection onto R 2 of the orthogonal projection of (a, v(a)) onto the horograph of u.

On one hand, Busemann-Feller Lemma implies that (5)

d u (p ⊥ (a), p ⊥ (b)) ≤ d v (a, b) .
On the other hand, Busemann-Feller Lemma implies that d u (p ⊥ (a), a) is less than the distance in H 3 between (a, v(a)) and (a, u(a)), and this last quantity is less than δ by assumption, so

(6) d u (p ⊥ (a), a) ≤ δ .
The result follows from (5), (6) and the triangle inequality.

Proof of Theorem 1.1

Now let (S, m) be a CBB(-1) metric on the torus. According to Theorem 2.2 there exists a sequence of polyhedral CBB(-1) metric m n on the torus Gromov-Hausdorff converging to m. By Theorem 1.3, for any n there exists a hyperbolic cusp C n with convex boundary and induced metric on ∂C n isometric to m n .

As mentioned in the introduction, the universal cover C n can be isometrically embedded as a convex subset of H 3 via the developing map D. The action of the fundamental group π 1 (C n ) ∼ = π 1 (T ) on C n by deck transformations yields a representation ρ : π 1 (T ) → Iso + (H 3 ). The cusp C n contains a totally umbilic torus M with Euclidean metric. It follows that the developing map maps the universal cover of M to a horosphere. The group ρ(π 1 (C n )) = Γ n acts on D( M ) freely with a compact orbit space. The group Γ n is a group of parabolic isometries. The surface S n = ∂D( C n ) is convex and globally invariant under the action of Γ n . It is easy to see that S n is homeomorphic to H via the central projection from the center of D( M ). Up to rotations of the hyperbolic space, we normalize the surfaces S n in such a way that the point fixed by Γ n is ∞ in the half space model. Moreover, choosing a point x 0 in the universal cover of the torus, up to compose by parabolic and hyperbolic isometries, we consider that the developing maps send x 0 onto (0, 0, 1) E .

So the surfaces S n are described by horoconvex functions u n . We identify Γ n with the corresponding lattice in H = R 2 . In particular, u n (γ •x) = u n (x) for any γ ∈ Γ n and x ∈ R 2 , and the normalization above says that u n (0) = 0 for any n. The quotient of d un by Γ n is isometric to m n .

We will prove that (u n , Γ n ) converge to some (u, Γ) and that the quotient of d u by Γ is isometric to m. This will prove Theorem 1.1: the wanted cusp is the quotient by Γ of the convex side of the horograph of u.

3.1.

A uniform bound on horographs. From Lemma 2.3, there exists a uniform upper bound diam of all the diameters of the metrics m n .

Lemma 3.1.

(1) The sequence (u n ) n is uniformly bounded.

(2) There is a compact set D ⊂ R 2 such that for any y ∈ R 2 and any n, there exists γ ∈ Γ n with γ • y ∈ D.

Proof. Recall that all the horographs S n of u n pass through x 0 = (0, 0, 1) E . Let b n be the set of points on S n at distance ≤ diam from (0, 0, 1) E . Then as the distance on S n is greater than the extrinsic distance of H 3 , all the b n are contained in a same hyperbolic ball B.

In the half space model, let D be the projection of the ball B onto the horizontal plane passing through the origin. Observe that D = B R 2 δ (0) is a Euclidean closed ball centred at the origin of R 2 . As B is contained between two horosphere centred at ∞ (i.e. two horizontal plane) the u n are uniformly bounded on D, say c 1 < u n < c 2 . Now by construction, for any y ∈ R 2 , there exists

γ ∈ Γ n such that γ • y ∈ D. Hence c 1 < u n (γ • y) = u n (y) < c 2 .
By Lemma 3.1 (1) and Corollary 2.10, we get Corollary 3.2. The sequence (u n ) n is equi-Lipschitz on every compact set of R 2 .

Convergence of groups.

Lemma 3.3. There exists a sequence (a n , b n ) n of generators of Γ n which converge in R 2 (up to extract a subsequence) to two linearly independent non-zero vectors a and b.

Proof. Let us choose generators (a n , b n ) of Γ n which are contained in B R 2 3δ (0) (here we identify an element of γ of Γ n with the vector γ • 0 of R 2 ), that is possible by Lemma 3.1. Since B R 2 3δ (0) is compact, up to take a subsequence we get the existence of two vectors a, b ∈ R 2 such that a n → a and b n → b as n → ∞.

Suppose that either one of the vectors v or w is zero, or that they are parallel. Since by continuity |a| and |b| are bounded by 3δ, necessarily we would have that the area of the parallelogram with side a n and b n tend to zero, as n → ∞. In turn, this means that the area of a fundamental domain of R 2 for the action of Γ n tend to zero as n → ∞. Applying Lemma 2.11 with for n large enough. In fact k(a -a n ) + k (b -b n ) → 0 as n → ∞, and as the u n are equi-Lipschitz on a sufficiently large compact set the absolute value at line (8) is smaller than /4 for n large enough. Moreover the absolute value at line (9) is zero for every n by the Γ n -invariance of u n , and the absolute value at lines (7) and (10) are smaller then /4 for n large enough by the uniform convergence of the u n . Since > 0 is arbitrary, this concludes the proof.

K = B R 2 3δ (
3.4. Convergence of metrics. In the preceding section, we have constructed a pair (u, Γ). It remains to check that the induced metric m u on (R 2 , d u )/Γ is isometric to (T, m). Basically, one has to check that if the sequence (u n ) converges, then the sequence of induced metric converges. In the remaining of this section we will prove the following result, that ends the proof of the theorem, because on compact metric spaces, uniform convergence imply Gromov-Hausdorff convergence, and the Gromov-Hausdorff limit is unique.

Proposition 3.5. The sequence (m n ) uniformly converges to m u . Lemma 3.6. Let K ⊂ R 2 be compact. Then where γ is considered as a vector of R 2 . The map φn descends to a homeomorphism ϕ n between R 2 /Γ and R 2 /Γ n .

Lemma 3.10. Let K ⊂ R 2 . Then on K,

x → d un ( φn (x), x)

uniformly converge to zero and d un ( φn (x), φn (y)) uniformly converge to d u (x, y).

Proof. φn converge to the identity map, uniformly on any compact for the Euclidean metric. The first result follows from Lemma 2.11. The second result follows easily from the first one, the triangle inequality and Lemma 3.8.

Lemma 3.11. There exists a compact set K ⊂ R 2 such that for any n, for any p, q in the torus, a lift of a shortest path for m n between p and q is contained in K.

Proof. Let K = E(D), where D is the compact set obtained in Lemma 3.1. By definition of D, there exists a lift x of p in D. By construction of K, the ball for d n centred at x with radius m n (p, q) is contained in K.

Let C be the closure of ∪ n φn (K), where K is given by Lemma 3.11. C is a compact set. Lemma 3.12. For any ν > 0, if n is sufficiently large, for any p, q ∈ T , if x and y are respective lifts to the set C defined above, if d u (x, y) = m(p, q), then m n (ϕ n (p), ϕ n (q)) ≤ d un ( φn (x), φn (y)) ≤ m n (ϕ n (p), ϕ n (q)) + ν .

Proof. As d u (x, y) = m(p, q), for any γ ∈ Γ, The result follows because m n (ϕ n (p), ϕ n (q)) is the minimum on Γ of all the d un ( φn (x), φn (γ) • φn (y)).

Proof of Proposition 3.5. Let > 0. For any p, q ∈ T , with the notations of Lemma 3.12, for n large enough, m n (ϕ n (p), ϕ n (q)) -m(p, q) ≤ d un ( φn (x), φn (y)) -d u (x, y) ≤ d un ( φn (x), x) + d un ( φn (x), y) + d un (x, y) -d u (x, y) . Applying Lemma 3.8 and Lemma 3.10 on the compact set C, for n sufficiently large, the last quantity above is less than , independently of x and y. For the same reasons, the same conclusion holds for m(p, q) -m n (ϕ n (p), ϕ n (q)) ≤ d u (x, y) -d un ( φn (x), φn (y)) + ν ≤ d u (x, y) -d un (x, y) + d un (x, y) -d un ( φn (x), φn (y)) + ν .

  Lemma 2.3 ([BH99, I.5.40],[BBI01, 7.3.14]). Gromov-Hausdorff convergence implies convergence of the diameter Theorem 2.4 ([BGP92],[BBI01, 10.10.11]). If a sequence (S, m n ) of CBB(k) metrics on a compact surface S converges in the Gromov-Hausdorff sense to a CBB(k) metric on S, then the sequence of the areas of (S, m n ) (the total two dimensional Hausdorff measure) is bounded from below by a positive constant.

  0), by Proposition 3.1.4 in [AT04], the two dimensional Hausdorff measure of m n tends to zero, thus contradicting Theorem 2.4. 3.3. Construction of the solution. By Corollary 2.10 and Lemma 3.1, up to extract a subsequence, the sequence (u n ) converges to a horoconvex function u, uniformly on any compact set. Let a, b ∈ R 2 given by Lemma 3.3, and define Γ ⊂ Iso(R 2 ) as the direct product of a and b . Since a and b are linearly independent vectors, R 2 /Γ is a torus. Lemma 3.4. The function u is Γ-invariant. Proof. Let y ∈ R 2 and γ ∈ Γ. Then, for every > 0 |u(γy) -u(y)| = |u(y + ka + k b) -u(y)| ≤ |u(y + ka + k b) -u n (y + ka + k b)| (7) + |u n (y + ka + k b) -u n (y + ka n + k b n )| (8) + |u n (y + ka n + k b n ) -u n (y)| (9) + |u n (y) -u(y)| < (10)

  E(K) = closure (∪ x∈K ∪ n {y|d un (x, y) ≤ diam})Let φn be the linear isomorphism sending a to a n and b to b n . Hence clearly, for any γ ∈ Γ,(11) φn (γ • x) = φn (γ) • φn (x)

  d u (x, γ • y) ≥ d u (x, y) .By Lemma 3.10, uniformly on C, if n is sufficiently large, d un ( φn (x), φn (γ) • φn (y)) + ν ≥ d un ( φn (x), φn (y)) .

is compact.

Proof. We have d H 3 x, e -un(x) , y, e -un (y) ≤ d un (x, y) ≤ diam , but [START_REF] Ratcliffe | Foundations of hyperbolic manifolds[END_REF]4.6.1] cosh d H 3 x, e -un(x) , y, e -un(y) = 1 + x -y 2 2e -un(x) e -un(y) so

x -y ≤ √ 2e -c cosh(diam) -1 where c is the uniform lower bound of the u n . The result follows because K is compact.

Corollary 3.7. Let K ⊂ R 2 be compact. Let L(K) be the set of shortest paths for any d n between points of K (we don't ask the shortest path to be contained in K). Then there exists a constant α such that ∀c ∈ L(K),

Proof. By Lemma 2.11 applied to K, for any x, y ∈ K,

Let c be a shortest path for u n between x and y, so that L un (c) = d un (x, y).

The shortest path is contained in the compact set E(K) given by Lemma 3.6, so by Lemma 2.11 again, but applied to

Lemma 3.8. Let K ⊂ R 2 be compact. Then d un uniformly converge to d u on K.

Proof. Let > 0. As u n uniformly converge to u, for n sufficiently large, u ≤ u n + , so by Lemma 2.12

Let x, y ∈ K and let c be a shortest path for u n between x and y. Then

and from (4), the fact that the u n are uniformly bounded and Corollary 3.7, there exists a constant β depending only on K such that

and as L un (c) = d un (x, y) we obtain

Exchanging the role of u and u n , we finally obtain

Remark 3.9. A result of A.D. Alexandrov gives a weaker convergence of the induced metrics for any convex surfaces converging in the Hausdorff sense to a convex surface in the hyperbolic space, see [Slu].