Luca Ciccone

Francesco Dagnino

Luca Padovani

Fair Termination of Multiparty Sessions

Keywords: 2012 ACM Subject Classification Theory of computation → Process calculi, Theory of computation → Type structures, Theory of computation → Program analysis Multiparty sessions, fair termination, fair subtyping, deadlock freedom .CVIT.2016.23

There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that well-typed multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair termination, combined with the usual safety properties ensured within sessions, not only is desirable per se, but it entails progress and enables a compositional form of static analysis such that the well-typed composition of fairly terminating sessions results in a fairly terminating program.

Introduction

Sessions [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF] are private conversations among processes following a protocol specification called session type. The decomposition of a distributed program into sessions enables its modular static analysis and the enforcement of useful properties through a type system. Examples of such properties are communication safety (no message of the wrong type is ever exchanged), protocol fidelity (messages are exchanged in the order prescribed by session types) and deadlock freedom (the program keeps running unless all sessions have terminated). These are all instances of safety properties, implying that "nothing bad" happens. In general, one is also interested in reasoning and possibly enforcing liveness properties, those implying that "something good" happens [38]. Examples of liveness properties are junk freedom (every message is eventually received), progress (every non-terminated participant of a session eventually performs an action) and termination (every session eventually comes to an end).

An enduring limitation of current type systems for multiparty sessions is that they ensure progress for any participant of a session only when such progress can be established independently of the choices performed by the other participants. To illustrate the impact of this limitation, consider a session made of three participants named buyer, seller and carrier in which the buyer aims at purchasing an unspecified number of items from the seller and the seller relies on a carrier for delivering the purchased items to the buyer. The buyer behaves according to the session type S that satisfies the equation S = seller!add.S + seller!pay.!end [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF] indicating that it either pays the seller or it adds an item to the shopping cart and then repeats the same behavior. In this session type, add and pay are messages targeted to the participant with role seller. In turn, the seller accepts add messages from the buyer until a pay message is received, at which point it instructs the carrier to ship the items. Thus, its behavior is described by the session type T that satisfies the equation T = buyer?add.T + buyer?pay.carrier!ship.!end

Finally, the carrier just waits for the ship message from the seller. So, its behavior is described by the session type seller?ship.?end

No available type system is able to guarantee progress for every participant of this multiparty session. What makes this session somewhat difficult to reason about is that the progress of the carrier is not unconditional but depends on the choices performed by the buyer: the carrier can make progress only if the buyer eventually pays the seller.

In this work we propose a type system that guarantees the fair termination of sessions, that is termination under a fairness assumption. The assumption we make is an instance of relative fairness [44] and can be roughly spelled out as follows:

If termination is always possible, then it is inevitable.

(4)

The multiparty session sketched above terminates under this fairness assumption: since it is always possible for the buyer to pay the seller and terminate, in every fair execution of the session the buyer eventually pays the seller, even though we do not know (nor do we impose) an upper bound to the number of items that the buyer may add to the shopping cart. Simply, the non-terminating execution of the session in which the buyer keeps adding items to the shopping cart but never pays is assumed unrealistic and so it can be ignored insofar as termination is concerned.

The reader might wonder why we focus on fair termination instead of considering some fair version of progress. There are three reasons why we think that fair termination is overall more appropriate than just progress. First of all, ensuring that sessions (fairly) terminate is consistent with the usual interpretation of the word "session" as an activity that lasts for a finite amount of time, even when the maximum duration of the activity is not known a priori. Second, fair termination implies progress when it is guaranteed along with the usual safety properties of sessions. Indeed, if the session eventually terminates, it must be the case that any non-terminated participant (think of the carrier waiting for a ship message) is guaranteed to eventually make progress, even when such progress depends on choices made by other participants (like the buyer sending pay to the seller). Last but not least, fair session termination enables compositional reasoning in the presence of multiple sessions. This is not true for progress: if an action on a session s is blocked by actions on a different session t, then knowing that the session t enjoys progress does not necessarily guarantee that the action on s will eventually be performed (the interaction on t might continue forever). On the contrary, knowing that t fairly terminates guarantees that the action on s will eventually be scheduled and performed, so that s may in turn progress towards termination.

Remarkably, the fairness assumption alone does not suffice to turn any multiparty session type system into one that ensures fair termination. In fact, there are several sources of potentially non-terminating behaviors that must be ruled out in well-typed processes: 1. Fairly terminating (and even finite) sessions may be chained, nested, interleaved in such a way that some pending activities are postponed forever. To avoid this problem, our type system makes sure that the effort required by a well-typed process in order to terminate remains finite. At the same time, it does not (always) prevent the modeling of processes that create an unbounded number of sessions.

2.

The type-level constraints usually imposed to well-typed sessions -duality [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF], liveness [45], coherence [START_REF] Carbone | Multiparty session types as coherence proofs[END_REF], just to mention a few -are in general too weak to entail fair session termination. Our type system adopts a stronger notion of "correct multiparty session" that entails fair termination. Variants of this notion have already appeared in the literature [5,41], but we use it here for the first time to relate types and processes. 3. A certain mismatch is usually allowed between the structure of session types and the structure of the processes that adhere to those types. This mismatch is formalized by a subtyping relation for session types which, in its standard formulation [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF], may introduce non-terminating behaviors. Our type system adopts fair subtyping [41], a liveness-preserving refinement of the standard subtyping relation for session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF].

Summary of contributions.

We present the first type system ensuring the fair termination of multiparty sessions and capable of addressing a number of natural communication patterns that are out of scope of existing multiparty session type systems [45,47]. We exploit the compositional reasoning enabled by fair termination to prove a strong soundness result whereby a well-typed composition of fairly terminating sessions is a fairly terminating program (Theorem 5.4). This result scales smoothly also in presence of session chaining, session nesting, session interleaving, session delegation and dynamic session creation. In sharp contrast, the liveness properties ensured by previous multiparty session type systems are either limited to single-session programs [45,47] or require a richer type structure [42,[START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF].

Our contributions extend and generalize previous work on the fair termination of binary sessions [START_REF] Ciccone | Fair termination of binary sessions[END_REF] and allow for the modeling of (intra-session) cyclic network topologies and of multiparty sessions that cannot be decomposed into equivalent (well-typed) binary sessions. Decidability of type checking is not substantially more difficult than the same problem in the binary setting [START_REF] Ciccone | Fair termination of binary sessions[END_REF]. En passant, in this paper we also provide a new characterization of fair subtyping for (multiparty) session types (Table 5) that is substantially simpler than those appearing in previous works [39,41,[START_REF] Ciccone | Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types[END_REF][START_REF] Ciccone | Fair termination of binary sessions[END_REF].

Structure of the paper. We recall the key notions related to fair termination (Section 2) before presenting our language of multiparty sessions (Section 3). Then, we define multiparty session types and fair subtyping (Section 4) and present the typing rules and the soundness properties of the type system (Section 5). In the latter part of the paper we illustrate a few more advanced examples of well-typed processes (Section 6), we discuss related work in more detail (Section 7) and we provide hints at further developments (Section 8). Additional technical material and all the proofs of the presented results can be found in the Appendix, which we provide for completeness but is not necessary for reviewing the submission.

Fair Termination

Since the notion of fair termination will apply to several different entities (session types, multiparty sessions, processes) here we define it for a generic reduction system. Later on we will show various instantiations of this definition. A reduction system is a pair (S, →) where S is a set of states and → ⊆ S × S is a reduction relation. We adopt the following notation: we let C and D range over states; we write C → if there exists D ∈ S such that C → D; we write C → if not C →; we write ⇒ for the reflexive, transitive closure of →. We say that D is reachable from C if C ⇒ D.

As an example, the reduction system ({A, B}, {(A, A), (A, B)}) models an entity that can be in two states, A or B, and such that the entity may perform a reduction to remain in C V I T 2 0 1 6

23:4 Fair Termination of Multiparty Sessions

state A or a reduction to move from state A to state B. To formalize the evolution of an entity from a particular state we define runs.

▶ Definition 2.1 (runs and maximal runs). A run of C is a (finite or infinite) sequence

C 0 C 1 . . . C i . . . of states such that C 0 = C and C i → C i+1 for every valid i. A run is maximal if either it is infinite or if its last state C n is such that C n →.
Hereafter we let ρ range over runs. Each run in the previously defined reduction system is either of the form A n -a finite sequence of A -or of the form A n B -a finite sequence of A followed by one B -or A ω -an infinite sequence of A. Among these, the runs of the form A n B and A ω are maximal, whereas no run of the form A n is maximal.

We now use runs to define different termination properties of states: we say that C is weakly terminating if there exists a maximal run of C that is finite; we say that C is terminating if every maximal run of C is finite; we say that C is diverging if every maximal run of C is infinite. Fair termination [START_REF] Francez | Fairness[END_REF] is a termination property that only considers a subset of all (maximal) runs of a state, those that are considered to be "realistic" or "fair" according to some fairness assumption. The assumption that we make in this work, and that we stated in words in (4), is formalized thus: ▶ Definition 2.2 (fair run). A run is fair if it contains finitely many weakly terminating states. Conversely, a run is unfair if it contains infinitely many weakly terminating states. Continuing with the previous example, the runs of the form A n and A n B are fair, whereas the run A ω is unfair. In general, an unfair run is an execution in which termination is always within reach, but is never reached.

A key requirement of any fairness assumption is that it must be possible to extend every finite run to a maximal fair one. This property is called feasibility [START_REF] Krzysztof | Appraising fairness in languages for distributed programming[END_REF]46] or machine closure [START_REF] Lamport | Fairness and hyperfairness[END_REF]. It is easy to see that our fairness assumption is feasible:

▶ Lemma 2.3.
If ρ is a finite run, then there exists ρ ′ such that ρρ ′ is a maximal fair run.

Fair termination is finiteness of all maximal fair runs: ▶ Definition 2.4 (fair termination). We say that C is fairly terminating if every maximal fair run of C is finite. In the reduction system given above, A is fairly terminating. Indeed, all the maximal runs of the form A n B are finite whereas A ω , which is the only infinite fair run of A, is unfair.

For the particular fairness assumption that we make, it is possible to provide a sound and complete characterization of fair termination that does not mention fair runs. This characterization will be useful to relate fair termination with the notion of correct multiparty session (Definition 4.2) and the soundness property of the type system (Theorem 5.4). ▶ Theorem 2.5. Let (S, →) be a reduction system and C ∈ S. Then C is fairly terminating if and only if every state reachable from C is weakly terminating. ▶ Remark 2.6 (fair reachability of predicates [44]). Most fairness assumptions have the form "if something is infinitely often possible then something happens infinitely often" and, in this respect, our formulation of fair run (Definition 2.2) looks slightly unconventional. However, it is not difficult to realize that Definition 2.2 is an instance of the notion of fair reachability of predicates as defined by Queille and Sifakis [44, Definition 3]. According to Queille and Sifakis, a run ρ is fair with respect to some predicate C ⊆ S if, whenever in ρ there are infinitely many states from which a state in C is reachable, then in ρ there are infinitely many

.P i } i∈I tag input/output | (s)(P 1 | • • • | P n ) session | A⟨u⟩ invocation | close u signal output | u[p]!v.P channel output | P ⊕ Q choice | ⌈u⌉P cast occurrences of states in C.
When we take C to be →, that is the set of terminated states that do not reduce, pretending that irreducible states should occur infinitely often in the run is nonsensical. So, the fairness assumption boils down to assuming that such states should not be reachable infinitely often, which is precisely the formulation of Definition 2.2. ⌟

A Calculus of Multiparty Sessions

In this section we define the calculus for multiparty sessions on which we apply our static analysis technique. The calculus is an extension of the one presented by Ciccone and Padovani [START_REF] Ciccone | Fair termination of binary sessions[END_REF] to multiparty sessions in the style of Scalas and Yoshida [45].

We use an infinite set of variables ranged over by x, y, z, an infinite set of session names ranged over by s and t, a set of roles ranged over by p, q, r, a set of message tags ranged over by m, and a set of process names ranged over by A, B, C. In the literature of sessions tags are usually called labels. We adopt a different terminology to avoid confusion with another notion of label that we introduce in Section 4. We use roles to distinguish the participants of a session. In particular, an endpoint s[p] consists of a session name s and a role p and is used by the participant with role p to interact with the other participants of the session s. We use u and v to range over channels, which are either variables or session endpoints. We write x and u to denote possibly empty sequences of variables and channels, extending this notation to other entities. We use π to range over the elements of the set {?, !} of polarities, distinguishing input actions (?) from output actions (!).

A program is a finite set of definitions of the form A(x) △ = P , at most one for each process name, where P is a term generated by the syntax shown in Table 1. The term done denotes the terminated process that performs no action. The term A⟨u⟩ denotes the invocation of the process with name A passing the channels u as arguments. When u is empty we just write A instead of A⟨⟩. The term close u denotes the process that sends a termination signal on the channel u, whereas wait u.P denotes the process that waits for a termination signal from channel u and then continues as P . The term u[p]!v.P denotes the process that sends the channel v on the channel u to the role p and then continues as P . Dually, u[p]?(x).P denotes the process that receives a channel from the role p on the channel u and then continues as P where x is replaced with the received channel. The term u[p]π{m i .P i } i∈I denotes a process that exchanges one of the tags m i on the channel u with the role p and then continues as P i . Whether the tag is sent or received depends on the polarity π and, as it will be clear from the operational semantics, the polarity π also determines whether the process behaves as an internal choice (when π is !) or an external choice (when π is ?). In the first case the process chooses actively the tag being sent, whereas in the second case the process reacts passively to the tag being received. We assume that I is finite and non-empty and also that the tags m i are pairwise distinct. For brevity, we write u[p]πm k .P k instead of u[p]π{m i .P i } i∈I when I is the singleton set {k}. The term P ⊕ Q denotes a process that non-deterministically behaves C V I T 2 0 1 6

23:6 Fair Termination of Multiparty Sessions

(s)(P | P | Q | Q) ≼ (s)(P | Q | P | Q) [s-par-assoc] (s)(P | (t)(R | Q)) ≼ (t)((s)(P | R) | Q) if s ∈ fn(R) [s-cast-comm] ⌈u⌉⌈v⌉P ≼ ⌈v⌉⌈u⌉P [s-cast-new] (s)(⌈s[p]⌉P | Q) ≼ (s)(P | Q) [s-cast-swap] (s)(⌈t[p]⌉P | Q) ≼ ⌈t[p]⌉(s)(P | Q) if s ̸ = t [s-call] A⟨u⟩ ≼ P {u/x} if A(x) △ = P
Table 3 Reduction of processes.

[r-choice]

P 1 ⊕ P 2 → P k k ∈ {1, 2} [r-signal] (s)(wait s[p].P | close s[q 1 ] | • • • | close s[q n ]) → P [r-channel] (s)(s[p][q]!v.P | s[q][p]?(x).Q | R) → (s)(P | Q{v/x} | R) [r-pick] (s)(s[p][q]!{m i .P i } i∈I | Q) → (s)(s[p][q]!m k .P k | Q) k ∈ I [r-tag] (s)(s[p][q]!m k .P | s[q][p]?{m i .Q i } i∈I | R) → (s)(P | Q k | R) k ∈ I [r-par] P → Q (s)(P | R) → (s)(Q | R) [r-cast] P → Q ⌈u⌉P → ⌈u⌉Q [r-struct] P ≼ P ′ P ′ → Q ′ Q ′ ≼ Q P → Q either as P or as Q. A term (s)(P 1 | • • • | P n )
with n ≥ 1 denotes the parallel composition of n processes, each of them being a participant of the session s. Each process is associated with a distinct a role p i and communicates in s through the endpoint s[p i ]. Combining session creation and parallel composition in a single form is common in session type systems based on linear logic [START_REF] Caires | Linear logic propositions as session types[END_REF]48,37] and helps guaranteeing deadlock freedom. Finally, a cast ⌈u⌉P denotes a process that behaves exactly as P . This form is only relevant for the type system (Section 5) and denotes the fact that the type of u is subject to an application of subtyping.

The free and bound names of a process are defined as usual, the latter ones being easily recognizable as they occur within round parenteses. We write fn(P ) for the set of free names of P and we identify processes modulo renaming of bound names. Note that fn(P ) may contain variables and session names, but not endpoints. Occasionally we write A(x) △ = P as a predicate or side condition, meaning that P is the process associated with the process name A. For each of such definitions we assume that fn(P ) ⊆ {x}.

The operational semantics of processes is given by the structural precongruence relation ≼ defined in Table 2 and the reduction relation → defined in Table 3. As usual, structural precongruence allows us to rearrange the structure of processes without altering their meaning, whereas reduction expresses an actual computation or interaction step. The adoption of a structural precongruence (as opposed to a more common congruence relation) is not strictly necessary, but it simplifies the technical development by reducing the number of cases we have to consider in proofs without affecting the properties of the calculus in any way.

Rules [s-par-comm] and [s-par-assoc] state commutativity and associativity of parallel composition of processes (we write P to denote possibly empty parallel compositions of processes). In [s-par-assoc], the side condition s ∈ fn(R) makes sure that R is indeed a participant of the session s. Note that this rule only states right-to-left associativity. Left-to-right associativity is derivable from this rule and repeated uses of [s-par-comm]. Rule [s-cast-comm] allows us to swap two consecutive casts. Rule [s-cast-new] removes an unguarded cast on an endpoint of the restricted session (we refer to this operation as "performing the cast"). Rule [s-cast-swap] swaps a cast and a restricted session as long as the endpoint in the cast refers to a different session. Finally, rule [s-call] unfolds a process invocation to its definition. Hereafter, we write {u/x} for the capture-avoiding substitution of each free occurrence of x with u and {u/x} for its natural extension to equal-length tuples of variables and names. The rules [s-cast-new], [s-cast-swap] and [s-call] are not invertible: by [s-cast-new] casts can only be removed but never added; by [s-cast-swap] casts can only be moved closer to their restriction, so that they can be eventually performed by [s-cast-new]; by [s-call] process invocations can only be unfolded.

The reduction relation is quite standard. Rule [r-choice] reduces P 1 ⊕ P 2 to either P 1 or P 2 , non deterministically. Rule [r-signal] terminates a session in which all participants (q 1 , . . . , q n ) but one (p) are sending a termination signal and p is waiting for it; the resulting process is the continuation of the participant p. Rule [r-channel] models the exchange of a channel among two participants of a session. Rule [r-pick] models an internal choice whereby a process picks one particular tag m k to send on a session. Rule [r-tag] synchronizes two participants p and q on the tag chosen by p. Finally, rules [r-par], [r-cast] and [r-struct] close reductions under parallel compositions and casts and by structural precongruence.

In the rest of this section we illustrate the main features of the calculus with some examples. For none of them the existing multiparty session type systems are able to guarantee progress. ▶ Example 3.1 (purchase). We model a particular instance of the buyer-seller-carrier interaction that we have informally discussed in Section 1 with the following definitions: Note that the buyer either sends pay or it sends two add messages in a row before repeating this behavior. That is, this particular buyer always adds an even number of items to the shopping cart. Nonetheless, the buyer periodically has a chance to send a pay message and terminate. Therefore, the execution of the program in which the buyer only sends add is unfair according to Definition 2.2 hence this program is fairly terminating. ⌟ ▶ Example 3.2 (purchase with negotiation). Consider a variation of Example 3.1 in which the buyer, before making the payment, negotiates with a secondary buyer for an arbitrarily long time. The interaction happens in two nested sessions, an outer one involving the primary buyer, the seller and the carrier, and an inner one involving only the two buyers. We model C V I T 2 0 1 6

Main △ = (s)(Buyer⟨s[buyer]⟩ | Seller⟨s[seller]⟩ | Carrier⟨s[carrier]⟩) Buyer(x) △ = x[seller]!{add.x[

23:8

Fair Termination of Multiparty Sessions the interaction as the program below, in which we collapse role names to their initials. The buyer queries the seller which replies with a price. At this point, Buyer creates a new session t and forks as a primary buyer Buyer 1 and a secondary buyer Buyer 2 . The interaction between the two sub-buyers goes on until either Buyer 1 gives up or Buyer 2 accepts its share of the price. In the former case, the primary buyer waits for the internal session to terminate and cancels the order with the seller which, in turn, aborts the transaction with the carrier. In the latter case, the buyer confirms the order to the seller, which then instructs the carrier to ship a box to the buyer.

Main △ = (s)(Buyer⟨s[b]⟩ | Seller⟨s[s]⟩ | Carrier⟨s[c]⟩) Buyer(x) △ = x[s]!query.x[s]?price.(t)(Buyer 1 ⟨x, t[b 1 ]⟩ | Buyer 2 ⟨t[b 2 ]⟩) Seller(x) △ = x[
Note that the outermost session s, taken in isolation, terminates in a bounded number of interactions, but its progress cannot be established without assuming that the innermost session t terminates. In particular, if the two buyers keep negotiating forever, the seller and the carrier starve. However, the innermost session can terminate if Buyer 1 sends giveup to Buyer 2 or if Buyer 2 sends yes to Buyer 1 . Thus, the run in which the two buyers negotiate forever is unfair, the session t fairly terminates and the session s terminates as well.

On the technical side, note that the definition of Buyer 1 contains two casts on the variable x. As we will see in Example 6.1, these casts are necessary for the typeability of Buyer 1 to account for the fact that x is used differently in two distinct branches of the process. ⌟ ▶ Example 3.3 (parallel merge sort). To illustrate an example of program that creates an unbounded number of sessions we model a parallel version of the merge sort algorithm. The program starts as a single session s in which a master m sends the initial collection of data to the worker w as a req message and waits for the result. The worker is modeled as a process Sort that decides whether to sort the data by itself (right branch of the choice in Sort), in which case it sends the result directly to the master, or to partition the collection (left branch of the choice in Sort). In the latter case, it creates a new session t in which it sends requests to two sub-workers w 1 and w 2 , it gathers the partial results from them and gets back to the master with the complete result.

Main △ = (s)(s[m][w]!req.s[m][w]?res.wait s.done | Sort⟨s[w]⟩) Sort(x) △ = x[m]?req.((t)(Merge⟨x, t[m]⟩ | Sort⟨t[w 1 ]⟩ | Sort⟨t[w 2 ]⟩) ⊕ x[m]!res.close x) Merge(x, y) △ = y[w 1 ]!req.
Since a worker may always choose to start two sub-workers in a new session, the number of sessions that may be created by this program is unbounded. At the same time, each worker may also choose to complete its task without creating new sessions. So, while in principle there exists a run of this program that keeps creating new sessions forever, this run is unfair according to Definition 2.2. ⌟

Multiparty Session Types and Fair Subtyping

In this section we define syntax and semantics of multiparty session types (Section 4.1) as well as an inference system for fair subtyping (Section 4.2).

Syntax and Semantics

A session type is a regular tree [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF] coinductively generated by the productions below:

Session type S, T, U, V ::= πend | i∈I pπm i .S i | pπS.T
The session type πend describes the behavior of a process that sends/receives a termination signal. The session type i∈I pπm i .S i describes the behavior of a process that sends to or receives from the participant p one of the tags m i and then behaves according to S i . Note that the source or destination role p and the polarity π are the same in every branch. We require that I is not empty and i, j ∈ I with i ̸ = j implies m i ̸ = m j . Occasionally we write

pπm 1 .S 1 + • • • + pπm n .S n instead of n i=1 pπm i .S i .
Finally, a session type pπS.T describes the behavior of a process that sends to or receives from the participant p an endpoint of type S and then behaves according to T . We often specify infinite session types as solutions of equations of the form S = • • • where the metavariable S may occur on the right hand side of = guarded by at least one prefix. A regular tree satisfying such equation is guaranteed to exist and to be unique [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF].

In order to describe a whole multiparty session at the level of types we introduce the notion of session map.

▶ Definition 4.1 (session map).

A session map is a finite, partial map from roles to session types written {p i ▷ S i } i∈I . We let M and N range over session maps, we write dom(M ) for the domain of M , we write M | N for the union of M and N when dom(M ) ∩ dom(N ) = ∅, and we abbreviate the singleton map {p ▷ S} as p ▷ S.

We describe the evolution of a session at the level of types by means of a labeled transition system for session maps. Labels are generated by the grammar below:

Label ℓ ::= τ | α Action α, β ::= π✓ | p ▷ qπm | p ▷ qπS
The label τ represents either an internal action performed by a participant independently of the others or a synchronization between two participants. The labels of the form π✓ describe the input/output of termination signals, whereas the labels of the form p ▷ qπm and p ▷ qπS represent the input/output of a tag m or of an endpoint of type S.

The labeled transition system is defined by the rules in Table 4, most of which are straightforward. Rule [l-pick] models the fact that the participant p may internally choose one particular tag m k before sending it to q. The chosen tag is not negotiable with the receiver. Rule [l-terminate] models termination of a session. A session terminates when there is exactly one participant waiting for the termination signal and all the others are sending it. This property follows from a straightforward induction on the derivation of

M ?✓ -→ N using [l-terminate] and [l-end].
The existence of a single participant waiting for the termination signal ensures that there is a uniquely determined continuation process after the session has been closed. Finally, rule [l-sync] models the synchronization between two participants performing complementary actions. The complement of an action α, denoted by α, is the partial operation defined by the equations

p ▷ qπm def = q ▷ pπm p ▷ qπS def = q ▷ pπS C V I T 2 0 1 6

23:10 Fair Termination of Multiparty Sessions

Table 4 Labeled transition system for session maps.

[l-end]

p ▷ πend π✓ --→ p ▷ πend [l-channel] p ▷ qπU.S p▷qπU ----→ p ▷ S [l-pick] p ▷ i∈I q!m i .S i τ -→ p ▷ q!m k .S k k ∈ I [l-tag] p ▷ i∈I qπm i .S i p▷qπm k -----→ p ▷ S k k ∈ I [l-tau] M τ -→ M ′ M | N τ -→ M ′ | N [l-terminate] M ?✓ -→ M ′ N !✓ -→ N ′ M | N ?✓ -→ M ′ | N ′ [l-sync] M α -→ M ′ N α -→ N ′ M | N τ -→ M ′ | N ′
where π denotes the complement of the polarity π. The complement of actions of the form π✓ is undefined, so rule [l-sync] cannot be applied to terminated sessions. Hereafter we write ⇒ for the reflexive, transitive closure of τ -→ and α =⇒ for the composition ⇒ α -→. We call coherence the property of multiparty sessions that we wish to enforce with our type system, namely the fact that a session can always terminate no matter how it evolves. We formulate coherence directly on the transition system of session maps, in line with the approach of Scalas and Yoshida [45] and without introducing global types.

▶ Definition 4.2. We say that M is coherent, notation #M , if M ⇒ N implies N ?✓ =⇒.
The term "coherence" is borrowed from Carbone et al. [START_REF] Carbone | Coherence generalises duality: A logical explanation of multiparty session types[END_REF][START_REF] Carbone | Multiparty session types as coherence proofs[END_REF], although the property is actually stronger than the one of Carbone et al. as it entails fair termination of multiparty sessions through Theorem 2.5. In particular, if we consider the reduction system whose states are session maps and whose reduction relation is The session map buyer ▷ S b | seller ▷ S s | carrier ▷ S c is coherent. To see that, consider any interaction between the buyer and the seller. One of two cases applies: either the buyer has sent an even number of add messages to the seller, in which case it can send pay and the session eventually terminates, or the buyer has sent an odd number of add messages to the seller, in which case it can send one more add message followed by a pay message and once again the session eventually terminates. ⌟

Coherence allows us to provide a semantic definition of fair subtyping, the relation that defines the safe substitution principle for session endpoints in our type system. ▶ Definition 4.4 (fair subtyping). We say that S is a fair subtype of T , notation S ⊑ T , if M | p ▷ S coherent implies M | p ▷ T coherent for every M and p. Definition 4.4 does not say much about the properties of fair subtyping except for the fact that it is a coherence-preserving preorder. For this reason, we devote Section 4.2 to Table 5 Inference system for fair subtyping.

[f-end] πend ⩽ n πend [f-channel] S ⩽ n T pπU.S ⩽ n pπU.T [f-tag-in] ∀i ∈ I : S i ⩽ ni T i ∀i ∈ I : n i ≤ n i∈I p?m i .S i ⩽ n i∈I∪J p?m i .T i [f-tag-out-1] ∀i ∈ I : S i ⩽ ni T i ∀i ∈ I : n i ≤ n i∈I p!m i .S i ⩽ n i∈I p!m i .T i [f-tag-out-2] ∀i ∈ I : S i ⩽ ni T i ∃i ∈ I : n i < n i∈I∪J p!m i .S i ⩽ n i∈I p!m i .T i
defining an alternative characterization of fair subtyping that highlights its relationship with the standard subtyping relation for session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF].

Inference System for Fair Subtyping

Consider the relation ⩽ n coinductively defined by the inference system in Table 5, where n ranges over natural numbers. The characterization of fair subtyping that we consider is the relation

⩽ def = n∈N ⩽ n .
The rules for deriving S ⩽ n T are quite similar to those of the standard subtyping relation for session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]: [f-end] states reflexivity of subtyping on terminated session types; [f-channel] relates higher-order session types with the same polarity and payload type; [f-tag-in] is the usual covariant rule for the input of tags (the set of tags in the larger session type includes those in the smaller one); [f-tag-out-2] is the usual contravariant rule for the output of tags (the set of tags in the smaller session type includes those in the larger one). Overall, these rules entail a "simulation" between the behaviors described by S and T whereby all inputs offered by S are also offered by T and all outputs performed by T are also performed by S. The main differences between ⩽ and the subtyping relation of Gay and Hole [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] are the presence of an invariant rule for outputs [f-tag-out-1] and the natural number n annotating each subtyping judgment S ⩽ n T . Intuitively, this number estimates how much S and T differ in terms of performed outputs. In all rules but [f-tag-out-2], the annotation in the conclusion of the rule is just an upper bound of the annotations found in the premises. In [f-tag-out-2], where the sets of output tags in related session types may differ, the annotation n is required to be a strict upper bound for at least one of the premises. That is, there must be at least one premise in which the annotation strictly decreases, while no restriction is imposed on the others. Intuitively, this ensures the existence of a tag shared by the two related session types whose corresponding continuations are slightly less different. So, the annotation n provides an upper bound to the number of applications of [f-tag-out-2] along any path (i.e. any sequence of actions) shared by S and T that leads to termination. In the particular case when n = 0, the rule [f-tag-out-2] cannot be applied, so that T may perform all the outputs also performed by S. ▶ Example 4.5. Consider the session type S = seller!add.S + seller!pay.!end, which describes the behavior of the buyer in Equation ( 1) purchasing an arbitrary number of items, T = seller!add.seller!add.T +seller!pay.!end, which describes the behavior of the buyer in Example 3.1 always purchasing an even number of items, and U = seller!add.U , which describes the behavior of a buyer attempting to purchase an infinite number of items without ever paying C V I T 2 0 1 6

23:12 Fair Termination of Multiparty Sessions

the seller. We have S ⩽ T and S ̸ ⩽ U . Indeed, we can derive . . .

S ⩽ 1 T [f-tag-out-2] S ⩽ 2 seller!add.T [f-end] !end ⩽ 0 !end [f-tag-out-2] S ⩽ 1 T
but there is no derivation for S ⩽ n U no matter how large n is chosen. Note that there are infinitely many sequences of actions of S that cannot be performed by both T and U . In particular, T cannot perform any sequence of actions consisting of an odd number of add outputs followed by a pay output, whereas U cannot perform any sequence of add outputs followed by a pay output. Nonetheless, there is a path shared by S and T that leads into a region of S and T in which no more differences are detectable. The annotations in the derivation tree measures the distance of each judgment from such region. In the case of S and U , there is no shared path that leads to a region where no differences are detectable. ⌟ ▶ Example 4.6. Consider the session types S = player?play.(player!win.S + player!lose.S) + player?quit.!end and T = player?play.player!lose.T + player?quit.!end describing the behavior of two slot machines, an unbiased one in which the player may win at every play and a biased one in which the player never wins. If we try to build a derivation for S ⩽ n T we obtain . . .

S ⩽ n-1 T [f-tag-out-1] player!win.S + player!lose.S ⩽ n player!lose.T [f-end] !end ⩽ n !end [f-tag-in] S ⩽ n T
which would contain an infinite branch with strictly decreasing annotations. Therefore, we have S ̸ ⩽ T . In this case there exists a shared path leading into a region of S and T in which no more differences are detectable between the two protocols, but this path starts from an input. The fact that S is not a fair subtype of T has a semantic justification. Think of a player that deliberately insists on playing until it wins. This is possible when player interacts with the unbiased slot machine S but not with the biased one T . ⌟

In the rest of this section we study the fundamental properties of ⩽, starting from the non-obvious fact that it is a preorder.

▶ Theorem 4.7. ⩽ is a preorder. While reflexivity of ⩽ is trivial to prove (since [f-tag-out-2]
is never necessary, it suffices to only consider judgments with a 0 annotation), transitivity is surprisingly complex. The challenging part of proving that from S ⩽ m U and U ⩽ n T we can derive S ⩽ k T is to come up with a feasible annotation k. As it turns out, such k depends not only on m and n, but also on annotations found in different regions of the derivation trees that prove S ⩽ m U and U ⩽ n T . In particular, the "difference" of S and T is not simply the "maximum difference" or "the sum of the differences" of S and U and of U and T . More in detail, we first show that we can always find a derivation of S ⩽ m U where the rank annotations of all judgements occurring in it are below some h ≥ m; then, the judgement S ⩽ k T is provable for k = m + (1 + h)n. For previous characterizations of fair subtyping [39, 41, 12, 13], transitivity has been established indirectly by relating the inference system of fair subtyping (Table 5) with its semantic definition (Definition 4.4). For Theorem 4.7 we are able to provide a direct proof (cf. Appendix B.1). Now we establish the connection between ⩽ and ⊑ (Definition 4.4). First of all, we prove that ⩽ is coherence-preserving just like ⊑ is.

▶ Theorem 4.8 (soundness). If S ⩽ T then S ⊑ T .
The proof of this result relies on a key property of ⩽ not enjoyed by the usual subtyping relation on session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]: when S ⩽ T and M | p ▷ S is coherent, the session map M | p ▷ T can successfully terminate. The rank annotation on subtyping judgements is used to set up an appropriate inductive argument for proving this property.

Theorem 4.8 alone suffices to justify the adoption of ⩽ as fair subtyping relation, but we are interested in understanding to which extent ⩽ covers ⊑. In this respect, it is quite easy to see that there exist session types that are related by ⊑ but not by ⩽. For example, consider S = p!a.S and T = p?b.T and observe that these two session types describe completely different protocols (the output of infinitely many a's in the case of S and the input of infinitely many b's in the case of T ). In particular, we have S ̸ ⩽ T and T ̸ ⩽ S but also S ⊑ T and T ⊑ S. That is, S and T are unrelated according to ⩽ but they are equivalent according to ⊑. This equivalence is justified by the fact that there exists no coherent session map in which S and T could play any role, because none of them can ever terminate.

This discussion hints at the possibility that, if we restrict the attention to those session types that can terminate, which are the interesting ones as far as this work is concerned, then we can establish a tighter correspondence between ⩽ and ⊑. We call such session types bounded, because they describe protocols for which termination is always within reach.

▶ Definition 4.9 (bounded session type). We say that a session type is bounded if all of its subtrees contain a πend leaf.

Note that a finite session type is always bounded but not every bounded session type is finite. If we consider the reduction system in which states are session types and we have S → T if T is an immediate subtree of S, then S is bounded if and only if S is fairly terminating. Now, for the family of bounded session types we can prove a relative completeness result for ⩽ with respect to ⊑.

▶ Theorem 4.10 (relative completeness). If S is bounded and S ⊑ T then S ⩽ T .

The proof of Theorem 4.10 is done by contradiction. We show that, for any bounded S, if S ⩽ T does not hold then we can build a session map M called discriminator such that M | p ▷ S is coherent and M | p ▷ T is not, which contraddicts the hypothesis S ⊑ T . The boundedness of S is necessary to make sure that it is always possible to find a session map N such that N | p ▷ S is coherent.

Type System

In this section we describe the type system for the calculus of multiparty sessions of Section 3. The typing judgments have the form Γ ⊢ n P , meaning that the process P is well typed in the typing context Γ and has rank n. As usual, the typing context is a map associating channels with session types and is meant to contain an association for each name in fn(P ). We write u 1 : S 1 , . . . , u n : S n for the map with domain {u 1 , . . . , u n } that associates u i with S i . Occationally we write u : S for the same context, when the number and the specific associations are unimportant. We also assume that endpoints occurring in a typing context have different session names. That is, s[p], s[q] ∈ dom(Γ) implies p = q. This constraint makes sure that each well-typed process plays exactly one role in each of the sessions in

C V I T 2 0 1 6
u : !end ⊢ n close u [t-channel-in] Γ, u : T, x : S ⊢ n P Γ, u : p?S.T ⊢ n u[p]?(x).P [t-channel-out] Γ, u : T ⊢ n P Γ, u : p!S.T, v : S ⊢ n u[p]!v.P [t-tag] ∀i ∈ I : Γ, u : S i ⊢ n P i Γ, u : i∈I pπm i .S i ⊢ n u[p]π{m i .P i } i∈I [t-choice] Γ ⊢ n1 P 1 Γ ⊢ n2 P 2 Γ ⊢ n k P 1 ⊕ P 2 k ∈ {1, 2} [t-cast] Γ, u : T ⊢ n P Γ, u : S ⊢ m+n ⌈u⌉P S ⩽ m T [t-par] ∀i ∈ {1, . . . , h} : Γ i , s[p i ] : S i ⊢ ni P i Γ 1 , . . . , Γ h ⊢ 1+n1+•••+n h (s)(P 1 | • • • | P h ) #{p i ▷ S i } i=1..h [co-tag] Γ, u : S k ⊢ n P k Γ, u : i∈I pπm i .S i ⊢ n u[p]π{m i .P i } i∈I = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = k ∈ I [co-choice] Γ ⊢ n P k Γ ⊢ n P 1 ⊕ P 2 = = = = = = = = = = = = k ∈ {1, 2}
which it participates. It is also a common assumption made in all multiparty session calculi. We use Γ and ∆ to range over typing contexts, we write ∅ for the empty context and Γ, ∆ for the union of Γ and ∆ when they have disjoint domains and disjoint sets of session names.

The rank n in a typing judgment estimates the number of sessions that P has to create and the number of casts that P has to perform in order to terminate. The fact that the rank is finite suggests that so is the effort required by P to terminate.

The typing rules are shown in Table 6 as a generalized inference system [START_REF] Ancona | Generalizing inference systems by coaxioms[END_REF][START_REF] Dagnino | Coaxioms: flexible coinductive definitions by inference systems[END_REF][START_REF] Ciccone | Flexible coinduction in agda[END_REF][START_REF] Dagnino | Flexible Coinduction[END_REF] in which, roughly speaking, the singly-lined rules are interpreted coinductively and the doublylined rules -called corules -are interpreted inductively. We will come back with a more detailed intuition later on (Definition 5.1), although we will not provide a formal definition of the interpretation of a generalized inference system in this paper. The interested reader may refer to the cited literature for details. We type check a program {A i (x i ) △ = P i } i∈I under a global set of assignments {A i : [S i ; n i ]} i∈I associating each process name A i with a tuple of session types S i , one for each of the variables in x i , and a rank n i . The program is well typed if x i : S i ⊢ ni P i is derivable for every i ∈ I, establishing that the tuple S i corresponds to the way the variables x i are used by P i and that n i is a feasible rank annotation for P i . We now describe the typing rules in detail.

The rule [t-done] states that the terminated process is well typed in the empty context, to make sure that no unused channels are left behind. Note that done can be given any rank, since it performs no casts and it creates no new sessions. The rule [t-call] checks that a process invocation A⟨u⟩ is well typed by unfolding A into the process associated with A. The types associated with u must match those of the global assignment A : [S; n] and the rank of the process must be no greater than that of the invocation. The potential mismatch between the two ranks improves typeability in some corner cases. The rules [t-wait] and [t-close] concern processes that exchange termination signals. The channel being closed is consumed and, in the case of [t-wait], no longer available in the continuation P . Again, close u can be typed with any rank whereas the rank of wait u.P coincides with that of P . The rules [t-channel-in] and [t-channel-out] deal with the exchange of channels in a quite standard way. Note that the actual type of the exchanged channel is required to coincide with the expected one. In particular, no covariance or contravariance of input and output respectively is allowed. Relaxing the typing rule in this way would introduce implicit applications of subtyping that may compromise fair termination [START_REF] Ciccone | Fair termination of binary sessions[END_REF]. In our type system, each application of subtyping must be explicitly accounted for as we will see when discussing [t-cast]. Rule [t-tag] deals with the exchange of tags. Channels that are not used for such communication must be used in the same way in all branches, whereas the type of the channel on which the message is exchanged changes accordingly. All branches are required to have the same rank, which also corresponds to the rank of the process. Unlike other presentations of this typing rule [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF], we require the branches in the process to be matched exactly by those in the type. Again, this is to avoid implicit application of subtyping, which might jeopardize fair termination. The rule [t-choice] deals with non-deterministic choices and requires both continuations to be well typed in the same typing context. The judgment in the conclusion inherits the rank of one of the processes, typically the one with minimum rank. As we will see in Example 6.3, this makes it possible to model finite-rank processes that may create an unbounded number of sessions or that perform an unbounded number of casts.

The rule [t-cast] models the substitution principle induced by fair subtyping: when S ⩽ m T , a channel of type S can be used where a channel of type T is expected or, in dual fashion [START_REF] Gay | Subtyping supports safe session substitution[END_REF], a process using u according to T can be used in place of a process using u according to S. To keep track of this cast, the rank in the conclusion is augmented by the weight m of the subtyping relation between S and T . Note that the typing rule guesses the target type of the cast.

Finally, the rule [t-par] deals with session creation and parallel composition. This rule is inspired to the multiparty cut rule found in linear logic interpretations of multiparty session types [START_REF] Carbone | Coherence generalises duality: A logical explanation of multiparty session types[END_REF][START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] and provides a straightforward way for enforcing deadlock freedom. Each process in the composition must be well typed in a slice of the typing context augmented with the endpoint corresponding to its role. The session map of the new session must be coherent, implying that it fairly terminates. The rank of the composition is one plus the aggregated rank of the composed processes, to account for the fact that one more session has been created. Recall that coherence is a property expressed on the LTS of session maps (Definition 4.2) in line with the approach of Scalas and Yoshida [45].

The typing rules described so far are interpreted coinductively. That is, in order for a rank n process P to be well typed in Γ there must be a possibly infinite derivation tree built with these rules and whose conclusion is the judgment Γ ⊢ n P . But in a generalized inference system like the one we are defining, this is not enough to establish that P is well typed. In addition, it must be possible to find finite derivation trees for all of the judgments occurring in this possibly infinite derivation tree using the discussed rules and possibly the corules, which we are about to describe. Since the additional derivation trees must be finite, all of their branches must end up with an application of [t-done] or [t-close], which are the only axioms in Table 6 corresponding to the only terminated processes in Table 1. So, the purpose of these finite typing derivations is to make sure that in every well-typed (sub-)process there exists a path that leads to termination. On the one hand, this is a sensible condition to require as our type system is meant to enforce fair process termination. On the other hand, insisting that these finite derivations can be built using only the typing rules discusses thus far is overly restrictive, for a process might have one path that leads to termination, but also alternative paths that lead to (recursive) process invocations. In fact, all of the processes we have discussed in Examples 3.1-3.3 are structured like this. The two corules [co-choice] and [co-tag] in Table 6 establish that, whenever a multi-branch process is dealt with, it suffices for one of the branches to lead to termination. A key detail to note in the case of [co-choice] is that the rank of the non-deterministic choice coincides with that of the branch that leads to termination. This makes sense recalling that the rank associated with a process represents the overall effort required for that process to terminate.

Let us recap the notion of well-typed process resulting from the typing rules of Table 6.

▶ Definition 5.1 (well-typed process). We say that P is well typed in the context Γ and has rank n if [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF] there exists an arbitrary (possibly infinite) derivation tree obtained using the (singly-lined) rules in Table 6 and whose conclusion is Γ ⊢ n P and ( 2) for each judgment in such tree there is a finite derivation obtained using the rules and the (doubly-lined) corules.

▶ Remark 5.2. The term "corule" seems to suggest that the rule should be coinductively interpreted. As we have seen above (Definition 5.1), corules are interpreted inductively. We have chosen to stick with the terminology used in the works that introduced generalized inference systems [START_REF] Ancona | Generalizing inference systems by coaxioms[END_REF][START_REF] Dagnino | Coaxioms: flexible coinductive definitions by inference systems[END_REF]. x : We can prove a strong soundness result for our type system, stating that well-typed, closed processes can always successfully terminate no matter how they reduce.

S b ⊢ 0 Buyer⟨x⟩ [t-tag] x : seller!add.S b ⊢ 0 x[seller]!add.Buyer⟨x⟩ [t-close] x : !end ⊢ 0 close x [t-tag] x : S b ⊢ 0 x[
▶ Theorem 5.4 (soundness). If ∅ ⊢ n P and P ⇒ Q, then Q ⇒≼ done.
There are several valuable implications of Theorem 5.4 on a well-typed, closed process P : Deadlock freedom. If Q cannot reduce any further, then it must be (structurally precongruent to) done, namely there are no residual input/output actions. Fair termination. Under the fairness assumption, Theorem 2.5 assures that P eventually reduces to done. This also implies that every session created by P eventually terminates. Progress. If Q contains a sub-process with pending input/output actions, the fact that Q may reduce to done means that these actions are eventually performed.

The proof of Theorem 5.4 is essentially composed of a standard subject reduction result showing that typing is preserved by reductions and a proof that every well-typed process other than done may always reduce in such a way that a suitably defined well-founded measure strictly decreases. The measure is a lexicographically ordered pair of natural numbers with the following meaning: the first component measures the number of sessions that must be created and the total weight of casts that must be performed in order for the process to terminate (this information is essentially the rank we associate with typing judgments); the second component measures the overall effort required to terminate every session that has already been created (these sessions are identified by the fact that their restriction occurs unguarded in the process). We account for this effort by measuring the shortest reduction that terminates a coherent session map (Definition 4.2). The reason why we need two quantities in the measure is that in general every application of fair subtyping may increase the length of the shortest reduction that terminates a coherent session map. So, when casts are performed the second component of the measure may increase, but the first component reduces. As a final remark, it should be noted that the overall measure associated with a well-typed process may also increase, for example if new sessions are created (Example 3.3). However, one particular reduction that decreases the measure is always guaranteed to exist.

We conclude this section discussing a few more examples that motivate the features of the type system that are key for ensuring fair program termination.

▶ Example 5.5. To see simple examples of processes whose ill/well typing crucially depends on the fact that we use a generalized inference system consider the definitions

A △ = A B △ = B ⊕ B C △ = C ⊕ done
which define a stuck process A, a diverging process B and a fairly terminating process C that admits an infinite reduction. For them we can find the infinite typing derivations below:

. . .

[t-call] ∅ ⊢ 0 A [t-call] ∅ ⊢ 0 A . . . . . . [t-call] ∅ ⊢ 0 B [t-choice] ∅ ⊢ 0 B ⊕ B [t-call] ∅ ⊢ 0 B . . . [t-call] ∅ ⊢ 0 C [t-done] ∅ ⊢ 0 done [t-choice] ∅ ⊢ 0 C ⊕ done ∅ ⊢ 0 C
However, only for C it is possible to find a finite typing derivation using the corule [cochoice]. So, A and B are ill typed, whereas C is well typed. This is consistent with the fact that only C can always reduce to the successfully terminated process done. ⌟ ▶ Example 5.6 (infinitely ranked processes). The mere existence of a path that leads to termination ensured by the generalized interpretation of the typing rules in Table 6 does not always guarantee that the process is actually able to terminate. An example where this is the case is shown by the process A defined as

A △ = (s)(s[p][q]!{a.close s[p], b.wait s[p].A} | s[q][p]?{a.wait s[q].A, b.close s[q]})
which creates a session s and splits as two parallel sub-processes connected by s. Each sub-process has a path that leads to termination but, because of the way they synchronize, when one sub-process terminates the other one restarts A. For A it would be possible to build a finite typing derivation with the help of [co-tag], but A is ill typed because it cannot be assigned a finite rank, since it creates a new session at each recursive invocation. Further examples of infinitely ranked processes, including ones where the rank is affected by the presence of casts, are discussed by Ciccone and Padovani [START_REF] Ciccone | Fair termination of binary sessions[END_REF] for binary sessions and can be easily reframed in our multiparty setting.

⌟ We wish to build a typing derivation showing that Buyer 1 has rank 1 and uses x and y respectively according to S and T , where S = s!ok.c?box.?end + s!cancel.?end and T = b 2 !split.(b 2 ?yes.?end + b 2 ?no.T ) + b 2 !giveup.?end. As it has been noted previously, what makes this process interesting is that it uses the endpoint x differently depending on the messages it exchanges with b 2 on y. Since rule [t-tag] requires any endpoint other than the one on which messages are exchanged to have the same type, the only way Buyer 2 can be declared well typed is by means of the casts that occur in its body. For the branch in which Buyer 1 proposes to split the payment we obtain the following derivation tree:

C V I T
[t-done] ∅ ⊢ 0 done [t-wait]
y : ?end ⊢ 0 wait y.done [t-wait] x : ?end, y : ?end ⊢ 0 wait x . . .

[t-tag]

x : c?box.?end, y : ?end ⊢ 0 x[c]?box . . .

[t-tag]

x : s!ok.c?box.?end, y : ?end ⊢ 0 x[s]!ok . . .

[t-cast]

x : S, y : ?end ⊢ 1 ⌈x⌉ • • • . . .

[t-call]

x : S, y : T ⊢ 1 Buyer 1 ⟨x, y⟩ For the branch in which Buyer 1 sends giveup we obtain the following derivation tree:

[t-done] ∅ ⊢ 0 done [t-wait]
x : ?end ⊢ 0 wait x.done

x : s!cancel.?end ⊢ 0 x[s]!cancel.wait x.done

[t-cast] x : S ⊢ 1 ⌈x⌉x[s]!cancel.wait x.done [t-wait]
x : S, y : ?end ⊢ 1 wait y.

⌈x⌉x[s]!cancel.wait x.done

Once again the cast is necessary to change the type of x, but this time leveraging on the fair subtyping relation S ⩽ 1 s!cancel.?end. These two derivations can then be combined to complete the proof that the body of Buyer 1 is well typed: . . . . . .

[t-tag]

x : S, y :

T ⊢ 1 y[b 2 ]!{split . . . , giveup . . . }
Clearly, it is also necessary to find finite derivation trees for all of the judgments shown above. This can be easily achieved using the corule [co-tag]. ⌟ ▶ Example 6.2. Casts can be useful to reconcile the types of a channel that is used differently in different branches of a non-deterministic choice. For example, below is an alternative modeling of Buyer from Example 3.1 where we abbreviate seller to s for convenience:

B(x) △ = ⌈x⌉x[s]!add.x[s]!add.B⟨x⟩ ⊕ ⌈x⌉x[s]!pay.close x
Note that x is used for sending two add messages in the left branch of the non-deterministic choice and for sending a single pay message in the right branch. Given the session type S = s!add.S + s!pay.!end and using the fair subtyping relations S ⩽ 2 s!add.s!add.S and S ⩽ 1 s!pay.!end we can obtain the following typing derivation for the body of B:

. . .

[t-call]

x : S ⊢ where T = m!res.!end, U = m?req.T and V = w 1 !req.w 2 !req.w 1 ?res.w 2 ?res.?end.

For the branch of Sort that creates a new session we obtain the derivation tree . . .

[t-call]

x :

T, t[m] : V ⊢ 0 Merge⟨x, t[m]⟩ . . . [t-call], i = 1, 2 t[w i ] : U ⊢ 0 Sort⟨t[w i ]⟩ [t-par] x : T ⊢ 1 (t)(Merge⟨x, t[m]⟩ | Sort⟨t[w 1 ]⟩ | Sort⟨t[w 2 ]⟩) C V I T 2 0 1 6

23:20 Fair Termination of Multiparty Sessions

where the rank 1 derives from the fact that the created session involves three zero-ranked participants. For the body of Sort we obtain the following derivation tree: . . .

[t-par] x : T ⊢ 1 (t)(Merge⟨x, t[m]⟩ | Sort⟨t[w 1 ]⟩ | • • • ) [t-close] x : !end ⊢ 0 close x [t-tag] x : T ⊢ 0 x[m]!res.close x [t-choice] x : T ⊢ 0 (t)(Merge⟨x, t[m]⟩ | Sort⟨t[w 1 ]⟩ | • • • ) ⊕ x[m]!res.close x [t-tag] x : U ⊢ 0 x[m]?req.((t)(Merge⟨x, t[m]⟩ | Sort⟨t[w 1 ]⟩ | • • • ) ⊕ x[m]!res.close x)
In the application of the rule [t-choice], the rank of the whole choice coincides with that of the branch in which no new sessions are created. This way we account for the fact that, even though Sort may create a new session, it does not have to do so in order to terminate. ⌟

Related Work

Fair termination of binary sessions. Our type system is both a refinement and an extension of the one presented by Ciccone and Padovani [START_REF] Ciccone | Fair termination of binary sessions[END_REF], which ensures the fair termination of binary sessions. The main elements of the two type systems are closely related, but there are some key differences. In that work, the fairness assumption being made is strong fairness [START_REF] Francez | Fairness[END_REF][START_REF] Krzysztof | Appraising fairness in languages for distributed programming[END_REF][START_REF] Kwiatkowska | Survey of fairness notions[END_REF]46] which guarantees fair termination of binary sessions at the level of types but not necessarily at the level of processes. The key difference between types and processes is that types generate finite-state reduction systems (because of their regularity) whereas processes may generate infinite-state reduction systems. While strong fairness is known to be the strongest possible fairness assumption for finite-state systems [47], it is not strong enough to make the right-to-left direction of Theorem 2.5 hold for infinite-state systems. In fact, it can be shown that strong fairness and the fairness assumption we make in this work (Definition 2.2) are unrelated for infinite-state reduction systems, in the sense that there exist fair runs that are not strongly fair and there exist strongly fair runs that are not fair runs. The fairness assumption we make in this work is general enough so that it can be related to both types (Definition 4.2) and processes (Theorem 5.4) through Theorem 2.5.

The main advantage of working with native multiparty sessions is that they enable the natural modeling of interactions involving multiple participants in possibly cyclic network topologies, like those in Examples 3.2 and 3.3. Another difference and contribution of our work compared to the one of Ciccone and Padovani [START_REF] Ciccone | Fair termination of binary sessions[END_REF] is that the definition of the fair subtyping relation is simpler. In particular, the inference system we provide (Table 5) does not make use of corules [START_REF] Ciccone | Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types[END_REF][START_REF] Ciccone | Fair termination of binary sessions[END_REF] nor does it require auxiliary predicates [39,41].

Liveness properties of multiparty sessions.

The enforcement of liveness properties has always been a key aspect of session type systems, although previous works have almost exclusively focused on progress rather than on (fair) termination. Scalas and Yoshida [45] define a general framework for ensuring safety and liveness properties of multiparty sessions.

In particular, they define a hierarchy of three liveness predicates to characterize "live" sessions that enjoy progress. They also point out that the coarsest liveness property in this hierarchy, which is the one more closely related to fair termination, cannot be enforced by their type system. In part, this is due to the fact that their type system relies on a standard subtyping relation for session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] instead of fair subtyping [39, 41]. As we have seen in Section 5, even for single-session programs the mere adoption of fair subtyping is not enough and it is necessary to meet additional requirements (Examples 5.5 and 5.6). The work of van Glabbeek et al.

[47] presents a type system for multiparty sessions that ensures progress and is not only sound but also complete. The fairness assumption they make -called justness -is substantially weaker than our own (Definition 2.2) and such that the unfair runs are those in which some interactions between participants are systematically discriminated in favor of other interactions involving a disjoint set of independent participants. For this reason, their progress property is in between the two more restrictive liveness predicates of Scalas and Yoshida [45] and can only be guaranteed when it is independent of the behavior of the other participants of the same session. In the end, simple sessions like those described in Examples 3.1-3.3 fall outside the scope of these works as far as liveness properties are concerned.

Another major difference between our work and the ones cited above [45, 47] is that fair termination, unlike progress, enables compositional reasoning and so we are able to enforce a global liveness property (Theorem 5.4) even in the presence of multiple sessions (see Examples 3.2 and 3.3). Notable examples of multiparty session type systems ensuring progress also in the presence of multiple (possibly interleaved) sessions are provided by Padovani et al. [42] and by Coppo et al. [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF]. This is achieved by a rich type structure that prevents mutual dependencies between different sessions. In any case, these works do not address sessions in which progress may depend on choices made by session participants.

Termination of binary sessions. Termination is a liveness property that can be guaranteed when finite session types are considered [43]. As soon as infinite session types are considered, many session type systems weaken the guaranteed property to deadlock freedom. Lindley and Morris [37] define a type system for a functional language with session primitives and recursive session types that is strongly normalizing. That is, a well-typed program along with all the sessions it creates is guaranteed to terminate. This strong result is due to the fact that the type language is equipped with least and greatest fixed point operators that are required to match each other by duality. Termination is strictly stronger than fair termination. In particular, there exist fairly terminating programs that are not terminating because they allow reductions of unbounded length (see Examples 3.1-3.3).

Liveness properties in the π-calculus. Kobayashi [START_REF] Kobayashi | A type system for lock-free processes[END_REF] defines a behavioral type system that guarantees lock freedom in the π-calculus. Lock freedom is a liveness property akin to progress for sessions, except that it applies to any communication channel (shared or private). Padovani [40] adapts and extends the type system of Kobayashi [START_REF] Kobayashi | A type system for lock-free processes[END_REF] to enforce lock freedom in the linear π-calculus [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], into which binary sessions can be encoded [START_REF] Dardha | Session types revisited[END_REF]. All of these works annotate types with numbers representing finite upper bounds to the number of interactions needed to unblock a particular input/output action. For this reason, none of our key examples (Examples 3.1-3.3) is in the scope of these analysis techniques. Kobayashi and Sangiorgi [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF] show how to enforce lock freedom by combining deadlock freedom and termination. Our work can be seen as a generalization of this approach whereby we enforce lock freedom by combining deadlock freedom (through a mostly conventional session type system) and fair termination. Since fair termination is coarser than termination, the family of programs for which lock freedom can be proved is larger as well.

Deadlock freedom. Our type system enforces deadlock freedom essentially thanks to the shape of the rule [t-par] which is inspired to the cut rule of linear logic. This rule has been applied to session type systems for binary sessions [48,[START_REF] Caires | Linear logic propositions as session types[END_REF]37] and subsequently extended to multiparty sessions [START_REF] Carbone | Coherence generalises duality: A logical explanation of multiparty session types[END_REF][START_REF] Carbone | Multiparty session types as coherence proofs[END_REF]. In the latter case, the rule -dubbed multiparty cut -requires a coherence condition among cut types establishing that the session types followed by the single C V I T 2 0 1 6

23:22 Fair Termination of Multiparty Sessions

participants adhere to a so-called global type describing the multiparty session as a whole. The rule [t-par] adopts with schema, except that the coherence condition is stronger to entail fair session termination. The key principle of these formulations of the cut rule as a typing rule for parallel processes is to impose a tree-like network topology, whereby two parallel processes can share at most one channel. In the multiparty case, cyclic network topologies can be modeled within each session (Example 3.3) since coherence implies deadlock freedom.

Having a single construct that merges session restriction and parallel composition allows for a simple formulation of the typing rules so that dealock freedom is easily guaranteed. However, many session calculi separate these two forms in line with the original presentation of the π-calculus. We think that our type system can be easily reformulated to support distinct session restriction and parallel composition by means of hypersequents [START_REF] Kokke | Taking linear logic apart[END_REF][START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF].

A more liberal version of the cut rule, named multi-cut and inspired to Gentzen's "mix" rule, is considered by Abramsky et al. [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF] enabling processes to share more than one channel. In this setting, deadlock freedom is lost but can be recovered by means of a richer type structure that keeps track of the dependencies between different channels. This approach has been pioneered by Kobayashi [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] for the π-calculus and later on refined by Padovani [40]. Other approaches to ensure deadlock freedom based on dependency/connectivity graphs that capture the network topology implemented by processes have been studied by Carbone and Debois [START_REF] Carbone | A graphical approach to progress for structured communication in web services[END_REF], Kobayashi and Laneve [START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF], de'Liguoro and Padovani [START_REF] De | Mailbox types for unordered interactions[END_REF], and Jacobs et al. [START_REF] Jacobs | Connectivity graphs: a method for proving deadlock freedom based on separation logic[END_REF].

Concluding Remarks

Sessions ought to terminate. Until recently this property has been granted only for sessions whose duration is bounded. In this work we have presented the first type system ensuring the fair termination of multiparty sessions, that is a termination property under the assumption that, if termination is always reachable, then it is eventually achieved. Fair termination is stronger than weak termination but substantially weaker than strong normalization. In particular, fair termination does not rule out infinite runs of well-typed processes as long as they purposefully eschew termination. When fair termination is combined with the usual safety properties of sessions, it entails a strong progress property whereby any pending action is eventually performed. Our type system is the first ensuring such strong progress property for multiparty (and possibly multiple) sessions.

A cornerstone element of the type system is fair subtyping, a coherence-preserving refinement of the standard subtyping relation for session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]. In this work, we have also contributed a new characterization of fair subtyping (Table 5 and Theorems 4.8 and 4.10) that is substantially simpler than previous ones [39,41,[START_REF] Ciccone | Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types[END_REF][START_REF] Ciccone | Fair termination of binary sessions[END_REF] since it does not require auxiliary predicates nor the use of a generalized inference system [START_REF] Ancona | Generalizing inference systems by coaxioms[END_REF][START_REF] Dagnino | Coaxioms: flexible coinductive definitions by inference systems[END_REF][START_REF] Ciccone | Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types[END_REF][START_REF] Ciccone | Fair termination of binary sessions[END_REF]. Thanks to this new characterization we have been able to prove the transitivity of fair subtyping (Theorem 4.7) without relying on its (relative) completeness with respect to its semantic counterpart (Definition 4.4).

The decidability of fair subtyping and of type checking follow from analogous results for binary sessions [START_REF] Ciccone | Fair termination of binary sessions[END_REF]. The rank of processes can be inferred using the same algorithm that works for the binary case [13, auxiliary material]. Considering that fair subtyping for multiparty session types coincides with fair subtyping for binary session types except for the presence of roles, it would be easy to adapt the type checking tool FairCheck [START_REF] Ciccone | Faircheck[END_REF] to the process language we consider in this paper. The most relevant difference would be the algorithm for deciding the coherence of a session map, which is somewhat more complex than that for the compatibility between two session types. As for the binary setting, to which extent the type system is amenable to full type reconstruction is yet to be established. In particular, a hypothetical type inference algorithm would have to be able to solve fair subtyping inequations and this problem has not been investigated yet. Another open question that may have a relevant practical impact is whether the type system remains sound in a setting where communications are asynchronous. We expect the answer to be positive, as is the case for other synchronous multiparty session types systems [45], but we have not worked out the details yet.

In this paper we have focused on the theoretical aspects of fairly terminating multiparty sessions. A natural development of this work is its application to a real programming environment. We envision two approaches that can be followed to this aim. A bottom-up approach may apply our static analysis technique to a program (in our process calculus) that is extracted from actual code and that captures the code's communication semantics. We expect that suitable annotations may be necessary to identify those branching parts of the code that represent non-deterministic choices in the program. Most typically, these branches will correspond to finite loops or to queries made to the human user of the program that have several different continuations. A top-down approach may provide programmers with a generative tool that, starting from a global specification in the form of a global type [START_REF] Honda | Multiparty asynchronous session types[END_REF], produces template code that is "well-typed by design" and that the programmer subsequently instantiates to a specific application. Scribble [49, 2] is an example of such a tool. Interestingly, the usual notion of global type projectability is not sufficient to entail that the session map resulting from a projection is coherent. However, coherence would be guaranteed by requiring that the projected global type is fairly terminating.

Finally, we plan to investigate the adaptation of the type system for ensuring the fair termination in the popular actor-based model. This is a drastically different setting in which the order of messages is not as controllable as in the case of sessions. As a consequence, type based analyses require radically different formalisms such as mailbox types [START_REF] De | Mailbox types for unordered interactions[END_REF], for which the study of fair subtyping and of type systems enforcing fair termination is unexplored.

A Supplement to Section 2

Proof of Lemma 2.3. Let D be the last state of ρ. We distinguish two possibilities: if D is weakly terminating, then there exists a finite maximal run Dρ ′ of D; if D is diverging, then there exists an infinite run Dρ ′ of D such that no state in ρ ′ is weakly terminating. In both cases we conclude by noting that ρρ ′ is a maximal fair run. ◀ Proof of Theorem 2.5. (⇒) Let D be a state reachable from C. That is, there exists a finite run ρ of C ending with D. By Lemma 2.3 we deduce that this run can be extended to a maximal fair one ρρ ′ . From the hypothesis that C is fairly terminating we deduce that ρρ ′ is finite. Hence, D is weakly terminating. (⇐) Let C 0 C 1 . . . be an infinite fair run of C. Using the hypothesis we deduce that each C i is weakly terminating, which is absurd. Hence, either there are no maximal fair runs or every maximal fair run of C is finite, but the first case is not possible by Lemma 2.3, thus C is fairly terminating. ◀

B Supplement to Section 4.2

In this section we prove that ⩽ (Table 5) is a preorder and also that it is sound and (relatively) complete with respect to ⊑ (Definition 4.4). To do so it is convenient to introduce some more notation concerning the lebeled transition system of sessions (Table 4). We write Proof. The "if" part is obvious. Concerning the "only if" part, it suffices to show that each judgment in the set

S def = {U ⩽ m V | U ⩽ m V ∧ ∄n < m : U ⩽ n V }
is derivable from premises that are also in S. This is enough to prove S ⩽ m n T from S ⩽ n T , because in S there is at most one judgment U ⩽ n V for each pair of session types U and V and, by regularity of U and V , the derivation of U ⩽ n V obtained using judgments in S contains finitely many annotations, which must have a maximum.

Suppose U ⩽ m V ∈ S. Then U ⩽ m V is derivable. We reason by cases on the last rule applied to derive this judgment.

Case [f-end]. Then U = V = πend and there is nothing left to prove since [f-end] has no premises.

Case [f-tag-in]. Then U = i∈I p?m i .U i and V = i∈J p?m i .V i and I ⊆ J and U i ⩽ ni V i and n i ≤ m for every i ∈ I. By definition of S we have that, for every i ∈ I, there exists

m i ≤ n i such that U ⩽ mi V i ∈ S. Then U ⩽ m V is derivable by [f-tag-in] using premises in S.
Case [f-tag-out-1]. Analogous to the previous case.

Case [f-tag-out-2].
Then U = i∈I p!m i .U i and V = i∈J p!m i .V i and J ⊆ I and U i ⩽ ni V i for every i ∈ J and n k < m for some k ∈ I. By definition of S we have that, for

C V I T 2 0 1 6 every i ∈ J, there exists m i ≤ n i such that U ⩽ mi V i ∈ S. In particular, m k ≤ n k < m. Then U ⩽ m V is derivable by [f-tag-out-2] using premises in S.
◀ Proof of Theorem 4.7. The proof that ⩽ is reflexive is trivial, since S ⩽ n S is derivable for every n. Concerning transitivity, by Lemma B.1 it suffices to show that each judgment in the set

S def = {S ⩽ n1+(1+m)n2 T | S ⩽ m n1 U ∧ U ⩽ n2 T }
is derivable using the rules in Table 5 from premises that are also in S. Suppose S ⩽ n T ∈ S.

Then there exist U , n 1 , m and n 2 such that S ⩽ m n1 U and U ⩽ n2 T and n = n 1 + (1 + m)n 2 . We reason by cases on the last rules applied to derive S ⩽ n1 U and U ⩽ n2 T .

Case [f-end]. Then S = U = T = πend hence S ⩽ n T is derivable by [f-end]. Case [f-tag-in].
Then S = i∈I p?m i .S i and U = i∈J p?m i .U i and T = i∈K p?m i .T i and I ⊆ J ⊆ K and S i ⩽ m n1i U i and n 1i ≤ n 1 for every i ∈ I and U i ⩽ n2i T i and n 2i ≤ n 2 for every i ∈ J. By definition of S we have that

S i ⩽ n1i+(1+m)n2i T i ∈ S for every i ∈ I. Observe that n 1i + (1 + m)n 2i ≤ n 1 + (1 + m)n 2 = n for every i ∈ I hence S ⩽ n T is derivable by [f-tag-in]. Case [f-tag-out-1]. Then S = i∈I p!m i .S i and U = i∈I p!m i .U i and T = i∈I p!m i .T i and S i ⩽ m n1i U i and n 1i ≤ n 1 and U i ⩽ n2i T i and n 2i ≤ n 2 for every i ∈ I. By definition of S we have that S i ⩽ n1i+(1+m)n2i T i ∈ S for every i ∈ I. Observe that n 1i + (1 + m)n 2i ≤ n 1 + (1 + m)n 2 = n for every i ∈ I hence S ⩽ n T is derivable by [f-tag-out-1]. Case [f-tag-out-1] and [f-tag-out-2].
Then S = i∈I p!m i .S i and U = i∈I p!m i .U i and T = i∈J p!m i .T i and J ⊆ I and S i ⩽ m n1i U i and n 1i ≤ n 1 for every i ∈ I and U i ⩽ n2i T i for every i ∈ J and n 2k < n 2 for some k ∈ J. By definition of S we have that

S i ⩽ n1i+(1+m)n2i T i ∈ S for every i ∈ J. Observe that n 1k + (1 + m)n 2k < n 1 + (1 + m)n 2 = n hence S ⩽ n T is derivable by [f-tag-out-2].
Case [f-tag-out-2] and [f-tag-out-1]. Then S = i∈I p!m i .S i and U = i∈J p!m i .U i and T = i∈J p!m i .T i and J ⊆ I and S i ⩽ m n1i U i for every i ∈ J and n 1k < n 1 for some k ∈ J and U i ⩽ n2i T i for every i ∈ J and n 2i ≤ n 2 for every i ∈ J. By definition of S we have that

S i ⩽ n1i+(1+m)n2i T i ∈ S for every i ∈ J. Observe that n 1k + (1 + m)n 2k < n 1 + (1 + m)n 2 = n hence S ⩽ n T is derivable by [f-tag-out-2].
Case [f-tag-out-2]. Then S = i∈I p!m i .S i , U = i∈J p!m i .U i and T = i∈K p!m i .T i and K ⊆ J ⊆ I and S i ⩽ m n1i U i for every i ∈ J and n 1j < n 1 for some j ∈ J and U i ⩽ n2i T i for every i ∈ K and n 2k < n 2 for some k ∈ K. By definition of S we have that S i ⩽ n1i+(1+m)n2i T i ∈ S for every i ∈ K. Observe that

n 1k + (1 + m)n 2k ≤ m + (1 + m)n 2k since n 1k ≤ m < 1 + m + (1 + m)n 2k = (1 + m)(1 + n 2k ) ≤ (1 + m)n 2 since n 2k < n 2 < n 1 + (1 + m)n 2 since n 1j < n 1 hence S ⩽ n T is derivable by [f-tag-out-2]. ◀

B.2 Proof of Theorem 4.8

We start with an auxiliary result formalizing the simulation entailed by the relation S ⩽ T .

▶ Lemma B.2. If S ⩽ T and M | p ▷ S is coherent and M | p ▷ T ⇒ N | p ▷ T ′ , then M | p ▷ S ⇒ N | p ▷ S ′ for some S ′ ⩽ T ′ .
Proof. We prove the result for a single reduction

M | p ▷ T τ -→ N | p ▷ T ′ .
The general statement then follows by a straightforward induction on the length of the reduction M | p ▷ T ⇒ N | p ▷ T ′ using the fact that coherence is preserved by reductions.

Case M τ -→ N . Then T ′ = T and we conclude by taking

S ′ def = S. Case p ▷ T τ -→ p ▷ T ′′ . Then p ▷ T = p ▷ i∈I q!m i .T i τ -→ p ▷ q!m k .T k = p ▷ T ′ for some k ∈ I.
From the hypothesis S ⩽ T we deduce S = i∈J q!m i .S i where I ⊆ J and S i ⩽ T i for every i ∈ I. Now we have

M | p ▷ S τ -→ M | p ▷ q!m k .S k and also q!m k .S k ⩽ T ′ . We conclude by taking S ′ def = q!m k .S k . Case M q▷p!m ---→ N and p ▷ T p▷q?m
----→ p ▷ T ′ . Then T = i∈I q?m i .T i and m = m k and T ′ = T k for some k ∈ I. From the hypothesis S ⩽ T we deduce S = i∈J q?m i .S i and J ⊆ I and S i ⩽ T i for every i ∈ J. From the hypothesis M | p ▷ S coherent we deduce k ∈ J or else the participant p would not be able to receive the m tag. We conclude by taking

S ′ def = S k . Case M q▷p?m ----→ N and p ▷ T p▷q!m ---→ p ▷ T ′ . Then T = i∈I q!m i .
T i and m = m k and T ′ = T k for some k ∈ I. From the hypothesis S ⩽ T we deduce S = i∈J q!m i .S i and I ⊆ J and S i ⩽ T i for every i ∈ I. We conclude by taking

S ′ def = S k . Case M q▷p!U ---→ N and p ▷ T p▷q?U ----→ p ▷ T ′ .
Then T = q?U.T ′ . From the hypothesis S ⩽ T we deduce S = q?U.S ′ and S ′ ⩽ T ′ . We conclude by observing that

M | p ▷ S τ -→ N | p ▷ S ′ . Case M q▷p?U ----→ N and p▷T p▷q!U ---→ p▷T ′ . Then T = q!U.T ′ . From the hypothesis S ⩽ T we deduce S = q!U.S ′ and S ′ ⩽ T ′ . We conclude by observing that M | p ▷ S τ -→ N | p ▷ S ′ . ◀
Next we show that S ⩽ T preserves the termination of any session map that completes S into a coherent one.

=⇒.

Case φ = p ▷ q?mψ. Then S = i∈I q?m i .S i and m = m k for some k ∈ I. From the hypothesis S ⩽ n T and [f-tag-in] we deduce T = i∈J q?m i .T i and I ⊆ J and S i ⩽ ni T i and n i ≤ n for every i ∈ I. We conclude using the induction hypothesis.

Case φ = p ▷ q!mψ. Then S = i∈I q!m i .S i and m = m k for some k ∈ I. We distinguish two sub-cases, according to the last rule used in the derivation of S ⩽ n T . If the last rule was [f-tag-out-1], then T = i∈I q!m i .T i and S i ⩽ ni T i and n i ≤ n for every i ∈ I. In particular, S k ⩽ n k T k and n k ≤ n and we conclude using the induction hypothesis. If the last rule was [f-tag-out-2], then T = i∈J q!m i .T i with J ⊆ I and S i ⩽ ni T i for every i ∈ J and n j < n for some j ∈ J. In particular, we have S j ⩽ nj T j and we conclude using the induction hypothesis.

◀ Proof of Theorem 4.8. Consider a run M | p ▷ T ⇒ N | p ▷ T ′ . From Lemma B.2 we deduce that there exists S ′ ⩽ T ′ such that M | p ▷ S ⇒ N | p ▷ S ′ . From the hypothesis that M | p ▷ S is coherent we deduce N | p ▷ S ′ is also coherent. From Lemma B.3 we conclude N | p ▷ T ′ ?✓ =⇒. ◀ C V I T 2 0 1 6

23:30 Fair Termination of Multiparty Sessions

Table 7 Inference system for unfair subtyping.

[u-end]

πend ⩽ * πend [u-channel] S ⩽ * T pπU.S ⩽ * pπU.T [u-tag-in] ∀i ∈ I : S i ⩽ * T i i∈I p?m i .S i ⩽ * i∈I∪J p?m i .T i [u-tag-out] ∀i ∈ I : S i ⩽ * T i i∈I∪J p!m i .S i ⩽ * i∈I p!m i .T i

B.3 Proof of Theorem 4.10

The proof of Theorem 4.10 is by contradiction, showing that from the hypothesis S ̸ ⩽ T we are able to find a session map M that is coherent when completed by S but not when it is completed by T . For this proof we need some auxiliary notions and notation. First of all, we consider unfair subtyping as the subtyping relation ⩽ * coinductively defined by the rules in Table 7. It is straightforward to see that ⩽ ⊆ ⩽ * . Then, we introduce some convenient notation for building session maps. To do this, we assume the existence of an arbitrary total order < on the set of roles. Now, given a finite set of roles {p 1 , . . . , p n } where p 1 < • • • < p n , we write {p 1 , . . . , p n }!m.S for the session type p 1 !m • • • p n !m.S. Given a finite family {M i } i∈I of session maps all having the same domain {q} ⊆ D ⊆ Roles \ {p}, we write q ▷ i∈I pπm i .M i for the session map M having domain D and such that

M (r) def = i∈I pπm i .D \ {q}!m i .M i (q) if r = q i∈I q?m i .M i (r) if r ̸ = q
for every r ∈ D. As suggested by the notation, this session map realizes a conversation in which q first interacts with p by exchanging a tag m i and then it informs all the other participants about the tag that has been exchanged. This session map has the property

M q:pπm k ----→⇒ M i for every k ∈ I.
Similarly, given a session map N with domain D ⊇ {q}, we write q ▷ pπU.N for the session map M with domain D such that

M (r) def = pπU.N (q) if r = q N (r) if r ∈ D \ {p, q}
for every r ∈ D. Note that M has the property

M q:pπU ----→ N
The first key step is showing that S ⊑ T implies S ⩽ * T when S is a bounded session type. That is, unfair subtyping is a necessary condition for fair subtyping to hold. 5 from premises that satisfy the same property. Let S ⩽ * T ∈ S. Then S is bounded and S ⊑ T . We reason by cases on the shape of S.

Case S = πend. Consider M def = q ▷ πend and observe that M | p ▷ S is coherent. Then M | p ▷ T is coherent as well, which implies T = πend. We conclude by observing that πend ⩽ * πend is derivable with [u-end].

Case S = i∈I q!m i .S i . Let {M i } i∈I be a family of session maps such that M i | p ▷ S i is coherent for every i ∈ I. Such family is guaranteed to exist from the hypothesis that S is bounded. Without loss of generality we may assume that the M i all have the same domain D ⊇ {q}. Let M def = q ▷ i∈I p?m i .M i and observe that M | p ▷ S is coherent by definition of M . Then M | p ▷ T is coherent as well. We deduce that T = i∈J q!m i .T i and J ⊆ I and also that M i | p ▷ T i is coherent for every i ∈ J. Hence S i ⊑ T i for every i ∈ J, namely S i ⩽ * T i ∈ S for every i ∈ J by definition of S. We conclude by observing that S ⩽ * T is derivable by [u-tag-out].

Case S = i∈I q?m i .S i . Let {M i } i∈I be a family of session maps such that M i | p ▷ S i is coherent for every i ∈ I. Such family is guaranteed to exist from the hypothesis that S is bounded. Without loss of generality we may assume that the M i all have the same domain D ⊇ {q}. Let M def = q ▷ i∈I p!m i .M i and observe that M | p ▷ S is coherent by definition of M . We deduce that T = i∈J q?m i .T i and I ⊆ J and also that M i | p ▷ T i is coherent for every i ∈ I. Hence S i ⊑ T i for every i ∈ I, namely S i ⩽ * T i ∈ S for every i ∈ I by definition of S. We conclude by observing that S ⩽ * T is derivable by [u-tag-in].

Case S = qπU.S ′ . Let N be a session map such that N | p ▷ S ′ is coherent. Such N is guaranteed to exist from the hypothesis that S is bounded. Let M def = q ▷ pπU.N and observe that M | p ▷ S is coherent by definition of M . We deduce that T = qπU.T ′ and also that N | p ▷ T ′ is coherent. Hence S ′ ⊑ T ′ , namely S ′ ⩽ * T ′ ∈ S by definition of S. We conclude by observing that S ⩽ * T is derivable by [u-channel].

◀

Next we show that every bounded session type may be part of a coherent session map. This result is somewhat related to the notion of duality in binary session type theories [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], showing that every behavior can be completed by a matching -dual -one.

▶ Definition B.5 (duality). Let targets(•) be the function that yields the set of roles occurring in a session type, let S be a bounded session type and D be a non-empty set of roles that includes targets(S) but not p. Let dual D (p ▷ S) be the session map corecursively defined by the following equations: wg(πend, πend) = 0 wg( i∈I p?m i .S i , i∈J p?m i .T i ) = max i∈I wg(S i , T i ) I ⊆ J wg( i∈I p!m i .S i , i∈J p!m i .T i ) = 1 + min i∈J wg(S i , T i ) J ⊊ I wg( i∈I p!m i .S i , i∈I p!m i .T i ) = min{1 + min i∈I wg(S i , T i ), max i∈I wg(S i , T i )} wg(pπU.S ′ , pπU.T ′ ) = wg(S ′ , T ′ )

dual D (p ▷ ?end) = {q ▷ !end} q∈D dual D (p ▷ !end) = min D ▷ ?end | {q ▷ !end} q∈D\{min D} dual D (p ▷ i∈I qπm i .S i ) = q ▷ i∈I pπm i .dual D (p ▷ S i ) dual D (p ▷ qπU.S) = q ▷ pπU.
To see that wg(S, T ) is well defined, observe that the system of equations defining wg(S, T ) under the hypothesis S ⩽ * T contains finitely many equations, say n, by regularity of S and T . The system is representable as a monotone endofunction F on the complete lattice (N ∪ {∞}) n . Thus, F has a least solution of which wg(S, T ) is a component.

We call two session types S and T divergent if they are related by unfair subtyping and have infinite rank. Then S = i∈I p?m i .S i and T = i∈J p?m i .T i with I ⊆ J and S i ⩽ * T i for every i ∈ I and ∞ = wg(S, T ) = max i∈I wg(S i , T i ). That is, wg(S k , T k ) = ∞ for some k ∈ I, hence we conclude S k ↑ T k .

Case [u-tag-out]. Then S = i∈I p!m i .S i and T = i∈J p!m i .T i with J ⊆ I and S i ⩽ * T i for every i ∈ J. We distinguish two sub-cases. If J ⊊ I then ∞ = wg(S, T ) = 1 + min i∈J wg(S i , T i ), that is wg(S i , T i ) = ∞ for every i ∈ J. If J = I then ∞ = wg(S, T ) = min{1 + min i∈I wg(S i , T i ), max i∈I wg(S i , T i )} ≤ 1 + min i∈I wg(S i , T i ) and we have wg(S i , T i ) = ∞ for every i ∈ I. Therefore, in both cases, we conclude S i ↑ T i for every i ∈ J.

Case [u-channel]. Then S = pπU.S ′ and T = pπU.T ′ and S ′ ⩽ * T ′ and ∞ = wg(S, T ) = wg(S ′ , T ′ ) hence we conclude S ′ ↑ T ′ . ◀

Finally, the key aspect of the proof of Lemma B.11 is how we build the session map M such that M | p ▷ S is coherent while M | p ▷ T is not.

▶ Definition B.10 (discriminator). Let disc(p, S, T ) be the session map corecursively defined by the following equations: disc(p, i∈I q?m i .S i , i∈J q?m i .T

i ) = q ▷ i∈I,Si↑Ti p!m i .disc(p, S i , T i ) if I ⊆ J disc(p, i∈I q!m i .S i , i∈J q!m i .T i ) = q ▷ i∈J q?m i .disc(p, S i , T i ) + i∈I\J q?m i .dual D (p ▷ S i ) if J ⊆ I disc(p,
S def = {S ⩽ wg(S,T ) T | S ⩽ @ T }
is derivable using one of the rules in Table 5 whose premises all belong to S. ◀

C Type System Soundness

In this section we provide lemmas and proofs required to prove Theorem 5.4. We write

h i=1 p i ▷ S i for p 1 ▷ S 1 | • • • | p 1 ▷ S 1 = {p h ▷ S h } i=1,...,h .
Concerning the notation about the transitions of session maps, we refer to Appendix B. Finally, we write Γ ⊢ ind P for the inductive type derivation.

C.1 Subject Reduction

′ | Q ′ | Q) ≼ (s)(P | Q ′ | P ′ | Q) = Q. From rule [t-par] we deduce that there exist Γ i , p i , S i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h n = 1 + h i=1 n i h i=1 p i ▷ S i coherent Γ i , s[p i ] : S i ⊢ ni P i for i = 1, . . . , k Γ k+1 , s[p k+1 ] : S k+1 ⊢ n k+1 P ′ Γ k+2 , s[p k+2 ] : S k+2 ⊢ n k+2 Q ′ Γ i , s[p i ] : S i ⊢ ni Q i for i = k + 3, . . . , h We conclude Γ ⊢ m Q with one application of [t-par] by taking m def = n. Case [s-par-assoc]. Then P = (s)(P | (t)(R | Q)) ≼ (t)((s)(P | R) | Q) = Q and s ∈ fn(R).
From rule [t-par] we deduce that there exist Γ i , p i , S i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h C V I T 2 0 1 6

23:34 Fair Termination of Multiparty Sessions

n = 1 + h i=1 n i h i=1 p i ▷ S i coherent Γ i , s[p i ] : S i ⊢ ni P i for i = 1, . . . , h -1 Γ h , s[p h ] : S h ⊢ n h (t)(R | Q)
From rule [t-par] and the hypothesis that s ∈ fn(R) we deduce that there exist ∆ i , q i , T i , m i for i = 1, . . . , k such that From rule [t-par] we deduce that there exist ∆, n ′ and Γ i , q i , n i for i = 1, . . . , h such that Γ = ∆, Γ 1 , . . . , Proof. By induction on the derivation of P → Q and by cases on the last rule applied.

Γ h = ∆ 1 , . . . , ∆ k n h = 1 + k 1 m i k 1 q i ▷ T i coherent ∆ 1 , s[p h ] : S h , t[q 1 ] : T 1 ⊢ m1 R ∆ i+1 , t[q i+1 ] : T i+1 ⊢ mi+1 Q i for i = 1, . . . , k -1 Using [t-par] we deduce Γ 1 , . . . , Γ h-1 , ∆ 1 , t[q 1 ] : T 1 ⊢ 1+ h-1 i=1 ni+m1 (s)(P | R). We conclude Γ ⊢ m (t)((s)(P | R) | Q) with another application of [t-par] by taking m def = n. Case [s-cast-comm]. Then P = ⌈u⌉⌈v⌉R ≼ ⌈v⌉⌈u⌉R = Q. We can assume u ̸ = v or else P = Q. From rule [t-cast] we deduce that there exist Γ 1 , S, T, n 1 , n u such that Γ = Γ 1 , u : S S ⩽ nu T n = n u + n 1 Γ 1 , u : T ⊢ n1 ⌈v⌉R From rule [t-cast] we deduce that there exist Γ 2 , S ′ , T ′ , n 2 , n v such that Γ 1 = Γ 2 , v : S ′ S ′ ⩽ nv T ′ n 1 = n v + n 2 Γ 2 , u : T, v : T ′ ⊢ n2 R We derive Γ 2 , u : S, v : T ′ ⊢ nu+n2 ⌈u⌉R
Γ h for i = 1, . . . , h n = 1 + n ′ + h i=1 n i p ▷ S | h i=1 q i ▷ S i coherent ∆, s[p] : S ⊢ n ′ ⌈s[p]⌉R Γ i , s[q i ] : S i ⊢ ni P i for i = 1, . . . , h From rule [t-cast] we deduce that there exist T, m ′ , m s such that S ⩽ ms T n ′ = m s + m ′ ∆, s[p] : T ⊢ m ′ R From p ▷ S | h i=1 q i ▷ S i coherent, S ⩽ ms T and Definition 4.4 we deduce p ▷ T | h i=1 q i ▷ S i coherent. We conclude with an application of [t-par] by taking m def = 1 + m ′ + h i=1 n i ≤ n. Case [s-cast-swap]. Then P = (s)(⌈t[p]⌉R | P ) ≼ ⌈t[p]⌉(s)(R | P ) = Q and t ̸ = s. From rule [t-par] we deduce that there exist Γ i , q i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h for i = 1, . . . , h n = 1 + h i=1 n i h i=1 q i ▷ S i coherent Γ 1 , s[q 1 ] : S 1 ⊢ n1 ⌈t[p]⌉R Γ i , s[q i ] : S i ⊢ ni P i for i = 2, . . . , h From rule [t-cast] we deduce that there exist ∆, T, n ′ , m t such that Γ 1 = ∆, t[p] : S S ⩽ mt T n 1 = m t + n ′ ∆, t[p] : T, s[q 1 ] : S 1 ⊢ n ′ R We derive ∆, t[p] : T, Γ 2 , . . . , Γ h ⊢ 1+n ′ + h i=2 ni (s)(R |
Case

[r-choice]. Then P = P 1 ⊕ P 2 → P k = Q and k ∈ {1, 2}. From [t-choice] we deduce that Γ ⊢ m Q for some m. Case [r-signal]. Then P = (s)(wait s[p].Q | close s[q 1 ] | • • • | close s[q h ]) → Q. From [t-
= 1 + m + h i=1 n i Γ, s[p] : ?end ⊢ m wait s[p].Q Γ ⊢ m Q s[q i ] : !end ⊢ ni close s[q i ] for i = 1, .

. . , h

There is nothing left to prove.

Case

[r-channel]. Then P = (s)(s[p][q]!v.P ′ | s[q][p]?(x).Q ′ | R) → (s)(P ′ | Q ′ {v/x} | R) = Q. From [t-par] we deduce that there exist Γ i , S i , p i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h n = 1 + h i=1 n i h i=1 p i ▷ S i coherent p = p 1 and q = p 2 Γ 1 , s[p] : S 1 ⊢ n1 s[p][q]!v.P ′ Γ 2 , s[q] : S 2 ⊢ n2 s[q][p]?(x).Q ′ Γ i , s[p i ] : S i ⊢ ni R i for i = 3, . . . , h From [t-channel-out] and [t-channel-in] we deduce that there exist S v , T 1 , T 2 , ∆ 1 such that S 1 = q!S v .T 1 Γ 1 = ∆ 1 , v : S v ∆ 1 , s[p] : T 1 ⊢ n1 P ′ S 2 = p?S v .T 2 Γ 2 , s[q] : T 2 , x : S v ⊢ n2 Q ′ Using Lemma C.1 we deduce Γ 2 , s[q] : T 2 , v : S v ⊢ n2 Q ′ {v/x}. Using Definition 4.2 we deduce p ▷ T 1 | q ▷ T 2 | h i=3 p i ▷ S i coherent. We conclude with one application of [t-par] taking m def = n. Case [r-pick]. Then P = (s)(s[p][q]!{m i .P i } i∈I | Q) → (s)(s[p][q]!m k .P k | Q) = Q and k ∈ I. From [t-par] we deduce that there exist Γ i , p i , n i , S i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h n = 1 + h i=1 n i h i=1 p i ▷ S i coherent p = p 1 and q = p i for some i ∈ {2, . . . , h} Γ 1 , s[p] : S 1 ⊢ n1 s[p][q]!{m i .P i } i∈I Γ i , s[p i ] : S i ⊢ ni Q i for i = 2, . . . , h From [t-tag] we deduce that there exist T i for all i ∈ I such that S 1 = i∈I q!m i .T i Γ 1 , s[p] : T i ⊢ n1 P i (i∈I)
C V I T 2 0 1 6

23:36 Fair Termination of Multiparty Sessions

From the hypothesis that k ∈ I we deduce that Γ

= n. Case [r-tag]. Then P = (s)(s[p][q]!m k .P ′ | s[q][p]?{m i .Q i } i∈I | R) → (s)(P ′ | Q k | R) = Q and k ∈ I. From [t-par] we deduce that there exist Γ i , S i , p i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h n = 1 + h i=1 n i h i=1 p i ▷ S i coherent p = p 1 and q = p 2 Γ 1 , s[p] : S 1 ⊢ n1 s[p][q]!m k .P ′ Γ 2 , s[q] : S 2 ⊢ n2 s[q][p]?{m i .Q i } i∈I Γ i , s[p i ] : S i ⊢ ni R i for i = 3, . . . , h
From [t-tag] we deduce that there exist S ′ 1 and T i for every i ∈ I such that

S 1 = q!m k .S ′ 1 Γ 1 , s[p] : S ′ 1 ⊢ n1 P ′ S 2 = i∈I p?m i .T i Γ 2 , s[q] : T i ⊢ n2 Q i (i∈I) From Definition 4.2 we deduce that p ▷ S ′ 1 | q ▷ T k | h i=2 p i ▷ S i coherent. We conclude with an application of [t-par] by taking m def = n. Case [r-par]. Then P = (s)(P ′ | R) → (s)(Q ′ | R) = Q and P ′ → Q ′ . From [t-par] we deduce that there exist Γ i , p i , S i , n i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h n = 1 + h i=1 n i h i=1 p i ▷ S i coherent Γ 1 , s[p 1 ] : S 1 ⊢ n1 P ′ Γ i , s[p i ] : S i ⊢ ni R i for i = 2, . . . , h Using the induction hypothesis on Γ 1 , s[p 1 ] : S 1 ⊢ n1 P ′ and P ′ → Q ′ we deduce Γ 1 , s[p 1 ] : S 1 ⊢ n ′ 1 Q ′ for some n ′ 1 .
We conclude with an application of [t-par] taking m We derive Γ 2 , u : S, v : T ′ ⊨ µ2+(mu,0) ⌈u⌉R with one application of [mt-cast] and we conclude with another application of [mt-cast] by taking ν we deduce that Γ ⊨ n A⟨u⟩ for some n such that µ = (n, 0). Using Lemma C.2 we deduce Γ ⊢ m Q for some m ≤ n. Using Lemma C.6 we deduce that Γ ⊨ ν Q for some ν ≤ (m, 0). We conclude observing that ν ≤ (m, 0) ≤ (n, 0) = µ. ◀

def = 1 + n ′ 1 + h i=2 n i . Case [r-cast]. Then P = ⌈u⌉P ′ → ⌈u⌉Q ′ = Q and P ′ → Q ′ . From [t-cast] we deduce that there exist S, T, Γ ′ , n ′ , m u such that Γ = Γ ′ , u : S S ⩽ mu T n = m u + n ′ Γ ′ , u : T ⊢ n ′ P ′ Using the induction hypothesis on Γ ′ , u : T ⊢ n ′ P ′ and P ′ → Q ′ we deduce Γ ′ , u : T ⊢ m ′ Q ′ for some m ′ . We conclude with an application of [t-cast] taking m def = m u + m ′ . Case [r-struct]. Then P ≼ P ′ → Q ′ ≼ Q. From Lemma C.2 we deduce that Γ ⊢ n ′ P ′ for some n ′ ≤ n. Using the induction hypothesis on Γ ⊢ n ′ P ′ and P ′ → Q ′ we deduce Γ ⊢ m ′ Q ′ for some m ′ .
def = µ. Case [s-cast-new]. Then P = (s)(⌈s[p]⌉R | P ) ≼ (s)(R | P ) = Q. From rule [mt-par] we deduce that there exist ∆, µ ′ , S and Γ i , q i , S i , µ i for i = 1, . . . , h such that Γ = ∆, Γ 1 , . . . , Γ h µ = µ ′ + h i=1 µ i + (0, ∥p ▷ S | h i=1 q i ▷ S i ∥) p ▷ S | h i=1 q i ▷ S i coherent ∆, s[p] : S ⊨ µ ′ ⌈s[p]⌉R Γ i , s[q i ] : S i ⊨ µi P i for i = 1, . . . , h From rule [mt-cast] we deduce that there exist T, ν ′ , m s such that S ⩽ ms T ν ′ = µ ′ + (m s , 0) ∆, s[p] : T ⊨ ν ′ R From p ▷ S | h i=1 q i ▷ S i coherent, S ⩽ ms T and Definition 4.4 we deduce p ▷ T | h i=1 q i ▷ S i coherent. We conclude with an application of [mt-par] by taking ν = ν ′ + h i=1 µ i + (0, ∥p ▷ S | h i=1 q i ▷ S i ∥) ≤ n. Case [s-cast-swap]. Then P = (s)(⌈t[p]⌉R | P ) ≼ ⌈t[p]⌉(s)(R | P ) = Q and t ̸ = s. From rule [mt-par] we deduce that there exist Γ i , q i , µ i for i = 1, . . . , h such that Γ = Γ 1 , . . . , Γ h µ = h i=1 µ i + (0, ∥ h i=1 q i ▷ S i ∥) h i=1 q i ▷ S i coherent Γ 1 , s[q 1 ] : S 1 ⊨ µ1 ⌈t[p]⌉R Γ i , s[q i ] : S i ⊨ µi P i for i = 2, . . . , h From rule [mt-cast] we deduce that there exist ∆, T, µ ′ , m t such that Γ 1 = ∆, t[p] : S S ⩽ mt T µ 1 = µ ′ + (m t , 0) ∆, t[p] : T, s[q 1 ] : S 1 ⊨ µ ′ R We derive ∆, t[p] : T, Γ 2 , . . . , Γ h ⊨ µ ′ + h i=2 µi+(0,∥

C.3 Normal Forms

We introduce process contexts to easily refer to unguarded sub-processes:

Process

23:40 Fair Termination of Multiparty Sessions

Intuitively, a process is in thread normal form if it consists of an initial prefix of casts followed by a parallel composition of threads, where a thread is either done or a process waiting to perform an input/output action on some channel u = s[p] for some p. In this latter case, we say that the thread is an s-thread.

▶ Definition C.10 (Proximity Normal Form). We say that P nf is in proximity normal form if P nf = C[(s)(P th )] for some C, s, P th where each P th i for i = 1, . . . , h is a s-thread.

▶ Lemma C.11. If Γ ⊢ n P and Γ ⊢ ind P , then there exists Q in choice normal form such that P ⇒ Q and Γ ⊢ m Q for some m ≤ n.

Proof. By induction on Γ ⊢ ind P and by cases on the last rule applied.

Case P is already in choice normal form. We conclude taking Q is used in the coinductive judgment as well. Using the induction hypothesis we deduce that there exist Q in choice normal form and m ≤ n ′ such that R{u/x} ⇒ Q and Γ ⊢ m Q. We conclude by observing that P ⇒ Q using [r-struct] and that m ≤ n ′ ≤ n.

Case [co-choice]. Then P = P 1 ⊕ P 2 . We deduce Γ ⊢ ind P k with k ∈ {1, 2}. Moreover, it must be the case that Γ ⊢ n P k since [t-choice] is used in the coinductive judgment. Using the induction hypothesis we deduce that there exist Q in choice normal form and m ≤ n such that P k ⇒ Q and Γ ⊢ m Q. We conclude by observing that P → P k by [r-choice].

Case [t-choice]. Analogous to the previous case but we consider the premise in which the rank is the same of the conclusion to keep sure that it does not increase.

Case [t-par]. Then P = (s)(P 1 | • • • | P h ). We deduce Γ = Γ 1 , . . . , Γ h Γ i , s[p i ] : S i ⊢ ind P i for i = 1, . . . , h h i=1 p i ▷ S i coherent Furthermore, it must be the case that Γ i , s[p i ] : S i ⊢ ni P i for i = 1, . . . , h and n = 1+ h i=1 n i since [t-par] is used in the coinductive judgment as well. Using the induction hypothesis we deduce that there exist Q i in choice normal form and m i ≤ n i such that P i ⇒ Q i and Γ i , s[p i ] : S i ⊢ mi Q i for i = 1, . . . , h. We conclude by taking Then P is a thread. We deduce that µ = (n, 0) for some n Γ ⊢ n P From Lemma C.12 we deduce that there exist Q and m ≤ n such that P ⇒ Q and Γ ⊢ m Q. From Lemma C.6 we deduce Γ ⊨ ν Q for some ν ≤ (m, 0). We conclude observing that ν ≤ (m, 0) ≤ (n, 0) = µ.

m def = 1 + h i=1 m i and Q def = (s)(Q 1 | • • • | Q h )
Case [mt-cast]. Then P = ⌈u⌉P ′ . We deduce that Γ = ∆, u : S S ⩽ n T µ = µ ′ + (n, 0) Γ ′ , u : T ⊨ µ ′ P ′ Using the induction hypothesis we deduce that there exist Q ′ and ν ′ ≤ µ ′ such that P ′ ⇒ Q ′ and Γ ′ , u : T ⊨ ν ′ Q ′ . We conclude with an application of Proof. By induction on the derivation of ∅ ⊨ µ P nf we deduce that P nf consists of s 1 , . . . , s h sessions and h i=1 k i -h + 1 threads where k i is the number of roles in s i . The scenarios in which no communication is possible are those in which for each session s i there are less than k i s i -threads. If we assume that for each s i there are k i -1 threads, then we obtain

h i=1 k i -h + 1 - h i=1 (k i -1) = h i=1 k i -h + 1 - h i=1 k i + h = 1

τ

  -→, then #M implies M fairly terminating. ▶ Example 4.3 (buyer-seller-carrier session map). Consider the session types S b = seller!add.seller!add.S b + seller!pay.!end S s = buyer?add.S s + buyer?pay.carrier!ship.!end S c = seller?ship.?end which describe the behavior of the processes Buyer, Seller and Carrier in Example 3.1.

  [t-tag]x : S, y : b 2 ?yes.?end + b 2 ?no.T ⊢ 1 y[b 2 ]?{yes . . . , no . . . } Note how the application of [t-cast] is key to change the type of x in the branch where the proposed split is accepted by b 2 . In that branch, x is deterministically used to send an ok message and we leverage on the fair subtyping relation S ⩽ 1 s!ok.c?box.?end.

- 7 ▶

 7 let φ and ψ range over strings of actions; we write ε for the empty string and |φ| for the length of φ; we write M ℓ -→ if there exists N such that M ℓ Lemma B.1. Let S ⩽ m n T if and only if S ⩽ n T is the conclusion of a derivation in which every rank annotation is at most m. Then S ⩽ n T if and only S ⩽ m n T for some m.

▶ Lemma B. 3 .

 3 If S ⩽ n T and M | p ▷ S is coherent, then M | p ▷ T ?✓ =⇒. Proof. By induction on the lexicographically ordered tuple (n, |φ|) where φ is any string of actions such that M φπ✓ = == ⇒ and p ▷ S φπ✓ = == ⇒. We know that at least one such φ least does exist from the hypothesis M | p ▷ S is coherent. We now reason by cases on the shape of φ. Case φ = ε. Then S = πend. From the hypothesis S ⩽ n T and [f-end] we deduce T = πend and we conclude M | p ▷ T ?✓

▶ Lemma B. 4 .

 4 If S is bounded and S ⊑ T then S ⩽ * T . Proof. Using the coinduction principle it suffices to show that each judgment in the set S def = {S ⩽ * T | S is bounded and S ⊑ T } is derivable by the rules in Table

6 23: 32 Fair

 632 dual D (p ▷ S) ▶ Lemma B.6 (duality). dual D (p ▷ S) | p ▷ S is coherent. Proof. Follows from the definition of dual D (p ▷ S). ◀ Now we provide an algorithmic way of computing the "difference" between two session types related by unfair subtyping. ▶ Definition B.7 (subtyping weight). Under the hypothesis S ⩽ * T , let wg(S, T ) ∈ N ∪ {∞} C V I T 2 0 1 Termination of Multiparty Sessions be the least solution of the system of equations below:

▶

  Definition B.8 (divergence). We write S ↑ T if S ⩽ * T and wg(S, T ) = ∞. ▶ Lemma B.9. If S ↑ T then the derivation of S ⩽ * T contains at least one application of [u-tag-out] with J ⊊ I and one of the following holds: 1. S = i∈I p?m i .S i and T = i∈J p?m i .T i with I ⊆ J and S k ↑ T k for some k ∈ I, or 2. S = i∈I p!m i .S i and T = i∈J p!m j .T j with J ⊆ I and S i ↑ T i for every i ∈ J, or 3. S = pπU.S ′ and T = pπU.T ′ and S ′ ↑ T ′ . Proof. If the derivation of S ⩽ * T contained no application of [u-tag-out] with J ⊊ I we would have wg(S, T ) = 0. Now we reason by cases on the last rule used to derive S ⩽ * T . Case [u-end]. Then S = T = πend. This case is impossible because wg(πend, πend) = 0 by definition. Case [u-tag-in].

  qπU.S, qπU.T ) = q ▷ pπ.disc(p, S, T ) ▶ Lemma B.11. If S is bounded and S ↑ T then S ̸ ⊑ T . From the hypothesis that S ↑ T and Lemma B.9 we deduce that the derivation of S ⩽ * T contains at least one application of [u-tag-out] with J ⊊ I. Consider disc(p, S, T ) from Definition B.10. Note that disc(p, S, T ) always sends a subset of the labels accepted by S, it is willing to receive any label sent by S, and it can always terminate successfully when interacting with S. Note also that it terminates successfully only after receiving a label from S that T cannot sent. Therefore, we have disc(p, S, T ) | p ▷ S coherent and disc(p, S, T ) | p ▷ T incoherent, which proves S ̸ ⊑ T . ◀ Proof of Theorem 4.10. Let S ⩽ @ T if S ⩽ * T and wg(U, T ) < ∞ for every judgment U ⩽ * V in the derivation of S ⩽ * T . From Lemmas B.4 and B.11 we have that S ⊑ T implies S ⩽ @ T . Indeed, if there is a judgment U ⩽ * V in the derivation of S ⩽ * T such that wg(U, V ) = ∞, then it is possible to build a session M such that M | p ▷ S is coherent and M | p ▷ T is not by induction on the minimum depth of the judgment U ⩽ * V in the derivation using the hypothesis that S is bounded and Lemma B.11. Now, using the principle of coinduction, it suffices to show that each judgment in the set

  with one application of [t-cast] and we conclude with another application of [t-cast] by taking m def = n. Case [s-cast-new]. Then P = (s)(⌈s[p]⌉R | P ) ≼ (s)(R | P ) = Q.

  P ) with an application of [t-par]. We conclude with an application of [t-cast] by taking m def = n. Case [s-call]. Then P = A⟨u⟩ ≼ R{u/x} = Q and A(x) △ = R. From [t-call] we conclude that there exist S and m such that A : [S; m] and Γ = u : S and u : S ⊢ m Q and m ≤ n. ◀ ▶ Lemma C.3 (Subject Reduction). If Γ ⊢ n P and P → Q, then Γ ⊢ m Q for some m.

C. 2 Measure▶

 2 We conclude using Lemma C.2 once more. ◀ Definition C.4 (rank). The rank of a session map M = h i=1 p i ▷ S i , written ∥M ∥, is the element of N ∪ {∞} defined as |M α =⇒ N | denotes the length of the sequence τ, . . . , τ, α and we postulate that min ∅ = ∞.

  s)(R | P ) with an application of [mt-par]. We conclude with an application of [mt-cast] by taking m def = n. Case [s-call]. Then P = A⟨u⟩ ≼ R{x/u} = Q and A(x) △ = R. From [mt-thread]

def=

  P and m def = n. Case [t-call]. Then P = A⟨u⟩ and A(x) △ = R. We deduce Γ = u : S, A : [S; n ′ ] and Γ ⊢ ind R{u/x}. Moreover, it must be the case that Γ ⊢ n ′ R{u/x} and n ′ ≤ n since [t-call]

  [mt-cast] taking Q def = ⌈u⌉Q ′ , ν def = ν ′ + (n, 0) and observing that P ⇒ Q using [r-cast].Case[mt-par]. Then P = (s)(P 1 | •

1 | 6 23:

 16 • • • | P par h ) and using the fact that ≼ is a pre-congruence and observing thatP = (s)(P 1 | • • • | P h ) by definition of P ≼ (s)(P nf 1 | • • • | P nf h ) using the induction hypothesis = (s)(⌈u 1 ⌉P par 1 | • • • | ⌈u h ⌉P par h ) by definition of thread normal form ≼ ⌈v 1 . . . v h ⌉(s)(P par 1 | • • • | P par h ) by [s-cast-new], [s-cast-swap], [s-par-comm] = P nf by definition of P nf Case [t-cast].Then there exist u, Q, Γ ′ , S and T such that C V I T 2 0 1 42 Fair Termination of Multiparty SessionsP = ⌈u⌉Q Γ = Γ ′ , u : S Γ ′ , u : T ⊢ ind Q S ⩽ T Using the induction hypothesis on Γ ′ , u : T ⊢ ind Q we deduce that there exists Q nf such that Q ≼ Q nf . We conclude by taking P nf def = ⌈u⌉Q nf using the fact that ≼ is a pre-congruence. ◀ ▶ Lemma C.15 (Proximity). If s ∈ fn(P ) \ bn(C), then (s)(C[P ] | Q) ≼ D[(s)(P | Q)] for some D.Proof. By induction on the structure of C and by cases on its shape.Case C = [ ].We conclude by takingD def = [ ] using the reflexivity of ≼. Case C = (t)(P ′ | C ′ | Q ′ ). From the hypothesis s ∈ fn(P ) \ bn(C) we deduce s ̸ = t and s ∈ fn(P ) \ bn(C ′ ). Using the induction hypothesis and [s-par-comm] we deduce that there existsD ′ such that (s)(C ′ [P ] | Q) ≼ D ′ [(s)(P | Q)]. Take D def = (t)(D ′ | P ′ | Q ′ ). We conclude (s)(C[P ] | Q) = (s)((t)(P ′ | C ′ [P ] | Q ′ ) | Q) by definition of C ≼ (s)(Q | (t)(C ′ [P ] | P ′ | Q ′ )) by [s-par-comm] ≼ (t)((s)(Q | C ′ [P ]) | P ′ | Q ′ ) by [s-par-assoc] and s ∈ fn(C ′ [P ]) ≼ (t)((s)(C ′ [P ] | Q) | P ′ | Q ′ ) by [s-par-comm] ≼ (t)(D ′ [(s)(P | Q)] | P ′ | Q ′ ) using the induction hypothesis = D[(s)(P | Q)] by definition of D Case C = ⌈t[p]⌉C ′ and s ̸ = t.Using the induction hypothesis we deduce that there existsD ′ such that (s)(C ′ [P ] | Q) ≼ D ′ [(s)(P | Q)]. Take D def = ⌈t[p]⌉D ′ . We conclude (s)(C[P ] | Q) = (s)(⌈t[p]⌉C ′ [P ] | Q) by definition of C ≼ ⌈t[p]⌉(s)(C ′ [P ] | Q) by[s-cast-swap] and t ̸ = s ≼ ⌈t[p]⌉D ′ [(s)(P | Q)] using the induction hypothesis = D[(s)(P | Q)] by definition of D Case C = ⌈s[p]⌉C ′ . Using the induction hypothesis we deduce that there exists D such that(s)(C ′ [P ] | Q) ≼ D[(s)(P | Q)]. We conclude (s)(C[P ] | Q) = (s)(⌈s[p]⌉C ′ [P ] | Q) by definition of C ≼ (s)(C ′ [P ] | Q) by [s-cast-new] ≼ D[(s)(P | Q)]using the induction hypothesis ◀ ▶ Lemma C.16 (Quasi -Deadlock Freedom). If ∅ ⊨ µ P nf , then P nf = done or P nf ≼ Q nf for some Q nf in proximity normal form.

Table 1

 1 Syntax of processes.

	P, Q, R ::=		Process
		done	termination
	|	wait u.P	signal input
	|	u[p]?(x).P	channel input
	|	u[p]π{m i

Table 2

 2 Structural precongruence of processes.

	[s-par-comm]

seller]!add.Buyer⟨x⟩, pay.close x}

	Seller(x)	△ = x[buyer]?{add.Seller⟨x⟩, pay.x[carrier]!ship.close x}
	Carrier(x)	△ = x[seller]?ship.wait x.done

  ]?{split.y[b 1 ]!{yes.close y, no.Buyer 2 ⟨y⟩}, giveup.close y}

		b]?query.x[b]!price.x[b]?{pay.x[c]!ship.close x, cancel.x[c]!cancel.close x}
	Carrier(x)	△ = x[s]?{ship.x[b]!box.close x, cancel.close x}
	Buyer 1 (x, y)	△ = y[b 2 ]!{split.y[b 2 ]?{yes.⌈x⌉x[s]!ok.x[c]?box.wait x.wait y.done,
		no.Buyer 1 ⟨x, y⟩},
		giveup.wait y.⌈x⌉x[s]!cancel.wait x.done}
	Buyer 2 (y)	△ = y[b 1

Table 6

 6 Typing rules.

	[t-done]	[t-call]
	∅ ⊢ n done

u : S ⊢ n P {u/x} u : S ⊢ n+m A⟨u⟩ A : [S; n], A(x) △ = P [t-wait] Γ ⊢ n P Γ, u : ?end ⊢ n wait u.P [t-close]

2 0 1 6 23:18 Fair Termination of Multiparty Sessions 6 Advanced Examples

  In this example we show that the process Buyer 1 playing the role b 1 in the inner session of Example 3.2 is well typed. For clarity, we recall its definition here: 2 ]!{split.y[b 2 ]?{yes.⌈x⌉x[s]!ok.x[c]?box.wait x.wait y.done, no.Buyer 1 ⟨x, y⟩}, giveup.wait y.⌈x⌉x[s]!cancel.wait x.done}

	Buyer 1 (x, y)

▶ Example 6.1. △ = y[b

  Slot always recurs after a cast, so it is not obvious that finitely many casts suffice in order for Slot to terminate. Here we provide evidence that the process definitions in Example 3.3 are well typed, even if they model processes that can open arbitrarily many sessions. In that example, the most interesting process definition is that of the worker Sort, which is recursive and may create a new session. In contrast, Merge is finite and Main only refers to Sort. We claim that these process definitions are well typed under the global type assignments

		1 B⟨x⟩
	x : s!add.S ⊢ 1 x[s]!add.B⟨x⟩	[t-tag]	x : !end ⊢ 0 close x	[t-close]
			[t-tag]		[t-tag]
	Main : [(); 1]	Sort : [U ; 0]	Merge : [T, V ; 0]

x : s!add.s!add.S ⊢ 1 x[s]!add.x[s]!add.B⟨x⟩

[t-cast]

x : S ⊢ 3 ⌈x⌉x[s]!add.x[s]!add.B⟨x⟩

x : s!pay.!end ⊢ 0 x[s]!pay.close x [t-cast] x : S ⊢ 1 ⌈x⌉x[s]!pay.close x [t-choice] x : S ⊢ 1 ⌈x⌉x[s]!add.x[s]!add.B⟨x⟩ ⊕ ⌈x⌉x[s]!pay.close x In general, the transformation u[p]!{m i .P i } i=1..n ⇝ ⌈u⌉u[p]!m 1 .P 1 ⊕ • • • ⊕ ⌈u⌉u[p

]!m n .P n does not always preserve typing, so it is not always possible to encode the output of tags using casts and non-deterministic choices. As an example, the definition Slot(x) △ = x[player]?{play.x[player]!{win.Slot⟨x⟩, lose.Slot⟨x⟩}, quit.close x} implements the unbiased slot machine of Example 4.6. It is easy to see that Slot is well typed under the global type assignment Slot : [T ; 0] where T = player?play.(player!win.T + player!lose.T ) + player?quit.!end. In particular, Slot has rank 0 since it performs no casts and it creates no sessions. If we encode the tag output in Slot using casts and non-deterministic choices we end up with the following process definition, which is ill typed because it cannot be given a finite rank: Slot(x) △ = x[player]?{play.(⌈x⌉x[player]!win.Slot⟨x⟩ ⊕ ⌈x⌉x[player]!lose.Slot⟨x⟩), quit.close x} The difference between this version of Slot and the above definition of B is that ⌟ ▶ Example 6.3.

  If Γ, x : S ⊢ n P and Γ, u : S is defined, then Γ, u : S ⊢ n P {u/x}. A typing context is defined if the endpoints occurring in it all have different session names.

	Proof. By bounded coinduction.	◀
	▶ Lemma C.2 (Subject Congruence). If Γ ⊢

▶ Lemma C.1. n P and P ≼ Q, then Γ ⊢ m Q for some m ≤ n.

Proof. By induction on the derivation of P ≼ Q and by cases on the last rule applied.

Case [s-par-comm]. Then P = (s)(P | P

  par], [t-wait] and [t-close] we deduce that there exist m and n i for i = 1, . . . , h such that n

  1 , s[p] : T k ⊢ n1 P k and from [t-tag] we deduce Γ 1 , s[p] : q!m k .T k ⊢ n1 s[p][q]!m k .P k . From Definition 4.2 we deduce that q!m k .T k | h i=2 p i ▷ S i coherent.We conclude with an application of [t-par] taking m

	def

  We say that P 1 ⊕ P 2 is an unguarded choice of P if there exists C such that P ≼ C[P 1 ⊕ P 2 ]. We say that P is in choice normal form if it has no unguarded choices. ▶ Definition C.9 (Thread Normal Form). A process is in thread normal form if it is generated by the grammar below: P nf , Q nf ::= ⌈u⌉P nf | P par P par , Q par ::= (s)(P par ) | P th P

context C, D ::= [ ] | (s)(P | C | Q) | ⌈u⌉C ▶ Definition C.8 (Choice Normal Form). th ::= done | close u | wait u.P | u[p]π{l i .P i } i∈I | u[p]!v.P | u[p]?(x).P C V I T 2 0 1 6

  with one application of [t-par], observing that m = 1 + = n and that P ⇒ Q by [r-par]. Case [t-cast]. Then P = ⌈u⌉P ′ . Analogous to the previous case, just simpler. Consequence of Lemma C.11 noting that Γ ⊢ n P implies Γ ⊢ ind P . ◀ ▶ Lemma C.13. If Γ ⊨ µ P , then there exist Q in choice normal form and ν ≤ µ such that P ⇒ Q and Γ ⊨ ν Q. Proof. By induction on Γ ⊨ µ P and by cases on the last rule applied. Case [mt-thread].

	1 +	h i=1 n i	h i=1 m i ≤

◀ ▶ Lemma C.12. If Γ ⊢ n P , then there exists Q in choice normal form such that P ⇒ Q and Γ ⊢ m Q for some m ≤ n.

Proof.

  • • | P h ). We deduce Γ = Γ 1 , . . . , Γ h µ = ▷ S i ∥) Γ i , s[p i ] : S i ⊨ µi P i for i = 1, . . . , h h i=1 p i ▷ S i coherentUsing the induction hypothesis we deduce that there exist Q i in choice normal form andν i ≤ µ i such that P i ⇒ Q i and Γ i , s[p i ] : S i ⊨ νi Q i for i = 1, . . . , h. We conclude by taking ν ▷ S i ∥) and Q def = (s)(Q 1 | • • • | Q h ) with one application of [mt-par], observing that ν = ▷ S i ∥) = µ and that P ⇒ Q by [r-par].If Γ ⊢ ind P and P is in choice normal form, then there exists P nf such that P ≼ P nf .Proof. By induction on Γ ⊢ ind P and by cases on the last rule applied.Cases [t-choice] and [co-choice]. These cases are impossible from the hypothesis that P is in choice normal form.Cases [t-done], [t-wait], [t-close], [t-channel-in], [t-channel-out], [t-tag], [co-tag].Then P is a thread and is already in thread normal form and we conclude by reflexivity of ≼.Case [t-call]. Then there exist A, Q, u and S such that ⊢ ind Q{u/x} Using the induction hypothesis on u : S ⊢ ind Q{u/x} we deduce that there exists P nf such that Q{u/x} ≼ P nf . We conclude P ≼ P nf using [s-call] and the transitivity of ≼.Case[t-par]. Then there exist s and P i , Γ i , S i , p i for i = 1, . . . , h such thatP = (s)(P 1 | • • • | P h ) Γ = Γ 1 , . . . , Γ h Γ i , s[p i ] : S i ⊢ ind P i for i = 1, . . . ,h Using the induction hypothesis on Γ i , s[p i ] : S i ⊢ ind P i we deduce that there exist P nf i such that P i ≼ P nf i for i = 1, . . . , h. By definition of thread normal form, it must be the case that P nf i = ⌈u i ⌉P par i for some u i and P par i . Let v i be the same sequence as u i except that occurrences of s[p i ] have been removed. We conclude by taking P nf def = ⌈v 1 . . . v h ⌉(s)(P par

	h i=1 µ i + (0, ∥ i=1 p i def h = h i=1 ν i + (0, ∥ h i=1 p i h i=1 ν i + (0, ∥ i=1 p i P = A⟨u⟩ h i=1 p i ▷ S i ∥) ≤ h i=1 µ i + (0, ∥ h
	A(x)

◀ ▶ Lemma C.14. △ = Q Γ = u : S u : S

▶ Definition C.5 (Measure). The measure of a process is a lexicographically ordered pair of natural numbers (m, n) where:

m is an upper bound to the number of sessions that the process may open and of weights of casts that the process may perform in the future before it terminates; n is the overall effort for terminating the sessions that have been already opened in the past, i.e. the sum of their rank (Definition C.4).

We now introduce a refined set of typing rules for processes that allow us to associate them with their measure, not just with their rank.

µi+(0,∥{pi▷Si} i=1,...,h ∥) (s

The idea behind these rules is that they distinguish between past and future of a process by looking at its structure. Indeed, unguarded sessions have been created, casts have not been performed yet and sessions that occur guarded have not been created yet. [mt-thread] adopts the rank of the process inside the usual typing judgment (Table 6) as first component of the measure. This rule has lower priority with respect to the other rules so that it is applied to processes that are not casts or restrictions. In [mt-cast] the first component of the measure is increased by the weight of the cast. [mt-par] increases the second component of the measure by the rank of the involved session.

▶ Lemma C.6. The following properties hold: 1. Γ ⊢ n P implies Γ ⊨ µ P for some µ ≤ (n, 0); 2. Γ ⊨ µ P implies Γ ⊢ n P for some n such that µ ≤ (n, 0).

Proof. We prove item 1 by induction on the structure of P . The proof of item 2 is by a straightforward induction over Γ ⊨ µ P .

Case P = (s)(P ). From [t-par] we deduce that there exist Γ i , p i , S i , n

Using the induction hypothesis on Γ i , s[p i ] : S i ⊢ ni P i (i=1,...,h) we deduce that there exist

. . , h We conclude with one application of [mt-par] by taking µ

Case P = ⌈u⌉Q. From [t-cast] we deduce that there exist ∆, S, T, m, m u such that Γ = ∆, u :

23:38 Fair Termination of Multiparty Sessions

Using the induction hypothesis on ∆, u : T ⊢ m Q we deduce ∆, u : T ⊨ ν Q for some ν ≤ (m, 0). We conclude with an application of [mt-cast] by taking µ def = ν + (m u , 0) and observing that µ ≤ (m, 0) + (m u , 0) = (n, 0).

In all the other cases. We conclude with an application of [mt-thread] by taking µ def = (n, 0). ◀ ▶ Lemma C.7. If Γ ⊨ µ P and P ≼ Q, then there exists ν ≤ µ such that Γ ⊨ ν Q.

Proof. By induction on the derivation of P ≼ Q and by cases on the last rule applied. We only consider the base cases.

From rule [mt-par] and the hypothesis that s ∈ fn(R) we deduce that there exist ∆ i , q i , T i , ν i for i = 1, . . . , k such that

s i -thread for some s i ; hence, there exist k i s i -threads. In other words, there exist D, C 1 , . . . , C ki and P th 1 , . . . , P th ki s i -threads such that

We conclude

The fact that Q nf is in thread normal form follows from the observation that P nf does not have unguarded casts (it is a closed process in thread normal form) so the pre-congruence rules applied here and in Lemma C.15 do not move casts around. We conclude that Q nf is in proximity normal form by its shape. ◀ Lemma C.16 is dubbed "quasi-deadlock freedom" because it does not say that Q nf reduces. Indeed, a process in proximity normal form is only ready to communicate thanks to its shape (see reduction rules). We can prove that a well typed process of such kind actually reduces by observing that [t-par] requires that the involved session is coherent. This result is the key ingredient for proving Lemma C.17.

C.4 Soundness

▶ Lemma C.17. If Γ ⊨ µ P nf where P nf is in proximity normal form, then there exist Q and ν < µ such that P nf ⇒ + Q and Γ ⊨ ν Q.

Proof. From the hypothesis that P nf is in proximity normal form we know that

for some C, s and P th 1 , . . . , P th h s-threads. We reason by induction on C and by cases on its shape.

Case C = [ ]. From [mt-thread] and [mt-par] we deduce that there exist Γ i , S i , p i , n i for i = 1, . . . , h such that

=⇒. We now reason on the rank of the session and on the shape of S i . For the sake of simplicity, we implicitly apply [s-par-comm] at process level.

Case S 1 = ?end and S j = !end for j = 2, . . . , h. Then Γ j = ∅ and P th j = close s[p j ] for j = 2, . . . , h

23:44 Fair Termination of Multiparty Sessions

Case S 1 = i∈I p 2 !m i .S ′ i and S 2 = j∈J p 1 ?m j .T j with k ∈ I. From the hypothesis that h i=1 p i ▷ S i coherent we deduce I ⊆ J. From Definition 4.2 we deduce

. We conclude with one application of [mt-par] observing that

From the hypothesis that h i=1 p i ▷ S i coherent and Definition 4.2 we deduce

. We conclude with one application of [mt-par] observing that

] and observe that R nf is in proximity normal form. From [mt-par] we deduce that there exist Γ i , S i , µ i ,

Using the induction hypothesis on Γ 1 , t[p 1 ] : S 1 ⊨ µ1 R nf we deduce that there exists Q ′ and ν ′ < µ 1 such that L. Ciccone, F. Dagnino and L. Padovani 23:45

and observing that ν < µ and

] and note that R nf is in proximity normal form. From [mt-cast] we deduce that there exists ∆, µ ′ , S, T, m t such that Proof. From Lemma C.6 we deduce that there exists µ ≤ (n, 0) such that ∅ ⊨ µ P . We proceed doing an induction on the lexicographically ordered pair µ. From Lemma C.18 we deduce either P ≼ done or P ⇒ + Q and ∅ ⊨ ν Q for some ν < µ. In the first case there is nothing left to prove. In the second case we use the induction hypothesis to deduce that either Q ≼ done or Q ⇒ + done. We conclude using either