A Categorical Model of an $\mathbf {i/o}$-typed $\pi$-calculus

Abstract

This paper introduces a new categorical structure that is a model of a variant of the $\mathbf {i/o}$-typed $\pi$-calculus, in the same way that a cartesian closed category is a model of the $\lambda$-calculus. To the best of our knowledge, no categorical model has been given for the $\mathbf {i/o}$-typed $\pi$-calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate the relevance of the categorical model, we show by a semantic consideration that the $\pi$-calculus is equivalent to a core calculus of Concurrent ML.

1 Introduction

The Curry-Howard-Lambek correspondence reveals the trinity of the simply-typed $\lambda$-calculus, propositional intuitionistic logic and cartesian closed category. Via the correspondence, a type of the calculus can be seen as a formula of the logic, and as an object of a category; a term can be seen as a proof and as a morphism (see, e.g., [23]). Since its discovery, a number of variations have been proposed and studied.

In concurrency theory, a correspondence between a process calculus and logic was established by Caires, Pfenning and Toninho [8, 9] and later by Wadler [48]. What they found is that session types [18, 20] can be seen as formulas of linear logic [14], and processes as proofs. This remarkable result has inspired lots of work (e.g. [3, 4, 10, 25, 45, 46]).

This correspondence is, however, not completely satisfactory as pointed out in [3, 26], as well as by Wadler himself [48]. The session-typed calculi in [9, 48] corresponding to linear logic have only well-behaved processes, because the session type systems guarantee deadlock-freedom and race-freedom of well-typed processes. This strong guarantee is often useful for programmers writing processes in the typed calculus, but can be seen as a significant limitation of expressive power. For example, it prevents us from modelling wild concurrent systems or programs that might fall into deadlocks or race conditions.

This paper describes an approach to a Curry-Howard-Lambek correspondence for concurrency in the presence of deadlocks and race conditions, from the viewpoint of categorical type theory.

What Is the Categorical Model of the $\varvec{\pi }$-calculus? We focus on the $\pi$-calculus [30, 31] in this paper. This is not only because the $\pi$-calculus is widely used and powerful, but also because of a classical result by Sangiorgi [39, 42], which is the starting point of our development.

Sangiorgi, in the early 90s, gave translations between the conventional, first-order $\pi$-calculus and its higher-order variant [39, 42]. This translation allows us to regard the $\pi$-calculus as a higher-order programming language.

Let us review the observation by Sangiorgi, using a core of the asynchronous $\pi$-calculus: .¹ The idea is to decompose the input-prefixing $a(x).P$ into $a$ and $(x).P$. Let us write $a[(x).P]$ for $a(x).P$ to emphasise the decomposition. Then a reduction can also be decomposed as

$$ \bar{a}\langle x \rangle \mid a[(y).P] \mid Q \;\longrightarrow \; [(y).P]\langle x \rangle \mid Q \;\longrightarrow \; P\{x/y\} \mid Q, $$

where the first step is the communication and the second step is the $\beta$-reduction (i.e. $(\lambda y.P)\,x \longrightarrow P\{x/y\}$ in the $\lambda$-calculus notation). Hence we regard

• an output $\bar{a} \langle x \rangle$ as an application of a function $\bar{a}$ to x, and

• an input a(x).P as an abstraction $(x).P$ (or $\lambda x.P$) “located” at $a[{-}]$.

Now, ignoring the mysterious operator $a[{-}]$, what we had are the core operations of functional programming languages (i.e. abstraction and application). This functional programming language is effectful; in fact, communication via channels is a side effect.

This observation leads us to base our categorical model for the $\pi$-calculus on a model for effectful functional programs. Among several models, we choose closed Freyd category [37] for modelling the functional part.

Then what is the categorical counterpart of $a[{-}]$? As this operation seems responsible for communication, this question can be rephrased as: what is the categorical structure for communication? An observation by Abramsky et al. [2] answered this question. They pointed out the importance of compact closed category [21] in concurrency theory, which nicely describes CCS-like processes interconnected via ports.

By combining the two structures described above, this paper introduces a categorical structure, which we call compact closed Freyd category, as a categorical model of the $\pi$-calculus.² Despite its simplicity, compact closed Freyd category captures the strong expressive power of the $\pi$-calculus. The compact closed structure allows us to connect ports in an arbitrary way, in return for the possibility of deadlocks; the Freyd structure allows us to duplicate objects, and duplication of input channels introduces the possibility of race conditions.

Reconstructing Calculi. This paper introduces two calculi that are sound and complete with respect to the compact closed Freyd category model. One is a variant of the $\pi$-calculus, named $\pi _F$; the design of $\pi _F$ is based on the observations described above. The other is a higher-order programming language $\lambda _{ ch }$ defined as an instance of the computational $\lambda$-calculus [33]. Designing $\lambda _{ ch }$ is not so difficult because we can make use of the correspondence between computational $\lambda$-calculus and closed Freyd category (see Sect. 4). The $\lambda _{ ch }$-calculus have operations for creating a channel and for sending a value via the channel and, therefore, can be seen as a core calculus of Concurrent ML (or CML) [38].

Since the higher-order calculus $\lambda _{ ch }$ and $\pi _F$ correspond to the same categorical model, we can obtain translations between these calculi by simple semantic computations. These translations are “correct by definition” and, interestingly, coincide with those between higher-order and first-order $\pi$-calculus [39, 42].

On $\varvec{\beta }$- vs. $\varvec{\beta \eta }$-theories. The categorical analysis of this paper reveals that many conventional behavioural equivalences for the $\pi$-calculus are problematic from a viewpoint of categorical type theory. The problem is that they induce only semicategories, which may not have identities for some objects. This is a reminiscent of the $\beta$-theory of the $\lambda$-calculus, of which categorical model is given by semi-categorical notions [16].

Adding a single rule (which we call the $\eta$-rule) resolves the problem. Our categorical type theory deals with only equivalences that admits the $\eta$-rule, and the simplicity of the theory of this paper essentially relies on the $\eta$-rule.

Interestingly the $\eta$-rule seems to explain some phenomenon in the literature. For example, Sangiorgi observed that a syntactic constraint called locality [28, 49] is essential for his translation [39, 42]. The correctness of the translation can be proved without using the $\eta$-rule, when one restricts the calculus local; we expect that Sangiorgi’s observation can be related to this phenomenon.

Contributions. This paper introduces a new variant of the $\mathbf {i/o}$-typed $\pi$-calculus, which we call $\pi _F$. A remarkable feature of $\pi _F$ is that it has a categorical counterpart, called compact closed Freyd category. The correspondence is fairly firm; the categorical semantics is sound and complete, and the term model is the classifying category. The relevance of the model is demonstrated by a semantic reconstruction of Sangiorgi’s translation [39, 42]. These results open a new frontier in the Curry-Howard-Lambek correspondence for concurrency; session-type is not the only base for a Curry-Howard-Lambek correspondence for $\pi$-calculi.

Organisation of this Paper. Section 2 introduces the calculus $\pi _F$ and discuss equivalences on processes. Section 3 gives the categorical semantics of $\pi _F$ and shows soundness and completeness. A connection to a higher-order programming language with channels is studied in Sect. 4. In Sect. 5, we (1) discuss how our work relates to linear logic and (2) present some ideas for how to extend the application range of our model. We discuss related work in Sect. 6 and conclude in Sect. 7. Omitted proofs, as well as detailed definitions, are available in the full version.

2 A Polyadic, Asynchronous $\pi$-calculus with $\mathbf {i/o}$-types

This section introduces a variant of $\pi$-calculus, named $\pi _F$. It is based on a fairly standard calculus, namely polyadic and asynchronous $\pi$-calculus with $\mathbf {i/o}$-types, but the details are carefully designed so that $\pi _F$ has a categorical model.

2.1 The $\pi _F$-calculus

This subsection defines the calculus $\pi _F$, which is based on an asynchronous variant of the polyadic $\pi$-calculus with $\mathbf {i/o}$-types in [35]. The aim of this subsection is to explain what are the differences from the conventional $\pi$-calculus. Although $\pi _F$ has some uncommon features, each of them was studied in the literature; see Related Work (Sect. 6) for related ideas and calculi.

Types. The set of types, ranged over by $S$ and $T$, is given by

The type $\mathbf {ch}^{o}[T_1, \dots , T_n]$ is for output channels sending $n$ arguments of types $T_1, \dots , T_n$. The type $\mathbf {ch}^{i}[T_1, \dots , T_n]$ is for input channels. The dual $T^{\bot }$ of type $T$ is defined by and . For a sequence of types, we write $\vec {T}^{\bot }$ for $T_1^{\bot }, \dots , T_n^{\bot }$.

An important difference from [35] is that no channel allows both input and output operations. We will refer this feature of $\pi _F$ as $\mathbf {i/o}$-separation.

Processes. Let $\mathcal {N}$ be a denumerable set of names, ranged over by $x$, $y$ and $z$. Each name is either input-only or output-only, because of $\mathbf {i/o}$-separation.

The set of processes, ranged over by $P$, $Q$ and $R$, is defined by

The notion of free names, as well as bound names, is defined as usual. The set of free names (resp. bound names) of $P$ is written as $\mathbf {fn}(P)$ (resp. $\mathbf {bn}(P)$). We allow tacit renaming of bound names, and identify $\alpha$-equivalent processes.

The meaning of the constructs should be clear, except for $(\varvec{\nu }_{T}\,x y) P$ which is less common. The process $\mathbf {0}$ is the inaction; $P \mid Q$ is a parallel composition; $x \langle \vec {y} \rangle$ is an output; and ${!} x (\vec {x}). P$ is a replicated input. The restriction $(\varvec{\nu }_{T}\,x y)P$ hides the names $x$ and $y$ of type $T$ and $T^{\bot }$ and, at the same time, establishes a connection between $x$ and $y$. Communication takes place only over bound names explicitly connected by $\varvec{\nu }$. This is in contrast to the conventional $\pi$-calculus, in which input-output correspondence is a priori (i.e. $\bar{a}$ is the output to $a$).

The $\pi _F$-calculus does not have non-replicated input $x(\vec {y}).P$.

Typing Rules. A type environment $\varGamma$ is a finite sequence of type bindings of the form $x :T$. We assume the names in $\varGamma$ are pairwise distinct. If $\vec {x}= x_1,\dots ,x_n$ and $\vec {T}= T_1,\dots ,T_n$, we write $\vec {x}:\vec {T}$ for $x_1 :T_1, \dots , x_n :T_n$. We write $(\vec {x}:\vec {T}) \subseteq \varGamma$ to mean $x_i :T_i \in \varGamma$ for every $i$.

A type judgement is of the form $\varGamma \vdash P : \diamond$, meaning that $P$ is a well-typed process under $\varGamma$. The typing rules are listed in Fig. 1.

Fig. 1.

Typing rules for processes

Notation 1

We define $(\varvec{\nu }_{\mathbf {ch}^{i}[\vec {T}]}\,x y)P$ as $(\varvec{\nu }_{\mathbf {ch}^{o}[\vec {T}]}\,y x)P$; then $(\varvec{\nu }_{T}\,x y)P$ is defined for every $T$. We abbreviate $(\varvec{\nu }_{T_1}\,x_1 y_1) \dots (\varvec{\nu }_{T_n}\,x_n y_n)P$ as $(\varvec{\nu }_{\vec {T}}\,\vec {x} \vec {y})P$. We often omit type annotations and write $(\varvec{\nu } x y)$ for $(\varvec{\nu }_{T}\,x y)$ and $(\varvec{\nu } \vec {x} \vec {y})$ for $(\varvec{\nu }_{\vec {T}}\,\vec {x} \vec {y})$. We use $a$ and $b$ for names of input channel types and $\bar{a}$ and $\bar{b}$ for output. Note that $a$ and $\bar{a}$ are connected only if they are bound by the same occurrence of $\varvec{\nu }$.    $\square$

Operational Semantics. Structural congruence, written $\equiv$, is the smallest congruence relation on processes that satisfies the following rules:

$$ \begin{array}{c} P \mid \mathbf {0}\equiv P \qquad P \mid Q \equiv Q \mid P \qquad (P \mid Q) \mid R \equiv P \mid (Q \mid R) \\[3pt] (\varvec{\nu } x y)(P \mid Q) \equiv ((\varvec{\nu } x y)P) \mid Q \qquad (\varvec{\nu } w x)(\varvec{\nu } y z)P \equiv (\varvec{\nu } y z)(\varvec{\nu } w x)P \end{array} $$

where $x, y \notin \mathbf {fn}(Q)$ in the fourth rule and $w, x, y, z$ are distinct in the fifth rule.

The reduction relation on processes, written $\longrightarrow$, is defined by the base rule

$$ (\varvec{\nu } \vec {w} \vec {z})(\varvec{\nu } \bar{a} a)({{!} a (\vec {x}). P} \mid \bar{a} \langle \vec {y} \rangle \mid Q) \longrightarrow (\varvec{\nu } \vec {w} \vec {z})(\varvec{\nu } \bar{a} a)({{!} a (\vec {x}). P} \mid P \{\vec {y} / \vec {x}\} \mid Q) $$

(where $P\{\vec {x}/\vec {y}\}$ is the capture-avoiding substitution) and the structural rule which concludes $P \longrightarrow Q$ from $\exists P'\,Q'.\,P \equiv P' \longrightarrow Q' \equiv Q$. Note that, unlike conventional $\pi$-calculi, communication only occurs over bound names connected by $\nu$. We write $\longrightarrow ^*$ for the reflexive and transitive closure of $\longrightarrow$.

It should be clear that deadlocks and racy communications can be expressed in $\pi _F$. An example of race is $(\varvec{\nu } \bar{a} a)(\bar{a} \langle \vec {y} \rangle \mid {!} a (\vec {x}). P \mid {!} a (\vec {x}). Q)$, where two input actions are trying to consume the output regarded as a resource. A similar process $(\varvec{\nu } \bar{a} a)({!} a (\vec {x}). P \!\mid \!\bar{a}\langle \vec {y} \rangle \mid \bar{a}\langle \vec {z} \rangle )$ does not have a race since the receiver ${!} a (\vec {x}). P$ is replicated. In general, race conditions on output actions do not occur in $\pi _F$.

2.2 Equivalences on Processes

To establish a Curry-Howard-Lambek correspondence is to find a nice algebraic or categorical structure of terms. For example, the original Curry-Howard-Lambek correspondence reveals the cartesian closed structure of $\lambda$-terms.

Such a nice structure would become visible only when appropriate notions of composition and of equivalence could be identified, such as substitution and $\beta \eta$-equivalence for the $\lambda$-calculus.

As for process calculi, so-called “parallel composition + hiding” paradigm [17] has been used to compose processes. Given typed processes

$$ \vec {x}: \vec {T},\; \vec {y}: \vec {S}\vdash P : \diamond \quad \text{ and }\quad \vec {w}: \vec {S}^{\bot },\; \vec {u} : \vec {U} \vdash Q : \diamond , $$

their composite via $(\vec {y}, \vec {w})$ is defined as

$$ \vec {x}: \vec {T},\; \vec {u} : \vec {U} \vdash (\varvec{\nu }_{\vec {S}}\,\vec {y} \vec {w})(P \mid Q) : \diamond . $$

This kind of composition appears quite often in logical studies of $\pi$-calculi [1, 5, 19]. It also plays a central role in interaction category paradigm proposed by Abramsky, Gay and Nagarajan [2].

So it remains to determine an equivalence on $\pi$-calculus processes, appropriate for our purpose. This subsection approaches the problem from two directions:

• Examining behavioural equivalences proposed and studied in the literature

• Developing a new equivalence based on categorical considerations

Let us clarify the notion of equivalence discussed below. An equation-in-context is a judgement of the form $\varGamma \vdash P = Q$, where $\varGamma \vdash P : \diamond$ and $\varGamma \vdash Q : \diamond$. An equivalence $\mathcal {E}$ is a set of equations-in-context that is reflexive, transitive and symmetric (e.g. $(\varGamma \vdash P=P) \in \mathcal {E}$ for every $\varGamma \vdash P : \diamond$).

Behavioural Equivalences. As mentioned above, we are interested in the structure of $\pi _F$-processes modulo existing behavioural equivalences. Among the various behavioural equivalence, we start with studying barbed congruence [32], which is one of the most widely used equivalences.

We define (asynchronous and weak) barbed congruence for $\pi _F$. For each name $\bar{a}$, we write $P{\downarrow _{\bar{a}}}$ if $P \equiv (\varvec{\nu } \vec {x} \vec {y})(\bar{a} \langle \vec {z} \rangle \mid Q)$ and $\bar{a}$ is free, and $P{\Downarrow _{\bar{a}}}$ if $\exists Q.\, P \longrightarrow ^* Q {\downarrow _{\bar{a}}}$. A $(\varGamma /\varDelta )$-context is a context $C$ such that $\varGamma \vdash C[P] : \diamond$ for every $\varDelta \vdash P : \diamond$.

Definition 1

A barbed bisimulation is a symmetric relation $\mathrel {\mathcal {R}}$ on processes such that, whenever $P \mathrel {\mathcal {R}}Q$, (1) $P{\downarrow _{\bar{a}}}$ implies $Q{\Downarrow _{\bar{a}}}$ and (2) $P \longrightarrow P'$ implies $\exists Q'.\, (Q \longrightarrow ^* Q') \wedge (P' \mathrel {\mathcal {R}}Q')$. Barbed bisimilarity $\mathrel {{\mathop {\approx }\limits ^{\bullet }}}$ is the largest barbed bisimulation. Typed processes $\varDelta \vdash P : \diamond$ and $\varDelta \vdash Q : \diamond$ are barbed congruent at $\varDelta$, written $\varDelta \vdash P \mathrel {\approxeq ^c}Q$, if $C[P] \mathrel {{\mathop {\approx }\limits ^{\bullet }}}C[Q]$ for every $(\varGamma /\varDelta )$-context $C$.    $\square$

Let us consider a category-like structure $\mathcal {C}$ in which an object is a type and a morphism is an equivalence class of $\pi _F$-processes modulo barbed congruence. More precisely, a morphism from $T$ to $S$ is a process $x :T,\, y:S^{\bot } \vdash P:\diamond$ modulo barbed congruence (and renaming of free names $x$ and $y$). Then the composition (i.e. “parallel composition + hiding”) is well-defined on equivalence classes, because barbed congruence is a congruence. This is a fairly natural setting.

We have a strikingly negative result.

Theorem 1

$\mathcal {C}$ is not a category.

Proof

In every category, if $f : A \longrightarrow A$ is a left-identity on $A$ (i.e. $f \circ g = g$ for every $g : A \longrightarrow A$), then $f$ is the identity on $A$. The process $a : \mathbf {ch}^{o}[], \bar{b}: \mathbf {ch}^{i}[] \vdash {!} a (). \bar{b} \langle \rangle : \diamond$ seen as a morphism $(\mathbf {ch}^{o}[]) \longrightarrow (\mathbf {ch}^{o}[])$ is a left-identity but not the identity. The former means that $c :\mathbf {ch}^{o}[], \, \bar{b}:\mathbf {ch}^{i}[] \,\vdash \, \left( (\varvec{\nu } \bar{a} a) ({!} a (). \bar{b} \langle \rangle \mid P)\right) \,\mathrel {\approxeq ^c}\, P\{\bar{b}/\bar{a}\}$ for every $c :\mathbf {ch}^{o}[],\, \bar{a}:\mathbf {ch}^{i}[] \vdash P :\diamond$, which is a consequence of the replicator theorems [35]. To prove the latter, observe that $(\varvec{\nu } \bar{b} b)({!} a (). \bar{b} \langle \rangle \mid \mathbf {0})$ and $\mathbf {0}$ are not barbed congruent. Indeed the context distinguishes the processes, where $\bar{o}$ is the observable.    $\square$

Note that race condition is essential for the proof, specifically, for the part proving that the process ${!} a (). \bar{b} \langle \rangle$ is not the identity. A race condition occurs in $C[(\varvec{\nu } \bar{b} b)({!} a (). \bar{b} \langle \rangle \mid \mathbf {0})]$, where $\bar{a}$ in $C$ has two receivers.

The process ${!} a (). \bar{b} \langle \rangle$ is called forwarder, and forwarders will play a central role in this paper. Its general form is . When $x : T$ and $y : T^{\bot }$, we write ${x \leftrightharpoons y}$ to mean ${x \hookrightarrow y}$ if $T = \mathbf {ch}^{i}[\vec {S}]$ and otherwise ${y \hookrightarrow x}$.

Remark 1

The argument in the proof of Theorem 1 is widely applicable to $\mathbf {i/o}$-typed calculi, not specific to $\pi _F$. In particular, $\mathbf {i/o}$-separation (i.e. absence of $\mathbf {ch}^{i/o}[\vec {T}]$) is not the cause, but the existence of $\mathbf {ch}^{o}[\vec {T}]$ or $\mathbf {ch}^{i}[\vec {T}]$ is.    $\square$

Remark 2

Session-typed calculi in Caires, Pfenning and Toninho [8, 9], which correspond to linear logic, do not seem to suffer from this problem. In our understanding, this is because of race-freedom of their calculi.    $\square$

To obtain a category, we should think of a coarser equivalence that identifies $(\varvec{\nu } \bar{b} b)({!} a (). \bar{b} \langle \rangle \mid \mathbf {0})$ with $\mathbf {0}$. Such an equivalence should be very coarse; even must-testing equivalence [11] fails to equate them. As long as we have checked, only may-testing equivalence [11] defined below satisfies the requirement.

Definition 2

Typed processes $\varDelta \vdash P : \diamond$ and $\varDelta \vdash Q : \diamond$ are may-testing equivalent at $\varDelta$, written $\varDelta \vdash P \mathrel {=_{ may }}Q$, if $C[P] {\Downarrow _{\bar{a}}} \Leftrightarrow C[Q]{\Downarrow _{\bar{a}}}$ for every $(\varGamma /\varDelta )$-context $C$ and name $\bar{a}$.    $\square$

As we shall see, $\pi _F$-processes modulo may-testing equivalence behaves well. May-testing equivalence is, however, often too coarse.

Category-Driven Approach. In this approach, we first guess an appropriate categorical structure sufficient for interpreting $\pi _F$, based on intuitions discussed in Introduction (see also Sect. 3.1), and then design an equivalence so that it is sound and complete with respect to the categorical semantics.

Figure 2 defines the equivalence, described as a set of rules. A $\pi _F$-theory is an equivalence that behaves well from the categorical perspective.

Fig. 2.

Inference rules of equations-in-context. Each rule has implicit assumptions that the both sides of the equation are well-typed processes.

Definition 3

An equivalence $\mathcal {E}$ is a $\pi _F$-theory if it is closed under the rules in Fig. 2. Any set $Ax$ of equations-in-context has the minimum theory $Th ( Ax )$ that contains $Ax$. We write $Ax \rhd \varGamma \vdash P = Q$ if $(\varGamma \vdash P = Q) \in Th ( Ax )$.    $\square$

Let us examine each rule in Fig. 2.

The rule (E-Beta) should be compared with the reduction relation. When $C = ([\,]\mid Q)$, then (E-Beta) claims

$$ (\varvec{\nu } \bar{a} a)({!} a (\vec {x}). P \mid \bar{a} \langle \vec {y} \rangle \mid Q) = (\varvec{\nu } \bar{a} a)({!} a (\vec {x}). P \mid P \{\vec {y} / \vec {x}\} \mid Q) $$

provided that $a \notin \mathbf {fn}(P, Q)$, which is indeed an instance of the reduction.

A significant difference from reduction is the side condition. It is essential in the presence of race conditions. Without the side condition, every $\pi _F$-theory would be forced to contain the symmetric and transitive closure of the reduction relation; thus it would identify $P \mid (\varvec{\nu } \bar{a} a)({!} a (). P \mid {!} a (). Q)$ with $Q \mid (\varvec{\nu } \bar{a} a)({!} a (). P \mid {!} a (). Q)$ for every processes $P$ and $Q$ (where $\bar{a}, a$ are fresh), because

$$\begin{aligned} (\varvec{\nu } \bar{a} a) (\bar{a} \langle \rangle \mid {!} a (). P \mid {!} a (). Q)&\quad \longrightarrow \quad P \mid (\varvec{\nu } \bar{a} a)({!} a (). P \mid {!} a (). Q) \\ (\varvec{\nu } \bar{a} a) (\bar{a} \langle \rangle \mid {!} a (). P \mid {!} a (). Q)&\quad \longrightarrow \quad Q \mid (\varvec{\nu } \bar{a} a)({!} a (). P \mid {!} a (). Q). \end{aligned}$$

The side condition prevents $\pi _F$-theories from collapsing.

Another, relatively minor, difference is that application of (E-Beta) is not limited to the contexts of the form $[\,]\mid Q$. This kind of extension can be found in, for example, work by Honda and Laurent [19] studying $\pi$-calculus from a logical perspective.

The rule (E-GC) runs “garbage-collection”. Because no one can send a message to the hidden name $a$, the process ${!} a (\vec {x}). P$ will never be invoked and thus is safely discarded. This rule is sound with respect to many behavioural equivalences, including barbed congruence. Rules of this kind often appear in the literature studying logical aspects of concurrent calculi (as in Honda and Laurent [19] and Wadler [48]). There is, however, a subtle difference in the side condition: (E-GC) requires that $a$ and $\bar{a}$ do not appear at all in $P$.

The rule (E-FOut) can be seen as the $\eta$-rule of abstractions, as in the $\lambda$-calculus and in the higher-order $\pi$-calculus [39]. In the latter, an output name $\bar{b}$ can be identified with an abstraction $(\vec {y}).\bar{b} \langle \vec {y} \rangle$. Then we have, for example,

$$ (\varvec{\nu } \bar{a} a)({a \hookrightarrow \bar{b}} \mid \bar{c} \langle \bar{a} \rangle ) \;=\; (\varvec{\nu } \bar{a} a)({a \hookrightarrow \bar{b}} \mid \bar{c} \langle \,(\vec {y}).\bar{a} \langle \vec {y} \rangle \, \rangle ) \;=\; \bar{c} \langle \,(\vec {y}).\bar{b} \langle \vec {y} \rangle \, \rangle \;=\; \bar{c} \langle \bar{b} \rangle $$

where we use (E-Beta) and (E-GC) in the second step. An important usage of (E-FOut) is to replace an output of free names with that of bound names. This kind of operation has been studied in [7, 28] as a part of translations from the $\pi$-calculus to its local/internal fragments.³

The rule (E-Eta) requires the forwarders are left-identities, directly describing the requirement discussed above.⁴

The rules (E-SCong) and (E-Ctx) are easy to understand. The former requires that structurally congruent processes should be identified; the latter says that a $\pi _F$-theory is a congruence.

These rules can be justified from the operational viewpoint, as well. A well-known result on the $\mathbf {i/o}$-typed $\pi$-calculus (see, e.g., [35, 43]) shows the following propositions.

Proposition 1

Barbed congruence is closed under all rules but (E-Eta).    $\square$

Proposition 2

May-testing equivalence is a $\pi _F$-theory.    $\square$

In particular, the latter means that may-testing equivalence is in the scope of the categorical framework of this paper; see Theorem 5.

3 Categorical Semantics

This section introduces the class of compact closed Freyd categories and discusses the interpretation of the $\pi _F$-calculus in the categories. We show that the categorical semantics is sound and complete with respect to the equational theory given in Sect. 2.2, and that the syntax of the $\pi _F$-calculus induces a model.

This section, by its nature, is slightly theoretical compared with other sections. Section 3.1 explains the ideas of this section without heavily using categorical notions; the subsequent subsections require familiarity with categorical type theory.

3.1 Overview

As mentioned in Sect. 1, the categorical model of $\pi _F$ is compact closed Freyd category, which has both closed Freyd and compact closed structures. Here we informally discuss what is a compact closed Freyd category and how to interpret $\pi _F$ by using syntactic representation.

A closed Freyd category is a model of higher-order programs with side effects. It has, among others, the structures to interpret the function type $A \Rightarrow B$ and its constructor and destructor, namely, abstraction $\lambda x. t$ and application $t\,u$. It also has a mechanism for unrestricted duplication of variables; in terms of logic, contraction is admissible.

A compact closed category can be seen as MLL [14] with the left rule:

$$ \dfrac{ \varGamma , A^*, A \vdash I }{ \varGamma \vdash I } \qquad \left[ \dfrac{ \varGamma \vdash A^* \qquad \varDelta \vdash A }{ \varGamma , \varDelta \vdash I } \right] . $$

(The right rule is the companion, which itself is derivable in MLL.)

A compact closed Freyd category has all the constructs. It has the structures corresponding to the following type constructors:

$$\begin{aligned} \text{(closed } \text{ Freyd) }&\quad I, A \otimes B, A \Rightarrow B&\text{(compact } \text{ closed) }&\quad I, A \otimes B, A^*. \end{aligned}$$

Note that the pair type $A\,\otimes \, B$ (as well as the unit $I$) coming from the closed Freyd structure is identified with that from the compact closed structure. Inference rules for a compact closed Freyd category is those for functional languages and the above rules of the compact closed structure.

Interpreting $\pi _F$ in a compact closed Freyd category is to interpret it by using these constructs. As mentioned in Sect. 1, following Sangiorgi [39], we regard

• an output $\bar{a} \langle \vec {x} \rangle$ as an application of a function $\bar{a}$ to a tuple $\langle \vec {x}\rangle$, and

• an input ${!} a (\vec {x}). P$ as an abstraction $(\vec {x}).P$ (or $\lambda \vec {x}.P$) located at $a$.

We interpret the output action by using the function application. Hence the type $\mathbf {ch}^{o}[T]$ is regarded as a function type $T \Rightarrow I$ (where the unit type $I$ is the type for processes i.e. $\diamond$); then the typing rule for output actions becomes

The type $\mathbf {ch}^{i}[T]$ is understood as $(T \Rightarrow I)^*$; the input-prefixing rule becomes

This derivation directly expresses the intuition that an input-prefixing is abstraction followed by allocation; here allocation is interpreted by using the compact closed structure, i.e. connection of ports. The name restriction also has a natural derivation:

3.2 Compact Closed Freyd Category

Let us formalise the ideas given in Sect. 3.1. Hereafter in this section, we assume basic knowledge of category theory and of categorical type theory.

We recall the definitions of compact closed category and closed Freyd category. For simplicity, the structures below are strict and chosen; a functor is required to preserve the chosen structures on the nose.

Definition 4

(Compact closed category [21]). Let $(\mathcal {C}, \otimes , I)$ be a symmetric strict monoidal category. The dual of an object $A$ in $\mathcal {C}$ is an object $A^*$ equipped with unit $\eta _A :I \longrightarrow A \otimes A^*$ and counit $\epsilon _A :A^* \otimes A \longrightarrow I$ that satisfy the “triangle identities” $(\eta _A \otimes \mathrm {id}_A);(\mathrm {id}_A \otimes \epsilon _A) = \mathrm {id}_A$ and $(\mathrm {id}_{A^*} \otimes \eta _A); (\epsilon _A \otimes \mathrm {id}_{A^*}) = \mathrm {id}_{A^*}$. The category $\mathcal {C}$ is compact closed if each object is equipped with a chosen dual.    $\square$

Definition 5

(Closed Freyd category [37]). A Freyd category is given by (1) a category with chosen finite products $(\mathcal {C}, \otimes , I)$, called value category, (2) a symmetric strict monoidal category $(\mathcal {K}, \otimes , I, \mathbf {symm})$, called producer category, and (3) an identity-on-object strict symmetric monoidal functor $J:\mathcal {C}\rightarrow \mathcal {K}$. A Freyd category is a closed Freyd category if the functor $J({-}) \otimes A :\mathcal {C}\rightarrow \mathcal {K}$ has the (chosen) right adjoint $A \Rightarrow {-} :\mathcal {K}\rightarrow \mathcal {C}$ for every object A. We write $\varLambda _{A,B,C}$ for the natural bijection $\mathcal {K}(J(A) \otimes B, C) \longrightarrow \mathcal {C}(A, B \Rightarrow C)$ and $\mathbf {eval}_{A, B}$ for $\varLambda ^{-1}(\mathrm {id}_{A \Rightarrow B}) :{(A \Rightarrow B) \otimes A} \longrightarrow B$ in $\mathcal {K}$.    $\square$

Remark 3

The above definition is a restriction of the original one [37], in which $\mathcal {K}$ is a premonoidal [36] category. This change reflects concurrency of the calculus. In fact, it validates the following law, expressed by the syntax of the computational $\lambda$-calculus [33],

$$ \mathbf {let}\, {x} = {M}\, \mathbf {in}\,{\mathbf {let}\, {y} = {N}\, \mathbf {in}\,{L}} \quad = \quad \mathbf {let}\, {y} = {N}\, \mathbf {in}\,{\mathbf {let}\, {x} = {M}\, \mathbf {in}\,{L}}. $$

Then one can evaluate $M$ by using the left form and $N$ by using the right form. This law allows us to evaluate $M$ and $N$ in arbitrary order, or concurrently.    $\square$

We now introduce the categorical structure corresponding to the $\pi _F$-calculus.

Definition 6

(Compact closed Freyd category). A compact closed Freyd category is a Freyd category $J : \mathcal {C}\longrightarrow \mathcal {K}$ such that (1) $\mathcal {K}$ is compact closed, and (2) J has the (chosen) right adjoint $I \Rightarrow - :\mathcal {K}\rightarrow \mathcal {C}$.    $\square$

We shall often write $J$ for a compact closed Freyd category .

A compact closed Freyd category is a closed Freyd category:

$$ \mathcal {K}(J(A) \otimes B, C) \;\cong \; \mathcal {K}(J(A), B^* \otimes C) \;\cong \; \mathcal {C}(A, I \Rightarrow (B^* \otimes C)). $$

Example 1

The most basic example of a compact closed Freyd category is (the strict monoidal version of) . Here J is the identity-on-object functor that maps a function to its graph and $\mathcal {P}$ is the “power set functor” that maps a relation ${\mathrel {\mathcal {R}}} \subseteq A \times B$ to a function . Another example is obtained by replacing sets with posets, functions with monotone functions and relations with downward closed relations.    $\square$

Fig. 3.

Interpretation of types and processes. Here $!_{\varGamma }$, $\varDelta _\varGamma$ and $\pi ^{\varGamma }_y$ are maps in $\mathcal {C}$ induced by the cartesian structure, namely, $!_{\varGamma } :\llbracket \varGamma \rrbracket \longrightarrow I$ is the terminal map, $\varDelta _{\varGamma } :\llbracket \varGamma \rrbracket \longrightarrow \llbracket \varGamma \rrbracket \otimes \llbracket \varGamma \rrbracket$ is the diagonal map and, when $\varGamma = (y_1 :T_1, \dots , y_n :T_n)$ and $x = y_j$, the morphism $\pi ^{\varGamma }_{x} :\llbracket \varGamma \rrbracket \longrightarrow \llbracket T_j \rrbracket$ is the $j$-th projection. The interpretation of a type environment $x_1 :T_1, \dots , x_n :T_n$ is $\llbracket T_1 \rrbracket \otimes \cdots \otimes \llbracket T_n \rrbracket$.

Example 2

A more sophisticated example is taken from Laird’s game-semantic model of $\pi$-calculus [22]. Precisely speaking, the model in [22] itself is not compact closed Freyd, but its variant (with non-negative arenas) is. This model is important since it is fully abstract w.r.t. may-testing equivalence [22, Theorem 1]; hence our framework has a model that captures the may-testing equivalence.    $\square$

3.3 Interpretation

Given a compact closed Freyd category , this section defines the interpretation . It maps types and type environments to objects as usual, and a well-typed process $\varGamma \vdash P : \diamond$ to a morphism $\llbracket P \rrbracket :\llbracket \varGamma \rrbracket \rightarrow I$ in $\mathcal {K}$ (recall that the tensor unit $I$ is the interpretation of the type for processes).

Figure 3 defines the interpretation of types and processes. It simply formalises the ideas presented in Sect. 3.1: for example, the interpretation of ${!} a (\vec {x}). P$ is the abstraction $\varLambda$ (from the closed Freyd structure) followed by location $\epsilon$ (from the compact closed structure). There are some points worth noting.

• $(A \Rightarrow I)^*$ is not isomorphic to $A^* \Rightarrow I$, $A \Rightarrow I$ nor $I \Rightarrow A$. Indeed $(A \Rightarrow I)^*$ cannot be simplified. Do not confuse it with a valid law $I \Rightarrow (A^*) \cong A \Rightarrow I$.

• A parallel composition is interpreted as a pair. Recall that two components of a pair are evaluated in parallel in this setting (cf. Remark 3).

• All but the last rule use the cartesian structure of $\mathcal {C}$ in order to duplicate or discard the environment.

Example 3

Let us consider $y : T \vdash (\varvec{\nu } \bar{a} a)(\bar{a} \langle y \rangle \mid {!} a (x). P) : \diamond$, where $\bar{a}, a, y \notin \mathbf {fn}(P)$ and $a :\mathbf {ch}^{i}[T]$. By (E-Beta) and (E-GC), this process is equal to $P \{y / x\}$. It is natural to expect that the interpretations of the two processes coincide; indeed it is. As the following calculation indicates, our semantics factorises the reduction into two steps: (1) the “transmission” of the closure $\lambda \vec {x}.P$ by the triangle identity of the compact closed structure, and (2) the $\beta$-reduction modelled by $\mathbf {eval}$ of the closed Freyd structure:

(Here we implicitly use derived rules for weakening and exchange.)    $\square$

Example 4

The interpretation of a forwarder $a : \mathbf {ch}^{i}[\vec {T}], \bar{b}: \mathbf {ch}^{o}[\vec {T}] \vdash {a \hookrightarrow \bar{b}} : \diamond$ is the counit $\epsilon _{\mathbf {ch}^{o}[\vec {T}]} :\llbracket \mathbf {ch}^{o}[\vec {T}] \rrbracket ^* \otimes \llbracket \mathbf {ch}^{o}[\vec {T}] \rrbracket \longrightarrow I$ in $\mathcal {K}$, which is the one-sided form of the identity. Recall that a forwarder is the identity in every $\pi _F$-theory.    $\square$

The semantics is sound and complete. That means, a judgement $Ax \rhd \varGamma \vdash P = Q$ is provable if and only if $\varGamma \vdash P=Q$ is valid in all models $J$ of $Ax$.

Here we define the related notions and prove soundness; completeness is the topic of the next subsection.

Definition 7

An equational judgement $\varGamma \vdash P = Q$ is valid in $J$ if . Given a set $Ax$ of non-logical axioms, $J$ is a model of $Ax$, written $J \,\models \, Ax$, if it validates all judgements in $Ax$. We write $Ax \rhd \varGamma \Vdash P = Q$ if $\varGamma \vdash P = Q$ is valid in every $J$ such that $J \,\models \, Ax$.    $\square$

Theorem 2

(Soundness). If $Ax \rhd \varGamma \vdash P = Q$, then $Ax \rhd \varGamma \Vdash P = Q$.    $\square$

3.4 Term Model

A term model is a category whose objects are type environments and whose morphisms are terms (i.e. processes in this setting). This section gives a construction of the term model, by which we show completeness. This subsection basically follows the standard arguments in categorical type theory; we mainly focus on the features unique to our model, giving a sketch to the common part.

Given a set $Ax$ of axioms, we define the term model , which we also write as $Cl ( Ax )$.

The definition of the producer category $\mathcal {K}_{ Ax }$ follows the standard recipe. As usual, its objects are finite lists of types. The monoidal product $\vec {T}\otimes \vec {S}$ is the concatenation of the lists and the dual $\vec {T}^*$ is $\vec {T}^{\bot }$. Given objects $\vec {T}$ and $\vec {S}$, a morphism from $\vec {T}$ to $\vec {S}$ is a process $\vec {x}:\vec {T}, \, \vec {y}:\vec {S}^{\bot } \vdash P : \diamond$ (modulo renaming of variables $\vec {x}$ and $\vec {y}$). If $Ax \rhd \vec {x}:\vec {T}, \, \vec {y}:\vec {S}^{\bot } \vdash P = Q$ is provable, then $P$ and $Q$ are regarded as the same morphism. Composition of morphisms is defined as “parallel composition plus hiding”: For morphisms $P : \vec {T}\longrightarrow \vec {S}$ and $Q : \vec {S}\longrightarrow \vec {U}$, i.e. processes such that $\vec {x}:\vec {T},\; \vec {y}:\vec {S}^{\bot } \vdash P : \diamond$ and $\vec {z}:\vec {S},\; \vec {w} :\vec {U}^{\bot } \vdash Q : \diamond$, their composite is $\vec {x}:\vec {T}, \vec {w} :\vec {U}^{\bot } \vdash (\varvec{\nu } \vec {y} \vec {z}) (P \mid Q) : \diamond$. The monoidal product $P \otimes Q$ of morphisms is the parallel composition $P \mid Q$. The identity, as well as the symmetry of the monoidal product and the unit and counit of the compact closed structure, is a parallel composition of forwarders: for example, the identity on $\vec {S}$ is $\vec {x}: \vec {S},\, \vec {y}: \vec {S}^{\bot } \vdash {x_1 \leftrightharpoons y_1} \mid \dots \mid {x_n \leftrightharpoons y_n} : \diamond$ where $n$ is the length of $\vec {S}$. The facts that most structural morphisms are forwarders and that forwarders compose are the keys to show that $\mathcal {K}_{ Ax }$ is a compact closed category.

We then see the definition of $\mathcal {C}_{ Ax }$, of which the definition of morphisms has a subtle point. The objects of $\mathcal {C}_{ Ax }$ are by definition the same as $\mathcal {K}_{ Ax }$, i.e. lists of types. The definition of morphisms relies on the notion of values. The values are defined by the grammar , where $P$ is a process and $(\vec {x}).P$ is called an abstraction. Typing rules for values are as follows:

$$ \dfrac{ x : T \in \varGamma }{ \varGamma \vdash x : T } \qquad \dfrac{ \varGamma , \vec {x}:\vec {T}\vdash P }{ \varGamma \vdash (\vec {x}).P : \mathbf {ch}^{o}[\vec {T}] }. $$

(To understand the right rule, recall that $\llbracket \mathbf {ch}^{o}[\vec {T}] \rrbracket = \llbracket \vec {T} \rrbracket \Rightarrow I$.) A morphism from $\vec {T}$ to $\vec {S}= (S_1, \dots , S_n)$ is an $n$-tuple $(V_1, \dots , V_n)$ of values of type $\vec {x}:\vec {T}\vdash V_i :S_i$ for each $i$ (modulo renaming of $\vec {x}$). Composition is intuitively defined by “substitution followed by $\beta$-reduction” whose definition is omitted here.⁵

The functor $J_{ Ax }$ places the values to the channels. For example, let $\vec {T}= (\mathbf {ch}^{i}[U_1], \mathbf {ch}^{o}[U_2])$ and consider the morphism in $\mathcal {C}_{ Ax }$ given by

$$ a :\mathbf {ch}^{i}[T_1], \bar{b}:\mathbf {ch}^{o}[T_2] \vdash (a, \bar{b}, (\vec {x}).P) : (\mathbf {ch}^{i}[T_1], \mathbf {ch}^{o}[T_2], \mathbf {ch}^{o}[\vec {S}]) $$

where $\vec {S}$ is the type for $\vec {x}$. The image of this morphism by the functor $J_{ Ax }$ is

$$ a :\! \mathbf {ch}^{i}[T_1], \bar{b}:\! \mathbf {ch}^{o}[T_2], \bar{c}:\! \mathbf {ch}^{o}[T_1], d :\! \mathbf {ch}^{i}[T_2], e :\! \mathbf {ch}^{i}[\vec {S}] \vdash {a \hookrightarrow \bar{c}} \mid {d \hookrightarrow \bar{b}} \mid {!} e (\vec {x}). P :\! \diamond . $$

This example contains all the three ways to place a value to a given channel.

Theorem 3

$Cl ( Ax )$ is a compact closed Freyd category for every $Ax$.    $\square$

In the model $Cl ( Ax )$, the interpretation of a process $\varGamma \vdash P : \diamond$ is the equivalence class that $P$ belongs to. This fact leads to completeness.

Theorem 4

(Completeness). If $Ax \rhd \varGamma \Vdash P = Q$, then $Ax \rhd \varGamma \vdash P = Q$.    $\square$

Theorem 5

There exists a compact closed Freyd category $J$ that is fully abstract w.r.t. may-testing equivalence, i.e. $\varGamma \vdash P \mathrel {=_{ may }}Q$ iff .

Proof

Let $J$ be the term model $Cl (\mathrel {=_{ may }})$ and use Proposition 2.    $\square$

3.5 Theory/Model Correspondence

It is natural to expect that $Cl ( Ax )$ is the classifying category as in the standard categorical type theory. This means, to give a model of $Ax$ in $J$ is equivalent to give a structure-preserving functor $Cl ( Ax ) \longrightarrow J$. This subsection clarifies and studies this claim.

The set $\mathrm {Mod}( Ax , J)$ of models of $Ax$ in $J$ is defined as follows. If $J \,\models \, Ax$, then $\mathrm {Mod}( Ax , J)$ is a singleton set⁶; otherwise $\mathrm {Mod}( Ax , J)$ is the empty set.

We then define the notion of structure-preserving functors.

Definition 8

A strict compact closed Freyd functor from to is a pair of functor $(\varPhi , \varPsi )$ such that

• $\varPhi$ is a strict finite product preserving functor from $\mathcal {C}$ to $\mathcal {C}'$,

• $\varPsi$ is a strict symmetric monoidal functor from $\mathcal {K}$ to $\mathcal {K}'$ that preserves the chosen compact closed structures (i.e. units and counits) on the nose, and

• $(\varPhi , \varPsi )$ is a map of adjoints between $J \dashv I \Rightarrow (-)$ and $J' \dashv I \Rightarrow ' (-)$.

   $\square$

The collection of (small) compact closed Freyd categories and strict compact closed Freyd functors form a $1$-category, which we write as $CCFC$.

Now the question is whether in $\mathbf {Set}$.

Unfortunately this does not hold. More precisely, the left-to-right inclusion does not hold in general. This means that the term model satisfies some additional axioms reflecting some aspects of the $\pi _F$-calculus.

The additional axioms reflect the definition of the dual $\vec {T}^*$ in the term model; we have by definition, and thus $\vec {T}^{**} = \vec {T}$ and $(\vec {T}\otimes \vec {S})^{*} = \vec {T}^{*} \otimes \vec {S}^{*}$. It might be surprising that these equations are harmful because isomorphisms $A^{**} \cong A$ and $(A \otimes B)^* \cong A^* \otimes B^*$ exist in every compact closed category. The point is that the equations also require $\mathcal {C}$ to have isomorphisms $A^{**} \cong A$ and $(A \otimes B)^* \cong A^* \otimes B^*$ (witnessed by the respective identities).

We formally define the additional axioms, which we call (I) and (D):

• (I) The canonical isomorphism $A^{**} \longrightarrow A$ in $\mathcal {K}$ is the identity.

• (D) The canonical isomorphism $(A \otimes B)^{*} \longrightarrow A^* \otimes B^*$ in $\mathcal {K}$ is the identity.

Theorem 6

$\mathrm {Mod}( Ax , J) \cong CCFC ( Cl ( Ax ), J)$ if J satisfies (I) and (D).    $\square$

4 A Concurrent $\lambda$-calculus and (de)compilation

In order to demonstrate the relevance of our semantic framework, this section tries to give a semantic reconstruction of fully-abstract compilation and decompilation from a higher-order calculus to the (first-order) $\pi$-calculus, such as [39, 42]. We first design an instance of the computational $\lambda$-calculus [33], named $\lambda _{ ch }$, that is sound and complete with respect to compact closed Freyd categories. It is obtained by a straightforward extension of the coincidence between the computational $\lambda$-calculus and closed Freyd categories (Sect. 4.1). There are translations between $\pi _F$ and $\lambda _{ ch }$ since both are sound and complete with respect to compact closed Freyd categories. Section 4.2 actually calculates the translations, and compare them with those in [39, 42].

Fig. 4.

Syntax of types and terms of the $\lambda _{c}$- and $\lambda _{ ch }$-calculi. The syntax of $\lambda _{c}$ is adapted to the setting of this paper.

4.1 The $\lambda _{ ch }$-calculus

The $\lambda _{ ch }$-calculus is a computational $\lambda$-calculus with additional constructors dealing with channels. This section introduces and explains the calculus.

The situation is nicely expressed by the following intuitive equation:

The base calculus $\lambda _{c}$ is the computational $\lambda$-calculus, which corresponds to closed Freyd category [33, 37]. It is a call-by-value higher-order programming language, given in Fig. 4(a). Our calculus $\lambda _{ ch }$ is obtained by adding type and term constructors originating from the compact closed structure, which $\lambda _{c}$ does not have.

Syntax. As for types, $\lambda _{ ch }$ has a new constructor coming from the dual object $A^*$. Normalising occurrences of the dual $A^*$ using the axioms (I) $A^{**} = A$ and (D) $(A \otimes B)^* = A^* \otimes B^*$, we obtain the following grammar of types:

where $n \ge 0$ and $(\xi _1, \dots , \xi _n)$ is an alternative notation for $\xi _1 \otimes \dots \otimes \xi _n$. Compared with $\lambda _{c}$, the only new type is the dual type $\sigma ^*$ of a function type $\sigma$.

As for terms, $\lambda _{ ch }$ has constructors corresponding to the unit and counit

$$ \eta _A : I \longrightarrow A \otimes A^* \qquad \epsilon _A : A^* \otimes A \longrightarrow I \quad \qquad \text{(for } \text{ each } \text{ object } A\text{) } $$

of the compact closed structure. We simply add these morphisms as constants:

$$ \dfrac{ }{ \varGamma \vdash \mathbf {channel}_{\sigma } : () \rightarrow (\sigma , \sigma ^*) } \qquad \text{ and }\qquad \dfrac{ }{ \varGamma \vdash \mathbf {send}_{\sigma } : (\sigma ^*, \sigma ) \rightarrow () }. $$

We shall often omit the subscript $\sigma$.

In summary, we obtain the syntax of $\lambda _{ ch }$ shown in Fig. 4. Interestingly, $\lambda _{ ch }$ can be seen as a very core of Concurrent ML [38], a practical higher-order concurrent language, although $\lambda _{ ch }$ is developed from purely semantic considerations.

Semantics. Let us first discuss the intuitive meanings of the new constructors. The type $\sigma ^*$ is for output channels; $\mathbf {channel}\,\langle \rangle$ creates and returns a pair of an input channel and an output channel that are connected; and $\mathbf {send}\,\langle {\alpha },{V} \rangle$ sends the value $V$ via the output channel $\alpha$. The following points are worth noting.

• $\lambda _{ ch }$ has no type constructor for input channels. The type system does not distinguish between input channels for type $\sigma$ and values of type $\sigma$.

• $\lambda _{ ch }$ has no receive constructor. Receiving operation is implicit and on demand, delayed as much as possible.

• The send operator broadcasts a value via a channel. Several receivers may receive the same value from the same channel.

The first two points reflect the asynchrony of $\pi _F$, and the last point reflects the absence of non-replicated input (cf. Sect. 4.2).

Based on this intuition, we develop the operational, axiomatic and categorical semantics of $\lambda _{ ch }$. We shall use the following abbreviations:

Operational Semantics. Assume an infinite set $\mathcal {X}$ of channels, ranged over by $\alpha$ and $\beta$. For each channel $\alpha$, we write $\alpha$ for the input name and $\bar{\alpha }$ for the output name, both of which are values. A configuration is a tuple $(M, \vec {\alpha } ,\mu )$ of a term $M$, a sequence $\vec {\alpha }$ of generated channels and a sequence $\mu$ of performed send operations, i.e. $\mu = (\mathbf {send}\,\langle {\bar{\beta }_1},{V_1} \rangle , \dots , \mathbf {send}\,\langle {\bar{\beta }_k},{V_k} \rangle )$. The reduction relation is defined by the following rules for channels

in addition to the standard rules for $\lambda$-abstractions and let-expressions, which change only $M$. Here the set of evaluation contexts is given by the grammar:

Note that $M$ and $N$ in $\mathbf {let}\, {\langle \vec {x} \rangle } = {M}\, \mathbf {in}\,{N}$ are evaluated in parallel (cf. Remark 3). This justifies the notation $M \parallel N$, an abbreviation for $\mathbf {let}\, {\langle \rangle } = {M}\, \mathbf {in}\,{N}$.

Axiomatic Semantics. The inference rules of the equational logic for $\lambda _{ ch }$ are those for $\lambda _{c}$ with the rule of concurrent evaluation

$$ \mathbf {let}\, {\langle \vec {x} \rangle } = {M}\, \mathbf {in}\,{\mathbf {let}\, {\langle \vec {y} \rangle } = {N}\, \mathbf {in}\,{L}} \quad =\quad \mathbf {let}\, {\langle \vec {y} \rangle } = {N}\, \mathbf {in}\,{\mathbf {let}\, {\langle \vec {x} \rangle } = {M}\, \mathbf {in}\,{L}}; $$

the $\beta$- and $\eta$-rules for channels

$$\begin{aligned} (\varvec{\nu } x \bar{x})(\mathbf {send}\,\langle {\bar{x}},{V} \rangle \parallel M)&\quad =\quad (\varvec{\nu } x \bar{x})(\mathbf {send}\,\langle {\bar{x}},{V} \rangle \parallel M\{V/x\}) \\ (\varvec{\nu } y \bar{y})(\mathbf {send}\,\langle {\bar{z}},{y} \rangle \parallel N)&\quad =\quad N\{\bar{z}/\bar{y}\} \end{aligned}$$

where $\bar{x}\notin \mathbf {Fv}(V) \cup \mathbf {Fv}(M)$, $y \notin \mathbf {Fv}(N)$ and $\bar{z}\ne \bar{y}$; and a GC rule.

Categorical Semantics. One can interpret $\lambda _{ ch }$-terms in a compact closed Freyd category with (I) and (D). The interpretation of the $\lambda _{c}$-calculus part is standard [24, 37]; the constant $\mathbf {channel}_{\sigma }$ (resp. $\mathbf {send}_{\sigma }$) is interpreted as the “closure” whose body is $\eta _{\sigma }$ (resp. $\epsilon _{\sigma }$) as expected.

The categorical semantics is sound and complete with respect to the equational theory of the $\lambda _{ ch }$-calculus. The proofs are basically straightforward but there is a subtle issue in the definition of the term model: we have different definitions of the right adjoint $I \Rightarrow ({-})$, which are of course equivalent but do not coincide on the nose. Our choice here is .

4.2 Translations Between $\lambda _{ ch }$ and $\pi _F$

The higher-order calculus $\lambda _{ ch }$ is equivalent to $\pi _F$. This is because both calculi correspond to the same class of categories, namely, the class of compact closed Freyd categories with (I) and (D), i.e.,

This subsection studies translations derived from this semantic correspondence.

The translations are defined by the interpretations in the term models. For example, the translation from $\lambda _{ ch }$ to $\pi _F$ is induced by the interpretation of $\lambda _{ ch }$-terms in the term model $Cl (\emptyset )$. The interpretation of a $\lambda _{ ch }$-term $M$ is an equivalence class of $\pi _F$-processes, since a morphism in $Cl (\emptyset )$ is an equivalence class of $\pi _F$-processes. The translation is defined by choosing a representative of the equivalence class. The other direction $[\!({-})\!]$ is obtained by the interpretation of $\pi _F$ in the term model of $\lambda _{ ch }$.

Figures 5 and 6 are concrete definitions of the translations for a natural choice of representatives. Let us discuss the translations in more details.

The translation from $\pi _F$ to $\lambda _{ ch }$ (Fig. 5) is easy to understand. It directly expresses the higher-order view of the first-order $\pi$-calculus. For example, an output action is mapped to an application and an input-prefixing ${!} a (\vec {x}). P$ to a send operation of the value $\lambda \langle \vec {x} \rangle .P$ via the channel $a$.

An interesting (and perhaps confusing) phenomenon is that an input channel in $\pi _F$ is mapped to an output channel in $\lambda _{ ch }$. This can be explained as follows. In the name-passing viewpoint, the reduction

$$ (\varvec{\nu } x y) ({!} y (\vec {z}). P \mid x \langle \vec {u} \rangle ) \quad \longrightarrow \quad (\varvec{\nu } x y) ({!} y (\vec {z}). P \mid P\{\vec {u}/\vec {z}\}) $$

Fig. 5.

Translation from $\pi _F$ to $\lambda _{ ch }$

Fig. 6.

Translation from $\lambda _{ ch }$ to $\pi _F$

sends $\vec {u}$ to the process ${!} y (\vec {z}). P$, and thus $x$ is output and $y$ is input. In the process-passing viewpoint, the abstraction $(\vec {z}).P$ is sent to the location of $x$, and thus $y$ is the output and $x$ is the input.

Next, we explain the translation from $\lambda _{ ch }$ to $\pi _F$ (Fig. 6).

Let us first examine the translation of types. The most non-trivial part is the translation of a function type $\tau _1 \rightarrow \tau _2$. A key to understand the translation is the isomorphism $\tau _1 \rightarrow \tau _2 \cong \tau _1 \otimes \tau _2^{\bot } \rightarrow ()$. The latter form of function type corresponds to an output channel type in $\pi _F$. Hence a function is understood as a process additionally taking channels to which the return values are passed.

The translation of a $\lambda _{ ch }$-term $\varGamma \vdash M : (\xi _1,\dots ,\xi _n)$ takes extra parameters $\vec {p} = p_1, \dots , p_n$ to which the values should be placed. This is a consequence of the definition in the $\pi _F$-term model that a morphism $\vec {T}\longrightarrow \vec {S}$ is a process $\vec {x}:\vec {T},\, \vec {y}:\vec {S}^{\bot } \vdash P : \diamond$. Here $\vec {p}$ corresponds to $\vec {y}$, $\varGamma$ to $\vec {x}:\vec {T}$ and $\vec {\xi }$ to $\vec {S}$.

Now it is not so difficult to understand the interpretations of constructs in the $\lambda _{c}$-calculus. For example, the abstraction is mapped to an abstraction placed at $p$, which takes additional channels $\vec {q}$ to which the results of the evaluation of $M$ should be sent.

It might be surprising that the interpretations of $\mathbf {channel}$ and $\mathbf {send}$ coincide. This is because of the one-sided formulation of $\pi _F$. In the two-sided formulation, the unit $\eta$ and counit $\epsilon$ of the compact closed structure, corresponding to $\mathbf {channel}$ and $\mathbf {send}$, can be written as logical inference rules

$$ \dfrac{ \varGamma , A, A^{\bot } \vdash \varDelta }{ \varGamma \vdash \varDelta } \qquad \text{ and }\qquad \dfrac{ \varGamma \vdash A^{\bot }, A, \varDelta }{ \varGamma \vdash \varDelta }, $$

which are different. In the one-sided formulation, however, they become

$$ \dfrac{ \varGamma , A, A^{\bot }, \varDelta ^{\bot } \vdash }{ \varGamma , \varDelta ^{\bot } \vdash }. $$

Fig. 7.

Translation from AHO$\pi$ to $\pi _F$

Hence $\eta$ and $\epsilon$ (or $\mathbf {channel}$ and $\mathbf {send}$) cannot be distinguished in $\pi _F$.

The translation must be the inverse of $[\!({-})\!]$ because both the term models are the initial compact closed Freyd category with (I) and (D). That means, and are provable for every $P$ and $M$. This result is independent of the choice of representatives.

4.3 Relation to Other Calculi and Translations

A number of higher-order concurrent calculi, as well as their translations to the first-order $\pi$-calculus, have been proposed and studied (e.g. [29, 39, 40, 42, 45, 47]). The calculus $\lambda _{ ch }$ and the translations have a lot of ideas in common with those calculi and translations; see Sect. 6.

This subsection mainly discusses the relationship to the translations by Sangiorgi [42] (see also [43]) between asynchronous higher-order $\pi$-calculus (AHO$\pi$ for short) and asynchronous local $\pi$-calculus (L$\pi$ for short). Here we focus on this work because it is closest to ours. We shall see that our semantic or categorical development provides us with a semantic reconstruction of Sangiorgi’s translations, as well as an extension.

A variant of AHO$\pi$ can be seen as a fragment of $\lambda _{ ch }$. The syntax of processes of AHO$\pi$ and representation by $\lambda _{ ch }$-terms are given as follow:

(It slightly differs from the original syntax, as $\varvec{\nu }$ binds a pair of names.)

This fragment is nicely described as the limitation on types:

Recall that $\sigma$ is a type for abstractions, $\xi$ is a type for variables, and $\tau$ is a type for terms. This limitation means that (1) an abstraction cannot take a channel as an argument, and (2) a term $M$ must be of the unit type, i.e. a process.

Once regarding AHO$\pi$ as a fragment of $\lambda _{ ch }$, the translation from AHO$\pi$ to $\pi _F$ is obtained by restricting to AHO$\pi$. The resulting translation is in Fig. 7. As mentioned, the translation is the same as that of Sangiorgi [42] except for minor differences due to the slight change of the syntax.

Sangiorgi also gave a translation in the opposite direction, from L$\pi$ to AHO$\pi$ in the same paper. The calculus L$\pi$ is a fragment of the $\pi$-calculus in which only output channels can be passed. The $\mathbf {i/o}$-separation of $\pi _F$ allows us to characterise the local version of $\pi _F$ by a limitation on types. In the local variant, the output channel type is restricted to , expressing that only output channels can be passed via an output channel. Then the definition of type environment should be changed accordingly: (since the syntactic class represented by $T$ is not closed under the dual $({-})^{\bot }$ in the local setting).

Interestingly the limitation on types in AHO$\pi$ coincides with that in L$\pi$, when one identify $\mathbf {ch}^{o}[\vec {T}]$ with $(\vec {T}) \rightarrow ()$ (as we have done in many places). In other words, the syntactic restrictions of AHO$\pi$ and L$\pi$ are the same semantic conditions described in different syntax. As a consequence, the image of L$\pi$ by $[\!({-})\!]$ is indeed in AHO$\pi$.

Remark 4

There is, however, a notable difference from Sangiorgi’s work [42]. Sangiorgi proved that the translation is fully-abstract with respect to barbed congruence; in contrast, we only show that $\vdash M = N$ iff . In particular, the $\eta$-rule is inevitable for our argument. The presence of the $\eta$-rules significantly simplifies the argument, at the cost of operational justification (recall that the $\eta$-rule is not sound with respect to barbed congruence).

It is natural to ask how one can reconstruct the full-abstraction result with respect to barbed congruence. An interesting observation is that, if $M$ and $N$ are AHO$\pi$ processes, then $\vdash ^{\ominus } M = N$ iff , where $\vdash ^{\ominus }$ means provability without using $\eta$-rules. We expect that this semantic observation explains why locality is essential as noted in [42]; we leave the details for future work.    $\square$

5 Discussions

Connection to Logics. We have so far studied a connection between compact closed Freyd category and $\pi$-calculus. Here we briefly discuss the missing piece of the Curry-Howard-Lambek correspondence, namely logic.

The model of this paper is closely related to linear logic. Actually, every compact closed Freyd category is a model of linear logic (more precisely, MELL), as an instance of linear-non-linear model [6] (see, e.g., [27] for categorical models of linear logic). The interpretation of formulas is shown in Table 1. It differs from the translations by Abramsky [1] and Bellin and Scott [5] and from the Curry-Howard correspondence for session types by Caires and Pfenning [8], but resembles the connection between a variant of local $\pi$-calculus and a polarised linear logic by Honda and Laurent [19]; a detailed analysis of the translation is left for future work.

The logic corresponding to compact closed Freyd category should be a proper extension of linear logic, since compact closed Freyd categories form a proper subclass of linear-non-linear models. For example, the following rules are invalid in linear logic but admissible in compact closed Freyd categories:

$$ \dfrac{ \vdash \varGamma \qquad \vdash \varDelta }{ \vdash \varGamma , \varDelta } \qquad \dfrac{ \vdash \varGamma , A, B \qquad \vdash \varDelta , A^{\bot }, B^{\bot } }{ \vdash \varGamma , \varDelta } \qquad \dfrac{ \vdash \varGamma , A, A^{\bot } }{ \vdash \varGamma }. $$

Table 1. The categorical and $\pi _F$-calculus interpretations of MELL formulas

These rules, especially the second rule called multicut, were often studied in concurrency theory; see Abramsky et al. [2] for their relevance to concurrency.

Do the above rules fill the gap between linear logic and compact closed Freyd category? Recent work by Hasegawa [15] suggests that MELL with above rules is still weaker than compact closed Freyd category. First observe that the above rules can be interpreted in any linear-non-linear model of which the monoidal category is compact closed. Hasegawa showed that a linear-non-linear model whose monoidal category is compact closed induces a closed Freyd category of which the monoidal category is traced (and vice versa) but the induced Freyd category is not necessarily compact closed. Hence the logic corresponding to compact closed Freyd category has further axioms or rules in addition to the above ones. A reasonable candidate for the additional axiom is ${!} \cong {?}$; interestingly, Atkey et al. [3] reached a similar rule from a different perspective. Further investigation is left for future work.

Non-empty Signature. The categorical type theory for the $\lambda$-calculus considers a family parameterised by signatures, consisting of atomic types and constants. It covers, for example, the $\lambda$-calculus with natural number type and arithmetic constants (such as addition and multiplication), as well as a calculus with integer reference type and read and update functions.

Although this paper only considers the calculus with the empty signature, which has no additional type nor constant, extending our theory to handle non-empty signatures is, in a sense, not difficult. The easiest way is to apply the established theory of the computational $\lambda$-calculus [33, 37]. As we have seen in Sect. 4, the $\pi _F$-calculus can be seen as a computational $\lambda$-calculus $\lambda _{ ch }$ having constants for manipulating channels; hence the $\pi _F$-calculus with additional constants is $\lambda _{ ch }$ with the additional constants, which is still in the family of computational $\lambda$-calculus.

The $\pi _F$-calculus with non-empty signature has several applications. We shall briefly discuss some of them.

An important example of $\pi _F$ with non-empty signature is the calculus with non-replicated input, which we regard as a calculus with additional “process constants” but without any additional type. A key observation is that every non-replicated input process $a(\vec {x}).P$ can be expressed as

$$ a(\vec {x}).P \;\mathrel {\approxeq ^c}\; (\varvec{\nu } \bar{b} b)(a(\vec {x}).{\bar{b} \langle \vec {x} \rangle } \mid {!} b (\vec {x}). P) \qquad \text{( } \mathrel {\approxeq ^c} \text{ is } \text{ weak } \text{ barbed } \text{ congruence) } $$

and thus it suffices to deal with non-replicated input processes in special form, namely $a : \mathbf {ch}^{i}[\vec {T}],\; \bar{b}: \mathbf {ch}^{o}[\vec {T}] \vdash a(\vec {x}).{\bar{b} \langle \vec {x} \rangle } : \diamond$. Adding these processes as constants and the computational rules of $a(\vec {x}).{\bar{b} \langle \vec {x} \rangle }$ as equational axioms results in a calculus with non-replicated inputs. The categorical model is a compact closed Freyd category with distinguished morphisms $(A \Rightarrow I) \longrightarrow (A \Rightarrow I)$ for each object $A$ which satisfy certain axioms.

This technique is applicable to synchronous output as well. Because

$$ \bar{a}\langle \vec {x}\rangle .P \;\mathrel {\approxeq ^c}\; (\varvec{\nu } \bar{b} b)(\bar{a}\langle \vec {x}\rangle .\bar{b}\langle \rangle \mid {!} b (). P), $$

it suffices to consider constants representing $\bar{a}:\! \mathbf {ch}^{o}[\vec {T}], \vec {x}:\!\vec {T}, \bar{b}:\!\mathbf {ch}^{o}[] \vdash \bar{a}\langle \vec {x}\rangle .\bar{b}\langle \rangle :\! \diamond$.

6 Related Work

Logical Studies of $\varvec{\pi }$-calculi. There is a considerable amount of studies on connections between process calculi and linear logic. Here we divide these studies into two classes. These classes are substantially different; for example, one regards the formula $A \otimes B$ as a type for processes with two “ports” of type A and B, whereas the other as the session-type !A.B. Our work is more closely related to the former than the latter, but some interesting coincidence to the latter kind of studies can also be found.

The former class of research dates back to the work by Abramsky [1] and Bellin and Scott [5], where they discovered that $\pi$-calculus processes can encode proof-nets of classical linear logic. Later, Abramsky et al. [2] introduced the interaction categories to give a semantic description of a CCS-like process calculus. In their work, they observed that the compact closed structure is important to capture the strong expressive power of process calculi.

A tighter connection between $\pi$-calculus and proof-nets was recently presented by Honda and Laurent [19]. They showed that an $\mathbf {i/o}$-typed $\pi$-calculus corresponds to polarised proof-nets, and introduced the notion of extended reduction for the $\pi$-calculus to simulate cut-elimination. The $\pi$-calculus used in this work is very similar to $\pi _F$ in terms of syntax and reduction. Their calculus is asynchronous, does not allow non-replicated inputs, and requires $\mathbf {i/o}$-separation. Furthermore, the extended reduction is almost the same as the rules (E-Beta) and (E-GC) except for the side conditions. A significant difference compared to our work is that their calculus is local [28, 49], reflecting the fact that the corresponding logic is polarised.

Our work is inspired by these studies. The idea of $\mathbf {i/o}$-separation can already be found in the work by Bellin and Scott and the use of compact closed category is motivated by the study of interaction category. It is worth mentioning here that the design of $\pi _F$ is also influenced by the calculus introduced by Laird [22], although it is not a logical study but categorical (see below).

The latter approach started with the Curry-Howard correspondences between session-typed $\pi$-calculi and linear logic established by Caires, Pfenning and Toninho [8, 9] and subsequently by Wadler [48]. These correspondences are exact in the sense that every process has a corresponding proof, and vice versa. As a consequence, processes of the calculi inherit good properties of linear logic proofs such as termination and confluence of cut-elimination. In terms of process calculi, process of these calculi do not fall into deadlock or race condition. This can be seen as a serious restriction of expressive power [3, 26, 48].

Several extensions to increase the expressiveness of these calculi have been proposed and studied. Interestingly, ideas behind some of these extensions are related to our work, in particular to Sect. 5 discussing the multicut rule [2] and the axiom ${!} \cong {?}$. Atkey et al. [3] studied CP [48] with the multicut rule and ${!} \cong {?}$ and discussed how these extensions increase the expressiveness of the calculus, at the cost of losing some good properties of CP. Dardha and Gay [10] studied another extension of CP with multicut, keeping the calculus deadlock-free by an elaborated type system.

Balzer and Pfenning [4] proposed a session-typed calculus with shared (mutable) resources, inspired by linear-non-linear adjunction [6].

Categorical Semantics of $\varvec{\pi }$-calculi. The idea of using a closed Freyd category to model the $\pi$-calculus is strongly inspired by Laird [22]. He introduced the distributive-closed Freyd category to describe abstract properties of a game-semantic model of the asynchronous $\pi$-calculus and showed that distributive-closed Freyd categories with some additional structures suffice to interpret the asynchronous $\pi$-calculus. The additional structures are specific to his game model and not completely axiomatised.⁷ Our notion of compact closed Freyd category might be seen as a reformulation of his idea, obtained by filtering out some structures difficult to axiomatise and by strengthening some others to make axioms simpler. A significant difference is that our categorical model does not deal with non-replicated inputs, which we think is essential for a simple axiomatisation.

Another approach for categorical semantics of the $\pi$-calculus has been the presheaf based approach [12, 44]. These studies gave particular categories that nicely handles the nominal aspects of the $\pi$-calculus; these studies, however, do not aim for a correspondence between a categorical structure and the $\pi$-calculus.

Higher-Order Calculi with Channels. Besides the $\lambda _{ ch }$-calculus, there are numbers of functional languages augmented by communication channels, from theoretical ones [13, 25, 46, 48] to practical languages [34, 38].

On the practical side, Concurrent ML (CML) [38], among others, is a well-developed higher-order concurrent language. CML has primitives to create channels and threads, and primitives to send and accept values through channels. Since our $\lambda _{ ch }$-calculus can create (non-linear) channels and send values via channels, the $\lambda _{ ch }$-calculus can be seen as a core calculus of CML despite its origin in categorical semantics. The major difference between CML and the $\lambda _{ ch }$-calculus is that communications in CML are synchronous whereas communications in the $\lambda _{ ch }$-calculus are asynchronous.

On the theoretical side, session-typed functional languages have been actively studied [13, 25, 46, 48]. Notably, some of these languages [25, 46, 48] are built upon the Curry-Howard foundation between linear logic and session-typed processes. It might be interesting to investigate whether we can relate these languages and the $\lambda _{ ch }$-calculus through the lens of Curry-Howard-Lambek correspondence.

Higher-Order vs. First-Order $\varvec{\pi }$-calculus. A number of translations from higher-order languages to the $\pi$-calculus have been developed [39, 40, 42, 45, 47] since Milner [29] presented the encodings of the $\lambda$-calculus into the $\pi$-calculus. The basic idea shared by these studies is to transform $\lambda x.M$ to a process ${!} a (x,p). P$ that receives the argument x together with a name p where the rest of the computation will be transmitted. In our framework, this idea is described as the isomorphism $A \Rightarrow B \cong A \otimes B^* \Rightarrow I$.

Among others, the translation from AHO$\pi$ to L$\pi$ [42] is the closest to our translation from the $\lambda _{ ch }$-calculus to the $\pi _F$-calculus. Sangiorgi [41] observed that Milner’s translation can be established via the translation of AHO$\pi$ by applying the CPS transformation to the $\lambda$-calculus. This observation also applies to our translation. That is, we can obtain Milner’s translation by combining CPS transformation and the compilation of the $\lambda _{ ch }$-calculus.

7 Conclusion and Future Work

We have introduced an $\mathbf {i/o}$-typed $\pi$-calculus ($\pi _F$-calculus) as well as the categorical counterpart of $\pi _F$-calculus (compact closed Freyd category) and showed the categorical type theory correspondence between them. The correspondence was established by regarding the $\pi$-calculus as a higher-order programming language, introducing the $\mathbf {i/o}$-separation, and introducing the $\eta$-rule, a rule that explains the mismatch between behavioural equivalences and categorical models.

As an application of our semantic framework we introduced a higher-order calculus $\lambda _{ ch }$-calculus “equivalent” to the $\pi _F$-calculus. We have demonstrated that translations between $\lambda _{ ch }$-calculus and $\pi _F$-calculus can be derived by a simple semantic argument, and showed that the translation from $\lambda _{ ch }$ to $\pi _F$ is a generalisation of the translation from AHO$\pi$ to L$\pi$ given by Sangiorgi [42].

There are three main directions for future work. First, further investigation on the $\eta$-rule is indispensable. We plan to construct a categorical model of the $\pi _F$-calculus with an additional constant that captures barbed congruence. Revealing the relationship between locality and the $\eta$-rule is another important problem. Second, the operational properties of the $\lambda _{ ch }$-calculus and its relation to the equational theory needs a further investigation. Third, finding the logical counterpart of compact closed Freyd category to establish a proper Curry-Howard-Lambek correspondence is an interesting future work.