Das Kapitel vertieft sich in die faszinierende Beziehung zwischen Logik und gleichzeitigen Programmiersprachen, aufbauend auf dem Curry-Howard-Isomorphismus. Es führt einen neuartigen Ansatz ein, der Formeln als Prozesse, Folgeregeln als operative Semantik und Ableitungen als Hinrichtungsbäume interpretiert. Dieses Rahmenwerk ermöglicht ein direktes Nachdenken über Programme und ihre Ausführung in der Sprache der Programme selbst, wobei die Notwendigkeit zwischengeschalteter Strukturen oder Sprachen umgangen wird. Das Kapitel stellt ein rekursionsfreies Fragment der π-Berechnung dar, das in ein nicht-kommutatives und nicht-assoziatives lineares Logiksystem eingebettet ist, und beweist Schlüsselergebnisse zu operativer Semantik und Sicherheitseigenschaften wie Stillstandsfreiheit und Fortschritt. Es stellt auch ein starkes Vollständigkeitsergebnis für die choreografische Programmierung dar und zeigt, dass alle rasse- und festgefahrenen Netzwerke als Choreografien ausgedrückt werden können. Das Kapitel schließt mit einer Diskussion zukünftiger Forschungsrichtungen, einschließlich der Ausweitung rekursiver Prozesse und asynchroner Kommunikation. Die Erforschung dieser Themen bietet eine fesselnde Reise in die Schnittstelle von Logik und gleichzeitiger Programmierung und verspricht wertvolle Einsichten für diejenigen, die sich für die theoretischen Grundlagen der Berechnung interessieren.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We introduce a novel approach to studying properties of processes in the \(\pi \)-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free \(\pi \)-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the \(\pi \)-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite \(\pi \)-calculus processes composed in parallel at the top level can be faithfully represented by a choreography.
With these results, we show how the computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the \(\pi \)-calculus, and the expressiveness of choreographic languages.
1 Introduction
The Curry-Howard isomorphism is a remarkable example of the synergy between logic and programming languages, which establishes a formulas-as-types and proofs-as-programs (and computation-as-reduction) correspondences for functional programs [67, 90]. In view of this success, an analogous proofs-as-processes correspondence has been included in the agenda of the study of concurrent programming languages [1, 17]. The main idea in this research line is that, as types provide a high-level specification of the input/output data types for a function, propositions in linear logic correspond to session types [56] that specify the communication actions performed by processes (as in process calculi) [20]. However, while the Curry-Howard correspondence fits functional programming naturally, it does not come without issues when applied to concurrency (we discuss the details in related work, section 5). This is because functional programming deals with the ‘sequential’ aspect of computation (given an input, return a specific output), while most of the interesting aspects of concurrent computation are about the communication patterns used during the computation itself. Therefore, as suggested in numerous works (e.g., [11, 11, 13, 69, 72]), the Curry-Howard correspondence may not be the right lens for the study of concurrent programs.
In this paper we investigate an alternative proof-theoretical approach to the study of processes, which is based on logical operators that faithfully model the fundamental operators of process calculi (like prefixing, parallel, and restriction). Our approach is close to the computation-as-deduction paradigm, where program executions are modelled as proof searches in a given sequent calculus; executions are therefore grounded in a logic by construction, as originally proposed by Miller in [69]. Specifically, we interpret formulas as processes, inference rules as rules of an operational semantics, and (possibly partial) derivations as execution trees (snapshots of computations up to a certain point).
Anzeige
The approach we follow is not to be confused with the intent of using logic as an auxiliary language to enunciate statements about computations, that is, viewing computation-as-model as done in Hennessy-Milner logic [51, 54], modal \(\mu \)-calculus [65], Hoare logic [52], or dynamic logics [10, 48]. We are instead interested in directly reasoning on programs and their execution using the language of the programs itself. This allows for an immediate transfer of properties of proofs to properties of programs, without needing intermediate structures (e.g., models) or languages (e.g., types).
1.1 Contributions of the paper
We consider the recursion-free fragment of the \(\pi \)-calculus – as presented in [22, 42] – and embed it in the language of the system \(\textsf{PiL}\) from [8]. \(\textsf{PiL}\) extends Girard’s first order multiplicative and additive linear logic [43] with a non-commutative and non-associative sequentiality connective (
), and nominal quantifiers (
and its dual
) for variable scoping.
Using this embedding, we prove the following main results.
1
We show that the operational semantics of the \(\pi \)-calculus is captured by the linear implication (\(\multimap \)) in \(\textsf{PiL}\): if we denote by \([\![ P ]\!]\) the formula encoding the process P, then
if P is a process reducing to \(P'\) by performing a communication or an external choice, then
; while
if P may reduce to \(P_{\ell _1},\ldots , P_{\ell _n}\) by performing an internal choice, then
.
Crucial to prove this result is our proof that the system \(\textsf{PiL}\) supports a substitution principle, which allows us to simulate reductions within a context.
2
We establish a computation-as-deduction correspondence, which we use to characterise two key safety properties studied for race-free processes in terms of derivability in \(\textsf{PiL}\): deadlock-freedom, i.e., the property that a process can always keep executing until it eventually terminates [96]; and progress, i.e., the property that if a process gets stuck, it is always because of a missing interaction with an action that can be provided by the environment [29].1
In particular, thanks to the structure of \(\textsf{PiL}\) and its operators, we can successfully detect safe processes that were previously problematic in the logical setting due to cyclic dependencies, like the process in Equation (1) below.
We show that our approach provides an adequate logical foundation for choreographic programming, a paradigm where programs are choreographies (coordination plans) that express the communications that a network of processes should enact [77].2 Specifically, we establish a choreographies-as-proofs correspondence by using a sequent system, called \(\textsf{ChorL}\), that consists of rules derivable in \(\textsf{PiL}\).
Our choreographies-as-proofs correspondence has an important consequence. An open question in theory of choreographic programming [78] is about how expressive choreographies can be:
To date, there are no answers to this question for the setting of processes with unrestricted name mobility and cyclic dependencies. Our correspondence implies a strong completeness result: in our setting, all and only race- and deadlock-free networks can be expressed as choreographies. This is the first such completeness result in the case of recursion-free networks.
Fig. 1.
Road map of the main technical results in this work.
Anzeige
1.2 Structure of the paper
In Section 2 we report \(\textsf{PiL}\) and prove the additional technical results required for our development. In Section 3 we recall the syntax and semantics of the \(\pi \)-calculus, introduce an alternative reduction semantics with the same expressiveness with respect to the property of deadlock-freedom, show that the reduction semantics of the \(\pi \)-calculus is captured by linear implication in \(\textsf{PiL}\), and that each step of the reduction semantics of the \(\pi \)-calculus can be seen as blocks of rules in this system. In Section 4 we define our choreographic language and provide our completeness result for choreographies. We discuss related work in Section 5. We conclude in Section 6, where we discuss research directions opened by this work. Due to space constraints, details of certain proofs are provided in the extended version of this paper [9].
2 Non-commutative logic
In this section we recall \(\textsf{PiL}\) and some of its established properties [8]. We then prove additional results required for our development.
Fig. 2.
Formulas (with \(x,y\in \mathcal {V}\)), and their syntactic equivalences.
2.1 The system \(\textsf{PiL}\)
The language of \(\textsf{PiL}\) is a first-order language containing the following.
Atoms generated by (i) a countable set of variables \(\mathcal {V}\), (ii) a binary predicate on symbols \(\langle -!-\rangle \), and (iii) its dual binary predicate \((-?-)\);
The multiplicative connectives for disjunction (
) and conjunction (\(\mathop \otimes \)) and the additive connectives for disjunction (\(\mathop \oplus \)) and conjunction (
) form multiplicative additive linear logic [43]. We generalize the standard binary \(\mathop \oplus \) and
, allowing them to have any positive arity (including 1) in order to avoid dealing with associativity and commutativity when modelling choices;
A binary non-commutative and non-associative self-dual multiplicative connective precede (
), whose properties reflect the ones of the prefix operator used in standard process calculi (see CCS [74] and \(\pi \)-calculus [42, 75]);
A unit (\(\circ \)). We observe that its properties reflect the ones of the terminated process \(\textsf{Nil}\). Notably, it is the neutral element of the connectives that we will use to represent parallelism (
) and sequentiality (
), and it is derivable from no assumption (thus also neutral element of \(\mathop \otimes \));
The standard first order existential (\(\exists \)) and universal (\(\forall \)) quantifiers.
A nominal quantifiernew (
), and its dual ya (
). We observe that these restrict variable scope in formulas in the same way that the \(\nu \) constructor in process calculi restricts the scope of names.
More precisely, we consider formulas generated by grammar in Figure 2 modulo the standard \(\alpha \)-equivalence from the same figure. From now on, we assume formulas and sequents to be clean, that is, such that each variable \(x\in \mathcal {V}\) occurring in them can be bound by at most a unique universal quantifier or at most a pair of dual nominal quantifiers, and, if bound, it cannot occur free .3 The (linear) implication\(A\multimap B\) (resp. the logical equivalence
) is defined as
(resp. as \((A \multimap B)\mathop \otimes (B\multimap A)\)), where the negation (\(\bar{\cdot }\)) is defined by the de Morgan duality in Figure 2.
The set \(\textsf{free}(A)\) (resp. \(\textsf{free}(\Gamma )\)) of free variables of a formula A (resp. of a sequent \(\Gamma =A_1,\ldots , A_n\)) is the set of atoms occurring in A which are not bound by any quantifier (resp. the set \(\bigcap _{i=1}^{n}\textsf{free}(A_i)\)). A context is a formula containing a single occurrence of a propositional variable \(\bullet \) (called hole). We denote by \(\mathcal {C}[A]:=\mathcal {C}\left[ A/\bullet \right] \). A
-context is a context \(\mathcal {K}[\bullet ]\) of the form
for a \(n\in \mathbb N\).
In this work we assume the reader to be familiar with the syntax of sequent calculus (see, e.g., [93]), but we recall here the main definitions.
Notation 1
A sequent is a set of occurrences of formulas.4 A sequent rule\(\textsf{r} \) with premise sequents \(\Gamma _1,\ldots ,\Gamma _n\) and conclusion\(\Gamma \) is an expression of the form
. A formula occurring in the conclusion (resp. in a premise) of a rule but in none of its premises (resp. not in its conclusion) is said principal (resp. active). Given a set of rules \(\textsf{X}\), a derivation in \(\textsf{X}\) is a non-empty tree \(\mathcal {D}\) of sequents, whose root is called conclusion, such that every sequent occurring in \(\mathcal {D}\) is the conclusion of a rule in \(\textsf{X}\), whose children are (all and only) the premises of the rule. An open derivation is a derivation whose leaves may be conclusions of no rules, in which case are called open premises. We may denote a derivation (resp. an open derivation with a single open premise \(\Delta \)) with conclusion \(\Gamma \) by
. Finally we may write
if there is an open derivation with premises \(\Gamma _1,\ldots ,\Gamma _n\) and conclusion \(\Gamma \) made only of rules \(\textsf{r} \).
A nominal variable is an element of the form
with
and
. If
is a set of nominal variables, we say that xoccurs in
if
or
is an element of
. A (nominal) store
is a set of nominal variables such that each variable occurs at most once in
. A judgement
is a pair consisting of a clean sequent \(\Gamma \) and a store
. We write judgements
with
simply as \(\vdash \Gamma \)
. We write
to denote the union of two stores such that a same variable does not occur in both
and
– i.e., a disjoint union.
The system \(\textsf{PiL}\) is defined by the all rules in Figure 3 except the rule \(\textsf{cut}\). We write
to denote that the judgement
is derivable in \(\textsf{PiL}\).
Remark 1
The system
is the standard one for first order multiplicative linear logic [43]. The rules \(\mathop \oplus \) and
are generalisations of the standard ones in additive linear logic for the n-ary generalized connectives we consider here; thus, in proof search, the rule \(\mathop \oplus \) keeps only one \(A_k\) among all \(A_i\) occurring in \(\bigoplus _{i=1}^{n} A_i\), and the rule
branches the proof search in n premises. The rule \(\textsf{mix}\) and \(\circ \) are standard for multiplicative linear logic with mix in presence of units5 [28, 40], and the rule
ensures that the unit \(\circ \) is not only the unit for the connectives
and \(\mathop \otimes \), but also for
. The rule
is required to capture the self-duality of the connective
; it should be read as introducing at the same time the connective
and its dual (which in this case is
itself) – as a general underlying pattern for multiplicative connectives, see [2, Remark 5]. The store is used to guarantee that each
is linked to at most a unique
(or vice versa) in any branch of a derivation. If a rule
is applied, then the nominal quantifier is not linked, reason why the rule reminds the standard universal quantifier rule. Otherwise, either the rule
loads a nominal variable in the store, or a rule
uses a nominal variable (of dual type) occurring in the store as a witness variable. Note that in a derivation with the conclusion a judgement with empty store any
is uniquely linked to a
below it.
Fig. 3.
Sequent calculus rules, with \(\dagger := x\notin \textsf{free}(\Gamma )\).
2.2 Proof Theoretical Properties of \(\textsf{PiL}\)
We now recall some basic proof-theoretical properties of the system \(\textsf{PiL}\) and then prove additional results (Theorem 2) that will be important for the main technical results in this paper.
In \(\textsf{PiL}\) we can prove that atomic axioms are sufficient to prove that the implication \(A\multimap A\) holds for any formula A. Moreover, the \(\textsf{cut}\)-rule is admissible in these systems, allowing us to conclude the transitivity of the linear implication, as well as the sub-formula property for all the rules of the systems.
Theorem 1
([8]). Let \(\Gamma \) be a non-empty sequent in \(\textsf{PiL}\). Then
1.
for any formula A;
2.
if
, then
;
3.
if
and
, then
.
Proposition 1
([8]). The following logical equivalences are derivable in \(\textsf{PiL}\) (for any \(\sigma \) permutation over \(\{1,\ldots ,n\}\)).
(3)
Moreover,
.
In addition to these properties, our development requires some new ones showing that implication is preserved in different contexts. This is necessary because some rules in the operational semantics of the \(\pi \)-calculus enables rewriting of deeply nested subterms. For this reason, we are required to establish properties similar to those for proving subject reduction in \(\lambda \)-calculus. That is, we prove that in \(\textsf{PiL}\) we can still reproduce the application of inference rules inside contexts preserving soundness and completeness. These necessary properties are collected in the next theorem.
Theorem 2
For any context \(\mathcal {C}[\bullet ]\) and
\(\mathcal {K}[\bullet ]\) we have:
1.
if
, then
;
2.
if
for \(i\in \{1,\ldots ,n\}\), then
;
3.
if
and
, then
.
Proof
Item 1 and Item 2 are proven by induction on the structure of the contexts. To prove Item 3 we use Theorem 1.3 since if
, then by 1 also
. Details of the proof are available in [9].
Remark 2
In the proofs-as-processes interpretation, \(\textsf{cut}\) is the linchpin that triggers the rewriting simulating the reduction semantics (cut elimination). In our work, as in general in the study of processes-as-formulas, the \(\textsf{cut}\)-rule is freed from being the keystone of the system. Instead, the admissibility of the \(\textsf{cut}\)-rule in the computation-as-deduction approach guarantees the existence of canonical models [53, 70, 71]. In particular, we use this property to tame the syntactic bureaucracy of the reduction semantics due to rules \(\textsf{Par}\), \(\textsf{Res}\), and \(\textsf{Struc}^\Rrightarrow \), as well as to ensure the transitivity of logical implication (required to compose reduction steps).
3 Embedding the \(\pi \)-calculus in \(\textsf{PiL}\)
In this section we provide an interpretation of \(\pi \)-calculus processes as formulas in \(\textsf{PiL}\), showing also that each successful execution of a process corresponds to a branch in a correct derivation in \(\textsf{PiL}\).
We start by recalling the definition of the \(\pi \)-calculus and its operational semantics. Our presentation has explicit primitives for communicating choices, as usual in the literature of session types [64, 95, 96]. We then present an alternative semantics in which we use structural precongruence instead of structural equivalence (this is a standard simplification [33, 62], which does not affect reasoning about deadlock-freedom, progress, or races). We then provide a translation of processes P into formula \([\![ P ]\!]\) in \(\textsf{PiL}\) and characterise deadlock-freedom for P in terms of provability of \([\![ P ]\!]\) in \(\textsf{PiL}\).
Fig. 4.
Syntax for \(\pi \)-calculus processes with \(x,y\in \mathcal {N}\) and \(L \subset \mathcal {L}\), and their sets of free and bound names.
Fig. 5.
The standard \(\alpha \)-equivalence, and relations generating of the structural equivalence (\(\equiv \)) \(\pi \)-calculus processes, where
stands for \(A\Rrightarrow B\) and \(B\Rrightarrow A\).
3.1 The \(\pi \)-calculus and its reduction semantics
The set of \(\pi \)-calculus processes is generated by the grammar in Figure 4, which uses a fixed countable set of (channel) names\(\mathcal {N}=\{x,y,\ldots \}\) and a finite set of labels\(\mathcal {L}\). We may denote by \((vx_1\dots x_k)\) a generic sequence \((\nu x_1)\cdots (\nu x_n)\) of \(\nu \)-constructors of length \(n>0\), and we may simply write \(x \triangleleft \left\{ \ell :P_\ell \right\} \) (resp. \(x \triangleright \left\{ \ell :P_\ell \right\} \)) as a shortcut for \(x \triangleleft \left\{ \ell : P_\ell \right\} _{\ell \in L}\) (resp. \(x \triangleright \left\{ \ell : P_\ell \right\} _{\ell \in L}\)) whenever \(L=\{\ell \}\). A process is sequential if it contains no parallel (\(\;|\;\)) or restrictions (\(\nu \)), it is flat6 if of the form \(P=(vx_1\dots x_k) \left( P_1\;|\;\cdots \;|\;P_n\right) \) for some sequential processes \(P_1,\ldots , P_n\) (also called sequential components of P). We use the common notation \(P\left[ x/y \right] \) for substitution (see the Appendix of [9]).
The set \(\mathcal {F}_{P}\) of free names and the set \(\mathcal {B}_{P}\) of bound names in a process P are defined in Figure 4. The set of names in P is denoted \(\mathcal N_{P}\) and a name x is fresh in P if \(x\notin \mathcal N_{P}\). A context is a process \(\mathcal {P}[\bullet ]\) containing a single occurrence of a special free name \(\bullet \) called hole such that \(\mathcal {P}[P]:=\mathcal {P}\left[ P/\bullet \right] \) is a process. A network context is a context of the form \(\mathcal {N}[\bullet ]=(vx_1\dots x_k)\left( [\bullet ]\;|\;P_1 \;|\;\cdots \;|\;P_n\right) \).
The \(\alpha \)-equivalence (\(\equiv _{\alpha }\)) is recalled in Figure 5. To improve the presentation of the technical results, we assume processes written in an unambiguous form, that is, in such a way each bound variable \(x\in \mathcal {B}_{P}\) is bound by a unique \(\nu \)-constructor and do not occur free in P. In the same figure we provide the relation \(\Rrightarrow \), whose reflexive and transitive closure is denoted
, and we define the standard (structural) equivalence (\(\equiv \)) as the equivalence relation generated by the union of \(\Rrightarrow \) and \(\equiv _{\alpha }\).
Fig. 6.
Reduction semantics for the \(\pi \)-calculus.
The reduction semantics for processes is defined by the relation \(\rightarrow \) over processes induced by the rules in Figure 6. As standard, we denote by \(\twoheadrightarrow \) the reflexive and transitive closure of \(\rightarrow \). As in [22], to allow for nondeterminism, the syntax of processes contains a construct \(x \triangleleft \left\{ \ell :P_\ell \right\} _{\ell \in L}\) allowing for different options rather than the typical \(x \triangleleft \left\{ P:\ell \right\} \). Thus, the corresponding rule \(\textsf{Choice}\) for choosing among the available options induces a branching in the computation tree of the process. We say that a process P is stuck if \(P \not \equiv \textsf{Nil}\) and there is no \(P'\) such that \(P \rightarrow P'\). A process P is called deadlock-free if there is no stuck process \(P'\) such that \(P \twoheadrightarrow P'\). Also, a process P has progress7 if it is deadlock-free or \(P\;|\;Q\) is deadlock-free for a stuck process Q.
Remark 3
Intuitively, deadlock-freedom means that there is always a part of a process that can reduce [62, 78]. Progress for processes, instead, was introduced in [29] to characterise processes that get stuck merely because they lack a communicating partner that could be provided by the environment.
For example, the process \(P=(\nu x) (x!\langle a\rangle . \textsf{Nil}\;|\;x?(b).\textsf{Nil}\;|\;y!\langle c\rangle . \textsf{Nil})\) is not deadlock-free because it reduces (via \(\textsf{Com}\)) to the stuck process \((\nu x) (\textsf{Nil}\;|\;y!\langle c\rangle .\textsf{Nil})\equiv y?(d).\textsf{Nil}\), but this later has progress since \(y!\langle d\rangle .\textsf{Nil}\;|\;y?(d).\textsf{Nil}\) is deadlock-free.
A process P has a race condition if there is a network context \(\mathcal {N}[\bullet ]\) such that P is structurally equivalent to a term of the following shape.
A process P is race-free if there is no \(P'\) with a race condition such that \(P\twoheadrightarrow P'\).
Remark 4
Race conditions identify in a syntactic way the semantic property of a process potentially having nondeterministic executions because of concurrent actions on a same channel. For example, \(P= x!\langle a\rangle .\textsf{Nil}\;|\;x?(b). \textsf{Nil}\;|\;x?(c).\textsf{Nil}\) has a race condition, and it can reduce either to \(P_b=x?(b). \textsf{Nil}\) or to \(P_c=x?(c). \textsf{Nil}\) according to the way the reduction rule \(\textsf{Com}\) is applied. We specify ‘potentially’ because, for example, the process \(Q= (\nu x)\left( x?(b). \textsf{Nil}\;|\;x?(c).\textsf{Nil}\right) \) has a race but cannot reduce. In fact, in the execution of a race-free process, rules \(\textsf{Com}\) and \(\textsf{Label}\) are applied deterministically. That is, the same send (resp. selection) is synchronised via a \(\textsf{Com}\) (resp. a \(\textsf{Label}\)) with the same receive (resp. branching), and vice versa, in any possible (branch of an) execution.
3.2 A Simpler Equivalent Presentation of the Reduction Semantics
To simplify the presentation of the new methodologies we use in our new framework, we replace the structural equivalence \(\equiv \) with the precongruence
(as in [33, 62]). In particular, such a precongruence orients the direction of scope extrusion (by extending the scope of the binder as much as possible), but also rules out those rewritings that may add superfluous information such as \(P\Rrightarrow (P \;|\;\textsf{Nil})\) or \(P\Rrightarrow ((\nu x) P)\) for a \(x\notin \mathcal N_{P}\). Thus in the reduction semantics we consider in this paper we employ the following rule instead of the standard \(\textsf{Struc}\) (see Figure 6):
(4)
Remark 5
The reduction semantics using the rule \(\textsf{Struc}^\Rrightarrow \) instead of \(\textsf{Struc}\) is weaker because the set of processes reachable via a step of \(\textsf{Struc}^\Rrightarrow \) is strictly contained in the set of processes reachable via \(\textsf{Struc}\). By means of example, consider the process \(x!\langle y\rangle . \textsf{Nil}\;|\;x?(z). \textsf{Nil}\) which reduces to both \(\textsf{Nil}\;|\;\textsf{Nil}\) and \(\textsf{Nil}\) using \(\textsf{Struc}\), but can only reduce to \(\textsf{Nil}\;|\;\textsf{Nil}\) using \(\textsf{Struc}^\Rrightarrow \).
However, it is immediate to show that if \(P\rightarrow P'\) via \(\textsf{Struc}\), then there is a \(Q\equiv P'\) such that \(P\rightarrow Q\) via \(\textsf{Struc}^\Rrightarrow \). Therefore, the standard reduction semantics (containing the rule \(\textsf{Struc}\)) is as informative as the one we consider here (where we use the rule \(\textsf{Struc}^\Rrightarrow \) instead) for the study of deadlock-freedom and for the definition of the race condition.
In the definition of the rules of the reduction semantics, the rules \(\textsf{Com}\), \(\textsf{Choice}\) and \(\textsf{Label}\) are, in some sense, performing ‘meaningful’ transformation on processes, while rules \(\textsf{Res}\), \(\textsf{Par}\) and \(\textsf{Struc}^\Rrightarrow \) deal with the syntactic bureaucracy of rewriting modulo the structural equivalence. In the proofs in the next sections we need to be able to identify in each reduction step \(P\rightarrow P'\) the sub-process \(\textsf{rdx}_{(P,P')}\) of P (called core-redex) which is irreversibly transformed to the process \(\textsf{rdt}_{(P,P')}\) (called core-reductum), as well as to measure the amount of syntactical manipulations we need to ‘reach’ such a sub-process to apply a reduction step (which we call entropy). We make these concepts precise in the next definitions and exemplify them in Figure 7.
Definition 1
Let P and \(P'\) processes such that \(P\rightarrow P'\). The core\(\textsf{Core}_{(P,P')}=(\textsf{rdx}_{(P,P')},\textsf{rdt}_{(P,P')})\) and the entropy\(\textsf{Ent}_{(P,P')}\in \mathbb N\) of \(P\rightarrow P'\) are defined as:
if \(P\rightarrow P'\) via \(\textsf{Com}\), \(\textsf{Label}\) or \(\textsf{Choice}\), then \(\textsf{Ent}_{(P,P')}=1\) and \(\textsf{Core}_{(P,P')}=(P,P')\);
if \(P\rightarrow P'\) via \(\textsf{Par}\) (resp. \(\textsf{Res}\)), then there are processes Q and \(Q'\) such that \(Q\rightarrow Q'\) and a context \(\mathcal {P}[\bullet ]\) of the form \(\bullet \;|\;R\) (resp. of the form \((\nu x) (\bullet )\)) such that \(P=\mathcal {P}[Q]\) and \(P'=[Q']\) by definition of the reduction step. Then \(\textsf{Ent}_{(P,P')}=2\textsf{Ent}_{(Q,Q')}\) and \(\textsf{Core}_{(P,P')}=\textsf{Core}_{(Q,Q')}\);
if \(P\rightarrow P'\) via \(\textsf{Struc}^\Rrightarrow \), then there are processes Q and \(Q'\) such that
with
and
. Then \(\textsf{Ent}_{(P,P')}=3\textsf{Ent}_{(Q,Q')}\) and \(\textsf{Core}_{(P,P')}=\textsf{Core}_{(Q,Q')}\).
The core-reduction of \(P\rightarrow P'\) is the rule used to reduce \(\textsf{rdx}_{(P,P')}\) to \(\textsf{rdt}_{(P,P')}\).
Fig. 7.
Examples of processes S and \(S'\) such that \(S\rightarrow S'\), and the core-redex, core-reductum, and entropy of the rewriting step.
Definition 2
A execution tree of a process P is a tree of processes \(\textsf{Ctree}(P)\) with root P, such that a process \(Q'\) is a child of Q if \(Q\rightarrow Q'\), and such that:
if the core-reduction of \(Q\rightarrow Q'\) is a \(\textsf{Com}\) or a \(\textsf{Label}\), then \(Q'\) is the unique child of Q;
if the core-reduction of \(Q\rightarrow Q'\) is a \(\textsf{Choice}\), then the set \(\{Q_1,\ldots , Q_n\}\ni Q'\) of children of Q is such that the core-reduction of \(Q\rightarrow Q_i\) is a \(\textsf{Choice}\) and \(\textsf{rdx}_{(Q,Q_i)}=\textsf{rdx}_{(Q,Q')}\) for all \(i\in \{1,\ldots ,n\}\).
It is maximal if each leaf of the tree is a process \(R\equiv \textsf{Nil}\) or is stuck.
We conclude this subsection with this result, which, together with Remark 5, allows us to consider each maximal execution tree as a witness of deadlock-freedom for race-free processes.
Lemma 1
Let P be a process. If P is deadlock-free, then each execution tree with root P can be extended to a maximal execution tree whose leaves are processes structurally equivalent to \(\textsf{Nil}\).
3.3 Translating Processes into Formulas
We define a translation of \(\pi \)-calculus processes into \(\textsf{PiL}\) formulas.
Definition 3
(Processes as Formulas). We associate to each \(\pi \)-calculus process P a formula \([\![ P ]\!]\) inductively defined as follows.
(5)
Note that assuming P unambiguous, the translation is a clean formula.
Remark 6
The reader familiar with session types could be curious about the choice of representing by a
-formula a process of the form \(x \triangleleft \left\{ \ell :P_\ell \right\} _{\ell \in L}\) (whose session type is a \(\mathop \oplus \)-type) and, dually, by a \(\mathop \oplus \)-formula a process \(x \triangleright \left\{ \ell :P_\ell \right\} _{\ell \in L}\) (whose session type is a
-type). This is only an apparent contradiction because our formulas are not types. Rather, they encode processes whose executions are then derivations in the \(\textsf{PiL}\) system. Under this new interpretation, during proof search the rule for
gives exactly the expected branching of possible executions of terms like \(x \triangleleft \left\{ \ell :P_\ell \right\} _{\ell \in L}\), corresponding to rule \(\textsf{Choice}\) in the reduction semantics. Rule \(\textsf{Label}\) can then be applied ‘afterwards’ (above in the derivation) to select the appropriate branch at the receiver, discarding all the others. Thus, in the formulas-as-processes, receiving a label corresponds to \(\oplus \).
For the same reason, parallel composition is represented by
(as in [14, 71]), while in most works using propositions as session types it is represented by \(\textsf{cut}\) and \(\mathop \otimes \). We will come back to this aspect in Section 5.
Proposition 2
Let \(P_1\) and \(P_2\) processes. If \(P_1\Rrightarrow P_2\) then \([\![ P_2 ]\!]\multimap [\![ P_1 ]\!]\).
Proof
and
derive from commutativity and associativity of
(see Proposition 1). The logical equivalences
and
are direct consequence of the ones in Figure 2. The implication \([\![ (\nu x) (P \;|\;Q) ]\!] \multimap [\![ (\nu x) P \;|\;Q ]\!] \) for \(x\notin \textsf{free}(Q)\) is shown in Proposition 1. Finally,
derives from the quantifier shifts
(Figure 2).
Fig. 8.
Derivations in \(\textsf{PiL}\) corresponding to the rules \(\textsf{Com}\), \(\textsf{Choice}\) and \(\textsf{Label}\) of the reduction semantics of the \(\pi \)-calculus.
3.4 Deadlock-Freedom as Provability in \(\textsf{PiL}\)
We can now establish a correspondence between process reductions and linear implication in \(\textsf{PiL}\), as well as a correspondence between each computation tree with root a process P and a proof search strategy in \(\textsf{PiL}\) for the formula \([\![ P ]\!]\). Combining these two results, we obtain a purely logical characterisation of deadlock-free processes as pre-images via \([\![ \cdot ]\!]\) of formulas derivable in \(\textsf{PiL}\).
Lemma 2
Let P and \(P'\) processes.
1.
If
, then \([\![ P' ]\!]\multimap [\![ P ]\!]\).
2.
If \(P\rightarrow P'\), then either
(a)
the core-reduction of \(P \rightarrow P'\) is a \(\textsf{Com}\) or a \(\textsf{Label}\), and
;
(b)
or the core-reduction of \(P \rightarrow P'\) is a \(\textsf{Choice}\) then there is a set \(\{P_\ell \mid \ell \in L\}\ni P'\) such that \(P \rightarrow P_\ell \) for all \(\ell \in L\) and
.
Proof
Item 1 is proven using Proposition 1 and transitivity of \(\multimap \) (see Theorem 1.3). To prove Item 2 we reason by induction on entropy:
if \(\textsf{Ent}_{(P,P')}=1\) then \(P\rightarrow P'\) via \(\textsf{Com}\), \(\textsf{Label}\) or \(\textsf{Choice}\) and we conclude using the derivations in Figure 8;
if \(P\rightarrow P'\) via \(\textsf{Par}\) (resp. \(\textsf{Res}\)), then there is a context \(\mathcal {P}[\bullet ]=\left( \bullet \;|\;R\right) \) (resp. \(\mathcal {P}[\bullet ]=(\nu x)\bullet \)) such that \(P=\mathcal {P}[S]\) and \(P'=\mathcal {P}[S']\). We conclude using Theorem 2.1 and Theorem 1.3;
if \(P\rightarrow P'\) via \(\textsf{Struc}^\Rrightarrow \), then there is S such that
and \(S\rightarrow P'\) (via a rule different from \(\textsf{Struc}^\Rrightarrow \)). We conclude by Theorem 1.3 using Item 1 and Theorem 22.
Using this lemma we can prove the correspondence between deadlock-freedom and derivability in \(\textsf{PiL}\).
Theorem 3
Let P be a race-free process. Then P is deadlock-free iff
. More precisely,
.
Proof
It suffices to establish a correspondence between maximal execution trees and derivations in \(\textsf{PiL}\). Details are provided in the appendix of [9].
(\(\Rightarrow \)) If P is deadlock-free, then, any maximal execution tree \(\textsf{Ctree}(P)\) with root P has leaves which are processes structurally equivalent to \(\textsf{Nil}\) by Lemma 1. By induction on the structure of \(\textsf{Ctree}(P)\), we can define a derivation in \(\textsf{PiL}\cup \{\textsf{cut}\}\) composing (using \(\textsf{cut}\)) the derivations allowing simulating the transitions of the reduction semantics (Lemma 2); thus we obtain a derivation in \(\textsf{PiL}\) by applying cut-elimination (Theorem 1.2). We conclude observing that the subformula property ensures that only rules in such cut-free derivation are in
. Note that all judgements in such a derivation are empty.
(\(\Leftarrow \)) To prove the converse, we show that each derivation \(\mathcal {D}_P\) of \([\![ P ]\!]\) can be transformed using the rule permutations in Figure 9 into a derivation \(\widetilde{\mathcal {D}_P}\) made of blocks of rules consisting of sequences of
- and
-rules only, or blocks as the ones shown in Equation (6) below.
(6)
We conclude by induction on the number of such blocks, since each block in the left (resp. right) of Equation (6) identifies an application of a \(\textsf{Com}\) (resp. a \(\textsf{Bra}\) followed by a \(\textsf{Sel}\)).
Note that since P is race-free, then it suffices to reason on a single execution tree and not to take into account all possible execution trees of P.
Corollary 1
Let P be a race-free process. Then P has progress iff there is a
\(\mathcal {C}[\bullet ]\) such that
.
Fig. 9.
Rule permutations with
and
.
We conclude this section by showing that progress for processes which never send ‘private’ channels can be easily captured in this new setting. Specifically, we say that a process P has private mobility if it is of the form \(P=\mathcal {P}[a!\langle x\rangle ]\) for an a bound by a \(\nu \) in \(\mathcal {P}\). We also denote by \(\partial _{x_1,\ldots ,x_k} [\![ P ]\!]\) the formula obtained by replacing with a unit (\(\circ \)) any atom in \([\![ P ]\!]\) of the form \(\langle x!y\rangle \) or \((x?y)\) for any \(x\in \{x_1,\ldots ,x_k\}\).
Theorem 4
Let P be a race-free process without private mobility. Then P has progress iff
.
Proof
We prove a simulation result (as Lemma 2) for \(\partial _{\mathcal {F}_{P}} [\![ P ]\!]\), and we conclude with the same argument used in the proof of Theorem 3. It P is deadlock-free, then we conclude as in Theorem 3. Otherwise, since P has progress there is Q such that \(P \;|\;Q\) is deadlock-free. By definition, we must have that \(\mathcal N_{Q}=\mathcal {F}_{Q}\) (otherwise either Q is not stuck or \(P \;|\;Q\) is not deadlock-free) and that \(\mathcal {F}_{Q}=\mathcal {F}_{P}=x_1,\ldots ,x_k\). Thus
by the fact that \(\partial _{x_1,\ldots ,x_k} [\![ Q ]\!]\) contains no atoms (i.e., only units) and
(see Proposition 1).
If \(P \;|\;Q \) is deadlock-free for Q stuck and \(P \;|\;Q \rightarrow R\) via \(\textsf{Par}\) then, \(R = P' \;|\;Q\) and \(P \rightarrow P'\). If the core-reduction of \(P\twoheadrightarrow P'\) is a \(\textsf{Com}\) or a \(\textsf{Label}\), then
; if the core-reduction is a \(\textsf{Choice}\), there is a set of processes \(\{P_\ell \}_{\ell \in L}\ni P'\) such that
. This is proven by induction on the entropy as in Lemma 2.
If \(P'\;|\;Q\rightarrow P'\) not via \(\textsf{Par}\) and then the core-reduction is either a \(\textsf{Com}\) or a \(\textsf{Sel}\). In this case can prove as that
.
Remark 7
To understand the requirement on private mobility in Proposition 4, consider the process \(P=(\nu a) (b!\langle a\rangle . a!\langle c\rangle . \textsf{Nil})\). This process has progress, because
However,
is not derivable in \(\textsf{PiL}\). This makes our characterisation of progress as powerful as in previous work [22] (where the condition is not made explicit but clearly necessary, see the definition of ‘co-process’ therein).
4 Completeness of Choreographies
In this section we prove that any deadlock-free flat process can be expressed as a choreography, as intended in the paradigm of choreographic programming [77]. Key to this result is establishing a proofs-as-choreographies correspondence, whereby choreographies can be seen as derivations in the \(\textsf{PiL}\) system.
To this end, we first introduce the syntax and semantics of choreographies, the typical accompanying language for describing their implementations in terms of located processes (the endpoint calculus), and a notion of endpoint projection (EPP) from choreographies to processes. We then define the sequent calculus \(\textsf{ChorL}\) operating on sequents in which (occurrences of) formulas are labelled by process names, and we conclude by establishing the proofs-as-choreographies correspondence.
Fig. 10.
Syntax and semantics for choreographies, where \({\textsf{p}}\) and \({\textsf{q}}\) are distinct process names in \(\mathcal {P}\), \(x,y\in \mathcal {V}\), \(L\subseteq L' \subseteq \mathcal {L}\), and \(S_\ell \) are sequential processes (see Remark 8).
4.1 Choreographies
In a choreographic language, terms (called choreographies) are coordination plans that express the overall behaviour of a network of processes [78]. The choreographies that we consider in this paper are generated by a set of process names\(\mathcal {P}\), a set of variables \(\mathcal {V}\), and a set of selection labels\(\mathcal {L}\) as shown in Figure 10. A choreography can be either:
, the terminated choreography;
, a communication from a process \({\textsf{p}}\) to another \({\textsf{q}}\) with a continuation C (y is bound in C and can appear only under \({\textsf{q}}\));
, a choice by a process \({\textsf{p}}\) of a particular branch L offered by another process \({\textsf{q}}\)8; or
, which restricts x in a choreography
in which the variable x always occur free (i.e., no
occurs in
).9
Note that we consider communication of process names or variables only (that is, \(k\in \mathcal {P}\cup \mathcal {V}\)). We say that a choreography is flat if it is of the form
for a restriction-free (i.e., containing no occurrences of \(\nu \)) choreography
. In the same figure we also provide the reduction semantics of our choreographic language, where each reduction step is labelled by a reduction label
from the following set.
(7)
To each reduction label
we associate the set
of processes names and variables occurring in it – i.e.
and
.
In the semantics,
executes a communication while
allows a process \({\textsf{p}}\) to make an internal choice. Rule
then communicates a label from \({\textsf{p}}\) to \({\textsf{q}}\), which then continue with the choreography
(but never with a sequential process \(S_\ell \), see Remark 8). Rule
lifts reductions under restrictions. Lastly,
models the standard out-of-order execution of independent communications that can be reduced by rule
– this is the choreographic equivalent of parallel composition in process calculi [78].
Example 1
The next choreography expresses the communication behaviour of the processes given in Equation (1).
(8)
It can be executed by applying rule
and then rule
. Note that we do not need to use rule
before applying
, because the set of labels L in the choice constructor is a singleton.
Remark 8
From the programmer’s viewpoint, choice instructions may contain some unnecessary information since no label \(\ell '\in L'\setminus L\) will never be selected during the execution of a choreography – and thus no continuation will execute the process \(S_{\ell '}\). This ‘garbage’ code is typical of works on choreographies and logic [21, 26], and we share the same motivation: we want to be able to capture the entire flat fragment of the \(\pi \)-calculus, where such garbage code cannot be prohibited. For example, without garbage code, the choreography in Equation (8) would not be a complete representation of the endpoint process in Equation (10) (see also Equation (1)).
Fig. 11.
Simplified presentation of the structural equivalence and reduction semantics for the endpoint calculus, where \(\mathcal {N}[P]\equiv (vx_1\dots x_k) \left( P \;|\;\prod _{i=1}^{n}{\textsf{p}}_i:\!\!\!:T_i \right) \).
4.2 Endpoint Projection
Our choreographies can be mechanically translated into processes via the standard technique of endpoint projection (EPP) [78]. To simplify the presentation of projection, we adopt the standard convention of enriching the language of processes with process names labelling each sequential component of a flat process [50, 78]. That is, a flat process of the form \((vx_1\dots x_k)\left( S_1 \;|\;\cdots \;|\;S_n\right) \) is represented by an endpoint process
where all names \({\textsf{p}}_1,\ldots ,{\textsf{p}}_n\) are distinct.10 The process calculus over these processes is dubbed endpoint calculus.
The definition of endpoint projection is provided by the partial function \(\textsf{EPP}\) in Figure 12 (it is defined only for flat choreographies, as in [25]). It is a straightforward adaptation to our syntax of the textbook presentation of projection [78]. In particular, it uses a merge operator \(\sqcup \) (originally from [23]) to support propagation of knowledge about choices. That is, if a process \(\textsf{r}\) needs to behave differently in two branches of a choice communicated from \({\textsf{p}}\) to \({\textsf{q}}\), it can do so by receiving different labels in these two branches. Merge then produces a term for \(\textsf{r}\) that behaves as prescribed by the first (respectively the second) branch when it receives the first (respectively the second) label. If
is defined for
we say that
is projectable.
which is precisely the one in Equation (1) annotated with process names.
Structural equivalence and reduction semantics for the endpoint calculus are obtained by the one of the \(\pi \)-calculus assuming that each structural equivalence (\(\equiv \)) and reduction step (\(\rightarrow \)) preserves the process names. Note that, for the purpose of studying deadlock-freedom, structural equivalence and reduction rules can be simplified as shown in Figure 11. Each reduction step is labelled by the same labels used in the reduction semantics of choreographies (see Equation (7)), allowing us to retain the information about which sequential components and channel are involved in each reduction step.
Fig. 12.
Endpoint Projection for flat choreographies, and the merge operator (\(\sqcup \)).
Notation 2
If P and Q are endpoint processes, we write \(P\sqsupseteq Q\) iff \(P \sqcup Q = P\).
Theorem 5
Let
be a projectable flat choreography.
Completeness: if
, then
;
Soundness: if
and
, then there is a choreography
such that
and
.
Proof
The proof is obtained by adapting the proof provided in, e.g., [77‐79] to the language we consider in this paper. Details can be found in [4].
4.3 A Sequent Calculus for the Endpoint Calculus
To establish the correspondence between proofs of (formulas encoding) endpoint processes and choreographies, we enrich the syntax of formulas by adding labels (on sub-formulas) carrying the same information of the process names used in the syntax of the endpoint calculus. More precisely, we consider a translation \(\left[ \!\left[ \cdot \right] \!\right] ^\mathcal {N}\) from endpoint processes to annotated formulas of the form \(\left( A\right) _{{\textsf{p}}}\).
Definition 4
For any endpoint process \(P=(vx_1\dots x_k) \left( \prod _{i=1}^{n}{\textsf{p}}_i:\!\!\!:S_i\right) \) we define the formula
, and the sequent \(\left\lfloor \!\left\lfloor P\right\rfloor \!\right\rfloor =\left( [\![ S_1 ]\!]\right) _{{\textsf{p}}_1},\ldots , \left( [\![ S_n ]\!]\right) _{{\textsf{p}}_n}\).
Note that because of the subformula property11 of rules in \(\textsf{PiL}\), such labelling can be propagated in a derivation by labelling each active formula of a rule (which is a sub-formula of one of the principal formulas of the rule) with the same process name of the corresponding active formula.
Example 3
Consider the following derivation in \(\textsf{PiL}\) with conclusion the formula \(\left[ \!\left[ {\textsf{p}}:\!\!\!:x!\langle y\rangle . \textsf{Nil} \;|\;{\textsf{q}}:\!\!\!:x?(y). \textsf{Nil} \right] \!\right] ^\mathcal {N}\):
(11)
Fig. 13.
Sequent calculus rules for the system \(\textsf{ChorL}\).
Fig. 14.
Derivability (in \(\textsf{PiL}\)) of the rules in \(\textsf{ChorL}\).
We now introduce a sequent calculus for the endpoint calculus, given in Figure 13, which consists purely of rules that are derivable in \(\textsf{PiL}\). That is, for every rule \(\textsf{r} \) in \(\textsf{ChorL}\) there is an open derivation in \(\textsf{PiL}\) with the same open premises and conclusion as \(\textsf{r} \).
Lemma 3
Each rule in \(\textsf{ChorL}\) is derivable in \(\textsf{PiL}\).
Moreover, if the premise (resp. conclusion) of a rule in \(\textsf{ChorL}\) is of the form \(\left[ \!\left[ P \right] \!\right] ^\mathcal {N}\), then its conclusion is so (resp. all its premise are so).
Proof
Derivations with the same premise(s) and conclusion of a rule in \(\textsf{ChorL}\) are shown in Figure 14. The second part of the statement follows by rule inspection.
We can refine Theorem 3 for race-free flat processes thanks to the fact that in endpoint processes parallel and restrictions can only occur at the top level. This allows us to consider derivations in \(\textsf{PiL}\) made of blocks of rule applications as those in Figure 14, each corresponding to a single instance of a rule in \(\textsf{ChorL}\).
Theorem 6
A race-free endpoint process P is deadlock-free iff
.
Proof
If \(P=(vx_1\dots x_k) \left( \prod _{i=1}^{n}{\textsf{p}}_i:\!\!\!:S_i\right) \) is deadlock-free, then by Theorem 3 there is a derivation \(\widetilde{\mathcal {D}}\) in \(\textsf{PiL}\) with conclusion \(\left[ \!\left[ P \right] \!\right] ^\mathcal {N}\). Using rule permutations, we can transform \(\widetilde{\mathcal {D}}\) into a derivation made (bottom-up) of possibly some
-rules followed by
-rules (i.e., an open derivation of the same shape of \(\mathcal {D}_{\langle x_1,\ldots ,x_k\rangle }\) or \(\mathcal {D}_{\varnothing }\) from Figure 14), followed by a derivation \(\mathcal {D}\) of the sequent \(\left[ \!\left[ P_1 \right] \!\right] ^\mathcal {N},\ldots , \left[ \!\left[ P_n \right] \!\right] ^\mathcal {N}\) which is organized in blocks of rules as open derivations in Figure 14. Note that derivations of the form \(\mathcal {D}_{\langle {\textsf{p}},x,{\textsf{q}},y,k\rangle }\) (resp. \(\mathcal {D}_{\langle {\textsf{p}},L,{\textsf{q}},L',k\rangle }\)) correspond to the open derivations in Equation (6). Thus we can replace \(\mathcal {D}_{\langle x_1,\ldots ,x_k\rangle }\) or \(\mathcal {D}_{\varnothing }\) by a
, each \(\mathcal {D}_{\langle {\textsf{p}},x,{\textsf{q}},y,k\rangle }\) (resp. \(\mathcal {D}_{\langle {\textsf{p}},L,{\textsf{q}},L',k\rangle }\)) by a
, and each \(\mathcal {D}_n\) with a
, obtaining the desired derivation in \(\textsf{ChorL}\).
The converse is a consequence of Lemma 3 and Theorem 3.
Fig. 15.
Interpretation of a derivation in \(\textsf{ChorL}\) as a choreography.
4.4 Proofs as Choreographies
We can now prove a completeness result of choreographies with respect to the set of deadlock-free flat processes : each deadlock-free flat process is the EPP of a (flat) choreography. To prove this result, we rely on Theorem 6 to establish a direct correspondence between derivations of a sequent encoding a race-free endpoint process in the sequent system \(\textsf{ChorL}\), and execution trees of the same endpoint process. An example the process of choreography extraction from a derivation in \(\textsf{ChorL}\) of a deadlock-free endpoint process can be found in the Appendix of [9].
Theorem 7
Let P be a race-free endpoint process. Then
Proof
If P is deadlock-free, then by Theorem 6 there is a derivation in \(\textsf{ChorL}\) with conclusion \(\left[ \!\left[ P \right] \!\right] ^\mathcal {N}\). We define the choreography
by case analysis on the bottom-most rule \(\textsf{r} \) in \(\mathcal {D}\) as shown in Figure 15. We conclude by showing that
by induction on the structure of \(\mathcal {D}\) reasoning on the bottom-most rule \(\textsf{r} \) in \(\mathcal {D}\). The rigth-to-left implication follows by Theorem 5.
Remark 9
Note that the statement could be made stronger by requiring the choreography
to be flat. In this case, the proof of the right-to-left implication can be proven directly using the inverse of the translation in Figure 15.
Since every flat process in the \(\pi \)-calculus can be decorated with process names, we can easily extend the completeness result to the \(\pi \)-calculus. We need to pay attention to the difference that
(instead of
) because of the definition of
. For example, the choreography that captures \(\textsf{Nil}\;|\;\textsf{Nil}\) is
, and
.
Corollary 2
Every race-free and deadlock-free flat process P admits a choreography
such that
.
An important consequence of our results is that the processes that can be captured by choreographies can have cyclic dependencies, as we exemplified with Equations (1) and (8). This significantly extends the proven expressivity of choreographic languages with name mobility, which so far have been shown to capture only the acyclic processes typable with linear logic [21, 26].
Fig. 16.
Summary of key results in the literature. We describe each column in order: the term constructors for restriction and parallel are separate (independent) in the syntax of processes; cyclic dependencies are allowed; processes can interact (communicate) on a free name (the name does not need to be restricted in the context); choreographies are proven complete for a class of processes (N/A means that this was not considered).
5 Related Work
We now report on relevant related work. A summarising table of the differences between our work and others based on logic is given in Figure 16.
Proofs as Processes: Linear Logic and Session Types. The proofs-as-processes agenda investigates how linear logic [43] can be used to reason about the behaviour of concurrent processes [1, 17]. It has inspired a number of works that aim at preventing safety issues, like processes performing incompatible actions in erroneous attempts to interact (e.g., sending a message with the wrong type). Notable examples include session types [55, 56] and linear types for the \(\pi \)-calculus [63]. The former can actually be encoded into the latter – a formal reminder of their joint source of inspiration [36].
A more recent line of research formally interprets propositions and proofs in linear logic as, respectively, session types and processes [20, 96]. This proofs-as-processes correspondence based on linear logic works for race-free processes, as we consider here. However, it also presents some limitations compared to our framework. Parallel composition and restriction are not offered as independent operators, because of a misalignment with the structures given by the standard rules of linear logic. For example, the \(\textsf{cut}\) rule in linear logic handles both parallel composition and hiding, yielding a ‘fused’ restriction-parallel operator \((\nu x) ( - \;|\;- )\). Also, the \(\otimes \) rule for typing output has two premises, yielding another fused output-parallel operator \(x!(y).( - \;|\;- )\) – note that only bound names can be sent, as in the internal \(\pi \)-calculus [87]. In particular, interaction between processes does not arise simply from parallel composition as in the standard \(\pi \)-calculus, but rather requires both parallel composition and restricting all names on which communication can take place (so communication is always an internal action). This syntactic and semantic gap prevents linear logic from typing safe cyclic dependencies among processes, as in this simplification of Equation (1):
The same gap prevents having communication on unrestricted channels (as in \(x!\langle a\rangle . \textsf{Nil}\;|\;x?(a). \textsf{Nil}\)) and having a private channel used by more than two processes. Using
and \(\mathop \otimes \) to type input and output is also in tension with the associativity and commutativity isomorphisms that come with these connectives. These isomorphisms yield unexpected equivalences at the process level, like \(x?(a). y?(b). \textsf{Nil}\equiv y?(b). x?(a). \textsf{Nil}\).
These shortcomings are not present in our approach, thanks to the use of:
1.
The connective
for prefixing. The latter then has the expected ‘rigid’ non-commutative and non-associative semantics.
2.
The connective
for parallelism. The latter then has the expected equivalences supported by the isomorphisms for
.
3.
Nominal quantifiers, which allow for restricting names without imposing artificial constraints on the structure of processes.
While it is not the first time that these limitations are pointed out, our method is the first logical approach that overcomes them without ad-hoc machinery. Previous works have introduced additional structures to linear logic, like hyperenvironments or indexed families of connectives, in order to address some of these issues [24, 27, 35, 64, 83, 92]. These additional structures are not necessary to our approach.
Choreographic Programming. Choreographic programming was introduced in [77] as a paradigm for simplifying concurrent and distributed programming. Crucial to the success of this paradigm is building choreographic programming languages that are expressive enough to capture as many safe concurrent behaviours as possible [78]. However, most of the work conducted so far on the study of such expressivity is driven by applications, and a systematic understanding of the classes of processes that can be captured in choreographies is still relatively green.
In [31, 61] the authors present methods for choreography extraction – inferring from a network of processes an equivalent choreography – for an asynchronous process calculus, respectively without and with process spawning. Another purely algorithmic extraction procedure is provided in [66], for simple choreographies without data – global types, which are roughly the choreographic equivalent of session types. In linear logic, extracting global types from session types can be achieved via derivable rules [24].
The only previous completeness result for the expressivity of choreographic programming is given in [21, 26], where it is shown that choreographies can capture the behaviours of all well-typed processes in linear logic. Our work extends the completeness of choreographies to processes that, notably, can (i) have cyclic dependencies (like Equation (12)), (ii) perform communication over free channels, (iii) respect the sequentiality of prefixing. Moreover, and similarly to our previous discussion for proofs-as-processes, extraction in [21, 26] requires additional structures (hypersequents and modalities to represent connections) that are not necessary in our method.
Non-Commutative Logic and Nominal Quantifiers. Guglielmi proposed in [45, 46] an extension of multiplicative linear logic with a non-commutative operator modelling the interaction of parallel and sequential operators. This led to the design of the calculus of structures [47], a formalism for proofs where inference rules can be applied at any depth inside a formula rather than at the top-level connective, and the logic \(\textsf{BV}\) including the (associative) non-commutative self-dual connective \(\triangleleft \) to model sequentiality. In [19] Bruscoli has established a computation-as-deduction correspondence between specific derivations in \(\textsf{BV}\) and executions in a simple fragment of \(\textsf {CCS} \). This correspondence has been extended in the works of Horne, Tiu et al. to include the choice operator (\(+\)) of Milner’s \(\textsf {CCS} \) (modelled via the additive connective \(\mathop \oplus \)), as well as the restriction to model private channels in the \(\pi \)-calculus [58, 59]. In these works, restriction has been modelled via nominal quantifiers in the spirit of the ones introduced by Pitts and Gabbay for nominal logic [41, 85], by considering a pair of dual quantifiers12, instead of a single self-dual quantifier as in [68, 73, 86].
The logic \(\textsf{PiL}\) we use as logical framework to establish our correspondences in this paper takes inspiration from Bruscoli’s work and its extension, but it uses a non-associative non-commutative self-dual connective
instead of the \(\triangleleft \) from \(\textsf{BV}\). This seemingly irrelevant difference (the non-associativity of
) guarantees the existence of a \(\textsf{cut}\)-free sequent calculus to be used as a framework for our correspondence, while for the logic \(\textsf{BV}\) and its extension \(\textsf{cut}\)-free sequent calculi cannot exist, as proven in [91]. Note that requiring non-associativity for the connective modelling sequentiality is not a syntactical stretch, because the same restriction naturally occurs in process calculi such as \(\textsf {CCS} \) and the \(\pi \)-calculus, where sequentiality is defined by an asymmetric prefix operation only allowing to sequentially compose (on the left) atomic instructions, such as send and receive. The other main difference is that in these works derivations represent a single execution, while our derivations represent execution trees. This allows us to state our Theorem 3 without quantifying on the set of derivations of \([\![ P ]\!]\).
6 Conclusion and Future Works
We presented a new approach to the study of processes based on logic, which leverages an interpretation of processes in the \(\pi \)-calculus as formulas in the proof system \(\textsf{PiL}\). By seeing derivations as computation trees, we obtained an elegant method to reason about deadlock-freedom that goes beyond the syntactic and semantic limitations of previous work based on logic. This led us to establishing the first completeness result for the expressivity of choreographic programming with respect to mobile processes with cyclic dependencies.
We discuss next some interesting future directions.
Recursion. Recursion could be modelled by extending \(\textsf{PiL}\) with fixpoint operators and rules like the ones in [3, 4, 10, 15, 16]. We foresee no major challenges in extending the proof of cut-elimination for \(\mu \textsf{MALL}\) to \(\textsf{PiL}\), since the behaviour of the connective
is purely multiplicative (in the sense of [6, 34, 44]) and the rules for nominal quantifiers do not require the employment of new techniques. In \(\textsf{PiL}\) with recursion, properties such as justness or fairness could be characterised by specific constraints on derivations, corresponding to constraints on threads and paths of the (possibly cyclic) execution trees.
Asynchronous\(\boldsymbol{\pi }\)-calculus. We foresee the possibility of modelling asynchronous communication by including shared buffers, inspired by previous work on concurrent constraint programming [82, 88] and its strong ties to logic programming [39, 60, 76, 80, 81, 84, 89]. However, buffers with capacity greater than 2 have non-sequential-parallel structures and therefore cannot be described efficiently using binary connectives [30, 94]. We may thus need to consider graphical connectives [2, 5].
Proof Nets. In [8] we define proof nets for \(\textsf{PiL}\), capturing local rule permutations, and providing canonical representative for execution trees up-to interleaving concurrency. This syntax could be used to refine the correspondence between proofs and choreographies (Theorem 7). We plan to study the extension of the computation-as-deduction paradigm in the case of proof net expansion, following the ideas in [7, 12, 13], as well as to use a notion of orthogonality for modules of proof nets (in the sense of [7, 13, 34]) to study testing preorders [18, 37, 38, 49].
Completeness of Choreographies. The literature of choreographic programming languages includes features of practical interest that extend the expressivity of choreographies – like process spawning [32] and nondeterminism [78]. Exploring extensions of \(\textsf{PiL}\) to capture these features is interesting future work. For process spawning, a simple solution could be achieved by defining a way to dynamically assign process names to properly define the map
.
Acknowledgements
Partially supported by Villum Fonden (grants no. 29518 and 50079). Co-funded by the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No 945332. Co-funded by the European Union (ERC, CHORDS, 101124225). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
This can be considered as a variation of Barendregt’s convention. It allows us to avoid variable renaming for universal and nominal quantifier rules in derivations, by assuming the bound variable to be the eigenvariable of the quantifier or the shared fresh name in the case of a pair of dual nominal quantifiers.
In a set of occurrences of formulas, it is assumed that each formula has a unique identifier, differently from a multiset of formulas where each formula has a multiplicity. The former definition simplifies the process of tracing occurrences of formulas in a derivation, as we need in Section 4.
The set \(L'\) of labels the process \({\textsf{q}}\) can accept contains the set L of labels \({\textsf{p}}\) can send. For the continuation of labels in \(L'\setminus L\) we only allow sequential processes because we do not allow nested parallel in the target language of the projection (see next subsection).
By allowing the construct
only in the case in which x is not bound in
, we ensure that choreographies are always written using Barendregt’s convention. This means that each variable x can be bound by at most one restriction \(\nu \), and x cannot appear both free and bound in a choreography
. As a result, we can adopt a lighter labelling discipline for the reduction semantics compared to the one used in [25] – see the rule
in Figure 10.
In the literature, a process P with name \({\textsf{p}}\) is usually written \({\textsf{p}}[P]\) [50, 78]. We adopt the alternative writing \({\textsf{p}}:\!\!\!:P\) to avoid confusion with the notation used for contexts.
Assuming an initial \(\alpha \)-renaming on P such that P is unambiguous, and such each variable bound by a receive action is the same as the unique (because of race-freedom) variable sent by the matching send action. For example, we would write \(x!\langle a\rangle \;|\;x?(a)\) instead of \(x!\langle a\rangle \;|\;x?(b)\).
In [57] the authors report the use of a non-self-dual quantifier to model restriction was suggested them by Alessio Guglielmi in a private communication. As explained in detail in [8], the pair of dual nominal quantifiers in [57‐59] is not the same pair we consider in this paper. This can be observed by looking at the implication
, which is valid in these works, but it is not valid in \(\textsf{PiL}\). For this reason we adopted a different symbol for the dual quantifier of
– i.e., our
instead of their
.
), and nominal quantifiers (
and its dual
) for variable scoping.
; while
.
) and conjunction (\(\mathop \otimes \)) and the additive connectives for disjunction (\(\mathop \oplus \)) and conjunction (
) form multiplicative additive linear logic [43]. We generalize the standard binary \(\mathop \oplus \) and
, allowing them to have any positive arity (including 1) in order to avoid dealing with associativity and commutativity when modelling choices;
) and sequentiality (
), and it is derivable from no assumption (thus also neutral element of \(\mathop \otimes \));
), and its dual ya (
). We observe that these restrict variable scope in formulas in the same way that the \(\nu \) constructor in process calculi restricts the scope of names.
), whose properties reflect the ones of the prefix operator used in standard process calculi (see 
) is defined as
(resp. as \((A \multimap B)\mathop \otimes (B\multimap A)\)), where the negation (\(\bar{\cdot }\)) is defined by the de Morgan duality in Figure 2.
-context is a context \(\mathcal {K}[\bullet ]\) of the form
for a \(n\in \mathbb N\).
. A formula occurring in the conclusion (resp. in a premise) of a rule but in none of its premises (resp. not in its conclusion) is said principal (resp. active). Given a set of rules \(\textsf{X}\), a derivation in \(\textsf{X}\) is a non-empty tree \(\mathcal {D}\) of sequents, whose root is called conclusion, such that every sequent occurring in \(\mathcal {D}\) is the conclusion of a rule in \(\textsf{X}\), whose children are (all and only) the premises of the rule. An open derivation is a derivation whose leaves may be conclusions of no rules, in which case are called open premises. We may denote a derivation (resp. an open derivation with a single open premise \(\Delta \)) with conclusion \(\Gamma \) by
. Finally we may write
if there is an open derivation with premises \(\Gamma _1,\ldots ,\Gamma _n\) and conclusion \(\Gamma \) made only of rules \(\textsf{r} \).
with
and
. If
is a set of nominal variables, we say that x occurs in
if
or
is an element of
. A (nominal) store
is a set of nominal variables such that each variable occurs at most once in
. A judgement
is a pair consisting of a clean sequent \(\Gamma \) and a store
. We write judgements
with
simply as \(\vdash \Gamma \)
. We write
to denote the union of two stores such that a same variable does not occur in both
and
– i.e., a disjoint union.
to denote that the judgement
is derivable in \(\textsf{PiL}\).
is the standard one for first order multiplicative linear logic [43]. The rules \(\mathop \oplus \) and
are generalisations of the standard ones in additive linear logic for the n-ary generalized connectives we consider here; thus, in proof search, the rule \(\mathop \oplus \) keeps only one \(A_k\) among all \(A_i\) occurring in \(\bigoplus _{i=1}^{n} A_i\), and the rule
branches the proof search in n premises. The rule \(\textsf{mix}\) and \(\circ \) are standard for multiplicative linear logic with mix in presence of units5 [28, 40], and the rule
ensures that the unit \(\circ \) is not only the unit for the connectives
and \(\mathop \otimes \), but also for
. The rule
is required to capture the self-duality of the connective
; it should be read as introducing at the same time the connective
and its dual (which in this case is
itself) – as a general underlying pattern for multiplicative connectives, see [2, Remark 5]. The store is used to guarantee that each
is linked to at most a unique
(or vice versa) in any branch of a derivation. If a rule
is applied, then the nominal quantifier is not linked, reason why the rule reminds the standard universal quantifier rule. Otherwise, either the rule
loads a nominal variable in the store, or a rule
uses a nominal variable (of dual type) occurring in the store as a witness variable. Note that in a derivation with the conclusion a judgement with empty store any
is uniquely linked to a
below it.
for any formula A;
, then
;
and
, then
.
Moreover,
.
\(\mathcal {K}[\bullet ]\) we have:
, then
;
for \(i\in \{1,\ldots ,n\}\), then
;
and
, then
.
, then by 
. Details of the proof are available in [
stands for \(A\Rrightarrow B\) and \(B\Rrightarrow A\).
, and we define the standard (structural) equivalence (\(\equiv \)) as the equivalence relation generated by the union of \(\Rrightarrow \) and \(\equiv _{\alpha }\).
(as in [33, 62]). In particular, such a precongruence orients the direction of scope extrusion (by extending the scope of the binder as much as possible), but also rules out those rewritings that may add superfluous information such as \(P\Rrightarrow (P \;|\;\textsf{Nil})\) or \(P\Rrightarrow ((\nu x) P)\) for a \(x\notin \mathcal N_{P}\). Thus in the reduction semantics we consider in this paper we employ the following rule instead of the standard \(\textsf{Struc}\) (see Figure 6):
with
and
. Then \(\textsf{Ent}_{(P,P')}=3\textsf{Ent}_{(Q,Q')}\) and \(\textsf{Core}_{(P,P')}=\textsf{Core}_{(Q,Q')}\).
-formula a process of the form \(x \triangleleft \left\{ \ell :P_\ell \right\} _{\ell \in L}\) (whose session type is a \(\mathop \oplus \)-type) and, dually, by a \(\mathop \oplus \)-formula a process \(x \triangleright \left\{ \ell :P_\ell \right\} _{\ell \in L}\) (whose session type is a
-type). This is only an apparent contradiction because our formulas are not types. Rather, they encode processes whose executions are then derivations in the \(\textsf{PiL}\) system. Under this new interpretation, during proof search the rule for
gives exactly the expected branching of possible executions of terms like \(x \triangleleft \left\{ \ell :P_\ell \right\} _{\ell \in L}\), corresponding to rule \(\textsf{Choice}\) in the reduction semantics. Rule \(\textsf{Label}\) can then be applied ‘afterwards’ (above in the derivation) to select the appropriate branch at the receiver, discarding all the others. Thus, in the formulas-as-processes, receiving a label corresponds to \(\oplus \).
(as in [
and
derive from commutativity and associativity of
(see Proposition 1). The logical equivalences
and
are direct consequence of the ones in Figure 2. The implication \([\![ (\nu x) (P \;|\;Q) ]\!] \multimap [\![ (\nu x) P \;|\;Q ]\!] \) for \(x\notin \textsf{free}(Q)\) is shown in Proposition 1. Finally,
derives from the quantifier shifts
(Figure 2).
, then \([\![ P' ]\!]\multimap [\![ P ]\!]\).
;
.
and 
. More precisely,
.
. Note that all judgements in such a derivation are empty.
- and
-rules only, or blocks as the ones shown in Equation (6) below.
We conclude by induction on the number of such blocks, since each block in the left (resp. right) of Equation (6) identifies an application of a \(\textsf{Com}\) (resp. a \(\textsf{Bra}\) followed by a \(\textsf{Sel}\)).
\(\mathcal {C}[\bullet ]\) such that
.
and
.
.
by the fact that \(\partial _{x_1,\ldots ,x_k} [\![ Q ]\!]\) contains no atoms (i.e., only units) and
(see Proposition 1).
; if the core-reduction is a \(\textsf{Choice}\), there is a set of processes \(\{P_\ell \}_{\ell \in L}\ni P'\) such that
. This is proven by induction on the entropy as in Lemma 2.
.
is not derivable in \(\textsf{PiL}\). This makes our characterisation of progress as powerful as in previous work [22] (where the condition is not made explicit but clearly necessary, see the definition of ‘co-process’ therein).
, the terminated choreography;
, a communication from a process \({\textsf{p}}\) to another \({\textsf{q}}\) with a continuation C (y is bound in C and can appear only under \({\textsf{q}}\));
, a choice by a process \({\textsf{p}}\) of a particular branch L offered by another process \({\textsf{q}}\)8; or
, which restricts x in a choreography
in which the variable x always occur free (i.e., no
occurs in
).9
for a restriction-free (i.e., containing no occurrences of \(\nu \)) choreography
. In the same figure we also provide the reduction semantics of our choreographic language, where each reduction step is labelled by a reduction label
from the following set.
To each reduction label
we associate the set
of processes names and variables occurring in it – i.e.
and
.
executes a communication while
allows a process \({\textsf{p}}\) to make an internal choice. Rule
then communicates a label from \({\textsf{p}}\) to \({\textsf{q}}\), which then continue with the choreography
(but never with a sequential process \(S_\ell \), see Remark 8). Rule
lifts reductions under restrictions. Lastly,
models the standard out-of-order execution of independent communications that can be reduced by rule
– this is the choreographic equivalent of parallel composition in process calculi [78].
It can be executed by applying rule
and then rule
. Note that we do not need to use rule
before applying
, because the set of labels L in the choice constructor is a singleton.
is defined for
we say that
is projectable.
be a projectable flat choreography.
, then
;
and
, then there is a choreography
such that
and
.
, and the sequent \(\left\lfloor \!\left\lfloor P\right\rfloor \!\right\rfloor =\left( [\![ S_1 ]\!]\right) _{{\textsf{p}}_1},\ldots , \left( [\![ S_n ]\!]\right) _{{\textsf{p}}_n}\).
.
-rules followed by
-rules (i.e., an open derivation of the same shape of \(\mathcal {D}_{\langle x_1,\ldots ,x_k\rangle }\) or \(\mathcal {D}_{\varnothing }\) from Figure 14), followed by a derivation \(\mathcal {D}\) of the sequent \(\left[ \!\left[ P_1 \right] \!\right] ^\mathcal {N},\ldots , \left[ \!\left[ P_n \right] \!\right] ^\mathcal {N}\) which is organized in blocks of rules as open derivations in Figure 14. Note that derivations of the form \(\mathcal {D}_{\langle {\textsf{p}},x,{\textsf{q}},y,k\rangle }\) (resp. \(\mathcal {D}_{\langle {\textsf{p}},L,{\textsf{q}},L',k\rangle }\)) correspond to the open derivations in Equation (6). Thus we can replace \(\mathcal {D}_{\langle x_1,\ldots ,x_k\rangle }\) or \(\mathcal {D}_{\varnothing }\) by a
, each \(\mathcal {D}_{\langle {\textsf{p}},x,{\textsf{q}},y,k\rangle }\) (resp. \(\mathcal {D}_{\langle {\textsf{p}},L,{\textsf{q}},L',k\rangle }\)) by a
, and each \(\mathcal {D}_n\) with a
, obtaining the desired derivation in \(\textsf{ChorL}\).
by case analysis on the bottom-most rule \(\textsf{r} \) in \(\mathcal {D}\) as shown in Figure 15. We conclude by showing that
by induction on the structure of \(\mathcal {D}\) reasoning on the bottom-most rule \(\textsf{r} \) in \(\mathcal {D}\). The rigth-to-left implication follows by Theorem 5.
to be flat. In this case, the proof of the right-to-left implication can be proven directly using the inverse of the translation in Figure 15.
(instead of
) because of the definition of
. For example, the choreography that captures \(\textsf{Nil}\;|\;\textsf{Nil}\) is
, and
.
such that
.
and \(\mathop \otimes \) to type input and output is also in tension with the associativity and commutativity isomorphisms that come with these connectives. These isomorphisms yield unexpected equivalences at the process level, like \(x?(a). y?(b). \textsf{Nil}\equiv y?(b). x?(a). \textsf{Nil}\).
for prefixing. The latter then has the expected ‘rigid’ non-commutative and non-associative semantics.
for parallelism. The latter then has the expected equivalences supported by the isomorphisms for
.
instead of the \(\triangleleft \) from \(\textsf{BV}\). This seemingly irrelevant difference (the non-associativity of
) guarantees the existence of a \(\textsf{cut}\)-free sequent calculus to be used as a framework for our correspondence, while for the logic \(\textsf{BV}\) and its extension \(\textsf{cut}\)-free sequent calculi cannot exist, as proven in [91]. Note that requiring non-associativity for the connective modelling sequentiality is not a syntactical stretch, because the same restriction naturally occurs in process calculi such as \(\textsf {CCS} \) and the \(\pi \)-calculus, where sequentiality is defined by an asymmetric prefix operation only allowing to sequentially compose (on the left) atomic instructions, such as send and receive. The other main difference is that in these works derivations represent a single execution, while our derivations represent execution trees. This allows us to state our Theorem 3 without quantifying on the set of derivations of \([\![ P ]\!]\).
is purely multiplicative (in the sense of [6, 34, 44]) and the rules for nominal quantifiers do not require the employment of new techniques. In \(\textsf{PiL}\) with recursion, properties such as justness or fairness could be characterised by specific constraints on derivations, corresponding to constraints on threads and paths of the (possibly cyclic) execution trees.
.
only in the case in which 
, we ensure that choreographies are always written using 
. As a result, we can adopt a lighter labelling discipline for the reduction semantics compared to the one used in [
in Figure 
, which is valid in these works, but it is not valid in 
– i.e., our
instead of their
.
