$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

TL;DR

This paper interprets multiplicative linear logic as a typing system for concurrent functional programming, introducing a new calculus that supports parallelism and communication with desirable language properties.

Contribution

It presents a novel extension of lambda calculus, called λ⊗, that models concurrent computation based on linear logic proofs, with formal proofs of key language properties.

Findings

λ⊗ satisfies subject reduction and progress

The calculus is strongly normalizing and confluent

Provides a logical foundation for concurrent programming languages

Abstract

Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $\lambda$-calculus with parallelism and communication primitives, called $\lambda_{\unicode{8523}}$. We shall prove that $\lambda_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.

Tables

Table 1. Table 1 : The type assignment rules of NMLL NMLL \mathrm{NMLL} .

$x:A\Rightarrow x:A$

Table 2. Table 2 : Reduction rules for NMLL NMLL \mathrm{NMLL} terms.

$\left(\lambda xu\right)t\mapsto u\left[t/x\right]$

Table 3. Table 3 : The sequent calculus MLL MLL \mathrm{MLL} .

$\begin{array}{cc}\Gamma \Rightarrow \Delta & \perp \\ \overline{\Gamma \Rightarrow \Delta ,\perp }\end{array}\perp \Rightarrow$

Equations

$$\nu z(x(y).z(w).P\mid z[a].Q)\mapsto x(y).\nu z(z(w).P\mid z[a].Q)$$

$$x(y).\nu z(z(w).P\mid z[a].Q)\mapsto x(y).\nu z(P[a/w]\mid Q)$$

$$\nu z(P\mid w[a].Q)\mapsto \nu z(P[a/w]\mid Q)$$

$$\Gamma \Rightarrow \lambda xt:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$\Gamma \Rightarrow \overline{x}.t:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$\Gamma \Rightarrow s\mid t:A\text{parr}B,\Delta \Gamma \Rightarrow s:A,t:B,\Delta$$

$$u,v::=$$

$$|\overline{x}.u$$

$$|\overline{x}\overline{y}u$$

$$|u\mid v$$

$$|\mathsf{close}(u)$$

$$|x$$

$$|uv$$

$$\mathsf{syntactic}\mathsf{sugar}$$

$$|\lambda xu:=\overline{x}.u$$

$$|\overline{x}v.u:=(\overline{x}.u)v$$

$$u,v::=x|uv|\lambda xu|\overline{x}v.u\mid u\mid v|\overline{x}\overline{y}u|\circ |\mathsf{close}(u)$$

$$\Gamma \Rightarrow \lambda xt:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$\Gamma \Rightarrow \overline{x}.t:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$\Gamma ,\Sigma \Rightarrow st:B,\Delta ,\Theta \text{lx@proof@logical@and}\Gamma \Rightarrow s:A⊸B,\Delta \Sigma \Rightarrow t:A,\Theta$$

$$\Gamma \Rightarrow s\mid t:A\text{parr}B,\Delta \Gamma \Rightarrow s:A,t:B,\Delta$$

$$\Gamma ,{\Sigma }_1,{\Sigma }_2\Rightarrow \overline{x}\overline{y}s:\perp ,\Delta ,{\Theta }_1,{\Theta }_2\text{lx@proof@logical@and}\Gamma \Rightarrow s:A\text{parr}B,\Delta {\Sigma }_1,x:A\Rightarrow {\Theta }_1{\Sigma }_2,y:B\Rightarrow {\Theta }_2$$

$$\Gamma \Rightarrow \Delta ,\circ :\perp \Gamma \Rightarrow \Delta \Gamma \Rightarrow \mathsf{close}(t),\Delta \Gamma \Rightarrow t:\perp ,\Delta$$

$$\Gamma \Rightarrow s\mid t:A\text{parr}B,\Delta \Gamma \Rightarrow s:A,t:B,\Delta$$

$$\Gamma ,\Sigma \Rightarrow st:B,\Delta ,\Theta \text{lx@proof@logical@and}\Gamma \Rightarrow s:A⊸B,\Delta \Sigma \Rightarrow t:A,\Theta$$

$$x:A\Rightarrow x:A$$

$$\Gamma \Rightarrow \lambda xt:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$(\lambda xu)t\mapsto u[t/x]$$

$$\Gamma \Rightarrow \overline{x}.t:A⊸B,\Delta \Gamma ,x:A\Rightarrow t:B,\Delta$$

$$\mathcal{C}[\overline{x}u.s]\mid \mathcal{D}[x]\mapsto \mathcal{C}[s]\mid \mathcal{D}[u]$$

$$\mathcal{C}[x]\mid \mathcal{D}[\overline{x}u.s]\mapsto \mathcal{C}[u]\mid \mathcal{D}[s]$$

$$\overline{x}u.\circ \mid (\lambda yy\mid zx)\mapsto \circ \mid (\lambda yy\mid zu).$$

$$(\lambda y\overline{x}(yw).\circ )v\mid x\mapsto \overline{x}(vw).\circ \mid x\mapsto \circ \mid vw$$

$$(\lambda y\overline{x}(yw).\circ )v\mid x=(\overline{y}.\overline{x}(yw).\circ )v\mid x\mapsto (\overline{y}.\circ )v\mid yw=\overline{y}v.\circ \mid yw\mapsto \circ \mid vw$$

$$\overline{x}v.y\mid \overline{y}x.\circ \mapsto y\mid \overline{y}v.\circ \mapsto v\mid \circ$$

Full text

1 Introduction

The Proofs-as-Processes Program

Introduced by Girard in 1987, linear logic was announced right off the bat as the logic of parallelism. According to [14], the “connectives of linear logic have an obvious meaning in terms of parallel computation (…) In particular, the multiplicative fragment can be seen as a system of communication without problems of synchronization.” Stimulated by this remark and the further observation that “cut elimination is parallel communication between processes” ([15], pp. 155), Abramsky [1] launched the “Proofs-as-Processes” program, whose goal was to support with computational evidence Girard’s claims. Namely, the goal was “to show how a process calculus, sufficiently expressive to allow a reasonable range of concurrent programming examples to be handled, could be exhibited as the computational correlate of a proof system” [1]. A candidate process calculus was Milner’s $\pi$-calculus [24]; a possible proof system, the linear sequent calculus. The hope was that linear logic could provide a canonical and firm foundation to concurrent computation, serving as a tool for typing and reasoning about communicating processes.

Early successes

After the early work of [7], the turning point was the discovery by Caires and Pfenning [9] of a tight correspondence between intuitionistic linear logic and a session typed $\pi$-calculus, the motto being: linear propositions as session types, proofs as processes, cut-elimination as communication. This was yet another instance of the famous Curry-Howard correspondence [33], linking proofs to programs, propositions to types, proof normalization to computation. Soon after, Wadler [32] introduced the session typed $\pi$-calculus CP, shown to tightly correspond to classical linear logic.

Limitations

This important research notwithstanding, it appears that there is still ground to cover toward canonical and firm foundations for concurrent computation. First of all, asynchronous communication does not appear to rest on solid foundations. Yet this communication style is easier to implement and more practical than the purely synchronous paradigm, so it is widespread and asynchronous typed process calculi have been already investigated (see [13]). Unfortunately, linear logic has not so far provided via Curry-Howard a logical account of asynchronous communication. The reason is that there is a glaring discrepancy between full cut-elimination and $\pi$-calculus reduction which has not so far been addressed. On one hand, as we shall see, linear logic does support asynchronous communication, but only through the full process of cut-elimination, which indeed makes essential use of asynchronous communication. On the other hand, the $\pi$-calculus of [9] only mimics a partial cut-elimination process that only eliminates top-level cuts. Indeed, by comparison with its type system, the $\pi$-calculus lacks some necessary computational reduction rules. Some of the missing reductions, corresponding to commuting conversions, were provided in Wadler’s CP. The congruence rules that allow the extra reductions to mirror full cut-elimination, however, were rejected: in Wadler’s [32] own words, “such rules do not correspond well to our notion of computation on processes, so we omit them”. A set of reductions similar to that rejected by Wadler is regarded in [27] as sound relatively to a notion of “typed context bisimilarity”. The notion, however, only ensures that two “bisimilar” processes have the same input/output behaviour along their main communication channel; the internal synchronization among the parallel components of the two processes is not captured and may differ significantly. Thus, the extensional flavor of the bisimilarity notion prevents it to detect the intensionally different behaviour of the related processes, that is, how differently they communicate and compute.

There is no way out: attempts to model asynchronous communication by mirroring full cut-elimination with Milner’s $\pi$-calculus are bound to fail. An example will clarify the matter. In the process $\nu z(x(y).z(w).P\mid z[a].Q)$, the second process $z[a].Q$ wishes to transmit the message $a$ along the channel $z$ to the first process. However, the first process is not ready to receive on $z$ yet, because it is designed to first receive a message on the channel $x$. In Milner’s $\pi$-calculus, this is a deadlock, because input and output actions are rigidly ordered and blocking, for the sake of synchronization. Indeed, as the heir of CCS [22], $\pi$-calculus is in its essence a formalism for representing synchronization: a communication happens when two processes synchronize by consuming two dual constructs, as for instance $\overline{x}\,m$ and $x(y)$. However, when a process is seen as proof in the logical system, the order between prefixes becomes less relevant, thus in CP there is an extra commuting conversion

[TABLE]

In CP, there is no further reduction allowed, and rightly so: otherwise the blocking nature of the prefix $x(y)$ would be violated, making the very construct pointless for synchronization. On the other hand, for cut-elimination the now possible reduction

[TABLE]

is needed. In this case, however, as we have seen the very existence of a construct for input becomes misleading and would be more coherent to drop it altogether, so that the first process would be directly re-written and reduced as follows

[TABLE]

This is indeed the approach of the present paper. Sensitive to similar concerns, [18] introduced HCP, which features delayed input-output actions, modeling a form of asynchrony. However, the change in the transitions with respect to CP undermines the synchronous nature of Milner’s $\pi$-calculus, as we have seen, making it quite a different calculus and jeopardizing its canonicality ambitions. Moreover, HCP comes at the cost of adding redundant logical structures to the linear sequent calculus, namely hypersequents [6], which were instead used by Avron to increase the logical power of sequents.

There are other limitations in the current linear logic foundations of concurrent computation. The linear sequent calculus fails to combine seamlessly functional and concurrent computation. Indeed, according to Abramsky et al. [2] it is a “major open problem (…) to combine our understanding of the functional and concurrent paradigms, with their associated mathematical underpinnings, in a single unified theory”. The standard sequent calculus falls short in several other respects: it prevents deadlocks, but by excessively restricting possible communication patterns, for instance by forbidding cyclic configurations; it does not permit in any simple way code mobility, that is, the ability to communicate code, like in higher-order $\pi$-calculus [30]; it does not represent multi-party communication sessions; the syntax of processes does not match exactly the syntax of the typing system. In order to address some of these pitfalls, much work has been done, by either considering non-standard proof systems for linear logic or by extending the logic itself; unfortunately for the canonical-foundation enterprise and practical usability, these systems tends to be proof-theoretically artificial. A system adding a functional language on top of linear-logic-based typed $\pi$-calculus was studied in [31]. A solution for allowing, also in the context of the session typed $\pi$-calculus, cyclic communication patterns, was given in [12] by coming up with a new variant of linear logic; this makes possible for example to implement Milner’s scheduler process. Multi-party session types has been treated for example in [10]. A hypersequent proof system for linear logic whose syntax perfectly matches the syntax of $\pi$-calculus has been introduced in [18]. A logic for typing asynchronous communication in a non-standard process calculus has been proposed in [29].

$\lambda_{\parr}$: A concurrent extension of $\lambda$-calculus arising from linear logic

We shall illustrate a new approach in the study of linear logic as typing system for concurrent programs. Our framework does not suffer any of the mentioned limitations of linear sequent calculus. Inspired by [17, 25], we move away from sequent calculus and adopt a multiple-conclusion natural deduction for multiplicative linear logic, which we show to be isomorphic to a concurrent extension of $\lambda$-calculus, called $\lambda_{\parr}$. As a result, $\lambda_{\parr}$ is typed by linear multiple-conclusion natural deduction; it is naturally asynchronous, yet it can model synchronous communication as well; it allows arbitrary communication patterns, like cyclic ones, but prevents deadlocks; it allows higher-order communication and code mobility; it mirrors perfectly a full normalization procedure resulting in analytic proofs; its types can be read as program specifications in the traditional way, although they do not describe communication protocols as session types do.

The typing system of $\lambda_{\parr}$, in its non-linear variant, has been very well studied: computationally, it was famously interpreted by Parigot [26] as $\lambda\mu$-calculus; proof-theoretically, it was thoroughly investigated by [11]. Although proof-nets have sometimes been dubbed “the natural deduction of linear logic”, our typing system is closer to a natural deduction. It is not exactly natural deduction [28], since it is multiple-conclusion, hence it is natural for building and typing parallel programs, but not much so for modeling human deduction. However, our system is based on natural-deduction normalization rather than sequent-calculus cut-elimination and linear implication $\multimap$ is a primitive connective, with the standard introduction and elimination rules. Like proof-nets, $\lambda_{\parr}$ abstracts away from those inessential permutations in the order of rules that plague multiple-conclusion logical systems. As a result, $\lambda_{\parr}$ avoids commuting conversions, which have never been convincing from the computational point of view. Actually, $\lambda_{\parr}$ is not only a concurrent $\lambda$-calculus, it also looks like the natural deduction version of proof nets. Finally, it enjoys all the good properties that a well-behaved functional programming language should have: subject reduction, progress, strong normalization, and confluence. It is a step forward in the direction of that elusive concurrent $\lambda$-calculus which Milner attempted to find, before creating CCS out of the failure333According to Milner [23], “CCS is an attempt to provide a paradigm for concurrent computation. It arose after several unsuccessful attempts by the author to finds a satisfactory generalization of the lambda calculus, to admit concurrent computation.”.

The Insight

The main insight behind the typing system of $\lambda_{\parr}$ is to break into two rules the linear implication introduction. One rule is intuitionistic and yields functional abstraction, the second is classical and yields communication. Namely, the first rule, taken from [17], introduces the $\lambda$-operator, the second a communication channel with continuation:

[TABLE]

[TABLE]

Indeed, a communication channel $\overline{x}.\,t$ is supposed to take as argument a term $u:A$, transmit it along the channel $x$ and then continue with $t:B$. We shall indeed denote the application of $\overline{x}.\,t$ to $u$ as $\overline{x}u.t$, as in $\pi$-calculus: a promising sign!

The parallel operator $\mid$ is introduced by the $\parr$ introduction rule:

[TABLE]

finally doing justice to the $\parr$ connective, called par since the beginning.

2 Multiplicative Linear Logic as a Concurrent Functional Calculus

In this section, we present the syntax, the typing system $\mathrm{NMLL}$ and the reduction rules of the concurrent functional calculus $\lambda_{\parr}$.

2.1 The calculus $\lambda_{\parr}$

Definition 2.1** (Terms of $\lambda_{\parr}$).**

The untyped terms of $\lambda_{\parr}$ are defined by the following grammar:

[TABLE]

The calculus $\lambda_{\parr}$ is nothing but a linear lambda calculus extended with communication primitives. When $x$ occurs in $u$, the operator $\overline{x}.\,{u}$ is denoted and behaves exactly as $\lambda x\,u$. When $x$ does not occur in $u$, the term $\overline{x}.\,{u}$ behaves as an output channel $\overline{x}$ followed by a continuation $u$. Channels in $\lambda_{\parr}$ are thus first-class citizens that can be transmitted, shared, moved and applied to messages just like functions to arguments. When the channel $\overline{x}.\,{u}$ is applied to an argument $v$, it will be denoted as $\overline{x}v.u$, because it behaves exactly as its $\pi$-calculus counterpart: it transmits the message $v$ and continues with $u$. The term $\overline{x}\,\overline{y}\,\,u$ is an output channel which transmits the two messages contained in $u$ and then terminates.

If we omit parentheses, each term of $\lambda_{\parr}$ can be rewritten, not uniquely, as a parallel composition of several terms: $t_{1}\mid t_{2}\mid\ldots\mid t_{n}$. We will adopt this notation throughout the paper since it is irrelevant how the parallel operator $|$ associates.

Remark 2.1*.*

An alternative choice for the syntax of $\lambda_{\parr}$ may have been:

[TABLE]

Then the operator $\overline{x}v.u$ would have been typed by a cut-rule and the construct $\overline{x}.\,u$ would have been defined as: $\lambda y\,\overline{x}y.u$. This approach, however, would have raised some technical complications: when transmitting a message $v$, one would have to deal with the free variables of $v$ which are bound by $\lambda$ operators occurring outside $v$. A similar issue is solved in [4], and a simpler solution could be adopted here. Nevertheless, we adopt the present approach as it is the smoothest.

2.2 The Typing System $\mathrm{NMLL}$

Definition 2.2** (Types).**

The types of $\mathrm{NMLL}$ are built in the usual way from propositional variables, $\bot$ and the connectives $\multimap$ and $\parr$.

Since the typing system of $\lambda_{\parr}$ is classical linear logic, the $\otimes$ connective can be defined in terms of the others. Indeed, its computational interpretation seems less primitive, as it does not define any computational construct that is not already captured by $\multimap$ and $\parr$. Hence, we leave it out of the system.

Definition 2.3** (Sequents).**

The judgments of the typing system $\mathrm{NMLL}$ for $\lambda_{\parr}$ are sequents $\Gamma\Rightarrow\Delta$, where:

1. $\Gamma=x_{1}:A_{1},\ldots,x_{n}:A_{n}$ is a sequence of distinct variable declarations, each $x_{i}$ being a variable, $A_{i}$ a type and $x_{i}\neq x_{j}$ for $i\neq j$.

2. $\Delta=t_{1}:B_{1},\ldots,t_{n}:B_{n},t_{n+1},\ldots,t_{m}$, each $t_{i}$ being a term of $\lambda_{\parr}$ and $B_{i}$ a type.

The typing system of $\lambda_{\parr}$ is a linear version of the multiple-conclusion classical natural deduction of [11]. It is presented in Table 1 and discussed in detail below. As usual, we interpret a derivable sequent $\Gamma\Rightarrow\Delta$ as a judgement giving types to a sequence of terms $\Delta$, provided their variables are used with types declared in $\Gamma$. The terms in $\Delta$ that have no type are processes that return no value, and always have the form ${\mathsf{close}}(u)$, with $u:\bot$. These terms however cannot be ignored, as they may be involved in some communication; thus they are evaluated and then terminated.

2.3 Linearity of Variables

The only condition that the typing rules must satisfy in order to be applied is that their premises share no variable. This amounts to requiring the linearity of variables and to making sure that there is no clash among the names of the output channels. As we shall see in Proposition 7.1, the result of this implicit renaming is that a typed term cannot contain two distinct occurrences of the same output channel $\overline{x}$ nor of the same input channel $x$. This property has two consequences. First, in $\lambda_{\parr}$ we do not need, and actually do not use, any renaming during reductions. Secondly, communication channels cannot be used twice: once a message is transmitted along a channel, the channel is consumed and disappears forever, both from the sender and from the receiver of the message. These two processes can of course keep communicating with each other or with other processes, but they must use different channels for further communications.

2.4 $\parr$ as a Parallel Operator

The typing system of $\lambda_{\parr}$ is tailored to parallel computation. It is based on the view that the different processes of a parallel program are not independent entities, but make sense only as components of a larger and more complex system: they share resources through communication and they exploit the computational power of one another. Hence, one cannot build and type one process, without building at the same time all the interconnected processes. Coherently, a derivation of a sequent $\Gamma\Rightarrow t_{1}:A_{1},\ldots,t_{n}:A_{n},t_{n+1},\ldots t_{m}$ builds in parallel the terms $t_{1},\ldots,t_{m}$, following the logical structure of the intended communication pattern. The commas in the conclusion of a sequent, indeed, mean exactly parallel composition. Since the comma, in the final analysis, is the $\parr$ connective, we obtain the following typing rule:

[TABLE]

As the $\parr$ is commutative and associative, so it is the comma. Our reduction rules, indeed, treat parallel composition as commutative and associative, since they bypass the order and association of processes. Technically, however, the term $s\mid t:A\parr B$ is different from the term $t\mid s:B\parr A$, since $A\parr B$ and $B\parr A$ are logically equivalent, but not the same type. It would be possible to add explicit commutation and association congruences on the outermost parallel operators $|$, provided Subject Reduction is restated modulo logical equivalence. Since there is no computational gain in adding such congruences, we do not consider them.

2.5 Linear $\lambda$-calculus

$\lambda_{\parr}$ contains the linear $\lambda$-calculus as subsystem. On one hand, function application and variable declaration are respectively given by the rule

[TABLE]

and the axiom

[TABLE]

as usual. On the other hand, the treatment of linear implication is the main novelty of the type system of $\lambda_{\parr}$. Namely, the linear implication introduction rule is broken in two rules. The first is intuitionistic and yields functional abstraction, the second is classical and yields communication. Functional abstraction $\lambda$ is obtained by the rule:

[TABLE]

Such a rule has been studied by [17] in the context of multiple-conclusion intuitionistic linear logic. Indeed, when $x$ occurs in $t$, the term $\lambda x\,t$ is a standard linear $\lambda$-term. The application of a function to an argument generates in $\lambda_{\parr}$ the standard $\lambda$-calculus reduction

[TABLE]

where $u[t/x]$ is the term obtained from $u$ by replacing the occurrence of $x$ with $t$.

2.6 Communication

The other rule for the linear implication introduction is:

[TABLE]

In this case, the variable $x$ does not occur in $t$, therefore the term $\overline{x}.\,t$ is no more a $\lambda$-term and behaves like an output channel with continuation $t$. Namely, when $\overline{x}.\,t$ is applied to an argument $u$, a communication is triggered: the term $u$ is transmitted along the channel $x$ to another process inside $\Delta$ and will replace $x$ inside that process. We thus have in $\lambda_{\parr}$ the reduction rules:

[TABLE]

[TABLE]

where $\mathcal{C}[\;]$ and $\mathcal{D}[\;]$ are arbitrary contexts, as usual defined as follows.

Definition 2.4** (Contexts).**

A context $\mathcal{C}[\;]$ is a term containing a variable $[\;]$ occurring exactly once. For any term $t$ we denote by $\mathcal{C}[t]$ the result of replacing $[\;]$ by $t$ in $\mathcal{C}[\;]$. $\mathcal{C}[\;]$ is simple if it does not contain subterms of the form $\mathcal{D}[\;]\mid u$ or $u\mid\mathcal{D}[\;]$ .

In the reduction above, by definition of context, only one occurrence of $x$ is replaced by $u$. Therefore, if the context $\mathcal{D}[\;]$ is not simple, then the term $\mathcal{D}[x]$ is a parallel composition of several processes and only one of them will actually receive $u$. For instance, we have

[TABLE]

Unlike in pure $\pi$-calculus, the output operator $\overline{x}u.s$ may transmit its message even if it is surrounded by a potentially non-empty context. This is necessary for fully normalizing the proofs: the alternative is to give up on a full correspondence with the normalization/cut-elimination process, as done in Wadler’s typed $\pi$-calculus CP [32]. In our case, it might happen that some variable $y$ of the message $u$ lies under the scope of an operator $\lambda y$ occurring in the context. There is no problem, though: the operator $\lambda y$ is just a notation which automatically becomes $\overline{y}$, if the need arises – namely, if $y$ changes location. For instance, let us consider the natural reduction strategy that avoids to reduce under $\lambda$:

[TABLE]

If we instead first fire the communication reduction along the channel $x$, we obtain the very same result, but by a different mechanism:

[TABLE]

What happens in this second reduction is that the value of $y$, still not known during the first communication, is automatically redirected and communicated to the new location of $y$ by the second communication. Therefore, the code mobility issues created by closures, solved in [3] in a more complicated way, literally disappear in $\lambda_{\parr}$.

Similarly, the “capture” of variables during communications by output operators $\overline{x}$ creates no issue. For instance, the result of the reduction above communicating first along $x$, then along $y$:

[TABLE]

can also be obtained by communicating first along $y$, then along $x$, thus letting the variable $x$ to be captured by the $\overline{x}$ operator, which then automatically becomes $\lambda x$:

[TABLE]

2.7 Output channels without continuation

The elimination rule for the connective $\parr$ types binary output channels with no associated continuation, a kind of operator also found in the asynchronous $\pi$-calculus [8]:

[TABLE]

When $s$ is a parallel composition $u\mid v$, the term $\overline{x}\,\overline{y}\,s$ transmits $u$ and $v$ respectively along the channel $x$ and $y$ and then terminates with no value, as reflected by its type $\bot$. As a result, exactly one occurrence of $x$ will be replaced by $u$ and exactly one occurrence of $y$ will be replaced by $v$, in two different processes or in the same. The correspondent reduction rules of $\lambda_{\parr}$ are:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

The first two reduction rules concern the case in which the variables $x$ and $y$ occur in the same context. The last two address the case in which the variables $x$ and $y$ occur in two different contexts.

2.8 Process Termination

Classical logic is obtained by a combination of the classical linear implication introduction rule and the $\bot$-introduction rule:

[TABLE]

which introduces the terminated process $\circ$, which does nothing. Indeed, we can derive the linear excluded middle as follows:

$x:A\Rightarrow x:A$

$x:A\Rightarrow x:A,\,\circ:\bot$

$\Rightarrow x:A,\,\overline{x}.\,\circ:A\multimap\bot$

$\Rightarrow x\mid\overline{x}.\,\circ:A\parr(A\multimap\bot)$

Since terms of type $\bot$ return no value, we have the typing rule

[TABLE]

which introduces the construct ${\mathsf{close}}(t)$, whose intended meaning is to execute $t$ and then terminate the computation with no return value, hence it has no type.

2.9 The reduction rules of $\lambda_{\parr}$

The complete list of reduction rules of $\lambda_{\parr}$ is presented in Table 2 for the reader’s convenience.

As usual, for any context $\mathcal{C}[\;]$, we adopt the reduction scheme $\mathcal{C}[t]\mapsto\mathcal{C}[u]$ whenever $t\mapsto u$. We denote by $\mapsto^{*}$ the reflexive and transitive closure of the one-step reduction $\mapsto$. As usual, we shall employ the $\lambda$-calculus concepts of normal form and strong normalization.

Definition 2.5** (Normal Forms and Strongly Normalizable Terms).**

• •

A redex is a term $u$ such that $u\mapsto v$ for some $v$ and reduction in Table 2. A term $t$ is called a normal form or, simply, normal, if there is no $u$ such that $t\mapsto u$.

• •

A finite or infinite sequence of terms $u_{1},u_{2},\ldots,u_{n},\ldots$ is said to be a reduction of $t$, if $t=u_{1}$, and for all $i$, $u_{i}\mapsto u_{i+1}$. A term $u$ of $\lambda_{\parr}$ is normalizable if there is a finite reduction of $u$ whose last term is normal and is strong normalizable if every reduction of $u$ is finite.

3 Programming with $\lambda_{\parr}$

In order to acquire familiarity with the main features of $\lambda$, we discuss now some programming examples. Namely, we shall see how to implement client-server communication, synchronization, cyclic communication patterns and channel sharing.

Example 3.1** (Client-Server: Request/Answer).**

In this example, we discuss how to represent in $\lambda_{\parr}$ a simple communication protocol, consisting in a request/answer message exchange. A server hosts an online catalogue, mapping product names to prices. A client transmits a string $\mathsf{prod}:\mathsf{String}$ to the server, representing a product name whose price the client wishes to know. The server answers the client request by sending back the price of the product $\mathsf{prod}$, computed by the function $\mathsf{cost}:\mathsf{String}\multimap\mathbb{N}$. A naive way to implement client and server would be

[TABLE]

Although, as expected

[TABLE]

we observe that, this way, synchronization is implemented poorly. As we see below, the server may send to the client the message $(\mathsf{cost}\,x)$ before it receives any request whatsoever!

[TABLE]

What we expect, instead, is that only the request of the client can trigger computation and transmission of the answer by the server. In order to force that, the trick is to encapsulate the message $\mathsf{prod}$ into the $\lambda$-term $\lambda a\lambda b\,a\,(b\,\mathsf{prod})$, whose task is to take as input a server channel $a$, a continuation $b$ and apply the channel $a$ to $b\,\mathsf{prod}$. We thus implement client and server as follows:

[TABLE]

Since now the server output channel $\overline{y}.\,\circ$ is not applied to any argument, the server has no choice but to wait for the client request:

[TABLE]

By defining $X:=(\mathbb{N}\multimap\bot)\multimap(\mathsf{String}\multimap\mathbb{N})\multimap\bot$, we can type the process above as follows:

$x:X\Rightarrow x:X$         $\Rightarrow y:\mathbb{N},\,\overline{y}.\,\circ:\mathbb{N}\multimap\bot$

$x:X\Rightarrow y:\mathbb{N},\,x\,(\overline{y}.\,\circ):(\mathsf{String}\multimap\mathbb{N})\multimap\bot$

       $\Rightarrow\mathsf{cost}:\mathsf{String}\multimap\mathbb{N}$

$x:X\Rightarrow y:\mathbb{N},\,x\,(\overline{y}.\,\circ)\,\mathsf{cost}:\bot$

$\Rightarrow\overline{x}.\,y:X\multimap\mathbb{N},\,x\,(\overline{y}.\,\circ)\,\mathsf{cost}:\bot$

   $\Rightarrow(\lambda a\lambda b\,a\,(b\,\mathsf{prod})):X$

$\Rightarrow\overline{x}(\lambda a\lambda b\,a\,(b\,\mathsf{prod})).y:\mathbb{N},\,x\,(\overline{y}.\,\circ)\,\mathsf{cost}:\bot$

$\Rightarrow\overline{x}(\lambda a\lambda b\,a\,(b\,\mathsf{prod})).y\mid x\,(\overline{y}.\,\circ)\,\mathsf{cost}:\mathbb{N}\parr\bot$

Example 3.2** (Client-Server: Dialogue).**

We present now a continuation of the previous example which models a longer interaction. We want to represent the following transaction of an online sale. As before, a buyer transmits to a seller a product name $\mathsf{prod}:\mathsf{String}$, the seller computes by the function $\mathsf{cost}$ the monetary cost $\mathsf{price}:\mathbb{N}$ of $\mathsf{prod}$ and communicates it to the buyer. Then the buyer apply a function $\mathsf{pay}:\mathbb{N}\rightarrow\mathsf{String}$ to $\mathsf{price}$, that will transmit to the server the credit card number $\mathsf{card}:\mathsf{String}$ if the client wishes to buy the product, the empty string otherwise. By comparison with the previous example, we must add a new communication channel $\overline{z}$ for the third communication, because in $\lambda_{\parr}$ each communication requires a fresh channel. As before, in order to implement synchronization, messages $M$ will be always transmitted as $(\lambda a\lambda b\,a\,(b\,M))$:

[TABLE]

We can observe the following interaction:

[TABLE]

By defining

$X:=(Y\multimap\mathsf{String})\multimap(\mathsf{String}\multimap Y)\multimap\mathsf{String}$

$Y:=(\mathsf{String}\multimap\bot)\multimap(\mathbb{N}\multimap\mathsf{String})\multimap\bot$

we can type the process above as follows:

$x:X\Rightarrow x:X$   

$\Rightarrow z:\mathsf{String},\,\overline{z}.\,\circ:\mathsf{String}\multimap\bot$         $y:Y\Rightarrow y:Y$

$y:Y\Rightarrow y\,(\overline{z}.\,\circ):(\mathbb{N}\multimap\mathsf{String})\multimap\bot,\,z:\mathsf{String}$

$\Rightarrow y\,(\overline{z}.\,\circ):(\mathbb{N}\multimap\mathsf{String})\multimap\bot,\,\overline{y}.\,z:Y\multimap\mathsf{String}$

   $\Rightarrow\mathsf{pay}:\mathbb{N}\multimap\mathsf{String}$

$\Rightarrow y\,(\overline{z}.\,\circ)\,\mathsf{pay}:\bot,\,\overline{y}.\,z:Y\multimap\mathsf{String}$

$x:X\Rightarrow y\,(\overline{z}.\,\circ)\,\mathsf{pay}:\bot,\,x\,(\overline{y}.\,z):(\mathsf{String}\multimap Y)\multimap\mathsf{String}\qquad\Rightarrow\lambda c\lambda a^{\prime}\lambda b^{\prime}\,a^{\prime}\,(b^{\prime}\,\mathsf{cost}\,c):\mathsf{String}\multimap Y$

$x:X\Rightarrow y\,(\overline{z}.\,\circ)\,\mathsf{pay}:\bot,\,x\,(\overline{y}.\,z)(\lambda c\lambda a^{\prime}\lambda b^{\prime}\,a^{\prime}\,(b^{\prime}\,\mathsf{cost}\,c)):\mathsf{String}$

$\Rightarrow\overline{x}.\,{y\,(\overline{z}.\,\circ)\,\mathsf{pay}}:X\multimap\bot,\,x\,(\overline{y}.\,z)(\lambda c\lambda a^{\prime}\lambda b^{\prime}\,a^{\prime}\,(b^{\prime}\,\mathsf{cost}\,c)):\mathsf{String}\qquad\Rightarrow\lambda a\lambda b\,a\,(b\,\mathsf{prod}):X$

$\Rightarrow\overline{x}(\lambda a\lambda b\,a\,(b\,\mathsf{prod})).y\,(\overline{z}.\,\circ)\,\mathsf{pay}:\bot,\,\,x\,(\overline{y}.\,z)(\lambda c\lambda a^{\prime}\lambda b^{\prime}\,a^{\prime}\,(b^{\prime}\,\mathsf{cost}\,c)):\mathsf{String}$

$\Rightarrow\overline{x}(\lambda a\lambda b\,a\,(b\,\mathsf{prod})).y\,(\overline{z}.\,\circ)\,\mathsf{pay}\mid\,x\,(\overline{y}.\,z)(\lambda c\lambda a^{\prime}\lambda b^{\prime}\,a^{\prime}\,(b^{\prime}\,\mathsf{cost}\,c)):\bot\parr\mathsf{String}$

Example 3.3** (Cyclic Communication).**

Unlike in the session typed $\pi$-calculi in [9] and [32], in $\lambda_{\parr}$ one can type in a natural way cyclic communication patterns, as the following example shows. A client possesses some secret information $M:\mathsf{String}$, which it wishes to encrypt. For added security, the client desires two encryptions of the message. A couple of servers, by joining forces, offer this kind of double-encryption service. Therefore, the client sends $M$ to the first server, which encrypts $M$ by applying the function $\mathsf{enc}_{1}:\mathsf{String}\multimap\mathsf{String}$ and then transmits the result to the second server, which in turn encrypts it by applying the function $\mathsf{enc}_{2}:\mathsf{String}\multimap\mathsf{String}$ and finally transmits the result to the client. We implement client and servers as follows:

[TABLE]

We observe the following interaction:

[TABLE]

We can type the process above as follows:

$\Rightarrow z:\mathsf{String},\,\overline{z}.\,\circ:\mathsf{String}\multimap\bot$         $y:\mathsf{String}\Rightarrow\circ:\bot,\,\mathsf{enc_{2}}\,y:\mathsf{String}$

$y:\mathsf{String}\Rightarrow z:\mathsf{String},\,\circ:\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot$

$\Rightarrow z:\mathsf{String},\,\overline{y}.\,\circ:\mathsf{String}\multimap\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot$

   $x:\mathsf{String}\Rightarrow\mathsf{enc_{1}}\,x:\mathsf{String}$

$x:\mathsf{String}\Rightarrow z:\mathsf{String},\,\overline{y}(\mathsf{enc_{1}}\,x).\circ:\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot$

$\Rightarrow\overline{x}.\,z:\mathsf{String}\multimap\mathsf{String},\,\overline{y}(\mathsf{enc_{1}}\,x).\circ:\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot\qquad\Rightarrow M:\mathsf{String}$

$\Rightarrow\overline{x}M.z:\mathsf{String},\,\overline{y}(\mathsf{enc_{1}}\,x).\circ:\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot$

$\Rightarrow\overline{x}M.z\mid\overline{y}(\mathsf{enc_{1}}\,x).\circ:\mathsf{String}\parr\bot,\,\overline{z}(\mathsf{enc_{2}}\,y).\circ:\bot$

$\Rightarrow\overline{x}M.z\mid\overline{y}(\mathsf{enc_{1}}\,x).\circ\mid\overline{z}(\mathsf{enc_{2}}\,y).\circ:(\mathsf{String}\parr\bot)\parr\bot$

Example 3.4** (Channel Transmission).**

As $\pi$-calculus, $\lambda_{\parr}$ supports communication of channel names and thus dynamic communication patterns, as we see in the following example. A server offers a printing service, which is hosted on another machine, connected to the server. In order to exploit the service an access code is required. A consumer, which wants to print the string $M$, sends its access code $\mathsf{access}:\mathsf{String}$ to the server, which checks it by the function $\mathsf{check}$. Upon success, the server transmits to the consumer the channel $\overline{z}$ along which the printer offers its services, so that finally the consumer can send $M$ to the printer. We model printer, server and client as follows:

[TABLE]

We observe the following interaction:

[TABLE]

By defining $C:=((\mathsf{String}\multimap\bot)\multimap\bot)\multimap\bot$, we can type the above process as follows:

$x:\mathsf{String}\Rightarrow\mathsf{check}\,x:C\multimap C\multimap\bot$       

$y:C\Rightarrow\circ:\bot,\,y\,(\lambda a\,a\,M):\bot$

$\Rightarrow\overline{y}.\,\circ:C,\,y\,(\lambda a\,a\,M):\bot$

$x:\mathsf{String}\Rightarrow(\mathsf{check}\,x)(\overline{y}.\,\circ):C\multimap\bot,\,y\,(\lambda a\,a\,M):\bot$

$\Rightarrow(\mathsf{check}\,x)(\overline{y}.\,\circ):C\multimap\bot,\,\overline{x}.\,y\,(\lambda a\,a\,M):\mathsf{String}\multimap\bot$

   $\Rightarrow\mathsf{access}:\mathsf{String}$

$\Rightarrow(\mathsf{check}\,x)(\overline{y}.\,\circ):C\multimap\bot,\,\overline{x}\mathsf{access}.y\,(\lambda a\,a\,M):\bot\qquad\Rightarrow z\,\mathsf{print}:\bot,\overline{z}.\,\circ:C$

$\Rightarrow z\,\mathsf{print}:\bot,\,(\mathsf{check}\,x)(\overline{y}.\,\circ)(\overline{z}.\,\circ):\bot,\,\overline{x}\mathsf{access}.y\,(\lambda a\,a\,M):\bot$

$\Rightarrow z\,\mathsf{print}\mid(\mathsf{check}\,x)(\overline{y}.\,\circ)(\overline{z}.\,\circ):\bot\parr\bot,\,\overline{x}\mathsf{access}.y\,(\lambda a\,a\,M):\bot$

$\Rightarrow z\,\mathsf{print}\mid(\mathsf{check}\,x)(\overline{y}.\,\circ)(\overline{z}.\,\circ)\mid\overline{x}\mathsf{access}.y\,(\lambda a\,a\,M):(\bot\parr\bot)\parr\bot$

4 Intermezzo: Synchronous Communication in $\lambda_{\parr}$

In $\pi$-calculus the actions of both sending and receiving messages are synchronous and blocking. They are synchronous, because they require that the sender and the receiver synchronize; they are blocking, because the execution of both the sender and the receiver is blocked until the message is actually transmitted. Therefore, on one hand, if there is no receiver listening to the channel, a process can neither transmit its message along the channel nor proceed with its execution. On the other hand, a process which does listen cannot proceed with its execution until it receives the message it is waiting for. In $\pi$-calculus, synchronicity is implemented by a construct for sending $\overline{x}m.\,\_$ and a construct for receiving $x(y).\,\_$ which need to be outermost in the connected processes in order to activate the reduction:

[TABLE]

The blocking nature of the actions is implemented by forbidding to reduce inside $P$ and $Q$ before the actions are executed, that is, by forcing a reduction strategy.

Non-blocking actions have been advocated by various authors (e.g. [21], [18]) and are necessary for a full correspondence between cut-elimination and process execution. In $\lambda_{\parr}$, the fact that sending and receiving are non-blocking is implemented by just removing the input construct $x(y)$, so in $\lambda_{\parr}$ we have :

[TABLE]

provided that $x$ occurs in $Q$.

4.1 The call-by-value $\lambda_{\parr}$

Although $\lambda_{\parr}$ is naturally asynchronous, we can model synchronous and blocking actions also in $\lambda_{\parr}$, by defining reduction to automatically follow a call-by-value discipline.

Definition 4.1** (Value).**

A value is any term of one of the following forms:

[TABLE]

Definition 4.2** (Call-by-value Contexts).**

We define a call-by-value evaluation context by the following grammar:

[TABLE]

where $V$ is any value.

In order to obtain a call-by-value version of $\lambda_{\parr}$, we rewrite the main reduction rules of $\lambda_{\parr}$ as following:

[TABLE]

[TABLE]

[TABLE]

where $V$ is a value and $E,E^{\prime}$ call-by-value evaluation contexts. The idea is that call-by-value contexts bring back a notion of order among operations, which can be used to represent the sequential facet of computation. Thus a term $E^{\prime}[x]$ represents a process whose next operation is a read operation on the channel $x$, followed by the operations contained in $E^{\prime}[\;]$. Similarly to Wadler’s principal-cut-elimination strategy for CP, the $\mapsto^{cbv}$ reduction acts only on the top level parallel operators.

We can now define in $\lambda_{\parr}$ the synchronous input-construct as follows:

[TABLE]

Indeed, the term $x(y).u$ is always stuck: since $u$ is located under a $\lambda$, no reduction can be performed inside $u$; since $x$ is not a value, the redex $(\lambda y\,u)\,x$ cannot be contracted either. For similar reasons, the term $\overline{x}V.u=(\overline{x}.\,u)V$ is stuck as well: since $V$ is a value, no reduction can be performed inside $V$; since $u$ is located under an output operator, no reduction can be performed inside $u$ either. Thus, the only reduction that could be fired is the transmission of $V$ along the channel $x$, which however requires a suitable receiver, namely a process whose call-by-value evaluation cannot further proceed: the process requires an input value and waits for it. Indeed, in the following configuration, we can reduce

[TABLE]

In the configuration

[TABLE]

however, the process $\overline{x}V.u$ cannot transmit its message $V$ until $(\lambda z\,z\,x(y).w)(\lambda k\,k)$ is ready to receive, which will happen as soon as its head redex will be contracted and the value of $x(y).w$ will be really needed. Thus, after one reduction step, we have

[TABLE]

5 Soundness and Completeness

We show now that the typing system $\mathrm{NMLL}$ of $\lambda_{\parr}$ captures exactly classical multiplicative linear logic. Namely, we show that $\mathrm{NMLL}$ is equivalent to the sequent calculus $\mathrm{MLL}$ for classical multiplicative linear logic. The cut rule and the logical rules of $\mathrm{MLL}$ – namely, the rules introducing the logical connectives of linear logic on the left or on the right – are the standard double-sided sequent rules for classical linear logic. The initial sequent $\bot\Rightarrow$ corresponds to the initial sequent $\Rightarrow 1$. We use the former since we do not have an explicit duality operator. The only non-standard rule of $\mathrm{NMLL}$ is $\bot\mathrm{E}$. It is clearly sound since it captures the neutrality of $\bot$ with respect to $\parr$, and hence to the comma on the right-hand side of sequents. As we will see in the completeness proof, the rule $\bot\mathrm{E}$ is key in handling the occurrences of $\bot$ introduced by the rules $\parr\mathrm{E}$.

Proposition 5.1** (Soundness).**

For any sequent $S=\Gamma\Rightarrow\Delta$, if $S$ is derivable in $\mathrm{NMLL}$, then $S$ is derivable in $\mathrm{MLL}$.

Proof.

We proceed by induction on the number of rule applications in the $\mathrm{NMLL}$ derivation of $S$. Since the term assignment of the logical inferences is irrelevant for the argument, we ignore it in the present proof.

If no rule is applied in the derivation, then $S=A\Rightarrow A$, which is an initial sequents of $\mathrm{MLL}$.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $n$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation containing $n+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation.

• •

$\Gamma\Rightarrow\Delta,\bot\Gamma\Rightarrow\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow\Delta$ is derivable in $\mathrm{MLL}$. Then by the same application of the $\bot$ rule we can derive $\Gamma\Rightarrow\Delta,\bot$ also in $\mathrm{MLL}$.

• •

$\Gamma\Rightarrow\Delta\Gamma\Rightarrow\Delta,\bot$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow\Delta,\bot$ is derivable in $\mathrm{MLL}$. Then by

[TABLE]

we can derive $\Gamma\Rightarrow\Delta$ also in $\mathrm{MLL}$.

• •

$\Gamma,\Sigma\Rightarrow B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow A\multimap B,\Delta\Sigma\Rightarrow A,\Theta$

. Since the derivations of the premises of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow A\multimap B,\Delta$ and $\Sigma\Rightarrow A,\Theta$ are derivable in $\mathrm{MLL}$. By

[TABLE]

we can derive $\Gamma,\Sigma\Rightarrow B,\Delta,\Theta$ in $\mathrm{MLL}$.

• •

$\Gamma\Rightarrow A\multimap B,\Delta\Gamma,A\Rightarrow B,\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma,A\Rightarrow B,\Delta$ is derivable in $\mathrm{MLL}$. By the rule application

[TABLE]

we can derive $\Gamma\Rightarrow A\multimap B,\Delta$ in $\mathrm{MLL}$.

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow A\parr B,\Delta\Sigma_{1},A\Rightarrow\Theta_{1}\Sigma_{2},B\Rightarrow\Theta_{2}$

. Since the derivations of the premises of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow A\parr B,\Delta$ and $\Sigma_{1},A\Rightarrow\Theta_{1}$ and $\Sigma_{2},B\Rightarrow\Theta_{2}$ are derivable in $\mathrm{MLL}$. By the rule application

[TABLE]

we can derive $\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\bot,\Delta,\Theta_{1},\Theta_{2}$ in $\mathrm{MLL}$.

• •

$\Gamma\Rightarrow A\parr B,\Delta\Gamma\Rightarrow A,B,\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma,A\Rightarrow A,B,\Delta$ is derivable in $\mathrm{MLL}$. By the rule application

[TABLE]

we can derive $\Gamma\Rightarrow A\parr B,\Delta$ in $\mathrm{MLL}$.

∎

The natural deduction calculus $\mathrm{NMLL}$ corresponds very neatly to the sequent calculus $\mathrm{MLL}$. Hence, a completeness proof of $\mathrm{NMLL}$ with respect to $\mathrm{MLL}$ is quite straightforward. The proof deviates from standard reasoning only insofar as we need to handle the occurrences of $\bot$ introduced by $\parr\mathrm{E}$. We counterbalance this introductions of $\bot$ by applying the rule $\bot\mathrm{E}$.

Proposition 5.2** (Completeness).**

For any sequent $S=\Gamma\Rightarrow\Delta$, if $S$ is derivable in $\mathrm{MLL}$, then $\Gamma\Rightarrow\Delta$ is derivable in $\mathrm{NMLL}$.

Proof.

We first remark that the restriction on $\mathrm{NMLL}$ rule applications can always be bypassed by renaming the variables in the premises, so that the set of variables used in each premise is disjoint from the set of variables used in any other premise. Therefore, we ignore the term assignment also in the present proof. We proceed by induction on the number of rule applications in the $\mathrm{MLL}$ derivation of $S$.

If no rule is applied in the derivation, then either $S=\;A\Rightarrow A$, which is an initial sequent of $\mathrm{NMLL}$, or $S=\bot\Rightarrow\;$. Since in $\mathrm{NMLL}$ we can derive

[TABLE]

the claim holds.

Suppose now that the statement holds for any $\mathrm{MLL}$ derivation containing $n$ or less rule applications, we show the result for a generic $\mathrm{MLL}$ derivation containing $n+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{MLL}$ derivation.

• •

$\Gamma\Rightarrow\Delta,\bot\Gamma\Rightarrow\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow\Delta$ is derivable in $\mathrm{NMLL}$. Then by the same application of the $\bot$ rule we can derive $\Gamma\Rightarrow\Delta$ also in $\mathrm{NMLL}$.

• •

$\Gamma,\Sigma,A\multimap B\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow A,\Delta\Sigma,B\Rightarrow\Theta$

. Since the derivations of the premises of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow A,\Delta$ and $\Sigma,B\Rightarrow\Theta$ are derivable in $\mathrm{NMLL}$. By

[TABLE]

we can derive $\Gamma,\Sigma,A\multimap B\Rightarrow\Delta,\Theta$ in $\mathrm{NMLL}$.

• •

$\Gamma\Rightarrow A\multimap B,\Delta\Gamma,A\Rightarrow B,\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma,A\Rightarrow B,\Delta$ is derivable in $\mathrm{NMLL}$. By the rule application

[TABLE]

we can derive $\Gamma\Rightarrow A\multimap B,\Delta$ in $\mathrm{NMLL}$.

• •

$\Gamma,\Sigma,A\parr B\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma,A\Rightarrow\Delta\Sigma,B\Rightarrow\Theta$

. Since the derivations of the premises of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma,A\Rightarrow\Delta$ and $\Sigma,B\Rightarrow\Theta$ are derivable in $\mathrm{NMLL}$. By the rule application

[TABLE]

we can derive $\Gamma,\Sigma,A\parr B\Rightarrow\Delta,\Theta$ in $\mathrm{NMLL}$.

• •

$\Gamma\Rightarrow A\parr B,\Delta\Gamma\Rightarrow A,B,\Delta$

. Since the derivation of the premise of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow A,B,\Delta$ is derivable in $\mathrm{NMLL}$. By a rule application

[TABLE]

we can derive $\Gamma\Rightarrow A\parr B,\Delta$ in $\mathrm{NMLL}$.

• •

$\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow A,\Delta\Sigma,A\Rightarrow\Theta$

. Since the derivations of the premises of the rule contain $n$ or less rule applications, by inductive hypothesis we know that $\Gamma\Rightarrow A,\Delta$ and $\Sigma,A\Rightarrow\Theta$ are derivable in $\mathrm{NMLL}$. By

[TABLE]

we can derive $\Gamma,\Sigma\Rightarrow\Delta,\Theta$ in $\mathrm{NMLL}$.

∎

6 Subject Reduction

We are now going to prove that the reductions of $\lambda_{\parr}$ preserve the typing of terms, property well-known under the name of Subject Reduction.

We first need the concept of substitution, which in $\lambda_{\parr}$ is just a replacement of some variables, with no renaming involved.

Definition 6.1** (Substitution).**

For any multiset of typed terms $\Delta$ and terms $v_{1},\ldots,v_{n}$, we denote by $\Delta[v_{1}/x_{1}\;\;\ldots\;\;v_{n}/x_{n}]$ the simultaneous replacement, for any $i\in\{1,\ldots,n\}$, of all occurrences of $x_{i}$ in all terms of $\Delta$ by $v_{i}$. Given a substitution $[t/x]$, we refer to $t$ as the substituting term and to $x$ as the substituted variable.

In order to prove Subject Reduction, we first prove that if we have a variable $x:A$ in the context of a derivable sequent $\Gamma,x:A\Rightarrow\Delta$ and we can type a term $t:A$ by deriving a sequent $\Sigma\Rightarrow t:A,\Theta$, then we can derive the sequent $\Gamma,\Sigma\Rightarrow\Delta[t/x],\Theta$ effectively replacing the variable $x:A$ with the term $t:A$. The proof-theoretical intuition is the following: if $A$ is among the assumptions of a proof, and we have a derivation $t$ of $A$, then we can use $t$ to derive $A$ directly inside the proof.

Lemma 6.1** (Substitution).**

If $\Sigma\Rightarrow t:A,\Theta$ and $\Gamma,x:A\Rightarrow\Delta$ are derivable in $\mathrm{NMLL}$ and share no variable, then $\Gamma,\Sigma\Rightarrow\Delta[t/x],\Theta$ is derivable in $\mathrm{NMLL}$ as well.

Proof.

We proceed by induction on the number of rule applications in the derivation of $\Gamma,x:A\Rightarrow\Delta$.

If no rule is applied in the derivation, then $\Gamma,x:A\Rightarrow\Delta$ is of the form $x:A\Rightarrow x:A$. Therefore, $\Gamma,\Sigma\Rightarrow\Delta[t/x],\Theta$ is just $\Sigma\Rightarrow t:A,\Theta$ and the claim trivially holds.

Suppose now that the statement holds for any sequent which is derivable with $n$ or less rule applications, we show the result for any sequent $\Gamma,x:A\Rightarrow\Delta$ which is derivable using $n+1$ rule applications. We reason by cases on the last rule applied in this derivation of $\Gamma,x:A\Rightarrow\Delta$.

• •

$\Gamma,x:A\Rightarrow\Delta^{\prime},\circ:\bot\Gamma,x:A\Rightarrow\Delta^{\prime}$

where $\Delta=\Delta^{\prime},\circ:\bot$. By inductive hypothesis $\Gamma,\Sigma\Rightarrow\Delta^{\prime}[t/x],\Theta$ is derivable. By applying

[TABLE]

we obtain a derivation of $\Gamma,\Sigma\Rightarrow\Delta[t/x],\Theta$, which verifies the claim.

• •

$\Gamma_{1},\Gamma_{2}\Rightarrow vw:C,\Delta_{1},\Delta_{2}\lx@proof@logical@and\Gamma_{1}\Rightarrow v:B\multimap C,\Delta_{1}\Gamma_{2}\Rightarrow w:B,\Delta_{2}$

where $\Delta=vw:C,\Delta_{1},\Delta_{2}$. Suppose that $x:A$ is contained in $\Gamma_{1}$ and hence that $\Gamma_{1}=\Gamma_{1}^{\prime},x:A$ and that $\Gamma=\Gamma_{1}^{\prime},\Gamma_{2}$. The case in which $x:A$ is contained in $\Gamma_{2}$ is analogous. By inductive hypothesis $\Gamma_{1}^{\prime},\Sigma\Rightarrow v[t/x]:B\multimap C,\Delta_{1}[t/x],\Theta$ is derivable. Now, due to the type assignment rules of $\mathrm{NMLL}$ and since $x:A$ is contained in $\Gamma_{1}$, we have that $x$ cannot occur in $w$. By hypothesis, $t$ and $\Theta$ share no variable with $\Gamma_{2},w,\Delta_{2}$. Hence, by applying

[TABLE]

we obtain a derivation of $\Gamma,\Sigma\Rightarrow(vw)[t/x]:C,\Delta[t/x],\Theta$, which verifies the claim.

• •

$\Gamma\Rightarrow\overline{y}.\,s:B\multimap C,\Delta^{\prime}\Gamma,y:B\Rightarrow s:C,\Delta^{\prime}$

where $\Delta=\overline{y}.\,s:B\multimap C,\Delta^{\prime}$. Since $x:A$ must occur in $\Gamma$ in the conclusion of the rule application, we know that $x\neq y$. By inductive hypothesis, $\Gamma,y:B,\Sigma\Rightarrow s[t/x]:C,\Delta^{\prime}[t/x],\Theta$ is derivable. Hence, since by hypothesis $y$ does not occur in $t$, by applying

[TABLE]

we obtain a derivation of $\Gamma,\Sigma\Rightarrow(\overline{y}.\,s)[t/x]:B\multimap C,\Delta^{\prime}[t/x],\Theta$, which verifies the claim.

• •

$\Gamma_{1},\Gamma_{2},\Gamma_{3}\Rightarrow\overline{y}\,\overline{z}\,t:\bot,\Delta_{1},\Delta_{2},\Delta_{3}\lx@proof@logical@and\Gamma_{1}\Rightarrow s:B\parr C,\Delta_{1}\Gamma_{2},y:B\Rightarrow\Delta_{2}\Gamma_{3},z:C\Rightarrow\Delta_{3}$

where $\Delta=\overline{y}\,\overline{z}\,t:\bot,\Delta_{1},\Delta_{2},\Delta_{3}$. Suppose that $x:A$ is contained in $\Gamma_{1}$ and hence that $\Gamma_{1}=\Gamma_{1}^{\prime},x:A$ and that $\Gamma=\Gamma_{1}^{\prime},\Gamma_{2},\Gamma_{3}$. The case in which $x:A$ is contained in $\Gamma_{2}$ or in $\Gamma_{3}$ are analogous. By inductive hypothesis $\Gamma_{1},\Sigma\Rightarrow s[t/x]:B\parr C,\Delta_{1}[t/x],\Theta$ is derivable. By hypothesis, $t,\Theta$ and $\Gamma_{2},y:B,\Delta_{2}$ and $\Gamma_{3},z:C,\Delta_{3}$ share no variable. Therefore, by applying

[TABLE]

we obtain a derivation of $\Gamma,\Sigma\Rightarrow(\overline{y}\,\overline{z}\,s)[t/x]:\bot,\Delta[t/x],\Theta$, which verifies the claim.

• •

$\Gamma,x:A\Rightarrow v\mid w:B\parr C,\Delta^{\prime}\Gamma,x:A\Rightarrow v:B,w:C,\Delta^{\prime}$

where $\Delta=v\mid w:B\parr C,\Delta^{\prime}$. By inductive hypothesis $\Gamma,\Sigma\Rightarrow v[t/x]:B,w[t/x]:C,\Delta^{\prime}[t/x],\Theta$ is derivable. By applying

[TABLE]

we obtain a derivation of $\Gamma,\Sigma\Rightarrow(v\mid w)[t/x]:B\parr C,\Delta^{\prime}[t/x],\Theta$, which verifies the claim.

∎

The proof of the Subject Reduction is now quite standard.

Theorem 6.2** (Subject Reduction).**

Assume there is a $\mathrm{NMLL}$ derivation of $\Pi\Rightarrow t_{1}:F_{1},\ldots,t_{n}:F_{n},t_{n+1},\dots,t_{m}$. If $t_{1}\mid\ldots\mid t_{m}\ \mapsto t_{1}^{\prime}\mid\ldots\mid t_{m}^{\prime}$, then there is a derivation of $\Pi\Rightarrow\Phi,t_{1}^{\prime}:F_{1},\ldots,t_{n}^{\prime}:F_{n},t_{n+1}^{\prime},\ldots,t_{m}^{\prime}$.

Proof.

We prove the statement by induction on the number of rule applications in the derivation of $\Pi\Rightarrow t_{1}:F_{1},\ldots,t_{n}:F_{n},t_{n+1},\dots,t_{m}$.

If no rule is applied in the derivation, then $\Pi\Rightarrow t_{1}:F_{1},\ldots,t_{n}:F_{n},t_{n+1},\dots,t_{m}$ is of the form $x:A\Rightarrow x:A$ and the claim holds. Since no reduction applies to any term in the right-hand side of the sequents, the claim trivially holds.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $m$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation of $\Pi\Rightarrow t_{1}:F_{1},\ldots,t_{n}:F_{n},t_{n+1},\dots,t_{m}$ containing $m+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation.

• •

$\Gamma,\Sigma\Rightarrow\overline{x}w.v:B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\overline{x}.\,v:A\multimap B,\Delta\Sigma\Rightarrow w:A,\Theta$

where

[TABLE]

and

[TABLE]

since $x$ occurs only once.

• –

If the last rule applied above $\Gamma\Rightarrow\overline{x}.\,v:A\multimap B,\Delta$ is

[TABLE]

then, by the restriction on $\mathrm{NMLL}$ rule applications, $x$ occurs either in $v$ or in $\Delta$, by Lemma 6.1 applied to the sequents $\Sigma\Rightarrow w:A,\Theta$ and $\Gamma,x:A\Rightarrow v:B,\Delta$ we obtain that $\Gamma,\Sigma\Rightarrow v[w/x]:B,\Delta[w/x],\Theta$ is derivable and hence that we have a derivation of $\Pi\Rightarrow t_{1}^{\prime}:F_{1},\ldots,t_{n}^{\prime}:F_{n},t_{n+1}^{\prime},\dots,t_{m}^{\prime}$.

• –

Otherwise, we have

[TABLE]

where $\overline{x}.\,v:A\multimap B$ only occurs in one of the premises of $\rho$ – we display it in the first premise without loss of generality.

If we construct the following derivation

[TABLE]

we know without loss of generality that

[TABLE]

and that

[TABLE]

because $x$ occurs either in $v$ or in $\Psi_{1}$. By inductive hypothesis, there is a derivation of

[TABLE]

[TABLE]

By assumption we have

[TABLE]

Therefore, by inspection of the rules of $\mathrm{NMLL}$, it is easy to see that by the rule application

[TABLE]

we obtain a derivation of the sequent

[TABLE]

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,(v\mid w):\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow v\mid w:A\parr B,\Delta\Sigma_{1},x:A\Rightarrow\Theta_{1}\Sigma_{2},y:B\Rightarrow\Theta_{2}$

where

[TABLE]

and

[TABLE]

• –

If the last rule applied above $\Gamma\Rightarrow v\mid w:A\parr B,\Delta$ is

[TABLE]

By the application of Lemma 6.1 to the sequents $\Gamma\Rightarrow v:A,w:B,\Delta$ and $\Sigma_{1},x:A\Rightarrow\Theta_{1}$ we obtain that $\Gamma,\Sigma_{1}\Rightarrow w:B,\Delta,\Theta_{1}[v/x]$ is derivable. Furthermore, by applying Lemma 6.1 to the sequents $\Gamma,\Sigma_{1}\Rightarrow w:B,\Delta,\Theta_{1}[v/x]$ and $\Sigma_{2},y:B\Rightarrow\Theta_{2}$ we obtain that $\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\Delta,\Theta_{1}[v/x],\Theta_{2}[w/y]$. Since $x$ occurs in $\Theta_{1}$ and $y$ occurs in $\Theta_{2}$, we can construct a derivation of $\Pi\Rightarrow t_{1}^{\prime}:F_{1},\ldots,t_{n}^{\prime}:F_{n},t_{n+1}^{\prime},\ldots,t_{m}^{\prime}$ by applying $\bot\mathrm{I}$.

• –

Otherwise, we have

[TABLE]

where $v\mid w:A\parr B$ only occurs in one of the premises of $\rho$ – we display it in the first premise without loss of generality.

If we construct the following derivation

[TABLE]

we know without loss of generality that

[TABLE]

and that

[TABLE]

because $x$ and $y$ occur in $\Theta_{1}$ and $\Theta_{2}$ respectively. By inductive hypothesis, there is a derivation of

[TABLE]

By assumption

[TABLE]

Therefore, by the rule application

[TABLE]

we have a derivation of the sequent

[TABLE]

• •

In all other cases, the term $\overline{x}w.v$ (or $\overline{x}\,\overline{y}\,v$) that triggered the reduction $t_{1}\mid\ldots\mid t_{m}\mapsto t_{1}^{\prime}\mid\ldots\mid t_{m}^{\prime}$ already occurs in the premises of the last rule $\rho$ applied in the $\mathrm{NMLL}$ derivation of $\Pi\Rightarrow t_{1}:F_{1},\ldots,t_{n}:F_{n},t_{n+1},\ldots,t_{m}$.

According to the typing rules, no variable can occur in different premises of the same rule application. Therefore, both the term $\overline{x}w.v$ (respectively $\overline{y}\,\overline{z}\,v$) and the variable $x$ (respectively $y$ and $z$) occur inside the same premise of the last rule application

[TABLE]

in the derivation of

[TABLE]

Without loss of generality, we assume that $x$ (or $y$ and $z$) occurs in the premise

[TABLE]

By reducing the redex triggered by $\overline{x}w.v$ or $\overline{x}\,\overline{y}\,v$ in the term $u_{1}\mid\ldots\mid u_{p}$ we have $u_{1}\mid\ldots\mid u_{p}\mapsto u_{1}^{\prime}\mid\ldots\mid u_{p}^{\prime}$. By inductive hypothesis, there is a derivation of $\Gamma\Rightarrow u_{1}^{\prime}:G_{1},\ldots,u_{p}^{\prime}:G_{p}$. Now, by inspection of $\mathrm{NMLL}$ typing rules, we can easily see that $t_{1}\mid\ldots\mid t_{m}$ is of the form $\mathcal{D}[\;\mathcal{C}_{1}[u_{1}]\mid\ldots\mid\mathcal{C}_{p}[u_{p}]\;]$ and by assumption

[TABLE]

Therefore, by inspection of the rules of $\mathrm{NMLL}$, it is easy to see that by the application of $\rho$

[TABLE]

to the root of the derivation of $\Gamma\Rightarrow u_{1}^{\prime}:G_{1},\ldots,u_{p}^{\prime}:G_{p}$, we obtain a derivation of

[TABLE]

∎

7 Progress

We show now that $\lambda_{\parr}$ is deadlock-free: if a process contains a potential communication, then the term is not normal and the communication will be carried out. In $\lambda_{\parr}$, potential communications are represented by subterms of the form $\overline{x}v.w$or $\overline{x}\,\overline{y}\,v$. Indeed, the presence of one of such subterms in a process means that the process can use a communication channel $x$ – or a pair of channels $x$ and $y$ – to transmit a message $v$. Technically, then, we need to show that if such a subterm occurs in a term, there is also a receiver, hence the term is not normal. We start by showing some properties of the distribution of variables inside $\mathrm{NMLL}$ sequents and inside typed $\lambda_{\parr}$-terms

Proposition 7.1** (Linearity of Channels).**

Assume $\Gamma\Rightarrow\Delta$ is derivable in $\mathrm{NMLL}$ and let $x$ be any variable. Then:

• •

if $x$ occurs in $\Gamma$, then $x$ occurs exactly once in $\Delta$ and $\overline{x}$ does not occur in $\Delta$;

• •

if $x$ does not occur in $\Gamma$, but occurs in $\Delta$, then $x$ occurs exactly once as $x$ and exactly once as $\overline{x}$ in $\Delta$.

Proof.

By straightforward induction on the length of the derivation of $\Gamma\Rightarrow\Delta$. ∎

We recall that by Definition 2.4 a simple context $\mathcal{C}[\;]$ is a process which is not a direct parallel composition of simpler processes. A crucial property of simple contexts that we are going to obtain now is the following: if $\mathcal{C}[\overline{z}u.v]$ is typable and $\mathcal{C}[\;]$ is simple, then the variable $z$ cannot occur in $\mathcal{C}[\;]$. If such a configuration were possible, we might type $\lambda_{\parr}$-terms like

[TABLE]

and we would have to choose between allowing components of the same process reduction to communicate

[TABLE]

or tolerating a deadlock. Fortunately, the next proposition rules out this scenery.

Proposition 7.2**.**

Suppose $\Phi\Rightarrow\mathcal{C}[u]:F,\Pi$ or $\Phi\Rightarrow\mathcal{C}[u],\Pi$ is derivable in $\mathrm{NMLL}$. Then, if $\mathcal{C}[\;]$ is simple and the variable $\overline{z}$ occurs in $u$, then $z$ does not occur in $\mathcal{C}[\;]$.

Proof.

We prove the statement by induction on the number of rule applications in the derivation of $\Phi\Rightarrow\mathcal{C}[u]:F,\Pi$ or $\Phi\Rightarrow\mathcal{C}[u],\Pi$.

If $\mathcal{C}[\;]$ is empty, we are done.

If no rule is applied in the derivation, then $\Phi\Rightarrow\mathcal{C}[u]:F,\Pi$ or $\Phi\Rightarrow\mathcal{C}[u],\Pi$ is of the form $x:A\Rightarrow x:A$, thus $u=x$ and $\mathcal{C}[\;]$ is empty, therefore the claim trivially holds.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $m$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation containing $m+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation. We may assume that the term $\mathcal{C}[u]$ does not occur in any premise of this last rule, otherwise we just apply the inductive hypothesis to any premise containing $\mathcal{C}[u]$ and obtain the thesis.

• •

$\Gamma\Rightarrow\Delta,\circ:\bot\Gamma\Rightarrow\Delta$

. Since $\mathcal{C}[u]$ occurs in $\Delta$, this case is ruled out by our assumption that $\mathcal{C}[u]$ does not occur in $\Gamma\Rightarrow\Delta$.

• •

$\Gamma\Rightarrow\Delta,{\mathsf{close}}(t)\Gamma\Rightarrow\Delta,t:\bot$

. By our assumption, it must be the case that $\mathcal{C}[u]={\mathsf{close}}(t)$. If $\mathcal{C}[\;]={\mathsf{close}}([\;])$, surely $z$ does not occur in $\mathcal{C}[\;]$. If $\mathcal{C}[\;]={\mathsf{close}}(\mathcal{D}[\;])$, with $t=\mathcal{D}[u]$, then by inductive hypothesis, $z$ does not occur in $\mathcal{D}[\;]$, thus it does not occur in $\mathcal{C}[\;]={\mathsf{close}}(\mathcal{D}[\;])$ either.

• •

$\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow t:A\multimap B,\Delta\Sigma\Rightarrow s:A,\Theta$

. By our assumption, it must be the case that $\mathcal{C}[u]=ts$. Therefore, $t=\mathcal{D}[u]$ or $s=\mathcal{D}[u]$, with respectively $\mathcal{C}[\;]=\mathcal{D}[\;]\,s$ and $\mathcal{C}[\;]=t\,\mathcal{D}[\;]$. By inductive hypothesis, $z$ does not occur in $\mathcal{D}[\;]$. Moreover, since the premises of the typing rule share no variable, $z$ cannot occur respectively in $s$ and $t$. Therefore, $z$ does not occur in $\mathcal{C}[\;]$.

• •

$\Gamma\Rightarrow\overline{x}.\,t:A\multimap B,\Delta\Gamma,x:A\Rightarrow t:B,\Delta$

. By our assumption, it must be the case that $\mathcal{C}[u]=\overline{x}.\,t$. Therefore, $t=\mathcal{D}[u]$ and $\mathcal{C}[\;]=\overline{x}.\,\mathcal{D}[\;]$. By inductive hypothesis, $z$ does not occur in $\mathcal{D}[\;]$. Moreover, $z\neq x$, otherwise $\overline{z}$ would occur twice in $\overline{x}.\,t$, contradicting Proposition 7.1. Therefore, $z$ does not occur in $\mathcal{C}[\;]=\overline{x}.\,\mathcal{D}[\;]$.

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow t:A\parr B,\Delta\Sigma_{1},x:A\Rightarrow\Theta_{1}\Sigma_{2},y:B\Rightarrow\Theta_{2}$

. By our assumption, it must be the case that $\mathcal{C}[u]=\overline{x}\,\overline{y}\,t$. Therefore, $t=\mathcal{D}[u]$ and $\mathcal{C}[\;]=\overline{x}\,\overline{y}\,\mathcal{D}[\;]$. By inductive hypothesis, $z$ does not occur in $\mathcal{D}[\;]$. Moreover, $z\neq x,y$, otherwise $\overline{z}$ would occur twice in $\overline{x}\,\overline{y}\,t$, contradicting Proposition 7.1. Therefore $z$ does not occur in $\mathcal{C}[\;]=\overline{x}\,\overline{y}\,\mathcal{D}[\;]$.

• •

$\Gamma\Rightarrow t\mid s:A\parr B,\Delta\Gamma\Rightarrow t:A,s:B,\Delta$

. We claim that this case is not possible. Indeed, if it were, by our assumption we would have $\mathcal{C}[u]=t\mid s$. Therefore $t=\mathcal{D}[u]$ or $s=\mathcal{D}[u]$, with respectively $\mathcal{C}[\;]=\mathcal{D}[\;]\mid s$ and $\mathcal{C}[\;]=t\mid\mathcal{D}[\;]$. Since by Definition 2.4 the context $\mathcal{C}[\;]$ would not be simple, we would have a contradiction.

∎

It is now easy to show that if a communication is possible, it will be carried out: if a typable $\lambda_{\parr}$-term contains output channels ready to transmit messages, then it can always perform the communication, because there is always a suitable receiver.

Theorem 7.3** (Progress).**

**

Suppose

[TABLE]

is derivable in $\mathrm{NMLL}$. Then the term $\mathcal{C}[\overline{x}v.u]\mid t_{1}\mid\ldots\mid t_{m}$ is not normal. 2. 2.

Suppose

[TABLE]

is derivable in $\mathrm{NMLL}$. Then the term $\mathcal{C}[\overline{x}\,\overline{y}\,u]\mid t_{1}\mid\ldots\mid t_{m}$ is not normal.

Proof.

1. By Proposition 7.1, $\overline{x}$ and $x$ must occur exactly once in the term $\mathcal{C}[\overline{x}v.u]\mid t_{1}\mid\ldots\mid t_{m}$. If $x$ occurs in some $t_{i}$, then a reduction is possible and we are done. We assume therefore that $x$ occurs in $\mathcal{C}[\overline{x}v.u]$. We also assume $\mathcal{C}[\;]$ is empty, otherwise $x$ occurs in $u$, hence $\overline{x}v.u=(\lambda x\,u)v$, which is not normal and we are done.

We claim now that $\mathcal{C}[\overline{x}v.u]$ has a subterm of the form $\mathcal{E}[\overline{x}v.u]\mid\mathcal{D}[x]$ or $\mathcal{D}[x]\mid\mathcal{E}[\overline{x}v.u]$, which implies a communication reduction is possible, allowing us to conclude the proof. We prove our claim by induction on $\mathcal{C}[\overline{x}v.u]$.

If $\mathcal{C}[\overline{x}v.u]=\overline{z}.\,\mathcal{C}^{\prime}[\overline{x}v.u]$ or $\mathcal{C}[\overline{x}v.u]=\overline{y}\,\overline{z}\,{\mathcal{C}^{\prime}[\overline{x}v.u]}$ or $\mathcal{C}[\overline{x}v.u]={\mathsf{close}}(\mathcal{C}^{\prime}[\overline{x}v.u])$, then we apply the induction hypothesis on $\mathcal{C}^{\prime}[\overline{x}v.u]$, and we are done.

If $\mathcal{C}[\overline{x}v.u]=w\,\mathcal{C}^{\prime}[\overline{x}v.u]$ or $\mathcal{C}[\overline{x}v.u]=\mathcal{C}^{\prime}[\overline{x}v.u]\,w$, then by Proposition 7.2, $x$ must occur in $\mathcal{C}^{\prime}[\overline{x}v.u]$, hence we apply the induction hypothesis on $\mathcal{C}^{\prime}[\overline{x}v.u]$, and we are done.

If $\mathcal{C}[\overline{x}v.u]=\mathcal{C}^{\prime}[\overline{x}v.u]\mid w$ or $\mathcal{C}[\overline{x}v.u]=w\mid\mathcal{C}^{\prime}[\overline{x}v.u]$, then if $x$ occurs in $w$, we are done. Otherwise, we apply the induction hypothesis on $\mathcal{C}^{\prime}[\overline{x}v.u]$, and concluding the proof of the claim.

2. By Proposition 7.1, $\overline{x}$ and $x$ must occur both exactly once in the term $\mathcal{C}[\overline{x}\,\overline{y}\,u]\mid t_{1}\mid\ldots\mid t_{m}$ and so do $\overline{y}$ and $y$. By inspection of the inference rules of $\mathrm{NMLL}$ it is easy to see that $x,y$ cannot occur in $u$, therefore they occur in some $t_{i}$. Thus, a reduction is possible. ∎

8 The Subformula Property

We show in this section that each normal $\lambda_{\parr}$-term corresponds to an analytic derivation. In other words, the type of each subterm of any normal $\lambda_{\parr}$-term $t$ is either a subformula of the type of $t$ or a subformula of the types of the variables of $t$. This Subformula Property guarantees that, proof-theoretically, the reduction rules of $\lambda_{\parr}$ give rise to a complete detour removal procedure, hence we can conclude they are also satisfactory from the logical point of view. Indeed, without this property is not possible to relate normalization to cut-elimination, as a normal proof without the subformula property cannot be translated in to a cut-free proof to begin with. Our multiple-conclusion natural deduction system can then be considered as a well-behaved alternative to sequent calculus for and proof-nets for multiplicative linear logic.

We start off by defining what it means for a derivation to be in normal form.

Definition 8.1** (Normal form).**

An $\mathrm{NMLL}$ derivation of a sequent $\Gamma\Rightarrow t_{1}:T_{1},\ldots,t_{n}:T_{n},t_{n+1},\ldots,t_{m}$ is in normal form if the term $t_{1}\mid\ldots\mid t_{m}$ is in normal form.

We then recall the notion of stack [19]. From a logical perspective, a stack represents a series of elimination rules.

Definition 8.2** (Stack).**

A stack is a possibly empty sequence $\sigma=\xi_{1}\xi_{2}\ldots\xi_{n}$ such that for every $1\leq i\leq n$, $\xi_{i}=t$, with $t$ term of $\mathrm{NMLL}$. If $t$ is a proof term, $t\,\sigma$ denotes as usual the term $(((t\,\xi_{1})\,\xi_{2})\ldots\xi_{n})$.

Before proving the Subformula Property, we need to establish two auxiliary results concerning the shape of terms. The first of these two results guarantees that the expected connection between the shape of a term with its type holds.

Proposition 8.1** (Type coherence).**

If $\Gamma\Rightarrow t:F,\Delta$ is derivable in $\mathrm{NMLL}$ and $t$ is a value, then one of the following holds:

• •

$t=\overline{x}.\,t$* and $F=A\multimap B$*

• •

$t=s\mid t$* and $F=A\parr B$*

for some types $A$ and $B$.

Proof.

We prove the statement by induction on the number of rule applications in the derivation of $\Gamma\Rightarrow t:F,\Delta$.

If no rule is applied in the derivation, then $\Gamma\Rightarrow t:F,\Delta$ is of the form $x:A\Rightarrow x:A$ and the claim trivially holds.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $m$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation containing $m+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation.

• •

$\Gamma\Rightarrow\Delta,\circ:\bot\Gamma\Rightarrow\Delta$

. By inductive hypothesis the claim holds for any value occurring in $\Gamma\Rightarrow\Delta$. Since $\circ$ is not a value, the claim holds also for any value occurring in $\Gamma\Rightarrow\Delta,\circ:\bot$.

• •

$\Gamma\Rightarrow\Delta,{\mathsf{close}}(t)\Gamma\Rightarrow\Delta,t:\bot$

. By inductive hypothesis the claim holds for any value occurring in $\Gamma\Rightarrow\Delta$. Since ${\mathsf{close}}(t)$ is not a value, the claim holds also for any value occurring in $\Gamma\Rightarrow\Delta,{\mathsf{close}}(t)$.

• •

$\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow t:A\multimap B,\Delta\Sigma\Rightarrow s:A,\Theta$

. By inductive hypothesis the claim holds for any value occurring in $\Gamma\Rightarrow t:A\multimap B,\Delta$ and $\Sigma\Rightarrow s:A,\Theta$. Since $ts$ is not a value, the claim holds for all values in $\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta$ as well.

• •

$\Gamma\Rightarrow\overline{x}.\,t:A\multimap B,\Delta\Gamma,x:A\Rightarrow t:B,\Delta$

. By inductive hypothesis the claim holds for any value occurring in $\Gamma,A\Rightarrow B,\Delta$. Since the value $\overline{x}.\,t:A\multimap B$ has the required type, the claim holds for all values in $\Gamma\Rightarrow\overline{x}.\,\,t:A\multimap B,\Delta$ as well.

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow t:A\parr B,\Delta\Sigma_{1},x:A\Rightarrow\Theta_{1}\Sigma_{2},y:B\Rightarrow\Theta_{2}$

.

By inductive hypothesis the claim holds for any value occurring in $\Gamma\Rightarrow t:A\parr B,\Delta$ and $\Sigma_{1},x:A\Rightarrow\Theta_{1}$ and $\Sigma_{2},y:B\Rightarrow\Theta_{2}$. Since $\overline{x}\,\overline{y}\,t:\bot$ is not a value, the claim holds for all values in $\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}$ as well.

• •

$\Gamma\Rightarrow t\mid s:A\parr B,\Delta\Gamma\Rightarrow t:A,s:B,\Delta$

. By inductive hypothesis the claim holds for any value occurring in $\Gamma\Rightarrow t:A,s:B,\Delta$. Since the value $t\mid s:A\parr B$ has the required type, the claim holds for $\Gamma\Rightarrow t\mid s:A\parr B,\Delta$ as well.

∎

The second auxiliary result establishes that any normal $\lambda_{\parr}$-term – the type of which is not $\bot$ – is either a value or a sequence of operations that cannot be carried out.

Lemma 8.2** (The shape of normal terms).**

If there is a derivation in $\mathrm{NMLL}$ of $\Gamma\Rightarrow u:F,\Pi$, where $u$ is in normal form, is not a value and $F\neq\bot$, then $u=y\sigma$.

Proof.

We prove the statement by induction on the number of rule applications in the derivation of $\Gamma\Rightarrow u:F,\Pi$.

If no rule is applied in the derivation, then $\Gamma\Rightarrow u:F,\Pi$ is of the form $x:A\Rightarrow x:A$, thus the claim holds since $u=x$.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $m$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation containing $m+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation.

• •

$\Gamma\Rightarrow\Delta,\circ:\bot\Gamma\Rightarrow\Delta$

. By inductive hypothesis the claim holds for any term occurring in $\Gamma\Rightarrow\Delta$. Since $\circ$ has type $\bot$, the claim holds also for any term occurring in $\Gamma\Rightarrow\Delta,\circ:\bot$.

• •

$\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow t:A\multimap B,\Delta\Sigma\Rightarrow s:A,\Theta$

. By inductive hypothesis the claim holds for any term occurring in $\Gamma\Rightarrow t:A\multimap B,\Delta$ and $\Sigma\Rightarrow s:A,\Theta$. Since $ts$ is in normal form, also $t$ must be in normal form. Hence, by inductive hypothesis, $t=y\sigma$. Therefore, the claim holds for all terms in $\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta$ as well.

• •

$\Gamma\Rightarrow\overline{x}.\,t:A\multimap B,\Delta\Gamma,x:A\Rightarrow t:B,\Delta$

. By inductive hypothesis the claim holds for any term occurring in $\Gamma,A\Rightarrow B,\Delta$. Since $\overline{x}.\,t:A\multimap B$ is a value, the claim holds for all terms in $\Gamma\Rightarrow\overline{x}.\,t:A\multimap B,\Delta$ as well.

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow t:A\parr B,\Delta\Sigma_{1},x:A\Rightarrow\Theta_{1}\Sigma_{2},y:B\Rightarrow\Theta_{2}$

.

By inductive hypothesis the claim holds for any term occurring in $\Gamma\Rightarrow t:A\parr B,\Delta$ and $\Sigma_{1},x:A\Rightarrow\Theta_{1}$ and $\Sigma_{2},y:B\Rightarrow\Theta_{2}$. Since $\overline{x}\,\overline{y}\,t:\bot$ has type $\bot$, the claim holds for all terms in $\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}$ as well.

• •

$\Gamma\Rightarrow t\mid s:A\parr B,\Delta\Gamma\Rightarrow t:A,s:B,\Delta$

. By inductive hypothesis the claim holds for any term occurring in $\Gamma\Rightarrow t:A,s:B,\Delta$. Since $t\mid s:A\parr B$ is a value, the claim holds for $\Gamma\Rightarrow t\mid s:A\parr B,\Delta$ as well.

∎

We can now show that normal $\lambda_{\parr}$-terms satisfy the Subformula Property. The proof is by induction on the size of the $\mathrm{NMLL}$ derivation and, as usual, the difficult case is the one involving implication elimination. Even though we handle this case by a standard argument on the type of sequences of eliminations, represented here by stacks, the multiple-conclusion setting forces us to integrate this argument in the main induction. We do so by using a stronger inductive statement that carries along the induction the required statement about the type of stacks.

Theorem 8.3** (Subformula Property).**

Consider any normal $\mathrm{NMLL}$ derivation $\mathcal{P}$ of the sequent $x_{1}:X_{1},\ldots,x_{m}:X_{m}\Rightarrow t_{1}:T_{1},\ldots,t_{n}:T_{n},\Pi$, where $\Pi$ does not contain any type. Then every type $S$ occurring in $\mathcal{P}$ is a subformula of some type $T_{1},\ldots,T_{n}$ or $X_{1},\ldots,X_{m}$ or $\bot$.

Proof.

We prove a stronger statement:

Consider any normal $\mathrm{NMLL}$ derivation $\mathcal{P}$ of the sequent $x_{1}:X_{1},\ldots,x_{m}:X_{m}\Rightarrow t_{1}:T_{1},\ldots,t_{n}:T_{n},\Pi$, where $\Pi$ does not contain any type. Then every type $S$ occurring in $\mathcal{P}$ is a subformula of some type $T_{1},\ldots,T_{n}$ or $X_{1},\ldots,X_{m}$ or $\bot$. Moreover, if a term $t_{i}$ with $i\in\{1,\ldots,n\}$ is of the form $y\sigma$ where $\sigma$ is a stack, then $T_{i}$ is a subformula of some type $T_{1},\ldots,T_{i-1},T_{i+1},\ldots,T_{n}$ or $X_{1},\ldots,X_{m}$ or $\bot$.

We proceed by induction on the number of rule applications in $\mathcal{P}$.

If no rule is applied in the derivation, then the root of $\mathcal{P}$ is $x:A\Rightarrow x:A$ and the claim holds.

Suppose now that the statement holds for any $\mathrm{NMLL}$ derivation containing $q$ or less rule applications, we show the result for a generic $\mathrm{NMLL}$ derivation containing $q+1$ rule applications. We reason by cases on the last rule applied in this $\mathrm{NMLL}$ derivation.

• •

$\Gamma\Rightarrow\Delta,\circ:\bot\Gamma\Rightarrow\Delta$

. By inductive hypothesis the claim holds for the derivation of the sequent $\Gamma\Rightarrow\Delta$, which must be normal, thus it holds also for $\mathcal{P}$.

• •

$\Gamma\Rightarrow\Delta,{\mathsf{close}}(t)\Gamma\Rightarrow\Delta,t:\bot$

. By inductive hypothesis the claim holds for the derivation of the sequent $\Gamma\Rightarrow\Delta,t:\bot$, which must be normal, thus it holds also for $\mathcal{P}$.

• •

$\Gamma,\Sigma\Rightarrow ts:B,\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow t:A\multimap B,\Delta\Sigma\Rightarrow s:A,\Theta$

. By inductive hypothesis the claim holds for the derivations of the sequents $\Gamma\Rightarrow t:A\multimap B,\Delta$ and $\Sigma\Rightarrow s:A,\Theta$, which must be both normal. Let $S$ be any type occurring in $\mathcal{P}$. If $S$ is a subformula of some type in $\Gamma,\Sigma,B,\Delta,\Theta$, then the claim holds. If $S$, on the other hand, is a subformula of $A\multimap B$ or $A$, we consider the form of the term $t:A\multimap B$. Since $t:A\multimap B$, if $t$ were a value, then by Proposition 8.1, $t=\overline{x}.\,u$. Since the premises of the inference do not share variables, $x$ does not occur in $s$, thus it occurs in $u$ or $\Delta,\Theta$ and it would be possible to apply a reduction rule and $\mathcal{P}$ would not be in normal form. Therefore, $t$ cannot be a value. Hence, by Lemma 8.2, $t=y\sigma$ where $\sigma$ is a stack. Thus, by inductive hypothesis, $A\multimap B$ is a subformula of some type in $\Gamma$ or $\Delta$ and so is $S$. Moreover, the type $B$ of $ts$ is a subformula of some type in $\Gamma$ or $\Delta$. Hence, the claim holds for $\mathcal{P}$ as well.

• •

$\Gamma\Rightarrow\overline{x}.\,t:A\multimap B,\Delta\Gamma,x:A\Rightarrow t:B,\Delta$

. By inductive hypothesis the claim holds for the derivation of the sequent $\Gamma,A\Rightarrow B,\Delta$, which must be normal. Since all types which are subformulae of $A$ or $B$ are subformulae of $A\multimap B$ as well and since we do not have to prove anything more about the term $\overline{x}.\,t:A\multimap B$, the claim holds for $\mathcal{P}$ as well.

• •

$\Gamma,\Sigma_{1},\Sigma_{2}\Rightarrow\overline{x}\,\overline{y}\,t:\bot,\Delta,\Theta_{1},\Theta_{2}\lx@proof@logical@and\Gamma\Rightarrow t:A\parr B,\Delta\Sigma_{1},x:A\Rightarrow\Theta_{1}\Sigma_{2},y:B\Rightarrow\Theta_{2}$

.

By inductive hypothesis the claim holds for the derivations of the sequents $\Gamma\Rightarrow t:A\parr B,\Delta$ and $\Sigma_{1},x:A\Rightarrow\Theta_{1}$ and $\Sigma_{2},y:B\Rightarrow\Theta_{2}$, which must be all normal. Let $S$ be any type occurring in $\mathcal{P}$. If $S$ is a subformula of some type in $\Gamma,\Sigma,\bot,\Delta,\Theta$, then the claim holds. If $S$, on the other hand, is a subformula of $A\parr B$, we consider the form of the term $t:A\parr B$. Since $t:A\parr B$, if $t$ were a value, then by Proposition 8.1, $t=u\mid v$. Since $x$ and $y$ must occur in $\Theta$, it would be possible to apply a reduction rule and $\mathcal{P}$ would not be in normal form. Therefore, $t$ cannot be a value. Hence, by Lemma 8.2, $t=y\sigma$ where $\sigma$ is a stack. Thus, by inductive hypothesis, $A\parr B$ is a subformula of some type in $\Gamma$ or $\Delta$ and thus the claim holds with respect to $\mathcal{P}$ for all terms in the derivation the type of which is a subformula of $A\parr B$. Since we do not have to prove anything more about the term $\overline{x}\,\overline{y}\,t:\bot$, the claim holds for $\mathcal{P}$ as well.

• •

$\Gamma\Rightarrow t\mid s:A\parr B,\Delta\Gamma\Rightarrow t:A,s:B,\Delta$

. By inductive hypothesis the claim holds for the derivation of the sequent $\Gamma\Rightarrow t:A,s:B,\Delta$ and hence also for $\mathcal{P}$.

∎

9 Strong Normalization

It is quite immediate to see that all terms of the calculus strongly normalize. Indeed, each reduction step strictly decreases the size of the term. This is due to the linear nature of terms (Proposition 7.1): each communication or $\lambda$-reduction moves one or two terms from one location to another. Therefore, no duplication is involved in the reductions. Since, moreover, each reduction removes one binder from the term, we have that the size of the term strictly decreases. We formally show this in the following theorem.

Definition 9.1** (Communication-size of a term).**

For any term $t$, its communication size $\mathrm{cs}(t)$ is the number of occurrences of $\overline{x}.\,$ and $\overline{x}\,\overline{y}\,$ in $t$.

Theorem 9.1** (Strong normalization).**

For any term $t$ such that the sequent $\Gamma\Rightarrow t:F$ is derivable in $\mathrm{NMLL}$, all sequences of terms $t_{1},t_{2}\ldots$ such that $t_{1}=t$ and $t_{i}\mapsto t_{i+1}$ are finite and contain exactly $\mathrm{cs}(t)$ terms.

Proof.

The proof is by induction on the communication-size $\mathrm{cs}(t)$ of $t$. In the base case, $t$ does not contain any redex and the claim trivially holds. We prove then that the claim holds for a generic term $t$ such that $\mathrm{cs}(t)=n+1$, under the assumption that the claim holds for all terms $s$ such that $\mathrm{cs}(u)=n$. In order to do so, we consider a generic sequence of terms $t_{1},t_{2}\ldots$ such that $t_{1}=t$ and $t_{i}\mapsto t_{i+1}$, and we reason by case distinction on the shape of the reduction $t\mapsto t_{2}$.

• •

$t_{1}=s_{1}\mid\ldots\mid\mathcal{C}[\overline{x}w.v]\mid\ldots\mid s_{n}\quad\mapsto\quad(\;s_{1}\mid\ldots\mid\mathcal{C}[v]\mid\ldots\mid s_{n}\;)[w/x]=t_{2}$. Since, by Proposition 7.1, $x$ occurs exactly once in $t_{2}$ and since $\overline{x}w.v$ is replaced by $v$, we have that $\mathrm{cs}(t_{2})=n$ and that, by inductive hypothesis, the claim holds for $t_{2}$. Thus, all sequences of terms $t_{2},t_{3}\ldots$ such that $t_{i}\mapsto t_{i+1}$ contain exactly $n$ terms. The sequence $t_{1},t_{2}\ldots$ contains thus $n+1$ terms.

• •

$t_{1}=s_{1}\mid\ldots\mid\mathcal{C}[\overline{x}\,\overline{y}\,(v\mid w)]\mid\ldots\mid s_{n}\quad\mapsto\quad(\;s_{1}\mid\ldots\mid\mathcal{C}[\circ]\mid\ldots\mid s_{n}\;)[v/x\;\;w/y]=t_{2}$. Since, by Proposition 7.1, both $x$ and $y$ occur exactly once in $t_{2}$ and since $\overline{x}\,\overline{y}\,(v\mid w)$ is replaced by $\circ$, we have that $\mathrm{cs}(t_{2})=n$ and that, by inductive hypothesis, the claim holds for $t_{2}$. Thus, all sequences of terms $t_{2},t_{3}\ldots$ such that $t_{i}\mapsto t_{i+1}$ contain exactly $n$ terms. The sequence $t_{1},t_{2}\ldots$ contains thus $n+1$ terms.

∎

10 Confluence

We show now that each $\lambda_{\parr}$-term has a unique normal form. Since all $\lambda_{\parr}$-terms have a normal form, this implies that the calculus $\lambda_{\parr}$ is confluent: for any term $t$, if $t\mapsto t^{\prime}$ and $t\mapsto t^{\prime\prime}$, then there is a term $t^{\star}$ such that both $t^{\prime}\mapsto t^{\star}$ and $t^{\prime\prime}\mapsto t^{\star}$.

In order to simplify the proof of confluence, we define the concept of activator. Intuitively, the activator of a reduction is the term which is responsible for the reduction. For instance, to trigger a communication we only need a subterm which is ready to send a message, such as $\overline{x}w.v$. If we do trigger this communication of $w$ through $x$, the term $\overline{x}w.v$ is going to be the activator of the reduction.

Definition 10.1** (Activator).**

Given any reduction $s\mapsto t$, we say that the activator of $s\mapsto t$ is the subterm of $s$ of the form $(\lambda x\,v)w$, $\overline{x}w.v$, $\overline{y}\,\overline{z}\,v$, which is displayed in the corresponding reduction rule.

Theorem 10.1** (Uniqueness of the normal form).**

For any term $t$ such that the sequent $\Gamma\Rightarrow t:F$ is derivable in $\mathrm{NMLL}$, $t$ has only one normal form.

Proof.

The proof is by induction on the length of the normalization of $t$.

If $\mathrm{cs}(t)=0$, the claim trivially holds. We show the claim for a generic term $t$ such that $\mathrm{cs}(t)=m+1$, under the assumption that the claim holds for all terms with communication-size $m$ or less.

Suppose that the term $t$ reduces to two different terms $t^{\prime}$ and $t^{\prime\prime}$ if we reduce two different redexes in $t$. We show that both $t^{\prime}$ and $t^{\prime\prime}$ can reduce to the same term $t^{\star}$. Since, by inductive hypothesis, $t^{\prime}$ has a unique normal form and $t^{\prime\prime}$ has a unique normal form as well, this is enough to show that $t$ has a unique normal form. Since the argument for the $\parr$-reductions is everywhere close to identical to the argument for $\multimap$-reductions, we only present the latter. Let us denote then the reduction $t\mapsto t^{\prime}$ as

[TABLE]

There are two main cases.

1. If one of the activators of $t\mapsto t^{\prime}$ and $t\mapsto t^{\prime\prime}$ is a subterm of the other, we consider the outermost activator. Without loss of generality, we assume that the outermost is the activator of $t\mapsto t^{\prime}$. Now, the activator $\overline{y}r.s$ of $t\mapsto t^{\prime\prime}$ is either a subterm of $v$ or of $w$.

• •

The activator of $t\mapsto t^{\prime\prime}$ is a subterm of $v$. The reduction $t\mapsto t^{\prime\prime}$ is then of the form

[TABLE]

where $v^{\prime}$ is obtained from $v$ by replacing $\overline{y}r.s$ with $s$. Since, by Proposition 7.2, $y$ does not occur in $w$, we have $t^{\prime\prime}\mapsto t^{\star}$, with

[TABLE]

We just need to show that $t^{\prime}\mapsto t^{\star}$, that is

[TABLE]

By Proposition 7.1 we have that $y\neq x$. Now, if $r$ contains $x$,

[TABLE]

[TABLE]

If $r$ does not contain $x$ and since $y$ does not occur in $w$, we have

[TABLE]

• •

The activator of $t\mapsto t^{\prime\prime}$ is a subterm of $w$. The reduction $t\mapsto t^{\prime\prime}$ is then of the form

[TABLE]

where $w^{\prime}$ is obtained from $w$ by replacing $\overline{y}r.s$ with $s$. We have $t^{\prime\prime}\mapsto t^{\star}$, with

[TABLE]

We just need to show that $t^{\prime}\mapsto t^{\star}$, that is

[TABLE]

We have the following reduction:

[TABLE]

Now, $r$ does not contain $x$, by Proposition 7.2 and because the activator of $t\mapsto t^{\prime\prime}$ occurs in $w$. Since, moreover, $y\neq x$, we also have

[TABLE]

and therefore that $t^{\prime}\mapsto t^{\star}$.

2. If neither of the activators of $t\mapsto t^{\prime}$ and $t\mapsto t^{\prime\prime}$ is a subterm of the other, the reduction $t\mapsto t^{\prime\prime}$ is of the form

[TABLE]

where $u_{i}^{\prime}$ and $\mathcal{C}^{\prime}[\;]$ are either equal to, respectively, $u_{i}$ and $\mathcal{C}[\;]$ or obtained from $u_{i}$ and $\mathcal{C}[\;]$, respectively, by replacing the activator $\overline{y}r.s$ of $t\mapsto t^{\prime\prime}$ with $s$. We have $t^{\prime\prime}\mapsto t^{\star}$, with

[TABLE]

We just need to show that $t^{\prime}\mapsto t^{\star}$, that is

[TABLE]

Now, if $s$ is the activator of a reduction, also $s[w/x]$ has the suitable shape to be one; and the relative reductions substitute the same variable. By Definition 2.3, moreover, $y\neq x$ and hence $y$ occurs in the term $(\;u_{1}\mid\ldots\mid\mathcal{C}[v]\mid\ldots\mid u_{n}\;)[w/x]$, and we can reduce it as follows:

[TABLE]

We must now consider several cases, according as to whether $x$ and $y$ occurs in the messages $w$ and $r$.

• If $x$ occurs in $r$, but $y$ does not occur in $w$, then, by Proposition 7.1, $x$ does not occur in $u_{1}^{\prime}\mid\ldots\mid\mathcal{C}^{\prime}[v]\mid\ldots\mid u_{n}^{\prime}$ and we obtain indeed

[TABLE]

[TABLE]

• If $x$ does not occur in $r$, but $y$ occurs in $w$, then, by Proposition 7.1, $y$ does not occur in $u_{1}^{\prime}\mid\ldots\mid\mathcal{C}^{\prime}[v]\mid\ldots\mid u_{n}^{\prime}$ and we obtain indeed

[TABLE]

[TABLE]

• If neither $x$ occurs in $r$ nor $y$ occurs in $w$, then, by Proposition 7.1, $y$ does not occur in $u_{1}^{\prime}\mid\ldots\mid\mathcal{C}^{\prime}[v]\mid\ldots\mid u_{n}^{\prime}$ and we obtain indeed

[TABLE]

[TABLE]

• Finally, we show it cannot be that both $x$ occurs in $r$ and $y$ occurs in $w$. Indeed, suppose, for the sake of contradiction, that they do. By letting the term $\overline{y}r.s$ transmit its message $r$, we would have

[TABLE]

By Theorem 6.2, $\Gamma\Rightarrow t^{\prime\prime\prime}:F$, which is in contradiction with Proposition 7.2, since $x$ occurs in $w[r/y]$. ∎

11 Related Work and Conclusions

The origins of $\lambda_{\parr}$ are influenced by and related to several functional and process calculi. We shall consider them one by one.

$\lambda_{\parr}$ and Linear Session Typed $\pi$-calculi

One of the most established ways to interpret linear logic proofs into concurrent programs consists in interpreting sequent calculi for linear logic into $\pi$-calculi with session types, main references being [9, 32, 18]. In those calculi, a session type is a logical expression containing information about the whole sequence of exchanges that occur between two processes through one channel. Session types are attached only to communication channels, therefore they only describe the channels’ input/output behaviour, not the processes using them. In $\lambda_{\parr}$, as in the tradition of the Curry-Howard correspondence, types are instead attached to processes, are read as process specifications and are employed to formally guarantee that processes will behave according to the specifications expressed by their type. Nevertheless, since the nature of $\pi$-calculus processes is determined by their channels’ behaviour, specifying channels means also specifying processes, hence the difference with $\lambda_{\parr}$ is not as significant as it may appear.

A channel typed by a session type will occur in general more than once and will support several transmissions. This is not the case in $\lambda_{\parr}$. The linearity of the calculus implies that each output channel can only occur once and thus be used once. As shown in our examples, two processes of $\lambda_{\parr}$ can nevertheless communicate more than once, since they can be connected by several different channels. In particular, in $\lambda_{\parr}$ there is no restriction on the number and direction of the communications between any two processes: dialogues are possible and information can be exchanged back and forth with no limitation.

Unlike in $\pi$-calculus, there is no need in $\lambda_{\parr}$ of a construct $\nu x$ for declaring a channel private. Since in our calculus any given communication channel connects exactly two processes, the channel is already a private link between the involved processes, simply because there is no other process sharing the same channel.

The typing system of $\lambda_{\parr}$ supports also cyclically interconnected processes, therefore $\lambda_{\parr}$ cannot be faithfully translated in the linearly session typed $\pi$-calculi [9, 32, 18]. At the time of this writing, there is no known straightforward translation of the multiplicative fragments of those calculi in $\lambda_{\parr}$, but also no known reason a translation should not be possible.

$\lambda_{\parr}$ and other Typed Concurrent $\lambda$-calculi

As a consequence of adopting linear sequent calculus, the session typings of [9, 32, 18] do not support directly functional computation. Several approaches have been developed to overcome this intrinsic limitation.

The system in [31] provides some combination of session typed processes and functional programs. However, the typing system for the functional part is just added on top of the linear logic system. Therefore, there is no seamless account of both functional and concurrent computation by a single system for linear logic, which is the main accomplishment of our work on $\lambda_{\parr}$.

The linear concurrent functional calculus GV in [32] is more similar in spirit to $\lambda_{\parr}$. However, when it comes to linear logic, it is not as pure as ours and displays no connection between computation and the full normalization process leading to analytic proofs. No direct reduction rules for GV are provided either.

The two concurrent $\lambda$-calculi studied in [3, 4] are typed by Gödel and classical logic. They are more expressive than $\lambda_{\parr}$ when it comes to functional computation, because they are based on extensions of intuitionistic natural deduction and thus feature full typed $\lambda$-calculus. However, the reduction rules are significantly more complex than those of $\lambda_{\parr}$, due to the complicated treatment that code mobility requires. Moreover, strong normalization and confluence do not hold.

The concurrent $\lambda$-calculus of [5] is typed by first-order classical logic. It resembles a session-typed $\lambda$-calculus, but supports only data transmission. It is strongly normalizing, but is non-confluent and does not enjoy any subformula property.

The calculus Lolliproc in [20] is a parallel interpretation of control operators, rather than a calculus centered on communication. The completeness of the typing system with respect to linear logic is not proved and no subformula property is shown either, which makes unclear if it actually is a legitimate proof system for linear logic.

$\lambda_{\parr}$ and Proof-Nets

Proof-nets for multiplicative linear logic [14] can encode several programming languages, among them linear $\lambda$-calculus [15] and typed $\pi$-calculus [16]. We believe $\lambda_{\parr}$ can be encoded in proof-nets as well and hence offers a new way of using proof-nets for representing functional concurrent computation. However, $\lambda_{\parr}$ is based on the connectives $\multimap,\parr$ and normalization, while proof-nets are based on the connectives $\otimes,\parr$ and cut-elimination, which makes $\lambda_{\parr}$ far more suitable as syntax for functional concurrent programming. Indeed, $\lambda_{\parr}$ is a full-blown programming language right off the bat, while proof-nets were created as an elegant and economical proof system for linear logic.

$\lambda_{\parr}$ and Exponentials

As type system of $\lambda_{\parr}$, multiplicative linear logic already features all the important characters of functional concurrent computation, and because of both its expressiveness and simplicity, it deserves to be treated as a type system on its own, as traditional in linear logic. One non-trivial problem is to extend the type system of $\lambda_{\parr}$ with exponentials. We do not see any real obstacles to doing that, but we leave the problem as future work. As a result, $\lambda_{\parr}$ may gain more duplication and replication abilities, as those of CP [32].

$\lambda\mu$ and $\lambda_{\parr}$: Sequentiality vs Parallelism

As far as the logical rules for implication are concerned, the type system of the original version of $\lambda\mu$ [25] is exactly the non-linear version of the type system of $\lambda_{\parr}$. However, $\lambda\mu$ and $\lambda_{\parr}$ strongly diverge if we consider their computational behaviour. In particular, the crucial difference between $\lambda_{\parr}$ and $\lambda\mu$ is that while in $\lambda\mu$ a whole list of formulas is used to type a single term: $t:A_{1},\ldots,A_{n}$, in $\lambda_{\parr}$ each element of the list of formulas types a different term: $t_{1}:A_{1},\ldots,t_{n}:A_{n}$. Indeed, although the type system of $\lambda\mu$ actually builds several different terms, it does it sequentially, so the result is a unique term; instead, the type system of $\lambda_{\parr}$ builds several different terms in parallel and let them communicate.

The reason is that $\lambda\mu$ forces only one distinguished “active” formula of each list to be used at any time in the derivation. Labels $\alpha,\beta\dots$ – also called $\mu$-variables – are introduced to explicitly activate a formula, rule below left, which can therefore be used in an inference, or deactivate it, rule below right:

[TABLE]

where $\Gamma$ is a context containing declaration of $\lambda$-variables $x,y,\dots$ and $\Delta$ is a multiset containing formulae labeled by $\mu$-variables $\alpha,\beta\dots$. As we can see from the condition on the context $\Delta$, at most one formula in each sequent can be without a label.

The history of activations and deactivations occurring in the derivation is recorded inside the corresponding $\lambda\mu$-term, as we can see in the following example

[TABLE]

Here the construction of $w$ has been paused for a while and resumed with the last inference rule. Hence, $v$ can be considered as the “real” argument of $w$, rather than of $(\mu\beta.u)v$. As consequence, there is the reduction $(\mu\beta.u)v\;\mapsto\;\mu\beta.u[[\beta](wv)/[\beta]w]$, where the argument $v$ of $\mu\beta.u$ is transmitted as argument to all subterms of $t$ with label $[\beta]$.

Multiple-conclusion Full Intuitionistic Linear Logic

The $\lambda$-calculus in [17] provides a computational interpretation of an intuitionistic linear logic with the $\parr$ connective. The typing system however is a linear sequent calculus, so the corresponding $\lambda$-calculus is rather obtained by translation than by a Curry-Howard isomorphism between proofs and $\lambda$-terms. To obtain such an isomorphism, our move to natural deduction was necessary. Also, in [17] cut-elimination is not interpreted as usual as communication, so the system does not support concurrency. A radical change in the treatment of linear implication was needed to recover communication and an interpretation of $\parr$ as parallel operator was needed to recover parallelism, which is what we did. It is also instructive to compare $\parr\mathrm{E}$ rule to the corresponding rule in [17]:

[TABLE]

This rule duplicates the term $s$, compromising linearity of variables. Nevertheless, the linearity of the computation is safe if we consider that $s$ virtually occurs twice, but it will only be used once: one half of it, inside $v$, the other half, inside $w$; the two spare halves will be discarded. Instead, $\lambda_{\parr}$ is built around communication. We thus re-interpreted disjunction redexes as communications in order to avoid unnecessary duplication in case distinction constructs. Indeed, what we need in interpreting a $\parr\mathrm{E}$ rule with premises $\Gamma\Rightarrow s:A\parr B,\Delta$, $\quad\Sigma_{1},x:A\Rightarrow v:C,\Theta_{1}\quad$ and $\quad\Sigma_{2},y:B\Rightarrow w:D,\Theta_{2}$ is simply a way to provide one half of $s$ to $v$ and the other half to $w$ when $s$ will assume a form which is suitable for a reduction. Instead of duplicating $s$ and attaching one copy of it to $v$ and one to $w$, we just let $s$ be an autonomous term – living in parallel with all other terms in our multiple-conclusion – and established a communication channel from $s$ to both $v$ and $w$. Thus, when $s$ assumes the right form, we triggered a communication transmitting part of $s$ to $v$ and part to $w$ as required.