Multirole Logic and Multiparty Channels

While the first and foremost inspiration for multirole logic originates from studies on multiparty session types in distributed programming, it seems natural in retrospective to introduce multirole logic by exploring the well-known duality between conjunction and disjunction in classical logic. For instance, in a two-sided presentation of the classical sequent calculus (LK), we have the following rules for conjunction and disjunction:

$$\begin{array}[]{c}\underline{A}\vdash\underline{B},A\land B\lx@proof@logical@and\underline{A}\vdash\underline{B},A\underline{A}\vdash\underline{B},B\\[6.0pt] \underline{A},A\land B\vdash\underline{B}\underline{A},A\vdash\underline{B}\kern 18.0pt\underline{A},A\land B\vdash\underline{B}\underline{A},B\vdash\underline{B}\\[6.0pt] \underline{A},A\lor B\vdash\underline{B}\lx@proof@logical@and\underline{A},A\vdash\underline{B}\underline{A},B\vdash\underline{B}\\[6.0pt] \underline{A}\vdash\underline{B},A\lor B\underline{A}\vdash\underline{B},A\kern 18.0pt\underline{A}\vdash\underline{B},A\lor B\underline{A}\vdash\underline{B},B\\ \end{array}$$

where $\underline{A}$ and $\underline{B}$ range over sequents (that are essentially multisets of formulas). One possible explanation of this duality is to think of the availability of two roles $0$ and $1$ such that the left side of a sequent judgment (of the form $\underline{A}\vdash\underline{B}$) plays role $1$ while the right side does role $0$. In addition, there are two logical connectives $\land_{0}$ and $\land_{1}$; $\land_{r}$ is given a conjunction-like interpretation by the side playing role $r$ and disjunction-like interpretation by the other side playing role $1-r$, where $r$ ranges over $0$ and $1$. With this explanation, it seems entirely natural for us to introduce more roles into classical logic.

Multirole logic is parameterized over a chosen underlying set of roles, which may be infinite, and we use ${\overline{\emptyset}}$ to refer to this set. We use $R$ to range over role sets, which are just subsets of ${\overline{\emptyset}}$. Given any role set $R$, we use ${\overline{R}}$ for the complement of $R$ in ${\overline{\emptyset}}$. Also, we use $R_{1}\uplus R_{2}$ for the disjoint union of $R_{1}$ and $R_{2}$ (where $R_{1}\cap R_{2}=\emptyset$ is assumed).

For the moment, let us assume that ${\overline{\emptyset}}$ consists all of the natural numbers less than $N$ for some given $N\geq 2$. Intuitively, a conjunctive multirole logic is one in which there is a logical connective $\land_{r}$ for each $r\in{\overline{\emptyset}}$ such that $\land_{r}$ is given a conjunction-like interpretation by a side playing role $r$ and a disjunction-like interpretation otherwise. If we think of the universal quantifier $\forall$ as an infinite form of conjunction, then what is said about $\land$ can be readily applied to $\forall$ as well. In fact, additive, multiplicative, and exponential connectives in linear logic [\citenameGirard, 1987] can all be treated in a similar manner. Dually, a disjunctive multirole logic can be formulated (by giving $\land_{r}$ a disjunction-like interpretation if the side plays the role $r$ and a conjunction-like interpretation otherwise). We primarily focus on conjunctive multirole logic in this paper.

Given a formula $A$ and a set $R$ of roles, we write $[A]_{R}$ for an i-formula, which is some sort of interpretation of $A$ based on $R$. For instance, the interpretation of $\land_{r}$ based on $R$ is conjunction-like if $r\in R$ holds, and it is disjunction-like otherwise. A crucial point, which we take from studies on multiparty session types, is that interpretation should be based on sets of roles rather than just individual roles. In other words, one side is allowed to play multiple roles simultaneously. A sequent $\Gamma$ in multirole logic is a multiset of i-formulas, and such a sequent is inherently many-sided as each $R$ appearing in $\Gamma$ represents precisely one side. As can be readily expected, the (binary) cut-rule in (either conjunctive or disjunctive) multirole logic is of the following form:

$$\begin{array}[]{l}\Gamma_{1},\Gamma_{2}\lx@proof@logical@and\Gamma_{1},[A]_{R}\Gamma_{2},[A]_{{\overline{R}}}\end{array}$$

The cut-rule can be interpreted as some sort of communication between two parties in distributed programming [\citenameAbramsky, 1994, \citenameBellin & Scott, 1994, \citenameCaires & Pfenning, 2010, \citenameWadler, 2012]. For communication between multiple parties, it seems natural to seek a generalization of the cut-rule that involves more than two sequents. In conjunctive multirole logic, the admissibility of the following rule, which is given the name $\mbox{\it{mp-cut-conj}}(n)$, can be established:

$$\begin{array}[]{l}\vdash\Gamma_{1},\ldots,\Gamma_{n}\lx@proof@logical@and{\overline{R}_{1}}\uplus\cdots\uplus{\overline{R}_{n}}={\overline{\emptyset}}\vdash\Gamma_{1},[A]_{R_{1}}\cdots\vdash\Gamma_{n},[A]_{R_{n}}\end{array}$$

In disjunctive multirole logic, the admissibility of the following rule, which is given the name $\mbox{\it{mp-cut-disj}}(n)$, can be established:

$$\begin{array}[]{l}\vdash\Gamma_{1},\ldots,\Gamma_{n}\lx@proof@logical@and R_{1}\uplus\cdots\uplus R_{n}={\overline{\emptyset}}\vdash\Gamma_{1},[A]_{R_{1}}\cdots\vdash\Gamma_{n},[A]_{R_{n}}\end{array}$$

We may use the name mp-cut to refer to either mp-cut-conj or mp-cut-disj, which itself is a shorthand for multiparty-cut.

In classical logic, the negation operator is clearly one of a kind. With respect to negation, the conjunction and disjunction operators behave dually, and the universal and existential quantifiers behave dually as well. For the moment, let us write $\lnot{A}$ for the negation of $A$. It seems rather natural to interpret $[\lnot{A}]_{R}$ as $[A]_{{\overline{R}}}$. Unfortunately, such an interpretation of negation immediately breaks $\mbox{\it{mp-cut}}(n)$ for any $n\geq 3$ (and it breaks $\mbox{\it{mp-cut}}(1)$ as well). What we discover regarding negation is a bit of surprise: The notion of negation can be generalized to endomorphisms on the underlying set ${\overline{\emptyset}}$ of roles. For instance, if $f$ maps $i$ to $(i+1)~{}\mbox{mod}~{}{3}$ for $i=0,1,2$, then the negation operator $\lnot_{f}$ based on $f$ is of order $3$, that is, $A$ and $\lnot_{f}(\lnot_{f}(\lnot_{f}(A)))$ are equivalent for any formula $A$ in MRL (which is a multirole version of CL)

Furthermore, we incorporate the notion of multirole into intuitionistic logic as well as linear logic, formulating MRLJ and LMRL as multirole versions of IL and CLL, respectively. An immediate application of multirole logic can be found in the practical domain of distributed programming, where we make direct use of LMRL in a design of linearly typed channels for supporting communication between multiple parties.

The rest of the paper is organized as follows. In Section 2, we formulate MRL, a multirole version of first-order classical predicate logic, and then mention some key meta-properties of MRL. In particular, we formally state the admissibility of a cut-rule (mp-cut) involving $n$ sequents for any $n\geq 1$. In Section 3, we present an ultrafilter-based interpretation for intuitionism, formulating MRLJ as a multirole version of first-order intuitionistic predicate logic. We move onto formulating LMRL in Section 4 as a multirole version of first-order linear classical predicate logic. In Section 5, we point out a profound relation between LMRL and session types for multiparty channels. Subsequently, we present in Section 6 and Section 7 a multi-threaded lambda-calculus equipped with linearly typed channels for multiparty communication, where the types for channels are directly rooted in LMRL, and briefly mention some implementation work in Section 8. Lastly, we compare with some closely related work and then conclude.

Let ${\overline{\emptyset}}$ be the underlying (possibly infinite) set of roles for the multirole logic MRL presented in this section. Strictly speaking, this MRL should be referred to as first-order classical multirole predicate logic.

A filter $\mathcal{F}$ on ${\overline{\emptyset}}$ is an ultrafilter if either $R\in\mathcal{F}$ or ${\overline{R}}\in\mathcal{F}$ holds for every subset $R$ of ${\overline{\emptyset}}$. We use $\mathcal{U}$ to range over ultrafilters on ${\overline{\emptyset}}$. When there is no risk of confusion, we may simply use $r$ for the principal ultrafilter at $r$, which is defined as $\{R\subseteq{\overline{\emptyset}}\mid r\in R\}$. If ${\overline{\emptyset}}$ is finite, then it can be readily proven that each $\mathcal{U}$ on ${\overline{\emptyset}}$ is a principal filter at some element $r\in{\overline{\emptyset}}$.

Given an endomorphism $f$ on ${\overline{\emptyset}}$, we use $\lnot_{f}$ for a unary connective. Given an ultrafilter $\mathcal{U}$ on ${\overline{\emptyset}}$, we use $\land_{\mathcal{U}}$ for a binary connective and $\forall_{\mathcal{U}}$ for a quantifier. Note that we may equally choose the name $\lor_{\mathcal{U}}$ for $\land_{\mathcal{U}}$ (and $\exists_{\mathcal{U}}$ for $\forall_{\mathcal{U}}$) as the meaning of the named connective (quantifier) solely comes from the ultrafilter $\mathcal{U}$.

We use $t$ for first-order terms, which are standard (and thus not formulated explicitly for brevity). The formulas in MRL are defined as follows:

$$\begin{array}[]{lrcl}\mbox{formulas}&A,B&::=&a\mid{\lnot_{f}}(A)\mid A\,{\land_{\mathcal{U}}}\,B\mid{\forall_{\mathcal{U}}}(\lambda x.A)\\ \end{array}$$

where $a$ ranges over pre-defined primitive formulas. Instead of writing something like $\forall_{\mathcal{U}}x.A$, we write $\forall_{\mathcal{U}}(\lambda x.A)$, where $x$ is a bound variable. Given a formula $A$, a term $t$ and a variable $x$, we use $A[t/x]$ for the result of substituting $t$ for $x$ in $A$ and treat it as a proper subformula of $\forall_{\mathcal{U}}(\lambda x.A)$. For notational convenience, we may also write $f(A)$ for ${\lnot_{f}}(A)$, $\mathcal{U}(A_{1},A_{2})$ for $A_{1}\,{\land_{\mathcal{U}}}\,A_{2}$, and $\mathcal{U}(\lambda x.A)$ for ${\forall_{\mathcal{U}}}(\lambda x.A)$.

Note that there is no connective for implication in MRL. If desired, one may simply treat $A\,{\supset_{f,\mathcal{U}}{B}}$ as $\mathcal{U}(f(A),B)$. We are only to introduce $\supset_{f,\mathcal{U}}$ as a primitive connective corresponding to implication for each given pair of $f$ and $\mathcal{U}$ when formulating an intuitionistic version of MRL.

Given a formula $A$ and a set $R$ of roles, $[A]_{R}$ is referred to as an i-formula (for interpretation of $A$ based on $R$). Let us use $\Gamma$ for multisets of i-formulas, which are also referred to as sequents. The inference rules for MRL are listed in Figure 1. In the rule ($\forall$-pos), $x\not\in\Gamma$ means that $x$ does not have any free occurrences in i-formulas contained inside $\Gamma$. Please note that a sequent $\Gamma$ in this formulation is many-sided (rather than one-sided) as every $R$ appearing $\Gamma$ represents precisely one side.

Let us use $|A|$ for the size of $A$, which is the number of connectives contained in $A$, and use $\mathcal{D}$ for derivations of sequents, which are just trees containing nodes that are applications of inference rules. Given a derivation $\mathcal{D}$, $\mbox{\it ht}(\mathcal{D})$ stands for the tree height of $\mathcal{D}$. When writing $\mathcal{D}::\Gamma$, we mean that $\mathcal{D}$ is a derivation of $\Gamma$, that is, $\Gamma$ is the conclusion of $\mathcal{D}$. We may use the following format to present an inference rule:

$$(\Gamma_{1};\ldots;\Gamma_{n})\Rightarrow\Gamma_{0}$$

where $\Gamma_{i}$ for $1\leq i\leq n$ are the premisses of the rule and $\Gamma_{0}$ the conclusion. Such an inference rule is said to be admissible if its conclusion is derivable whenever its premisses are. Given two i-formulas $[A]_{R_{1}}$ and $[B]_{R_{2}}$, we write $[A]_{R_{1}}\Rightarrow[B]_{R_{2}}$ to mean that the rule $(\Gamma,[A]_{R_{1}})\Rightarrow(\Gamma,[B]_{R_{2}})$ is admissible. And we write $A\Rightarrow B$ if $[A]_{R}\Rightarrow[B]_{R}$ holds for any role set $R$. For instance, for any ultrafilter $\mathcal{U}$ and formulas $A$ and $B$, we have $\mathcal{U}(A,B)\Rightarrow\mathcal{U}(B,A)$. In addition, we write $[A]_{R_{1}}\Leftrightarrow[B]_{R_{2}}$ for both $[A]_{R_{1}}\Rightarrow[B]_{R_{2}}$ and $[B]_{R_{2}}\Rightarrow[A]_{R_{1}}$, and $A\Leftrightarrow B$ for both $A\Rightarrow B$ and $B\Rightarrow A$.

As a new form of logic, MRL may not seem intuitive. We present as follows some simple properties to facilitate the understanding of MRL.

Given an endomorphism $f$ on ${\overline{\emptyset}}$, we refer to $f$ as a permutation if it is actually a bijection and use $\overline{f}$ for the inverse permutation of $f$. Please note that $\overline{f}(R)={f}^{-{\kern-1.0pt}1}(R)$ for any role set $R$.

Given two endomorphisms $f_{1}$ and $f_{2}$ on ${\overline{\emptyset}}$, we write $f_{1}\cdot f_{2}$ for a composition of $f_{1}$ and $f_{2}$ such that $(f_{1}\cdot f_{2})(r)=f_{2}(f_{1}(r))$ for $r\in{\overline{\emptyset}}$. The set of permutations on ${\overline{\emptyset}}$ forms a group where the group unit is the identity function ${\it id}$, and the group inverse of $f$ is $\overline{f}$, and the group product of $f_{1}$ and $f_{2}$ is $f_{1}\cdot f_{2}$. Given a natural number $n$, $f^{n}$ is defined to be ${\it id}$ if $n=0$ and $f\cdot{f^{n-1}}$ if $n>0$. The order of $f$, if exists, is the least positive integer $n$ such that $f^{n}={\it id}$.

The classical sequent calculus LK of Gentzen is a special case of MRL where ${\overline{\emptyset}}=\{0,1\}$. In a two-sided formulation of LK, let us assume that the left side plays role $1$ and the right side does role $0$; the negation operator $\lnot$ is $\lnot_{f}$ for $f=(0\;1)$, that is, $f(0)=1$ and $f(1)=0$; the conjunction operator $\land$ is $\land_{0}$, where $0$ refers to the principal ultrafilters at $0$, and the disjunction operator $\lor$ is $\land_{1}$; the universal quantifier $\forall$ is $\forall_{0}$, and the existential quantifier $\exists$ is $\forall_{1}$. Clearly, the order of the permutation $(0\;1)$ is $2$. Therefore, we have $A\Leftrightarrow\lnot(\lnot(A))$.

Clearly, Proposition 2.6 suggests that many notions of duality in mathematics can and should be revisited in the context of multirole logic.

If in classical logic the most prominent logical connective is negation, then it is implication in intuitionistic logic. Given an endomorphism $f$ and an ultrafilter $\mathcal{U}$ (on ${\overline{\emptyset}}$), we introduce a logical connective $\supset_{f,\mathcal{U}}$ in MRLJ (for representing the notion of implication). The formulas in MRLJ are defined as follows:

$$\begin{array}[]{lrcl}\mbox{formulas}&A,B&::=&a\mid{\lnot_{f}}(A)\mid A\,{\land_{\mathcal{U}}}\,B\mid A\,{\supset_{f,\mathcal{U}}{B}}\mid{\forall_{\mathcal{U}}}(\lambda x.A)\\ \end{array}$$

We may also write $\mathcal{U}_{f}(A,B)$ for $A\,{\supset_{f,\mathcal{U}}{B}}$.

Intuitionistic multirole logic is parameterized over a fixed ultrafilter on ${\overline{\emptyset}}$. In MRLJ, we refer to this ultrafilter as $\mathcal{J}$. Every inference rule in Figure 1 is also an inference rule in MRLJ if it is $\mathcal{J}$-intuitionistic. In addition, we have the following rules for handling implication:

$$\begin{array}[]{c}\vdash\Gamma,[A\,{\supset_{f,\mathcal{U}}{B}}]_{R}\lx@proof@logical@and R\not\in\mathcal{U}\vdash\Gamma,[A]_{{f}^{-{\kern-1.0pt}1}(R)},[B]_{R}\\[6.0pt] \vdash\Gamma_{1},\Gamma_{2},[A\,{\supset_{f,\mathcal{U}}{B}}]_{R}\lx@proof@logical@and R\in\mathcal{U}\vdash\Gamma_{1},[A]_{{f}^{-{\kern-1.0pt}1}(R)}\vdash\Gamma_{2},[B]_{R}\\[6.0pt] \end{array}$$

The intuitionistic sequent calculus LJ of Gentzen is a special case of MRLJ where ${\overline{\emptyset}}=\{0,1\}$ and $\mathcal{J}$ is the principal filter at $1$; the implication connective $\supset$ is $\supset_{f,\mathcal{U}}$ for $f=(0\;1)$ and $\mathcal{U}$ being the principal filter at $0$. As an example, the well-known fact that $A\supset\lnot{B}$ implies $B\supset\lnot{A}$ in LJ can be generalized in MRLJ as follows:

In LJ, $[A]_{R}\Rightarrow[B]_{R}$ can be internalized as $[A\supset B]_{R}$ if $R=\{1\}$. This form of internalization can be generalized in MRLJ as follows:

We see the very ability to incorporate intuitionism into multirole logic as solid evidence in support of multirole being an inherent notion in logic.

In this section, we generalize classical linear logic (CLL) to linear multirole logic (LMRL), which is to guide subsequently a design of linearly typed channels for multiparty communication in distributed programming.

Let ${\overline{\emptyset}}$ be the full set of roles for LMRL. For each endomorphism $f$ on ${\overline{\emptyset}}$, we assume a corresponding unary connective $\lnot_{f}$ (generalized negation). For each ultrafilter $\mathcal{U}$ on ${\overline{\emptyset}}$, we assume two binary connectives ${\&}_{\mathcal{U}}$ and ${\otimes}_{\mathcal{U}}$ (corresponding to ${\&}$/${\oplus}$ and ${\otimes}$/${\invamp}$ in linear logic, respectively) and a unary connective ${!}_{\mathcal{U}}$ (corresponding to ${!}$/${?}$ in linear logic) and a quantifier $\forall_{\mathcal{U}}$ (corresponding to $\forall$/$\exists$). The formulas in LMRL are defined as follows:

$$\begin{array}[]{lrcl}\mbox{formulas}&A,B&::=&a\mid{\lnot_{f}}(A)\mid A\,{{\otimes}_{\mathcal{U}}{B}}\mid A\,{{\&}_{\mathcal{U}}{B}}\mid{!}_{\mathcal{U}}({A})\mid{\forall_{\mathcal{U}}}(\lambda x.A)\\ \end{array}$$

We may write $[{?}(A)]_{R}$ to mean $[{!}_{\mathcal{U}}({A})]_{R}$ for some $R\not\in\mathcal{U}$, and $?(\Gamma)$ to mean that each i-formula in $\Gamma$ is of the form $[{?}(A)]_{R}$.

The inference rules for LMRL are listed in Figure 2. Note that there are one rule for each $\lnot_{f}$, and one positive rule and two negative rules for each ${\&}_{\mathcal{U}}$, and one positive rule and one negative rule for each ${\otimes}_{\mathcal{U}}$, and one positive rule and three negative rules for each ${!}_{\mathcal{U}}$, and one positive rule and one negative rule for each $\forall_{\mathcal{U}}$. Let us take the rule (${\&}$-neg-l) as an example; the i-formula $[A\,{{\&}_{\mathcal{U}}{B}}]_{R}$ is referred to as the major i-formula of the rule. Let us take the rule (${\otimes}$-pos) as another example; the i-formula $[A\,{{\otimes}_{\mathcal{U}}{B}}]_{R}$ is referred to as the major i-formula of the rule. The major i-formulas for the other rules (excluding the rule (Id)) should be clear as well. For the rule (Id), each $[a]_{R_{i}}$ is referred to as a major i-formula.

Please recall that $|A|$ is for the size of $A$ that is, the number of connectives contained in $A$, and $\mathcal{D}$ for a derivation tree and $\mbox{\it ht}(\mathcal{D})$ for the height of the tree. Also, we use $\mathcal{D}::\Gamma$ for a derivation of $\Gamma$.

The following lemmas in LMRL are the counterparts of of a series of lemmas (Lemma 2.9, Lemma 2.11, Lemma 2.13, Lemma 2.15, Lemma 2.17, and Lemma 2.8) in MRL.

Given an i-formula $[A]_{R}$, let us use $\{[A]_{R}\}$ for a sequent consisting of only $[A]_{R}$ if $A$ is not of the form ${!}_{\mathcal{U}}({B})$ for $R\not\in\mathcal{U}$ or some repeated occurrences of $[A]_{R}$ otherwise (that is, if $A$ is of the form ${!}_{\mathcal{U}}({B})$ for $R\not\in\mathcal{U}$).

By following some recent work on encoding cut-elimination as reduction in variants of $\pi$-calculus [\citenameCaires & Pfenning, 2010, \citenameWadler, 2012], we can readily formulate a variant of $\pi$-calculus in which process reduction follows precisely the strategy employed in the proof of Lemma 4.9 for reducing the complexity of a cut-formula. Alternatively, we can interpret formulas in LMRL as session types for channels in a multi-threaded lambda-calculus and various meta-properties of LMRL as certain (primitive) functions on channels. We take the alternative here as it is closer to the goal of implementing session-typed multiparty channels for practical use.