The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version)

TL;DR

This paper develops a geometry of interaction model using multiple tokens to accurately represent concurrent computation in multiport interaction combinators, bridging graph theory and process algebra.

Contribution

It introduces a novel token machine model with multiple tokens for concurrent computation, proving its soundness and adequacy for Mazza's multiport interaction nets.

Findings

Model accurately captures concurrent computation.

Proves soundness via simulation between token machines.

Establishes adequacy through convergence analysis.

Abstract

We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the $\pi$-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines.

Equations

$$\frac{INs}{ICs}=\frac{MINs}{MICs}.$$

$$\{|({\ell }_1,a_1),\dots ,({\ell }_n,a_n),(\sigma ({\ell }_1),b_1),\dots ,(\sigma ({\ell }_n),b_n)|\}$$

$${⇝}_{\mathbf{A}}=$$

$${⇝}_{\mathbf{B}}=$$

$${⇝}_{\mathbf{AB}}=$$

$$\wedge \mathsf{a}\cup \mathsf{d}=\mathsf{b}\cup \mathsf{c}\}.$$

$$\sim$$

$$\precsim$$

$$\stackrel{\mathsf{a}}{\Rightarrow }=\{\begin{array}{ll}{\stackrel{\varnothing }{\to }}^{\ast }\stackrel{\mathsf{a}}{\to }{\stackrel{\varnothing }{\to }}^{\ast }& \text{if }\mathsf{a}\ne \varnothing \\ {\stackrel{\varnothing }{\to }}^{\ast }& \text{if }\mathsf{a}=\varnothing .\end{array}$$

$$\approx$$

$$⪷$$

$$\mathcal{R}=\{((u_{\mathbf{A}},u_{\mathbf{B}}),(u_{\mathbf{B}},u_{\mathbf{A}}))\mid u_{\mathbf{A}}\in S_{\mathbf{A}},u_{\mathbf{B}}\in S_{\mathbf{B}}\}$$

$$\hat{\mathcal{R}}=\{((u_{\mathbf{A}},u_{\mathbf{C}}),(u_{\mathbf{B}},u_{\mathbf{C}}))\mid (u_{\mathbf{A}},u_{\mathbf{B}})\in \mathcal{R},u_{\mathbf{C}}\in S_{\mathbf{C}}\}$$

$$\mathbf{s},\mathbf{t},\mathbf{u}::=\epsilon\;\;\mbox{\Large{$\mid$}}\;\;\mathbf{s}\mathtt{p}\;\;\mbox{\Large{$\mid$}}\;\;\mathbf{s}\mathtt{q}\;\;\mbox{\Large{$\mid$}}\;\;\mathbf{s}n,$$

$$\overline{ϵ}$$

$$A,B::=\mathsf{out}(C)\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{in}(C)\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{ma}_{cd}(C)\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{kill}(C)\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{cokill}(C)$$

$$\mathsf{out}(C)\perp \mathsf{in}(C);{\mathsf{ma}}_{cd}(C)\perp {\mathsf{ma}}_{dc}(\overline{C});\mathsf{kill}(C)\perp \mathsf{cokill}(C).$$

$$\Theta :X_1\stackrel{[}{S}]\to X_2\stackrel{[}{S}]\to \cdots \stackrel{[}{S}]\to X_n,$$

$$\mathsf{U}\stackrel{{\ell }_1}{\to }\cdots \stackrel{{\ell }_n}{\to }\mathsf{S}.$$

$$\Theta :X_1\stackrel{[}{S}]\to X_2\stackrel{[}{S}]\to \cdots \stackrel{[}{S}]\to X_n$$

$${\Theta }_{r,E}^{OP}:{X_n}_{r,E}^{OP}\stackrel{[}{S}]\to {X_{n-1}}_{r,E}^{OP}\stackrel{[}{S}]\to \cdots \stackrel{[}{S}]\to {X_1}_{r,E}^{OP}.$$

$$f^{\ast }(\mathsf{S})=({\cup }_{T\in \mathsf{S}}{f}_{\rho }(\mathsf{S},T),{\cup }_{T\in \mathsf{S}}{f}_{\pi }(\mathsf{S},T))$$

$$\mathsf{U}$$

$$\mathsf{V}$$

$$\ell \cup \xi$$

$${\mathsf{U}}_{\rho }\stackrel{{\nu }_{\rho }}{\to }{\mathsf{V}}_{\rho };$$

$${\mathsf{U}}_{\pi }\stackrel{{\nu }_{\pi }}{\to }{\mathsf{V}}_{\pi }.$$

$${fin}_{{\mathsf{TM}}_{\rho }}^{\varnothing }(s_{\rho })$$

$${inf}_{{\mathsf{TM}}_{\rho }}^{\varnothing }(s_{\rho })$$

$$\Theta$$

$$\Xi$$

$$\Theta :T_1\stackrel{[}{S}]\to T_2\stackrel{[}{S}]\to \cdots \stackrel{[}{S}]\to T_n$$

$$\rho {\to }_{\gamma \gamma }^{\ast }\pi {\to }_a\theta$$

Full text

1 Introduction

Game semantics [26, 3] and the geometry of interaction (GoI for short) [23, 13] are semantic frameworks in which programs and proofs are interpreted as mathematical or computational objects exhibiting nontrivial interactive behaviours (e.g. strategies [26], token machines [13], operators [23]). This allows for a number of nice properties. First of all, these models can be defined so as to be compositional, but close to contexts as for their discriminating power; this is particularly true in game semantics, for which many full abstraction results have been proved. Secondly, interactive models can often be presented concretely, either as circuits [20, 22], automata [13], or abstract machines for strategies [19], thus enabling direct compilation of higher-order programs into low-level languages.

The bulk of the huge amount of literature on interactive semantic models is about sequential languages [26, 3] but, especially in the last fifteen years, the research community has been able to devise game models sufficiently powerful to interpret not only advanced features like polymorphisms and general references [2, 1], but also concurrency [4, 34, 37, 8], thus going significantly beyond game semantics as originally conceived (more on this is in Section 1.1 below). The same cannot be said about the geometry of interaction, which until very recently has been able to interpret only sequential, although potentially effectful, forms of computation [25, 35].

A crucial observation, which is the starting point of this work, is that the geometry of interaction, when formulated in terms of so-called token machines, can be made parallel by allowing more than a single token to float around at the same time [9]. The consequences of this idea have been analysed for sequential languages [10], also in presence of probabilistic and quantum effects [11]. Are multiple tokens enough to model fully-fledged concurrency, as embodied by process algebras? This is the question we will try to address in this paper. The answer will be positive, although the walk to it will not be easy.

When looking for a GoI semantics for concurrent models of computation, one could of course proceed by considering any concrete process algebra, and define a token machine for it directly, being inspired by the literature. As an example, the way the higher-order $\pi$-calculus is classically encoded into the usual name-passing $\pi$-calculus [38] can be seen reminiscent of the usual GoI construction, since higher-order process passing is encoded into a somehow more basic, essentially first-order calculus. This route would however be biased to a specific process algebra, thus losing in generality and canonicity. In turn, relying on a (possibly complicated) computational model would mean hiding the structure of the introduced GoI, understanding what is our main aim here.

For these reasons, we will purposely take a minimalistic approach, being inspired by Lafont’s interaction nets (INs for short) and interaction combinators (for short, ICs) [27]. The latter is a system of interaction nets which is universal, and thus embodies a vast class of graph-theoretic models for sequential interaction, including logical systems [24], programming languages [30], and optimal reduction algorithms [29]. ICs are not only very simple themselves, but also admit an elementary geometry of interaction model, arguably the simplest of all [27]. ICs, however, cannot form the basis on which to build a GoI model of concurrent computation: they are strongly confluent and simply lack the mixture of parallelism and nondeterminism which is at the heart of concurrency, although being a very good model of (low-level) sequential computation.

A picture similar to the one drawn by Lafont but envisioned with concurrency in mind is the one due to Alexiev, Mazza, and coauthors [5, 33, 32, 15]. In the last twenty years, in particular, concurrent extensions of interaction nets, called multiport interaction nets (MINs for short), have been proved to be powerful enough to faithfully encode process algebras [33, 32], to admit an event-structure model [31], and to be strictly more expressive than multirule interaction nets [15]. Remarkably, MINs have also been shown to admit a universality theorem with respect to a specific interaction system, namely multiport interaction combinators (for short, MICs) [33]. In a sense, then, we have the following equation:

[TABLE]

MINs generalise INs in that cells can have more than one principal port, this way allowing for a very general form of nondeterministic interaction, and MICs, being universal for MINs, are a natural candidate model for studying GoI models for concurrent systems, as suggested by Mazza himself [33]. Nevertheless, we are not aware of any attempt to give geometry of interaction models for any system of MINs.

When trying to define a GoI model for MICs, one immediately realises that classic token machines are simply not adequate to faithfully model concurrent interaction. In particular, multiport interaction, i.e., nondeterminism as found in MICs, cannot be captured by automata in which just one token is allowed to float around the underlying graph, as will be explained in Section 2.3 below. The only way out consists in allowing for the simultaneous presence of multiple tokens [9, 10], which becomes essential here. In particular, it allows for nondeterministic and nonlocal interaction, which is an essential ingredient of MICs’ dynamics, and of concurrency in general.

This paper is devoted to presenting the first geometry of interaction model for multiport interaction combinators. Our GoI model is a substantial extension of Lafont’s classic token machine model for ICs [27]. We allow multiple tokens to move around at the same time and make use of them to realise the process of resolving nondeterminism and keeping track of choices, that we call marriages. This requires four different kinds of token, three of them being static, and only one meant to really travel inside the net. This way, we get a stateless notion of a machine even if, of course, static tokens could be replaced by stateful cells.

Our Multi-token machines can be seen as locative transition systems, a special class of labelled transition systems. This framework provides us with a natural way of defining parallel composition, and we will prove our semantics to be indeed compositional, i.e., that the parallel composition of two nets can be interpreted as the parallel composition of the two respective machines, modulo bisimilarity. We can thus establish soundness of the model in terms of labelled (bi)similarity. What makes everything much more complex than in single-token machines is the nondeterministic nature of the reduction system: a net can make nondeterministic choices, thus losing the capability of behaving in a certain way. If a net $\rho$ reduces to another net $\pi$ by performing such a reduction step, then the interpretation of $\rho$ is not necessarily behaviourally equivalent to that of $\pi$, but can rather be “larger”. As a consequence, soundness of our GoI model needs to be spelled out in the form of similarity which, by the way, turns out to come from bisimilarity between other associated states of the two involved machines.

We also show that our model is not too coarse but adequate, in the sense that token machines reflect the convergence behaviour of the nets they interpret, both in the “may” and in the “must” sense. Our proof heavily exploits the bisimulation relations we use to prove our soundness result, which can relate an execution of a token machine to another one along net reduction.

1.1 Related Work

Concurrent (or asynchronous) game semantics, first introduced in [4] and pursued later by Melliés [34], is a generalisation of usual game semantics for sequential computation [26, 3]. It yielded a fully abstract model of multiplicative additive linear logic proofs, followed by (again fully abstract) models of many concurrent calculi, e.g. CSP or Parallel Algol [28, 21]. Recently, Winskel and his coauthors have studied winning conditions and determinacy results for such games, that may lead to applications in verification of concurrent systems [37, 8]. We are not aware of any attempt to relate all this to geometry of interaction and token machines.

Another formalism of concurrent and distributed systems that is worth mentioning here is the one of Petri nets [36]. Indeed, our token machines resemble Petri nets to a large extent: multiple tokens circulate around a graph structure, dynamically enabling or disabling each other’s transition. However, there is one remarkable difference: while in Petri nets the underlying graph consists itself of places and transitions and computation is inherently local, out token machines indeed allow tokens lying next to cells which are far away from each other in a net to communicate, meaning that interaction is nonlocal. This is an inevitable price to pay if we want token machines to properly reflect the behaviour of the MIC reduction rules. See Section 2.3 for the details, and Section 7 for more observations in this direction.

Differential interaction nets [18] are a graphical calculus for differential linear logic [16], and can be seen as a multirule variant of interaction nets, for which a single token GoI model already exists [14]. They exhibit nondeterministic behaviour and are able to encode finitary fragments of Milner’s $\pi$-calculus [17], although the encoding cannot be completely satisfactory, as highlighted by Dorman and Mazza [15]. We chose MICs as our target calculus with this observation in mind: multirule interaction nets simply lack the expressive power which is necessary to model concurrency in its generality. On the other hand, the solid logical basis and the accompanying type system of differential interaction nets may offer us a more structural way to deal with problems in concurrency theory. The authors believe that studying the nature and structure of the token-flowing can be a way to devise appropriate type structures and logical systems for calculi which lacks any of those, like MICs. This is a topic the authors are currently working on, but which lies outside the scope of this paper.

2 Multiport Interaction Combinators at a Glance

This section is devoted to introducing the objects of study of this paper, namely multiport interaction combinators.

2.1 Nets

A cell is a triple $(\alpha,\vec{p},\vec{q})$ of a symbol $\alpha$, a sequence $\vec{p}$ of auxiliary ports, the length of which is the arity of $\alpha$, and a sequence $\vec{q}$ of principal ports, the length of which is the coarity of $\alpha$. A cell is drawn in Figure 1(a).

A net consists of finitely many cells, free ports and wires which connect each ports with another one. Formally, then, given a set of cell kinds $\mathscr{K}$, a net $\rho$ is $\mathcal{CEL}^{\rho}$ and $\mathcal{WIR}^{\rho}$ where:

• •

$\mathcal{POR}^{\rho}$ is a finite set of ports.

• •

$\mathcal{CEL}^{\rho}$ is a finite set of cells of a kind $\alpha\in\mathscr{K}$, whose ports are elements of $\mathcal{POR}^{\rho}$.

• •

$\mathcal{WIR}^{\rho}$ is a finite set of unordered pairs of ports.

• •

Each port appears at least once in $\mathcal{WIR}^{\rho}$ and at most twice in $\mathcal{CEL}^{\rho}\cup\mathcal{WIR}^{\rho}$.

The ports of $\rho$ which appear only once in $\mathcal{CEL}^{\rho}\cup\mathcal{WIR}^{\rho}$ are said to be free. The set of free ports of $\rho$ is $\mathcal{FPOR}^{\rho}$. Nets are indicated with metavariables like $\rho$ or $\pi$. Given a set of cell kinds $\mathscr{K}$, the set of all nets is denoted by $\mathsf{NETS}_{\mathscr{K}}$. We assume that each free port $p$ of any net is labelled with a distinct label $\ell$. Often, nets are presented graphically, e.g. a net $\rho$ with free ports labelled with $\ell_{1},\ldots,\ell_{n}$ looks as in Figure 1(b). Metavariables like $\mathcal{L}$ and $\mathcal{M}$ stands for finite sets of locations $\{\ell_{1},\ldots,\ell_{n}\}$.

In multiport interaction combinators, one considers cells of three different kinds, namely $\gamma$ (with arity $2$ and coarity $1$), $\delta_{n}$ (with arity $2n$ and coarity $n$, for each $n\geq 1$), and $\varepsilon$ (with arity [math] and coarity $1$). These are pictured in Figure 1(c). Thus the set of nets in MICs is $\mathsf{NETS}_{\{\gamma,\delta_{n},\varepsilon\,|\,n\geq 1\}}$. A vicious circle is a subnet of a net like the one depicted in Figure 1(d), where $\tau$ is a tree consisting of $\gamma$ cells, and $\omega$ is a wiring, i.e. consists of wires only. An example of an MIC net can be found in Figure 2(a). It consists of two $\delta_{2}$ cells, one $\gamma$ cell, and nine free ports, connected in the way depicted. The reason why MICs are a relevant instance of multiport interaction nets is that they allow for a Universality Theorem (see [33], Theorem 6.16, page 209), which states that any other system of multiport interaction nets can be encoded into MICs. This makes MICs a minimal, but extremely powerful graph-rewriting formalism, since multiport interaction nets are well known to be expressive enough to faithfully capture the dynamics of process algebras, and of the $\pi$-calculus in particular [32, 5]. This is in contrast to multirule interaction nets, like differential interaction nets, which are known to be strictly less expressive than their multiport siblings [15].

Sometimes it is very convenient to form the parallel composition of two nets that share certain locations. Any partial injection $\sigma$ from a set $X$ to a set $Y$ can be seen as a bijection from $\mathit{dom}(\sigma)\subseteq X$ to $\mathit{rng}(\sigma)\subseteq Y$. Its inverse, as usual, is indicated with $\sigma^{-1}$. Given nets $\rho$ on $\mathcal{L}$ and $\pi$ on $\mathcal{M}$ (where $\mathcal{L}$ and $\mathcal{M}$ are disjoint) and a partial injection $\sigma$ from $\mathcal{L}$ and $\mathcal{M}$, the parallel composition of $\rho$ and $\pi$ is defined to be the net $\rho||_{\sigma}\pi$ depicted in Figure 3, where $\mathcal{L}=\{\ell_{1},\ldots,\ell_{n}\}$ and $\mathcal{M}=\{r_{1},\ldots,r_{m}\}$.

2.2 Reduction

The interaction rules for the multiport interaction combinators are the graph rewriting rules (also called reduction rules) in Figure 4. We will refer to the three rules as $\gamma\gamma$, $\delta\delta$ and $\gamma\delta$, respectively. A pair of principal ports facing each other in a rule is called a redex.

Rules can be applied anywhere in a net, giving rise to a binary relation between nets that we indicate as $\rightarrow$.

MICs as defined by Mazza [33] include three more interaction rules, called $\varepsilon$ rules, which allow to handle the situation in which an $\varepsilon$ cell faces another cell through its principal port. All what we say in this paper holds for the system Mazza considers, and proofs of that can be found in the Appendix. The choice of considering a simplified system is motivated by the desire to make our techniques and results easier to understand, and by the fact that the Universality Theorem holds also in absence of $\varepsilon$ rules [33, 12]. For closely related reasons, we decided to consider a system of multiport interaction combinators in which the co-arity $n$ of $\delta_{n}$ cells is always equal to $2$ hereafter in the paper, and write $\mathsf{NETS}$ for $\mathsf{NETS}_{\{\gamma,\delta_{2},\varepsilon\}}$. This, again, allows for a very simple presentation without sacrificing Universality of MICs.

Consider, as an example, the net in Figure 2(a), and call it $\rho$. It has a redex consisting of two $\delta_{2}$ cells facing each other through their principal ports. The net $\rho$ can thus be rewritten according to the $\delta\delta$ rule, to another net $\pi$, as described in Figure 2(b). The net $\pi$ has no redex, and is thus said to be in normal form. Please observe that a vicious circle occurs in $\rho$, while no vicious circle can be found in $\pi$. This, in other words, is a witness of the fact that vicious circles are not preserved by reduction, in general. By the way, we consider vicious circles as a form of a divergent net, given the cyclic chain of $\gamma$ cells they contain.

2.3 Why One Token is Not Enough

In the geometry of interaction, at least in its classic incarnation [23, 13], the behaviour of a net is captured by how the net itself transforms a so-called token when the latter travels inside it. The net, in other words, is seen as a token transformer, and correctness of the semantics means that reduction turns nets into equivalent ones, i.e., into nets which behave the same when seen as token transformers. An example IC net can be found in Figure 5. Seen as a token transformer, the net sends any token which comes from the free port $p_{1}$ to $p_{3}$; on the other hand any token coming from $p_{2}$ gets stuck. This is because the $\gamma$ cells in the middle work by pushing a symbol on one of the token’s stacks when traversed from their secondary to their principal port, and, dually, they pop the symbol when traversed the other way round. The net rewrites to another simple net consisting of an $\varepsilon$ cell connected to the free port $p_{2}$ and a wire connecting two free ports $p_{1}$ and $p_{3}$, which (obviously) exhibits the same behaviour seen as a token transformer. This is indeed the way token machines are proved to be a sound model of net reduction in ICs [27].

The same kind of framework cannot work in MICs. To convince yourself about that, please consider the net in Figure 6, and call it $\rho$.

It can reduce to three essentially different nets, namely the ones in Figure 7, call them $\pi_{1},\pi_{2},\pi_{3}$. By analogy with the previous example, it is clear that the way tokens travel inside $\rho$ should “mimick” the way they travel in each of the $\pi_{i}$. But each of the three $\pi_{i}$ behaves very differently from the others, i.e., the nondeterminism in the choice of which two of the three $\delta_{2}$ cells in $\rho$ should interact is of a genuine kind. On top of that, there is also the fact that the subnet $\xi$ of $\rho$ could be replaced by a much more complicated net (e.g. that in Figure 2(a)) and thus nondeterministic choices cannot be (all) resolved initially, when the whole computation starts. Some of them need to wait for other choices to be made, have to be delayed, and thus naturally become nonlocal. One way to deal with nonlocal nondeterminism is to charge tokens the task of resolving it. The inevitable price to pay, however, is the fact that more than one token may flow around the net at the same time: there is no way to decide which ones of the many $\delta_{2}$ cells will be the first ones to meet, and the way out is to be “lazy” and allow all $\delta_{2}$ cells to look for a partner. In $\rho$, as an example, we would have six tokens, each starting at a principal port of one of the three $\delta_{2}$ cells. Their task is to look for another cell with which the $\delta_{2}$ cell they started from could marry. Once this is identified, the actual marriage can happen, but this must be an indivisible and irreversible operation, after which the same cell cannot marry anyone else. This, in turn, requires the presence of another kind of token, which is static and whose role is to keep track of the “civil state” of any $\delta_{2}$ cell, i.e. whether it is married or not.

The ones just described are the basic ingredients of the geometry of interaction model we are going to introduce in Section 4 below. Before doing that, however, we need to setup a simple theory of labelled bisimilarity without which one would not even have a way to define whether our semantics is correct.

3 Locative Transition Systems and Bisimilarity

Usual, single-token machines, can be seen as token-transformers, i.e., as partial functions capturing the input-output behaviour of a net seen as an automaton turning any token flowing into the net into a token flowing out of it. This simple picture does not hold anymore in the kind of multi-token machines we work with in this paper. The causal dependencies between tokens are much more complicated here, and we cannot simply proceed by letting token machines to take in input all tokens (like in [9, 10]). It is thus natural to see the token machines as labelled transition systems which interact with their environment by letting tokens to flow in and out of them.

It is convenient to introduce a special class of labelled transition systems, called locative transition systems, where labels are of a peculiar kind, namely consist of multisets of actions played at certain locations. Allowing more than one action to be played together, atomically, in turn allows more than one token to flow in and out at the same time. Locative transition systems support a natural form of parallel composition, and notions of (bi)similarity for which parallel composition can be shown to be a congruence. We will give the status of a locative transition system to multi-token machines in Section 4 below.

3.1 Locative Transition Systems

Action sets, i.e., finite set of actions, are ranged over by metavariables like $A$ and $B$. For each action set $A$, we assume the existence of an involution $\mathrm{dual}_{A}:A\rightarrow A$. If for some $a,b\in A$, $\mathrm{dual}_{A}(a)=b$, we often write $a\bot_{A}b$ or simply $a\bot b$. For every set $X$, let $\mathbb{M}(X)$ be the collection of all multisets on $X$, i.e., of all functions with domain $X$ and codomain $\mathbb{N}$. $\mathbb{FM}(X)$ is the subset of $\mathbb{M}(X)$ consisting of finite multisets only. To distinguish between sets and multisets, the latter are denoted with expressions like $\{{\kern-1.5pt}|x_{1},\dots,x_{n}|{\kern-1.5pt}\}$ instead of $\{x_{1},\ldots,x_{n}\}$, the latter standing for a set, as usual. Let $\mathcal{L}$ be a finite set of labels, and let $A$ be a set of actions. The expression $\mathcal{L}_{A}$ stands for the collection $\mathbb{FM}(\mathcal{L}\times A)$. Elements of $\mathcal{L}_{A}$ are denoted as $\mathsf{a},\mathsf{b}$, etc. Further, if $\sigma$ is a partial injection on $\mathcal{L}$, a multiset in $\mathbb{FM}(\mathcal{L}\times A)$ is said to be $\sigma$-dual if it is in the form

[TABLE]

where $b_{i}=\mathrm{dual}_{A}(a_{i})$ for every $1\leq i\leq n$. The set of $\sigma$-dual multisets is $\bot_{\sigma}$.

We are here interested in labelled transition systems whose labels are drawn from a set in the form $\mathcal{L}_{A}$. This is said to be a locative transition system on $\mathcal{L}_{A}$ (or a $\mathcal{L}_{A}$-LTS) and is an ordinary LTS $\mathbf{A}=(S_{\mathbf{A}},\rightarrow_{\mathbf{A}},s_{\mathbf{A}})$ where $S_{\mathbf{A}}$ is a set of states, $s_{\mathbf{A}}\in S_{\mathbf{A}}$ is the initial state, and $\rightarrow_{\mathbf{A}}\subseteq S_{\mathbf{A}}\times\mathcal{L}_{A}\times S_{\mathbf{A}}$ is the transition relation. We write $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow_{\mathbf{A}}}}t$ for ${(u,\mathsf{a},t)}\in{\rightarrow_{\mathbf{A}}}$.

The parallel composition of two locative transition systems requires a slightly complicated machinery to be defined. Given an $\mathcal{L}_{A}$-LTS $\mathbf{A}$, an $\mathcal{M}_{A}$-LTS $\mathbf{B}$ (where $\mathcal{L}$ and $\mathcal{M}$ are disjoint), and a partial injection $\sigma:\mathcal{L}\rightarrow\mathcal{M}$, one can define the $\sigma$-parallel composition $\mathbf{A}||_{\sigma}\mathbf{B}$ of $\mathbf{A}$ and $\mathbf{B}$ as the $\mathcal{N}_{A}$-LTS $(S_{\mathbf{A}}\times S_{\mathbf{B}},\leadsto,(s_{\mathbf{A}},s_{\mathbf{B}}))$ where $\mathcal{N}=\mathcal{L}\cup\mathcal{M}-\mathit{dom}(\sigma)-\mathit{rng}(\sigma)$, the transition relation $\leadsto$ is $\leadsto_{\mathbf{A}}\cup\leadsto_{\mathbf{B}}\cup\leadsto_{\mathbf{A}\mathbf{B}}$, where

[TABLE]

Informally, $\mathbf{A}||_{\sigma}\mathbf{B}$ can perform an action $\mathsf{a}$ iff either one of $\mathbf{A}$ or $\mathbf{B}$ can perform it on one of the non-shared locations, or both $\mathbf{A}$ and $\mathbf{B}$ perform some actions which, when put in parallel, result precisely in $\mathsf{a}$.

Again, please observe that a locative transition system evolves not by performing one (located) action $(\ell,a)$, but a multiset of such actions.

3.2 Bisimilarity

The notion of (strong) simulation and bisimulation relations on a $\mathcal{L}_{A}$-LTS can be defined as usual:

• •

given two such LTSs $\mathbf{A}$ and $\mathbf{B}$, a simulation is any subset $\mathcal{R}$ of $S_{\mathbf{A}}\times S_{\mathbf{B}}$ such that

$s_{\mathbf{A}}\;\mathcal{R}\;s_{\mathbf{B}}$;

• 2.

whenever $u\;\mathcal{R}\;t$ and $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}v$, it holds that $t\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}w$, where $v\;\mathcal{R}\;w$.

• •

given two such LTSs $\mathbf{A}$ and $\mathbf{B}$, a bisimulation is any subset $\mathcal{R}$ of $S_{\mathbf{A}}\times S_{\mathbf{B}}$ such that

$s_{\mathbf{A}}\;\mathcal{R}\;s_{\mathbf{B}}$;

• 2.

whenever $u\;\mathcal{R}\;t$ and $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}v$, it holds that $t\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}w$, where $v\;\mathcal{R}\;w$;

• 3.

whenever $u\;\mathcal{R}\;t$ and $t\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}w$, it holds that $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}v$, where $v\;\mathcal{R}\;w$.

Similarity and bisimilarity are themselves defined as usual:

[TABLE]

Weak simulation and bisimulation relations, similarity and bisimilarity on $\mathcal{L}_{A}$-LTSs are also defined as usual. Given any $\mathcal{L}_{A}$-LTS, the weak transition relation $\Rightarrow$ is defined as

[TABLE]

• •

given two such LTSs $\mathbf{A}$ and $\mathbf{B}$, a weak simulation is any subset $\mathcal{R}$ of $S_{\mathbf{A}}\times S_{\mathbf{B}}$ such that

$s_{\mathbf{A}}\;\mathcal{R}\;s_{\mathbf{B}}$;

• 2.

whenever $u\;\mathcal{R}\;t$ and $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}v$, it holds that $t\stackrel{{\scriptstyle\mathsf{a}}}{{\Rightarrow}}w$, where $v\;\mathcal{R}\;w$.

• •

given two such LTSs $\mathbf{A}$ and $\mathbf{B}$, a weak bisimulation is any subset $\mathcal{R}$ of $S_{\mathbf{A}}\times S_{\mathbf{B}}$ such that

$s_{\mathbf{A}}\;\mathcal{R}\;s_{\mathbf{B}}$;

• 2.

whenever $u\;\mathcal{R}\;t$ and $u\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}v$, it holds that $t\stackrel{{\scriptstyle\mathsf{a}}}{{\Rightarrow}}w$, where $v\;\mathcal{R}\;w$;

• 3.

whenever $u\;\mathcal{R}\;t$ and $t\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}w$, it holds that $u\stackrel{{\scriptstyle\mathsf{a}}}{{\Rightarrow}}v$, where $v\;\mathcal{R}\;w$.

Weak similarity and bisimilarity are defined as:

[TABLE]

Noticeably, parallel composition is commutative, modulo strong bisimilarity.

Lemma 1**.**

$\mathbf{A}||_{\sigma}\mathbf{B}\sim\mathbf{B}||_{\sigma^{-1}}\mathbf{A}$.

Proof.

We show that

[TABLE]

is a bisimulation. We have $(s_{\mathbf{A}},s_{\mathbf{B}})\;\mathcal{R}\;(s_{\mathbf{B}},s_{\mathbf{A}})$. Assume $(u_{\mathbf{A}},u_{\mathbf{B}})\;\mathcal{R}\;(u_{\mathbf{B}},u_{\mathbf{A}})$ and $(u_{\mathbf{A}},u_{\mathbf{B}})\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}(t_{\mathbf{A}},t_{\mathbf{B}})$ in $\mathbf{A}||_{\sigma}\mathbf{B}$. Let us distinguish three cases:

• •

If $((u_{\mathbf{A}},u_{\mathbf{B}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{B}}))\in\;\leadsto_{\mathbf{A}}$, then $u_{\mathbf{B}}=t_{\mathbf{B}}$ and $u_{\mathbf{A}}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}t_{\mathbf{A}}$. One can see that $\mathbf{B}||_{\sigma}\mathbf{A}$ is able to perform $(u_{\mathbf{B}},u_{\mathbf{A}})\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}(u_{\mathbf{B}},t_{\mathbf{A}})$ since $((u_{\mathbf{B}},u_{\mathbf{A}}),\mathsf{a},(u_{\mathbf{B}},t_{\mathbf{A}}))\in\;\leadsto_{\mathbf{A}}$.

• •

If $((u_{\mathbf{A}},u_{\mathbf{B}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{B}}))\in\;\leadsto_{\mathbf{B}}$, then we can proceed in the similar way.

• •

If $((u_{\mathbf{A}},u_{\mathbf{B}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{B}}))\in\;\leadsto_{\mathbf{A}\mathbf{B}}$, then there exist $\mathsf{b}\in\mathcal{L}_{A}$, $\mathsf{c}\in\mathcal{M}_{A}$ and $\mathsf{d}\in\bot_{\sigma}$ such that $u_{\mathbf{A}}\stackrel{{\scriptstyle\mathsf{b}}}{{\rightarrow}}t_{\mathbf{A}}\wedge u_{\mathbf{B}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}t_{\mathbf{B}}\wedge\mathsf{a}\cup\mathsf{d}=\mathsf{b}\cup\mathsf{c}$. By definition, $\sigma$-dual is equivalent to $\sigma^{-1}$-dual, thus we indeed have $((u_{\mathbf{B}},u_{\mathbf{A}}),\mathsf{a},(t_{\mathbf{B}},t_{\mathbf{A}}))\in\;\leadsto_{\mathbf{B}\mathbf{A}}$.

The opposite direction is similar. ∎

As expected, strong bisimilarity is a congruence for parallel composition:

Proposition 1**.**

If $\mathbf{A}\sim\mathbf{B}$, then $\mathbf{A}||_{\sigma}\mathbf{C}\sim\mathbf{B}||_{\sigma}\mathbf{C}$.

Proof.

Let $\mathcal{R}$ be a bisimulation relation between $\mathbf{A}$ and $\mathbf{B}$. We show that

[TABLE]

is a bisimulation. We have $(s_{\mathbf{A}},s_{\mathbf{C}})\;\hat{\mathcal{R}}\;(s_{\mathbf{B}},s_{\mathbf{C}})$ since $s_{\mathbf{A}}\;\mathcal{R}\;s_{\mathbf{B}}$. Assume that $(u_{\mathbf{A}},u_{\mathbf{C}})\;\hat{\mathcal{R}}\;(u_{\mathbf{B}},u_{\mathbf{C}})$, and $(u_{\mathbf{A}},u_{\mathbf{C}})\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}(t_{\mathbf{A}},t_{\mathbf{C}})$.

• •

If $((u_{\mathbf{A}},u_{\mathbf{C}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{C}}))\in\;\leadsto_{\mathbf{A}}$, then $u_{\mathbf{C}}=t_{\mathbf{C}}$ and $u_{\mathbf{A}}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}t_{\mathbf{A}}$. The latter and $u_{\mathbf{A}}\;\mathcal{R}\;u_{\mathbf{B}}$ imply $u_{\mathbf{B}}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}t_{\mathbf{B}}$ and $t_{\mathbf{A}}\;\mathcal{R}\;t_{\mathbf{B}}$ for some $t_{\mathbf{B}}$. Therefore $\mathbf{B}||_{\sigma}\mathbf{C}$ have the corresponding transition $((u_{\mathbf{B}},u_{\mathbf{C}}),\mathsf{a},(t_{\mathbf{B}},t_{\mathbf{C}}))\in\;\leadsto_{\mathbf{A}}$.

• •

If $((u_{\mathbf{A}},u_{\mathbf{C}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{C}}))\in\;\leadsto_{\mathbf{C}}$, then $u_{\mathbf{A}}=t_{\mathbf{A}}$ and $u_{\mathbf{C}}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}t_{\mathbf{C}}$. From the latter, it immediately follows that $(u_{\mathbf{B}},u_{\mathbf{C}})\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}(u_{\mathbf{B}},t_{\mathbf{C}})$.

• •

If $((u_{\mathbf{A}},u_{\mathbf{C}}),\mathsf{a},(t_{\mathbf{A}},t_{\mathbf{C}}))\in\;\leadsto_{\mathbf{A}\mathbf{C}}$, then there exist $\mathsf{b}\in\mathcal{L}_{A}$, $\mathsf{c}\in\mathcal{M}_{A}$ and $\mathsf{d}\in\bot_{\sigma}$ such that $u_{\mathbf{A}}\stackrel{{\scriptstyle\mathsf{b}}}{{\rightarrow}}t_{\mathbf{A}}\wedge u_{\mathbf{C}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}t_{\mathbf{C}}\wedge\mathsf{a}\cup\mathsf{d}=\mathsf{b}\cup\mathsf{c}$. We use $u_{\mathbf{A}}\;\mathcal{R}\;u_{\mathbf{B}}$ to obtain $t_{\mathbf{B}}$ such that $u_{\mathbf{B}}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}t_{\mathbf{B}}$ and $t_{\mathbf{A}}\;\mathcal{R}\;t_{\mathbf{B}}$. Now observe $((u_{\mathbf{B}},u_{\mathbf{C}}),\mathsf{a},(t_{\mathbf{B}},t_{\mathbf{C}}))\in\;\leadsto_{\mathbf{B}\mathbf{C}}$.

This concludes the proof. ∎

The same holds for weak bisimilarity:

Proposition 2**.**

If $\mathbf{A}\approx\mathbf{B}$, then $\mathbf{A}||_{\sigma}\mathbf{C}\approx\mathbf{B}||_{\sigma}\mathbf{C}$.

4 Multi-Token Machines

This section is devoted to defining the multi-token machines which are the object of study of this paper, and to proving some basic properties of them. In particular, we will give a Compositionality Theorem that will be very helpful in the following section.

4.1 States

States of a multi-token machine are just multisets of tokens, each of them consisting of a port in the underlying net, modelling where the token is, and of some auxiliary information (e.g. the token’s origin, some stacks, etc.), which varies depending on the token’s kind. All this will be formalised in this section.

A stack $\mathbf{s}$ is any sequence whose elements are either symbols from the alphabet $\{\mathtt{p},\mathtt{q}\}$ or natural numbers. Formally:

[TABLE]

where $n\in\mathbb{N}$ and $\epsilon$ is the empty stack. The set of all stacks is $\mathcal{STK}$. A configuration is a pair of stacks $(\mathbf{s},\mathbf{t})$, and is denoted with metavariables like $C,D$. The set of all configurations is $\mathcal{CON}$. We define the conjugate $\overline{\mathbf{s}}$ of a stack $\mathbf{s}$ as follows:

[TABLE]

Given a configuration $C=(\mathbf{s},\mathbf{t})$, its conjugate $\overline{C}$ is defined to be $(\overline{\mathbf{s}},\mathbf{t})$.

Throughout this section, wires of the underlying net will be ranged over by metavariables like $e,f,g$. A cell type is any element of the set $\mathcal{CT}=\{\gamma,\delta\}$. Cell types will be denoted with metavariables like $c$ an $d$. Tokens can be of one of four different kinds:

• •

Single status tokens, which are elements of $\mathcal{POR}^{\rho}\times\mathcal{STK}$. Graphically, single status tokens are denoted with $\blacksquare$.

• •

Married status tokens, which are elements of $\mathcal{POR}^{\rho}\times\mathcal{STK}\times\mathcal{CT}$. Graphically, married status tokens are denoted with $\times$.

• •

Marriage tokens, which are elements of $\mathcal{POR}^{\rho}\times\mathcal{CON}\times\mathcal{POR}^{\rho}\times\mathcal{CON}$. Graphically, marriage tokens are denoted with $\medbullet$.

• •

Matching tokens, which are elements of $\mathcal{POR}^{\rho}\times\mathcal{CON}\times\mathcal{POR}^{\rho}\times\mathcal{CON}$. Graphically, matching tokens are denoted with $\medcirc$.

The first components of tokens indicate their current positions. Status tokens must be placed at principal ports while matching tokens must lie at free ports. The second components of marriage and matching tokens are their current configurations. At the third and fourth components, marriage and matching tokens keep their origins and configurations as initially installed. The set of all tokens for the net $\rho$ is indicated as $\mathcal{TKS}^{\rho}$.

States of the machine we are defining will just be multisets of tokens, and are denoted with metavariables like $\mathsf{S}$ and $\mathsf{U}$. We assume that marriage tokens on auxiliary or principal ports of cells are always going out of the cells while those on free ports are coming in from the environment. For example, we depict two marriage tokens $(p,(\mathbf{s},\mathbf{t}),q,(\mathbf{u},\mathbf{v}))$ on a principal port $p$ of a $\gamma$ cell and $(p^{\prime},(\mathbf{s}^{\prime},\mathbf{t}^{\prime}),q^{\prime},(\mathbf{u}^{\prime},\mathbf{v}^{\prime}))$ on a port $p^{\prime}$ which is connected with $p$ by wire ($p^{\prime}$ may be either a port of another cell or a free port) as in Figure 8.

The initial state of the machine comprises one marriage token $(p,(\epsilon,\epsilon),p,(\epsilon,\epsilon))$ and one single status token $(p,\epsilon)$ for each principal port $p$ of each $\delta_{2}$ cell in the underlying net, as shown in Figure 9. Intuitively, those tokens in the initial state are in charge of keeping track of the status of the $\delta_{2}$ cell, and to look for possible partners for it.

4.2 Internal Transition Rules

The behaviour of multi-token machines is given by a series of transition rules which prescribe how and when a marriage token can move inside a net, and the protocol governing marriages.

Transition rules prescribing how token moves are in Figure 10.

Please observe how marriage tokens can flow through $\gamma$ cells more or less the same way they do in interaction combinators [27]: some symbol is either pushed or popped from their first stack. On the other hand, when tokens face a $\delta_{2}$ cell, there are in principle more than one possibility as for how they should move, all this depending on the presence of certain married status tokens.

As for transition rules performing marriages, they are in Figure 11.

The first rule handles the marriage between two $\delta_{2}$ cells, while the second one is charged of handling the case in which a $\delta_{2}$ cell marries a $\gamma$ cell. In the first case, it is as if the two $\delta_{2}$ cells have interacted with each other, thus annihilating themselves, and producing some $\varepsilon$ cells. Notice also how the marriage token which originated from the other principal port, is annihilated in the process; summing up, there are four tokens involved altogether. In the second case, the $\delta_{2}$ is virtually duplicated, and indeed some new (status and marriage) tokens are created, each one corresponding to a virtual copy of the $\delta_{2}$ cell. In both cases, (single and married) status tokens are in charge of guaranteeing atomicity, and of keeping track of whether each (copy of a) $\delta_{2}$ cell is single or married, in the latter case remembering also the nature of the cell’s partner. It is instructive to notice how marriages between two $\delta_{2}$ cells are bidirectional and symmetric in nature, while those between a $\delta_{2}$ cell and a $\gamma$ cell are asymmetric and unidirectional: the latter are inert and marriage tokens are meant to start their journey from $\delta_{2}$ cells uniquely.

4.3 External Transition Rules

As already pointed out, it is quite convenient to see token machines not simply as automata evolving as described in the previous section, but also as labelled transition systems having a nontrivial interactive behaviour. More specifically, token machines can interact with their environment through free ports by inputting or outputting a token, by letting a marriage happen, or by killing a token as a part of a marriage. This makes locative transition systems an ideal candidate for the kind of LTSs one needs here. External actions, which express the interactions which could happen at such a location, are generated by the following grammar:

[TABLE]

where $C$ ranges over $\mathcal{CON}$ and $c,d$ ranges over $\mathcal{CT}$. The set of external actions is indicated as $\mathcal{EA}$. We define $\mathrm{dual}_{\mathcal{EA}}$ by the following rules:

[TABLE]

Actually, any net $\rho$ can be turned into an $\mathcal{FPOR}^{\rho}_{\mathcal{EA}}$-LTS $\mathsf{TM}_{\rho}=(\mathbb{FM}(\mathcal{TKS}^{\rho}),\rightarrow,s_{\rho})$, which is said to be the token machine for $\rho$. This is done considering internal transition rules as producing the empty multiset of action, and by giving some external transition rules, namely those in Figure 12 and Figure 13. Multiple external actions involving distinct tokens can be combined in just one labelled transition: this is possible because labels of $\mathsf{TM}_{\rho}$ are multisets.

Let us briefly comment on the role of each rule:

• •

The first two rules in Figure 12 allow tokens to flow into the net (thus giving rise to an action $\mathsf{in}(C)$) or to flow out of the net (thus giving rise to an action $\mathsf{out}(C)$). In the latter case, something needs to keep track of the fact that a marriage token has indeed left the net (in a certain configuration): this is precisely the role of matching tokens, that is to say tokens of the fourth (and last) kind.

• •

The fourth and fifth rules in Figure 12 model the situation in which a $\delta_{2}$ cell performs a marriage “with the environment”, by way of a pair of marriage tokens, the first of which is as usual next to the cell, but the other has flown out the net, a fact witnessed by the presence of a matching token. The fourth rule takes care of the case in which the cell in the environment is itself a $\delta_{2}$ cell, while the fifth rule accounts for an asymmetric marriage with a $\gamma$ cell.

• •

We also have a rule (the third one in Figure 12) that models the marriage between a $\gamma$ cell and the environment.

• •

The sixth and seventh rules in Figure 12 forward marriage actions via the matching tokens, emitting dual actions.

• •

In the third and fourth rules in Figure 12, the marriage token which needs to be killed as a result of the marriage still lies in the net, but nothing guarantees that it has not flown out of the net itself. It is thus necessary to have some further rules, for example the first rule in Figure 13, in which we not only marry a $\delta_{2}$ cell with the environment but also kill a marriage token which has already flown out of the net, expressed by a $\mathsf{kill}(C)$ action.

• •

The last two rules in Figure 13 describe how a $\mathsf{kill}(C)$ action is forwarded and how it actually acts on a marriage token, by emitting the dual action $\mathsf{cokill}(C)$.

Having those external rules, two nets can now interact via external actions. The precise situation which it yields will be analysed in the next sections.

4.4 Basic Properties

The expression $\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}$ where $\emptyset$ is the empty multiset will be indicated simply as $\rightarrow$.

Lemma 2**.**

Marriage status tokens are inflationary, i.e., if $\mathsf{S}=\mathsf{U}\cup\{T\}$, $T$ is a status token, and $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{V}$, then $T\in\mathsf{V}$.

Proof.

This is simple case analysis: whenever we perform any internal or external action, status tokens can be created, but once they are part of the current state, they never change their status (and, in particular, they never disappear). ∎

In the rest of this section, we develop notions and lemmas to show Theorem 1, which will be proved in the next Section 4.5. Suppose we are working with $\mathsf{TM}_{\rho}$ and suppose that $\mathsf{S}\cup\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{V}$ where, however, only the tokens from $\mathsf{U}$ are allowed to evolve, while those from $\mathsf{S}$ cannot change their status. If this is the case, then $\mathsf{V}$ is necessarily in the form $\mathsf{S}\cup\mathsf{T}$, and we write $\mathsf{U}\stackrel{{\scriptstyle[}}{{\mathsf{S}}}]{\ell}{\rightarrow}\mathsf{T}$. Given a marriage token $T=(p,C,q,D)$ and a pair $(r,E)$ of a port $r$ and a configuration $E$, a token ${T}^{\mathit{OP}}_{r,E}$ is defined as $(p,\overline{C},r,E)$.

Given a token $T$ and multiset of tokens $\mathsf{S}$, an $(\mathsf{S},T)$-focused sequence ending in $Y$ is any sequence $\Theta$ of tokens in the form

[TABLE]

where $X_{1}=T$ and $X_{n}=Y$. The sequence $\Theta$ are also called an $(\mathsf{S},T)$-focused sequence or even an $\mathsf{S}$-sequence. A state $\mathsf{S}$ is said to be reachable from $\mathsf{U}$ iff there is a sequence of labelled transitions leading $\mathsf{U}$ to $\mathsf{S}$:

[TABLE]

A state $\mathsf{S}$ is said to be reachable iff it is reachable from the initial state of the underlying net. A marriage token is said to be an origin token iff its origin and current positions coincide. For every marriage token $T=(p,C,q,D)$, its origin token is $\mathsf{Orig}(T)=(q,D,q,D)$. For every matching token $T$, there is a naturally defined marriage token $\mathsf{M2M}(T)$, namely the one that originated $T$. Given a state $\mathsf{S}$ and a marriage token $T$, $T$ is said to be $\mathsf{S}$-canonical iff there is an $(\mathsf{S},\mathsf{Orig}(T))$-focused sequence ending in $T$. A matching token $T$ is $\mathsf{S}$-canonical if $\mathsf{M2M}(T)$ is. If $\mathsf{S}$ is such that for every marriage or matching token $T$ in $\mathsf{S}$, $T$ is $(\mathsf{S}-\{T\})$-canonical, then $\mathsf{S}$ is said to be, simply, canonical. Canonicity is preserved by internal or external interaction:

Lemma 3**.**

If $\mathsf{S}$ is canonical and $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{U}$, then $\mathsf{U}$ is canonical, too.

Proof.

This can be proved by a simple case analysis on the rule for $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{U}$. ∎

The way one builds $\mathsf{S}$-focused sequences is essentially a deterministic process:

Lemma 4**.**

Given two $\mathsf{S}$-focused sequences $\Theta$ and $\Xi$, either $\Theta$ is a prefix of $\Xi$ or vice versa.

No nondeterminism is involved in building $\mathsf{S}$-focused sequences:

Lemma 5**.**

$\mathsf{S}$-focused sequences are invertible, i.e. for every such computation

[TABLE]

and for every pair $(r,E)$ of a port $r$ and a configuration $E$, there exists another $\mathsf{S}$-focused sequence ${\Theta}^{\mathit{OP}}_{r,E}$ such that

[TABLE]

4.5 Compositionality

Consider any marriage or matching token $T$ in a state $\mathsf{S}\cup\{T\}$ of $\mathsf{TM}_{\rho||_{\sigma}\pi}$. If $T$ is $\mathsf{S}$-canonical, then we can trace back $T$ (or $\mathsf{M2M}(T)$) to an origin token $X$ by way of an $\mathsf{S}$-focused sequence. Lemma 5 tells us that from $X$ we can go back to $T$ (or $\mathsf{M2M}(T)$), again by way of an $\mathsf{S}$-focused sequence, that we call $\Theta$. Intuitively, $\Theta$ is the computation that brought $T$ where it is now. We can see it as a path in $\rho||_{\sigma}\pi$, and depict it graphically as follows:

In particular, $\Theta$ can cross the border between $\rho$ and $\pi$ several times. If we want to somehow simulate $\Theta$ in $\mathsf{TM}_{\rho}||_{\sigma}\mathsf{TM}_{\pi}$, we need to keep track of each crossing by a matching token lying at the border, on the side of the sub-net we are leaving. Let $\mathsf{U}$ the set of all these matching tokens which are tokens of either $\mathsf{TM}_{\rho}$ or of $\mathsf{TM}_{\pi}$. What we have just implicitly defined is a pair of states $g_{\rho}(\mathsf{S},T)$ and $g_{\pi}(\mathsf{S},T)$: they are defined as the portions of $\mathsf{S}\cup\mathsf{U}$ which are tokens of $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$, respectively. If $T$ is not $\mathsf{S}$-canonical, then

Theorem 1** (Compositionality).**

$\mathsf{TM}_{\rho||_{\sigma}\pi}\approx(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$.

Proof.

We need to define a binary relation $\mathcal{R}$ between the states of the two involved LTSs, and then prove it to be a bisimulation. The simplest way to describe $\mathcal{R}$ is as the set of all the pairs in the form $(\mathsf{S},f^{*}(\mathsf{S}))$, where $\mathsf{S}$ is a canonical state of $\rho||_{\sigma}\pi$, and $f^{*}$ is defined as

[TABLE]

and the partial function $f_{\rho}$ (respectively, $f_{\pi}$) maps a pair in the form $(\mathsf{S},T)$ into a state of $\mathsf{TM}_{\rho}$ (respectively, of $\mathsf{TM}_{\pi}$). The way $f_{\rho}$ and $f_{\pi}$ are defined depends on the nature of $T$. In particular,

• •

If $T$ is either a single status token or a marriage status token lying next to its natural position, say a cell in $\rho$, then $f_{\rho}(\mathsf{S},T)$ will be just $\{X\}$, where $X$ is the counterpart of $T$ in $\rho$, while $f_{\pi}(\mathsf{S},T)$ will be just $\emptyset$. Similarly when the position of $T$ is a cell in $\pi$. If $T$ is not at a natural position, then both $f_{\rho}$ an $f_{\pi}$ are undefined at $(\mathsf{S},T)$.

• •

If $T$ is a marriage or matching token, then $f_{\rho}(\mathsf{S},T)=g_{\rho}(\mathsf{S},T)$ and $f_{\pi}(\mathsf{S},T)=g_{\pi}(\mathsf{S},T)$ where $g_{\rho}$ and $g_{\pi}$ are the maps defined above.

We now need to prove that $\mathcal{R}$ is a bisimulation relation. To do that, we need to prove three statements:

We first of all need to show that $(s_{\rho||_{\sigma}\pi},(s_{\rho},s_{\pi}))\in\mathcal{R}$. To prove that, first of all observe that $s_{\rho||_{\sigma}\pi}$ does not contain any matching token, that all the marriage tokens in it are trivially canonical, and are thus mapped simply to “themselves” by $f^{*}$.

• 2.

We then need to show that if $(\mathsf{S},\mathsf{U})\in\mathcal{R}$ and $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{V}$, then $\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\Rightarrow}}\mathsf{T}$ where $(\mathsf{V},\mathsf{T})\in\mathcal{R}$. We need to analyse several cases:

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing a crossing internal transition, then the crossing can be easily simulated in $\mathsf{U}$, the only proviso being that if the involved marriage token in $\mathsf{S}$ lies at the border between $\rho$ and $\pi$, then the simulating transitions could be two instead of one, namely a crossing and matching input-output pair.

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing an internal $\delta\delta$ marriage, then the four involved marriage tokens are as follows

where $X$ and $Y$ originated in the leftmost cell, while $T$ and $Z$ originated in the rightmost cell. The four tokens are canonical, and are thus mapped by $f^{*}$ to four marriage tokens, possibly with some matching tokens lying along the paths leading each of them to its origin. Now, suppose, just as an example, that the leftmost cell and link above are in $\rho$, while rightmost cell and link are in $\pi$ (the other cases can be handled similarly). Summing up, then, we are in the following situation:

where the four depicted paths can of course, in principle, go back and forth between $\rho$ and $\pi$, even several times. Now, observe that:

• •

Along the four paths, appropriate matching tokens in $f^{*}(\mathsf{S})$ mark the crossing of the border between $\rho$ and $\pi$.

• •

Let $T=(q,\overline{C},p,D)$ and $Y=(p,\overline{D},q,C)$ (by definition of the initial state and transition rules they are necessarily in this form ). ${T}^{\mathit{OP}}_{q,C}=\mathsf{Orig}(Y)$ and ${Y}^{\mathit{OP}}_{p,D}=\mathsf{Orig}(T)$, and by Lemma 5, there exist paths from $\mathsf{Orig}(T)$ to $T$ and to $\mathsf{Orig}(Y)$ to $Y$ that are the inverses of each other. Then, the two paths and the matching tokens along them are of the form:

where $\sigma(p_{i})=p^{\prime}_{i}$ and $n=2n^{\prime}+1$ for some $n^{\prime}\geq 0$.

• •

The paths from $\mathsf{Orig}(X)$ to $X$ and from $\mathsf{Orig}(Z)$ to $Z$ are depicted together with the matching tokens along them as follows:

where $\sigma(q_{i})=q^{\prime}_{i}$, $\sigma(r_{i})=r^{\prime}_{i}$, $m=2m^{\prime}$ and $l=2l^{\prime}$ for $m^{\prime},l^{\prime}\geq 0$.

As a consequence, one can prove that $\mathsf{U}$ silently evolves to a state $\mathsf{T}$. More specifically, if $\mathsf{U}=(\mathsf{U}_{\rho},\mathsf{U}_{\pi})$, then:

• •

$\mathsf{U}_{\rho}$ performs an external $\delta\delta$ marriage and several marriages between free ports, triggering a bag of actions $\mathsf{a}_{\rho}$ consisting of:

• •

$(p_{1},\mathsf{ma}_{\delta\delta}(\mathbf{u}_{1},\mathbf{v}_{1}))$

• •

$(p_{2i},\mathsf{ma}_{\delta\delta}(\overline{\mathbf{u}_{2i}},\mathbf{v}_{2i}))$ and $(p_{2i+1},\mathsf{ma}_{\delta\delta}(\mathbf{u}_{2i+1},\mathbf{v}_{2i+1}))$ for each $i=1,\ldots,n^{\prime}$

• •

$(q_{2i-1},\mathsf{kill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(q_{2i},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,m^{\prime}$

• •

$(r_{2i-1},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(r_{2i},\mathsf{kill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,l^{\prime}$

• •

$\mathsf{U}_{\pi}$ performs an external $\delta\delta$ marriage and marriages between free ports which invoke $\mathsf{a}_{\pi}$ consisting of:

• •

$(p^{\prime}_{2i-1},\mathsf{ma}_{\delta\delta}(\overline{\mathbf{u}_{2i-1}},\mathbf{v}_{2i-1}))$ and $(p^{\prime}_{2i},\mathsf{ma}_{\delta\delta}(\mathbf{u}_{2i},\mathbf{v}_{2i}))$ for each $i=1,\ldots,n^{\prime}$

• •

$(p^{\prime}_{n},\mathsf{ma}_{\delta\delta}(\mathbf{u}_{n},\mathbf{v}_{n}))$

• •

$(q^{\prime}_{2i-1},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(q^{\prime}_{2i},\mathsf{kill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,m^{\prime}$

• •

$(r^{\prime}_{2i-1},\mathsf{kill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(r^{\prime}_{2i},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,l^{\prime}$

• •

We can see they are balanced, i.e., $\mathsf{a}_{\rho}\cup\mathsf{a}_{\pi}\in\bot_{\sigma}$. Thus $\mathsf{U}$ can perform these marriages in an internal transition. The resulting state $\mathsf{T}$ coincides with $f^{\ast}(\mathsf{V})$.

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing an internal $\gamma\delta$ marriage, then we have two marriage tokens involved:

Both of the tokens $X$ and $Y$ originated in the $\delta_{2}$ cell. Similarly to the case of $\delta\delta$ marriage, the marriage can be internally simulated in $(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$ via finitely many communication between $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$:

• •

The paths of $T$ and $X$ crosses the border finitely many times, for example as in the following figure, where $\sigma(p_{i})=p^{\prime}_{i}$, $n=2n^{\prime}+1$ for some $n^{\prime}\geq 0$, and $m=2m^{\prime}$ for some $m^{\prime}\geq 0$. .

• •

A bag of actions $\mathsf{U}_{\rho}$ in $\mathsf{a}_{\rho}$ consisting of

• •

$(p_{1},\mathsf{ma}_{\delta\gamma}(\mathbf{u}_{1},\mathbf{v}_{1}))$

• •

$(p_{2i},\mathsf{ma}_{\gamma\delta}(\overline{\mathbf{u}_{2i}},\mathbf{v}_{2i}))$ and $(p_{2i+1},\mathsf{ma}_{\delta\gamma}(\mathbf{u}_{2i+1},\mathbf{v}_{2i+1}))$ for each $i=1,\ldots,n^{\prime}$

• •

$(q_{2i-1},\mathsf{kill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(q_{2i},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,m^{\prime}$

and another bag of actions $\mathsf{U}_{\pi}$ in $\mathsf{a}_{\pi}$ consisting of

• •

$(p_{2i},\mathsf{ma}_{\delta\gamma}(\mathbf{u}_{2i},\mathbf{v}_{2i}))$ and $(p_{2i-1},\mathsf{ma}_{\gamma\delta}(\overline{\mathbf{u}_{2i-1}},\mathbf{v}_{2i-1}))$ for each $i=1,\ldots,n^{\prime}$

• •

$(p_{n},\mathsf{ma}_{\gamma\delta}(\overline{\mathbf{u}_{1}},\mathbf{v}_{1}))$

• •

$(q_{2i-1},\mathsf{cokill}(\mathbf{u}^{\prime}_{2i-1},\mathbf{v}^{\prime}_{2i-1}))$ and $(q_{2i},\mathsf{kill}(\mathbf{u}^{\prime}_{2i},\mathbf{v}^{\prime}_{2i}))$ for each $i=1,\ldots,m^{\prime}$

allow us to perform an internal marriage that yields a state $\mathsf{T}=f^{*}(\mathsf{V})$.

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing any other internal transition, it must be an internal transition on a marriage token that does not cross the border. We can easily obtain $\mathsf{T}=f^{*}(\mathsf{V})$ by performing an internal transition on the corresponding marriage token in the same side (either in $\mathsf{TM}_{\rho}$ or $\mathsf{TM}_{\pi}$) of the token machine.

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing input action $\mathsf{in}({C})$, it is again easily simulated in $(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$ by performing the same input action on the same free port.

• •

If $\mathsf{V}$ is obtained from $\mathsf{S}$ by performing output action $\mathsf{out}({C})$ on a token with stacks $C$, there must be a token with the same stack $C$ on the same free port in $(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$. We can simulate the action by performing output action on that token.

• •

The other cases (external marriages and killing/killed) can be simulated similarly to the internal marriage cases: a corresponding action and several times of communication between $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$ yield the state $\mathsf{T}=f^{*}(\mathsf{V})$.

• •

The cases above extend to any external transition with multiple actions. This is because of the following reason. For each action, the involved tokens have their path from its origin as discussed above. Those paths (and matching tokens along them) are all distinct and thus their corresponding transitions in $(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$ do not interfere with each other.

• 3.

We then need to show that if $(\mathsf{S},\mathsf{U})\in\mathcal{R}$ and $\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{V}$, then $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\Rightarrow}}\mathsf{T}$ where $(\mathsf{T},\mathsf{V})\in\mathcal{R}$. By definition, the transition relation $\rightarrow$ on $(\mathsf{TM}_{\rho})||_{\sigma}(\mathsf{TM}_{\pi})$ is the union of three relations $\rightarrow_{\rho}$, $\rightarrow_{\pi}$ and $\rightarrow_{\rho\pi}$. Now, if $\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\rightarrow_{\rho}}}\mathsf{V}$ or $\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\rightarrow_{\pi}}}\mathsf{V}$, then finding $\mathsf{T}$ is trivial. If, on the other hand, $\mathsf{U}\stackrel{{\scriptstyle\ell}}{{\rightarrow_{\rho\pi}}}\mathsf{V}$, then by definition,

[TABLE]

Again, if $\xi=\emptyset$, then finding $\mathsf{T}$ with the required property is trivial because $\mathsf{S}\stackrel{{\scriptstyle\nu_{\rho}}}{{\rightarrow}}\mathsf{T}$ and $\mathsf{S}\stackrel{{\scriptstyle\nu_{\pi}}}{{\rightarrow}}\mathsf{T}$, then $\mathsf{S}\stackrel{{\scriptstyle\ell}}{{\rightarrow}}\mathsf{T}$, since $\ell=\nu_{\rho}\cup\nu_{\pi}$. If $\xi$ is not empty, then we need to analyse several cases, keeping in mind that $\xi$ is by definition of parallel composition a $\sigma$-dual multiset:

• •

Suppose that $(\ell,\mathsf{out}(C))\in\xi$. Then, $(\sigma(\ell),\mathsf{in}(C))$ is also an element of $\xi$. This can be simulated in $\mathsf{S}$ by just an internal transition. Similarly if $(\ell,\mathsf{in}(C))\in\xi$.

• •

Suppose that $(\ell,\mathsf{ma}_{\gamma\delta}(C))\in\xi$ as an effect of an external marriage between a $\gamma$ cell and a free port. Then there must also be another action $(\sigma(\ell),\mathsf{ma}_{\delta\gamma}(\overline{C}))$ in $\xi$. We can think of this action as being produced by a (possibly empty) chain of marriages between two free ports alternating between $\rho$ and $\pi$. The fact that the chain alternates is again due to $\sigma$-duality of $\xi$. Let us distinguish a few further cases depending on the rule in which this chain ends:

• •

If the chain ends in an external marriage between a $\delta$ cell and a free port, then the whole chain, including its extremes, can be simulated by just an internal $\gamma\delta$ marriage. If the latter comes in its version with a killing action in the form $(\ell^{\prime},\mathsf{kill}(C))$, then we need to do the same kind of chain-based reasoning.

• •

If the chain ends in a marriage between two free ports one of the two not being in the domain of $\sigma$, then the whole chain, including its extremes, can be simulated by an external marriage between a $\gamma$ cell and a free port.

• •

Suppose that $(\ell,\mathsf{ma}_{\gamma\delta}(C))\in\xi$ as the effect of an external marriage between an $\delta$ and a free port. Then, again, we can proceed as in the last but previous case, with an additional complication due to the presence of killing actions at both extremes of the chain.

• •

Suppose that $(\ell,\mathsf{ma}_{\gamma\delta}(C))\in\xi$ as the effect of an external marriage between two free ports. Then we can proceed with the usual chain-based reasoning, but on both sides of the action we have just identified.

This way, we can “strip-off” all the actions from $\xi$ and $\ell$, and each of the chains of actions identified above corresponds to an action in $\mathsf{TM}_{\rho||_{\pi}\sigma}$.

∎

While the Compositionality Theorem holds in single-token machines as well [13], it has not been considered in existing work on multi-token machines [9, 10], partially because the kind of nets to which the theory can be applied, the so-called closed nets, is quite restricted.

5 Soundness

As already mentioned several times, the transition rules for our token machines are tailored for capturing the behaviours of interaction rules of MICs. This intention is unsurprisingly formalised as a bisimulation between the machine for a net containing a redex (say $\rho$) and the machine for the net containing its reduct (say $\pi$). This, of course, must be done for each interaction rule. However, there is a subtlety. While the result for $\gamma\gamma$ rule is a mere bisimulation of the two machines $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$, those for the rules involving $\delta_{2}$ cells (i.e., $\gamma\delta$ and $\delta\delta$ rules) are not; instead, the results are described as bisimulations between the machines $\mathsf{TM}_{\pi}$ and $\mathsf{TM}_{\rho}$ in which the initial state is replaced by a state after a specific marriage transition. At the level of the entire machines $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$, the relations are thus simulations rather than bisimulations. This is because the token machine for a net is designed to simulate any possible sequence of reductions from it, while the reduction under consideration is a particular one of those all possibilities, since reduction is nondeterministic. Therefore, a reduction on a $\delta_{2}$ cell always results in discarding some otherwise possible behaviours. This is faithfully handled by a marriage transition in the token machine $\mathsf{TM}_{\rho}$ corresponding to that reduction. In the following three lemmas, we study how $\mathsf{TM}_{\rho}$ and $\mathsf{TM}_{\pi}$ relate whenever $\rho\rightarrow\pi$. This is done by giving certain relations, that we indicate with $\mathcal{R}^{\rho}_{\pi}$, between the states of $\mathsf{TM}_{\rho}$ and those of $\mathsf{TM}_{\pi}$. Those relations will be useful also in Section 6 below.

Let us first consider $\gamma\gamma$ reduction. In this case, the machines for the redex and the reduct behave precisely the same:

Lemma 6**.**

If $\rho\rightarrow_{\gamma\gamma}\pi$, then $\mathsf{TM}_{\rho}\approx\mathsf{TM}_{\pi}$.

Proof.

If $\rho\rightarrow_{\gamma\gamma}\pi$, then we are in the following situation:

where $p,q,r,s$ indicate the free ports of $\rho$ and $\pi$. We have a partial function $f:\mathcal{TKS}^{\rho}\rightharpoonup\mathcal{TKS}^{\pi}$ such that:

• •

Matching tokens are mapped to the same position in $\pi$ if their origins are free ports.

• •

Marriage tokens are pushed back to their origins in $\pi$ if they are $\emptyset$-canonical. Pictorially, it can be illustrated as:

and similarly for downward tokens.

The relation $\mathcal{R}$ we are looking for is defined as a pointwise extension of $f$. We can now show that, indeed, $\mathcal{R}$ is a bisimulation relation.

• •

Both $s_{\rho}$ and $s_{\pi}$ are empty. By definition, $\mathcal{R}$ relates $s_{\rho}$ and $s_{\pi}$.

• •

Assume $\mathsf{S}_{\rho}\;\mathcal{R}\;\mathsf{S}_{\pi}$ and $\mathsf{S}_{\rho}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}\mathsf{U}_{\rho}$. We need to find $\mathsf{S}_{\pi}\stackrel{{\scriptstyle\mathsf{a}}}{{\Rightarrow}}\mathsf{U}_{\pi}$ such that $\mathsf{U}_{\rho}\;\mathcal{R}\;\mathsf{U}_{\pi}$. Let us proceed by analysing the three transition types.

• •

If $\mathsf{a}=\emptyset$, then the transition must be an internal move of a marriage token because internal marriages never happen in $\rho$. The definition of $f$ tells us that $\mathsf{U}_{\rho}\;\mathcal{R}\;\mathsf{S}_{\pi}$, so we can take $\mathsf{U}_{\pi}=\mathsf{S}_{\pi}$.

• •

If $\mathsf{a}$ is an input action, let $\mathsf{U}_{\rho}=\mathsf{S}_{\rho}\uplus\{{\kern-1.5pt}|T|{\kern-1.5pt}\}$ where $T$ is the incoming token. Observe that $\mathsf{S}_{\pi}$ can evolve into $\mathsf{U}_{\pi}=\mathsf{S}_{\pi}\uplus\{{\kern-1.5pt}|T|{\kern-1.5pt}\}$ by performing the same input action and $\mathsf{U}_{\rho}\;\mathcal{R}\;\mathsf{U}_{\pi}$.

• •

If $\mathsf{a}$ is an output action, let $\mathsf{U}_{\rho}=\mathsf{S}_{\rho}\setminus\{{\kern-1.5pt}|T|{\kern-1.5pt}\}\uplus\{{\kern-1.5pt}|X|{\kern-1.5pt}\}$ where $T$ is the outgoing token and $X$ is a matching token. We can see that $f(T)$ is also ready to flow out and hence $\mathsf{S}_{\pi}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}\mathsf{S}_{\pi}\setminus\{{\kern-1.5pt}|f(T)|{\kern-1.5pt}\}\uplus\{{\kern-1.5pt}|X|{\kern-1.5pt}\}$.

• •

If $\mathsf{a}$ is a bunch of external marriages, then they should be marriages between free ports because no marriage tokens in $\mathsf{S}_{\rho}$ are placed on $e$ with empty $\gamma$-stacks. These actions come from matching tokens in $\mathsf{S}_{\rho}$ and let $\mathsf{V}$ be such tokens. They are included in $\mathsf{S}_{\pi}$ as well. Thus we have $\mathsf{S}_{\pi}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}\mathsf{S}_{\pi}\setminus\mathsf{V}$.

• •

Assume $\mathsf{S}_{\rho}\;\mathcal{R}\;\mathsf{S}_{\pi}$ and $\mathsf{S}_{\pi}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}\mathsf{U}_{\pi}$. As $\pi$ doesn’t allow any internal actions, we consider external actions.

• •

If $\mathsf{a}$ is an input, then we can find the counterpart in $\rho$ as we did before.

• •

If $\mathsf{a}$ is an output, we can suppose, without loss of generality, a marriage token $T=(r,(\mathbf{s},\mathbf{t}),r,(\mathbf{s},\mathbf{t}))\in\mathsf{S}_{\pi}$ flows out through $p$. Then $\mathsf{S}_{\rho}$ has a marriage token which belongs to $f^{-1}(T)$. The token can reach $p$ with a configuration $(\mathbf{s},\mathbf{t})$ after a few internal transitions and its origin is the same as $T$. So it allows $\mathsf{TM}_{\rho}$ to perform the compatible output action.

• •

If $\mathsf{a}$ consists of marriages, $\mathsf{TM}_{\rho}$ is able to consume the corresponding matching tokens in $\mathsf{S}_{\rho}$.

∎

If one of the cells involved in a reduction is a $\delta_{2}$ cell, one cannot hope to get a result as strong as Lemma 6:

Lemma 7**.**

If $\rho\rightarrow_{\gamma\delta}\pi$, then there is $t_{\rho}$ such that $s_{\rho}\rightarrow t_{\rho}$ by an internal marriage transition and $(\mathbb{FM}(\mathcal{TKS}^{\rho}),\rightarrow,t_{\rho})\approx\mathsf{TM}_{\pi}$.

Proof.

We are in the following situation:

Observe that $s_{\rho}$ can perform a marriage between the $\gamma$ and $\delta_{2}$ cells, resulting in a state $t_{\rho}$ which has 1 married status tokens, 5 single status tokens and 4 marriage tokens. We denote the 2 status tokens in $t_{\rho}$ which have empty $\gamma$ stacks by $\mathsf{V}$. We define a relation $\mathcal{R}$ between $\mathbb{FM}(\mathcal{TKS}^{\rho})$ and $\mathbb{FM}(\mathcal{TKS}^{\pi})$, which is described in a pointwise manner as follows:

• •

Status tokens in $\rho$ whose topmost symbols are $\mathtt{p}$ (resp. $\mathtt{q}$) are related to ones of the $\delta$ cell on the left (resp. on the right) in $\pi$:

and similarly for married status tokens.

• •

Marriage tokens originating from principal ports are related if their origins are related in a similar way to the one described above. Marriage tokens originating from free ports are related if they have the same origins.

• •

Matching tokens are related similarly to marriage tokens.

Then let $\mathcal{R}^{\prime}=\{(\mathsf{S}_{\rho},\mathsf{S}_{\pi})\mid(\mathsf{S}_{\rho}-\mathsf{V},\mathsf{S}_{\pi})\in\mathcal{R},\mathsf{S}_{\rho}\text{ and }\mathsf{S}_{\pi}\text{ are canonical}\}$. We claim $\mathcal{R}^{\prime}$ is a bisimulation.

• •

We can see that $\mathcal{R}^{\prime}$ relates $t_{\rho}$ and $s_{\pi}$.

• •

Suppose $(\mathsf{S}_{\rho},\mathsf{S}_{\pi})\in\mathcal{R}^{\prime}$ and $\mathsf{S}_{\rho}\stackrel{{\scriptstyle\mathsf{a}}}{{\rightarrow}}\mathsf{U}_{\rho}$.

• •

If $\mathsf{a}=\emptyset$, then one of marriage tokens in $\mathsf{S}_{\rho}$ moved. But the marriage token and its counterpart in $\mathsf{S}_{\pi}$ are still related and so $\mathsf{S}_{\pi}$ can remain unchanged.

• •

If $\mathsf{a}$ is an input action, it is easy to see that making the same input in $\pi$ will lead $\mathsf{S}_{\pi}$ to a state related to $\mathsf{U}_{\rho}$.

• •

If $\mathsf{a}$ is an output action, let $T$ be the outgoing token in $\mathsf{S}_{\rho}$ and $T^{\prime}$ be the token in $\mathsf{S}_{\pi}$ related to $T$. There are two cases.

• •

If the origin of $T$ is a principal port, then the pair of $T$ and $T^{\prime}$ is one of the following pairs:

In any case, $T^{\prime}$ can reach the same position and configuration as $T$ within zero or one transition steps. Thus we have $\mathsf{S}_{\pi}\stackrel{{\scriptstyle\mathsf{a}}}{{\Rightarrow}}\mathsf{U}_{\pi}$.

• •

If the origin of $T$ is a free port, then $T^{\prime}$ is on this free port. By definition of $\mathcal{R}^{\prime}$, $\mathsf{S}_{\rho}$ has a status tokens $Y$ which is necessary for $T$ to make a trip from its origin to its current position. The counterpart $Y^{\prime}$ for $Y$ is contained in $\mathsf{S}_{\pi}$ and indeed helps $T^{\prime}$ to go to the correct location. For instance, let us consider the situation below, in which we have $T=(r,(\mathbf{s},\mathbf{t}\mathtt{1}),p,(\mathbf{s}\mathtt{p},\mathbf{t}))$, $T^{\prime}=(r,(\mathbf{s}\mathtt{p},\mathbf{t})),p,(\mathbf{s}\mathtt{p},\mathbf{t}))$ and $Y=(q,(\mathbf{s}\mathtt{p},\gamma))$. Notice that $T^{\prime}$ can arrive at $r$ thanks to $Y^{\prime}=(q_{l},(\mathbf{s},\gamma))$.

• •

If $\mathsf{a}$ is a multiset of external marriages, each element of $\mathsf{a}$ is either a marriage between a principal port and a free port or one between two free ports.

• •

A marriage between two free ports involves one or two matching tokens whose origins are free ports. Since such matching tokens in $\mathsf{S}_{\rho}$ are related to their copies in $\mathsf{S}_{\pi}$, $\mathsf{S}_{\pi}$ can imitate that marriage.

• •

A marriage between a principal port and a free port provokes one marriage action, whose marriage type is either $\gamma\delta$, $\delta\delta$ or $\delta\gamma$. The pictures below illustrate how $\pi$ simulates the external marriage in $\rho$ for each marriage type.

• •

$\gamma\delta$

• •

$\delta\delta$

• •

$\delta\gamma$

• •

For the other direction, we can proceed similarly.

∎

Lemma 8**.**

If $\rho\rightarrow_{\delta\delta}\pi$, then there is $t_{\rho}$ such that $s_{\rho}\rightarrow t_{\rho}$ by an internal marriage transition and $(\mathbb{FM}(\mathcal{TKS}^{\rho}),\rightarrow,t_{\rho})\approx\mathsf{TM}_{\pi}$.

Proof.

Assume that the reduction is an interaction between two first principal ports of two $\delta_{2}$ cells.

We can see $s_{\rho}$ immediately evolves into $t_{\rho}$, which consists of 2 married status tokens and 2 single status tokens. We define a relation $\mathcal{R}\subseteq\mathbb{FM}(\mathcal{TKS}^{\rho})\times\mathbb{FM}(\mathcal{TKS}^{\pi})$ as:

• •

Matching tokens are related naturally.

• •

Marriage tokens in $\rho$ which originated in free ports and are $t_{\rho}$-canonical are related to the natural counterparts in $\pi$ for their origins.

The bisimulation between $t_{\rho}$ and $s_{\pi}$ is given by $\mathcal{R}^{\prime}=\{(\mathsf{S}_{\rho}\uplus t_{\rho},\mathsf{S}_{\pi})\mid(\mathsf{S}_{\rho},\mathsf{S}_{\pi})\in\mathcal{R}\}$. The proof that $\mathcal{R}^{\prime}$ is a bisimulation is very much similar to the one of Lemma 6. ∎

One may wonder why a $\gamma\delta$ reduction is treated the same as a $\delta\delta$ reduction, since no nondeterminism seems to be involved in it. This is however, only apparent: if a $\delta_{2}$ cell may “choose” to interact with either a $\delta_{2}$ or a $\gamma$ cell, it does not loose any behaviour only up to $\eta$-equivalence (see [33] for a definition) when choosing to interact with the $\gamma$ cell. GoI, on the other hand, is well-known not to be sound for $\eta$ in general. In other words, although $\gamma\delta$ reduction is deterministic as far as rewriting on nets is concerned, it is not so at the level of the underlying GoI model, and this happens for deep reasons which have little to do with MICs.

As a corollary of the three lemmas above, we can prove soundness of our model with respect to net reduction, which is spelled out as a similarity:

Corollary 1** (Soundness).**

If $\rho\rightarrow\pi$, then $\mathsf{TM}_{\pi}\precapprox\mathsf{TM}_{\rho}$.

Proof.

This follows from Lemma 6, Lemma 7, and Lemma 8. Indeed, if $s_{\rho}\rightarrow t_{\rho}$, then $(\mathbb{FM}(\mathcal{TKS}^{\rho}),\rightarrow,t_{\rho})\precapprox\mathsf{TM}_{\rho}$. ∎

6 Adequacy

Corollary 1 tells us that, along any interaction path (of which there could be many) starting from any net $\rho$, one finds nets whose token machines can all be related by way of weak similarity to $\mathsf{TM}_{\rho}$. This already tells us much about the way nets and token machines are related. However, there is still no result around about the relationship between the behaviour of $\mathsf{TM}_{\rho}$ and that of $\rho$ itself, e.g., any result on whether there is a way to “read” a property of $\rho$ from its interpretation $\mathsf{TM}_{\rho}$. This section is devoted to proving that, indeed, $\rho$ and its token machine have the same behaviour as for termination. This means that token machines are not only a sound but also an adequate model of multiport interaction, since termination is the most natural property to be observed.

Before stating adequacy, we need to introduce some more preliminary definitions and notations. In particular, in this section, contrarily to the previous ones, token machines will be seen as non-interactive objects, and thus analysed as closed systems. A (unlabelled) transition system (TS for short; also known as a Kripke structure) consists of a set $S$ of states and a binary relation ${\rightarrow}\subseteq S\times S$. A pointed transition system is a triple $(S,\rightarrow,s)$ where $(S,\rightarrow)$ is a TS and $s\in S$ is the initial state. Notions of simulation and bisimulation can easily be given for pointed transition systems. Noticeably, in a simulation we require each transition in the simulated TS to correspond to zero or more transitions in the simulating TS. We indicate the obtained notions of (weak) bisimilarity and similarity as $\approx$ and $\precapprox$, as usual. Given a transition system $\mathbf{A}=(S,\rightarrow)$, we define the following two predicates parametrised by an element $\mathsf{S}$ of $S$ and by a set of elements $\mathbf{X}$:

• •

$\mathit{fin}_{\mathbf{A}}^{\mathbf{X}}(\mathsf{S})$, which holds iff there is a finite transition sequence starting in $\mathsf{S}$ and ending in a normal form not in $\mathbf{X}$.

• •

$\mathit{inf}_{\mathbf{A}}^{\mathbf{X}}(\mathsf{S})$, which instead holds iff there is an infinite transition sequence starting in $\mathsf{S}$, or a finite transition sequence starting in $\mathsf{S}$ and ending in an element in $\mathbf{X}$.

$\mathsf{NETS}$ can be seen as a transition system whose states are nets, and whose transition relation is the one induced by the reduction relation. Let $\mathbf{VC}$ be the set of nets containing vicious circles. For any net $\rho$, the set $\mathsf{TM}_{\rho}$ can itself be seen as a transition system whose states are elements of $\mathcal{TKS}^{\rho}$ and whose transition relation consists of internal transitions.

Theorem 2** (Adequacy).**

For every net $\rho$, the following holds:

[TABLE]

The rest of this section will be devoted to proving the four implications which together form Theorem 2.

6.1 Standard Computations

In this section we define a key notion, called standard computation, which plays a crucial role to prove Adequacy. In the following, a computation means a transition sequence starting in the initial state of the underlying token machine.

A thunk is any transition sequence in one of two forms:

• •

Either in the form $\Theta,\Xi,\Pi$, where

[TABLE]

where $T_{1}$ and $X_{1}$ are origin tokens, and $\Pi$ is a $\delta\delta$ marriage whose main tokens are $T_{n}$ and $X_{m}$;

• •

Or in the form $\Theta,\Xi$, where

[TABLE]

$T_{1}$ is an origin token, and $\Xi$ is a $\gamma\delta$ marriage whose main token is $T_{n}$.

A standard sequence is a transition sequence in one of two forms:

• •

Either in the form $\Theta_{1},\ldots,\Theta_{n},\Xi$ where $\Theta_{1},\ldots,\Theta_{n}$ are all thunks, and $\Xi$ is any maximal transition sequence not containing any marriage step, called a continuation.

• •

Or in the form $\Theta_{1},\Theta_{2},\ldots$, where all the $\Theta_{i}$ (where $i\in\mathbb{N}^{+}$) is a thunk.

A standard computation is a computation which is a standard sequence. The key insight is that any maximal computation can be “represented” by a standard computation. Formally, we have the following lemma:

Lemma 9** (Standardisation).**

• •

Let $\Theta\colon s_{\mathsf{TM}_{\rho}}\rightarrow\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}\rightarrow\cdots\rightarrow\mathsf{S}_{n}$ be a finite maximal computation of $\mathsf{TM}_{\rho}$. There exists a finite standard computation $\Xi\colon s_{\mathsf{TM}_{\rho}}\rightarrow\mathsf{U}_{1}\rightarrow\mathsf{U}_{2}\rightarrow\cdots\rightarrow\mathsf{U}_{m}$ s.t. $\mathsf{U}_{m}=\mathsf{S}_{n}$.

• •

Let $\Theta:s_{\mathsf{TM}_{\rho}}\rightarrow\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}\rightarrow\cdots$ be an infinite maximal computation of $\mathsf{TM}_{\rho}$. There exists an infinite standard computation $\Xi\colon s_{\mathsf{TM}_{\rho}}\rightarrow\mathsf{U}_{1}\rightarrow\mathsf{U}_{2}\rightarrow\cdots$ s.t. for any state $\mathsf{S}_{i}$ right after a marriage in $\Theta$, there exists a state $\mathsf{U}_{i^{\prime}}=\mathsf{S}_{i}$ in $\Xi$.

Proof.

First we show the following auxiliary propositions.

Proposition 3**.**

*In any token machine, the following three hold.

Let $\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}$ be a move on a token $T$ and $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$ be a move on another $X\neq T$. Then there exists a state $\mathsf{S}^{\prime}_{1}$ satisfying $\mathsf{S}_{0}\rightarrow\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}_{2}$, where $\mathsf{S}_{0}\rightarrow\mathsf{S}^{\prime}_{1}$ is a move on $X$ and $\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}_{2}$ is a move on $T$.

• 2.

Let $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$ be a marriage and $\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}$ be a move on a token $T$ not involved in the marriage $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$. Then there exists a state $\mathsf{S}^{\prime}_{1}$ satisfying $\mathsf{S}_{0}\rightarrow\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}_{2}$, where $\mathsf{S}_{0}\rightarrow\mathsf{S}^{\prime}_{1}$ is a marriage on the same token(s) as the one $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$, and $\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}_{2}$ is a move on $T$.

• 3.

Let $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$ be a marriage and $\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}$ be a move on a token $T$ killed by the marriage $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$. Then $\mathsf{S}_{0}\rightarrow\mathsf{S}_{2}$, by a marriage on the same token(s).

Proof.

Any move transition does not affect the other token’s move transition. This is in particular because any move transition does not put any marriage status token by definition.

• 2.

Since $\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}$ is already allowed to happen before the marriage $\mathsf{S}_{1}\rightarrow\mathsf{S}_{2}$, there is already some marriage status token(s) that allow $T$ to move in $\mathsf{S}_{0}$. Since any marriage does not delete a marriage status token by definition, the move is still possible in $\mathsf{S}^{\prime}_{1}$.

• 3.

Since $\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}$ is a move, it does not put any new token nor change any other token’s stacks by definition.

∎

Let $\Theta\colon\mathsf{S}_{0}\rightarrow\mathsf{S}_{1}\rightarrow\cdots\rightarrow\mathsf{S}_{k}\rightarrow\mathsf{S}_{k+1}\rightarrow\mathsf{S}_{k+2}\rightarrow\cdots\rightarrow\mathsf{S}_{n}$ be a finite maximal transition sequence where $\mathsf{S}_{k}\rightarrow\mathsf{S}_{k+1}$ is the first marriage in the sequence $\Theta$. We first permute $\Theta$, by repeatedly applying Proposition 3.1, into another transition sequence $\Theta^{\prime}\colon\mathsf{S}_{0}\rightarrow^{*}\mathsf{S}^{\prime}_{1}\rightarrow^{*}\mathsf{S}^{\prime}_{2}\rightarrow^{*}\mathsf{S}_{k}\rightarrow\mathsf{S}_{k+1}\rightarrow\mathsf{S}_{k+2}\rightarrow\cdots\rightarrow\mathsf{S}_{n}$, where $\mathsf{S}_{0}\rightarrow^{*}\mathsf{S}^{\prime}_{1}$ is one (if the marriage is $\gamma\delta$) or two (if the marriage is $\delta\delta$) consecutive focused sequences on the token(s) involved in the marriage, $\mathsf{S}^{\prime}_{1}\rightarrow^{*}\mathsf{S}^{\prime}_{2}$ consists only of moves on tokens not involved in the marriage, $\mathsf{S}^{\prime}_{2}\rightarrow^{*}\mathsf{S}_{k}$ consists only of moves on tokens killed by the marriage, and the rest is the same as $\Theta$. Then, applying Proposition 3.2 and 3.3, we obtain a transition sequence $\Theta^{\prime\prime}\colon\mathsf{S}_{0}\rightarrow^{*}\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}^{\prime}_{2}\rightarrow^{*}\mathsf{S}_{k+1}\rightarrow\mathsf{S}_{k+2}\rightarrow\cdots\rightarrow\mathsf{S}_{n}$, where $\mathsf{S}_{0}\rightarrow^{*}\mathsf{S}^{\prime}_{1}$ is focused sequences on the token(s) involved in the marriage $\mathsf{S}^{\prime}_{1}\rightarrow\mathsf{S}^{\prime}_{2}$, i.e. with a thunk at its head. If the subsequence $\mathsf{S}^{\prime}_{2}\rightarrow^{*}\mathsf{S}_{k+1}\rightarrow\mathsf{S}_{k+2}\rightarrow\cdots\rightarrow\mathsf{S}_{n}$ still contains marriages, apply the procedure described above inductively.

∎

6.2 Preservation Properties

Given $\rho\rightarrow\pi$, one can define a relation $\mathcal{R}^{\rho}_{\pi}$ and prove it having certain bisimulation properties, as described in Section 5. The relations are actually useful here, too; in this section, we show various properties on a reduction and transition sequences using the relations $\mathcal{R}^{\rho}_{\pi}$. By definition, the relations $\mathcal{R}^{\rho}_{\pi}$ are all defined as set of pairs $(\mathsf{S}_{\rho},\mathsf{S}_{\pi})$, where marriage tokens in $\mathsf{S}_{\rho}$ have a natural counterpart in $\mathsf{S}_{\pi}$, and vice versa. The fact that $\mathcal{R}^{\rho}_{\pi}$ are weak bisimulation relations implies that if $(\mathsf{S}_{\rho},\mathsf{S}_{\pi})\in\mathcal{R}^{\rho}_{\pi}$ and $\Theta$ is a transition sequence starting in $\mathsf{S}_{\rho}$ and ending in $\mathsf{U}_{\rho}$, then there are some naturally defined sequences starting in $\mathsf{S}_{\pi}$ and ending in $\mathsf{U}_{\pi}$ such that $(\mathsf{U}_{\rho},\mathsf{U}_{\pi})\in\mathcal{R}^{\rho}_{\pi}$. In this case we say that $\mathcal{R}^{\rho}_{\pi}$ sends $\Theta$ to any of those transition sequences or, simply, that $\Theta$ is sent to any of them. Conversely if $\Xi$ is a transition sequence starting in $\mathsf{S}_{\pi}$ and ending in $\mathsf{U}_{\pi}$, then there are some naturally defined sequences starting from $\mathsf{S}_{\rho}$ and ending in $\mathsf{U}_{\rho}$ such that $(\mathsf{U}_{\rho},\mathsf{U}_{\pi})\in\mathcal{R}^{\rho}_{\pi}$. In this case we say that $\mathcal{R}^{\rho}_{\pi}$ sends back any of these sequences to $\Theta$ or, simply, that any of these sequences is sent back to $\Theta$. All this can be easily generalised to infinite transition sequences. If a transition sequence $\Theta$ in a collection $\mathit{RED}$ is sent (sent back, respectively) to a transition $\Xi$, not much can be said, in general, about whether $\Xi\in\mathit{RED}$. If, however, for every $\Theta\in\mathit{RED}$, there is $\Xi\in\mathit{RED}$ such that $\Theta$ is sent (sent back, respectively) to $\Xi$, we say that $\mathit{RED}$ (or the predicate on transition sequences defining $\mathit{RED}$) is preserved forward (preserved backward, respectively).

Lemma 10**.**

Infinite focused sequences starting in reachable states are preserved forward and backward.

Proof.

Suppose that $\rho\rightarrow\pi$. Then, $\rho$ can be seen as a redex $\theta$ in parallel to the rest of the net $\xi$, while $\pi$ can be seen as a reduct $\upsilon$ in parallel to $\xi$, graphically:

The redex $\theta$ can be any pair of cells facing each other, together with wires linking some of the auxiliary ports of the two cells, if this is the way they are linked in $\rho$. Now, consider an infinite focused sequence $\Theta$ in $\rho$. We can have two cases:

• •

$\Theta$ goes back and forth between $\theta$ and $\xi$ infinitely often. In this case, it is easy to realise that $\Theta$ is sent to an infinite focused sequence in $\pi$. Indeed, each of the infinitely many finite portions of it in $\theta$ (respectively, $\xi$) is mapped to a finite corresponding portion in $\upsilon$ (respectively, $\xi$). Moreover, each of the finite portions of $\Theta$ in $\xi$ is non-empty (because if it is empty, the corresponding wire would be part of $\theta$) and is sent to itself.

• •

$\Theta$ goes back and forth between $\theta$ and $\xi$ only finitely often. In this case, there needs to be an infinite suffix $\Xi$ of $\Theta$ which lies in one of the two components, which however must be $\xi$, because no infinite focused sequence starting in a reachable state can be constructed for a redex. As a consequence, $\Theta$ is sent forward to an infinite focused sequence in $\pi$, because $\Xi$ is also a transition sequence of $\pi$.

A similar argument can be given for every infinite focused sequence $\Theta$ in $\pi$. ∎

Lemma 11**.**

Thunks are preserved forward and backward.

Proof.

The first thing to observe here is that the left projection of $\mathcal{R}^{\rho}_{\pi}$ only includes states in which the marriage corresponding to the redex leading $\rho$ to $\pi$ has already been performed. Once we realise this, showing that thunks are preserved forward and backward amounts to the following observations:

• •

First of all, $\mathcal{R}^{\rho}_{\pi}$ puts origin tokens in correspondence with origin tokens, and states for which marriages are ready to states with the same property.

• •

Second of all, focused sequences are sent (and sent back) to focused sequences.

This concludes the proof. ∎

Lemma 12**.**

Continuations starting in a reachable state are preserved backward and forward.

Lemma 13**.**

Infinite continuations starting in a reachable state are preserved backward and forward.

Proof.

We can first of all observe that continuations are preserved backward and forward. Now, suppose by way of contradiction, that an infinite continuation $\Theta$ is sent to a finite continuation $\Xi$. Since in any continuation, marriages are not allowed to happen, it means that $\Theta$ (respectively, $\Xi$) can be seen as the interleaving of a finite number of focused reductions $\Theta_{1},\ldots,\Theta_{n}$ (respectively, $\Xi_{1},\ldots,\Xi_{n}$) such that $\Theta_{i}$ is mapped to $\Xi_{i}$. Now, at least one of the $\Theta_{i}$, say $\Theta_{j}$ must be infinite, otherwise $\Theta$ would be finite itself. By Lemma 10, $\Xi_{j}$ is thus infinite, and as a consequence the whole of $\Xi$ is infinite. ∎

Proposition 4**.**

Suppose that $\rho\rightarrow_{a}\pi$ where $a\in\{\delta\delta,\gamma\delta\}$. If $\mathsf{TM}_{\pi}$ has a finite standard computation with $n$ thunks then $\mathsf{TM}_{\rho}$ has a finite standard computation with $n+1$ thunks.

Proof.

By Lemma 7 and Lemma 8, there is $t_{\rho}$ such that $s_{\rho}\rightarrow t_{\rho}$ and $(t_{\rho},s_{\pi})\in\mathcal{R}^{\rho}_{\pi}$. Since thunks and continuations are preserved backward, the thesis easily follows. ∎

Proposition 5**.**

Suppose that $\rho\rightarrow_{\gamma\gamma}\pi$. If $\mathsf{TM}_{\pi}$ has a standard computation with $n$ thunks, then $\mathsf{TM}_{\rho}$ also has one.

Proof.

By Lemma 6, it holds that $\mathsf{TM}_{\rho}\approx\mathsf{TM}_{\pi}$. Since thunks and continuations are preserved backward, the thesis easily follows. ∎

Proposition 6**.**

If $\mathsf{TM}_{\rho}$ has a finite standard computation which is a continuation, then $\rho\rightarrow^{*}\pi$, where $\pi$ is in normal form and $\pi\notin\mathbf{VC}$.

Proof.

Consider the net $\pi$ obtained by reducing all $\gamma\gamma$ redexes in $\rho$, in an arbitrary order. This process of course terminates, because each reduction step makes the number of wires in the net to decrease. Now:

• •

$\pi$ is in normal form. If it contains a $\delta\delta$ or $\delta\gamma$ redex, indeed, $\mathsf{TM}_{\pi}$ would admit a standard computation with at least one thunk. Since thunks are preserved backward, one would get the same for $\mathsf{TM}_{\rho}$. This is however incompatible with $\mathsf{TM}_{\rho}$ having a finite standard computation which is a continuation.

• •

$\pi$ does not contain any $\gamma$-vicious circle. If it contains one, indeed, $\mathsf{TM}_{\pi}$ would admit an infinite standard computation which is a continuation, and then also $\mathsf{TM}_{\rho}$ would admit one. This is again incompatible with $\mathsf{TM}_{\rho}$ having a finite standard computation which is a continuation.

This concludes the proof. ∎

Proposition 7**.**

If $\mathsf{TM}_{\rho}$ has a standard computation with $n+1$ thunks and a continuation $\Theta$ (respectively, with infinitely many thunks), then $\rho\rightarrow^{+}\pi$, where $\mathsf{TM}_{\pi}$ has a standard computation with $n$ thunks and a continuation $\Xi$ (respectively, with infinitely many thunks). Moreover $\Theta$ is infinite iff $\Xi$ is.

Proof.

First of all, let us consider the net $\theta$ one obtains by reducing all $\gamma\gamma$ redexes in $\rho$, in an arbitrary order. This process of course terminates, because each reduction step makes the number of wires in the net to decrease. The net $\theta$ has itself a standard computation with $n+1$ thunks and a continuation (respectively, it has infinitely many thunks). Since $\theta$ only contains $\delta\delta$ or $\delta\gamma$ redexes, the first thunk in the standard computation corresponds to one of redex of one of those kinds. As a consequence there is $\pi$ such that $\theta\rightarrow\pi$. Moreover, by Lemma 7 and Lemma 8, $\pi$ admits a standard computation $\Xi$ with $n$ thunks and a continuation (respectively, with infinitely many thunks), which is infinite iff $\Theta$ is. ∎

Proposition 8**.**

Let $\rho$ be a net in normal form. If $\rho\notin\mathbf{VC}$, then $\mathsf{TM}_{\rho}$ only admits finite computations. Otherwise, all maximal computation of $\mathsf{TM}_{\rho}$ are infinite.

Proof.

Assume $\rho\notin\mathbf{VC}$. In this situation, a marriage token cannot hit any principal port, since it means there remains a redex (and thus there will be no marriage). Thus a marriage token can only hit auxiliary ports one by one; if it hits an auxiliary port of a $\delta_{2}$ cell, it stops. Moreover there is no way to make it able to move on, since no marriage can take place. Therefore the only possibility for a token to travel infinitely is to go through $\gamma$ cells infinitely many times, each time from an auxiliary port to the principal port. However, since $\rho$ is finite, this means the token is trapped into a loop consisting of $\gamma$ cells, which means there is a $\gamma$-vicious circle, which in turn contradicts to $\rho\notin\mathbf{VC}$. Hence a marriage token can perform transitions only finitely many times. Considering that the number of marriage tokens is also finite and it does not increase, all computations of $\mathsf{TM}_{\rho}$ are finite.

Assume $\rho\in\mathbf{VC}$. Recall it means $\rho$ contains a subnet in the following form:

Since $\nu$ contains one or more $\delta_{2}$ cells, they emit marriage tokens and at least one of them reaches $\sigma$ since $\nu$ is a tree. It reaches one of the leaves of $\tau$ since $\sigma$ is just a wiring. Finally, the token necessarily reaches the root of $\tau$ and is feeded back to $\sigma$, since $\tau$ consists only of $\gamma$ cells; this continues forever. By the same reason as the case of $\rho\notin\mathbf{VC}$, there will not be any marriage, hence the infinite trip described above cannot end by being killed. ∎

Proposition 9**.**

If $\mathsf{TM}_{\rho}$ has an infinite standard computation which is a continuation, then there exists $\pi$ satisfying $\rho\rightarrow^{*}\pi$ solely by $\gamma\gamma$ reductions and $\pi\in\mathbf{VC}$.

Proof.

First, we reduce $\gamma\gamma$ redexes as much as possible, obtaining $\rho\rightarrow^{*}\pi$. By Lem. 13, $\mathsf{TM}_{\pi}$ also has an infinite standard computation which is a continuation, say $\Theta$. Since $\Theta$ is a continuation, by definition it does not contain any marriage transition. Thus the number of marriage tokens is finitely bounded, implying there exists at least one token that moves infinitely many times. Let us follow the token’s infinite path. The token starts from a principal port of a $\delta_{2}$ cell with an empty configuration. then it cannot hit

• •

a principal port (of any kind of cells) since then a marriage happens.

• •

an auxiliary port of a $\delta_{2}$ cell, since $\Theta$ does not contain a marriage and thus it stops.

So it must hit an auxiliary port of a $\gamma$ cell and goes out from its principal port, now with a non-empty configuration. After passing a $\gamma$ cell, it cannot hit

• •

a principal port of a $\delta_{2}$ cell or an $\varepsilon$ cell since it stops due to $\gamma$ stack being not empty.

• •

a principal port of $\gamma$ cell since then $\pi$ has a $\gamma\gamma$ redex.

• •

an auxiliary port of a $\delta_{2}$ cell, because $\Theta$ does not contain a marriage and thus it stops.

So again it must hit an auxiliary port of a $\gamma$ cell and goes out from its principal port with a non-empty configuration. Since $\pi$ is finite, the net $\pi$ necessarily has a loop consisting only of $\gamma$ cells connected with a tree containing a $\delta_{2}$ cell, i.e. a $\gamma$-vicious circle. ∎

6.3 The Four Implications

Lemma 14**.**

$\mathit{inf}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)\Longrightarrow\mathit{inf}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})$**

Proof.

If $\mathit{inf}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)$, then we can distinguish two cases:

• •

Either $\rho$ admits an infinite reduction sequence. In this case, we prove that $\mathit{inf}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})$ by coinduction. Indeed, if $\rho$ admits an infinite reduction sequence, then there is a finite reduction

[TABLE]

where $a\in\{\delta\gamma,\delta\delta\}$ and $\mathit{inf}_{\mathsf{NETS}}^{\mathbf{VC}}(\theta)$. We know, by soundness, that $\mathsf{TM}_{\rho}\approx\mathsf{TM}_{\pi}$ and that $s_{\pi}$ reduces in at least one step to a state $t$ which is bisimilar to $s_{\theta}$. We can then conclude by coinduction that since $\mathit{inf}_{\mathsf{TM}_{\theta}}^{\emptyset}(s_{\mathsf{TM}_{\theta}})$, it holds that $\mathit{inf}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})$.

• •

Or $\rho$ admits a finite reduction sequence to a net $\pi$ in $\mathbf{VC}$. The net $\pi$ contains a $\gamma$-vicious circle, and then $\mathit{inf}_{\mathsf{TM}_{\pi}}^{\emptyset}(s_{\mathsf{TM}_{\pi}})$ holds. By induction on the number of reduction steps leading $\rho$ to $\pi$, one can then prove that $\mathit{inf}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})$.

This concludes the proof. ∎

Lemma 15**.**

$\mathit{fin}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)\Longrightarrow\mathit{fin}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})$**

Proof.

If $\mathit{fin}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)$, then $\rho$ reduces in $n$ steps to a normal net not in $\mathbf{VC}$. One can prove, that, for any such net $\rho$, $\mathsf{TM}_{\rho}$ admits a finite computation:

• •

First of all, if $\rho$ is itself a normal form not in $\mathbf{VC}$, then $\rho$ admits a finite (standard) computation, due to Proposition 8.

• •

If $\rho\rightarrow\pi$ and $\mathsf{TM}_{\pi}$ admits a finite standard computation, then $\mathsf{TM}_{\rho}$ itself admits a finite standard computation, due to Proposition 4 and Proposition 5.

∎

Lemma 16**.**

$\mathit{inf}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})\Longrightarrow\mathit{inf}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)$**

Proof.

If there is an infinite computation from $s_{\mathsf{TM}_{\rho}}$, then:

• •

Either there is an infinite standard computation with a finite number $n$ of thunks and an infinite continuation from $s_{\mathsf{TM}_{\rho}}$. Then, by induction on $n$, one can prove that $\rho$ reduces to another net $\pi$ such that $\mathsf{TM}_{\pi}$ has an infinite standard reduction which is a continuation. By Proposition 9, this implies the thesis.

• •

Or there is an infinite standard computation with infinitely many thunks from $s_{\mathsf{TM}_{\rho}}$. Then, we can apply Proposition 7 in a coinductive way to get an infinite reduction from $\rho$.

∎

Lemma 17**.**

$\mathit{fin}_{\mathsf{TM}_{\rho}}^{\emptyset}(s_{\mathsf{TM}_{\rho}})\Longrightarrow\mathit{fin}_{\mathsf{NETS}}^{\mathbf{VC}}(\rho)$**

Proof.

If there is a finite computation from $s_{\mathsf{TM}_{\rho}}$, then there is also a finite standard computation with $n$ thunks from $s_{\mathsf{TM}_{\rho}}$. We can then proceed by induction on $n$, thanks to Proposition 6 and Proposition 7. If $n=0$ then $\rho$ is in normal form not in $\mathbf{VC}$ by Proposition 6; if $n>0$ then there exists $\pi$ satisfying $\rho\rightarrow^{*}\pi$ and $\mathsf{TM}_{\pi}$ admits a finite standard computation with $n-1$ thunks by Proposition 7. ∎

7 Discussion

A formal comparison between multi-token machines and other concurrent models of computation, and in particular the so-called truly concurrent ones, is outside the scope of this paper. Some observations in this direction are anyway useful, and are the starting point of current investigations by the authors.

Multi-token machines as we defined them in this paper can be seen as Petri nets where, however, the set of places and transitions are both denumerable. In particular, places correspond to the possible states of a token, of which there can be countably many: remember that marriage tokens carry two stacks of unbounded length with them. Indeed, tokens lying at the same wire, but with different stacks need to correspond to different places at the level of Petri nets, because they can travel in completely different directions. Implementing the marriage mechanism in Petri nets is indeed possible, but requires nonlocal transitions, transitions with incoming arcs coming from places which are “far away” from each other: actually, there must be one such transition for any pair of (virtual copies of) $\delta_{2}$ principal ports in the underlying net. In other words, the nonlocal behaviour of certain multi-token machine interactions would be reflected, at the level of Petri nets, by a possibly very complex and nonlocal system of transitions. Apart from that, the encoding seems possible, and indeed targets plain Petri nets rather than the kind of Petri nets that are usually required to model process algebras like the $\pi$-calculus, e.g., Petri nets with inhibitor arcs [7]. Whether a finitary $\pi$-calculus can be given a plain Petri net semantics this way is an interesting open problem.

Perhaps even more direct is the correspondence between multi-token machines and chemical abstract machines as defined by, e.g., Berry and Boudol [6]. In this view, tokens would become molecules, and would be allowed to float in a soup, freely interacting between them. Marriage transitions of multi-token machines would be modelled by chemical rules allowing two matching molecules (i.e. marriage tokens) to interact, producing some other tokens. Moving transitions, on the other hand, are most often possible in presence of a status token, and this mechanism itself can be seen as a chemical reaction (which leave one of the two involved ingredients essentially unchanged). In this view, the underlying net’s wires would become molecule kinds, and the obtained abstract machine would be syntax-free.

8 Conclusions

In this paper, we introduced the first truly concurrent geometry of interaction model, by defining multi-token machines for Mazza’s multiport interaction combinators, and by proving them to be sound and adequate. Mazza himself suggested this as an open problem [33]. What is interesting about our results is also the way they are spelled out and proved, namely by way of labelled transition systems and (bi)similarity. This is something quite natural, but new to geometry of interaction models, at least to the authors’ knowledge.

As already mentioned, one topic for future work is a study of multi-token machines for differential interaction nets, and in particular to a “multiport” variation of them, something the authors are actually working on as a way towards a better modelling of the $\pi$-calculus. Another topic of future work concerns the study of the concurrent nature of multi-token machines, and in particular of their causal structure, especially in view of their interpretation as Petri nets.

Acknowledgment

The first author is partially supported by the ANR projects 12IS02001 PACE, and 14CE250005 ELICA. The third author is partially supported by the JST ERATO Grant Number JPMJER1603. The three authors are supported by the INRIA-JSPS joint project CRECOGI.

Appendix

In this section, we will give some more details as for why all the results we proved in this paper can be generalised to MIC where $\varepsilon$ cells are allowed to interact with other cells (including themselves).

Interaction Rules.

First of all, we need some additional interaction rules, namely those in Figure 14. Please notice that this new sets of rules taken in isolation turns MICs into a confluent and strongly normalizing rewrite system. Actually, the first of the three new rules implies that we cannot work with $\delta_{2}$ cells only, but also with $\delta_{1}$ cells.

Token Machines.

As for token machines, we need to substantially generalise the ones we introduced in the paper. First of all, cell types need to be generalised. Moreover, more reduction rules are needed, because $\delta$ cells can now marry not only with $\delta$ or $\gamma$ cells, but also with $\varepsilon$ cells. They are in Figure 15, Figure 16, and Figure 17. The proof of the compositionality remains essentially unaltered, except for the fact that more cases need to be taken into account.

Soundness.

The proof of soundness needs to be adapted. In particular, we need to prove lemmas analogous to Lemma 6, Lemma 7 and Lemma 8, but for interaction rules involving $\varepsilon$ cells. Here they are:

Lemma 18**.**

If $\rho\rightarrow_{\gamma\varepsilon}\pi$, then $\mathsf{TM}_{\rho}\approx\mathsf{TM}_{\pi}$.

Lemma 19**.**

If $\rho\rightarrow_{\varepsilon\varepsilon}\pi$, then $\mathsf{TM}_{\rho}\approx\mathsf{TM}_{\pi}$.

Lemma 20**.**

If $\rho\rightarrow_{\delta\varepsilon}\pi$, then there is $t_{\rho}$ such that $s_{\rho}\rightarrow t_{\rho}$ and $(\mathbb{FM}(\mathcal{TKS}^{\rho}),\rightarrow,t_{\rho})\approx\mathsf{TM}_{\pi}$.

Proof.

We are in the following situation:

Let $t_{\rho}$ be a state which is obtained by performing a $\delta\varepsilon$ marriage in $s_{\rho}$. Then we define a bisimulation relation in the same way as Lemma 8. ∎

Adequacy.

Finally, also the adequacy proof needs to be adapted, but only as for some of the technical lemmas, the overall structure of the proof remaining essentially unaltered. In particular, whenever we repeatedly apply $\gamma\gamma$ in the proofs, we instead apply the rules $\{\gamma\gamma,\gamma\varepsilon,\varepsilon\varepsilon\}$. This set of rules is also confluent and terminating, because the number of cells (in particular $\gamma$ cells) is decreasing.