# Concurrent Realizability on Conjunctive Structures

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, Étienne Miquey

► To cite this version:

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, Étienne Miquey. Concurrent Realizability on Conjunctive Structures. FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. hal-04083002v2

HAL Id: hal-04083002

https://inria.hal.science/hal-04083002v2

Submitted on 28 Apr 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Concurrent Realizability on Conjunctive Structures

Emmanuel Beffara ☐

Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, 38000 Grenoble, France

Félix Castro ☐

IRIF, Université Paris Cité, France

IMERL, Facultad de Ingeniería, Universidad de la República, Uruguay

Mauricio Guillermo ☐

IMERL, Facultad de Ingeniería, Universidad de la República, Uruguay

Étienne Miquey ☐

Aix-Marseille Université, CNRS, I2M, Marseille, France

## Abstract

This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.

**2012 ACM Subject Classification** Theory of computation → Process calculi; Theory of computation → Proof theory; Theory of computation → Linear logic

**Keywords and phrases** Realizability, Process Algebras, Concurrent Processes, Linear Logic

**Funding** This work was partially supported by projects STIC-AmSud *Qapla'* and *APCoRe*.

# 1 Introduction

## 1.1 Realizability and its algebrization

Realizability provides a well-established and general set of techniques for studying the relationships between programs and proofs. In the traditional presentation of intuitionistic realizability, one starts from a set $A$ of realizers, which are objects with computational meaning, programs in some formalism (codes of recursive functions, $\lambda$-terms, etc). Logic is then interpreted in the powerset of $A$, in such a way that the meaning of a formula is essentially a set of programs sharing a computational behavior dictated by the formula. From an algebraic viewpoint, the set $A$ induces in its powerset a *Heyting algebra*, which in turn induces a *topos* [12, 20].

Classical realizability adapts these principles to classical logic, building on different foundations [13]. The computational part is based on the duality between programs (potential proofs) and environments (counter-proofs). The proper categorical structure underlying classical realizability was discovered by Streicher [22] and involves an *ordered combinatory algebra* (OCA) induced by terms and stacks. This construction was later generalized in a different setting, namely Krivine ordered combinatory algebras [6], with the feature that Streicher's construction can be carried out in a purely axiomatic context. In particular, both truth values and realizers belong to the underlying set of these structures and the partial order subsumes subtyping, term reduction and the realizability relation. A similar approach was later followed within Miquel's implicative algebras [15] (and some variants by the last
author's [16]), a slightly different structure which allows to encompass intuitionistic and
classical models of forcing and realizability into a general framework, keeping the feature that
truth values and realizers (and also forcing conditions) both belong to the underlying set of
the implicative algebra. All these works therefore advocate for foundations of realizability
seeking to transform a rather complex and operational definition into a much simpler and
algebraic one.

## 1.2 Logic for concurrency

Process calculi form a wide range of formalisms designed to model concurrent systems and reason about them by means of term rewriting. Their applications are diverse, from the semantics of proof systems to the conception of concrete programming languages. Type systems for such calculi are therefore a wide domain, with systems of different kinds designed to capture different behaviors and ensure different properties of processes: basic interfacing, input-output discipline, linearity, lock-freeness, termination, respect of communication protocols, etc. To better understand the diversity of calculi and uncover basic structures and general patterns, many authors have searched for languages with simpler or more general theory in which the most features could be expressed by means of restrictions or encodings. Similar unification has been searched for in the realm of types, but no system can yet claim to be as basic and universal as, e.g., simple types for the λ-calculus, which perfectly capture the abstraction and application mechanism in the logical world.

Concurrent realizability, developed by Beffara [2], transposes the ideas of classical realizability in a context of interacting concurrent processes. Following the constructions of phase semantics from linear logic [8] and ludics [9], the combinatory algebra is replaced with a variant of the π-calculus, endowed with a structure of commutative monoid under parallel composition. The pole, which defines orthogonality as in classical realizability, is seen as a testing protocol between processes, and the sets of processes that are closed by biorthogonality act both as truth values and behaviors. However, in the original construction, processes are subject to polarization and interfacing constraints which restrict the use of names, in order to avoid ambiguity when composing and to ensure consistency. As a consequence, operations over behaviors inherit such restrictions, which makes them partial in general.

The aim of the present work is to set the basis for an algebraic presentation of concurrent realizability, as a way to study processes and their types in a well-structured algebraic framework. We propose that, as with sequential models, the algebraic presentation is based on an ordered algebraic structure which must allow interpreting truth values and concurrent programs in its underlying set, subsuming the reduction semantics in the order relation. Furthermore, we want to avoid imposing a priori restrictions on processes.

## 1.3 Principles of the construction

We aim for an algebraic structure in which we can represent processes, types and operators
in a uniform setting and we will refer to elements of such a structure as *behaviors*. A guiding
intuition is to see behaviors as particular sets of terms in a process algebra, with some notion
of closure by observational equivalence (a formal implementation is presented in Section 4).
We postulate three fundamental structures over behaviors:

- a complete lattice structure, taking a comparison $a \leq b$ to mean that $b$ exhibits more possible behaviors than $a$;

- a binary operator $\otimes$, continuous with respect to the lattice structure, that represents an operation of parallel composition without interaction.
an anti-monotone unary operator (·)⊥ s.t. a⊥ represents the tests that a passes.

This yields a variant of the last author’s conjunctive structure [16], including notions of arrow
and application and allowing for a sound interpretation of multiplicative linear logic. Within
this framework, we study parallel composition as an additional continuous binary operation
in the conjunctive structure.

Note that the notion of *name*, though pervasive in process algebra, is not taken to be
primitive because different calculi and type systems make different choices on the use of
names and actions (monadicity vs polyadicity, polarization, synchrony, etc). Instead, we
consider that the multiplicative structure includes some way of managing connections between
processes so that the axioms are satisfied.

1.4 Outline of the paper

We start by introducing in Section 2 the conjunctive structures that we identified to be conducive to the analysis of concurrent computation from an algebraic viewpoint. In Section 3, we develop a construction over process algebras to formally extend a language of processes with generalized fusions (PGF), on top of which we build a realizability model in Section 4 with the expected algebraic structure. We then explain in Section 5 how to equip conjunctive structures with parallelism and we illustrate it in the case of PGF. In Section 6, we prove that parallel composition cannot have an internal representation in the axioms of purely conjunctive structures, using a model that validates these axioms but does not have an operator for general parallel composition.

2 Logic in conjunctive structures

Following the program of algebrization of realizability models that was mostly undertaken
in the realm of Krivine realizability [22, 6, 15, 16] and previous work by the first author on
concurrent computation [2], we introduce a particular class of *conjunctive algebras* which we
identify as the key algebraic structures underlying realizability models induced by process
calculi. We first define the notion of *conjunctive structure*, which reflects the algebraic
structure of these models (*how are the truth values defined?*), and then define a notion of
*separator* that allows to capture the logical content (*which processes define valid realizers?*).

**2.1 Conjunctive structures**

► **Definition 1.** A conjunctive structure (CS) is a tuple $(C, \prec, \otimes, (\cdot)^\perp)$ such that

1. $(C, \prec)$ is a complete lattice;

2. $\otimes$ is a binary monotone operation of $C$ and $(\cdot)^\perp$ is a unary antimonotone function on $C$;

3. $\otimes$ distributes over the join operation $\Upsilon$, i.e. for any $a \in C$ and $\mathfrak{B} \subseteq C$ we have $\Upsilon_{b \in \mathfrak{B}}(a \otimes b) = a \otimes (\Upsilon_{b \in \mathfrak{B}} b)$ and $\Upsilon_{b \in \mathfrak{B}}(b \otimes a) = (\Upsilon_{b \in \mathfrak{B}} b) \otimes a$;

4. the orthogonal map $(\cdot)^{\perp}$ satisfies De Morgan's law $(\Upsilon_{b \in \mathfrak{B}} b)^{\perp} = \lambda_{b \in \mathfrak{B}} b^{\perp}$.

We say that the structure is involutive (CIS) if $(\cdot)^{\perp}$ is involutive: $a^{\perp\perp} = a$ for all $a \in C$.
Also we call unitary every CS (resp. CIS) with a distinguished element $1 \in C$.

To draw the comparison with the conjunctive structures defined in the last author’s
work [16], the only difference lies in the use of an orthogonal map instead of a negation $\neg$
that was meant to convey a computational content. In particular, even in the classical case,
$a$ and $\neg\neg a$ are logically equivalent but not necessarily equal.
**Example 2.** Any complete Boolean algebra ($\mathbb{B}$, $\prec$, $\wedge$, $\vee$, $\neg$) defines a CIS using the conjunction as tensor ($a \otimes b \triangleq a \wedge b$) and the negation for orthogonal map ($a^{\perp} \triangleq \neg a$).

**Example 3.** A phase space [8] is defined by a commutative monoid $M$ and a subset $\perp \subseteq M$. For $a \subseteq M$, define the dual $a^{\perp} \triangleq \{x : \forall y \in a, xy \in \perp\}$; define $a \otimes b \triangleq \{xy : x \in a, y \in b\}^{\perp\perp}$ for $a, b \subseteq M$. Then the set of subsets $a \subseteq M$ such that $a^{\perp\perp} = a$ forms a CIS.

Given a conjunctive structure $(\mathbb{C}, \prec, \otimes, (\cdot)^{\perp})$, we define the usual connectives and quantifiers of multiplicative linear logic (MLL) on $\mathbb{C}$ as follows, where $F$ is a function over $\mathbb{C}$:

$$ a \mathfrak{R} b \triangleq (a^{\perp} \otimes b^{\perp})^{\perp} \qquad a \to b \triangleq (a \otimes b^{\perp})^{\perp} \qquad \exists F \triangleq \bigvee_{a \in \mathbb{C}} F(a) \qquad \forall F \triangleq \bigwedge_{a \in \mathbb{C}} F(a) $$

These definitions induce a canonical interpretation of MLL formulas within any CIS.

**Definition 4.** Consider a unitary CS $(\mathbb{C}, \prec, \otimes, (\cdot)^{\perp}, 1)$. The interpretation of closed MLL formulas with parameters $P \in \mathbb{C}$ is defined as follows:

$$ \begin{align*} [[1]] &\triangleq 1 & [[A \otimes B]] &\triangleq [[A]] \otimes [[B]] & [[\exists X.A]] &\triangleq \exists (P \mapsto [[A]]\{X := P\}) \\ [[\perp]] &\triangleq 1^{\perp} & [[A \mathfrak{R} B]] &\triangleq [[A]] \mathfrak{R} [[B]] & [[\forall X.A]] &\triangleq \forall (P \mapsto [[A]]\{X := P\}) \\ [[P]] &\triangleq P & & & & \\ \end{align*} $$

Given a sequent $\vdash A_1, \dots, A_k$, the interpretation $[[A_1, \dots, A_k]]$ is defined as $[[A_1]]$ if $k=1$ and $[[A_1]] \mathfrak{R} [[A_2, \dots, A_k]]$ otherwise.

**Remark 5.** As usual, the interpretation $[[A]]$ of a formula $A$ depends only upon the assignment of the free variables of $A$. The same is valid for sequents.

**Remark 6.** If $\mathbb{C}$ is a CIS, the involutivity of $(\cdot)^{\perp}$ actually implies that $(\mathbb{C}, \prec, \neg)$ is an implicative structure in the sense of Miquel [15] since $\neg$ satisfies the expected variance and continuity properties: in particular $(\Upsilon_{b \in B} b) \negrightarrow a = \lambda_{b \in B} (b \negrightarrow a)$ for any $a \in \mathbb{C}$ and $B \subseteq \mathbb{C}$.

Note that this applies to *structures*, which only define operators and their relationships. The *algebras* defined below, which include a notion of logical validity, will actually diverge since implicative algebras model intuitionistic logic, while our algebras apply to linear logic.

## 2.2 Separators and internal logic

Conjunctive structures are suited to interpret formulas of MLL. To account for a validity notion, we need to introduce the notion of separator [15, 16], a subset of the structure which intuitively distinguishes valid formulas, similarly to a filter in a Boolean algebra. Separators are built upon a set of combinators that one can understand as axioms for the internal logic.

**Definition 7.** Consider a unitary CS $(\mathbb{C}, \prec, \Upsilon, (\cdot)^{\perp}, 1)$. The MLL combinators are:

$$ \begin{align*} S_3 &\triangleq \lambda_{a,b \in \mathbb{C}} (a \otimes b) \to (b \otimes a) & S_6 &\triangleq \lambda_{a \in \mathbb{C}} a \to (1 \otimes a) \\ S_4 &\triangleq \lambda_{a,b,c \in \mathbb{C}} (a \to b) \to (a \otimes c) \to (b \otimes c) & S_7 &\triangleq \lambda_{a \in \mathbb{C}} (1 \otimes a) \to a \\ S_5 &\triangleq \lambda_{a,b,c \in \mathbb{C}} ((a \otimes b) \otimes c) \to (a \otimes (b \otimes c)) & S_8 &\triangleq \lambda_{a,b \in \mathbb{C}} (a \to b) \to (b^{\perp} \to a^{\perp}) \end{align*} $$

$$ S_4 \triangleq \lambda_{a,b,c \in \mathbb{C}} (a \to b) \to (a \otimes c) \to (b \otimes c) \qquad S_7 \triangleq \lambda_{a \in \mathbb{C}} (1 \otimes a) \to a $$

$$ S_5 \triangleq \lambda_{a,b,c \in \mathbb{C}} ((a \otimes b) \otimes c) \to (a \otimes (b \otimes c)) \qquad S_8 \triangleq \lambda_{a,b \in \mathbb{C}} (a \to b) \to (b^{\perp} \to a^{\perp}) $$

The definitions (and names) for $S_3$, $S_4$ and $S_5$ come from the notion of separator in conjunctive algebras [16]. The original $S_1$ and $S_2$ are replaced here by $S_6$, $S_7$ and $S_8$ to account for linearity. The set of combinators $\{S_3, \dots, S_8\}$ is known to be complete for MLL [1].

**Definition 8.** Let us consider $(\mathbb{C}, \prec, \Upsilon, (\cdot)^{\perp}, 1)$ a unitary CIS. A monoidal separator on $\mathbb{C}$ is an upwards closed set $S \subseteq \mathbb{C}$ such that:

$$ S \text{ contains the MLL-combinators } S_3, \dots, S_8. $$
<figure><img src="image_2.png" /><figcaption>Figure 1 Semantic typing rules for MLL</figcaption></figure>

For any $a, b \in \mathbb{C}$, if $a \dashv b \in S$ and $a \in S$ then $b \in S$.

A conjunctive involutive monoidal algebra (CIMA) is a unitary $\mathbb{C}$ CIS together with a monoidal separator $S$.

**Example 9.** In any CIS induced by a complete Boolean algebra $\mathbb{B}$ (see Example 2), all the combinators are tautologies trivially interpreted by the maximal element $\top$. Therefore, the singleton $\{\top\}$ (or alternatively any filter on $\mathbb{B}$) defines a separator for this CIS.

**Definition 10.** Let $\mathbb{C}$ be a CS. A semantic judgement is a statement $\vdash a : \Gamma$ where $a \in \mathbb{C}$ and $\Gamma$ is a sequent of formulas with parameters in $\mathbb{C}$. Such a judgement is sound if $a \preceq \llbracket \Gamma \rrbracket$. A semantic typing rule is an inference rule where the premises and conclusion are semantic judgements, possibly involving free variables. Such a rule is sound if the soundness of its premises entails that of its conclusion for any instantiation of the variables in $\mathbb{C}$.

We provide semantic typing rules for MLL in Figure 1, Using the following terms, where $\sigma : [1; k] \to [1; k]$ is a permutation and $a * b \triangleq \lambda \{c \in \mathbb{C} \mid a \prec b \to c\}$ is the usual application from implicative algebras:

$$ 
\begin{align*}
\mathbf{I} &\triangleq \lambda_{a \in \mathbb{C}} (a \to a) \\
\mathbf{t} &\triangleq \lambda_{a,b,g,d \in \mathbb{C}} ((g \mathfrak{R} a) \to (b \mathfrak{R} d) \to g \mathfrak{R} ((a \otimes b) \mathfrak{R} d)) \\
\mathbf{c} &\triangleq \lambda_{a,g,d \in \mathbb{C}} ((g \mathfrak{R} a) \to (a^{\perp} \mathfrak{R} d) \to (g \mathfrak{R} d)) \\
\mathbf{ex}(\sigma) &\triangleq \lambda_{a_1, \dots, a_k \in \mathbb{C}} ((a_1 \mathfrak{R} \dots \mathfrak{R} a_k) \to (a_{\sigma(1)} \mathfrak{R} \dots \mathfrak{R} a_{\sigma(k)}))
\end{align*}
$$

**Proposition 11.** For any CIMA $(\mathbb{C}, S)$ and any permutation $\sigma$, the combinators $\mathbf{I}$, $\mathbf{t}$, $\mathbf{c}$ and $\mathbf{ex}(\sigma)$ belong to the separator $S$

*Proof.* These proofs are essentially simple combinatorial manipulations within conjunctive involutive structures. We detail here the proof that $\mathbf{I} \in S$ as an example. Let us consider a CIMA $(\mathbb{C}, S)$ and define:

$$ S'_4 \triangleq \bigwedge_{a,b,c \in \mathbb{C}} (a \to b) \to (b \to c) \to a \to c \qquad t \circ s \triangleq S'_4 * s * t $$

It is an easy exercise to check that $S'_4 \in S$ (this follows from combinatorial manipulations using the closure under modus ponens and the fact that $S_4, S_8 \in S$). Besides, similarly to what happens for implicative algebras, separators of CIMAs are closed under application $*$, and as such they are also closed under composition $\circ$. To prove that $\mathbf{I} \in S$, observe that for any $a \in \mathbb{C}$ we have $S_6 \prec a \to a \otimes \mathbf{1}$ and $S_7 \prec a \otimes \mathbf{1} \to a$. Then $S_7 \circ S_6 \prec a \to a$ (uniformly on $a \in \mathbb{C}$) and thus we get $S_7 \circ S_6 \in S$ and then $\lambda_{a \in \mathbb{C}} a \to a \in S$. $\quad$

**Theorem 12.** The semantic typing rules of Figure 1 are sound for all unitary CS. Moreover, for any CIMA $(\mathbb{C}, S)$ if $\vdash a : \Gamma$ is provable, then $a \in S$.
**Proof.** The soundness of rule (1) is just reflexivity of $\prec$ and that of rules (AX), ($\forall$) and ($\exists$) holds by definition of the meet operation. For the other rules, remark that if for some $a, b, t, u \in \mathbb{C}$ we have $t \prec a \neg b$ and $u \prec a$, then $t \prec u \neg b$, hence $t * u \prec b$ by definition of $*$. This entails the soundness of (EX), ($\otimes$) and (CUT) by definition of **I**, **t** and **c**.

Besides, by definition of $*$, we also have $a \prec b \neg a * b$ for all $a$ and $b$, which implies that separators are closed under $*$. This, with the results of Proposition 11, entails that the left-hand sides of derivable judgements are always in $S$. ◀

As a consequence, we conclude that all provable MLL formulas are interpreted by elements in the separator (i.e. validated by the model).

As stated in Remark 6, unitary CISs are implicative structures while in general CIMAs are not implicative algebras. Due to the chosen notion of separator, CIMAs do not (in general) model intuitionistic logic. Nevertheless, some specific CIMAs can model intuitionistic or classical logics if their separators contains non linear terms.

## 3 Processes with global fusions

In this section, we define a computational structure that will serve as our reference. We first recall the basic definitions of a standard $\pi$-calculus, then we build processes with fusions as a formal extension of this language. These fusions, being an additional structure to extend the expressiveness of an existing algebra (as opposed to a feature that we would impose on the underlying calculus, which would restrict the range of calculi our study applies to), bring the necessary connections to realize MLL axioms.

Hence, it should be made clear that the point of this section is not to define “yet another $\pi$-calculus” but, on the contrary, to show that our study applies to any process calculus. The only technical constraint is that the combinators from Definition 7 should not be degenerate (i.e. equal to $\perp$), otherwise there is no meaningful seperator. This essentially requires to have realizers that act as substitutions (or “forwarders”). The construction below consists in formally completing a process algebra with such objects.

So the choice of a particular variant of the $\pi$-calculus is essentially arbitrary, we pick this one for the purpose of illustration. The only features we need are the ability to perform renaming and the availability of parallel composition and hiding with usual properties. The point of the construction is to extend the language with name fusions at top-level while preserving this composition structure. Keeping fusions at top-level is the only generic choice that does not impose to reason on the syntax of the calculus we build on, thus allowing for working with fusions in the algebraic structure without imposing constraints on the underlying process language.

### 3.1 Basic processes

The following recalls the standard definitions of the polyadic asynchronous $\pi$-calculus with its operational semantics by reduction [21]. We leave out replication and addition because these will not be used in this paper, but including them is not a problem.

**► Definition 13.** The set $\Pi$ of $\pi$-processes is defined by the following grammar:

$$P, Q ::= 1 \mid (P \mid Q) \mid u(\vec{x}).P \mid \bar{u} \langle \vec{v} \rangle \mid (\nu y)P$$

where $\vec{x}$ is a finite sequence of pairwise distinct names that range over the set $\mathbb{N}$ of natural numbers, $\vec{v}$ is a finite sequence of names, $y$ and $u$ are names. The term $1$ is the unit and the
operators $|$, $u(\vec{x})$, $\bar{u}\langle v\rangle$, $(\nu y)$ are respectively called parallel composition, reception, emission and hiding.

The names in $\vec{x}$ are bound in $u(\vec{x}) \cdot P$, the name $y$ is bound in $(\nu y)P$. The set of free names of a term $P$ is denoted by $FN(P)$. Terms are considered up to renaming of bound names, also called $\alpha$-conversion, written $\equiv_\alpha$.

Structural equivalence is the smallest congruence over terms such that

- $(\Pi, |, \equiv)$ is an commutative monoid, i.e. $1|P \equiv P$, $P|Q \equiv Q|P$ and $(P|Q)|R \equiv P|(Q|R)$,

- $P \equiv (\nu x)P$ and $P | (\nu x)Q \equiv (\nu x)(P|Q)$ whenever $x \notin FN(P)$,

- $(\nu x)(\nu y)P \equiv (\nu y)(\nu x)P$ and we write $(\nu xy)P \triangleq (\nu x)(\nu y)P$.

**Definition 14.** A substitution is a function $\sigma : \mathbb{N} \to \mathbb{N}$. Provided that the names in $\vec{x}$ are pairwise distinct and that $\vec{x}$ and $\vec{v}$ have the same length, $\{\vec{x} := \vec{v}\}$ denotes the substitution which replaces $\vec{x}$ by $\vec{v}$ and leaves all other names unchanged.

Given $X \subseteq \mathbb{N}$ we denote by $\sigma|_X$ the substitution which coincides with $\sigma$ on $X$ and is the identity outside. We write $\sigma\backslash X$ for the substitution $\sigma|_{X\backslash X}$.

We denote by $P^\sigma$ the result of applying $\sigma$ to $P \in \Pi$, defined inductively in the standard way. Given substitutions $\sigma_1, \dots, \sigma_k$ we denote by $P^{\sigma_1 \cdots \sigma_k}$ the term $(\dots(P^{\sigma_1})\dots)^{\sigma_k}$.

**Definition 15.** One-step reduction is the smallest binary relation $\to_1$ over $\Pi$ such that

- $\bar{u} \langle \bar{v} \rangle | u(\vec{x}) \cdot P \to_1 P^{\{\vec{x}:=\vec{v}\}}$,

- $\to_1$ is compatible with $\equiv$, i.e. if $P \equiv P'$, $Q \equiv Q'$ and $P \to_1 Q$ then $P' \to_1 Q'$,

- $\to_1$ is compatible with parallel composition and hiding, i.e. if $x \in \mathbb{N}$ and $P \to_1 P'$, then $P|Q \to_1 P'|Q$ and $(\nu x)P \to_1 (\nu x)P'$.

We do not define a higher-level semantics at this point. The semantics induced by the conjunctive structures defined in the following sections will be a generic form of testing and most of the construction will be parametric in the particular testing protocol.

## 3.2 Processes with fusions

A fusion is, intuitively, a connection between channels. The defining property of a fusion $u \leftrightarrow v$ is that its presence within a process allows actions on channel $u$ to synchronize with actions on channel $v$. Several works have defined extensions of the $\pi$-calculus with this feature [7, 19, 23] and studied its effects on the theory and the expressiveness of the language.

Instead, the construction presented in this section rather aims at extending an arbitrary process calculus with fusions *without* affecting its theory, for our study to be compatible with any particular process language. This is made possible by the fact that we only need fusions at top-level, so that they can live side-by-side with standard processes. Intuitively, a fusion $u \leftrightarrow v$ at top level in a process can be interpreted as the information that $u$ and $v$ will eventually get substituted with the same name.

**Definition 16.** A fusion is an equivalence relation over $\mathbb{N}$. The set of fusions is written $\mathcal{E}$. Given $e \in \mathcal{E}$ we write $x \sim_e y$ instead of $(x, y) \in e$. For $e, f \in \mathcal{E}$ we write $ef$ for the smallest equivalence that contains both $e$ and $f$.

**Remark 17.** The set $\mathcal{E}$ is a complete lattice under inclusion, with the identity $\Delta_{\mathbb{N}} \triangleq \{(x, x) | x \in \mathbb{N}\}$ as minimum and the full relation $\nabla_{\mathbb{N}} \triangleq \mathbb{N} \times \mathbb{N}$ as maximum. The meet of a set $S \subseteq \mathcal{E}$ is the intersection $\bigcap S$ and its join $\bigcup S$ is the transitive closure of the union $\bigcup S$.

**Definition 18.** Given $e \in \mathcal{E}$, $x, y \in \mathbb{N}$, $X \subseteq \mathbb{N}$ and $\sigma : \mathbb{N} \to \mathbb{N}$, define

- the equivalence class of $x$ as $[x]_e \triangleq \{y \in \mathbb{N} | x \sim_e y\}$, extended as $[X]_e \triangleq \bigcup_{x \in X} [x]_e$;
- the domain of $e$ as $|e| \triangleq \{x \in \mathbb{N} \mid [x]_e \neq \{x\}\}$;

- the restriction of $e$ to $X$ as $e \cap X \triangleq (e \cap (X \times X)) \cup \Delta_N$;

- the hiding of $X$ in $e$ as $e \setminus X \triangleq e \cap X^c$;

- the elementary fusion of $x$ and $y$ as $x \leftrightarrow y \triangleq \{(x, y), (y, x)\} \cup \Delta_N$.

An equivalence $e$ can be induced by a function $\sigma$, considering that equivalent elements are the ones with the same image under $\sigma$. Such a function can always be deduced from $e$ by picking a representative in each equivalence class. The following definitions formalize these constructions, exploiting the well-ordering over $\mathbb{N}$ to get canonical representatives.

**Definition 19.** Given a fusion $e \in \mathcal{E}$, $x \in \mathbb{N}$ and a function $\tau : \mathbb{N} \to \mathbb{N}$, we define:

- $x_e^\bullet \triangleq \min[x]_e$ and $x_e^* \triangleq \begin{cases} x & \text{if } [x]_e = \{x\} \\ \min([x]_e \setminus \{x\}) & \text{if } [x]_e \neq \{x\} \end{cases}$

- $\sigma_e^\bullet : x \mapsto x_e^\bullet$ for all $x$, the substitution induced by $e$;

- $\varepsilon_\tau \triangleq \bigvee_{x \in \mathbb{N}} (x \leftrightarrow \tau(x))$, the fusion induced by $\tau$;

- $e^\tau \triangleq \bigvee_{x \sim y} (\tau(x) \leftrightarrow \tau(y))$, the composition of $e$ with $\tau$.

We are now ready to introduce the notion of processes with global fusions, and extend the constructions on processes to this generalization. This is similar to that of unitization in algebras, where a non-unital algebra is extended with a formal extra element and saturated to preserve the structure and endow the extra element with desired properties.

**Definition 20.** The set of processes with global fusions (PGF) is defined as

$$ \bar{\Pi} \triangleq \Pi \times \mathcal{E} = \{(P, e) \mid P \in \Pi, e \in \mathcal{E}\} $$

Over $\bar{\Pi}$, define substitution, free names, $\alpha$-equivalence and structural equivalence $\equiv$ as

$$ (P, e)^\tau \triangleq (P^\tau, e^\tau) $$

$$ (P, e) \equiv_{\alpha} (Q, f) \iff e = f \text{ and } P^{\sigma_e^\bullet} \equiv_{\alpha} Q^{\sigma_f^\bullet} $$

$$ \mathrm{FN}(P, e) \triangleq \mathrm{FN}(P) \cup \{e\} $$

$$ (P, e) \equiv (Q, f) \iff e = f \text{ and } P^{\sigma_e^\bullet} \equiv Q^{\sigma_f^\bullet} $$

When it is not necessary to specify process and fusion, we will use the lowercase letters $p, q, r, s$ to refer to processes with fusions.

Remark that the definitions of $\alpha$-equivalence and structural equivalence allow renaming of free names as long as the equivalence class of each name is unchanged, so that we have for instance $(a(x).P, a \leftrightarrow b) \equiv (b(x).P, a \leftrightarrow b)$. Including $|e|$ in $\mathrm{FN}(P, e)$ ensures that, despite such renaming, $\mathrm{FN}$ is invariant under $\equiv_\alpha$ as expected. Note also that if we identify each term $P$ with the pair $(P, \Delta_N)$, then the operations defined above coincide with those of $\Pi$.

**Definition 21.** One-step reduction in $\bar{\Pi}$ is the relation $\rightarrow_1$ such that $(P, e) \rightarrow_1 (Q, f)$ if and only if $e = f$ and $P^{\sigma_e^\bullet} \rightarrow_1 Q^{\sigma_f^\bullet}$. Multistep reduction $\rightarrow$ is the reflexive and transitive closure of $\rightarrow_1$.

Again, this extends the associated relation from $\Pi$ to $\bar{\Pi}$ and allows more reductions when the fusion relates two names on which compatible actions occur. For instance we have $(u(x).P \mid \bar{v}(y), u \leftrightarrow v) \rightarrow_1 (P\{x := y\}, u \leftrightarrow v)$.

**Definition 22.** For $(P, e), (Q, f) \in \bar{\Pi}$, define $(P, e) \mid (Q, f) \triangleq (P \mid Q, ef)$.

Identifying a pure fusion $e$ with the pair $(\mathbb{1}, e)$, we have $(P, e) \equiv P \mid e$ for every $P$, since $P \mid \mathbb{1} \equiv P$ in $\Pi$. So in this sense $\Pi$ and $\mathcal{E}$ generate $\bar{\Pi}$ under parallel composition. Besides, reduction $\rightarrow_1$ is compatible with $\equiv$ and parallel composition, as in the basic calculus.
We now need to extend name hiding to $\bar{\Pi}$. The result of $(\nu x)(P, e)$ must be $(Q, f)$ where $x \notin \text{FN}(Q, f)$, hence $x \notin \text{FN}(Q) \cup |f|$. Consider a pair $(\nu x)(\bar{x}, x \leftrightarrow y)$: even if $x$ must be bound in $(\nu x)(\bar{x}, x \leftrightarrow y)$, since $x$ is fused with $y$, we have $(\bar{x}, x \leftrightarrow y) \equiv_{\alpha} (\bar{y}, x \leftrightarrow y)$ so the only reasonable definition for $(\nu x)(\bar{x}, x \leftrightarrow y)$ is $(\bar{y}, \Delta_{\mathbb{N}})$, which is structurally equivalent to $((\nu x)\bar{y}, \Delta_{\mathbb{N}})$. On the other hand, if we consider $(\nu x)(\bar{x}, \Delta_{\mathbb{N}})$, we expect to get simply $((\nu x)\bar{x}, \Delta_{\mathbb{N}})$. Definition 19 provides the notation $x_e^*$ to represent this in a general way.

**Definition 23.** For $(P, e) \in \bar{\Pi}$ and $x \in \mathbb{N}$, define $(\nu x)(P, e) \triangleq ((\nu x)P\{x := x_e^*\}, e \setminus \{x\})$.

**Remark 24.** Whenever $x$ is not equivalent to another name, i.e. $[x]_e = \{x\}$, we have $x = x_e^*$ and therefore the binder $\nu x$ on a PGF process only computes as expected on the process side: $(\nu x)(P, e) = ((\nu x)P, e)$. If, instead, $x$ is equivalent to other names, i.e. $[x]_e \neq \{x\}$, then $x \neq x_e^*$ and $\nu x$ will disconnect $x$ from its fusion-side equivalents, while replacing it by an equivalent name on the process side: $((\nu x)P\{x := x_e^*\}, e \setminus \{x\}) \equiv (P\{x := x_e^*\}, e \setminus \{x\})$.

To extend the definition of $\nu$ to finite sets, we first need to ensure that, up to $\alpha$-equivalence, the order of application of $\nu$ is irrelevant.

**Lemma 25.** Consider $(P, e) \in \bar{\Pi}$ and $x, y \in \mathbb{N}$, then $(\nu x)(\nu y)(P, e) \equiv_{\alpha} (\nu y)(\nu x)(P, e)$.

*Proof.* On the one hand

$$((\nu x)(\nu y)(P, e) = (\nu x)((\nu y)P\{y := y_e^*\}, e \setminus \{y\}) = ((\nu xy)P\{y := y_e^*\}\{x := x_{e \setminus \{y\}}^*\}, e \setminus \{x, y\})).$$

On the other hand, it can be shown that the last process is $\alpha$-equivalent to

$$((\nu yx)P\{x:=x_e^*\}\{y:=y_{e \setminus \{x\}}^*\}, e \setminus \{x, y\}) = (\nu y)((\nu x)P\{x:=x_e^*\}, e \setminus \{x\}) = (\nu y)(\nu x)(P, e). \blacksquare$$

**Definition 26.** Given a finite set of names $X = \{x_1, \dots, x_k\}$ with $x_1 < \dots < x_k$, define $(\nu X)(P, e) \triangleq (\nu x_{k_1}) \dots (\nu x_{k_k}) (P, e)$.

Later on, we will need to extend this definition for a possibly infinite set $X$. Even if, for any PGF $p$, there exist only finitely many free names of $p$ in $X$ which we need to hide, for each of them we need to treat them differently depending on whether their equivalence class is included in $X$ or not. The following definitions generalize the unary definition of $\nu$ in that regards.

**Definition 27.** Consider a set $X \subseteq \mathbb{N}$ and a fusion $e \in \mathcal{E}$. Define the substitution

$$\mu_{(X,e)}(x) \triangleq \begin{cases} x_e^\bullet & \text{if } [x]_e \subseteq X \\ \min([x]_e \setminus X) & \text{if } [x]_e \setminus X \neq \emptyset \end{cases}$$

**Definition 28.** Let $(P, e) \in \bar{\Pi}$ and $X \subseteq \mathbb{N}$. Since $\text{FN}(P)$ is finite, there exists classes $[x_1]_e, \dots, [x_{h+k}]_e$ in the quotient $\mathbb{N}/e$ such that for each $i \le h$ we have $[x_i]_e \subseteq X$ and for each $j > h$ we have $[x_j] \setminus X \neq \emptyset$, and moreover $\text{FN}(P) \cap X \subseteq \bigcup_{i=1}^{h+k} [x_i]_e$. Define

$$(\nu X)(P, e) \triangleq ((\nu x_{1,e}^\bullet, \dots, x_{h,e}^\bullet)P^{\mu_{(X,e)}}e \setminus X)$$

Let us denote by $\bar{\nu}$ the binder $(\nu \mathbb{N})$.

Finally, let us state a technical result that emphasizes how we can embed a substitution within the calculus by means of the corresponding fusion.

**Proposition 29.** Consider a substitution $\tau: X \to X^c$ for a set $X \subseteq \mathbb{N}$ and $p, q \in \bar{\Pi}$ such that $\text{FN}(p) \subseteq X$ and $\text{FN}(q) \subseteq X^c$. Then $(\nu X)(p|q|\varepsilon_{\tau}) \equiv_{\alpha} p^{\tau}|q$.
We defer the proof to the extended version of this paper, as it requires a number of technical lemmas whose statements and proofs are of little interest by themselves. The property above will be a crucial ingredient later on to build appropriate realizers. Obtaining it is the point of the PGF construction and we will not rely on more details when studying the conjunctive structure.

## 4 Conjunctive structure of processes

Following the first author's work [2], we shall now see how to define realizability models which interpret MLL formulas as sets of processes. These models actually induce a conjunctive involutive monoidal algebra and as such provides a sound interpretation of MLL. In particular, we would like to emphasize that this illustrates a significant benefit of our approach, which allows us to isolate logical properties that are shared by all concurrent realizability models sharing this algebraic structure, ensuring that these properties are indeed insensitive to implementation details such as the choice of a particular syntax for processes.

### 4.1 Concurrent realizability with PGF

We build upon the main insight of Krivine's realizability [14], by parameterizing the interpretation by a pole, a set of processes somewhat characterizing valid interactions between terms. In this setting, we will consider poles that are simply closed under structural equivalence to characterize the soundness of interaction with respect to the renaming mechanism that is necessary for pure parallel composition, without focusing so far on the reduction of processes. From now on, we denote by $\mathbb{P}$ the set of all sets of processes $\mathbb{P} \triangleq \mathcal{P}(\bar{\Pi})$.

**Definition 30.** A pole is a set of closed processes $⊥ \subseteq \{p \in \bar{\Pi} | \text{FN}(p) = \emptyset\}$ that is closed under $\equiv$, i.e. if $p \equiv q$ and $q \in ⊥$ then $p \in ⊥$.

Given a pole $⊥$, we say that two processes $p, q$ are orthogonal, which we write $p \perp q$, whenever $\bar{\nu}(p|q) \in ⊥$. This naturally induces an orthogonal operator $(\cdot)^\perp : \mathbb{P} \to \mathbb{P}$ on sets of processes by defining $A^\perp \triangleq \{p \in \bar{\Pi} : \forall q \in A, p \perp q\}$. This operator satisfies the usual property of orthogonality.

**Proposition 31.** For all $A, B \in \mathbb{P}$ and for any non-empty $\mathfrak{B} \subseteq \mathbb{P}$ we have:

1. If $A \subseteq B$ then $B^\perp \subseteq A^\perp$

2. $A \subseteq A^{\perp\perp}$ and $A^\perp = A^{\perp\perp}$

3. $(\bigcup_{X \in \mathfrak{B}} X)^\perp = \bigcap_{X \in \mathfrak{B}} X^\perp$ and if $\mathfrak{B} \neq \emptyset$ then $(\bigcap_{X \in \mathfrak{B}} X)^\perp \supseteq (\bigcup_{X \in \mathfrak{B}} X^\perp)$

4. $(\bigcup_{X \in \mathfrak{B}} X^{\perp\perp})^\perp = (\bigcup_{X \in \mathfrak{B}} X)^\perp$

**Proof.** Part 1, 2, 3 directly follow from the definition, in particular $(\bar{\Pi}, \bar{\Pi}, \perp)$ where $\perp = \{(p, q) | p \perp q\}$ is called a polarity in [6] and it defines a Galois connection [3]. For part 4, it suffices to see that $(\bigcup_{X \in \mathfrak{B}} X^{\perp\perp})^\perp = \bigcap_{X \in \mathfrak{B}} X^{\perp\perp} = \bigcap_{X \in \mathfrak{B}} X^\perp = (\bigcup_{X \in \mathfrak{B}} X)^\perp$. ◀

Our realizability interpretation is inspired by the semantics of phases, in particular we interpret formulas in the set of behaviors $\mathfrak{B} \triangleq \{A \in \mathbb{P} : A^{\perp\perp} = A\}$, i.e. the sets that are closed under double orthogonal. This set can be endowed with a structure of complete lattice, as the next proposition shows.

**Proposition 32.** Let us define $\bigvee \mathfrak{B} \triangleq (\bigcup \mathfrak{B})^{\perp\perp}$ for all $\mathfrak{B} \subseteq \mathbb{B}$. Then:

1. $(\mathbb{P}, \cap, \cup, \subseteq)$ is a complete lattice with top element $\bar{\Pi}$ and bottom element $\emptyset$.

2. $(\mathbb{B}, \cap, \vee, \subseteq)$ is a complete lattice with top element $\bar{\Pi}$ and bottom element $\emptyset^{\perp\perp}$.
In order to interpret MLL formulas in this framework, the main idea consists in seeing
the tensor ⊗ as defining the parallel composition of two processes in such a way that they
do not communicate. This is achieved by making extensive use of substitutions to assign
each process a disjoint space of names. Technically, we rely on the fact that $\mathbb{N}$ is in bijection
with the set of even (or odd) natural numbers, somehow reflecting the tree structure of the
formulas into the space of names.

**► Definition 33.** We fix injections $\iota_1, \iota_2 : \mathbb{N} \to \mathbb{N}$ such that $\iota_1(\mathbb{N}) \cap \iota_2(\mathbb{N}) = \emptyset$ and $\iota_1(\mathbb{N}) \cup \iota_2(\mathbb{N}) = \mathbb{N}$. We use the following notations: $\mathbb{N}^i \triangleq \iota_i(\mathbb{N})$, $n.i := \iota_i(n)$, $p^i \triangleq p^{i_i}$ and $e^i \triangleq e^{i_i}$. Given $p \in \bar{\Pi}$ s.t. $\text{FN}(p) \subseteq \mathbb{N}^i$ we denote as $p^{-i}$ the process $p^{i_i}$. Similarly, if $e$ is a fusion s.t. $|e| \subseteq \mathbb{N}^i$, we denote as $e^{-i}$ the fusion $e^{i_i^{-1}}$.

We can now define the semantic counterpart of MLL connectives on processes, which can
then lift to behaviors.

For technical purposes, we also define an operator $\cdot * \cdot$, which in fact coincides with the
usual application, i.e. the left adjoint of the linear implication $\neg$ as Proposition 37 shows.

**► Definition 34.** For all $p = (P, e)$ and $q = (Q, f)$ define the following operations$^2$:

$$ \mathbf{p} \bullet \mathbf{q} \triangleq \mathbf{p}^1 | \mathbf{q}^2 = (\mathbf{P}^1|\mathbf{Q}^2, \mathbf{e}^1\mathbf{f}^2) \quad \mathbf{p} * \mathbf{q} \triangleq ((\nu\mathbb{N}^1)(\mathbf{p}|\mathbf{q}^1))^{-2} = ((\nu\mathbb{N}^1)(\mathbf{P}|\mathbf{Q}^1, \mathbf{e}\mathbf{f}^1))^{-2}. $$

**► Definition 35.** We define the following operations on $\mathbb{P}$:

$$ \begin{array}{l@{\qquad}l} 1 & := \{(1, \Delta_{\mathbb{N}})\}^{\perp\perp} \\ \mathbf{A} \bullet \mathbf{B} & := \{\mathbf{p} \bullet \mathbf{q} \mid \mathbf{p} \in A, \mathbf{q} \in B\} \\ \mathbf{A} | \mathbf{B} & := \{\mathbf{p} \mid \mathbf{q} \mid \mathbf{p} \in A, \mathbf{q} \in B\} \\ \mathbf{A} * \mathbf{B} & := \{\mathbf{p} * \mathbf{q} \mid \mathbf{p} \in A, \mathbf{q} \in B\}^{\perp\perp} \end{array} \quad \left| \begin{array}{l} \mathbf{A} \otimes \mathbf{B} := (\mathbf{A} \bullet \mathbf{B})^{\perp\perp} \\ \mathbf{A} \otimes \mathcal{N} \mathbf{B} := (\mathbf{A}^{\perp} \otimes \mathbf{B}^{\perp})^{\perp} \\ \mathbf{A} \negthinspace \circ \negthinspace \mathbf{B} := (\mathbf{A} \otimes \mathbf{B}^{\perp})^{\perp} \\ \mathbf{A} \parallel \mathbf{B} := (\mathbf{A} | \mathbf{B})^{\perp\perp} \\ \mathbf{A} \upharpoonright \mathbf{X} := \{\mathbf{p} \in A \mid \text{FN}(\mathbf{p}) \subseteq \mathbf{X}\} \end{array} \right. $$

Observe that the definitions of $1, *, \otimes, \mathcal{N}, \neg, \parallel$ define behaviors, and besides, they are
insensitive to double orthogonal:

**► Proposition 36.** For any $A, B \in \mathbb{P}$, it holds that $(A \bullet B)^{\perp} = (A^{\perp\perp} \bullet B^{\perp\perp})^{\perp}$. As a consequence, $A \otimes B = A^{\perp\perp} \otimes B^{\perp\perp}$, $A \otimes \mathcal{N} B = A^{\perp\perp} \otimes \mathcal{N} B^{\perp\perp}$ and $A \negthinspace \circ \negthinspace B = A^{\perp\perp} \negthinspace \circ \negthinspace B^{\perp\perp}$.

**Proof.** The inclusion $(A^{\perp\perp} \bullet B^{\perp\perp})^{\perp} \subseteq (A \bullet B)^{\perp}$ is true by anti monotonicity of the orthogonal operator. For the reverse inclusion, let us consider $r \in (A \bullet B)^{\perp}$ and let us prove that $r \in (A^{\perp\perp} \bullet B^{\perp\perp})^{\perp}$. First, observe that for any processes $p, q$, we have the following equivalences: $\bar{\nu}(p^1 | q^2 | r) \equiv \bar{\nu}((\nu\mathbb{N}^2)(r | q^2))^{-1} | p) \equiv \bar{\nu}((\nu\mathbb{N}^1)(r | p^1))^{-2} | q)$. In particular, for $p \in A$ and $q \in B$, we have $\bar{\nu}((\nu\mathbb{N}^2)(r|q^2))^{-1}|p) \equiv \bar{\nu}(p^1|q^2|r) \in \mathbb{1}$. Then $((\nu\mathbb{N}^2)(r|q^2))^{-1} \in A^{\perp} = A^{\perp\perp\perp}$ and thus $\bar{\nu}(p^1|q^2|r) \in \mathbb{1}$ for all $p \in A^{\perp\perp}$, $q \in B$. Using the same observation, we get that $((\nu\mathbb{N}^1)(r|p^1))^{-2} \in B^{\perp\perp\perp}$ for all $p \in A^{\perp\perp}$. Finally, using this observation again we obtain that $\bar{\nu}(p^1|q^2|r) \in \mathbb{1}$ for all $p \in A^{\perp\perp}$, $q \in B^{\perp\perp}$, which is what we wanted to prove. ◀

**► Proposition 37.** Let us consider $A, B, C \in \mathbb{P}$. Then:

$$ 1. C \subseteq A \negthinspace \circ \negthinspace B \iff C * A \subseteq B^{\perp\perp}. $$

$$ 2. C * A = \bigcap \{B \in \mathbb{B} \mid C \subseteq A \negthinspace \circ \negthinspace B\} = \min \{B \in \mathbb{B} \mid C \subseteq A \negthinspace \circ \negthinspace B\}. \\ \text{(In particular, if } B \in \mathbb{B} \text{ then } C \subseteq A \negthinspace \circ \negthinspace B \iff C * A \subseteq B\}. $$

<footnote n="1">¹ For instance, we can take $\iota_1(n) \triangleq 2n + 1$ and $\iota_2(n) \triangleq 2n$.</footnote>

<footnote n="2">² Observe that $\text{FN}((\nu\mathbb{N}^1)((P, e)|(Q, f)^1) \subseteq \mathbb{N}^2$ and thus we can apply $\iota_2^{-1}$ to this process.</footnote>
**Proof. 1.** Observe that $A \dashv B = (A \bullet B^{\perp})^{\perp}$. Therefore, we have:

$$
\begin{align*}
C \subseteq (A \bullet B^{\perp})^{\perp} &\Leftrightarrow \forall p \in C. \forall q \in A. \forall r \in B^{\perp}. p \perp q \bullet r \\
&\Leftrightarrow \forall p \in C. \forall q \in A. \forall r \in B^{\perp}. \bar{\nu}(p|q^1|r^2) \in \perp \\
&\Leftrightarrow \forall p \in C. \forall q \in A. \forall r \in B^{\perp}. (\nu \mathbb{N}^2)((\nu \mathbb{N}^1)(p|q^1)|r^2) \in \perp \\
&\Leftrightarrow \forall p \in C. \forall q \in A. \forall r \in B^{\perp}. \bar{\nu}((\nu \mathbb{N}^1)(p|q^1)^{-2}|r) \in \perp \\
&\Leftrightarrow \forall p \in C. \forall q \in A. \forall r \in B^{\perp}. p \ast q \perp r \\
&\Leftrightarrow C \ast A \subseteq B^{\perp \perp}
\end{align*}
$$

2. Using Part 1, we get that $C * A \subseteq C * A \iff C \subseteq A \dashv (C * A)$ from which we deduce that $C * A \in \{B | C \subseteq A \dashv B\}$. On the other hand, if $C \subseteq A \dashv B$, then $C * A \subseteq B$. ◀

To complete the definition of the concurrent realizability interpretation of MLL using processes, it only remains to define the realizability relation.

**Definition 38.** We say that a PGF $p$ realizes a behavior $A$, which we write $p \Vdash A$, if $p \in A$.

A detailed study of this interpretation and of the computational content of realizers, which mostly ensure adequate communication between adequate channels using an appropriate fusion, is out of the scope of this paper. We simply illustrate how the identity can be realized.

**Proposition 39.** For any $A \in \mathbb{P}$, we have that $I \triangleq \bigvee_{n \in \mathbb{N}} (n.1 \leftrightarrow n.2) \Vdash A \dashv A$.

**Proof.** We have $A \dashv A = (A \bullet A^{\perp})^{\perp}$ (using Proposition 37). Let us consider $p \in A$ and $q \in A^{\perp}$, it suffices to prove that $I \perp p^1 | q^2$. Using Proposition 29, we get that $\bar{\nu}(p^1 | q^2 | I) \equiv_{\alpha} (\nu_2)(\nu_1)(p^1 | q^2 | I) \equiv_{\alpha} (\bar{\nu})(p | q)$ and we conclude by observing that $(\bar{\nu})(p | q) \in \perp$. ◀

## 4.2 The induced conjunctive involutive monoidal algebra

Most importantly, we can prove that this construction actually defines a conjunctive involutive monoidal algebra. In particular, this entails (via Theorem 12) that it defines a valid interpretation of MLL. The proof is in two parts, we prove that the interpretation induces a CIS, then we show that the set of realized behaviors defines a valid separator.

**Proposition 40.** The tuple $(\mathbb{B}, \subseteq, \otimes, (\cdot)^{\perp})$, where $(\mathbb{B}, \subseteq)$ is the lattice defined in Proposition 32, is a conjunctive involutive structure.

**Proof.** We have to check that the axioms of Definition 1 are satisfied. The variance properties and De Morgan law directly follow from the definition of $\mathbb{B}$, $\otimes$ and from Proposition 31. We prove the first distributivity law, the other one being similar. For any $\mathfrak{B} \subseteq \mathbb{B}$, we have:

$$
\begin{align*}
A \otimes \bigvee_{B \in \mathfrak{B}} B &= \mathop{\bigwedge}_{\text{def } \vee} A \otimes (\bigcup_{B \in \mathfrak{B}} B)^{\perp \perp} = \mathop{\bigwedge}_{\text{Prop } 36} A \otimes \bigcup_{B \in \mathfrak{B}} B = \mathop{\bigwedge}_{\text{def } \otimes} (A \bullet \bigcup_{B \in \mathfrak{B}} B)^{\perp \perp} \\
&= (\bigcup_{B \in \mathfrak{B}} (A \bullet B))^{\perp \perp} = \mathop{\bigwedge}_{\text{Prop } 31.4} (\bigcup_{B \in \mathfrak{B}} (A \bullet B)^{\perp \perp})^{\perp \perp} = \mathop{\bigwedge}_{\text{def } \otimes} (\bigcup_{B \in \mathfrak{B}} (A \otimes B))^{\perp \perp} = \bigvee_{B \in \mathfrak{B}} (A \otimes B) \quad \text{◀}
\end{align*}
$$

**Proposition 41.** The following behaviors are realized by pure fusions:

1. $\bigcap_{A \in \mathbb{B}} A \dashv A$.

2. $\bigcap_{A,B \in \mathbb{B}} (A \otimes B) \dashv (B \otimes A)$.

3. $\bigcap_{A,B,C \in \mathbb{B}} (A \dashv B) \dashv (B \dashv C) \dashv A \dashv C$.

4. $\bigcap_{A,B,C \in \mathbb{B}} ((A \otimes B) \otimes C) \dashv (A \otimes (B \otimes C))$.

5. $\bigcap_{A \in \mathbb{B}} A \dashv (1 \otimes A)$.

6. $\bigcap_{A \in \mathbb{B}} (1 \otimes A) \dashv A$.

7. $\bigcap_{A,B \in \mathbb{B}} (A \dashv B) \dashv (B^{\perp} \dashv A^{\perp})$.
<figure><img src="image_3.png" /><figcaption>Figure 2 Axioms for the compositional structure associated to F</figcaption></figure>

**Proof.** The first statement is Proposition 39, and the other statements follow similar ideas. We give here a realizer for the second statement as an example.

By Definition 35, we have $(A \otimes B) \stackrel{\cdot}{\to} (B \otimes A) = ((A \bullet B) \bullet (B \bullet A)^\perp)^\perp$. Consider $p \in (B \bullet A)^\perp$, $q \in A$ and $r \in B$, in particular, they satisfy $\bar{\nu}(r^1 | q^2 | p) \in \perp$. By definition $q^{1,1} | r^{2,1} | p^2 \in (A \otimes B) \stackrel{\cdot}{\to} (B \otimes A)$. To get a realizer, we define the substitution $\tau: \mathbb{N}^1 \to \mathbb{N}^2$ s.t. $\tau(n.1.1) := n.2.2$ and $\tau(n.2.1) := n.1.2$. It is now enough to prove that $\varepsilon_\tau \perp q^{1,1} | r^{2,1} | p^2$, i.e.: $\bar{\nu}(q^{1,1} | r^{2,1} | p^2 | \varepsilon_\tau) \in \perp$. Moreover $\bar{\nu}(q^{1,1} | r^{2,1} | p^2 | \varepsilon_\tau) = (\nu\mathbb{N}^2)(\nu\mathbb{N}^1)(q^{1,1} | r^{2,1} | p^2 | \varepsilon_\tau) = (\nu\mathbb{N}^2)(q^{2,2} | r^{1,2} | p^2) = \bar{\nu}(r^1 | q^2 | p) \in \perp$, which ends the proof.

<figure><img src="image_4.png" /></figure>

**Proposition 42.** *The set of non-empty behaviors $S_B \triangleq \mathbb{B}\setminus\emptyset$ defines a separator for the conjunctive structure $(\mathbb{B}, \subseteq, \otimes, (\cdot)^\perp)$.*

**Proof.** $S_B$ is upwards closed by construction, and the proof that all the combinators are inhabited by fusions is given in Proposition 41. To prove that it is compatible with the modus ponens, let $a, b \in \mathbb{B}$ be behaviors and $p, q$ be processes such that $p \in a \stackrel{\cdot}{\to} b$ and $q \in a$. By Proposition 37, we get $(a \stackrel{\cdot}{\to} b) * a \subseteq b$, and thus in particular $p * q \in b$, i.e. $b \in S_B$. ◀

# 5 Conjunctive algebras for concurrency

## 5.1 Parallel composition

So far, we identified the conjunctive part of the realizability model, that is, processes handling disjoint namespaces. We shall now investigate the necessary structure to algebrize parallelism.

**Definition 43.** Let us consider a CS $(\mathbb{C}, \otimes, (\cdot)^\perp, \prec)$. A composition on $\mathbb{C}$ is an increasing and $\Upsilon$-continuous function $F: \mathbb{C} \times \mathbb{C} \to \mathbb{C}$.

Given a composition $F$ on $\mathbb{C}$, define the induced compositional structure associated to $F$ as the quotient $\mathbb{C} / \equiv_F$ where the equivalence relation $\equiv_F$ is the minimum equivalence relation that satisfies the rules of Figure 2.

Observe that the first four rules express that $(\mathbb{C}, F, 1, \equiv_F)$ is an commutative monoid while the last ones express that the structure of the CS $\mathbb{C}$ is lifted to the quotient $\mathbb{C} / \equiv_F$, thus inducing respectively the operations $\otimes_F, (\cdot)^\perp_F$ and the preorder $\prec_F$. It is a direct verification that the structure $(\mathbb{C} / \equiv_F, \otimes_F, (\cdot)^\perp_F, \prec_F)$ is also a CS. Provided there is no ambiguity, we will avoid the subscripts $F$ on the induced operations. The structure $(\mathbb{C} / \equiv_F, \otimes, (\cdot)^\perp, F, \prec)$ induced by $F$ on $\mathbb{C}$ is denoted as $C_F$.

**Definition 44.** Let us consider $(\mathbb{C}, \otimes, (\cdot)^\perp, 1, F, \prec)$ a CS with composition $F$. We define $\triangleright_F: \mathbb{C} \times \mathbb{C} \to \mathbb{C}$ by means of $b \triangleright_F c \triangleq \Upsilon\{x \in \mathbb{C} | x F b \prec c\}$

It is straightforward to check that $\triangleright_F$ defines a right adjoint to $F$.

**Proposition 45.** Let us consider $(\mathbb{C}, \otimes, (\cdot)^\perp, 1, F, \prec)$ a CS with composition $F$. Then $a F b \prec c \iff a \prec b \triangleright_F c$ for all $a, b, c \in \mathbb{C}$.
**Proof.** For the direct implication, $aFb \preceq c$ implies that $a \in \{x \in \mathbb{C} \mid xFb \preceq c\}$ hence $a \preceq b \triangleright_F c$. For the reverse implication, since $F$ is monotone, we have

$$aFb \preceq (b \triangleright_F c)Fb = (\bigvee \{x \in \mathbb{C} \mid xFa \preceq c\}) \mid b \preceq \bigvee \{xFb \mid x \in \mathbb{C}, xFb \preceq c\} \preceq c. \quad \triangleleft$$

**► Proposition 46.** Consider the CS $(\mathbb{B}, \otimes, (\cdot)^\perp, 1, \subseteq)$ of behaviors over $\bar{\Pi}$.

1. The operation $\parallel$ (from Definition 35) is a composition over $\mathbb{B}$, the equivalence $\equiv_\parallel$ is equality and its right adjoint is $B \triangleright_\parallel C := (B \parallel C^\perp)^\perp$.

2. The operation $\otimes$ (from Definition 35) is a composition over $\mathbb{B}$ and its right adjoint is $B \triangleright_\otimes C := (((B^2 \parallel C^\perp)^\perp)_{|\mathbb{N}^1})^{-1}$.

**Proof.** 1. Since $(\bar{\Pi}, |, 1)$ is a commutative monoid, then $(\mathbb{B}, \parallel, 1)$ is also a commutative monoid with unit $1 := \{1\}^{\perp\perp}$. The function $\parallel$ is increasing by definition. For the continuity, we can check that $(\bigvee \mathbb{B}) |A \subseteq \bigvee \{B \parallel A \mid B \in \mathbb{B}\}$ for all $\mathbb{B} \subseteq \mathbb{B}$ and $A \in \mathbb{B}$, and we prove the continuity in the right argument similarly. Besides, $A \parallel B \subseteq C$ is equivalent to $C^\perp \subseteq (A \parallel B)^\perp$, which is equivalent to $\forall p \in A, q \in B, r \in C^\perp, \bar{\nu}(p \mid q \mid r) \in \perp$. The last condition is equivalent to $A \subseteq (B \parallel C^\perp)^\perp$, which proves that $B \triangleright_\parallel C := (B \parallel C^\perp)^\perp$ is the right adjoint of $\parallel$.

2. We have $(\bigvee \mathbb{B}) \otimes A = \bigvee \{B \otimes A \mid B \in \mathbb{B}\}$ and $A \otimes (\bigvee \mathbb{B}) = \bigvee \{A \otimes B \mid B \in \mathbb{B}\}$ from Proposition 40, and by construction $\otimes$ is increasing. Moreover, $A \otimes B \subseteq C$ is equivalent to $C^\perp \subseteq (A \otimes B)^\perp$, which is equivalent to $\forall p \in A, q \in B, r \in C^\perp, \bar{\nu}(p^1 \mid q^2 \mid r) \in \perp$. The last condition is equivalent to $A^1 \subseteq (((B^2 \parallel C^\perp)^\perp)_{|\mathbb{N}^1})^{-1}$ hence $A \subseteq (((B^2 \parallel C^\perp)^\perp)_{|\mathbb{N}^1})^{-1}$, which proves that $B \triangleright_\otimes C := (((B^2 \parallel C^\perp)^\perp)_{|\mathbb{N}^1})^{-1}$ is the right adjoint of $\otimes$. $\triangleleft$

## 5.2 Embedding the $\pi$-calculus through Honda-Yoshida combinators

Following previous works on algebraic structures for realizability models based on sequential calculi [15, 16], we face two options to show that the $\pi$-calculus can be faithfully embedded with conjunctive involutive structure with compositions. Either we find a way to soundly embed the different constructs $u(\vec{x}).P, \bar{u}\langle\bar{v}\rangle, |(vy)P$, or we can define a set of combinators that is complete for this calculus (as are $S$ and $K$ for the $\lambda$-calculus). We opt for the second approach, building on Honda & Yoshida combinators for the $\pi$-calculus [10].

**Definition 47.** A Honda-Yoshida structure (HYS) is a CIS $(\mathbb{C}, \llcorner, \otimes, |, (\cdot)^\perp, 1)$ with composition $|$ together with a function $M: \mathbb{N} \times \mathbb{N} \to \mathbb{C}$. Given such a structure, we define the Honda-Yoshida combinators of $\mathbb{C}$ by means of:

$$ \begin{array}{c|c} K(a) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright 1) & \mathrm{Br}(a, b) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright F(b, x)) \\ F(a, b) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright M(b, x)) & D(a, b, c) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright M(b, x)|M(c, x)) \\ B(a, b) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright F(x, b)) & S(a, b, c) \triangleq \lambda_{x \in \mathbb{N}} (M(a, x) \triangleright F(b, c)) \end{array} $$

These definitions are sound with respect to the expected reductions of these combinators, in the sense that each reduction rule $p \to q$ (in [10]) directly yields an inequality $p \preceq q$.

**Proposition 48.** Given a HYS $(\mathbb{C}, \llcorner, \otimes, |, (\cdot)^\perp, 1, M)$ we have:

$$ \begin{array}{c|c} K(a)|M(a, x) & \preceq 1 \\ F(a, b)|M(a, x) & \preceq M(b, x) \\ D(a, b, c)|M(a, x) & \preceq M(b, x)|M(c, x) \end{array} \quad \begin{array}{c|c} B(a, b)|M(a, x) & \preceq F(x, b) \\ Br(a, b)|M(a, x) & \preceq F(b, x) \\ S(a, b, c)|M(a, x) & \preceq F(b, c) \end{array} $$

**Proof.** Straightforward from the definitions. $\triangleleft$
**► Definition 49.** A Honda-Yoshida algebra (HYA) is a HYS $(\mathbb{C}, \prec, \otimes, |, (\cdot)^\perp, 1, M)$ together with a monoidal separator $S \subseteq \mathbb{C}$ s.t. all Honda-Yoshida combinators belong to $S$.

So far we have not needed to introduce a notion of reduction because the constructors of Linear Logic in our types reflect the properties of connections and handling of names. However, to obtain a model of behaviors $\mathcal{B}$ where the Honda-Yoshida combinators are inhabited, we ask the poles to be closed by anti-reduction. This choice follows the first author's design when defining the regular poles in [2].

**► Definition 50.** Let us consider a pole $\perp \subseteq \bar{\Pi}$. We say that $\perp$ is regular iff for all $(P, e), (Q, f)$ (PGF)-processes and names $u, \vec{x}$, $\{(P | Q, ef)\}^\perp \subseteq \{(\bar{u} \langle \vec{x} \rangle .P | v(\vec{x}).Q, ef)\}^\perp$ whenever $u \sim v_{ef}$.

Following [11], the combinators of Honda & Yoshida can be encoded into PGF using the usual $\pi$-calculus (pure) processes:

<figure><img src="image_5.png" /></figure>

**► Proposition 51.** A CIMA of behaviours $(\mathbb{B}, \prec, \otimes, \|, (\cdot)^\perp, 1, S_{\mathbb{B}})$ induced by a regular pole $\perp$ is a HYA with the definition $M(a, b) \triangleq \{(\bar{a} \langle b \rangle .1, \Delta_N)\}^{\perp\perp}$.

**Proof.** It suffices to prove that all the combinators of Definition 47 are inhabited. For that we consider the standard encoding of the negative combinators into the $\pi$-calculus (which is embedded into PGF). Then, using the regularity of the pole, we prove that the encoding belongs to the corresponding combinator defined in $\mathbb{C}$. Since $M(a, b)$ is not empty, we have $M(a, b) \in S_{\mathbb{B}}$ by definition of $S_{\mathbb{B}}$. The other combinators $K(a), F(a, b), Bl(a, b), Br(a, b), D(a, b, c)$ and $S(a, b, c)$ are given by Definition 49 and they are inhabited by their respective encoding on (PGF).

Let us illustrate the technique by proving the case of $K_a$. Observe that since the pole is regular, we have $\{1\}^{\perp} \subseteq \{k(a)|m(a, x)\}^{\perp} = (\{k(a)\}^{\perp\perp} | M(a, x))^{\perp} = (\{k(a)\}^{\perp\perp} || M(a, x))^{\perp}$. Applying the orthogonal map we get: $\{k(a)\}^{\perp\perp} || M(a, x) \subseteq \{1\}^{\perp\perp} \stackrel{\text{def}}{=} 1$. By Proposition 45 we deduce that $\{k(a)\}^{\perp\perp} \subseteq M(a, x) \triangleright 1$ for all names $a, b, x$. Taking the meet over $x$, we obtain $k(a) \in \{k(a)\}^{\perp\perp} \subseteq \bigwedge_{x \in \mathbb{N}} (M(a, x) \triangleright 1) = K(a)$ and thus $k(a) \in K(a)$. ◀

# 6 Parallel composition cannot be derived

We shall now see that the extra structure presented in the previous section to encompass parallelism within conjunctive involutive monoidal algebra is actually necessary, in the sense that parallelism cannot be derived from the ground structure of a conjunctive involutive monoidal algebra. Indeed, we observed that in the CIMA induced by PGF behaviors, the parallel composition is preexistent since there exists not only an external$^3$ continuous function,

<footnote>$^3$ That is a meta-theoretic function, as opposed to an *internal* term definable in the language of the algebraic structure at play.</footnote>
<figure><img src="image_6.png" /><figcaption>■ **Figure 3** System L, typing rules</figcaption></figure>

but even a term $\Phi$ s.t. $\Phi * t * u = t \| u$ for all $t, u$. This explains why, in this case, there is no need for a quotient (see Proposition 46.1).

In the general case, when there is no such preexisting term, it is always possible to follow Definition 43 to recover the expected structure through a quotient. We will now highlight that this is, in general, necessary, in the sense that parallel composition can not always be defined with only terms and application in an arbitrary CIMA. We do so by providing a concrete example of a conjunctive involutive monoidal algebra in which we prove that there is no term satisfying the axioms of parallel composition.

We build on a realizability interpretation based on a fragment of Munch-Maccagnoni's system L [17], a polarised sequent calculus tailored to give a term language to Girard's classical logic LC. To draw the comparison with other sequent calculi such as Curien-Herbelin's $\tilde{\lambda}\mu\tilde{\mu}$-calculus [4], the main difference lies in the use of polarisation, which makes lazy and strict qualify logical connectives rather than evaluation strategies: instead of having to enforce globally a strategy to avoid critical pairs, lazy and strict evaluations coexist and are dictated locally by the polarities of the corresponding connectives. For a more detailed introduction on the rationale of L, we refer the interested reader to [18].

We work here with a fragment of L, keeping only the connectives necessary to induce a CIMA. As explained above, formulas are divided into positive and negative ones:

<figure><img src="image_7.png" /></figure>

To each positive formula $P$ is associated a dual negative formula $P^{\perp}$ (and vice-versa), defined by induction on the syntax of formulas. As is usual in linear logic, the map $(\cdot)^{\perp}$ defines an involutive function on formulas:

<figure><img src="image_8.png" /></figure>

Similarly, the syntax of terms and values reflect these distinction between negative and positive connectives. To ease the connection with [17], we stick to the same presentation:

<figure><img src="image_9.png" /></figure>

In the sequel, we write $\mathcal{T}_+$ (resp. $\mathcal{T}_-, \mathcal{C}, \mathcal{V}$) for the set of positive terms (resp. negative terms, commands, values), and denote by $\mathcal{T}_+^0$, etc... the corresponding set of closed terms. As in [17], we use monolateral sequents, following Girard's tradition to have all the formulas on the
right. To that end, we need to quotient the syntax with a new α-equivalence $\langle t \parallel u \rangle \equiv \langle u \parallel t \rangle$, which will simplify overall the presentation. The type system, which distinguishes between sequents of the shape $\vdash t : A \mid \Gamma$ to type terms (where A is the formula in the stoup) and sequents of the shape c : ($\vdash \Gamma$) to type commands, is given in Figure 3. The reader may observe that the rule for the universal quantifier has to be restricted to values in order to avoid the usual inconsistency of polymorphism in presence of side-effects [17].

The operational semantics is defined as a weak-head reduction relation on commands, by means of the following reduction rules:

$$ \begin{array}{l@{\quad}l@{\quad}l} \langle \mu\alpha.c \parallel V \rangle & \rightarrow_{\mu} & c[V/x] \\ \langle V \parallel \mu x.c \rangle & \rightarrow_{\mu} & c[V/x] \end{array} \quad \left| \begin{array}{l} \langle (V, V') \parallel \mu(\kappa, \kappa').c \rangle \rightarrow_{\beta} c[V/\kappa, V'/\kappa'] \\ \langle (t, t') \parallel u \rangle \rightarrow_{\epsilon} \langle t \parallel \mu\kappa.\langle t' \parallel \mu\kappa'.\langle (\kappa, \kappa') \parallel u \rangle \rangle \end{array} \right\} $$

The different binders only reduce in front of values, while the $\rightarrow_{\epsilon}$ rules specify how constructors should be expanded when they are built on top of a term instead of a value. In particular, it is worth noting that the reduction $\rightarrow_{\epsilon} \rightarrow_{\mu} \cup \rightarrow_{\beta} \cup \rightarrow_{\epsilon}$ has no critical pair, which entails the Church-Rosser property when considering its extension to subcommands.

Following [17], we can now define a realizability interpretation à la Krivine relying on this calculus. As is usual in Krivine realizability, we say that a pole is any subset of $C^0$ that is closed by anti-reduction. This induces an orthogonality relation on terms, which we extend to any sets $T \in \mathcal{P}(\mathcal{T}_+^0)$ or $U \in \mathcal{P}(\mathcal{T}_-^0)$ by defining:

$$ T^{\perp} \triangleq \{t_{-} \in \mathcal{T}_{-}^{0} : \forall t_{+} \in T, \langle t_{+} \parallel t_{-} \rangle \in \perp\} \mid U^{\perp} \triangleq \{t_{+} \in \mathcal{T}_{+}^{0} : \forall t_{-} \in U, \langle t_{+} \parallel t_{-} \rangle \in \perp\} $$

In this context, we call *behavior* any subset $T$ of $\mathcal{T}_+^0$ or $\mathcal{T}_-^0$ such that $T = T^{\perp\perp}$ and we denote by $\mathbf{H}$ the set of all behaviors. Observe that $(\cdot)^{\perp}$ defines an involutive map on $\mathbf{H}$.

We are now ready to define a realizability interpretation that will associate to any formula a behavior. More precisely, we extend the language of formulas to consider formulas with (positive) parameters $R$ in the set $\Pi \triangleq \mathcal{P}(\mathcal{T}_+^0 \cap \mathcal{V})$, and to any such positive formula $P$ we associate a behavior $|P| \in \mathcal{P}(\mathcal{T}_+^0)$ while to any negative formula $N$ we associate a behavior $|N| \in \mathcal{P}(\mathcal{T}_-^0)$. The interpretation $|\cdot|$ is defined by induction on formulas:

$$ \begin{array}{l@{\quad}l@{\quad}l} |R| & \triangleq & R^{\perp\perp} \\ |A \otimes B| & \triangleq & (|A| \otimes |B|)^{\perp\perp} \\ |\exists X.A| & \triangleq & (\bigcup_{R \in \mathcal{V}} |A[R/X]|_{\mathcal{V}})^{\perp\perp} \end{array} \quad \left| \begin{array}{l} |R^{\perp}| \triangleq R^{\perp} \\ |A \nparallel B| \triangleq (|A^{\perp}| \otimes |B^{\perp}|)^{\perp} \\ |\forall X.A| \triangleq (\bigcap_{R \in \mathcal{V}} |A[R/X]|_{\mathcal{V}})^{\perp\perp} \end{array} \right. $$

where $|A|_{\mathcal{V}} \triangleq |A| \cap \mathcal{V}$ and $T \otimes U \triangleq \{(t, u) : t \in T \wedge u \in U\}$. Observe that by construction, for any closed formula $A$, it holds that $|A^{\perp}| = |A|^{\perp}$.

**Definition 52.** For any term $t$, one says that $t$ realizes a formula $A$ whenever $t \in |A|$, which we denote by $t \Vdash A$. Similarly, we write $\sigma \Vdash \Gamma$ to denote that a substitution $\sigma$ realizes a context $\Gamma \equiv x_1 : A_1, \dots, x_n : A_n$ when for any $1 \le i \le n$, $\sigma(x_i) \Vdash A_i$.

We say that $t$ is a universal realizer of $A$ and we write $t \Vdash A$ when a term $t$ realizes $A$ for any possible choice of pole.

We will not develop any further the properties of this construction, but we shall at least emphasize that the typing rules defined in Figure 3 are adequate with respect to this interpretation, which is proven as usual by induction over typing derivations [17].

**Proposition 53 (Adequacy).** Let $\Gamma$ be a typing context, $\perp$ a pole and $\sigma$ be a substitution such that $\sigma \Vdash \Gamma$, then for any term $t$ and formula $A$, if $\vdash t : A \mid \Gamma$, then $t^{\sigma} \Vdash A$.
Even though the fragment of L we have selected does not account for linearity, the last proposition shows that the realizability interpretation still defines a model for MLL. In particular, as was observed in [16], algebraically it induces a conjunctive structure. This observation can be adapted to our framework, to show that the realizability interpretation defined above actually induces a conjunctive involutive monoidal algebra.

**Proposition 54.** The tuple $(\mathbf{H}, \subseteq, \otimes, (\cdot)^{\perp}, \mathbf{1}, \mathcal{S})$, where $\mathbf{1} \triangleq \mathcal{T}_{+}^{0}$ and $\mathcal{S} = \mathbf{H} \setminus \emptyset$, is a CIMA.

**Proof.** The proof is analogous to the proof in [16], up to the observation that $(\cdot)^{\perp}$ is involutive on $\mathbf{H}$ (by definition of $\mathbf{H}$). We first show that $(\mathbf{H}, \subseteq, \otimes, (\cdot)^{\perp})$ is a conjunctive involutive structure. Indeed, the set of behaviors, ordered by inclusion, defines a complete lattice whose join is given by the union, and the map $\cdot \otimes \cdot$ is clearly covariant in its two arguments. while it is clear that $(\cdot)^{\perp}$ is anti-monotonic. Regarding De Morgan law, we have for any set $\mathcal{U} \subseteq \mathcal{T}^{0}$:

$$ 
\begin{aligned}
(\bigcup_{T \in \mathcal{U}} T)^{\perp} &= \left( \bigcup_{T_+ \in \mathcal{U} \cap \mathcal{T}_+} T_+ \cup \bigcup_{T_- \in \mathcal{U} \cap \mathcal{T}_-} T_- \right)^{\perp} = \left( \bigcup_{T_+ \in \mathcal{U} \cap \mathcal{T}_+} T_+ \right)^{\perp} \cap \left( \bigcup_{T_- \in \mathcal{U} \cap \mathcal{T}_-} T_- \right)^{\perp} \\
&= \bigcap_{T_+ \in \mathcal{U} \cap \mathcal{T}_+} T_+^{\perp} \cap \bigcap_{T_- \in \mathcal{U} \cap \mathcal{T}_-} T_-^{\perp} = \bigcap_{T \in \mathcal{U}} T^{\perp}
\end{aligned}
$$

Then we prove that, when considering the unit $\mathbf{1} \triangleq \mathcal{T}_{+}^{0}$ (which is indeed a behavior), the set of non-empty behaviors $\mathcal{S} = \mathbf{H} \setminus \emptyset$ defines a valid separator. This mostly amounts to finding a realizer for each of the different axioms, since $\mathcal{S}$ is clearly upwards-closed. and is compatible with modus ponens. Indeed, if $A, B \in \mathbf{H}$ are such that $A \dashv B \in \mathcal{S}$ and $A \in \mathcal{S}$, by definition of $\mathcal{S}$ it means that there exists two terms $t$ and $u$ such that $t \in A \dashv B$ and $u \in A$. Then $tu = \mu\kappa.\langle t \parallel (u, \alpha) \rangle \vdash B$, using the typing rule for application above and Proposition 53. To find realizers for the axiom, it suffices to find a term of the expected type, and to use adequacy (cf. Proposition 53). For instance, we can pick:

- $\mu(x, \alpha).\langle x \parallel \mu(\kappa_1, \kappa_2).\langle (\kappa_2, \kappa_1) \parallel \alpha \rangle \rangle \vdash (A \otimes B) \dashv (B \otimes A)$

- $\lambda\alpha.\mu(x, \beta).\langle x \parallel \mu(\kappa, \kappa').\langle (\alpha \kappa, \kappa') \parallel \beta \rangle \rangle \vdash (A \dashv B) \dashv (A \otimes C) \dashv (B \otimes C)$

- $\mu(x, \alpha).\langle x \parallel \mu(y, \kappa_3).\langle y \parallel \mu(\kappa_1, \kappa_2).\langle (\kappa_1, (\kappa_2, \kappa_3)) \parallel \alpha \rangle \rangle \rangle \vdash ((A \otimes B) \otimes C) \dashv (A \otimes (B \otimes C))$

- For any $t_+ \in \mathcal{T}_+^0$, $\lambda\kappa.(t_+, \kappa) \vdash A \dashv 1 \otimes A$

- $\mu(x, \kappa).\langle x \parallel \mu(\_, \kappa').\langle \kappa' \parallel \kappa \rangle \rangle \vdash 1 \otimes A \dashv A$

- $\mu(x, \alpha).\langle x \parallel \mu(\kappa, \kappa').\langle (\kappa, \kappa') \parallel \alpha \rangle \rangle \vdash (A \dashv B) \dashv (B^{\perp} \dashv A^{\perp})$

◀

We have shown so far that the realizability interpretation based on L defines a conjunctive involutive monoidal algebra as expected. Besides, we can show that this particular kind of CIMA does not admit parallelism, thus justifying the necessity of the extra requirements formulated in Definition 43. Indeed, to obtain a compositional structure in such a model without adding some extra structure would mean the desired composition F could be defined by means of a term $t$ (i.e. $F(u, v) \triangleq tuv$) such that the expected axioms are satisfied.

We prove that this is not possible, in that the first two axioms $(F(a, 1) \equiv a$ and $F(1, a) \equiv a)$ cannot be satisfied together. The proof, which is folklore in Krivine realizability, mostly consists in proving that a term that realizes both of these axioms should essentially behave like a parallel $\otimes$ operator, which does not exist in L. This should not come as a surprise, since, to put it differently, it essentially means that to get the algebraic structure corresponding to parallelism, we actually need to have parallel computations in our calculus.

**Proposition 55.** There is no $t \in \mathcal{T}_+^0$ s.t. $t \vdash \forall X.(X \dashv 1 \dashv X)$ and $t \vdash \forall X.(1 \dashv X \dashv X)$.

**Proof.** To simplify the proof, let us assume that the calculus is extended with two inert (positive) constants $\kappa_1, \kappa_2$ and a negative one $\alpha$ (alternatively, one could consider any terms $u_1, u_2 \in \mathcal{T}_+^0$ and $v \in \mathcal{T}_-^0$ such that the commands $\langle u_1 \parallel v \rangle$ and $\langle u_2 \parallel v \rangle$ are blocked).
We reason by contradiction by assuming that such a term $t$ exists. Let $u \in \mathcal{T}_{-}^0$ be any term, and $\mathcal{X} \triangleq \{u\} \in \Pi$. Consider the pole $\bot_1 = \{c : c \rightarrow \langle \kappa_1 \parallel u \rangle\}$. By construction, we have that $\kappa_1 \in |\mathcal{X}|$, $\kappa_2 \in |\mathbb{1}|$ and $\alpha \in |\mathcal{X}|^{\perp}$. Since by assumption $t \Vdash \mathcal{X} \dashrightarrow \mathbb{1} \dashrightarrow \mathcal{X}$, we get $\langle t \parallel (\kappa_1, (\kappa_2, \alpha)) \rangle \in \bot_1$, i.e. $\langle t \parallel (\kappa_1, (\kappa_2, \alpha)) \rangle \rightarrow \langle \kappa_1 \parallel \alpha \rangle$.

By taking $\bot_2 = \{c : c \rightarrow \langle \kappa_2 \parallel \alpha \rangle\}$, we prove similarly that $\langle t \parallel (\kappa_1, (\kappa_2, \alpha)) \rangle \rightarrow \langle \kappa_2 \parallel \alpha \rangle$. Since both commands $\langle \kappa_1 \parallel \alpha \rangle$ and $\langle \kappa_2 \parallel \alpha \rangle$ are blocked and the calculus is deterministic, we indeed found a contradiction. ◀

# 7 Conclusion and future work

## 7.1 Exponentials

In addition to studying in more depth the properties of the various structures introduced in this paper, a natural prolongation of this work would be to investigate the possibility to build on conjunctive involutive monoidal algebra to account for more expressive logical systems, in particular MALL with exponentials. This would provide us with a complete algebraic presentation of the first author's work [2]. To that end, we could rely on Honda & Yoshida combinatorial approach to replication [11]. Another path to follow in that direction would consist in exploring the connections with the Geometry of Interaction as it is presented in Duchesne's work [5], where MLL is interpreted using partial permutations and the tensor corresponds to an appropriate disjoint union. This bears similarities with our interpretation using injections $\iota_i : \mathbb{N} \rightarrow \mathbb{N}$ for the tensor to ensure disjoint namespaces.

## 7.2 Concurrency

A central element in our study of parallelism and its axiomatization is the role of non-determinism. Indeed, the presence in a process of several actions that may synchronize together in different ways is both a source of expressiveness, as witnessed by the famous "parallel or" which relies on this feature, but also an obstacle for logical study. In some sense, our search for an axiomatization of parallel composition aims at identifying the part of the logical structure that is responsible for such phenomena. An analogy can be made with the computational interpretation of classical logic: it is well known that the classical sequent calculus LK is not confluent, to the point that any direct denotational semantics of proofs is degenerated, but interesting semantics can be obtained by means of translations into better behaved logics. Such translations are effective because they impose constraints on proof reduction, like call-by-name or call-by-value policies in languages with control. Our system with parallelism could be envisaged as a linear analogue of full classical logic with no a priori constraints on strategies.

<figure><img src="image_10.png" /></figure>

In this line of thought, the conjunctive structures we are after will provide the fundamental structure for logics of concurrent behaviours, which we can call an axiomatization
of concurrency. Particular logics or type systems would be built on top of this structure,
through the choice of appropriate operators, and possibly extra axioms, so that soundness
of a particular type system for a particular calculus reduces to the fact that the considered
calculus does provide an appropriate conjunctive structure.

References

1 Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. *Mathematical Structures in Computer Science*, 12(5):625–665, 2002. doi:10.1017/S0960129502003730.

2 Emmanuel Beffara. *Logique, réalisabilité et concurrence*. PhD Thesis, Université Paris 7, December 2005.

3 G. Birkhoff. *Lattice theory*, volume 25 of *Colloquium publications*. American Mathematical Society, 1940.

4 Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In *Proceedings of ICFP 2000*, SIGPLAN Notices 35(9), pages 233–243. ACM, 2000. doi:10.1145/351240.351262.

5 Étienne Duchesne. *La localisation en logique : géométrie de l'interaction et sémantique dénotationnelle*. Thèse de doctorat, Université Aix-Marseille 2, 2009. URL: http://www.theses.fr/2009AIX22080.

6 Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, and Alexandre Miquel. Ordered combinatory algebras and realizability. *Mathematical Structures in Computer Science*, 27(3):428–458, 2017. doi:10.1017/S0960129515000432.

7 Yuxi Fu. The χ-Calculus. In *1997 Advances in Parallel and Distributed Computing Conference (APDC)*, pages 74–81. Computer Society Press, 1997.

8 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1 – 101, 1987. doi:10.1016/0304-3975(87)90045-4.

9 Jean-Yves Girard. Locus Solum: From the rules of logic to the logic of rules. *Mathematical Structures in Computer Science*, 11(3):301–506, June 2001. doi:10.1017/S096012950100336X.

10 Kohei Honda and Nobuko Yoshida. Combinatory representation of mobile processes. In *ACM-SIGACT Symposium on Principles of Programming Languages*, 1994.

11 Kohei Honda and Nobuko Yoshida. Replication in concurrent combinators. In Masami Hagiya and John C. Mitchell, editors, *Theoretical Aspects of Computer Software*, pages 786–805, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.

12 J.M.E. Hyland. The effective topos. *Studies in Logic and the Foundations of Mathematics*, 110:165 – 216, 1982. The L. E. J. Brouwer Centenary Symposium. doi:10.1016/S0049-237X(09)70129-6.

13 J.-L. Krivine. Realizability in classical logic. In Interactive models of computation and program behaviour. *Panoramas et synthèses*, 27:197–229, 2009. Publisher: Société Mathématique de France.

14 Jean-Louis Krivine. Realizability algebras II : new models of ZF + DC. *Logical Methods in Computer Science*, 8(1):10, February 2012. 28 p. doi:10.2168/LMCS-8(1:10)2012.

15 Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing. *Mathematical Structures in Computer Science*, 30(5):458–510, 2020. doi:10.1017/S0960129520000079.

16 Étienne Miquey. Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. In Maribel Fernández and Anca Muscholl, editors, *28th EACSL Annual Conference on Computer Science Logic (CSL 2020)*, volume 152 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 30:1–30:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2020/11673, doi:10.4230/LIPIcs.CSL.2020.30.
17 Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In Erich Grädel and Reinhard Kahle, editors, *Computer Science Logic '09*, volume 5771 of *Lecture Notes in Computer Science*, pages 409–423. Springer, Heidelberg, 2009. doi:10.1007/978-3-642-04027-6\_30.

18 Guillaume Munch-Maccagnoni. *Syntax and Models of a non-Associative Composition of Programs and Proofs*. PhD thesis, Univ. Paris Diderot, 2013.

19 Joachim Parrow and Björn Victor. The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In *13th IEEE Symposium on Logic in Computer Science (LICS)*, pages 176–185, 1998.

20 Andrew M. Pitts. Tripos theory in retrospect. *Mathematical Structures in Computer Science*, 12(3):265–279, 2002. doi:10.1017/S096012950200364X.

21 Davide Sangiorgi and David Walker. *The π-Calculus: A Theory of Mobile Processes*. Cambridge University Press, 2001.

22 Thomas Streicher. Krivine's classical realisability from a categorical perspective. *Mathematical Structures in Computer Science*, 23(6):1234–1256, 2013. doi:10.1017/S0960129512000989.

23 Lucian Wischik and Philippa Gardner. Explicit fusions. *Theoretical Computer Science*, 340(3):606–630, August 2005. doi:10.1016/j.tcs.2005.03.017.
A Logic in conjunctive structures

We give here the proofs of Section 2, with all the details, but the proofs are mostly simple combinatorial manipulations within CISs.

► **Definition 56.** Let us consider a conjunctive involutive structure. We define:

$$S'_{3} \triangleq \lambda_{a,b \in \mathbb{C}}(a \mathfrak{N} b) \to (b \mathfrak{N} a)$$

$$S'_{4} \triangleq \lambda_{a,b,c \in \mathbb{C}}(a \to b) \to (b \to c) \to a \to c$$

$$t \circ s \triangleq S'_{4} * s * t$$

It is easy to check that:

► **Lemma 57.** For any CIMA $(\mathbb{C}, S)$, we have $S'_{3}, S'_{4} \in S$ and $S$ is closed under $\circ$.

**Proof.** As for implicative algebras, separators of CIMAs are closed under application $*$, therefore they contains $S'_{3}, S'_{4}$ and are also closed under composition $\circ$. ◀

► **Proposition 58.** Let us consider a CIMA $(\mathbb{C}, S)$. The following are members of $S$:

1. $I \triangleq \lambda_{a \in \mathbb{C}} a \to a$.

2. $\lambda_{a,b,c \in \mathbb{C}}(a \otimes (b \otimes c)) \to ((a \otimes b) \otimes c)$.

3. $\lambda_{a,b \in \mathbb{C}} a \to b \to (a \otimes b)$.

4. $\lambda_{a,b \in \mathbb{C}}(a \mathfrak{N} b) \to (b \mathfrak{N} a)$.

5. $\lambda_{a,b \in \mathbb{C}}(a \to b) \to (a \mathfrak{N} c) \to (b \mathfrak{N} c)$.

6. $\lambda_{a,b,c \in \mathbb{C}}(a \mathfrak{N} b) \mathfrak{N} c \to a \mathfrak{N} (b \mathfrak{N} c)$ and $\lambda a \mathfrak{N} (b \mathfrak{N} c) \to (a \mathfrak{N} b) \mathfrak{N} c$.

**Proof.**

1. For any $a \in \mathbb{C}$ we have $S_6 \preceq a \to a \otimes \mathbf{1}$ and $S_7 \preceq a \otimes \mathbf{1} \to a$. Then $S_7 \circ S_6 \preceq a \to a$ (uniformly on $a \in \mathbb{C}$) and by Lemma 57 we get $S_7 \circ S_6 \in S$ and then $\lambda_{a \in \mathbb{C}} a \to a \in S$.

2. For all $a, b, c \in \mathbb{C}$ we have:

$$S_3 \preceq a \otimes (b \otimes c) \to (b \otimes c) \otimes a$$

$$S_5 \preceq (b \otimes c) \otimes a \to b \otimes (c \otimes a)$$

$$S_3 \preceq b \otimes (c \otimes a) \to (c \otimes a) \otimes b$$

$$S_5 \preceq (c \otimes a) \otimes b \to c \otimes (a \otimes b)$$

$$S_3 \preceq c \otimes (a \otimes b) \to (a \otimes b) \otimes c$$

Then $S_3 \circ S_5 \circ S_3 \circ S_5 \preceq a \otimes (b \otimes c) \to (a \otimes b) \otimes c$ for all $a, b, c \in \mathbb{C}$ and by Lemma 57 we get $S_3 \circ S_5 \circ S_3 \circ S_5 \circ S_3 \in S$, thus concluding $\lambda_{a,b,c \in \mathbb{C}} a \otimes (b \otimes c) \to (a \otimes b) \otimes c \in S$.

3. By definition $a \to b \to (a \otimes b) = (a \otimes (b \otimes (a \otimes b)^{\perp}))^{\perp}$. It suffices to find $U \in S$ uniform on $a, b$ s.t. $U \preceq (a \otimes (b \otimes (a \otimes b)^{\perp}))^{\perp}$. By Item 2, $T \preceq a \otimes (b \otimes (a \otimes b)^{\perp}) \to (a \otimes b) \otimes (a \otimes b)^{\perp}$ for some $T \in S$. By monotonicity of $*$, $S_8 * T \preceq ((a \otimes b) \otimes (a \otimes b)^{\perp})^{\perp} \to (a \otimes (b \otimes (a \otimes b)^{\perp}))^{\perp}$ and then $S_8 * T * I \preceq (a \otimes (b \otimes (a \otimes b)^{\perp}))^{\perp} = a \to b \to (a \otimes b)$. By Lemma 57 we get the result.

4. $S_8 * S_3 \preceq \lambda_{a,b \in \mathbb{C}}(a \mathfrak{N} b) \to (b \mathfrak{N} a)$ and by Lemma 57 we get the result.

5. On one hand $(a \to b) \to (a \mathfrak{N} c) \to (b \mathfrak{N} c) = (a \to b) \to (a^{\perp} \otimes c^{\perp})^{\perp} \to (b^{\perp} \otimes c^{\perp})^{\perp}$. On the other hand we have:

$$S_3 \preceq (b^{\perp} \to a^{\perp}) \to (b^{\perp} \otimes c^{\perp}) \to (a^{\perp} \otimes c^{\perp})$$

$$S_3 \circ S_8 \preceq (a \to b) \to (b^{\perp} \otimes c^{\perp}) \to (a^{\perp} \otimes c^{\perp})$$

$$S_8 \circ S_3 \circ S_8 \preceq (a \to b) \to (a^{\perp} \otimes c^{\perp})^{\perp} \to (b^{\perp} \otimes c^{\perp})^{\perp}$$

By Lemma 57 we get the result.
6. On one hand $(a \mathfrak{N} b) \mathfrak{N} c \to a \mathfrak{N} (b \mathfrak{N} c) = ((a^{\perp} \otimes b^{\perp}) \otimes c^{\perp})^{\perp} \to (a^{\perp} \otimes (b^{\perp} \otimes c^{\perp}))^{\perp}$. On the other hand $T \asymp a^{\perp} \otimes (b^{\perp} \otimes c^{\perp}) \to (a^{\perp} \otimes b^{\perp}) \otimes c^{\perp}$ for some $T \in \mathcal{S}$ and $S_8 * T \asymp ((a^{\perp} \otimes b^{\perp}) \otimes c^{\perp})^{\perp} \to ((a^{\perp} \otimes (b^{\perp} \otimes c^{\perp}))^{\perp})$. By Lemma 57 we get the result. ▲

**► Proposition 59.** For any CIMA $(\mathbb{C}, \mathcal{S})$, $\lambda_{a,b,c \in \mathbb{C}}(a \mathfrak{N} b) \otimes c \to a \mathfrak{N} (b \otimes c) \in \mathcal{S}$

**Proof.** We must prove $\lambda_{a,b,c \in \mathbb{C}}(( (a^{\perp} \otimes b^{\perp})^{\perp} \otimes c ) \otimes (a^{\perp} \otimes (b \otimes c)^{\perp}) )^{\perp} \in \mathcal{S}$. On one hand we have $S_5 \asymp ((a^{\perp} \otimes b^{\perp})^{\perp} \otimes c) \otimes (a^{\perp} \otimes (b \otimes c)^{\perp}) \to (a^{\perp} \otimes b^{\perp})^{\perp} \otimes (c \otimes (a^{\perp} \otimes (b \otimes c)^{\perp}))$. By Proposition 58.2 $T_1 \asymp (a^{\perp} \otimes b^{\perp})^{\perp} \otimes (c \otimes (a^{\perp} \otimes (b \otimes c)^{\perp})) \to (a^{\perp} \otimes b^{\perp})^{\perp} \otimes ((c \otimes a^{\perp}) \otimes (b \otimes c)^{\perp})$ for some $T_1 \in \mathcal{S}$. Using the combinatorial $S_3, S_4$ we have $T_2 \asymp (a^{\perp} \otimes b^{\perp})^{\perp} \otimes ((c \otimes a^{\perp}) \otimes (b \otimes c)^{\perp}) \to (a^{\perp} \otimes b^{\perp})^{\perp} \otimes ((b \otimes c)^{\perp} \otimes (a^{\perp} \otimes c))$ for some $T_2 \in \mathcal{S}$. By Proposition 58.2 using the combinatorial $S_3, S_4$ we have $T_3 \asymp ((a^{\perp} \otimes b^{\perp})^{\perp} \otimes c) \otimes (a^{\perp} \otimes (b \otimes c)^{\perp}) \to (a^{\perp} \otimes b^{\perp})^{\perp} \otimes ((b \otimes c)^{\perp} \otimes (a^{\perp} \otimes c))$ for some $T_3 \in \mathcal{S}$ and $T_4 \asymp ((a^{\perp} \otimes b^{\perp})^{\perp} \otimes ((b \otimes c)^{\perp} \otimes (a^{\perp} \otimes c))^{\perp}) \to (( (a^{\perp} \otimes b^{\perp})^{\perp} \otimes c ) \otimes (a^{\perp} \otimes (b \otimes c)^{\perp})^{\perp})$ for some $T_4 \in \mathcal{S}$. In other terms we have:

$$T_4 \asymp ((a^{\perp} \to b) \to ((b \to c^{\perp}) \to (a^{\perp} \to c^{\perp}))) \to ((a \mathfrak{N} b) \otimes c \to a \mathfrak{N} (b \otimes c))$$

From which we deduce $T_4 * S'_4 \asymp (a \mathfrak{N} b) \otimes c \to a \mathfrak{N} (b \otimes c)$ for all $a, b, c \in \mathbb{C}$ and hence $T_4 * S'_4 \asymp \lambda_{a,b,c \in \mathbb{C}}(a \mathfrak{N} b) \otimes c \to a \mathfrak{N} (b \otimes c)$, thus proving the result. ▲

**► Proposition 60.** For any CIMA $(\mathbb{C}, \mathcal{S})$ and any permutation $\sigma$, we have:

1. $\mathrm{ex}(\sigma) \triangleq \lambda_{a_1, \dots, a_k \in \mathbb{C}} (a_1 \mathfrak{N} \cdots \mathfrak{N} a_k) \to (a_{\sigma(1)} \mathfrak{N} \cdots \mathfrak{N} a_{\sigma(k)}) \in \mathcal{S}$.

2. $I \in \mathcal{S}$.

3. $t \triangleq \lambda_{a,b,g,d \in \mathbb{C}} (g \mathfrak{N} a) \to (b \mathfrak{N} d) \to g \mathfrak{N} ((a \otimes b) \mathfrak{N} d) \in \mathcal{S}$

4. $c \triangleq \lambda_{a,g,d \in \mathbb{C}} (g \mathfrak{N} a) \to (a^{\perp} \mathfrak{N} d) \to (g \mathfrak{N} d) \in \mathcal{S}$.

5. $1 \in \mathcal{S}$.

**Proof.**

1. Is a consequence of $S'_3, S'_4 \in \mathcal{S}$, the Proposition 58.6 and Lemma 57. For instance, let us prove that $\lambda_{a_1, a_2, a_3} a_1 \mathfrak{N} a_2 \mathfrak{N} a_3 \to a_3 \mathfrak{N} a_2 \mathfrak{N} a_1 \in \mathcal{S}$. By Proposition 58.6 $T_1 \asymp (a_1 \mathfrak{N} (a_2 \mathfrak{N} a_3)) \to ((a_2 \mathfrak{N} a_3) \mathfrak{N} a_1)$ for some $T_1 \in \mathcal{S}$. By Proposition 58.4 and Definition 8, $T_2 \asymp ((a_2 \mathfrak{N} a_3) \mathfrak{N} a_1) \to ((a_3 \mathfrak{N} a_2) \mathfrak{N} a_1)$ for some $T_2 \in \mathcal{S}$. By Proposition 58.6, $T_3 \asymp ((a_3 \mathfrak{N} a_2) \mathfrak{N} a_1) \to (a_3 \mathfrak{N} (a_2 \mathfrak{N} a_1))$ for some $T_3 \in \mathcal{S}$. By Lemma 57 $T_3 \circ T_2 \circ T_1 \in \mathcal{S}$ and $T_3 \circ T_2 \circ T_1 \asymp (a_1 \mathfrak{N} a_2 \mathfrak{N} a_3) \to (a_3 \mathfrak{N} a_2 \mathfrak{N} a_1)$ for all $a_1, a_2, a_3 \in \mathbb{C}$, all which ends the proof.

2. By Proposition 58.1.

3. By Proposition 58.3, $T_0 \asymp (g \mathfrak{N} a) \to (b \mathfrak{N} d) \to (g \mathfrak{N} a) \otimes (b \mathfrak{N} d)$ for some $T_0 \in \mathcal{S}$. By Proposition 59, $T_1 \asymp (g \mathfrak{N} a) \otimes (b \mathfrak{N} d) \to g \mathfrak{N} (a \otimes (b \mathfrak{N} d))$ for some $T_1 \in \mathcal{S}$. By Definition 8, Proposition 58.5 and Proposition 59, $T_2 \asymp g \mathfrak{N} (a \otimes (b \mathfrak{N} d)) \to g \mathfrak{N} ((a \otimes b) \mathfrak{N} d)$ for some $T_2 \in \mathcal{S}$. By Lemma 57, $T_2 \circ T_1 \circ T_0 \in \mathcal{S}$ and $T_2 \circ T_1 \circ T_0 \asymp (g \mathfrak{N} a) \to (b \mathfrak{N} d) \to g \mathfrak{N} ((a \otimes b) \mathfrak{N} d)$ for all $g, d, a, b \in \mathbb{C}$, all which ends the proof.

4. On one hand $S'_4 \asymp (g^{\perp} \to a) \to (a \to d) \to (g^{\perp} \to d)$ which in turn gives

$$S'_4 \asymp (g \mathfrak{N} a) \to (a^{\perp} \mathfrak{N} d) \to (g \mathfrak{N} d) \in \mathcal{S}$$

for all $g, d, a \in \mathbb{C}$ and hence $S'_4 \asymp \lambda_{g,d,a \in \mathbb{C}}(g \mathfrak{N} a) \to (a^{\perp} \mathfrak{N} d) \to (g \mathfrak{N} d) \in \mathcal{S}$.
5. By Definition 8, (unit)-rule.

<figure><img src="image_11.png" /></figure>

As a consequence, we directly deduce from the previous proposition the soundness of MLL semantic typing rules:

**Theorem 12.** *The semantic typing rules of Figure 1 are sound for all unitary CS. Moreover, for any CIMA $(C, S)$ if $\vdash a : \Gamma$ is provable, then $a \in S$.*

**Proposition 61.** *We pose comp $\triangleq \lambda_{a,b,c \in C}(a \to b) \to (b \to c) \to a \to c$ and $t \circ u \triangleq$ comp@t@u. We have that comp $\in S$ and if $t \preceq a \to b$ and $u \preceq b \to c$ implies that $t \circ u \preceq a \to c$ (for any $t, u, a, b, c \in C$).*

**Proof.**

<figure><img src="image_12.png" /></figure>

**Proposition 62.** **For any $a, b \in C$, if $a \in S$ and $b \in S$, then $a \otimes b \in S$.**

**Proposition 41.** *The following behaviors are realized by pure fusions:*

1. $\bigcap_{A \in \mathbb{B}} A \to A$.

2. $\bigcap_{A,B \in \mathbb{B}} (A \otimes B) \to (B \otimes A)$.

3. $\bigcap_{A,B,C \in \mathbb{B}} (A \negmedspace\negmedspace\negmedspace\negmedspace\to B) \negmedspace\negmedspace\negmedspace\negmedspace\to (B \negmedspace\negmedspace\negmedspace\negmedspace\to C) \negmedspace\negmedspace\negmedspace\negmedspace\to A \negmedspace\negmedspace\negmedspace\negmedspace\to C$.

4. $\bigcap_{A,B,C \in \mathbb{B}} ((A \otimes B) \otimes C) \to (A \otimes (B \otimes C))$.

5. $\bigcap_{A \in \mathbb{B}} A \to (1 \otimes A)$.

6. $\bigcap_{A \in \mathbb{B}} (1 \otimes A) \to A$.

7. $\bigcap_{A,B \in \mathbb{B}} (A \to B) \to (B^{\perp} \to A^{\perp})$.

As we have seen, the first statement is the Proposition 39. We will prove the remaining statements one by one in the following lemmas.

**Lemma 63.** *Let us consider $A, B \in \mathcal{P}(\bar{\Pi})$. Let us define the substitution $\tau : \mathbb{N}^1 \to \mathbb{N}^2$ s.t. $\tau(n.1.1) \triangleq n.2.2$ and $\tau(n.2.1) \triangleq n.1.2$. Then $S'_3 \triangleq \varepsilon_\tau \in (A \otimes B) \to (B \otimes A)$*

**Proof.** By Definition 35 $(A \otimes B) \to (B \otimes A) = ((A \bullet B) \bullet (B \bullet A)^\perp)^\perp$. Consider $p \in (B \bullet A)^\perp$, $q \in A$ and $r \in B$. By hypothesis we get $\bar{\nu}(r^1|q^2|p) \in \perp$. By definition $q^{1.1}|r^{2.1}|p^2 \in (A \otimes B) \to (B \otimes A)$. It is enough to prove that $\varepsilon_\tau \perp q^{1.1}|r^{2.1}|p^2$, i.e.: $\bar{\nu}(q^{1.1}|r^{2.1}|p^2|\varepsilon_\tau) \in \perp$. Moreover $\bar{\nu}(q^{1.1}|r^{2.1}|p^2|\varepsilon_\tau) = (\nu\mathbb{N}^2)(\nu\mathbb{N}^1)(q^{1.1}|r^{2.1}|p^2|\varepsilon_\tau) = (\nu\mathbb{N}^2)(q^{2.2}|r^{1.2}|p^2) \equiv \bar{\nu}(r^1|q^2|p) \in \perp$, which ends the proof.

<figure><img src="image_13.png" /></figure>

**B Processes with global fusions**

The main technical issue that needs to be addressed is how to compose fusions whose domains
lies on disjoint spaces of names with substitutions that link those spaces. The following
lemma is a fundamental result in this sense:

**Lemma 64.** Let $X \subset \mathbb{N}$, $\tau: X \to X^c$ and $e, f \in \mathcal{E}$ with $|e| \subseteq X$ and $|f| \subseteq X^c$. Then:

1. $ef\varepsilon_\tau \Xleftarrow{} X = e^\tau f$.

2. If $x \in X^c$ then $[x]_{ef\varepsilon_\tau} \Xleftarrow{} X = [x]_{e^\tau f}$. If $x \in X$ then $[x]_{ef\varepsilon_\tau} \Xleftarrow{} X = [\tau(x)]_{e^\tau f}$.

**Proof.** **1.** We start by a remark: Let us consider $a \stackrel{\sim}{\sim} b$ with $a, b \in X^c$. By definition of $ef\varepsilon_\tau = \text{tcl}(e \cup f \cup \{(x, \tau(x)) \mid x \in X\})$, there exists sequences $S_0, \dots, S_k$ s.t. each $S_j$ has the shape $x_{4j} \stackrel{\sim}{\sim} x_{4j+1} \stackrel{\sim}{\sim} x_{4j+2} \stackrel{\sim}{\sim} x_{4j+3} \stackrel{\sim}{\sim} x_{4(j+1)}$ with $x_{4j}, x_{4j+1}, x_{4(j+1)} \in X^c$ and $x_{4j+2}, x_{4j+3} \in X$ and $a = x_0, x_{4(k+1)} \stackrel{\sim}{\sim} x_{4(k+1)+1} = b$:
<figure><img src="image_14.png" /></figure>

On the chain above observe that the sequences $x_{4j+1} \sim_{\varepsilon_\tau} x_{4j+2} \sim_e x_{4j+3} \sim_{\varepsilon_\tau} x_{4(j+1)}$ can be replaced by $x_{4j+1} \sim_{\varepsilon_\tau} x_{4(j+1)}$. This observation yields $ef\varepsilon_\tau \setminus X \subseteq e^\tau f$. The converse inclusion is straightforward since $e^\tau \subseteq e\varepsilon_\tau \setminus X$.

2. Let us consider $x \in X^c$. Given $y \in X^c$ by 1 it happens that $x \sim_{ef\varepsilon_\tau} y$ iff $x \sim_{e^\tau f} y$, thus concluding that $[x]_{ef\varepsilon_\tau} \setminus X = [x]_{e^\tau f}$. Let us consider $x \in X$. By definition of $ef\varepsilon_\tau$ we have $[x]_{ef\varepsilon_\tau} = [\tau(x)]_{ef\varepsilon_\tau}$ and then $[x]_{ef\varepsilon_\tau} \setminus X = [\tau(x)]_{e^\tau f}$, the last equality by the previous part.

<figure><img src="image_15.png" /></figure>

The following is a technical requirement to prove Proposition 29

**Lemma 65.** Consider $e, f \in \mathcal{E}$ with $|e| \subseteq X$ and $|f| \subseteq X^c$ for some set $X \subset \mathbb{N}$ and $\tau: X \to X^c$ a substitution. Clearly $[x]_{ef\varepsilon_\tau} \cap X^c \neq \emptyset$ for all $x \in \mathbb{N}$ and then $\mu_{(X,ef\varepsilon_\tau)}(x) = \min([x]_{ef\varepsilon_\tau} \setminus X)$ for all $x \in \mathbb{N}$. By Lemma 64.2 we have $[x]_{ef\varepsilon_\tau} \setminus X = [\tau(x)]_{e^\tau f}$ if $x \in X$ and $[x]_{ef\varepsilon_\tau} \setminus X = [x]_{e^\tau f}$ if not. We conclude that

$$ \mu_{(X,ef\varepsilon_\tau)}(x) = \begin{cases} (\tau(x))_{e^\tau f}^{\bullet} & \text{if } x \in X \\ x_{e^\tau f}^{\bullet} & \text{if } x \in X^c \end{cases} $$

**Proposition 29.** Consider a substitution $\tau: X \to X^c$ for a set $X \subset \mathbb{N}$ and $p, q \in \bar{\Pi}$ such that $\mathrm{FN}(p) \subseteq X$ and $\mathrm{FN}(q) \subseteq X^c$. Then $(\nu X)(p | q | \varepsilon_\tau) \equiv_\alpha p^\tau | q$.

**Proof.** Observe that $\varepsilon_\tau$ makes that $[x]_{ef\varepsilon_\tau} \cap X^c \neq \emptyset$ for all $x \in \mathbb{N}$. Observe also that by Lemma 64.1 $ef\varepsilon_\tau \setminus X = e^\tau f$. Suppose that $p = (P, e)$ and $q := (Q, f)$. Applying Definition 28 we get $(\nu X)(p | q | \varepsilon_\tau) = (\nu X)(P | Q, ef\varepsilon_\tau) \equiv_\alpha (P^{\mu_{(X,ef\varepsilon_\tau)}} | Q^{\mu_{(X,ef\varepsilon_\tau)}}, e^\tau f)$ (the vector of names $x_{1,ef\varepsilon_\tau}^\bullet, \dots, x_{h,ef\varepsilon_\tau}^\bullet$ is empty). By Lemma 65 and the hypothesis $\mathrm{FN}(P) \subseteq X$ and $\mathrm{FN}(Q) \subseteq X^c$ we get $(P^{\mu_{(X,ef\varepsilon_\tau)}} | Q^{\mu_{(X,ef\varepsilon_\tau)}}, e^\tau f) \equiv_\alpha (P^\tau | Q, e^\tau f) = p^\tau | q$. $\blacksquare$

<figure><img src="image_16.png" /></figure>

The following is a technical prerequisite to prove Lemma 25:

**Lemma 66.** Let us consider $x, y \in \mathbb{N}$, $e \in \mathcal{E}$ and $\sigma \triangleq \{y := y_e^*\}$, $\tau \triangleq \{x := x_e^* \setminus \{y\}\}$, $\sigma' \triangleq \{x := x_e^*\}$ and $\tau' \triangleq \{y := y_e^* \setminus \{x\}\}$. Then:

1. If $[x]_e = [y]_e = \{x, y\}$, then $\tau \circ \sigma = \{y := x\}$ and $\tau' \circ \sigma' = \{x := y\}$ and then they are equivalent by the transposition $(xy)$.

2. If $x \not\sim_e y$ or $[x]_e = [y]_e \supset \{x, y\}$, then $\tau \circ \sigma = \tau' \circ \sigma'$.

In both cases we conclude that $\tau \circ \sigma \sim \tau' \circ \sigma'$.

**Proof.** For $x = y$ is clear. If $x \neq y$ there are two cases:

1. $x \sim_e y$. This case splits into two subcases:

a. $[x]_e = [y]_e = \{x, y\}$. Observe that $x_e^* = y, y_e^* \setminus \{x\} = y, y_e^* = x$ and $x_e^* \setminus \{y\} = x$ and then $\tau \circ \sigma = \sigma = \{y := x\}$ and $\tau' \circ \sigma' = \sigma' = \{x := y\}$ which are equivalent by means of the permutation $(xy)$ (in fact a transposition).

b. $[x]_e = [y]_e \supset \{x, y\}$. Let us consider $z = \min([x]_e \setminus \{x, y\})$. Without loss of generality we can suppose that $x < y$. Then we have three subcases:
i. $z < x < y$. In this case $x_e^* = z$, $y_{e\{x\}}^* = z$ and $y_e^* = z$, $x_{e\{y\}}^* = z$. Thus $\sigma = \tau' = \{y := z\}$, $\sigma' = \tau = \{x := z\}$ and hence $\tau \circ \sigma = \tau' \circ \sigma'$ (which are equivalent by means of the identity).

ii. $x < z < y$. In this case $x_e^* = z$, $y_{e\{x\}}^* = z$ and $y_e^* = x$, $x_{e\{y\}}^* = z$. Thus $\sigma = \{y := x\}$, $\tau = \{x := z\}$, $\sigma' = \{x := z\}$ and $\tau' = \{y := z\}$ from which we get $\tau \circ \sigma = \{y := z, x := z\} = \tau' \circ \sigma'$.

iii. $x < y < z$. In this case $x_e^* = y$, $y_{e\{x\}}^* = z$ and $y_e^* = x$, $x_{e\{y\}}^* = z$. Thus $\sigma = \{y := x\}$, $\tau = \{x := z\}$, $\sigma' = \{x := y\}$ and $\tau' = \{y := z\}$ from which we get $\tau \circ \sigma = \{y := z, x := z\} = \tau' \circ \sigma'$.

2. Suppose that $x \not\sim_e y$. Then we have that $x_e^* = x_{e\{y\}}^* = x'$ and $y_e^* = y_{e\{x\}}^* = y'$ for some $x' \not\sim_e y'$. Thus $\sigma = \tau' = \{y := y'\}$, $\sigma' = \tau = \{x := x'\}$ from which we get $\tau \circ \sigma = \{x := x', y := y'\} = \tau' \circ \sigma'$.

**Lemma 25.** Consider $(P,e) \in \bar{\Pi}$ and $x, y \in \mathbb{N}$, then $(\nu x)(\nu y)(P,e) \equiv_{\alpha} (\nu y)(\nu x)(P,e)$.

**Proof.** On one side:

$$ (\nu x)(\nu y)(P,e) = (\nu x)((\nu y)P\{y := y_e^*\}, e\{y\}) = ((\nu xy)P\{y := y_e^*\}\{x := x_{e\{y\}}^*\}, e\{x, y\}) $$

On the other hand, by Lemma 66, the last process is $\alpha$-equivalent to

$$ ((\nu xy)P\{x := x_e^*\}\{y := y_{e\{x\}}^*\}, e\{x, y\}) = (\nu y)((\nu x)P\{x := x_e^*\}, e\{x\}) = (\nu y)(\nu x)(P,e) $$

The generalization to finite sets is direct.

## C Concurrent realizability with PGF

We give here the proof of Section 4.1.

**Proposition 31.** For all $A, B \in \mathbb{P}$ and for any non-empty $\mathfrak{B} \subseteq \mathbb{P}$ we have:

1. If $A \subseteq B$ then $B^{\perp} \subseteq A^{\perp}$

2. $A \subseteq A^{\perp\perp}$ and $A^{\perp} = A^{\perp\perp}$

3. $(\bigcup_{X \in \mathfrak{B}} X)^{\perp} = \bigcap_{X \in \mathfrak{B}} X^{\perp}$ and if $\mathfrak{B} \neq \emptyset$ then $(\bigcap_{X \in \mathfrak{B}} X)^{\perp} \supseteq (\bigcup_{X \in \mathfrak{B}} X^{\perp})$

4. $(\bigcup_{X \in \mathfrak{B}} X^{\perp\perp})^{\perp} = (\bigcup_{X \in \mathfrak{B}} X)^{\perp}$

**Proof.** 1, 2, 3 are evident by definition. Observe that $(\bar{\Pi}, \bar{\Pi}, \perp)$ where $\perp = \{(p, q) | p \perp q\}$ is called a *polarity* on [6] and it defines a Galois connection [3]. For 4. observe that

$$ (\bigcup_{X \in \mathfrak{B}} X^{\perp\perp})^{\perp} = \bigcap_{X \in \mathfrak{B}} X^{\perp\perp} = \bigcap_{X \in \mathfrak{B}} X^{\perp} = (\bigcup_{X \in \mathfrak{B}} X)^{\perp}. $$

**Proposition 37.** Let us consider $A, B, C \in \mathbb{P}$. Then:

1. $C \subseteq A \to B \iff C * A \subseteq B^{\perp\perp}$.

2. $C * A = \bigcap\{B \in \mathbb{B} | C \subseteq A \to B\} = \min\{B \in \mathbb{B} | C \subseteq A \to B\}$. (In particular, if $B \in \mathbb{B}$ then $C \subseteq A \to B \iff C * A \subseteq B$).
**Proof. 1.** Observe that $A \to B = (A \bullet B^{\perp})^{\perp}$.

$$ 
\begin{align*}
C \subseteq (A \bullet B^{\perp})^{\perp} &\Leftrightarrow \quad \forall p \in C \quad \forall q \in A \quad \forall r \in B^{\perp} \quad p \perp q \bullet r \\
&\Leftrightarrow \quad \forall p \in C \quad \forall q \in A \quad \forall r \in B^{\perp} \quad \bar{\nu}(p|q^1|r^2) \in \mathbb{1} \\
&\Leftrightarrow \quad \forall p \in C \quad \forall q \in A \quad \forall r \in B^{\perp} \quad (\nu\mathbb{N}^2)((\nu\mathbb{N}^1)(p|q^1)|r^2) \in \mathbb{1} \\
&\Leftrightarrow \quad \forall p \in C \quad \forall q \in A \quad \forall r \in B^{\perp} \quad \bar{\nu}((\nu\mathbb{N}^1)(p|q^1)^{-2}|r) \in \mathbb{1} \\
&\Leftrightarrow \quad \forall p \in C \quad \forall q \in A \quad \forall r \in B^{\perp} \quad p \ast q \perp r \\
&\Leftrightarrow \quad C \ast A \subseteq B^{\perp\perp}
\end{align*}
$$

2. Applying the immediate previous result, we have that $C \ast A \subseteq C \ast A \iff C \subseteq A \to (C \ast A)$. Then $C \ast A \in \{B | C \subseteq A \to B\}$. On the other hand, if $C \subseteq A \to B$, then $C \ast A \subseteq B$.

<figure><img src="image_17.png" /></figure>

**► Proposition 36.** For any $A, B \in \mathbb{P}$, it holds that $(A \bullet B)^{\perp} = (A^{\perp \perp} \bullet B^{\perp \perp})^{\perp}$. As a consequence, $A \otimes B = A^{\perp \perp} \otimes B^{\perp \perp}$, $A \otimes B = A^{\perp \perp} \otimes B^{\perp \perp}$ and $A \to B = A^{\perp \perp} \to B^{\perp \perp}$.

**Proof.** Observe that $\bar{\nu}(p^1 | q^2 | r) = \bar{\nu}(((\nu\mathbb{N}^2)(r | q^2))^{-1} | p) = \bar{\nu}(((\nu\mathbb{N}^1)(r | p^1))^{-2} | q)$ for all processes $p, q, r$.

The inclusion $(A^{\perp \perp} \bullet B^{\perp \perp})^{\perp} \subseteq (A \bullet B)^{\perp}$ is true by anti monotonicity of the orthogonal operator. It remains to prove the reverse inclusion. Let us consider $r \in (A \bullet B)^{\perp}$ and try to prove that $r \in (A^{\perp \perp} \bullet B^{\perp \perp})^{\perp}$. We know that $\bar{\nu}(((\nu\mathbb{N}^2)(r | q^2))^{-1} | p) = \bar{\nu}(p^1 | q^2 | r) \in \mathbb{1}$ for all $p \in A, q \in B$ by the observation above. Then $((\nu\mathbb{N}^2)(r | q^2))^{-1} \in A^{\perp} = A^{\perp \perp}$ and thus $\bar{\nu}(p^1 | q^2 | r) \in \mathbb{1}$ for all $p \in A^{\perp \perp}, q \in B$. Applying again the observation above we conclude that $((\nu\mathbb{N}^1)(r | p^1))^{-2} \in B^{\perp \perp \perp}$ for all $p \in A^{\perp \perp}$. Finally again by this observation we get $\bar{\nu}(p^1 | q^2 | r) \in \mathbb{1}$ for all $p \in A^{\perp \perp}, q \in B^{\perp \perp}$, what we wanted to prove.

<figure><img src="image_18.png" /></figure>

# D The induced conjunctive involutive monoidal algebra

**► Proposition 40.** The tuple $(\mathbb{B}, \subseteq, \otimes, (\cdot)^{\perp})$, where $(\mathbb{B}, \subseteq)$ is the lattice defined in Proposition 32, is a conjunctive involutive structure.

**Proof.** We have to check that the first axioms of conjunctive structures are satisfied. The first part is just Proposition 32. Parts 2, 4 and 5 directly follow from the definition of $\mathbb{B}$, $\otimes$ and from Proposition 31. We prove the first case of part 3. For any $\mathfrak{B} \subseteq \mathbb{B}$, we have

$$ 
\begin{align*}
A \otimes \bigvee_{B \in \mathfrak{B}} B &\stackrel{\text{def } \vee}{=} A \otimes (\bigcup_{B \in \mathfrak{B}} B)^{\perp \perp} \\
&= A \otimes \bigcup_{\text{def } \otimes} B_{\text{def } \otimes} = (A \bullet \bigcup_{B \in \mathfrak{B}} B)^{\perp \perp} \\
&= (\bigcup_{B \in \mathfrak{B}} (A \bullet B))^{\perp \perp} \\
&= \text{Prop } 31.4 \quad (\bigcup_{B \in \mathfrak{B}} (A \bullet B)^{\perp \perp})^{\perp \perp} \\
&= \text{def } \otimes \quad (\bigcup_{B \in \mathfrak{B}} (A \otimes B))^{\perp \perp} \\
&= \text{def } \vee \quad \bigvee_{B \in \mathfrak{B}} (A \otimes B)
\end{align*}
$$

<figure><img src="image_19.png" /></figure>

Following we define a localized version for the application $\ast$ of Definition 34:

**► Definition 67.** Let us consider bijections $\iota_X : \mathbb{N} \to X$ and $\iota_Y : \mathbb{N} \to Y$ for (infinite) sets of names $X, Y$. Let us define:

1. Given $i = 1, 2$ we denote by $i.X$ the set $\{\iota_X(n.i) | n \in \mathbb{N}\}$. The associated bijection between $\mathbb{N}$ and $i.X$ is $\iota_X \circ \iota_i : \mathbb{N} \to X$ and then $i.X \triangleq \text{Im}(\iota_X \circ \iota_i)$. Whenever it does not cause confusion, we will write $p^X$ instead of $p^{i.X}$.

2. The fusion induced by $\iota_X, \iota_Y$ is $\varepsilon_{X,Y} \triangleq \bigvee_{n \in \mathbb{N}} (\iota_X(n) \leftrightarrow \iota_Y(n))$.
3. Given processes $p, q \in \bar{\Pi}$ define $p \otimes_{X,Y} q \triangleq ((\nu1.X)(\nu Y)(p^X | q^Y |_{1.X,Y} \varepsilon))^{(-X).(-2)}$ and $p \odot_{X,Y} q \triangleq \bar{\nu}(p^X | q^Y |_{X,Y} \varepsilon)$.

**Remark 68.** The following properties are immediate from Proposition 29:

1. We note that all of the above definitions depend on the bijections $\iota_X, \iota_Y$ rather than only on $X, Y$. The choice to use $X$ and $Y$ is to simplify the writing. Observe also that $((\nu1.X)(\nu Y)(p^X | q^Y |_{1.X,Y} \varepsilon)) = (p \otimes_{X,Y} q)^{2.X}$ and $\mathrm{FN}((\nu1.X)(\nu Y)(p^X | q^Y |_{1.X,Y} \varepsilon)) \subseteq 2.X$.

2. If $X, Y$ are disjoint, $p \in A \to B$ and $r \in A$, then $p \otimes_{X,Y} r \in B$.

3. If $X, Y$ are disjoint, $p \in C$ and $q \in C^\perp$ then $p \odot_{X,Y} q \in \mathbb{1}$.

**Lemma 69.** Let us consider $A, B, C \in \mathcal{P}(\bar{\Pi})$ and the following sets of names and injections:

$$
\begin{align*}
X &= \mathbb{N}^1, & \iota_X : \mathbb{N} &\to X, & \iota_X &\triangleq \iota_1 \\
Y &\triangleq \mathbb{N}^{1.2.2}, & \iota_Y : \mathbb{N} &\to Y, & \iota_Y(n) &\triangleq \mathrm{n.1.2.2} \\
Z &\triangleq \mathbb{N}^{1.2}, & \iota_Z : \mathbb{N} &\to Z, & \iota_Z(n) &\triangleq \mathrm{n.1.2} \\
W &\triangleq \mathbb{N}^{2.2.2}, & \iota_W : \mathbb{N} &\to W, & \iota_W(n) &\triangleq \mathrm{n.2.2.2}
\end{align*}
$$

Then $S_4 \triangleq \varepsilon_{1.X,Y} | \varepsilon_{1.Z,2.X} | \varepsilon_{2.Z,W} \in (A \to B) \to (B \to C) \to A \to C$.

**Proof.** Let us consider $p \in A \to B, q \in B \to C, r \in A, s \in C^\perp$. We must prove that $\bar{\nu}(p^X | q^Z | r^Y | s^W | S_4) \in \mathbb{1}$.

By Remark 68 we have $p \otimes_{X,Y} r \in B$; $q \otimes_{Z,2.X} (p \otimes_{X,Y} r) \in C$ and $(q \otimes_{Z,2.X} (p \otimes_{X,Y} r)) \odot_{2.Z,W} s \in \mathbb{1}$. This last process being structurally equivalent to $\bar{\nu}(p^X | q^Z | r^Y | s^W | S_4) \in \mathbb{1}$, which ends the proof. ▶

**Lemma 70.** Let us consider $A, B, C \subseteq \mathcal{P}(\bar{\Pi})$ and the substitution $\tau : \mathbb{N}^1 \to \mathbb{N}^2$ defined as $\tau(n.1.1.1) \triangleq \mathrm{n.1.2}$, $\tau(n.2.1.1) \triangleq \mathrm{n.1.2.2}$ and $\tau(n.2.1) \triangleq \mathrm{n.2.2.2}$. Then $S_5 \triangleq \mathcal{E}_\tau \in ((A \otimes B) \otimes C) \to (A \otimes (B \otimes C))$.

**Proof.** By definition of $\to$ and $\otimes$ we have $((A \otimes B) \otimes C) \to (A \otimes (B \otimes C)) = ((A \bullet B) \bullet C) \bullet (A \bullet (B \bullet C))^\perp \to^\perp$ Let us consider $p \in A, q \in B, r \in C$ and $s \in (A \bullet (B \bullet C))^\perp$. We must prove that $\bar{\nu}(\mathcal{E}_\tau | p^{1.1.1} | q^{2.1.1} | r^{2.1} | s^2) \in \mathbb{1}$. By Proposition 29 we get $\bar{\nu}(\mathcal{E}_\tau | p^{1.1.1} | q^{2.1.1} | r^{2.1} | s^2) \equiv (\nu\mathbb{N}^2)(p^{1.2} | q^{1.2.2} | r^{2.2.2} | s^2) \equiv \bar{\nu}(p^1 | q^{1.2} | r^{2.2} | s^2) \in \mathbb{1}$; the last being consequence of $p^1 | q^{1.2} | r^{2.2} \in A \bullet (B \bullet C)$. ◇

**Lemma 71.** Let us consider $A \subseteq \mathcal{P}(\bar{\Pi})$ and the substitution $\tau : \mathbb{N}^1 \to \mathbb{N}^2$ s.t. $\tau(n.1) \triangleq \mathrm{n.2.2}$. Then $S_6 \triangleq \mathcal{E}_\tau \in A \to (1 \otimes A)$.

**Proof.** By definition of $\to$ and $\otimes$ we have $A \to (1 \otimes A) = (A \bullet (1 \bullet A))^\perp$. Let us consider $p \in A$ and $q \in (1 \bullet A)^\perp$. It suffices to prove that $\varepsilon_\tau \perp p^1 | q^2$, i.e. $(\bar{\nu})(\varepsilon_\tau | p^1 | q^2) \in \mathbb{1}$. Applying Proposition 29 we get $(\bar{\nu})(\varepsilon_\tau | p^1 | q^2) \equiv_\alpha (\nu\mathbb{N}^2)(q^2 | p^{2.2}) \equiv_\alpha (\nu\mathbb{N}^2)(q^2 | 1 | p^{2.2}) \equiv_\alpha (\bar{\nu})(q | 1 | p^2)$. Since $1 | p^2 \in 1 \otimes A$ and $q \in (1 \otimes A)^\perp$, then $(\bar{\nu})(q | 1 | p^2) \in \mathbb{1}$. ◇

**Lemma 72.** Let us consider $A \subseteq \mathcal{P}(\bar{\Pi})$ and the substitution $\tau : \mathbb{N}^1 \to \mathbb{N}^2$ s.t. $\tau(n.1) \triangleq \mathrm{n.2.2}$. Then $S_6 \triangleq \varepsilon_\tau \in A \to (1 \otimes A)$.
**Proof.** By definition of $\to$ and $\otimes$ we have $(1 \otimes A) \to A = ((1 \bullet A) \bullet A^\perp)^\perp$. Let us consider $p \in A$ and $q \in A^\perp$. It suffices to prove that $\varepsilon_\tau \perp 1 | p^{2.1} | q^2$, i.e. $(\bar{\nu})(\varepsilon_\tau | 1 | p^{2.1} | q^2) \in \perp$. Applying Proposition 29 we get $(\bar{\nu})(\varepsilon_\tau | 1 | p^{2.1} | q^2) \equiv_\alpha (\nu\mathbb{N}^2)(p^2 | q^2) \equiv_\alpha (\bar{\nu})(p | q)$, being the last at $\perp$ because $p \perp q$ by assumption. ◀

**Proposition 73.** Let us define the fusion $\Phi \triangleq \bigvee_{n \in \mathbb{N}} (n.1 \leftrightarrow n.2.2)|(n.1.2 \leftrightarrow n.2.2)$. Then $\Phi * p * q \equiv p | q$ for all PGFs $p$ and $q$.

**Proof.**

$$ \begin{align*} \Phi * p \triangleq & ((\nu\mathbb{N}^1)(p^1 | \Phi))^{-2} & \text{by definition of } * \\ & \equiv (p^{1.2} | \bigvee_{n \in \mathbb{N}} (n.1.2 \leftrightarrow n.2.2))^{-2} & \text{by Proposition 29} \\ & = p^1 | I & \text{applying } \iota_2^{-1} \end{align*} $$

Then we get

$$ \begin{align*} \Phi * p * q &\equiv (p^1 | I) *_1 q & \text{by the remark above} \\ &\triangleq (\nu_1)(p^1 | q^1 | I)^{-2} & \text{by definition of } * \\ &\equiv (p^2 | q^2)^{-2} & \text{by Proposition 29} \\ &= p | q & \text{applying } \iota_2^{-1} \end{align*} $$

◀

## E Conjunctive algebras for concurrency

**Proposition 45.** Let us consider $(\mathbb{C}, \otimes, (\cdot)^\perp, 1, F, \llcorner)$ a CS with composition $F$. Then $aFb \llcorner c \iff a \llcorner b \triangleright_F c$ for all $a, b, c \in \mathbb{C}$.

**Proof.** Firstly, $aFb \llcorner c$ implies that $a \in \{x \in \mathbb{C} | xFb \llcorner c\}$ and then $a \llcorner b \triangleright_F c$. Conversely, since $F$ is monotone, we have

$$ aFb \llcorner (b \triangleright_F c)Fb = (\Upsilon\{x \in \mathbb{C} | xFa \llcorner c\}) | b \llcorner \Upsilon\{xFb | x \in \mathbb{C}, xFb \llcorner c\} \llcorner c \quad \text{◀} $$

**Lemma 74.** Let us consider $\mathfrak{B} \subseteq \mathbb{P} = \mathcal{P}(\bar{\Pi})$ and $A \subseteq \mathbb{P}$. Then $(\bigvee \mathfrak{B}) | A \subseteq \bigvee \{B | A | B \in \mathfrak{B}\} = ((\bigcup \mathfrak{B})|A)^{\perp\perp}$. ▶

**Proof.** Let us consider $(P, e) \in \bigvee \mathfrak{B}$, $(Q, f) \in A$ and $(H, h) \in ((\bigcup \mathfrak{B})|A)^\perp$. It suffices to prove that $\bar{\nu}(P|Q|H, efh) \in \perp$. By the hypothesis that $(P, e) \in \bigvee \mathfrak{B} = (\bigcup \mathfrak{B})^{\perp\perp}$ it suffices to prove that $(Q|H, fh) \in (\bigcup \mathfrak{B})^\perp$. Let us consider that $(R, r) \in \bigcup \mathfrak{B}$. Then, it suffices to prove that $\bar{\nu}(H|R|Q, hrq) \in \perp$. This sentence is true because $(R|Q, rf) \in (\bigcup \mathfrak{B})|A$ and $(H, h) \in ((\bigcup \mathfrak{B})|A)^\perp$. ◀

**Proposition 46.** Consider the CS $(\mathbb{B}, \otimes, (\cdot)^\perp, 1, \subseteq)$ of behaviors over $\bar{\Pi}$.

1. The operation $\| \|$ (from Definition 35) is a composition over $\mathbb{B}$, the equivalence $\equiv_\|$ is equality and its right adjoint is $B \triangleright_\| C := (B \| C^\perp)^\perp$.

2. The operation $\otimes$ (from Definition 35) is a composition over $\mathbb{B}$ and its right adjoint is $B \triangleright \otimes C := (((B^2 \| C^\perp)^\perp)|_{\mathbb{N}^1})^{-1}$.
**Proof.**

1. Since $(\bar{\Pi}, |, \mathbf{1})$ is an commutative monoid, then $(\mathfrak{B}, \|, \mathbf{1})$ is also an commutative monoid with
unite $\mathbf{1} := \{\mathbf{1}\}^{\perp\perp}$. By definition, $\|$ is an increasing function. Observe that $(\sqrt{\mathfrak{B}})|A \subseteq
\sqrt{\{B\|A \mid B \in \mathfrak{B}\}}$ for all $\mathfrak{B} \subseteq \mathbb{B}$ and $A \in \mathbb{B}$ by Lemma 74. The continuity in the right
argument is proven symmetrically. On the other hand, $A\|B \subseteq C \Leftrightarrow C^{\perp} \subseteq (A\|B)^{\perp}$, which
is equivalent to $\forall p \in A, q \in B, r \in C^{\perp} \quad \bar{\nu}(p \mid q \mid r) \in \perp$. The last condition is equivalent to
$A \subseteq (B\|C^{\perp})^{\perp}$, which proves that $B \triangleright_{\|} C := (B\|C^{\perp})^{\perp}$ is the right adjoint of $\|$.

2. We have $(\sqrt{\mathfrak{B}}) \otimes A = \sqrt{\{B \otimes A \mid B \in \mathfrak{B}\}}$ and $A \otimes (\sqrt{\mathfrak{B}}) = \sqrt{\{A \otimes B \mid B \in \mathfrak{B}\}}$ by Definition 1. By definition, $\otimes$ is an increasing function. On the other hand, $A \otimes B \subseteq C \Leftrightarrow C^{\perp} \subseteq (A \otimes B)^{\perp}$, which is equivalent to $\forall p \in A, q \in B, r \in C^{\perp} \quad \bar{\nu}(p^1 \mid q^2 \mid r) \in \perp$. The last condition is equivalent to $A^1 \subseteq ((B^2 \mid C^{\perp})^{\perp})_{\upharpoonright N^1} \Leftrightarrow A \subseteq (((B^2 \mid C^{\perp})^{\perp})_{\upharpoonright N^1})^{-1}$, which proves that $B \triangleright_{\otimes} C := (((B^2 \mid C^{\perp})^{\perp})_{\upharpoonright N^1})^{-1}$ is the right adjoint of $\otimes$. $\quad \blacksquare$

**F Embedding π-calculus through Honda & Yoshida combinators**

**Definition 75.** Let us consider a pole $\perp \subseteq \bar{\Pi}$. We say that $\perp$ is regular iff for all $(P, e), (Q, f)$ (PGF)-processes and names $u, \vec{x}$, $\{(P \mid Q, ef)\}^{\perp} \subseteq \{(\bar{u} \langle \vec{x} \rangle .P \mid v(\vec{x}).Q, ef)\}^{\perp}$ whenever $u \sim_{ef} v$.

The Honda-Yoshida combinators are also encoded into PGF by usual π-calculus (pure)
processes:

**Definition 76.** Let us define the following processes:

<figure><img src="image_20.png" /></figure>

► **Remark 77.** Let us consider a regular pole $\perp$. Then for all names $a, b, c, d, x$ we have:

<figure><img src="image_21.png" /></figure>

**Proposition 51.** A CIMA of behaviours $(\mathfrak{B}, \ll, \otimes, \|, (\cdot)^{\perp}, 1, S_{\mathfrak{B}})$ induced by a regular pole $\perp$
is a HYA with the definition $M(a, b) \triangleq \{(\bar{a} \langle b \rangle . \mathbf{1}, \Delta_{\mathbb{N}})\}^{\perp\perp}$.

**Proof.** By definition, $M(a, b) \in S$ because is not empty. The other combinators $K(a)$, $F(a, b)$, $Bl(a, b)$, $Br(a, b)$, $D(a, b, c)$ and $S(a, b, c)$ are given by Definition 49 and they are inhabited by their respective encoding on (PGF). For instance: By the Remark 77 we have $\{\mathbf{1}\}^{\perp} \subseteq \{k(a) \mid m(a, x)\}^{\perp} = (\{k(a)\}^{\perp\perp} \mid M(a, x))^{\perp} = (\{k(a)\}^{\perp\perp} \parallel M(a, x))^{\perp}$. Applying the orthogonal map we get: $\{k(a)\}^{\perp\perp} \parallel M(a, x) \subseteq \{\mathbf{1}\}^{\perp\perp} =: 1$.

By Proposition 45 we deduce that {$k(a)$}^{⊥⊥} ⊆ M(a, x) ▷ 1 for all a, b, x. Taking the meet on x we get k(a) ∈ {$k(a)$}^{⊥⊥} ⊆ ⋀_{x∈N} (M(a, x) ▷ 1) = K(a) and thus k(a) ∈ K(a).

For $d(a, b, c)$ the reasoning is almost the same: By Remark 77 we have $\{m(b, x) | m(c, x)\}^{\perp} \subseteq \{d(a, b, c) | m(a, x)\}^{\perp}$. This inclusion can be rewritten as $(M(b, x) || M(c, x))^{\perp} \subseteq$
($\{d(a, b, c)\}^{\perp\perp} \parallel M(a, x)$) $^{\perp}$. Applying the orthogonal map we get $\{d(a, b, c)\}^{\perp\perp} \parallel M(a, x) \subseteq M(b, x) \parallel M(c, x)$ for all names $a, b, c, x$, which is equivalent to $\{d(a, b, c)\}^{\perp\perp} \subseteq M(a, x) \triangleright (M(b, x) \parallel M(c, x))$. Again taking the meet on $x$ we conclude that $d(a, b, c) \in D(a, b, c)$. For the rest of the combiners the proof is entirely analogous.

◀

**G Parallelism cannot be derived**

We give here detailed proof for the results given in of Section 6. First, as was noticed by Munch-Maccagnoni [17], we can characterize realizers as follows:

► **Proposition 78.** For any formula $A$, $t \Vdash A$ iff $\forall u.(u \Vdash A^{\perp} \Rightarrow \langle t \parallel u \rangle \in \perp)$.

**Proof.** This is a direct consequence of the observation that $|A^{\perp}| = |A|^{\perp}$.

The following lemma, which is barely more than a simple observation, describe on realizers for the implication.

► **Lemma 79.** For any closed formulas with parameters $A, B$, we have: $t \Vdash A \dashrightarrow B$ iff for any $u \Vdash A, v \Vdash B^{\perp}, \langle t \parallel (u, v) \rangle \in \perp$.

**Proof.** By definition, we have:

$$ 
\begin{align*}
|A \dashrightarrow B| &= |(A \otimes B^{\perp})^{\perp}| \\
&= |(A \otimes B^{\perp})|^{\perp} \\
&= \{(u, v) : u \in |A| \wedge v \in |B^{\perp}|\}^{\perp \perp} \\
&= \{(u, v) : u \in |A| \wedge v \in |B^{\perp}|\}^{\perp}
\end{align*}
$$

Hence the result.

Finally, to simplify the proofs below, let us recall that terms of the $\lambda$-calculus can be encoded in $L$ using the following shorthands:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
A \dashrightarrow B & \triangleq & A^{\perp} \mathcal{R} B \\
u \cdot e & \triangleq & (u, e)
\end{array}
\quad
\left|
\begin{array}{l@{\qquad}l@{\qquad}l}
\lambda\kappa.t & \triangleq & \mu(\kappa, \kappa').\langle t \parallel (\kappa, \kappa') \rangle & \kappa' \notin \mathrm{FV}(t) \\
tu & \triangleq & \mu\kappa.\langle t \parallel u \cdot \kappa \rangle & \kappa \notin \mathrm{FV}(t, u)
\end{array}
\right.
$$

These shorthands are sound with respect to computation (in the sense that the $\beta$-reduction of the $\lambda$-calculus is simulated, with an evaluation strategy dictated by the polarities of $A$ and $B$ (call-by-name corresponds to both formulas being negative, while call-by-value corresponds to both being positive)) but also to types. Indeed, one can show that the following rules are admissible$^4$:

$$ \frac{\vdash t : B \mid \kappa : A^{\perp}, \Gamma \qquad (\text{abs})}{\vdash \lambda\kappa.t : A \dashrightarrow B \mid \Gamma} \qquad \frac{\vdash t : A \dashrightarrow B \mid \Gamma \qquad (\text{app})}{\vdash tu : B \mid \Gamma} $$

► **Proposition 54.** The tuple $(H, \subseteq, \otimes, (\cdot)^{\perp}, 1, S)$, where $1 \triangleq T_+^0$ and $S = H \setminus \emptyset$, is a CIMA.

**Proof.** We first show that $(H, \subseteq, \otimes, (\cdot)^{\perp})$ is a conjunctive structure.

■ The set of behaviors, ordered by inclusion, defines a complete lattice whose join is given by the union.

<footnote>$^4$ They are in fact derivable up to weakening.</footnote>
■ The map $\cdot \otimes \cdot$ is clearly covariant in its two arguments.

■ Similarly, it is clear that $(\cdot)^\perp$ is anti-monotonic.

■ As is usual with orthogonality relations, we have that for any $U \subset T_+^0$ (resp. $T_-^0$):

$$ (\bigcup_{T \in U} T)^\perp = \bigcap_{T \in U} T^\perp $$

Observing that if for any set $U \subset T^0$ such that $U \cap T_+^0 \neq \emptyset$ and $U \cap T_-^0 \neq \emptyset$ we have

$$ \begin{align*} (\bigcup_{T \in U} T)^\perp &= (\bigcup_{T_+ \in U \cap T_+} T_+ \cup \bigcup_{T_- \in U \cap T_-} T_-)^\perp \\ &= (\bigcup_{T_+ \in U \cap T_+} T_+)^\perp \cap (\bigcup_{T_- \in U \cap T_-} T_-)^\perp \\ &= \bigcap_{T_+ \in U \cap T_+} T_+^\perp \cap \bigcap_{T_- \in U \cap T_-} T_-^\perp = \bigcap_{T \in U} T^\perp \end{align*} $$

(In fact, all these sets are empty since $T_+ \cap T_- = \emptyset$)

■ The map $(\cdot)^\perp$ is by definition (of $\mathbf{H}$) involutive on $\mathbf{H}$.

We can now prove that, when considering the unit $1 \triangleq T_+^0$ (which is indeed a behavior), the set of non-empty behaviors $S = \mathbf{H} \setminus \emptyset$ defines a valid separator. This mostly amounts to finding a realizer for each of the different axioms.

■ $S$ is clearly upwards-closed.

■ $S$ is compatible with modus ponens. Indeed, if $A, B \in \mathbf{H}$ are such that $A \dashv B \in S$ and $A \in S$, by definition of $S$ it means that there exists two terms $t$ and $u$ such that $t \in A \dashv B$ and $u \in A$. Then $t u = \mu\kappa.\langle t \parallel (u, \alpha) \rangle \vdash B$, using the typing rule for application above and Proposition 53.

■ $\mu(x, \alpha).\langle x \parallel \mu(\kappa_1, \kappa_2).\langle (\kappa_2, \kappa_1) \parallel \alpha \rangle \rangle \vdash (A \otimes B) \dashv (B \otimes A)$

■ $\lambda\alpha.\mu(x, \beta).\langle x \parallel \mu(\kappa, \kappa').\langle (\alpha \kappa, \kappa') \parallel \beta \rangle \rangle \vdash (A \dashv B) \dashv (A \otimes C) \dashv (B \otimes C)$

■ $\mu(x, \alpha).\langle x \parallel \mu(y, \kappa_3).\langle y \parallel \mu(\kappa_1, \kappa_2).\langle (\kappa_1, (\kappa_2, \kappa_3)) \parallel \alpha \rangle \rangle \rangle \vdash ((A \otimes B) \otimes C) \dashv (A \otimes (B \otimes C))$

■ For any $t \in T_+^0$, $\lambda\kappa.(t_+, \kappa) \vdash A \dashv 1 \otimes A$

■ $\mu(x, \kappa).\langle x \parallel \mu(\_, \kappa').\langle \kappa' \parallel \kappa \rangle \rangle \vdash 1 \otimes A \dashv A$

■ $\mu(x, \alpha).\langle x \parallel \mu(\kappa, \kappa').\langle (\kappa, \kappa') \parallel \alpha \rangle \rangle \vdash (A \dashv B) \dashv (B^\perp \dashv A^\perp)$

For each of the last terms, it suffices to check that they have the corresponding type and then use adequacy (cf. Proposition 53). ▼