A Hypergraph Model for Communication Patterns

Abstract

The article deals with interaction in concurrent systems. A calculus able to express specific communication patterns is defined, together with its abstract control structures. A hypergraph model for these structures is presented. The hypergraphs are able to properly express the communication patterns, providing a fully abstract model for the pattern calculus. It is also proved that the hypergraph model preserves the operational reductions of processes from pattern calculus and of the actions from the control structures.

1. Introduction

Mathematics has sometimes been called a ‘science of patterns’ [1], meaning that patterns are at the heart of mathematics. The nice description of mathematics as the “study of patterns” was given by G.H. Hardy in his book A Mathematician’s Apology: “A mathematician, like a painter or a poet, is a maker of patterns. If his patterns are more permanent than theirs, it is because they are made with ideas”. Essentially, patterns are regularities that we can perceive. Regarding the skilful ability of applying a pattern to multiple contexts, Solomon Marcus was a wonderful example of applying knowledge patterns to surprising contexts.

Since mathematics and technology have developed a fruitful relationship over past few decades, patterns have been investigated recently in modern fields. New communication technologies have changed the computing landscape, and the Internet is now a platform for large scale distributed programming. Nowadays, we deal with global computation based on multiple interactions with the environment (instead of isolated systems). Concurrency is essential now in computer science; web servers handle multiple simultaneous clients, and cloud servers allow several simultaneous applications and users. Message-passing represents a way in which concurrent processes communicate (a process is an instance of a running program). In software architecture, a messaging pattern describes how two different processes communicate with each other. In telecommunications, a message exchange pattern describes the messages required by a communications protocol or the message flow between parties involved in communication. For example, when navigating on Internet (representing the channel), a web browser (the communicating party) uses the communication protocol HTTP to request a web page from the server (another communicating party). In general, the interaction between clients and servers follows a specific communication pattern: the client sends a request, the server returns a response, and so on. Such an exchange of messages is only an example of communication patterns. More complicated behaviours appear due to the concurrent interaction of communicating processes; this complexity reveal the necessity to find new ways to describe and build up concurrent systems. The communicating parties in such a concurrent system should have a common language to communicate; moreover, they should follow the rules defined in a communications protocol. There exits already a calculus able to express communication patterns called join calculus; it is used as a basis for some programming languages (JoCaml and Cω), but also as a basis for libraries (embedded in C#, F# and Scala). This calculus is based on ‘join patterns’, namely rules describing how a certain combination of values sent through multiple channels triggers a specific reaction and removes the values from the communication channels. Interaction in such a calculus is provided by sharing the communication channels names.

We introduce the pattern calculus as a weak version of join calculus. After presenting the control structures for pattern calculus, we provide a hypergraph model of these structures. The hypergraphs are able to express properly the communication patterns described by the pattern calculus. It is proved that the hypergraph model is fully abstract for the calculus; a model is fully abstract if all observationally equivalent processes represent the same object in the model, meaning also that processes with different behaviour are not mapped to the same hypergraph. Furthermore, there is a correspondence between the dynamics of the processes of the calculus and their hypergraph representation.

2. Pattern Calculus

The pattern calculus is inspired by the join calculus [2], a calculus proposed to underlie programming languages for distributed systems. A presentation of the join calculus can also be found in [3]. The specific construction of the new calculus is the definition of communication channels: $\mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q$. To elucidate the simplicity of this syntactical construction, let us say that it could be expressed in the $\pi$-calculus [4] by using several syntactical constructions: $\mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q=\nu u.(!u(y).P\mid Q)$.

The syntax of the pattern calculus is defined by using a countable set $\mathcal{X}$ of names ranging over $u,v,x,\dots$, together with $\tilde{u},\tilde{v},\tilde{x},\tilde{y}\dots$ ranging over finite strings of names. We use $P,Q,R,\dots$ ranging over the set of processes. The set $\mathcal{P}$ of processes contains an empty process 0, as well as an output message $u\langle v\rangle$ sending v by using a channel u. The process $P\mid Q$ describes the parallel composition of processes P and Q. The communication between processes is achieved by the channel definition $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q$ indicating that the interaction of processes P and Q is realized by the channel u (which is created only for the communication between them).

Definition 1.

The processes of our calculus are defined by the following syntax:

P ::=   $0\mid u\langle v\rangle \mid P\mid Q\mid \mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q$.

In   $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q$, both u and v are bound. The scope of v is P, while the scope of u is given by the whole definition. It is worth noting that only this definition binds names. The free names are defined inductively by $\mathtt{fn}\left(0\right)=\varnothing ,\mathtt{fn}(u\langle v\rangle )=\{u,v\},\mathtt{fn}(P\mid Q)=\mathtt{fn}\left(P\right)\cup \mathtt{fn}\left(Q\right)$, and $\mathtt{fn}(\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q)=\left(\mathtt{fn}\right(Q)\cup (\mathtt{fn}\left(P\right)-\left\{v\right\}\left)\right)-\left\{u\right\}$.

A substitution $\{y/x\}P$ replaces all the free occurrences of name x in P by name y; name-capture is avoided by using the $\alpha$-conversion (defined in the standard way).

Definition 2.

A structural congruence $\equiv \subseteq \mathcal{P}\times \mathcal{P}$ is defined as the smallest congruence satisfying the following axioms:

• $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\equiv \mathtt{def}u\langle t\rangle ▹\{t/v\}P\mathtt{in}Q$, if $t\notin \mathtt{fn}\left(P\right)$
• $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\equiv \mathtt{def}w\langle v\rangle ▹\{w/u\}P\mathtt{in}\{w/u\}Q$ if $v\notin \{u,w\}$ and $w\notin \mathtt{fn}(P\mid Q)$
• $Q_1\mid \mathtt{def}u\langle v\rangle ▹P\mathtt{in}{Q}_2\equiv \mathtt{def}u\langle v\rangle ▹P\mathtt{in}(Q_1\mid Q_2)$ if $u\notin \mathtt{fn}\left(Q_1\right)$
• $\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}\mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}Q\equiv \mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}Q$
        if $u\ne w$, $u\notin \mathtt{fn}\left(P_2\right)$, and $w\notin \mathtt{fn}\left(P_1\right)$
• $P\mid 0\equiv P$       $P\mid Q\equiv Q\mid P$       $(P\mid Q)\mid R\equiv P\mid (Q\mid R)$.

The evolution of the processes is given by a reduction relation → .

For the specific construct $\mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q$, the reduction is described mainly by:

$\mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q\mid u\langle v\rangle \to \mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q\mid \{v/y\}P$.

More exactly, process Q can send a name v along the channel u, while process P waits at the other end of channel u to receive certain channel names. When the name v is received, process Q continues its execution in parallel with process P in which all free occurrences of y are replaced by v, i.e., $\{v/y\}P$. Then, channel u remains open to receive other names. The formal definition is given below.

Definition 3.

The reduction relation $\to \subseteq \mathcal{P}\times \mathcal{P}$ is defined as the smallest relation satisfying:

r1:

$\mathtt{def}{u}_1\langle v_1\rangle ▹Q_1\mathtt{in}\mathtt{def}{u}_2\langle v_2\rangle ▹Q_2\mathtt{in}\dots \mathtt{def}{u}_n\langle v_n\rangle ▹Q_n\mathtt{in}(P\mid u_i\langle v\rangle )\to$

$\mathtt{def}{u}_1\langle v_1\rangle ▹Q_1\mathtt{in}\mathtt{def}{u}_2\langle v_2\rangle ▹Q_2\mathtt{in}\dots \mathtt{def}{u}_n\langle v_n\rangle ▹Q_n\mathtt{in}(P\mid \{v/v_i\}{Q}_i)$

      if $\{u_{i+1},\dots ,u_n\}\cap (\mathtt{fn}\left(Q_i\right)\cup \left\{u_i\right\})=\varnothing$ with $i\in \left[n\right]$ and $n\ge 1$  

r2:

            ${\displaystyle \frac{P_1\to P_2}{\mathtt{def}u\langle v\rangle ▹Q\mathtt{in}{P}_1\to \mathtt{def}u\langle v\rangle ▹Q\mathtt{in}{P}_2}}$  

r3:

                  ${\displaystyle \frac{P_1\equiv Q_1,Q_1\to Q_2\mathrm{and}{Q}_2\equiv P_2}{P_1\to P_2}}$.

It is worth noting that there is no rule for parallel composition in the definition of this reduction. The following (easy-to-prove) results show that such a rule for parallel composition is just a consequence.

Lemma 1.

Considering any substitution $\sigma =\{x/y\}$,

$P\equiv Q$ implies $\sigma P\equiv \sigma Q$, and $P_1\to P_2$ implies $\sigma P_1\to \sigma P_2$.

Proposition 1.

   $P_1\to P_2$ implies $Q\mid P_1\to Q\mid P_2$.

3. Hypergraphs

In the theory of distributed systems, Petri nets [5] and $\pi$-nets [6] provide both algebraic and graphical descriptions for concurrent systems. Compared to Petri nets, our hypergraph model for pattern calculus has a flexible structure; compared to $\pi$-nets, the hypergraph model is simpler, but still able to describe a large class of processes.

Following [7], we present the definitions for hypergraphs and some standard related notions such as isomorphism and contractions (on nodes and on edges). For a set S of hyperedges and a set V of vertices, it is defined an incidence relation $E\subseteq S\times V$. A rooted hypergraph is a tuple $H=\langle S,V,E,s\rangle$, where $s\in S$ is the root hyperedge. For a hypergraph H, we use the notations $S_H$, $V_H$, $E_H$ and $s_H$.

The graphical presentation of a hypergraph H is provided by:

-

A hyperedge t represented as an oval with its name t outside.

-

A vertex v represented as a point having the name v .

-

An element $(t,v)$ of the incidence relation represented as lines from the hyperedge t to the vertex v; “v lies on t” whenever $(t,v)\in E_H$.

-

The root indicated by an arrow pointing to the hyperedge $s_H$.

Example 1.

Considering a hypergraph with $S_H=\{s,t,t^{\prime }\}$, $V_H=\{v,w,w^{\prime }\}$, $E_H=\{(s,v),$$(t,v),(t,w),(t^{\prime },v),(t^{\prime },w^{\prime })\}$ and $s_H=\left\{t\right\}$, various graphical representations are depicted in Figure 1. The left representation uses only lines of non-zero length, while the right one uses only lines of zero length. The representation in the middle is a compromise (between lengths) to provide a reasonable picture.

For a given rooted hypergraph H and a nonempty subset $W\subseteq V_H$ of nodes, a contraction on vertices is specified by the hypergraph $H/W$ with the same root hyperedge ($s_{H/W}=s_H$), the same hyperedges ($S_{H/W}=S_H$), but with $V_{H/W}=(V_H\backslash W)\cup \left\{v\right\}$ for a fresh $v\notin V_H$ and $E_{H/W}=(E_H\backslash S_H\times W)\cup \left\{(t,v)\right|\left\{t\right\}\times W\cap E_H\ne \varnothing \}$.

For a given rooted hypergraph H and a nonempty subset $T\subseteq S_H$ of hyperedges, a contraction on hyperedges is specified by the hypergraph $H/T$ with the same set of vertices ($V_{H/T}=V_H$), but with $S_{H/T}=(S_H\backslash T)\cup \left\{t\right\}$ for a fresh $t\notin S_H$, and $E_{H/T}=(E_H\backslash T\times V_H)\cup \left\{(t,v)\right|T\times \left\{v\right\}\cap E_H\ne \varnothing \}$. Regarding the root hyperedge $s_{H/T}$, if $s_H\in T$ then $s_{H/T}=t$, otherwise it remains the same $s_H$.

Example 2.

Considering two vertices $v,w\in V_H$, we denote by $H_{v=w}$ the contraction on vertices in $H/\{v,w\}$. For two hyperedges $s,t\in S_H$, we denote by $H_{s=t}$ the contraction on hyperedges in $H/\{s,t\}$. For the hypergraph H used in the previous example, the contraction on vertices $H_{w=w^{\prime }}$ and the contraction on hyperedges $H_{t=t^{\prime }}$ are depicted in Figure 2.

The isomorphism between two hypergraphs H and $H^{\prime }$ is defined by two bijections ${\varphi }_S:S_H\to S_{H^{\prime }}$ and ${\varphi }_V:V_H\to V_{H^{\prime }}$ which satisfy ${\varphi }_S\left(s_H\right)=s_{H^{\prime }}$ and $(s,v)\in E_H$ if and only if $({\varphi }_S\left(s\right),{\varphi }_V\left(v\right))\in E_{H^{\prime }}$ for all $s\in S_H$ and $v\in V_H$. In such a situation, we say that hypergraphs H and $H^{\prime }$ are isomorphic (denoted by $H=H^{\prime }$).

The isomorphism relation is an equivalence over hypergraphs. The names of hyperedges and vertices do not play any role in the isomorphism of hypergraphs. For the graphical representation of an equivalence class, it can be used any hypergraph (after removing the names of hyperedges and vertices).

4. Control Structure for Pattern Calculus

Milner proposed the control structures and action calculi as a unifying framework for the models of concurrent systems in [8]. A control structure defines the static aspects of a process calculus, while the corresponding action calculus describes various models of interactive behaviours. Regarding the behaviour, distinct action calculi differ only in their generators (called controls). Thus, the previously mentioned Petri nets and $\pi$-nets, as well as our hypergraph model, differ only in their generators. Analyzing these generators, it is possible to compare and classify the formal models for concurrent systems. Moreover, by selecting some specific generators, it is possible to combine existing models in order to obtain a new desired model.

The control structures presented here follow the definitions of [9]. Essentially, a control structure is defined by a set of terms, an equational theory, and a reduction relation over terms. This fact is condensed in the following expression:

$$ControlStructure=Actions+EquationalTheory+Reaction.$$

From an algebraic viewpoint, a control structure is a symmetric strict monoidal category with an additional structure [10]. The morphisms of the symmetric strict monoidal category correspond to the terms of the control structure; they are denoted by $a,b,c,\dots$ and called actions.

The control structure uses an enumerable set $\mathcal{X}$ of names together with a signature $(P,\mathcal{K})$ in which P is a set of prime arities and $\mathcal{K}$ is a set of control operators. Every name $x\in \mathcal{X}$ has a prime arity $p\in P$, and this is denoted by $x:p$. Each control $K\in \mathcal{K}$ has an arity rule. In addition to the specific control operators, every control structure contains a datum operator $\langle x\rangle :ϵ\to p$ (where $x:p$) and a discard operator ${\omega }_p:p\to ϵ$, as well as an abstractor operator ${\mathtt{ab}}_{x}a:p\otimes m\to p\otimes n$ (where $x:p$ and $a:m\to n$). The equational theory is the same for all control structures. To express the evolution, a set R of reaction rules is used; reaction rules are ordered pairs of terms with the same arity.

Each action a possesses a surface $\mathtt{surf}\left(a\right)=\{x\in X|\exists p.x:p\mathrm{and}{\mathtt{ab}}_{x}a\ne {\mathtt{id}}_p\otimes a\}$.

The equality = between actions is valid whenever the equation $a=b$ could be proved by using the axioms of the control structure; otherwise $a\ne b$.

We present here some results used later in the proofs of our results.

Proposition 2.

The following properties hold in any control structure:

$$\mathtt{surf}(\langle x\rangle )\subseteq \left\{x\right\}\mathtt{surf}\left(\omega \right)=\varnothing \mathtt{surf}(a\otimes b)\subseteq \mathtt{surf}\left(a\right)\cup \mathtt{surf}\left(b\right).$$

The following properties hold in any control structure, whenever $x\notin \mathtt{surf}\left(c\right)$:

$$\mathtt{surf}\left(\mathtt{id}\right)=\varnothing \mathtt{surf}\left(\mathtt{p}\right)=\varnothing \mathtt{surf}(a·b)\subseteq \mathtt{surf}\left(a\right)\cup \mathtt{surf}\left(b\right).$$

Additionally,

1.	${\mathtt{p}}_{n,ϵ}={\mathtt{id}}_n$
2.	$a\otimes b=b\otimes a$	$(a,b:ϵ\to ϵ)$
3.	$\left(x\right)(c·b)=({\mathtt{id}}_p\otimes c)·\left(x\right)b$	$(x:p)$
4.	$\left(x\right)(c\otimes b)=c\otimes \left(x\right)b$	$(c:ϵ\to n)$
5.	$\left(x\right)(a\otimes c)=\left(x\right)a\otimes c$
6.	$\left(z\right)\left(y\right)a=({\mathtt{p}}_{p,q}\otimes {\mathtt{id}}_m)·\left(y\right)\left(z\right)a$	$(z:p,y:q,a:m\to n)$

Proposition 3.

The following properties are provable in any control structure:

1.	$[x/y](a·b)=[x/y]a·[x/y]b$;
2.	$[x/y](a\otimes b)=[x/y]a\otimes [x/y]b$;
3.	$[x/y]\left(z\right)a=\left(z\right)[x/y]a$	if$z\notin \{x,y\}$;
4.	$[x/y]\left(x\right)a=\left(w\right)[x/y][w/x]a$	if$w\notin \mathtt{surf}\left(a\right)\cup \{x,y\}$ and $x\ne y$.

We define the control structure for our pattern calculus, emphasizing on its actions. We also present a graphical representation for its processes. The monoid $(\mathbb{N},+,0)$ of the natural numbers provides the arity monoid of the control structure, with $m,n,k,\dots$ ranging over natural numbers, and $\left[n\right]=\{1,2,\dots ,n\}$ denoting the first n natural numbers. The (unique) prime arity 1 is associated with each name $x\in \mathcal{X}$. For a number k and a function $f:\left[n\right]\to Y$, we define $k\oplus f:\{k+1,\dots k+n\}\to Y$ by $(k\oplus f)\left(i\right)=f(i-k)$. Following [9], the control structure is defined over the set $\mathcal{X}=\left\{z_i\right|i\in \mathbb{N}\}$ of names using $x,y,u,\dots$ as meta-variables.

Regarding the actions of the control structure for our calculus, they are given by enriched hypergraphs called shortly pattern nets. An action $a=(H,\Sigma )$ with arity $m\to n$ is given by a hypergraph H together with its decoration $\Sigma =\langle \mathtt{I},\mathtt{O},\lambda ,\tau ,\mu \rangle$ consisting of:

-

An input function given by an injective function $\mathtt{I}:\left[m\right]\to V_H$;

-

An output function given by a function $\mathtt{O}:\left[n\right]\to V_H$;

-

A label function given by an injective function $\lambda :Z\to V_H$, where $Z\subseteq \mathcal{X}$;

-

A transition relation $\tau \subseteq V_H\times V_H$;

-

A resource function $\mu :S_H\to {\mathbb{N}}^{V_H\times V_H}$.

We can look at these functions as multisets over $S_H\times V_H\times V_H$. We denote by $\{x,y,y\}$ a multiset $\mu$ over $\{x,y,z\}$ such that $\mu \left(x\right)=1$, $\mu \left(y\right)=2$ and $\mu \left(z\right)=0$; we use the standard multiset operations over these functions: ($\uplus ,-,\dots$).

We extend in a straightforward way the isomorphism and contraction introduced for hypergraphs. Considering $a_i=(H_i,{\Sigma }_i)$ with ${\Sigma }_i=\langle {\mathtt{I}}_i,{\mathtt{O}}_i,{\lambda }_i,{\tau }_i,{\mu }_i\rangle$ ($i\in \left[2\right]$), the nets $a_1$ and $a_2$ are isomorphic if there is a hypergraph isomorphism $({\varphi }_S,{\varphi }_V)$ between $H_1$ and $H_2$ such that ${\varphi }_V\circ {\mathtt{I}}_1={\mathtt{I}}_2$, ${\varphi }_V\circ {\mathtt{O}}_1={\mathtt{O}}_2$, ${\varphi }_V\circ {\lambda }_1={\lambda }_2$, and $(v,v^{\prime })\in {\tau }_1$ if and only if $({\varphi }_V\left(v\right),{\varphi }_V\left(v^{\prime }\right))\in {\tau }_2$, together with ${\mu }_1(s,v,v^{\prime })={\mu }_2({\varphi }_S\left(s\right),{\varphi }_V\left(v\right),{\varphi }_V\left(v^{\prime }\right))$ for all $s\in S_{H_1}$ and $v,v^{\prime }\in V_{H_1}$.

For the graphical representations of the pattern nets, let us consider a generic net $a=(H,\Sigma )$ with $\Sigma =\langle \mathtt{I},\mathtt{O},\lambda ,\tau ,\mu \rangle$; the hypergraph H is presented by assuming that its lines are of length zero (see Figure 1):

-

Whenever $\mathtt{I}\left(i\right)=v$, $\mathtt{O}\left(k\right)=v^{\prime }$ and $\lambda \left(x\right)=w$, an input label $\left(i\right)$ is assigned to vertex v, an output label $\langle k\rangle$ to vertex $v^{\prime }$, and a name labelx to vertex w;

-

Whenever $(v,v^{\prime })\in \tau$, an arc is drawn outside any oval from vertex v to vertex $v^{\prime }$;

-

Whenever $\mu (s,v,v^{\prime })>0$, v and $v^{\prime }$ lie on the same hyperedge s: $(s,v),(s,v^{\prime })\in E_H$; more exactly, whenever $\mu (s,v,v^{\prime })=k>0$, we have k arcs inside the oval s from vertex v to vertex $v^{\prime }$.

As for hypergraphs, isomorphic nets are not distinguished. The names of vertices and hyperedges do not play any role in the isomorphic nets, and so the graphical representation of an isomorphic (equivalence) class of pattern nets is given by any net of the class after removing the names of vertices and hyperedges.

The control structure operators for our pattern nets are:

- datum ${\langle x\rangle }^{\gamma }=(H,\Sigma ):0\to 1$ defined by
$H=\langle \left\{s\right\},\left\{v\right\},\left\{\right(s,v\left)\right\},s\rangle$ and $\Sigma =\langle \varnothing ,\{1\mapsto v\},\{x\mapsto v\},\varnothing ,\varnothing \rangle$
- discard ${\omega }^{\gamma }=(H,\Sigma ):1\to 0$ defined by
$H=\langle \left\{s\right\},\left\{v\right\},\left\{\right(s,v\left)\right\},s\rangle$ and $\Sigma =\langle \{1\mapsto v\},\varnothing ,\varnothing ,\varnothing ,\varnothing \rangle$

The three controls generating the pattern nets are:

– ${\nu }^{\gamma }=(H,\Sigma ):0\to 1$ defined by
$H=\langle \left\{s\right\},\left\{v\right\},\left\{\right(s,v\left)\right\},s\rangle$ and $\Sigma =\langle \varnothing ,\{1\mapsto v\},\varnothing ,\varnothing ,\varnothing \rangle$
– ${\mathtt{out}}^{\gamma }=(H,\Sigma ):2\to 0$ defined by
$H=\langle \left\{s\right\},\{v,v^{\prime }\},\{(s,v),(s,v^{\prime })\},s\rangle$ and $\Sigma =\langle \varnothing ,\{1\mapsto v,2\mapsto v^{\prime }\},\varnothing ,\varnothing ,\left\{(s,v^{\prime },v)\right\}\rangle$
– If $a=(H,\Sigma ):1\to 0$ and $\Sigma =\langle \mathtt{I},\mathtt{O},\lambda ,\tau ,\mu \rangle$, then
${\mathtt{def}}_{}^{\gamma }a=(H^{\prime },{\Sigma }^{\prime }):1\to 0$, where
$H^{\prime }=\langle S_H\cup \left\{t\right\},V_H\cup \left\{v\right\},E_H\cup \left\{(t,v)\right\},t\rangle$, for fresh
$t\notin S_H$ and $v\notin V_H$, and
${\Sigma }^{\prime }=\langle \{1\mapsto v\},\mathtt{O},\lambda ,\tau \cup \left\{(v,\mathtt{I}\left(1\right))\right\},\mu \rangle$.

The equational theory is defined by the following operators.

Let us consider the nets $a_i=(H_i,{\Sigma }_i)$ with ${\Sigma }_i=\langle {\mathtt{I}}_i,{\mathtt{O}}_i,{\lambda }_i,{\tau }_i,{\mu }_i\rangle$ and ${\lambda }_i:Z_i\to V_{H_i}$, where $i\in \left[2\right]$. Without loss of generality, we consider $s_{H_1}=s_{H_2}=s$. $(S_{H_1}-\left\{s_{H_1}\right\})\cap (S_{H_2}-\left\{s_{H_2}\right\})=\varnothing$ and ${\lambda }_1\left(z\right)={\lambda }_2\left(z\right)$$\forall z\in Z_1\cap Z_2$, as well as $(V_{H_1}-{\lambda }_1(Z_1\cap Z_2))\cap (V_{H_2}-{\lambda }_2(Z_1\cap Z_2))=\varnothing$.

– Identity ${\mathtt{id}}_m^{\gamma }=(H,\Sigma ):m\to m$ defined by
$H=\langle \left\{s\right\},\left\{v_i\right|i\in \left[m\right]\},\left\{(s,v_i)\right|i\in \left[m\right]\},s\rangle$ and $\Sigma =\langle \{i\mapsto v_i|i\in \left[m\right]\},\{i\mapsto v_i|i\in \left[m\right]\},\varnothing ,\varnothing ,\varnothing \rangle$
– Symmetry ${\mathtt{p}}_{m,n}^{\gamma }=(H,\Sigma ):m+n\to n+m$ defined by
$H=\langle \left\{s\right\},\left\{v_i\right|i\in [m+n]\},\left\{(s,v_i)\right|i\in [m+n]\},s\rangle$ $$\begin{gathered} \Sigma =\langle \{i\mapsto v_i|i\in [m+n]\},\{i\mapsto v_{m+i}|i\in \left[n\right]\}\cup \\ \{n+i\mapsto v_i|i\in \left[m\right]\},\varnothing ,\varnothing ,\varnothing \rangle \end{gathered}$$

– Tensorial product $a_1\otimes a_2:m+k\to n+l$ of two nets $a_1:m\to n$ and $a_2:k\to l$ is obtained by combining them as follows: in $a_2$, the input labels are incremented by m and the output labels are incremented by n; then overlap the two roots and the vertices of $a_1$ and of $a_2$ with the same name. Formally, $a_1\otimes a_2=(H,\Sigma )$, where

$$H=\langle S_{H_1}\cup S_{H_2},V_{H_1}\cup V_{H_2},E_{H_1}\cup E_{H_2},s\rangle \mathrm{and}$$

$$\Sigma =\langle {\mathtt{I}}_1\cup m\oplus {\mathtt{I}}_2,{\mathtt{O}}_1\cup n\oplus {\mathtt{O}}_2,{\lambda }_1\cup {\lambda }_2,{\tau }_1\cup {\tau }_2,{\mu }_1\uplus {\mu }_2\rangle .$$

– Composition $a_1·a_2:m\to k$ of two nets $a_1:m\to n$ and $a_2:n\to k$ is obtained by combining them as follows: overlap the two roots and vertices of $a_1$ and $a_2$ with the same name; for every $i\in \left[n\right]$, overlap the vertex labelled $\langle i\rangle$ in $a_1$ with the vertex labelled $\left(i\right)$ in $a_2$, and then remove the labels $\left(i\right)$ and $\langle i\rangle$.

Formally, $a_1·a_2={(H,\Sigma )}_{{\mathtt{O}}_1\left(1\right)={\mathtt{I}}_2\left(1\right),\dots ,{\mathtt{O}}_1\left(n\right)={\mathtt{I}}_2\left(n\right)}$, where

$$H=\langle S_{H_1}\cup S_{H_2},V_{H_1}\cup V_{H_2},E_{H_1}\cup E_{H_2},s\rangle \mathrm{and}$$

$$\Sigma =\langle {\mathtt{I}}_1,{\mathtt{O}}_2,{\lambda }_1\cup {\lambda }_2,{\tau }_1\cup {\tau }_2,{\mu }_1\uplus {\mu }_2\rangle .$$

– Abstractor. Let us consider a net $a=(H,\Sigma ):m\to n$ with $\Sigma =\langle \mathtt{I},\mathtt{O},\lambda ,\tau ,\mu \rangle$.

Then ${\mathtt{ab}}_x^{\gamma }a:1+m\to 1+n$ is obtained from a in the following steps: increment all the input and output labels by 1; assign both the input label $\left(1\right)$ and the output label $\langle 1\rangle$ to vertex x, and then remove the label x. Formally, ${\mathtt{ab}}_x^{\gamma }a=(H,{\Sigma }^{\prime })$, where

$${\Sigma }^{\prime }=\langle \{1\mapsto \lambda \left(x\right)\}\cup 1\oplus \mathtt{I},\{1\mapsto \lambda \left(x\right)\}\cup 1\oplus \mathtt{O},\lambda -\{x\mapsto \lambda \left(x\right)\},\tau ,\mu \rangle .$$

In general, these operators over the pattern nets are well-defined. However, the abstractor ${\mathtt{ab}}_x^{\gamma }a$ is not well-defined if a vertex labelled by x is not contained in the net a. To avoid such a situation, we adjust the definition of the above operators by

$$\mathtt{op}(a,\dots )\stackrel{def}{=}{\mathtt{op}}^{\gamma }(a{\otimes }^{\gamma }\mathbf{i},\dots ){\otimes }^{\gamma }\mathbf{i},$$

where op stands for each operator defined above, and $\mathbf{i}=(H,\Sigma )$ is the pattern net

$$H=\langle \left\{s\right\},\left\{v_i\right|i\in \mathbb{N}\},\left\{(s,v_i)\right|i\in \mathbb{N}\},s\rangle$$

$$\Sigma =\langle \varnothing ,\varnothing ,\{z_i\mapsto v_i|i\in \mathbb{N}\},\varnothing ,\varnothing \rangle .$$

Following [9], it is not difficult to prove the following result.

Proposition 4.

The operators $\langle x\rangle$, ω, ν, $\mathtt{out}$, $\mathtt{def}$, $\mathtt{id}$, $\mathtt{p}$, ·, ⊗ and ${\mathtt{ab}}_x$ define a control structure.

The actions of this control structure determine the hypergraph model for the pattern calculus. We actually use the derived control operators:

$$\begin{array}{ccc}\hfill {\mathtt{out}}_u& \stackrel{def}{=}& (\langle u\rangle \otimes {\mathtt{id}}_1)·\mathtt{out};\hfill \\ \hfill {\mathtt{def}}_{u}a& \stackrel{def}{=}& \langle u\rangle ·{\mathtt{def}}_{}a.\hfill \end{array}$$

The reaction ↘ is the smallest relation over the pattern nets closed under equality, composition, tensorial product and abstraction which satisfies the control rule

$${\mathtt{out}}_u\otimes {\mathtt{def}}_{u}a\searrow a\otimes {\mathtt{def}}_{u}a.$$

The corresponding graphical description of the reaction rule is given by:

In this diagram, the scope of the $\mathtt{def}$ operator is represented as a gray patch; due to the properties derived from the syntax of our calculus, this patch can actually be determined from the hypergraph structure.

The operators, actions and reaction complete the definition of our nets.

It is worth noting that the def operator can be generalized, namely we can have a more general control operator ${\mathtt{def}}_{u_1\dots u_m}$ by ${\mathtt{def}}_{u_1\dots u_m}a=(\langle u_1\rangle \otimes \dots \otimes \langle u_m\rangle )·{\mathtt{def}}_{}a$. Moreover, the corresponding graphical representation is extended by using m external arcs to connect the new root hyperedge to the old one. The corresponding reaction is generalized in the following way: ${\mathtt{out}}_{u_1}\otimes \dots \otimes {\mathtt{out}}_{u_m}\otimes {\mathtt{def}}_{u_1\dots u_m}a\searrow a\otimes {\mathtt{def}}_{u_1\dots u_m}a.$

We present some proprieties of the pattern nets. The proofs of these properties are tedious (but easy), based mainly on definitions and the structure of the nets.

Lemma 2.

We have the following properties:

1.

$\mathtt{surf}\left({\mathtt{out}}_u\right)\subseteq \left\{u\right\}$ and $\mathtt{surf}\left({\mathtt{def}}_{u}a\right)\subseteq \left\{u\right\}\cup \mathtt{surf}\left(a\right)$.

2.

For any substitution $\sigma =\{x/y\}$, $[x/y]{\mathtt{out}}_u={\mathtt{out}}_{\sigma u}$ and $[x/y]{\mathtt{def}}_{u}a={\mathtt{def}}_{\sigma u}[x/y]a$.

3.

If $a\searrow b$, then there exists $b^{\prime }$ such that $b=b^{\prime }$ and $\mathtt{surf}\left(b^{\prime }\right)\subseteq \mathtt{surf}\left(a\right)$.

4.

$\langle v\rangle ·{\mathtt{out}}_w\otimes {\mathtt{def}}_u\left(y\right)a\searrow b$ iff $u=w$ and $b=[v/y]a\otimes {\mathtt{def}}_u\left(y\right)a$.

5.

$a_1\otimes a_2\otimes a_3\searrow c$    iff    

• either there exists $i\in \left[3\right]$ such that $a_i\searrow b$ and $c=b\otimes a_j\otimes a_k$, or
• there exist $i,j\in \left[3\right]$ such that $a_i\otimes a_j\searrow b$ and $c=b\otimes a_k$, where $\left[3\right]=\{i,j,k\}$.

6.

Whenever $u\notin \mathtt{surf}\left(b\right)$, $b\otimes {\mathtt{def}}_{u}a\searrow c$    iff    $b\searrow b^{\prime }$ and $c=b^{\prime }\otimes {\mathtt{def}}_{u}a$.

7.

$\nu ·\left(x\right)a\searrow b$    iff    $a\searrow a^{\prime }$ and $b=\nu ·\left(x\right)a^{\prime }$.

5. Fully Abstract Hypergraph Model of the Pattern Calculus

This section presents the main results of the paper. These results reveal the hypergraphs as a fully abstract model for the pattern calculus. According to [11], a model is fully abstract if all observationally equivalent terms in the object language represent the same object in the model. This means that processes with different behaviour are not mapped to the same hypergraph. Moreover, we prove a correspondence between the reduction of the processes and the reduction of their hypergraph representation.

Definition 4.

The semantic relationship $\left[\right[-\left]\right]$ between the pattern calculus processes and the pattern nets is defined by structural induction as follows:

1.

$\left[\right[0\left]\right]={\mathtt{id}}_0$;

2.

$\left[\right[u\langle v\rangle \left]\right]=\langle v\rangle ·{\mathtt{out}}_u$;

3.

$\left[\right[P\mid Q\left]\right]=\left[\right[P\left]\right]\otimes \left[\right[Q\left]\right]$;

4.

$\left[\right[\mathtt{def}u\langle y\rangle ▹P\mathtt{in}Q\left]\right]=\nu ·\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[P\left]\right])$.

We prove some results involving this semantic relationship $\left[\right[-\left]\right]$.

Lemma 3.

For every process $P\in \mathcal{P}$, we have $\left[\right[P\left]\right]:0\to 0$.

Proof. 

A simple induction on the structure of P. In the case of our nets, 0 is the neutral element of the arity monoid $(\mathbb{N},+,0)$. For case $\left(4\right)$ of the previous definition, we use the discard operator $\omega$ instead of ${\omega }_p$. Since 1 is the only prime arity p of the monoid $(\mathbb{N},+,0)$, we omit the index without any risk of confusion.    □

Lemma 4.

For every process $P\in \mathcal{P}$, we have $\mathtt{surf}\left(\left[\right[P\left]\right]\right)\subseteq \mathtt{fn}\left(P\right)$.

Proof. 

By induction on the structure of P (the proof uses Lemma 2).    □

Lemma 5.

For two names $x,y\in X$ and a process $P\in \mathcal{P}$, we have $\left[\right[\{x/y\}P\left]\right]=[x/y]\left[\right[P\left]\right]$.

Proof. 

Induction on the definition of the substitution over processes (and Lemma 5).    □

Proposition 5.

If $P\equiv Q$, then $\left[\right[P\left]\right]=\left[\right[Q\left]\right]$.

Proof. 

Induction on the definition of structural congruence. Let us consider the relation

$$\sim =\left\{\right(P,Q)\in \mathcal{P}\mid P\equiv Q\mathrm{and}\left[\right[P\left]\right]=\left[\right[Q\left]\right]\}.$$

Proof is reduced to the equality between ∼ and ≡. Obviously, $\sim \subseteq \equiv$. We show that ∼ satisfies the axioms from the definition of ≡. Since ≡ is the smallest relation satisfying these axioms, it follows that $\equiv \subseteq \sim$, and so $\sim =\equiv$. Thus, to prove that $\equiv \subseteq \sim$, it is enough to verify that ∼ satisfies the axioms from the definition of ≡.

The cases $P\mid 0\equiv P$, $P\mid Q\equiv Q\mid P$ and $(P\mid Q)\mid R\equiv P\mid (Q\mid R)$ are rather trivial, based on the fact that ${\mathtt{id}}_0$ is neutral for tensor product, together with the commutativity and associativity of tensor product ⊗ in the equational theory (of the control structures).

Let us consider the other cases.

– $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\equiv \mathtt{def}u\langle t\rangle ▹\{t/v\}P\mathtt{in}Q$, if $t\notin \mathtt{fn}\left(P\right)$.

Assume $t\notin \mathtt{fn}\left(P\right)$. By Lemma 4, it follows that $t\notin \mathtt{surf}\left(\left[\right[P\left]\right]\right)$. Then,

$\left[\right[\mathtt{def}u\langle t\rangle ▹\{t/v\}P\mathtt{in}Q\left]\right]=$

$\begin{array}{cccc}& =& \nu ·\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(t\right)\left[\right[\{t/v\}P\left]\right])\hfill & \mathrm{by} \mathrm{Lemma} 5\hfill \\ & =& \nu ·\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(t\right)[t/v]\left[\right[P\left]\right])\hfill & \\ & =& \left[\right[\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\left]\right].\hfill & \end{array}$

– $\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\equiv \mathtt{def}w\langle v\rangle ▹\{w/u\}P\mathtt{in}\{w/u\}Q$ if $v\notin \{u,w\}$, $w\notin \mathtt{fn}(P\mid Q)$.

Assume $v\notin \{u,w\}$ and $w\notin \mathtt{fn}(P\mid Q)$; then, $u\ne v$ and $w\notin \mathtt{fn}\left(P\right)\cup \mathtt{fn}\left(Q\right)\cup \left\{v\right\}$. By Lemma 4, $w\notin \mathtt{surf}\left(\left[\right[P\left]\right]\right)\cup \mathtt{surf}\left(\left[\right[Q\left]\right]\right)$. If $u=w$, then the result is trivial.

Let us assume that $u\ne w$.

$\left[\right[\mathtt{def}w\langle v\rangle ▹\{w/u\}P\mathtt{in}\{w/u\}Q\left]\right]=$

$\begin{array}{cccc}& =& \nu ·\left(w\right)(\left[\right[\{w/u\}Q\left]\right]\otimes {\mathtt{def}}_w\left(v\right)\left[\right[\{w/u\}P\left]\right])\hfill & \mathrm{by} \mathrm{Lemma} 5\hfill \\ & =& \nu ·\left(w\right)([w/u]\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(v\right)[w/u]\left[\right[P\left]\right])\hfill & \mathrm{by} \mathrm{Proposition} 3 \mathrm{and}\mathrm{Lemma} 2\hfill \\ & =& \nu ·\left(w\right)[w/u](\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P\left]\right])\hfill & \mathrm{by} \mathrm{Lemma} 2\hfill \\ & =& \left[\right[\mathtt{def}u\langle v\rangle ▹P\mathtt{in}Q\left]\right].\hfill & \end{array}$

– $Q_1\mid \mathtt{def}u\langle v\rangle ▹P\mathtt{in}{Q}_2\equiv \mathtt{def}u\langle v\rangle ▹P\mathtt{in}(Q_1\mid Q_2)$ if $u\notin \mathtt{fn}\left(Q_1\right)$.

Assume $u\notin \mathtt{fn}\left(Q_1\right)$. By Lemma 4, $u\notin \mathtt{surf}\left(\left[\right[Q_1\left]\right]\right)$. Then,

$\left[\right[\mathtt{def}u\langle v\rangle ▹P\mathtt{in}(Q_1\mid Q_2)\left]\right]=$

$\begin{array}{cccc}& =& \nu ·\left(u\right)(\left[\right[Q_1\left]\right]\otimes \left[\right[Q_2\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P\left]\right])\hfill & \mathrm{by} \mathrm{Lemma} 3 \mathrm{and} \mathrm{Proposition} 2\hfill \\ & =& \left[\right[Q_1\mid \mathtt{def}u\langle v\rangle ▹P\mathtt{in}{Q}_2\left]\right].\hfill & \end{array}$

– $\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}\mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}Q\equiv \mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}Q$

      if $u\ne w$, $u\notin \mathtt{fn}\left(P_2\right)$, and $w\notin \mathtt{fn}\left(P_1\right)$.

Assume $u\ne w$, $u\notin \mathtt{fn}\left(P_2\right)$ and $w\notin \mathtt{fn}\left(P_1\right)$. By Lemma 4, it follows that $u\notin \mathtt{surf}\left(\left[\right[P_2\left]\right]\right)$ and $w\notin \mathtt{surf}\left(\left[\right[P_1\left]\right]\right)$. Furthermore, by Lemma 2, $w\notin \mathtt{surf}({\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right]$.

$\left[\right[\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}\mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}Q\left]\right]=$

$\begin{array}{cccc}& =& \nu ·\left(u\right)(\nu ·\left(w\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right])\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right])\hfill & \mathrm{by} \mathrm{Proposition} 2\hfill \\ & =& \nu ·\left(u\right)(\nu ·\left(w\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right]))\hfill & \mathrm{by} \mathrm{Proposition} 2\hfill \\ & =& (\nu \otimes \nu )·\left(u\right)\left(w\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right])\hfill & =\mathbf{X}.\hfill \end{array}$

In a similar way, we obtain $\left[\right[\mathtt{def}w\langle t\rangle ▹P_2\mathtt{in}\mathtt{def}u\langle v\rangle ▹P_1\mathtt{in}Q\left]\right]=$

$\begin{array}{cccc}& =& (\nu \otimes \nu )·\left(w\right)\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right])\hfill & =\mathbf{Y}.\hfill \end{array}$

To complete the proof, it remains to prove that X = Y.

$\mathbf{X}=\mathrm{by} \mathrm{Proposition} 2$      

$\begin{array}{cccc}& =& (\nu \otimes \nu )·{\mathtt{p}}_{1,1}·\left(w\right)\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right])\hfill & \\ & =& {\mathtt{p}}_{0,0}·(\nu \otimes \nu )·\left(w\right)\left(u\right)(\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[P_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_2\left]\right])\hfill & \\ & =& \mathbf{Y}.\hfill & \end{array}$    □

Theorem 1.

If $P\to Q$, then $\left[\right[P\left]\right]\searrow \left[\right[Q\left]\right]$.

Proof. 

By induction on the definition of $P\to Q$.

* r1: $P\to Q$ is

$$\mathtt{def}{u}_1\langle y_1\rangle ▹Q_1\mathtt{in}\mathtt{def}{u}_2\langle y_2\rangle ▹Q_2\mathtt{in}\dots \mathtt{def}{u}_n\langle y_n\rangle ▹Q_n\mathtt{in}R\mid u_i\langle v\rangle \to$$

$$\mathtt{def}{u}_1\langle y_1\rangle ▹Q_1\mathtt{in}\mathtt{def}{u}_2\langle y_2\rangle ▹Q_2\mathtt{in}\dots \mathtt{def}{u}_n\langle y_n\rangle ▹Q_n\mathtt{in}R\mid \{v/y_i\}{Q}_i,\mathrm{where}$$

$\{u_{i+1},\dots ,u_n\}\cap (\mathtt{fn}\left(Q_i\right)\cup \left\{u_i\right\})=\varnothing$, $i\in \left[n\right]$, and $n\ge 1$. According to Lemma 2 and Lemma 4, $\{u_{i+1},\dots ,u_n\}\cap \mathtt{surf}\left({\mathtt{def}}_{u_i}\left(y_i\right)\left[\right[Q_i\left]\right]\right)=\varnothing$. According to Proposition 2 and using the compatibility of ↘ with composition, tensorial product and abstraction,

$\left[\right[P\left]\right]=\nu ·\left(u_1\right)({\mathtt{def}}_{u_1}\left(y_1\right)\left[\right[Q_1\left]\right]\otimes$

$\begin{array}{cc}=& ⋮\hfill \\ & \nu ·\left(u_i\right)({\mathtt{def}}_{u_i}\left(y_i\right)\left[\right[Q_i\left]\right]\otimes \hfill \\ & ⋮\hfill \\ & \nu ·\left(u_n\right)({\mathtt{def}}_{u_n}\left(y_n\right)\left[\right[Q_n\left]\right]\otimes \left[\right[R\left]\right]\otimes \langle v\rangle ·{\mathtt{out}}_{u_i})\dots )\dots )\hfill \end{array}$

$\begin{array}{cc}=& \nu ·\left(u_1\right)({\mathtt{def}}_{u_1}\left(y_1\right)\left[\right[Q_1\left]\right]\otimes \mathrm{by} \mathrm{Lemma} 2\hfill \\ & ⋮\hfill \\ & \nu ·\left(u_{i-1}\right)({\mathtt{def}}_{u_{i-1}}\left(y_{i-1}\right)\left[\right[Q_{i-1}\left]\right]\otimes \hfill \\ & \nu ·\left(u_i\right)(\hfill \\ & \nu ·\left(u_{i+1}\right)({\mathtt{def}}_{u_{i+1}}\left(y_{i+1}\right)\left[\right[Q_{i+1}\left]\right]\otimes \hfill \\ & ⋮\hfill \\ & \nu ·\left(u_n\right)({\mathtt{def}}_{u_n}\left(y_n\right)\left[\right[Q_n\left]\right]\otimes \left[\right[R\left]\right]\otimes \langle v\rangle ·{\mathtt{out}}_{u_i}\otimes {\mathtt{def}}_{u_i}\left(y_i\right)\left[\right[Q_i\left]\right])...\left)\right))...)\hfill \end{array}$

$\begin{array}{cc}\searrow & \nu ·\left(u_1\right)({\mathtt{def}}_{u_1}\left(y_1\right)\left[\right[Q_1\left]\right]\otimes \mathrm{by} \mathrm{Lemma} 5\hfill \\ & ⋮\hfill \\ & \nu ·\left(u_i\right)({\mathtt{def}}_{u_i}\left(y_i\right)\left[\right[Q_i\left]\right]\otimes \hfill \\ & ⋮\hfill \\ & \nu ·\left(u_n\right)({\mathtt{def}}_{u_n}\left(y_n\right)\left[\right[Q_n\left]\right]\otimes \left[\right[R\left]\right]\otimes [v/y_i]\left[\right[Q_i\left]\right])\dots )\dots )\hfill \\ =& \left[\right[Q\left]\right].\hfill \end{array}$

* r2: $P\to Q$ is $\mathtt{def}u\langle v\rangle ▹R\mathtt{in}{P}^{\prime }\to \mathtt{def}u\langle v\rangle ▹R\mathtt{in}{Q}^{\prime }$ with $P^{\prime }\to Q^{\prime }$.

By induction, $\left[\right[P^{\prime }\left]\right]\searrow \left[\right[Q^{\prime }\left]\right]$. Since ↘ is closed under composition, tensor and abstraction, it follows that

$$\left[\right[P\left]\right]=\nu ·\left(u\right)(\left[\right[P^{\prime }\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[R\left]\right])\searrow \nu ·\left(u\right)(\left[\right[Q^{\prime }\left]\right]\otimes {\mathtt{def}}_u\left(v\right)\left[\right[R\left]\right])=\left[\right[Q\left]\right].$$

* r3: $P\to Q$ with $P\equiv P^{\prime }$, $P^{\prime }\to Q^{\prime }$ and $Q^{\prime }\equiv Q$.

By the induction hypothesis, $\left[\right[P^{\prime }\left]\right]\searrow \left[\right[Q^{\prime }\left]\right]$. By Proposition 5, we have $\left[\right[P\left]\right]=\left[\right[P^{\prime }\left]\right]$ and $\left[\right[Q^{\prime }\left]\right]=\left[\right[Q\left]\right]$. Since ↘ is closed under equality, then $\left[\right[P\left]\right]\searrow \left[\right[Q\left]\right]$.    □

Lemma 6.

$\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P\left]\right]\searrow a$    iff    $\left[\right[P\left]\right]\searrow b$ and $a=\langle v\rangle ·{\mathtt{out}}_u\otimes b$.

Proof. 

$(\Leftarrow )$ A consequence of the fact that the reaction is closed under tensorial product and equality.

$(\Rightarrow )$ Induction on the structure of P.

–

If P is the empty process or a message, then $\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P\left]\right]⤰$. Therefore, the statement of the lemma is obviously true because its premise is not satisfied.

–

If P is a parallel composition $P_1\mid P_2$, then $\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P_1\left]\right]\otimes \left[\right[P_2\left]\right]\searrow a$. Since $\langle v\rangle ·{\mathtt{out}}_u⤰$, it follows (Lemma 2) that one of the following cases remains possible:

(1)

$\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }\otimes \left[\right[P_j\left]\right]$;

(2)

$\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]\searrow b^{\prime }$ and $a=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }$;

(3)

$\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P_i\left]\right]\searrow a^{\prime }$ and $a=a^{\prime }\otimes \left[\right[P_j\left]\right]$, where $\{i,j\}=\left[2\right]$.

Note that by Proposition 2, we have $\left[\right[P\left]\right]=\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]$.

In case $\left(1\right)$, $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$, and we consider $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$. In case $\left(2\right)$, we take $b=b^{\prime }$. In case $\left(3\right)$, by induction, we have $\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a^{\prime }=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }$. Thus, $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$, considering $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$.

–

If P is a definition $\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{P}_2$, then we may assume without losing generality that $w\notin \{u,v\}$. It follows from Lemma 2 together with Proposition 2 that $\nu ·\left(w\right)(\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])\searrow a$. By Lemma 2, $\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow a^{\prime }$ and $a=\nu ·\left(w\right)a^{\prime }$. Since $\langle v\rangle ·{\mathtt{out}}_u⤰$, ${\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]⤰$ and $\langle v\rangle ·{\mathtt{out}}_u\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]⤰$, it follows (according to Lemma 2) that one of the following cases remains possible:

(1)

$\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{\prime }=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$;

(2)

$\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow b^{\prime }$ and $a^{\prime }=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }$;

(3)

$\langle v\rangle ·{\mathtt{out}}_u\otimes \left[\right[P_2\left]\right]\searrow a^{″}$ and $a^{\prime }=a^{″}\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$.

  In case $\left(1\right)$, $\left[\right[P\left]\right]=\nu ·\left(w\right)(\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])\searrow \nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$. Considering $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$, it satisfies the requirements (according to Proposition 2). In case $\left(2\right)$, we have $\left[\right[P\left]\right]\searrow \nu ·\left(w\right)b^{\prime }$, and consider $b=\nu ·\left(w\right)b^{\prime }$. In case $\left(3\right)$, by induction hypothesis, $\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{″}=\langle v\rangle ·{\mathtt{out}}_u\otimes b^{\prime }$. Thus, $\left[\right[P\left]\right]\searrow \nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$, and consider $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$.    □

Lemma 7.

$\left[\right[P\left]\right]\otimes \left[\right[Q\left]\right]\searrow a$    iff    one of the following conditions holds:

1.

$\left[\right[P\left]\right]\searrow b$ and $a=b\otimes \left[\right[Q\left]\right]$;

2.

$\left[\right[Q\left]\right]\searrow b$ and $a=\left[\right[P\left]\right]\otimes b$.

Proof. 

$(\Leftarrow )$ A consequence of the fact that the reaction is closed under tensorial product and equality.

$(\Rightarrow )$ Induction on the structure of P.

–

If P is the empty process 0, then condition 2 holds obviously.

–

If P is a message, then condition 2 holds by Lemma 6.

–

If P is a parallel composition $P_1\mid P_2$, then $\left[\right[P_1\left]\right]\otimes \left[\right[P_2\left]\right]\otimes \left[\right[Q\left]\right]\searrow a$.

By Lemma 2, it follows that one of the following cases is possible:

$\left(i\right)$

$\left[\right[Q\left]\right]\searrow b^{\prime }$ and $a=\left[\right[P_1\left]\right]\otimes \left[\right[P_2\left]\right]\otimes b^{\prime }$;

$\left(ii\right)$

$\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a=b^{\prime }\otimes \left[\right[P_j\left]\right]\otimes \left[\right[Q\left]\right]$;

$\left(iii\right)$

$\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]\searrow b^{\prime }$ and $a=b^{\prime }\otimes \left[\right[Q\left]\right]$;

$\left(iv\right)$

$\left[\right[P_i\left]\right]\otimes \left[\right[Q\left]\right]\searrow a^{\prime }$ and $a=a^{\prime }\otimes \left[\right[P_j\left]\right]$, where $\{i,j\}=\left[2\right]$.

According to Proposition 2, $\left[\right[P\left]\right]=\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]$. In case $\left(i\right)$, condition 2 holds by taking $b=b^{\prime }$. In case $\left(ii\right)$, we have $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$. Then, condition 1 holds by taking $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$. In case $\left(iii\right)$, condition 1 holds by taking $b=b^{\prime }$.

In case $\left(iv\right)$, by induction, we distinguish two sub-cases:

$\left(a\right)$

$\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes \left[\right[Q\left]\right]$;

$\left(b\right)$

$\left[\right[Q\left]\right]\searrow b^{\prime }$ and $a^{\prime }=\left[\right[P_i\left]\right]\otimes b^{\prime }$.

For $\left(a\right)$, we obtain $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$, and condition 1 holds for $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$. For $\left(b\right)$, condition 2 holds for $b=b^{\prime }$. In both sub-cases, some action commutations are required; they are possible according to Proposition 2.

–

If P is a definition $\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{P}_2$, then we may assume without losing generality that $w\notin \mathtt{fn}\left(Q\right)$. By Lemma 4, $w\notin \mathtt{surf}\left(\left[\right[Q\left]\right]\right)$. According to Proposition 2, we have $\nu ·\left(w\right)(\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes \left[\right[Q\left]\right])\searrow a$. By Lemma 2, $\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes \left[\right[Q\left]\right]\searrow a^{\prime }$ and $a=\nu ·\left(w\right)a^{\prime }$. Since ${\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]⤰$, it follows from Lemma 2 that one of the following cases remains possible:

$\left(i\right)$

$\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes \left[\right[Q\left]\right]$;

$\left(ii\right)$

$\left[\right[Q\left]\right]\searrow b^{\prime }$ and $a^{\prime }=\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes b^{\prime }$;

$\left(iii\right)$

$\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes \left[\right[Q\left]\right]$;

$\left(iv\right)$

$\left[\right[P_2\left]\right]\otimes \left[\right[Q\left]\right]\searrow a^{″}$ and $a^{\prime }=a^{″}\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$.

In case $\left(i\right)$, condition 1 holds for $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$.

In case $\left(ii\right)$, by Lemma 2, there exists b such that $\mathtt{surf}\left(b\right)\subseteq \mathtt{surf}\left(\left[\right[Q\left]\right]\right)$ and $b=b^{\prime }$; condition 2 holds for this b. In case $\left(iii\right)$, condition 1 holds for $b=\nu ·\left(w\right)b^{\prime }$.

In case $\left(iv\right)$, we distinguish two sub-cases:

$\left(a\right)$

$\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{″}=b^{\prime }\otimes \left[\right[Q\left]\right]$;

$\left(b\right)$

$\left[\right[Q\left]\right]\searrow b^{\prime }$ and $a^{″}=\left[\right[P_2\left]\right]\otimes b^{\prime }$.

For $\left(a\right)$, condition 1 holds for $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$. For $\left(b\right)$, there exists b such that $\mathtt{surf}\left(b\right)\subseteq \mathtt{surf}\left(\left[\right[Q\left]\right]\right)$ and $b=b^{\prime }$ (by Lemma 2); condition 2 holds for this b. Proposition 2 is used in all cases and sub-cases.    □

Lemma 8.

$\left[\right[P\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a$    iff    one of the following conditions holds:

1.

$\left[\right[P\left]\right]\searrow b$ and $a=b\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

2.

$P\equiv R\mid u\langle v\rangle$ and $a=\left[\right[R\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

3.

$P\equiv \mathtt{def}{v}_1\langle t_1\rangle ▹R_1\mathtt{in}\mathtt{def}{v}_2\langle t_2\rangle ▹R_2\mathtt{in}...\mathtt{def}{v}_n\langle t_n\rangle ▹R_n\mathtt{in}(R\mid u\langle v_n\rangle )$, and

$\begin{array}{ccc}a\hfill & =& \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & \nu ·\left(v_2\right)({\mathtt{def}}_{v_2}\left(t_2\right)\left[\right[R_2\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\mid \{v_n/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])...\left)\right),\hfill \end{array}$

where $v_i\notin \mathtt{fn}\left(Q\right)\cup \left\{u\right\}$ for every $i\in \left[n\right]$.

Proof. 

$(\Leftarrow )$ If condition 1 holds, then the implication follows as a consequence of the fact that the reaction is closed under tensorial product and equality. If condition 2 holds, then we have

$\left[\right[P\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]=$                      by Proposition 5

$\begin{array}{ccc}=& \left[\right[R\left]\right]\otimes \langle v\rangle ·{\mathtt{out}}_u\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\hfill & \mathrm{by} \mathrm{Lemma} 2\hfill \\ \searrow & \left[\right[R\left]\right]\otimes [v/y]\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\hfill & \mathrm{by} \mathrm{Lemma} 5\hfill \\ =& a.\hfill \end{array}$

If condition 3 holds, it follows by Lemma 2 and Lemma 4 that $v_i\notin \mathtt{surf}\left({\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\right)$ for every $i\in \left[n\right]$. Then,

$\left[\right[P\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]=$                                   by Propositions 5 and 2

$\begin{array}{cc}=& \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \mathrm{by} \mathrm{Lemma} 2\hfill \\ & ⋮\hfill \\ & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\left]\right]\otimes \langle v_n\rangle ·{\mathtt{out}}_u\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots )\hfill \end{array}$

$\begin{array}{cc}\searrow & \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \mathrm{by} \mathrm{Lemma} 5\hfill \\ & ⋮\hfill \\ & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\left]\right]\otimes [v_n/y]\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots )\hfill \\ =& a.\hfill \end{array}$

$(\Rightarrow )$ Induction on the structure of P.

–  If P is the empty process 0 or a message $w\langle v\rangle$ with $w\ne u$, then $\left[\right[P\left]\right]\otimes {\mathtt{def}}_u$$\left(y\right)\left[\right[Q\left]\right]⤰$. The statement of the lemma is obviously true as its premise is not satisfied. On the other hand, if P is a message $u\langle v\rangle$, then

$\left[\right[P\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow$             by Lemma 2

$\begin{array}{ccc}\searrow & [v/y]\left[\right[Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a\hfill & \mathrm{by} \mathrm{Lemma} 5\hfill \\ =& 0\mid \{v/y\}Q\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right].\hfill \end{array}$

Furthermore, $P\equiv 0\mid u\langle v\rangle$. Consequently, condition 2 holds.

–  If P is a parallel composition $P_1\mid P_2$, then $\left[\right[P_1\left]\right]\otimes \left[\right[P_2\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a$. Since ${\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]⤰$, it follows from Lemma 2 that one of the following cases remains possible:

$\left(i\right)$

$\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a=b^{\prime }\otimes \left[\right[P_j\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$,

$\left(ii\right)$

$\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]\searrow b^{\prime }$ and $a=b^{\prime }\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$,

$\left(iii\right)$

$\left[\right[P_i\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a^{\prime }$ and $a=a^{\prime }\otimes \left[\right[P_j\left]\right]$, where $\{i,j\}=\left[2\right]$.

According to Proposition 2, we obtain $\left[\right[P\left]\right]=\left[\right[P_i\left]\right]\otimes \left[\right[P_j\left]\right]$. In case $\left(i\right)$, we obtain $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$, and condition 1 holds for $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$. In case $\left(ii\right)$, condition 1 holds for $b=b^{\prime }$. In case $\left(iii\right)$, we distinguish three sub-cases:

$\left(a\right)$

$\left[\right[P_i\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

$\left(b\right)$

$P_i\equiv R^{\prime }\mid u\langle v\rangle$ and $a^{\prime }=\left[\right[R^{\prime }\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

$\left(c\right)$

$P_i\equiv \mathtt{def}{v}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{v}_n\langle t_n\rangle ▹R_n\mathtt{in}(R^{\prime }\mid u\langle v_n\rangle )$ and

$\begin{array}{ccc}\hfill a^{\prime }& =& \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R^{\prime }\mid \{v_n/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots ),\hfill \end{array}$ where $v_k\notin \mathtt{fn}\left(Q\right)\cup \left\{u\right\}$ for every $k\in \left[n\right]$.

In sub-case $\left(a\right)$, we obtain $\left[\right[P\left]\right]\searrow b^{\prime }\otimes \left[\right[P_j\left]\right]$. Therefore, condition 1 holds for $b=b^{\prime }\otimes \left[\right[P_j\left]\right]$. For $\left(b\right)$, we have $P\equiv R^{\prime }\mid P_j\mid u\langle v\rangle$. By Proposition 2, $a=\left[\right[R^{\prime }\mid P_j\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$. Thus, condition 2 holds. For sub-case $\left(c\right)$, we may assume (without losing generality) that $v_k\notin \mathtt{fn}\left(P_j\right)$ for every $k\in \left[n\right]$. By Lemma 4, it follows that $v_k\notin \mathtt{surf}\left(\left[\right[P_j\left]\right]\right)$ for every $k\in \left[n\right]$. Then $P\equiv \mathtt{def}{v}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{v}_n\langle t_n\rangle ▹R_n\mathtt{in}(R^{\prime }\mid P_j\mid u\langle v_n\rangle )$, and

$a=$                                                    by Proposition 2

$\begin{array}{cc}\hfill =& \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & ⋮\hfill \\ & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R^{\prime }\mid P_j\mid \{v_n/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots ).\hfill \end{array}$

Thus, condition 3 holds.

–  If P is a definition $\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{P}_2$, then we can assume without losing generality that $w\notin \mathtt{fn}\left(Q\right)\cup \left\{u\right\}$. By Lemma 4 and Lemma 2, $w\notin \mathtt{surf}\left({\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\right)$. It follows from Proposition 2 that $\left[\right[P\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]=\nu ·\left(w\right)(\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$ $\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\searrow a$. By Lemma 2, $\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a^{\prime }$ and $a=\nu ·\left(w\right)a^{\prime }$. Since ${\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]⤰$ and ${\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]⤰$, then ${\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]⤰$ (according to Lemma 2). It follows that one of the following cases remains possible:

$\left(i\right)$

$\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

$\left(ii\right)$

$\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow b^{\prime }$ and $a^{\prime }=b^{\prime }\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$;

$\left(iii\right)$

$\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]\searrow a^{″}$ and $a^{\prime }=a^{″}\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$.

In case $\left(i\right)$, condition 1 holds for $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$. In case $\left(ii\right)$, condition 1 holds for $b=\nu ·\left(w\right)b^{\prime }$. In case $\left(iii\right)$, by induction, we distinguish three sub-cases:

$\left(a\right)$

$\left[\right[P_2\left]\right]\searrow b^{\prime }$ and $a^{″}=b^{\prime }\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$,

$\left(b\right)$

$P_2\equiv R^{\prime }\mid u\langle v\rangle$ and $a^{″}=\left[\right[R^{\prime }\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$,

$\left(c\right)$

$P_2\equiv \mathtt{def}{v}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{v}_n\langle t_n\rangle ▹R_n\mathtt{in}(R^{\prime }\mid u\langle v_n\rangle )$ and

$\begin{array}{ccc}\hfill a^{″}& =& \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R^{\prime }\mid \{v_n/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots ),\hfill \end{array}$ where $v_k\notin \mathtt{fn}\left(Q\right)\cup \left\{u\right\}$ for every $k\in \left[n\right]$.

In sub-case $\left(a\right)$, condition 1 holds for $b=\nu ·\left(w\right)(b^{\prime }\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$. In sub-case $\left(b\right)$, we have $P\equiv \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}(R^{\prime }\mid u\langle v\rangle )$. We distinguish two situations:

•

$v\ne w$. Then $P\equiv \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{R}^{\prime }\mid u\langle v\rangle$. It is easy to see that $\mathtt{surf}\left(\left[\right[\right\{v/y\left\}Q\left]\right]\right)\subseteq \left\{v\right\}\cup \mathtt{surf}\left(\left[\right[Q\left]\right]\right)$, and so $w\notin \mathtt{surf}\left(\left[\right[\right\{v/y\left\}Q\left]\right]\right)$. By Proposition 2, $a=\left[\right[\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{R}^{\prime }\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right]$. Thus, condition 2 holds.

•

$v=w$. Then $P\equiv \mathtt{def}v\langle t\rangle ▹P_1\mathtt{in}(R^{\prime }\mid u\langle v\rangle )$. Moreover, $a=\nu ·\left(v\right)({\mathtt{def}}_v\left(t\right)\left[\right[P_1\left]\right]$$\otimes \left[\right[R^{\prime }\mid \{v/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])$. Thus, condition 3 holds.

In sub-case $\left(c\right)$, $P\equiv \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}\mathtt{def}{v}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{v}_n\langle t_n\rangle ▹R_n\mathtt{in}(R^{\prime }\mid u\langle v_n\rangle )$. Using Proposition 2, we obtain

$\begin{array}{ccc}\hfill a& =& \nu ·\left(w\right)({\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes \hfill \\ & & \nu ·\left(v_1\right)({\mathtt{def}}_{v_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(v_n\right)({\mathtt{def}}_{v_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R^{\prime }\mid \{v_n/y\}Q\left]\right]\otimes {\mathtt{def}}_u\left(y\right)\left[\right[Q\left]\right])\dots \left)\right).\hfill \end{array}$

Thus, condition 3 holds.    □

Theorem 2.

If $\left[\right[P\left]\right]\searrow a$, then there exists a process Q such that $P\to Q$ and $\left[\right[Q\left]\right]=a$.

Proof. 

Induction on the structure of P.

–  If P is the empty process or a message, then $\left[\right[P\left]\right]⤰$. Therefore, the statement of the theorem is obviously true because the premise is not satisfied.

–  If P is a parallel composition $P_1\mid P_2$, then $\left[\right[P_1\left]\right]\otimes \left[\right[P_2\left]\right]\searrow a$. By Lemma 7, one of the following cases holds:

(1)

$\left[\right[P_1\left]\right]\searrow a_1$ and $a=a_1\otimes \left[\right[P_2\left]\right]$;

(2)

$\left[\right[P_2\left]\right]\searrow a_2$ and $a=\left[\right[P_1\left]\right]\otimes a_2$.

It is sufficient to consider the case $\left(1\right)$, the other one being similar (symmetric).

By induction, we have $P_1\to Q_1$ and $a_1=\left[\right[Q_1\left]\right]$. According to Proposition 1, $P\to Q_1\mid P_2$ and $a=\left[\right[Q_1\left]\right]\otimes \left[\right[P_2\left]\right]$. Thus, the result of the theorem holds for $Q=Q_1\mid P_2$.

–  If P is a definition $\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{P}_2$, then $\nu ·\left(w\right)(\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow a$. It follows from Lemma 2 that $\left[\right[P_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\searrow a^{\prime }$ and $a=\nu ·\left(w\right)a^{\prime }$. By Lemma 8, only one of the following cases holds:

(i)

$\left[\right[P_2\left]\right]\searrow b$ and $a^{\prime }=b\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$;

(ii)

$P_2\equiv R\mid w\langle v\rangle$ and $a^{\prime }=\left[\right[R\mid \{v/t\}{P}_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]$;

(iii)

$P_2\equiv \mathtt{def}{w}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{w}_n\langle t_n\rangle ▹R_n\mathtt{in}(R\mid w\langle w_n\rangle )$ and

    $\begin{array}{ccc}\hfill a^{\prime }& =& \nu ·\left(w_1\right)({\mathtt{def}}_{w_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(w_n\right)({\mathtt{def}}_{w_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\mid \{w_n/t\}{P}_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])...),\hfill \end{array}$

    where $w_i\notin \mathtt{fn}\left(P_1\right)\cup \left\{w\right\}$ for every $i\in \left[n\right]$.

In case $\left(i\right)$, by the induction hypothesis, $P_2\to Q_2$ and $b=\left[\right[Q_2\left]\right]$. It follows that $P\to \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{Q}_2$ and $a=\nu ·\left(w\right)(\left[\right[Q_2\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])$ Thus, the result of the theorem holds for $Q=\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}{Q}_2$.

In case $\left(ii\right)$, we have $P\to \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}(R\mid \{v/t\}{P}_1)$ and $a=\nu ·\left(w\right)(\left[\right[R\mid \{v/t\}{P}_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])=\left[\right[Q\left]\right]$. Thus, the result of the theorem holds for $Q=\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}(R\mid \{v/t\}{P}_1)$.

In case $\left(iii\right)$, it follows that $w_i\notin \mathtt{surf}\left({\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\right)$ for any $i\in \left[n\right]$ (Lemmas 2 and 4).

$P\equiv \mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}\mathtt{def}{w}_1\langle t_1\rangle ▹R_1\mathtt{in}...\mathtt{def}{w}_n\langle t_n\rangle ▹R_n\mathtt{in}(R\mid w\langle w_n\rangle )\to$

$\underset{Q}{\overset{\mathtt{def}w\langle t\rangle ▹P_1\mathtt{in}\mathtt{def}{w}_1\langle t_1\rangle ▹R_1\mathtt{in}\dots \mathtt{def}{w}_n\langle t_n\rangle ▹R_n\mathtt{in}(R\mid \{w_n/t\}{P}_1)}{⏟}}$

$\begin{array}{ccc}\hfill a& =& \nu ·\left(w\right)(\mathrm{by} \mathrm{Proposition} 2\hfill \\ & & \nu ·\left(w_1\right)({\mathtt{def}}_{w_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(w_n\right)({\mathtt{def}}_{w_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\mid \{w_n/t\}{P}_1\left]\right]\otimes {\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right])\dots \left)\right)\hfill \\ & =& \nu ·\left(w\right)({\mathtt{def}}_w\left(t\right)\left[\right[P_1\left]\right]\otimes \hfill \\ & & \nu ·\left(w_1\right)({\mathtt{def}}_{w_1}\left(t_1\right)\left[\right[R_1\left]\right]\otimes \hfill \\ & & ⋮\hfill \\ & & \nu ·\left(w_n\right)({\mathtt{def}}_{w_n}\left(t_n\right)\left[\right[R_n\left]\right]\otimes \left[\right[R\mid \{w_n/t\}{P}_1\left]\right])\dots \left)\right)\hfill \\ & =& \left[\right[Q\left]\right].\hfill \end{array}$

   □

6. Describing Communication Patterns by Using the Hypergraph Model

In the Unix operating system, interprocess communications based on message queues allow exchange of information between processes. The processes exchange information by accessing a common message queue. Essentially, one process produces a message queue (via a message-passing module) that other processes may access; often a server places a message onto a queue which can be read by multiple clients. The sending process may specify its type when placing the message in a queue such that the reading processes can select the appropriate message; thus, message queues provide a way of multiplexing information from one producer to more consumers.

As example, we consider a simple system in which only one channel is used to exchange messages between the server and clients, and any message at the input of any client must appear at the output of all the clients (this is a requirement for several social networks including a chat messaging system). A type associated to each message allows a client to access the (unique) message queue for selectively reading only specific messages (in a first-in–first-out manner). We simplify the system, and consider a process S working as a server and two clients A and B. The channels idA and idB are used to indicate the type of messages from S to A and B, respectively; a channel idS indicates the type of messages from the clients to the server. Client A uses an input channel inA and an output channel outA; client B uses channels inB and outB). For a message m sent along the input channel inA, the pattern calculus process corresponding to this system is:

$$\begin{array}{cccccc}CommSyst=\hfill & \mathtt{def}& \hfill q\langle x\rangle \mid idS\langle y\rangle & ▹& q\langle x\rangle \mid idA\langle \_\rangle \mid q\langle x\rangle \mid idB\langle \_\rangle \hfill & \wedge \hfill \\ & & \hfill q\langle x\rangle \mid idA\langle y\rangle & ▹& outA\langle x\rangle \hfill & \wedge \hfill \\ & & \hfill q\langle x\rangle \mid idB\langle y\rangle & ▹& outB\langle x\rangle \hfill & \wedge \hfill \\ & & \hfill inA\langle x\rangle & ▹& q\langle x\rangle \mid idS\langle \_\rangle \hfill & \wedge \hfill \\ & & \hfill inB\langle x\rangle & ▹& q\langle x\rangle \mid idS\langle \_\rangle \hfill & \\ & \mathtt{in}& \hfill inA\langle m\rangle .& & & \end{array}$$

Using the hypergraph model, in Figure 3 is presented the net corresponding to this process.

Except the root hyperedge, the structure of this net does not change during the evolution. Therefore, the evolution of the system could be described graphically focusing only on the root hyperedge; this evolution is depicted in Figure 4.

In Figure 4 it is not difficult to check visually the requirement that a message appearing at the input of a client appears also at the output of all the clients. In our case, the message m on the input channel inA (the initial step) appears at the output channels outA and outB in the final step described in Figure 4.

7. Conclusions and Related Work

In this paper we introduce a hypergraph model (given by the pattern nets) for the communication patterns. These nets provide a fully abstract model for the pattern calculus. In this way, a new sound graphical model for concurrency is introduced. We present a semantic interpretation of the pattern calculus in the framework of control structures, creating a graphical representation for the pattern calculus given by a new hypergraph model given by the pattern nets. By introducing a mapping from the control structure of pattern calculus into a set of hypergraphs, we provide a graphical model for communication patterns. It is also proved that the hypergraph model preserves the operational reductions of processes from pattern calculus and of the actions from the control structures. As an example, simple interprocess communications based on message queues inspired by the social networks are described by using our pattern nets. This example could be a first step towards more realistic scenarios in which the proposed model can be used to identify control structures supporting specific communication patterns. Future work will investigate realistic autonomic networking, mobility management, multiaccess selection, wireless and mobile networks (as they are presented in [12], for instance).

Graphical representations for process calculi highlight a new perception, providing a visual approach of concurrency and networks. According to our knowledge, just a few papers are devoted to the graphical presentations of the process calculi. We mention our previous attempts, namely the faithful $\pi$-nets [13], a graphical representation of the $\pi$-calculus machine [14], and a related approach by using jc-nets [15]. There exist also the graphical representations introduced by Robin Milner, namely action graphs and $\pi$-nets. Action graphs [16] are the graphical presentation of action calculi; they are very general, and so they are not able to describe specific features of certain action calculi. In the graphical presentation of the $\pi$-calculus given by the $\pi$-nets [6], channels are represented as rather complicated nodes called torpedos together with boxes representing guards, and messages are represented as directed arcs. The boxes obscure the internal nodes representing channels; to ensure access to the hidden channels, a rather complex additional mechanism of links is used. To avoid such a mechanism, in [13,14] the channels are represented by nodes, messages are represented by boxes of arcs and guards are represented by arcs between boxes. This approach simplified the graphical representation of the $\pi$-calculus; unfortunately, it provided identical representations for processes with different behaviours. Fortunately, this deficiency was overtaken in the pattern calculus hypergraph model: processes with different behaviours are not mapped to the same hypergraph. The hypergraph model is presented in the same formal framework used for the $\pi$-nets (it is worth noting that hypergraph model avoids certain irrelevant aspects of $\pi$-nets). It is simpler than the $\pi$-nets, preserving much of their expressive power (according to [2], the join calculus has the same expressive power as the $\pi$-calculus). Compared with all of them, the pattern nets represent a simple but sound graphical model for concurrency, providing a fully abstract model for the pattern calculus.