# Compositional Separation of Control Flow and Data Flow

Damian Arellanes
Lancaster University, United Kingdom

###### Abstract

Every constructive model of computation (CMC) has an underlying composition
mechanism for combining simple computation devices into more complex ones.
Composition can be done by (explicitly or implicitly) defining control flow,
data flow or any combination thereof. Control flow specifies the order in
which individual computation devices are activated, whereas data flow defines
how data is exchanged among them. Unfortunately, traditional CMCs either mix
data and control or only consider one dimension explicitly, which makes it
difficult to reason about data flow and control flow separately. Reasoning
about these dimensions orthogonally is a crucial desideratum for optimisation,
maintainability and verification purposes. In this paper, we introduce a novel
model that explicitly treats data flow and control flow as separate
dimensions, while providing modularity. As the model is rooted in category
theory, it provides category-theoretic operations for compositionally
constructing sequential or parallel composites. Compositionality entails that
a composite exhibits the same properties as its respective constituents,
including separation of concerns and modularity.

1.3in

##  1 Introduction

In the context of theoretical computer science, _compositionality_ refers to
the property of constructive models of computation (CMCs) that allows the
inductive definition of complex computation devices from simpler ones [1].
Examples of such models, which are specifically designed to be useful in the
actual construction of computing systems, include the von Neumann model, the
actor model and process algebras [2].

When composition is done algebraically, the resulting computation structures
(known as _composites_) exhibit the same characteristics as their constituents
[3]. Algebraic compositionality can be realised by the composition of _control
flow_ [4] or _data flow_ [5]. Control flow defines the order in which
individual computation devices are computed, whereas data flow defines how
data is passed among them. Traditionally, CMCs do not support algebraic
composition and they allow the definition of computations in which data
follows control. This sort of coupling makes it difficult (i) to (formally)
reason about computation order and data production/consumption separately and
(ii) to explicitly distinguish between control and data dependencies [6].
Consequently, it is hard to (i) verify these dimensions independently [7, 8],
or (ii) modify/optimise control flow without affecting data flow (or
viceversa) [9, 10]. For these reasons, enabling separation of control flow and
data flow within the foundational composition semantics of any constructive
model of computation is a crucial desideratum.

While _control-based composition_ approaches define explicit control flow for
the coordination of computation devices, _data-based composition_ defines
implicit control in the collaborative exchange of data [11]. Thus, the notion
of control flow has higher precedence than data flow because it is always
present in any composition mechanism (and not the other way round).111A
potential explanation is that the notion of control flow is tightly linked to
the arrow of time, whereas data is just a piece of information that is sent
from one place to another in some specific time-dependent order. In fact, it
is possible to compose complex computations by control flow only and without
the need of passing data at all (cf. actuator composition [12]).222Even if we
argue that control is a piece of information/data, the act of sending it from
one computation device to another is still governed by the grandiose,
apparently unavoidable, notion of control flow (cf. interleaving semantics for
global execution traces in concurrent systems [13]).

For the above reasons, we believe that the right way of constructing complex
computational behaviours is through a control-based composition mechanism that
does not neglect the role of data passing. Accordingly, in this paper we
propose a model in which fundamental units of composition (known as
_computons_) are passive open systems able to interact with their environment
via an interface which consists of input and output ports. As a port is a
structural construct that can exclusively buffer either data or control,
computons exchange data and control separately. Our model is compositional in
the sense that computons can be inductively composed into larger ones via
well-defined control-based composition operations. Such operations are rooted
in category theory and allow the formal construction of sequential or parallel
computons from simpler ones. As a result of the compositional semantics,
composites preserve the structure of the composed entities, so they also
separate data and control and their port-based interface is inductively
constructed from the composed computons. Remarkably, unlike existing
compositional approaches, any two computons can always be composed either
sequentially or in parallel.

Apart from being compositional and separating concerns, our model enables
modularity and control flow encapsulation, which allows treating computons
unifiedly. Encapsulation is realised by the fact that a composite defines some
precise, explicit control flow structure (e.g., sequencing or parallelising)
that can only be accessed through the respective computon interface. Thus, a
computon can be perceived as an encapsulated black-box that can only interact
with other computons via its ports. Hiding internal details in this way enable
us to build computons of considerable complexity.

The rest of the paper is structured as follows. Section 2 presents the
definition of computons by treating them as set-valued functors in a category
that we introduce which we refer to as the _category of computons and computon
morphisms_. Although this paper is focused on the compositional construction
of such entities and not on their operational semantics, Section 3 briefly
discusses the notion of computon computation by borrowing ideas from the well-
known _token game_ that has been used in the context of P/T Petri Nets for
many years. Sections 4 and 5 present the most elementary classes of computons
that serve as building blocks for constructing complex composites. Section 6
describes formal category-theoretic operations to form either sequential or
parallel composites. Section 7 presents and analyses related work, and Section
8 outlines the conclusions and future directions of our work.

##  2 Computons

Intuitively, a _computon_ is a bipartite graph with two types of nodes:
_computation units_ and _ports_.333The word _computon_ derives from the Latin
root for computation (i.e., _computus_) and the Greek suffix _-on_ [14]. In
Physics, such a suffix is traditionally used to designate subatomic particle
names. A computation unit is a construct that receives information in ports,
performs some computation and produces new information in other ports. A port
that is connected between two computation units is known as _internal port_
(or _i-port_), whereas a port that is exclusively connected to or from a
computation unit is called _external_ (or _e-port_). As ports and computation
units are connected via edges, edges represent information flow ranging from
control signals to complex data values.

The interface of a computon towards the outside world is determined by its
collection of e-ports each being an external control inport (_ec-inport_), an
external control outport (_ec-outport_), an external data inport (_ed-inport_)
or an external data outport (_ed-outport_). An ec-inport is where control flow
originates, an ec-outport is where control-flow terminates, an ed-inport
stores data coming from the external world whereas an ed-outport stores data
resulting from the computon’s operation.

Just as there are _ec-ports_ and _ed-ports_ , there are also internal control
ports (_ic-ports_) and internal data ports (_id-ports_). The dichotomy between
data and control in our proposal entails that a computon is a unit of control-
driven computation wherein control signals and data values travel
independently via edges. Ports are differentiated by colours which, in
practice, can be abstract data types such as the type of Booleans or the type
of Integers. In this paper, in order to provide a general “type distinction
framework”, ports are deliberatively coloured with natural numbers.444From a
programmer’s perspective, a colour can correspond to a component interface in
the context of component-based software development [3]. Thus, in a user-
oriented programming language or in a component model, every natural number
can be associated with an actual type which can be defined as a many-sorted
sigma algebra. The number zero is reserved for control ports, whereas data
ports are coloured with natural numbers greater than zero.

Formally, a computon is a functor from Comp to Set (see Definition 1) where
Set is the category of sets and total functions and Comp is the free category
generated by the following diagram:555Following the notation of function
abstraction in Lambda Calculus, we use $\lambda$ to denote computons.

${E}$${U}$${P}$${\Sigma}$${F}$$\scriptstyle{\sigma}$$\scriptstyle{t}$$\scriptstyle{c}$$\scriptstyle{\tau}$$\scriptstyle{s}$

which consists of five objects and twelve morphisms (including identity and
composite morphisms given by trivial paths and path concatenation,
respectively).

######  Definition 1 (Computon).

A computon $\lambda$ is a functor ${\textbf{Comp}\rightarrow\textbf{Set}}$
that maps:

  * 1.

$U$ to a (possibly empty) set $\lambda(U)$ of computation units,

  * 2.

$P$ to a (non-empty) set $\lambda(P)$ of ports,

  * 3.

$E$ to a (possibly empty) set $\lambda(E)$ of edges,

  * 4.

$F$ to a (possibly empty) set $\lambda(F)$ of edges,

  * 5.

$\Sigma$ to a (non-empty) set ${\lambda(\Sigma)\subset\mathbb{N}}$ of colours,

  * 6.

$\sigma$ to a total surjective function
$\lambda(\sigma):\lambda(E)\twoheadrightarrow\lambda(U)$ that specifies the
outgoing edges of each computation unit,

  * 7.

$\tau$ to a total surjective function
$\lambda(\tau):\lambda(F)\twoheadrightarrow\lambda(U)$ that specifies the
incoming edges of each computation unit,

  * 8.

$t$ to a total function ${\lambda(t):\lambda(E)\rightarrow\lambda(P)}$ that
specifies the incoming edges of each port,

  * 9.

$s$ to a total function ${\lambda(s):\lambda(F)\rightarrow\lambda(P)}$ that
specifies the outgoing edges of each port, and

  * 10.

$c$ to a total surjective function
${\lambda(c):\lambda(P)\twoheadrightarrow\lambda(\Sigma)}$ that assigns to
each port a colour,

such that there is:

  * 1.

an identity function $1_{\lambda(x)}$ in Set for each object $x$ of Comp,

  * 2.

a composite function $\lambda(g)\circ\lambda(f)$ in Set for each pair $(f,g)$
of composable morphisms in Comp,

  * 3.

at least one port ${p\in{[\lambda(P)\setminus Im(\lambda(s))]}}$ with
${\lambda(c)(p)=0}$ and

  * 4.

at least one port ${q\in{[\lambda(P)\setminus Im(\lambda(t))]}}$ with
${\lambda(c)(q)=0}$.

As a computon $\lambda$ is a set-valued functor, it can be expressed in the
form of a tuple ${(U,P,E,F,\Sigma,\sigma,\tau,t,s,c)}$. Without loss of
generality, we took the liberty of simplifying the expression in order to
reduce clutter, e.g., we write $U$ for $\lambda(U)$. For the rest of the
paper, the reader must bear in mind that each component of $\lambda$ is an
actual set or a function, not an object or a morphism in Comp. To distinguish
between computons, we use natural numbers as subscripts which carry over
computon components. If the symbol for a computon has no subscript, we assume
that the computon components have no subcript either.

The surjectivity condition of Definition 1 entails that every computation unit
(if any) has at least one incoming edge and at least one outgoing edge. As
every function we deal with is a total function, we also have that every edge
goes from a port to a computation unit or viceversa. That is, a computon has
neither dangling edges nor dangling computation units.

######  Definition 2 (Computon Interface).

The interface of a computon $\lambda$ towards the external world is a tuple
$(P^{+},P^{-})$ where ${P^{+}:=\\{p\in P\mid(\nexists e\in E)[t(e)=p]\\}}$ is
the set of e-inports of $\lambda$ and $P^{-}:=\\{p\in P\mid(\nexists f\in
F)[s(f)=p]\\}$ is the set of e-outports of $\lambda$. A port ${p\in Im(s)\cap
Im(t)}$ is called an i-port of $\lambda$.

######  Notation 1.

Given a computon $\lambda$, $Q^{+}$ denotes its set of ec-inports, $Q^{-}$ its
set of ec-outports, $D^{+}$ its set of ed-inports and $D^{-}$ its set of ed-
outports. These sets are defined as follows:

${Q^{\square}:=\\{p\in P^{\square}\mid c(p)=0\\}}\text{ with
}\square\in\\{+,-\\}$ ${D^{\square}:=\\{p\in P^{\square}\mid c(p)>0\\}}\text{
with }\square\in\\{+,-\\}$

Notice in Definition 2 that the sets $P^{+}$ and $P^{-}$ are not necessarily
disjoint so that a port can be e-inport and e-outport at the same time. A port
$p$ of this sort is called _e-inoutport_ and, like the others, it can also
buffer control or data. If ${p\in Q^{+}\cap Q^{-}}$, then it is called _ec-
inoutport_. If ${p\in D^{+}\cap D^{-}}$, it is called _ed-inoutport_.

As control ports and data ports are identified as separate entities,
information movement within a computon corresponds to either data flow or
control flow. Particularly, we say that any control port is connected to or
from a computation unit via a control flow edge, whereas a data port is
connected analogously but with a data flow edge (see Definitions 3 and 4). The
collection of ports receiving and sending information from/to a computation
unit $u$ are denoted $u\bullet$ and $\bullet u$, respectively. Similarly,
$\bullet p$ and $p\bullet$ denote the source and target computation units of a
port $p$, respectively (see Definition 5). When there is information flow from
every e-inport to every e-outport, we say that the computon is connected (see
Definition 6). As per Proposition 1, a computon of this sort always has
computation units.

######  Definition 3 (Information Flow).

Given a computon $\lambda$, let $p\in P$ and $u\in U$. We say that there is
information flow from $p$ to $u$ if there is an edge $f\in F$ such that
$s(f)=p$ and $\tau(f)=u$. This is denoted ${p\xrightarrow{f}u}$. If there is
an edge $e\in E$ with $\sigma(e)=u$ and $t(e)=p$, we say that there is
information flow from $u$ to $p$, written ${u\xrightarrow{e}p}$. We use
${p_{1}\xrightarrow{*}p_{n}}$ to denote the existence of
${p_{1}\xrightarrow{f_{1}}u_{1}\xrightarrow{e_{1}}p_{2}\xrightarrow{f_{2}}u_{2}\xrightarrow{e_{2}}\cdots\xrightarrow{f_{n-1}}u_{n-1}\xrightarrow{e_{n-1}}p_{n}}$
where $p_{1},\ldots,p_{n}\in P$, $u_{1},\ldots,u_{n-1}\in U$,
$e_{1},\ldots,e_{n-1}\in E$ and $f_{1},\ldots,f_{n-1}\in F$.

######  Definition 4 (Control Flow and Data Flow Edges).

Given a computon $\lambda$ and an edge ${e\in E\cup F}$, we say that $e$
represents control flow if ${c(s(e))=0}$ or ${c(t(e))=0}$; otherwise, it
represents data flow.

######  Definition 5 (Pre- and Post-Sets).

For a computation unit ${u\in U}$ of a computon $\lambda$, ${\bullet u}$ and
${u\bullet}$ denote the sets ${\\{p\in P\mid(\exists f\in
F)(p\xrightarrow{f}u)\\}}$ and ${\\{p\in P\mid(\exists e\in
E)(u\xrightarrow{e}p)\\}}$, respectively. Similarly, for a port ${p\in P}$,
${\bullet p}$ and ${p\bullet}$ denote the sets $\\{u\in U\mid(\exists e\in
E)(u\xrightarrow{e}p)\\}$ and $\\{u\in U\mid(\exists f\in
F)(p\xrightarrow{f}u)\\}$, respectively.

######  Definition 6 (Connected Computon).

We say that a computon $\lambda$ is connected if and only if $(\forall p\in
P^{+})(\forall q\in P^{-})[p\xrightarrow{*}q]$.

######  Proposition 1.

Every connected computon has at least one computation unit.

###### Proof.

Assume for contrapositive that $\lambda$ is a computon with $U=\emptyset$,
which means that $\sigma$ and $\tau$ are well-defined only if
${E=\emptyset=F}$. Since $\lambda$ has no edges and no computation units, we
have that there is no $f\in F$ and no $e\in E$ where
$p\xrightarrow{f}\cdots\xrightarrow{e}q$ holds for some $p\in P^{+}$ and some
$q\in P^{-}$, i.e., $\lambda$ is not a connected computon because
$p\xrightarrow{*}q$ never holds (see Definition 6). By logical equivalence, we
conclude that the proposition is true. ∎

At this stage, we have provided sufficient details about the general structure
of computons by treating them as set-valued functors. Defining computons in
this way gives rise to a functor category $\textbf{Set}^{\textbf{Comp}}$ whose
objects are computons and whose morphisms are computon morphisms.

######  Definition 7 (Computon morphism).

If $\lambda_{1}$ and $\lambda_{2}$ are two computons, a computon morphism
${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ is a natural transformation whose
components are the total functions ${\alpha_{U}:U_{1}\rightarrowtail U_{2}}$,
${\alpha_{P}:P_{1}\rightarrowtail P_{2}}$, ${\alpha_{E}:E_{1}\rightarrowtail
E_{2}}$, ${\alpha_{F}:F_{1}\rightarrowtail F_{2}}$ and
${\alpha_{\Sigma}:\Sigma_{1}\hookrightarrow\Sigma_{2}}$ such that the diagrams
of Figure 1 commute and ${\vec{i}(\alpha)\cup\vec{o}(\alpha)\subseteq
P_{1}^{+}\cup P_{1}^{-}}$. Here, $\vec{i}(\alpha)$ and $\vec{o}(\alpha)$
denote ${\\{p_{1}\in P_{1}\mid\bullet\alpha(p_{1})\setminus\alpha(\bullet
p_{1})\neq\emptyset\\}}$ and ${\\{p_{1}\in
P_{1}\mid\alpha(p_{1})\bullet\setminus\alpha(p_{1}\bullet)\neq\emptyset\\}}$,
respectively.

${P_{1}}$${\Sigma_{1}}$${P_{2}}$${\Sigma_{2}}$$\scriptstyle{c_{1}}$$\scriptstyle{\alpha_{P}}$$\scriptstyle{\alpha_{\Sigma}}$$\scriptstyle{c_{2}}$

${F_{1}}$${U_{1}}$${E_{1}}$${F_{2}}$${U_{2}}$${E_{2}}$$\scriptstyle{\tau_{1}}$$\scriptstyle{\alpha_{F}}$$\scriptstyle{\alpha_{U}}$$\scriptstyle{\sigma_{1}}$$\scriptstyle{\alpha_{E}}$$\scriptstyle{\tau_{2}}$$\scriptstyle{\sigma_{2}}$

${F_{1}}$${P_{1}}$${E_{1}}$${F_{2}}$${P_{2}}$${E_{2}}$$\scriptstyle{s_{1}}$$\scriptstyle{\alpha_{F}}$$\scriptstyle{\alpha_{P}}$$\scriptstyle{t_{1}}$$\scriptstyle{\alpha_{E}}$$\scriptstyle{s_{2}}$$\scriptstyle{t_{2}}$

Figure 1: A computon morphism is a natural transformation
$\alpha:\lambda_{1}\rightarrow\lambda_{2}$.

######  Notation 2.

To simplify notation when referring to the components of a computon morphism
$\alpha:\lambda_{1}\rightarrow\lambda_{2}$, we write $\alpha(u)$ for
$\alpha_{U}(u)$, $\alpha(p)$ for $\alpha_{P}(p)$, $\alpha(e)$ for
$\alpha_{E}(e)$ and $\alpha(f)$ for $\alpha_{F}(f)$. For the rest of the
paper, we also write $\alpha(A)$ to denote $Im(\alpha_{P}|_{A})$ if
$A\subseteq P_{1}$ or $Im(\alpha_{U}|_{A})$ if $A\subseteq U_{1}$. Likewise,
we use $\alpha(B)^{-1}$ to denote $\\{p_{1}\in P_{1}\mid\alpha(p_{1})\in B\\}$
if $B\subseteq P_{2}$ or $\\{u_{1}\in U_{1}\mid\alpha(u_{1})\in B\\}$ if
$B\subseteq U_{2}$.

######  Remark 1.

From Definition 7, it is easy to see that a computon morphism is a
monomorphism because all its components are injective (even the
$\Sigma$-component which is an inclusion map). Naturally, composition of
computon morphisms $\alpha$ and $\beta$ is defined component-wise:

$\begin{split}(\beta_{U},\beta_{P},\beta_{E},&\beta_{F},\beta_{\Sigma})\circ(\alpha_{U},\alpha_{P},\alpha_{E},\alpha_{F},\alpha_{\Sigma})=(\beta_{U}\circ\alpha_{U},\beta_{P}\circ\alpha_{P},\beta_{E}\circ\alpha_{E},\beta_{F}\circ\alpha_{F},\beta_{\Sigma}\circ\alpha_{\Sigma})\end{split}$

A monomorphism avoids mapping multiple ports of $\lambda_{1}$ to the same port
in $\lambda_{2}$. As this restriction also applies to computation units and
edges, it is true that $\lambda_{2}$ has the same or more complex structure
than $\lambda_{1}$, i.e., a computon morphism does not describe a process of
simplifying a computon.

Intuitively, a computon morphism $\alpha:\lambda_{1}\rightarrow\lambda_{2}$ is
an embedding (or an insertion) of a computon $\lambda_{1}$ into a (potentially
more complex) computon $\lambda_{2}$, which preserves ports (with their
respective colours, incoming edges and outgoing edges) and computation units
(with their respective incoming and outgoing edges). As a result of this
preservation, an e-inport of $\lambda_{1}$ is either an e-inport in
$\lambda_{2}$ or an i-port $p_{2}\in P_{2}$ provided that ${(\exists e_{2}\in
E_{2})(\exists u_{2}\in U_{2})[u_{2}\xrightarrow{e_{2}}p_{2}]}$ — see
Propositions 2, 3 and 4. Similarly, an e-outport of $\lambda_{1}$ is either an
e-outport in $\lambda_{2}$ or an i-port $q_{2}\in P_{2}$ provided that
${(\exists f_{2}\in F_{2})(\exists u_{2}\in
U_{2})[q_{2}\xrightarrow{f_{2}}u_{2}]}$ — see Propositions 2, 3 and 4. While
external ports can be demoted to internal ports in $\lambda_{2}$, internal
ports can never be promoted to external ones due to the commutative diagrams
presented in Figure 1.

######  Proposition 2.

If ${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ is a computon morphism,
${\alpha^{-1}(P_{2}^{+})\subseteq P_{1}^{+}}$ and
${\alpha^{-1}(P_{2}^{-})\subseteq P_{1}^{-}}$.

###### Proof.

By letting ${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ be a computon
morphism, we only prove ${\alpha^{-1}(P_{2}^{+})\subseteq P_{1}^{+}}$ by
contrapositive, since the proof of ${\alpha^{-1}(P_{2}^{-})\subseteq
P_{1}^{-}}$ is completely analogous.

If ${p_{1}\in P\setminus P_{1}^{+}}$, then ${(\exists e_{1}\in
E_{1})[t_{1}(e_{1})=p_{1}]}$ (see Definition 2). By commutativity, we know
that ${t_{2}(\alpha(e_{1}))=\alpha(t_{1}(e_{1}))=\alpha(p_{1})}$ which implies
that ${\alpha(p_{1})\notin P_{2}^{+}}$ (see Definition 2) and, consequently,
that ${p_{1}\notin\alpha^{-1}(P_{2}^{+})}$. As the implication ${p_{1}\notin
P_{1}^{+}\implies p_{1}\notin\alpha^{-1}(P_{2}^{+})}$ is logically equivalent
to ${p_{1}\in\alpha^{-1}(P_{2}^{+})\implies p_{1}\in P_{1}^{+}}$, we conclude
that ${\alpha^{-1}(P_{2}^{+})\subseteq P_{1}^{+}}$, as required. ∎

######  Proposition 3.

If ${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ is a computon morphism,
${P_{1}^{+}\cap\vec{i}(\alpha)=\emptyset\implies\alpha^{-1}(P_{2}^{+})=P_{1}^{+}}$
and
${P_{1}^{-}\cap\vec{o}(\alpha)=\emptyset\implies\alpha^{-1}(P_{2}^{-})=P_{1}^{-}}$.

###### Proof.

Let ${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ be a computon morphism and
assume that ${P_{1}^{+}\cap\vec{i}(\alpha)=\emptyset}$. This assumption says
that if ${p_{1}\in P_{1}^{+}}$ then ${p_{1}\notin\vec{i}(\alpha)}$ so that
${\bullet\alpha(p_{1})\setminus\alpha(\bullet p_{1})=\emptyset}$ which is true
when ${\bullet\alpha(p_{1})=\alpha(\bullet p_{1})}$. As ${\bullet
p_{1}=\emptyset}$ because ${p_{1}\in P_{1}^{+}}$, we have that
${\bullet\alpha(p_{1})=\emptyset=\alpha(\bullet p_{1})}$. The fact
${\bullet\alpha(p_{1})=\emptyset}$ implies that ${\alpha(p_{1})\in
P_{2}^{+}}$, i.e., ${p_{1}\in\alpha^{-1}(P_{2}^{+})}$. Thus, proving that
${P_{1}^{+}\subseteq\alpha^{-1}(P_{2}^{+})}$. Since
${\alpha^{-1}(P_{2}^{+})\subseteq P_{1}^{+}}$ also holds by Proposition 2, we
conclude that
$P_{1}^{+}\cap\vec{i}(\alpha)=\emptyset\implies\alpha^{-1}(P_{2}^{+})=P_{1}^{+}$.

The proof of
${P_{1}^{-}\cap\vec{o}(\alpha)=\emptyset\implies\alpha^{-1}(P_{2}^{-})=P_{1}^{-}}$
follows analogously. ∎

######  Proposition 4.

If $\lambda_{1}$ is a connected computon and
${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ is a computon morphism,
${(P_{1}^{+}\cap\vec{i}(\alpha))\cup(P_{1}^{-}\cap\vec{o}(\alpha))\subseteq\alpha^{-1}(Im(t_{2})\cap
Im(s_{2}))}$.

###### Proof.

Let ${\alpha:\lambda_{1}\rightarrow\lambda_{2}}$ be a computon morphism. If
${p_{1}\in P_{1}^{+}\cap\vec{i}(\alpha)}$, then there is some
${u_{2}\in\bullet\alpha(p_{1})\setminus\alpha(\bullet p_{1})}$. By Definition
5, there must also be some ${e_{2}\in E_{2}}$ where
${\sigma_{2}(e_{2})=u_{2}}$ and ${t_{2}(e_{2})=\alpha(p_{1})}$. That is,
${\alpha(p_{1})\in Im(t_{2})}$.

Now, since $\lambda_{1}$ is a connected computon and ${p_{1}\in P_{1}^{+}}$,
there is some ${f_{1}\in F_{1}}$ and some ${u_{1}\in U_{1}}$ where
${p_{1}\xrightarrow{f_{1}}u_{1}}$ holds (see Proposition 1). By commutativity
and because ${s_{1}(f_{1})=p_{1}}$,
${s_{2}(\alpha(f_{1}))=\alpha(s_{1}(f_{1}))=\alpha(p_{1})}$. That is,
${\alpha(p_{1})\in Im(s_{2})}$.

Having ${\alpha(p_{1})\in Im(t_{2})\cap Im(s_{2})}$ implies
${p_{1}\in\alpha^{-1}(Im(t_{2})\cap Im(s_{2}))}$; thus, proving that
${P_{1}^{+}\cap\vec{i}(\alpha)\subseteq\alpha^{-1}(Im(t_{2})\cap Im(s_{2}))}$.
The proof of ${P_{1}^{-}\cap\vec{o}(\alpha)\subseteq\alpha^{-1}(Im(t_{2})\cap
Im(s_{2}))}$ is completely analogous. ∎

##  3 Operational Semantics

The operational semantics of a computon can be described as a _token game_
because the structure of a computon can be expressed as a whole-grain Petri
net with typed tokens (which we refer to as a _TWP_). To construct concrete
TWPs, in this paper we consider a variation to the scheme presented in [15],
which provides support not only to colour tokens but also places. This variant
scheme, which fits into the _individual token philosophy_ , is formalised
below.

######  Definition 8.

TWPetri is the free category generated by the following diagram:

${O}$${T}$${S}$${L}$${I}$${R}$$\scriptstyle{\sigma^{\prime}}$$\scriptstyle{t^{\prime}}$$\scriptstyle{c^{\prime}}$$\scriptstyle{\tau^{\prime}}$$\scriptstyle{s^{\prime}}$$\scriptstyle{\mu}$$\scriptstyle{\nu}$

where identity morphisms and composite morphisms are given by trivial paths
and path concatenation, respectively.

Naturally, there is an obvious functor
$X:\textbf{Comp}\rightarrow\textbf{TWPetri}$ sending $U$ to $T$, $P$ to $S$,
$E$ to $O$, $F$ to $I$, $\Sigma$ to $L$, $\sigma$ to $\sigma^{\prime}$, $\tau$
to $\tau^{\prime}$, $t$ to $t^{\prime}$, $s$ to $s^{\prime}$ and $c$ to
$c^{\prime}$, whose existence entails that a computon can be extended with the
notion of port marking. If $N:\textbf{TWPetri}\rightarrow\textbf{Set}$ is a
functor that specifies a concrete TWP, then the composite functor $N\circ
X:\textbf{Comp}\rightarrow\textbf{Set}$ defines a marked computon (see
Definition 9). From now on, we use traditional Petri net notation whenever we
need to discuss computon executions/computations. The mapping between computon
syntax and Petri net syntax is presented in A.

######  Definition 9 (Marked Computon).

A marked computon is a composite functor $N\circ
X:\textbf{Comp}\rightarrow\textbf{Set}$ where $N$ is a functor
${\textbf{TWPetri}\rightarrow\textbf{Set}}$ mapping:

  * 1.

$T$ to a (possibly empty) set $N(T)$ of transitions,

  * 2.

$O$ to a (possibly empty) set $N(O)$ of outputs,

  * 3.

$I$ to a (possibly empty) set $N(I)$ of inputs,

  * 4.

$S$ to a (non-empty) set $N(S)$ of places,

  * 5.

$R$ to a (non-empty) set $N(R)$ of tokens,

  * 6.

$L$ to a (non-empty) set $N(L)\subset\mathbb{N}$,

  * 7.

$\sigma^{\prime}$ to a function $N(\sigma^{\prime}):N(O)\rightarrow N(T)$ that
assigns outputs to transitions,

  * 8.

$\tau^{\prime}$ to a function $N(\tau^{\prime}):N(I)\rightarrow N(T)$ that
assigns inputs to transitions,

  * 9.

$t^{\prime}$ to a function $N(t^{\prime}):N(O)\rightarrow N(S)$ that assigns
outputs to places,

  * 10.

$s^{\prime}$ to a function $N(s^{\prime}):N(I)\rightarrow N(S)$ that assigns
inputs to places,

  * 11.

$c^{\prime}$ to a function $N(c^{\prime}):N(S)\rightarrow N(L)$ that assigns
to each place a label,

  * 12.

$\mu$ to a function $N(\mu):N(R)\rightarrow N(S)$, called a marking function,
which assigns tokens to places, and

  * 13.

$\nu$ to a function $N(\nu):N(R)\rightarrow N(L)$ that assigns to each token a
label,

such that there is:

  * 1.

an identity function $1_{\lambda(x)}$ in Set for each object $x$ of TWPetri
and

  * 2.

a composite function $\lambda(g)\circ\lambda(f)$ in Set for each pair $(f,g)$
of composable morphisms in TWPetri.

######  Remark 2.

The equation $N(c^{\prime})\circ N(\mu)=N(\nu)$ deduced from Definition 9
entails that tokens are labelled in the same way as the places they are mapped
to. That is, places admit tokens of one type only.

######  Notation 3.

Given a TWP ${N:\textbf{TWPetri}\rightarrow\textbf{Set}}$, a token ${r\in
N(R)}$ is called a control token if ${N(\nu)(r)=0}$; otherwise, it is called a
data token.

If ${\lambda}$ is a computon and $N\circ X$ is a marked computon constructed
from $\lambda$, then there is a natural transformation
${\gamma:\lambda\rightarrow N}$ whose components are the total functions
${\gamma_{S}:P\rightarrow N(S)}$, ${\gamma_{T}:U\rightarrow N(T)}$,
${\gamma_{I}:F\rightarrow N(I)}$, ${\gamma_{O}:E\rightarrow N(O)}$ and
${\gamma_{L}:\Sigma\rightarrow N(L)}$:

CompSetTWPetri$\scriptstyle{X}$$\scriptstyle{\lambda}$$\scriptstyle{N}$$\scriptstyle{\gamma}$

such that the following diagrams commute:

${P}$${\Sigma}$${N(S)}$${N(L)}$${N(R)}$$\scriptstyle{c}$$\scriptstyle{\gamma_{S}}$$\scriptstyle{\gamma_{L}}$$\scriptstyle{N(c^{\prime})}$$\scriptstyle{N(\mu)}$$\scriptstyle{N(\nu)}$
${F}$${U}$${E}$${N(I)}$${N(T)}$${N(O)}$$\scriptstyle{\tau}$$\scriptstyle{\gamma_{I}}$$\scriptstyle{\gamma_{T}}$$\scriptstyle{\sigma}$$\scriptstyle{\gamma_{O}}$$\scriptstyle{N(\tau^{\prime})}$$\scriptstyle{N(\sigma^{\prime})}$
${F}$${P}$${E}$${N(I)}$${N(S)}$${N(O)}$${N(R)}$$\scriptstyle{s}$$\scriptstyle{\gamma_{I}}$$\scriptstyle{\gamma_{S}}$$\scriptstyle{t}$$\scriptstyle{\gamma_{O}}$$\scriptstyle{N(s^{\prime})}$$\scriptstyle{N(t^{\prime})}$$\scriptstyle{N(\mu)}$

By defining a marked computon as a composite functor along TWPetri, it is
possible to describe the operational semantics of a computon in the form of a
concrete TWP (which behaves just like a traditional P/T Petri net [15, 16]).
Particularly, if $N\circ X$ is a marked computon, then:666Abusing the notation
used in Definition 5, we write $\bullet t$ and $t\bullet$ to denote the pre-
and post-set of places of a transition $t$.

  * 1.

A transition ${t\in(N\circ X)(U)}$ is enabled by a marking whenever each input
place $p\in\bullet t$ has at least one appropriately coloured token.

  * 2.

If a transition ${t\in(N\circ X)(U)}$ is enabled at some marking, then $t$
fires and a new marking is reached. The new marking indicates that $t$
consumes one token from each $p\in\bullet t$ and produces one appropriately
coloured token in each $q\in t\bullet$.

The main focus of this paper is on computon compositionality. Above we just
presented a general overview of the _token game for computons_. The fact that
the operational semantics of computons is given as a composite functor along
TWPetri entails that all the theory of processes presented in [16] can be
applicable to our work.

In the future, we intend to explore computon processes in more detail. For
now, we would just like to highlight that, due to the inherent concurrent
nature of Petri nets, control tokens can arrive before data tokens (or
viceversa). By having control ports separated from data ports, a transition
only fires when both control tokens and data tokens are placed in their
respective inports. This means that a computation unit is a passive construct
with blocking behaviour which synchronises data and control before firing.
After firing, a computation unit produces exactly one token in each of its
outports.

By the above, the e-inports and e-outports of a computon can be deemed as pre-
and post-conditions, respectively. So, we can say that a computon is activated
in some state of the world in which all pre-conditions hold, and its
computation results in a change of the state of the world in which all post-
conditions hold.

##  4 Trivial Computons

A _trivial computon_ has no computation units, no edges and no i-ports at all,
but just a number of e-inoutports. Up to isomorphism, it is the only object in
$\textbf{Set}^{\textbf{Comp}}$ with no computation units (see Proposition 5).

######  Definition 10 (Trivial Computon).

A trivial computon $\lambda$ is a computon whose diagram in Set has the form:

${\emptyset}$${\emptyset}$${P}$${\Sigma}$${\emptyset}$$\scriptstyle{\sigma}$$\scriptstyle{t}$$\scriptstyle{c}$$\scriptstyle{\tau}$$\scriptstyle{s}$

######  Proposition 5.

A computon has no computation units if and only if it is a trivial computon.

###### Proof.

$(\implies)$ Let $\lambda$ be a computon with $U=\emptyset$. By the definition
of empty function, we have that $U=\emptyset$ only if $E=\emptyset=F$ so that
$\sigma$ and $\tau$ are surjective. Definition 1 states that any computon is
required to have at least one coloured port so that $|P|\geq 1$ and
$|\Sigma|\geq 1$. As $s$ and $t$ are not surjective by the definition of empty
function, we have that $p\in P^{+}\cap P^{-}$ for all $p\in P$ (see Definition
2). Particularly, if $c(p)=0$, then $p\in Q^{+}\cap Q^{-}$; otherwise, $p\in
D^{+}\cap D^{-}$. As the function $c$ is surjective by Definition 1, we
conclude that $\lambda$ is a trivial computon.

$(\impliedby)$ This follows directly from Definition 10. ∎

The general structure of a trivial computon with $i$ ec-inoutports and $j$ ed-
inoutports is depicted in Figure 2.

$c(q_{1})$$\vdots$$c(q_{i})$$\vdots$$c(d_{1})$$\vdots$$c(d_{j})$ (a) Petri net
syntax. $c(q_{1})$$\vdots$$c(q_{i})$$\vdots$$c(d_{1})$$\vdots$$c(d_{j})$ (b)
Computon syntax.

Ec-inoutportEd-inoutport

Figure 2: Syntactic representations of a trivial computon $\lambda$ where
${q_{1},\ldots,q_{i}\in(Q^{+}\cap Q^{-})}$ and
${d_{1},\ldots,d_{j}\in(D^{+}\cap D^{-})}$.

Figure 2 shows two equivalent syntactic representations of a trivial computon.
One of them is based on Petri net syntax, whereas the other is based on a
syntax specifically designed to represent computons (see A), which is much
simpler and will be relevant to discuss the algebraic properties of computons,
apart from providing extra clarity when depicting complex structures. Computon
syntax also enables a clear separation of control and data ports. For
convenience, in our graphical notation we label ports by colours and not by
port identifiers. From now on, we omit the colour of control ports, which is
always zero. As a reminder, control ports include ec-inports, ic-ports, ec-
outports and ec-inoutports.

In our theory, there is a distinguished trivial computon consisting of a
single ec-inoutport, which we refer to as the _unit computon_.

######  Definition 11 (Unit Computon).

Up to isomorphism, the _unit computon_ is a trivial computon with
$|P|=|\Sigma|=1$. We use $\Lambda$ to denote it.

The existence of $\Lambda$ can be proven by the fact that, according to
Definition 1, the set of ports and the set of colours are never empty. By the
same definition, we can observe that a computon can have no computation units
and no edges at all. It is easy to show that $\Lambda$ is unique up to unique
isomorphism.

Since a computon is required to have at least one coloured port, $\Lambda$ can
be perceived as the “simplest” object in $\textbf{Set}^{\textbf{Comp}}$. In
spite of this structural feature, $\Lambda$ is not an initial object in such a
category since there are $k\geq 1$ computon morphisms from it to any other
computon $\lambda$, where $k$ is the number of control ports in
$\lambda$.777This can be easily proved by induction on the number of control
ports of an arbitrary computon. Under this premise, it follows that
$\textbf{Set}^{\textbf{Comp}}$ has no initial objects.

##  5 Primitive Computons

Like a trivial computon, a primitive one has no i-ports. The difference is
that there is exactly one computation unit to which all ports are attached via
edges. So, every port can be either e-inport or e-outport, never both (see
Proposition 6). This entails that a primitive computon is connected; in other
words, it has neither dangling ports nor dangling computation units (see
Proposition 7). In this paper, we consider three classes of primitive
computons, namely _fork computons_ (see Subsection 5.1), _join computons_ (see
Subsection 5.2) and _functional computons_ (see Subsection 5.3).

######  Definition 12.

A primitive computon is a computon whose diagram in Set has the form:888We use
$1$ to denote a singleton set.

${E}$${1}$${P}$${\Sigma}$${F}$$\scriptstyle{\sigma}$$\scriptstyle{t}$$\scriptstyle{c}$$\scriptstyle{\tau}$$\scriptstyle{s}$

with $P=Im(s)\triangle Im(t)$ and $E\neq\emptyset\neq F$.

######  Proposition 6.

If $\lambda$ is a primitive computon, then ${P=P^{+}\triangle P^{-}}$.

###### Proof.

If $\lambda$ is a primitive computon, then ${p\in P\iff p\in Im(s)\triangle
Im(t)}$ (see Definition 12). Particularly:

  * 1.

If $p\in Im(s)\setminus Im(t)$, then $p\in P^{+}\setminus P^{-}$ because
${(\exists f\in F)[s(f)=p]}$ and ${(\nexists e\in E)[t(e)=p]}$.

  * 2.

If $p\in Im(t)\setminus Im(s)$, then $p\in P^{-}\setminus P^{+}$ because
${(\exists e\in E)[t(e)=p]}$ and ${(\nexists f\in F)[s(f)=p]}$.

By the above cases and by the definition of symmetric difference, we have that
${p\in P}\iff{p\in Im(s)\triangle Im(t)}\iff{p\in(P^{+}\setminus
P^{-})\cup(P^{-}\setminus P^{+})}\iff p\in P^{+}\triangle P^{-}$. Hence, we
conclude that ${P=Im(s)\triangle Im(t)=(P^{+}\setminus
P^{-})\cup(P^{-}\setminus P^{+})=P^{+}\triangle P^{-}}$, as required. ∎

######  Proposition 7.

Every primitive computon is a connected computon.

###### Proof.

Let $\lambda$ be a primitive computon and $p$ be an e-inport of $\lambda$. By
Definition 2, there is no $e_{1}\in E$ such that $t(e_{1})=p$ so that $p\notin
Im(t)$. Consequently, we have that that $p\in Im(s)$ because $P=Im(s)\triangle
Im(t)$. This implies that there exists some $f_{1}\in F$ where $s(f_{1})=p$.
If $u$ is the only computation unit in $U$, we have that $\tau(f_{1})=u$ by
the fact that $\tau$ is surjective. As $\sigma$ is also surjective, there
exists some $e_{2}\in E$ such that $\sigma(e_{2})=u$. By the totality of $t$,
it follows that there exists some $q\in P$ such that $t(e_{2})=q$ so that
$q\in Im(t)$. Again, by the property $P=Im(s)\triangle Im(t)$, we have that
$q\notin Im(s)$ so there is no $f_{2}\in F$ such that $s(f_{2})=q$, i.e.,
$q\in P^{-}$ by Definition 2. As $p\xrightarrow{*}q$ holds, we conclude that
$\lambda$ is a connected computon. ∎

###  5.1 Fork Computons

A fork computon has exactly one ec-inport and two ec-outports, i.e., it has no
data ports at all. Intuitively, it just duplicates the control received in its
ec-inport into all its ec-outports.

######  Definition 13.

A fork computon $\lambda$ is a primitive computon with $|E|=2$ and
$|F|=|\Sigma|=1$.

From Definition 13, it is easy to deduce that a fork computon $\lambda$ has
exactly three ports because ${P=Im(s)\triangle Im(t)}$, ${|E|=2}$ and
${|F|=1}$. Specifically, ${|P^{-}|=2}$ and ${|P^{+}|=1}$ because
${P=P^{+}\triangle P^{-}}$ (see Definition 2 and Proposition 6). As
$|\Sigma|=1$ and $c$ is total and ${Q^{+}\neq\emptyset\neq Q^{-}}$ (see
Definition 1), the set of colours of $\lambda$ is $\\{0\\}$ so ${c(p)=0}$ for
all ${p\in P}$. The general structure of a fork computon and its equivalent
Petri net representation are depicted in Figure 3.

$0$$0$$0$ (a) Petri net syntax. (b) Computon syntax.

Computation unitControl flow edgeEc-inportEc-outport

Figure 3: Syntactic representations of a fork computon.

###  5.2 Join Computons

A join computon can be thought of as the dual of a fork computon since it has
exactly two ec-inports and one ec-outport. Intuitively, it merges the control
received in its ec-inports into its unique ec-outport.

######  Definition 14.

A join computon $\lambda$ is a primitive computon with $|E|=|\Sigma|=1$ and
$|F|=2$.

The properties of a join computon $\lambda$ are almost identical to that of a
fork computon so it is true that $c(p)=0$ for all $p\in P$. The only
difference is in terms of the number of ec-inports and ec-outports. The
general structure of a join computon and its equivalent Petri net
representation are depicted in Figure 4.

$0$$0$$0$ (a) Petri net syntax. (b) Computon syntax.

Computation unitControl flow edgeEc-inportEc-outport

Figure 4: Syntactic representations of a join computon.

###  5.3 Functional Computons

A functional computon has exactly one ec-inport, one ec-outport, any number of
ed-inports and any number of ed-outports. Intuitively, the unique computation
unit is a high-level representation of a (potentially halting) computation
that is triggered after receiving a control signal and a number of input data
values. The successful termination of such computation results in a single
control signal and a number of output data values.

######  Definition 15.

A functional computon $\lambda$ is a primitive computon with $|E|,|F|\geq 1$
such that $\exists!p\in P^{+}[c(p)=0]$ and $\exists!q\in P^{-}[c(q)=0]$.

The general structure of a functional computon with $i$ ed-inports and $j$ ed-
outports, together with its equivalent Petri net representation, are
illustrated in Figure 5.999We acknowledge that the definition of a computon
does not include labels for computation units. However, for increased clarity,
we took the liberty of using the symbol of a functional computon for labelling
its unique computation unit.

$0$$c(p_{1})$$\vdots$$c(p_{i})$$0$$c(q_{1})$$\vdots$$c(q_{j})$ (a) Petri net
syntax. $\lambda$$c(p_{1})$$\vdots$$c(p_{i})$$c(q_{1})$$\vdots$$c(q_{j})$ (b)
Computon syntax.

Computation unitControl flow edgeEc-inportEc-outportData flow edgeEd-inportEd-
outport

Figure 5: Syntactic representations of a functional computon $\lambda$ with
${p_{1},\ldots,p_{i}\in D^{+}}$ and ${q_{1},\ldots,q_{j}\in D^{-}}$.

Up to isomorphism, there is a particular functional computon which possesses
only one ec-inport and only one ec-outport. This sort of computon, referred to
as _the glue computon_ , is explicitly defined when $|E|=|F|=1$. Intuitively,
its behaviour is akin to a “do nothing” function because it just echoes the
control signal received in its unique ec-inport into its only ec-outport.

##  6 Composite Computons

A composite computon is algebraically formed via a composition operator which
defines control flow for the execution of sub-computons (i.e., operands) in
some order. As a composite cannot be a sub-computon of itself, such operators
enable control-based exogenous composition [17]. Exogenous means that the
composition process is done outside the internal structure of sub-computons
and entails that sub-computons are agnostic of the composition structure built
upon them.

More formally, a composite computon is canonically the colimit of other
computons, and it is constructed via a composition operator. A composition
operator defines a certain operation in $\textbf{Set}^{\textbf{Comp}}$,
depending on the composite being constructed. In this paper, we provide
operators to form either sequential or parallel computons.

###  6.1 Sequential Computons

Sequential composition is an operation that we characterise as a particular
pushout in $\textbf{Set}^{\textbf{Comp}}$. It is particular because,
intuitively, the common object needs to be a trivial computon $\lambda_{0}$
that can be “embedded” into some or all the e-outports of a computon
$\lambda_{1}$ and into some or all the e-inports of a computon $\lambda_{2}$.
Particularly, every port $p_{0}\in P_{0}$ that is embedded into an outport
$p_{1}\in P_{1}^{-}$ needs to be embedded into an inport $p_{2}\in P_{2}^{+}$
and viceversa. This restriction enables a strict sequence in which
$\lambda_{1}$ is computed before $\lambda_{2}$. A converse computation is
possible and requires a different embedding since sequencing is a non-
commutative operation in which order matters. To compute $\lambda_{2}$ before
$\lambda_{1}$, it suffices to reverse the way we insert $\lambda_{0}$ into
$\lambda_{1}$ and into $\lambda_{2}$.

Before providing the formal definition of a sequential computon, it is
necessary to introduce the general notion of a pushout construction in
$\textbf{Set}^{\textbf{Comp}}$ (see Definition 16), which can be computed if
and only if there is a pushable span of computon morphisms (see Definition 17
and Proposition 8).

######  Definition 16 (Pushout Construction).

Given a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms, the pushout of the corresponding diagram in
$\textbf{Set}^{\textbf{Comp}}$:

${\lambda_{0}}$${\lambda_{1}}$${\lambda_{2}}$${\lambda_{3}}$$\scriptstyle{\alpha_{1}}$$\scriptstyle{\alpha_{2}}$$\scriptstyle{\beta_{1}}$$\scriptstyle{\beta_{2}}$

denoted
${(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})}$,
is obtained by computing the pushout in Set of each individual computon
component:

$P_{3}=P_{1}+_{P_{0}}P_{2}$ $U_{3}=U_{1}+_{U_{0}}U_{2}$
$E_{3}=E_{1}+_{E_{0}}E_{2}$ $F_{3}=F_{1}+_{F_{0}}F_{2}$
$\Sigma_{3}=\Sigma_{1}+_{\Sigma_{0}}\Sigma_{2}$

with $\sigma_{3}$, $\tau_{3}$, $s_{3}$, $t_{3}$ and $c_{3}$ being defined in
the obvious way:

$\sigma_{3}:E_{1}+_{E_{0}}E_{2}\twoheadrightarrow U_{1}+_{U_{0}}U_{2}$
$\tau_{3}:F_{1}+_{F_{0}}F_{2}\twoheadrightarrow U_{1}+_{U_{0}}U_{2}$
$s_{3}:F_{1}+_{F_{0}}F_{2}\rightarrow P_{1}+_{P_{0}}P_{2}$
$t_{3}:E_{1}+_{E_{0}}E_{2}\rightarrow P_{1}+_{P_{0}}P_{2}$
$c_{3}:P_{1}+_{P_{0}}P_{2}\twoheadrightarrow\Sigma_{1}+_{\Sigma_{0}}\Sigma_{2}$

######  Definition 17 (Pushable Span).

A span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms is pushable if
${\alpha_{1}(\vec{i}(\alpha_{2}))\cup\alpha_{1}(\vec{o}(\alpha_{2}))\subseteq
P_{1}^{+}\cup P_{1}^{-}}$ and
${\alpha_{2}(\vec{i}(\alpha_{1}))\cup\alpha_{2}(\vec{o}(\alpha_{1}))\subseteq
P_{2}^{+}\cup P_{2}^{-}}$.

######  Proposition 8.

Let ${\alpha_{1}:\lambda_{0}\rightarrow\lambda_{1}}$ and
${\alpha_{2}:\lambda_{0}\rightarrow\lambda_{2}}$ be computon morphisms. The
pushout
${(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})}$
of ${\alpha_{1}}$ and ${\alpha_{2}}$ exists $\iff$
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
is pushable.

###### Proof.

${(\implies)}$ Assuming that the pushout
${(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})}$
of ${\alpha_{1}:\lambda_{0}\rightarrow\lambda_{1}}$ and
${\alpha_{2}:\lambda_{0}\rightarrow\lambda_{2}}$ exists in
${\textbf{Set}^{\textbf{Comp}}}$, we just prove that
${\alpha_{1}(\vec{i}(\alpha_{2}))\subseteq P_{1}^{+}\cup P_{1}^{-}}$. This is
because the satisfaction of the other conditions of Definition 17 follows
analogously.

Supposing there is some
${p_{1}\in\alpha_{1}(\vec{i}(\alpha_{2}))\setminus(P_{1}^{+}\cup P_{1}^{-})}$,
we know there is a port ${p_{0}\in\vec{i}(\alpha_{2})}$ such that
${\alpha_{1}(p_{0})=p_{1}}$. As the pushout
${(\beta_{1},\lambda_{3},\beta_{2})}$ exists in
$\textbf{Set}^{\textbf{Comp}}$, the equation
$\beta_{1}(\alpha_{1}(p_{0}))=\beta_{1}(p_{1})=\beta_{2}(\alpha_{2}(p_{0}))$
holds. Since ${p_{0}\in\vec{i}(\alpha_{2})}$, there is some
${u_{2}\in\bullet\alpha_{2}(p_{0})\setminus\alpha_{2}(\bullet p_{0})}$ so that
${\beta_{1}(p_{1})=\beta_{2}(\alpha_{2}(p_{0}))\in\beta_{2}(u_{2})\bullet}$.
As ${p_{1}\notin P_{1}^{+}\cup P_{1}^{-}}$, ${p_{1}\notin\vec{i}(\beta_{1})}$
(see Definition 7), meaning that there is some ${u_{1}\in\bullet p_{1}}$ where
${\beta_{1}(u_{1})=\beta_{2}(u_{2})}$. Using commutativity, we deduce the
existence of ${u_{0}\in U_{0}}$ such that ${\alpha_{1}(u_{0})=u_{1}}$ and
${\alpha_{2}(u_{0})=u_{2}}$. As this contradicts the fact that
${u_{2}\in\bullet\alpha_{2}(p_{0})\setminus\alpha_{2}(\bullet p_{0})}$, we
conclude that ${\alpha_{1}(\vec{i}(\alpha_{2}))\subseteq P_{1}^{+}\cup
P_{2}^{-}}$.

${(\impliedby)}$ Assuming
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
is a pushable span of computon morphisms (as per Definition 17), we prove that
the pushout
${(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})}$
of ${\alpha_{1}}$ and ${\alpha_{2}}$ can be constructed via Definition 16. For
this, we first prove that ${\beta_{1}}$ and ${\beta_{2}}$ are computon
morphisms. Below we provide the proof for ${\beta_{1}}$ only, since the other
one is completely analogous.

As Set has all pushouts, the existence of each component of ${\beta_{1}}$ and
${\beta_{2}}$ can be directly deduced. For example, the
${\beta_{1}}$-component injecting ports of ${P_{1}}$ into ${P_{3}}$ exists
because ${P_{3}=P_{1}+_{P_{0}}P_{2}}$ can always be computed in Set.
Consequently, the equations ${\beta_{i}\circ c_{1}=c_{3}\circ\beta_{i}}$,
${\beta_{i}\circ\tau_{1}=\tau_{3}\circ\beta_{i}}$,
${\beta_{i}\circ\sigma_{1}=\sigma_{3}\circ\beta_{i}}$, ${\beta_{i}\circ
s_{1}=s_{3}\circ\beta_{i}}$ and ${\beta_{i}\circ t_{1}=t_{3}\circ\beta_{i}}$
hold for $i=1,2$ (see the commutative diagrams of Definition 7).

To prove that the ${\Sigma}$-component of ${\beta_{1}}$ is an inclusion
function, we note that ${\Sigma_{0}=\Sigma_{1}\cap\Sigma_{2}}$ because
${\Sigma_{0},\Sigma_{1},\Sigma_{2}\subset\mathbb{N}}$ and because the
${\Sigma}$-components of ${\alpha_{1}}$ and ${\alpha_{2}}$ are both inclusion
functions (see Definition 7). This means that the pushout
${\Sigma_{1}+_{\Sigma_{0}}\Sigma_{2}}$ can be canonically identified with
${\Sigma_{1}\cup\Sigma_{2}\subset\mathbb{N}}$ and, consequently, that the
induced total function
${f:\Sigma_{1}\rightarrow\Sigma_{1}+_{\Sigma_{0}}\Sigma_{2}}$ (which
corresponds to the ${\Sigma}$-component of ${\beta_{1}}$) is an inclusion
function. That is, ${f(x)=x}$ for all ${x\in\Sigma_{1}}$. We now show that
${\vec{i}(\beta_{1})\cup\vec{o}(\beta_{1})\subseteq P_{1}^{+}\cup P_{1}^{-}}$
also holds.

If ${p_{1}\in\vec{i}(\beta_{1})}$ then
${\bullet\beta_{1}(p_{1})\setminus\beta_{1}(\bullet p_{1})\neq\emptyset}$ so
there exists some ${u_{3}\in\bullet\beta_{1}(p_{1})\setminus\beta_{1}(\bullet
p_{1})}$ and no ${u_{1}\in\bullet p_{1}}$ where ${\beta_{1}(u_{1})=u_{3}}$.
Since ${U_{3}=U_{1}+_{U_{0}}U_{2}}$ (by Definition 16), there must be some
${u_{2}\in U_{2}}$ where
${\beta_{2}(u_{2})=u_{3}\in\bullet\beta_{1}(p_{1})\setminus\beta_{1}(\bullet
p_{1})}$ and, consequently, some ${e_{3}\in E_{3}}$ where
${\beta_{2}(u_{2})\xrightarrow{e_{3}}\beta_{1}(p_{1})}$ (see Definition 5). As
there is no ${e_{1}\in E_{1}}$ satisfying
$\beta_{1}(\sigma_{1}(e_{1}))=\sigma_{3}(\beta_{1}(e_{1}))=\sigma_{3}(e_{3})=u_{3}$
because there is no ${u_{1}\in U_{1}}$ satisfying ${\beta_{1}(u_{1})=u_{3}}$,
${E_{3}=E_{1}+_{E_{0}}E_{2}}$ implies that there must be some ${e_{2}\in
E_{2}}$ for which ${\beta_{2}(e_{2})=e_{3}}$ is true. As
${\beta_{2}(u_{2})\xrightarrow{\beta_{2}(e_{2})}\beta_{1}(p_{1})}$ holds, we
use the commutativity property to deduce the existence of ${p_{2}\in P_{2}}$
such that ${\beta_{2}(p_{2})=\beta_{1}(p_{1})}$ and $u_{2}\in\bullet p_{2}$.
As ${\beta_{2}(p_{2})=\beta_{1}(p_{1})}$ and ${P_{3}=P_{1}+_{P_{0}}P_{2}}$, we
use again commutativity to deduce that there is also a port ${p_{0}\in P_{0}}$
with ${\alpha_{1}(p_{0})=p_{1}}$ and ${\alpha_{2}(p_{0})=p_{2}}$ so that
${u_{2}\in\bullet\alpha_{2}(p_{0})}$. Since ${U_{3}=U_{1}+_{U_{0}}U_{2}}$ and
${(\nexists u_{1}\in U_{1})[\beta_{1}(u_{1})=u_{3}=\beta_{2}(u_{2})]}$, we
have that there is no ${u_{0}\in U_{0}}$ where ${\alpha_{2}(u_{0})=u_{2}}$.
That is, ${u_{2}\notin\alpha_{2}(\bullet p_{0})}$ because ${\bullet
p_{0}\subseteq U_{0}}$. Thus, it is true that
${u_{2}\in\bullet\alpha_{2}(p_{0})\setminus\alpha_{2}(\bullet p_{0})}$ and,
therefore, that ${p_{0}\in\vec{i}(\alpha_{2})}$ (see Definition 7).

Since ${\alpha_{1}(\vec{i}(\alpha_{2}))\subseteq P_{1}^{+}\cup P_{1}^{-}}$ (by
Definition 17) and ${p_{0}\in\vec{i}(\alpha_{2})}$ (by the above), we have
that ${\alpha_{1}(p_{0})=p_{1}\in P_{1}^{+}\cup P_{1}^{-}}$. A similar
approach can be used to show that ${q_{1}\in\vec{o}(\beta_{1})}$ implies
$q_{1}\in P_{1}^{+}\cup P_{1}^{-}$. So,
${\vec{i}(\beta_{1})\cup\vec{o}(\beta_{1})\subseteq P_{1}^{+}\cup P_{1}^{-}}$.

Having proved that ${\beta_{1}}$ is a computon morphism, we now assume that
${\gamma_{1}:\lambda_{1}\rightarrow\lambda_{4}}$ and
${\gamma_{2}:\lambda_{2}\rightarrow\lambda_{4}}$ are computon morphisms with
${\gamma_{1}\circ\alpha_{1}=\gamma_{2}\circ\alpha_{2}}$, in order to show that
there is a unique computon morphism
${\gamma_{3}:\lambda_{3}\rightarrow\lambda_{4}}$ such that the corresponding
diagram commutes. As it is obvious that the ${\Sigma}$-component of
${\gamma_{3}}$ is an inclusion function because ${\beta_{i}}$ and
${\gamma_{i}}$ are (for $i=1,2$) and because
${\Sigma_{3}=\Sigma_{1}\cup\Sigma_{2}}$, we just prove that
${\vec{i}(\gamma_{3})\cup\vec{o}(\gamma_{3})\subseteq P_{3}^{+}\cup
P_{3}^{-}}$.

Let ${p_{3}\in\vec{i}(\gamma_{3})}$ so
${\bullet\gamma_{3}(p_{3})\setminus\gamma_{3}(\bullet p_{3})\neq\emptyset}$.
As ${P_{3}=P_{1}+_{P_{0}}P_{2}}$, we observe that ${p_{3}=\beta_{j}(p_{j})}$
for some ${p_{j}\in P_{j}}$ and ${j=1,2}$. With this in mind, we perform the
following operations:

$\displaystyle\emptyset$
$\displaystyle\neq\bullet\gamma_{3}(p_{3})\setminus\gamma_{3}(\bullet
p_{3})=\bullet\gamma_{3}(\beta_{j}(p_{j}))\setminus\gamma_{3}(\bullet\beta_{j}(p_{j}))$
$\displaystyle\hskip
94.17854pt=\bullet\gamma_{j}(p_{j})\setminus\gamma_{3}(\bullet\beta_{j}(p_{j}))\hskip
28.45274pt\text{because }\gamma_{3}\circ\beta_{j}=\gamma_{j}$
$\displaystyle\hskip
94.17854pt\subseteq\bullet\gamma_{j}(p_{j})\setminus\gamma_{3}(\beta_{j}(\bullet
p_{j}))\hskip 25.6073pt\text{ because }\beta_{j}(\bullet
p_{j})\subseteq\bullet\beta_{j}(p_{j})$ $\displaystyle\hskip
94.17854pt=\bullet\gamma_{j}(p_{j})\setminus\gamma_{j}(\bullet p_{j})\hskip
48.36958pt\text{because }\gamma_{3}\circ\beta_{j}=\gamma_{j}$

By the above, we deduce that ${p_{j}\in\vec{i}(\gamma_{j})}$ and,
consequently, that ${p_{j}\in P_{j}^{+}\cup P_{j}^{-}}$ (because $\gamma_{j}$
is a computon morphism with ${\vec{i}(\gamma_{j})\subseteq P_{j}^{+}\cup
P_{j}^{-}}$ — see Definition 7). Using the facts
${p_{3}=\beta_{j}(p_{j})\in\vec{i}(\gamma_{3})}$ and ${p_{j}\in P_{j}^{+}\cup
P_{j}^{-}}$, we further deduce that ${\beta_{j}^{-1}(p_{3})\subseteq
P_{j}^{+}\cup P_{j}^{-}}$. Hence, $p_{3}\in P_{3}^{+}\cup P_{3}^{-}$ by
Proposition 2. The proof that $q_{3}\in\vec{o}(\gamma_{3})\implies q_{3}\in
P_{3}^{+}\cup P_{3}^{-}$ is completely analogous.

As the $\Sigma$-component of $\gamma_{3}$ is an inclusion function and
$\vec{i}(\gamma_{3})\cup\vec{o}(\gamma_{3})\subseteq P_{3}^{+}\cup P_{3}^{-}$,
we conclude that $\gamma_{3}$ is a computon morphism. Such a morphism is
unique because each of its components are unique (by the fact that a pushout
in Set satisfies the universal property). ∎

Evidently, ${\textbf{Set}^{\textbf{Comp}}}$ does not have all pushouts because
a span must meet the requirements imposed by Definition 17 to enable square
completion. Nevertheless, when there is such a span whose legs are connected
computons, the respective pushout operation results in another connected
computon (see Proposition 9).

######  Proposition 9.

Let
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
be a pushable span of computon morphisms. If $\lambda_{1}$ and $\lambda_{2}$
are connected computons, then the pushout of $\alpha_{1}$ and $\alpha_{2}$
yields a connected computon.

###### Proof.

Let
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
be a pushable span of computon morphisms and assume that ${\lambda_{1}}$ and
${\lambda_{2}}$ are connected computons. By Proposition 8,
${(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})}$
can be constructed from ${\alpha_{1}}$ and ${\alpha_{2}}$.

To prove that ${\lambda_{3}}$ is a connected computon, it suffices to show
that ${p_{3}\xrightarrow{*}q_{3}}$ holds for some e-inport ${p_{3}\in
P_{3}^{+}}$ and for some e-outport ${q_{3}\in P_{3}^{-}}$. By Proposition 2
and by the fact that ${P_{3}=P_{1}+_{P_{0}}P_{2}}$, we know that there is some
${p_{i}\in P_{i}^{+}}$ and some ${q_{j}\in P_{j}^{-}}$ where
${\beta_{i}(p_{i})=p_{3}}$ and ${\beta_{j}(q_{j})=q_{3}}$ such that
${i,j\in\\{1,2\\}}$.

  * 1.

If ${i=j}$, then ${p_{i}\xrightarrow{*}q_{j}}$ trivially holds because
${\lambda_{1}}$ and ${\lambda_{2}}$ are connected computons. By the
commutativity property, ${\beta_{i}(p_{i})\xrightarrow{*}\beta_{j}(q_{j})}$
also holds.

  * 2.

If ${i\neq j}$, then ${\beta_{i}(p_{i})\xrightarrow{*}\beta_{j}(q_{j})}$
follows from the connectivity of $\lambda_{1}$ and $\lambda_{2}$ and from the
fact that there is always a port ${p_{0}\in\\{p\in P_{0}\mid c_{0}(p)=0\\}}$
where ${\beta_{1}(\alpha_{1}(p_{0}))=\beta_{2}(\alpha_{2}(p_{0}))}$.

As ${p_{3}\xrightarrow{*}q_{3}}$ is true in both cases, we conclude that
${\lambda_{3}}$ is a connected computon. ∎

######  Definition 18 (Sequential Computon).

Let
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
be a span of computon morphisms. We say that the pushout of $\alpha_{1}$ and
$\alpha_{2}$ yields a _sequential computon_ if and only if (i) $\lambda_{0}$
is a trivial computon with
${P_{0}=\vec{i}(\alpha_{1})\cap\vec{o}(\alpha_{2})}$, (ii) $\lambda_{1}$ and
$\lambda_{2}$ are connected computons, (iii)
${\alpha_{1}(\vec{o}(\alpha_{2}))\subseteq P_{1}^{-}}$ and (iv)
${\alpha_{2}(\vec{i}(\alpha_{1}))\subseteq P_{2}^{+}}$.

######  Proposition 10.

If a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms produces a sequential computon, then it is pushable.

###### Proof.

If
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
is a span of computon morphisms that produces a sequential computon (see
Definition 18), ${p_{0}\in P_{0}\implies
p_{0}\in\vec{i}(\alpha_{1})\cap\vec{o}(\alpha_{2})}$ so ${\alpha_{1}(p_{0})\in
P_{1}^{-}}$ and ${\alpha_{2}(p_{0})\in P_{2}^{+}}$. That is,
${\alpha_{1}(p_{0})\bullet=\emptyset=\bullet\alpha_{2}(p_{0})}$. As
${p_{0}\bullet=\emptyset=\bullet p_{0}}$ (because ${\lambda_{0}}$ is a trivial
computon), it follows that
${\alpha_{1}(p_{0})\bullet\setminus\alpha_{1}(p_{0}\bullet)=\emptyset=\bullet\alpha_{2}(p_{0})\setminus\alpha_{2}(\bullet
p_{0})}$, meaning that
${p_{0}\notin\vec{o}(\alpha_{1})\cup\vec{i}(\alpha_{2})}$ and, hence,
${\vec{o}(\alpha_{1})\cup\vec{i}(\alpha_{2})=\emptyset}$. For
${j\in\\{1,2\\}}$, we observe that ${P_{j}^{+}\neq\emptyset\neq P_{j}^{-}}$
(by Definition 1) and that ${\lambda_{j}}$ is not a trivial computon because
it is a connected computon (see Proposition 1). Thus,
${\alpha_{1}(\vec{i}(\alpha_{2}))\cup\alpha_{1}(\vec{o}(\alpha_{2}))\subseteq
P_{1}^{-}\subset P_{1}^{+}\cup P_{1}^{-}}$ and
${\alpha_{2}(\vec{i}(\alpha_{1}))\cup\alpha_{2}(\vec{o}(\alpha_{1}))\subseteq
P_{2}^{+}\subset P_{2}^{+}\cup P_{2}^{-}}$. ∎

######  Corollary 1.

If a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms produces a sequential computon, then
${\vec{o}(\alpha_{1})\cup\vec{i}(\alpha_{2})=\emptyset}$.

###### Proof.

The proof follows from Proposition 10. ∎

######  Remark 3.

Given a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms satisfying the conditions of Definition 18, we call
$\lambda_{0}$ the apex computon, $\lambda_{1}$ the left operand and
$\lambda_{2}$ the right operand.

When an apex computon is embedded into all the e-outports of the left operand
and into all the e-inports of the right one, we say that the computon operands
are totally sequentiable; otherwise, we say that they are partially
sequentiable (see Definition 19). By Proposition 11, total sequentiality
implies partial sequentiality.

######  Definition 19 (Total and Partial Sequential Composition).

Let
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
be a pushable span of computon morphisms whose pushout forms a sequential
computon. We say that $\lambda_{1}$ is totally sequentiable with
$\lambda_{2}$, written ${\lambda_{1}\unrhd\lambda_{2}}$, if
$\alpha_{1}(\vec{o}(\alpha_{2}))=P_{1}^{-}$ and
$\alpha_{2}(\vec{i}(\alpha_{1}))=P_{2}^{+}$. If
$\alpha_{1}(\vec{o}(\alpha_{2}))\subset P_{1}^{-}$ or
$\alpha_{2}(\vec{i}(\alpha_{1}))\subset P_{2}^{+}$, then $\lambda_{1}$ is
partially sequentiable with $\lambda_{2}$, written
$\lambda_{1}\rhd\lambda_{2}$.

######  Proposition 11.

If there is a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms where $\lambda_{1}\unrhd\lambda_{2}$, there is a span of
the form ${\lambda_{1}\leftarrow\lambda\rightarrow\lambda_{2}}$ where
$\lambda_{1}\rhd\lambda_{2}$.

###### Proof.

Let
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
be a span of computon morphisms where ${\lambda_{1}\unrhd\lambda_{2}}$. Since
$\lambda_{0}$ is required to have at least one ec-inoutport (see Definition
1), we know that there exists at least one computon morphism
${\alpha_{0}:\Lambda\rightarrow\lambda_{0}}$ where ${\alpha_{0}(p)\in
P_{0}}\iff{\alpha_{0}(p)\in\vec{i}(\alpha_{1})\cap\vec{o}(\alpha_{2})}$ (see
Definitions 18 and 19). Consequently, a span
${\lambda_{1}\xleftarrow{\alpha_{1}\circ\alpha_{0}}\Lambda\xrightarrow{\alpha_{2}\circ\alpha_{0}}\lambda_{2}}$
exists.

As ${\alpha_{0}(p)\in\vec{o}(\alpha_{2})}$ and
${\alpha_{1}(\vec{o}(\alpha_{2}))=P_{1}^{-}}$ (because
${\lambda_{1}\unrhd\lambda_{2}}$), we have that ${\alpha_{1}(\alpha_{0}(p))\in
P_{1}^{-}}$. The fact that ${\lambda_{1}}$ is a connected computon implies
that there exists some computation unit
${u_{1}\in\bullet\alpha_{1}(\alpha_{0}(p))}$ so that
${\bullet\alpha_{1}(\alpha_{0}(p))\neq\emptyset}$ (see Proposition 1). As
${\bullet p=\emptyset}$ because $\Lambda$ is a trivial computon,
${\bullet\alpha_{1}(\alpha_{0}(p))\setminus\alpha_{1}(\alpha_{0}(\bullet
p))\neq\emptyset}$ holds, meaning that
${p\in\vec{i}(\alpha_{1}\circ\alpha_{0})}$ (see Definition 7). A similar
reasoning can be used to deduce ${\alpha_{2}(\alpha_{0}(p))\in P_{2}^{+}}$ and
${p\in\vec{o}(\alpha_{2}\circ\alpha_{0})}$.

The facts ${\alpha_{1}(\alpha_{0}(p))\in P_{1}^{-}}$ and
${p\in\vec{o}(\alpha_{2}\circ\alpha_{0})}$ together imply that
${\alpha_{1}(\alpha_{0}(\vec{o}(\alpha_{2}\circ\alpha_{0})))\subseteq
P_{1}^{-}}$. Similarly, ${\alpha_{2}(\alpha_{0}(p))\in P_{2}^{+}}$ and
${p\in\vec{i}(\alpha_{1}\circ\alpha_{0})}$ imply that
${\alpha_{2}(\alpha_{0}(\vec{i}(\alpha_{1}\circ\alpha_{0})))\subseteq
P_{2}^{+}}$. Consequently, as
${\vec{i}(\alpha_{2}\circ\alpha_{0})=\emptyset=\vec{o}(\alpha_{1}\circ\alpha_{0})}$
because
${\bullet\alpha_{2}(\alpha_{0}(p))=\alpha_{1}(\alpha_{0}(p))\bullet=\bullet
p=p\bullet=\emptyset}$, we have that the span
${\lambda_{1}\xleftarrow{\alpha_{1}\circ\alpha_{0}}\Lambda\xrightarrow{\alpha_{2}\circ\alpha_{0}}\lambda_{2}}$
is pushable (see Definition 17). Now:

  1. 1.

If ${|P_{1}^{-}|=1}$ then
${\alpha_{1}(\alpha_{0}(\vec{o}(\alpha_{2}\circ\alpha_{0})))=P_{1}^{-}}$
because ${|P|=1}$. As every set is a subset of itself,
${\alpha_{1}(\alpha_{0}(\vec{o}(\alpha_{2}\circ\alpha_{0})))\subset
P_{1}^{-}}$.

  2. 2.

If ${|P_{1}^{-}|>1}$ then
${\alpha_{1}(\alpha_{0}(\vec{o}(\alpha_{2}\circ\alpha_{0})))\subset
P_{1}^{-}}$ because ${\alpha_{1}\circ\alpha_{0}}$ is monic and ${|P|=1}$.

  3. 3.

Analogously, if ${|P_{2}^{+}|\geq 1}$, then
${\alpha_{2}(\alpha_{0}(\vec{i}(\alpha_{1}\circ\alpha_{0})))\subset
P_{2}^{+}}$.

The pushout of ${\alpha_{1}\circ\alpha_{0}}$ and ${\alpha_{2}\circ\alpha_{0}}$
can always be computed because the span they form is pushable (see Proposition
8). As it satisfies the requirements for partial sequentiality too (see
(1)-(3) and Definition 19), we conclude that it forms a sequential computon
with ${\lambda_{1}\rhd\lambda_{2}}$. ∎

Any computon operand can be put in any order within a sequential computon,
since control e-inports and control e-outports always possess the same colour
(i.e., zero). This property, combined with the fact that a computon always has
at least one ec-inport and at least one ec-outport, allow us to compose any
two connected computons sequentially regardless of the data they require or
produce (see Theorem 1). Composing two connected computons sequentially
results in another connected computon (see Proposition 12).

######  Theorem 1.

Let $\lambda_{1}$ and $\lambda_{2}$ be two computons. Then,
${\lambda_{1}\rhd\lambda_{2}}$ $\iff$ $\lambda_{1}$ and $\lambda_{2}$ are
connected computons.

###### Proof.

$(\implies)$ This part of the proof follows directly from Definition 18.

$(\impliedby)$ Assuming that $\lambda_{1}$ and $\lambda_{2}$ are connected
computons, we first prove that there exists a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms whose pushout forms a sequential computon. For this, we
choose $\lambda_{0}$ to be $\Lambda$ which is a trivial computon with a unique
port $p\in P^{+}\cap P^{-}$ and $c(p)=0$ (see Definition 11). Below we
construct computon morphisms $\alpha_{1}:\Lambda\rightarrow\lambda_{1}$ and
$\alpha_{2}:\Lambda\rightarrow\lambda_{2}$ by only considering port injection
because ${E=F=U=\emptyset}$ and ${\Sigma=\\{0\\}}$.

Since any computon has at least one ec-inport and at least one ec-outport, we
have that $Q_{1}^{-}\neq\emptyset\neq Q_{2}^{+}$. If we trivially define
$\alpha_{1}(p)=p_{1}\in Q_{1}^{-}$ and $\alpha_{2}(p)=p_{2}\in Q_{2}^{+}$, we
have that $p\in\vec{i}(\alpha_{1})\cap\vec{o}(\alpha_{2})$ because
$\lambda_{1}$ and $\lambda_{2}$ are connected computons (see Proposition 1).
As $P=\\{p\\}$, $P=\vec{i}(\alpha_{1})\cap\vec{o}(\alpha_{2})$ so that
$\alpha_{1}(\vec{o}(\alpha_{2}))\subseteq Q_{1}^{-}\subseteq P_{1}^{-}$ and
$\alpha_{2}(\vec{i}(\alpha_{1}))\subseteq Q_{2}^{+}\subseteq P_{2}^{+}$. The
equation ${\bullet\alpha_{2}(p)=\alpha_{1}(p)\bullet=\bullet
p=p\bullet=\emptyset}$ allow us to determine that
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
is pushable. Since $\Lambda$ is a trivial computon, we deduce that the pushout
of $\alpha_{1}$ and $\alpha_{2}$ forms a sequential computon.

If ${\alpha_{1}(\vec{o}(\alpha_{2}))\subset Q_{1}^{-}}$ then
${\alpha_{1}(\vec{o}(\alpha_{2}))\subset P_{1}^{-}}$ because
${Q_{1}^{-}\subseteq P_{1}^{-}}$. Similarly,
${\alpha_{2}(\vec{i}(\alpha_{1}))\subset Q_{2}^{+}}$ implies
${\alpha_{2}(\vec{i}(\alpha_{1}))\subset P_{2}^{+}}$ because
${Q_{2}^{+}\subseteq P_{2}^{+}}$. Thus, ${\lambda_{1}\rhd\lambda_{2}}$ holds
in both cases. Now, when $\alpha_{1}(\vec{o}(\alpha_{2}))=Q_{1}^{-}$, we have
two possibilities: ${Q_{1}^{-}\subset P_{1}^{-}}$ or ${Q_{1}^{-}=P_{1}^{-}}$.
If ${Q_{1}^{-}\subset P_{1}^{-}}$, then
${\alpha_{1}(\vec{o}(\alpha_{2}))\subset P_{1}^{-}}$ so that
${\lambda_{1}\rhd\lambda_{2}}$ holds. A similar approach can be used to prove
that ${\lambda_{1}\rhd\lambda_{2}}$ is true when both
${\alpha_{2}(\vec{i}(\alpha_{1}))=Q_{2}^{+}}$ and ${Q_{2}^{+}\subset
P_{2}^{+}}$ are true.

The only scenario in which $\lambda_{1}\unrhd\lambda_{2}$ holds is when
$\lambda_{1}$ posesses only one ec-outport with no ed-outports and
$\lambda_{2}$ has only one ec-inport with no ed-inports. More precisely,
$\lambda_{1}\unrhd\lambda_{2}$ holds when
$\alpha_{1}(\vec{o}(\alpha_{2}))=Q_{1}^{-}=P_{1}^{-}$ and
$\alpha_{2}(\vec{i}(\alpha_{1}))=Q_{2}^{+}=P_{1}^{+}$. As Proposition 11
states that $\lambda_{1}\unrhd\lambda_{2}\implies\lambda_{1}\rhd\lambda_{2}$,
we conclude that for every pair $(\lambda_{1},\lambda_{2})$ of connected
computons, $\lambda_{1}\rhd\lambda_{2}$ holds. ∎

######  Proposition 12.

A sequential computon is a connected computon.

###### Proof.

The proof follows directly from Proposition 9 and Definition 18. ∎

Theorem 1 is important for our theory since it entails that any two connected
computons can always be composed sequentially. Although an apex computon
always exists, it is important to note that it does not need to correspond to
the entire common part between the e-outports of the left operand and the
e-inports of the right operand. By common, we mean ports sharing the same
colour. Figure 6 depicts a scenario of this sort.

$3$$\alpha_{1}$$\alpha_{2}$$\lambda_{1}$$1$$2$$3$$4$$\beta_{1}$$\beta_{2}$$\lambda_{2}$$3$$4$$5$$3$$\lambda_{1}$$1$$2$$4$$\lambda_{2}$$4$$5$
(a)

Computation unitControl flow edgeEc-inportEc-outportData flow edgeEd-inportEd-
outport

Figure 6: Constructing a sequential computon from a span
${\lambda_{1}\xleftarrow{\alpha_{1}}\lambda_{0}\xrightarrow{\alpha_{2}}\lambda_{2}}$
of computon morphisms where $\lambda_{1}\rhd\lambda_{2}$.

Figure 6 shows that, when a computon $\lambda_{1}$ is partially composed with
a computon $\lambda_{2}$, there is an implicit effect in which all the
e-outports of $\lambda_{1}$ that are not in the image of $\alpha_{1}$ become
e-outports in the sequential computon (let us call it $\lambda_{3}$).
Similarly, all the e-inports of $\lambda_{2}$ that are not in the image of
$\alpha_{2}$ become e-inports in $\lambda_{3}$. Naturally, this generative
effect does not occur in the case of total sequential composition since the
images of the computon morphisms involved would cover every e-outport of the
left operand and every e-inport of the right one. Instead, each $p_{1}\in
P_{1}^{-}$ and each $p_{2}\in P_{2}^{+}$ would be mapped to an i-port of
$\lambda_{3}$. No matter whether $\lambda_{1}\unrhd\lambda_{2}$ or
$\lambda_{1}\rhd\lambda_{2}$, it is true that $(\forall p_{1}\in
P_{1}^{+})(\exists p_{3}\in P_{3}^{+})[\beta_{1}(p_{1})=p_{3}]$ and $(\forall
p_{2}\in P_{2}^{-})(\exists q_{3}\in P_{3}^{-})[\beta_{2}(p_{2})=q_{3}]$ (see
Proposition 13).

######  Proposition 13.

If
$(\beta_{1}:\lambda_{1}\rightarrow\lambda_{3},\lambda_{3},\beta_{2}:\lambda_{2}\rightarrow\lambda_{3})$
is the pushout of computon morphisms
$\alpha_{1}:\lambda_{0}\rightarrow\lambda_{1}$ and
$\alpha_{2}:\lambda_{0}\rightarrow\lambda_{2}$ with
${\lambda_{1}\unrhd\lambda_{2}}$, then ${\beta_{1}(P_{1}^{+})=P_{3}^{+}}$ and
${\beta_{2}(P_{2}^{-})=P_{3}^{-}}$.

###### Proof.

Considering the commutative diagram presented in Definition 16 and assuming
that ${\lambda_{1}\unrhd\lambda_{2}}$, below we just show that
${\beta_{1}(P_{1}^{+})=P_{3}^{+}}$ since the proof of
${\beta_{2}(P_{2}^{-})=P_{3}^{-}}$ is completely analogous.

Assume for contrapositive that ${p_{3}\notin P_{3}^{+}}$ so there is some
${e_{3}\in E_{3}}$ where ${t_{3}(e_{3})=p_{3}}$. The fact
${E_{3}=E_{1}+_{E_{0}}E_{2}}$ entails that there are three possibilities: (i)
there exclusively is some ${e_{1}\in E_{1}}$ where ${\beta_{1}(e_{1})=e_{3}}$,
(ii) there exclusively is some ${e_{2}\in E_{2}}$ where
${\beta_{2}(e_{2})=e_{3}}$ or (iii) there are ${e_{4}\in E_{1}}$ and
${e_{5}\in E_{2}}$ such that ${\beta_{1}(e_{4})=e_{3}=\beta_{2}(e_{5})}$. The
third scenario never holds since ${\lambda_{0}}$ is trivial by the fact
${\lambda_{1}\unrhd\lambda_{2}}$. So, we just prove for (i) and (ii).

For (i),
${\beta_{1}(t_{1}(e_{1}))=t_{3}(\beta_{1}(e_{1}))=t_{3}(e_{3})=p_{3}}$ implies
that there is some ${p_{1}\in P_{1}}$ for which ${t_{1}(e_{1})=p_{1}}$ and
${\beta_{1}(p_{1})=p_{3}}$. Consequently, by Definition 2, ${p_{1}\notin
P_{1}^{+}}$ so ${p_{3}\notin\beta_{1}(P_{1}^{+})}$. If (ii) holds,
${\beta_{2}(t_{2}(e_{2}))=t_{3}(\beta_{2}(e_{2}))=t_{3}(e_{3})=p_{3}}$ implies
that there is some ${p_{2}\in P_{2}}$ for which ${t_{2}(e_{2})=p_{2}}$ and
${\beta_{2}(p_{2})=p_{3}}$. If there is some ${p_{1}\in P_{1}}$ where
${\beta_{1}(p_{1})=p_{3}=\beta_{2}(p_{2})}$, there is some ${p_{0}\in P_{0}}$
where ${\alpha_{1}(p_{0})=p_{1}}$ and ${\alpha_{2}(p_{0})=p_{2}}$. As
${(\nexists e_{1}\in E_{1})[\beta_{1}(e_{1})=e_{3}=\beta_{2}(e_{2})]}$ and
${\sigma_{2}}$ is surjective, ${p_{0}\in\vec{i}(\alpha_{2})}$ which
contradicts the fact ${\vec{i}(\alpha_{2})=\emptyset}$ (see Corollary 1). So,
there is no ${p_{1}\in P_{1}}$ where
${\beta_{1}(p_{1})=p_{3}=\beta_{2}(p_{2})}$. That is,
${p_{3}\notin\beta_{1}(P_{1}^{+})}$.

Proving ${p_{3}\notin P_{3}^{+}\implies p_{3}\notin\beta_{1}(P_{1}^{+})}$ in
the above cases entails that ${\beta_{1}(P_{1}^{+})\subseteq P_{3}^{+}}$. We
now prove that ${P_{3}^{+}\subseteq\beta_{1}(P_{1}^{+})}$ also holds. If we
let ${q_{3}\in P_{3}^{+}}$, by Proposition 2 and by the fact
${P_{3}=P_{1}+_{P_{0}}P_{2}}$, we have three options: (1) there exclusively is
some ${q_{1}\in P_{1}^{+}}$ such that ${\beta_{1}(q_{1})=q_{3}}$, (2) there
exclusively is some ${q_{2}\in P_{2}^{+}}$ such that
${\beta_{2}(q_{2})=q_{3}}$ or (3) there are ${q_{4}\in P_{1}^{+}}$ and
${q_{5}\in P_{2}^{+}}$ such that ${\beta_{1}(q_{4})=q_{3}=\beta_{2}(q_{5})}$.
If (1) is true, then ${q_{3}\in\beta_{1}(P_{1}^{+})}$ follows directly. We now
show that (2) and (3) do not hold.

Supposing (2) is true, ${q_{2}\in\alpha_{2}(\vec{i}(\alpha_{1}))}$ because
${\lambda_{1}\unrhd\lambda_{2}}$ implies
${\alpha_{2}(\vec{i}(\alpha_{1}))=P_{2}^{+}}$. Therefore, ${(\exists q_{0}\in
P_{0}\cap\vec{i}(\alpha_{1}))(\exists q_{1}\in
P_{1})[\alpha_{1}(q_{0})=q_{1}~{}\land~{}\alpha_{2}(q_{0})=q_{2}]}$. As
commutativity contradicts (2), there is no ${q_{2}\in P_{2}^{+}}$ such that
${\beta_{2}(q_{2})=q_{3}\in P_{3}^{+}}$. That is,
${q_{3}\notin\beta_{2}(P_{2}^{+})}$. To disprove (3), we deduce by
commutativity the existence of some ${q\in P_{0}}$ where
${\alpha_{1}(q)=q_{4}}$ and ${\alpha_{2}(q)=q_{5}}$. Since ${q_{4}\in
P_{1}^{+}}$ and ${q_{5}\in P_{2}^{+}}$, Proposition 2 says that ${q\in
P_{0}^{+}}$. The fact that ${\lambda_{2}}$ is a connected computon and that
${\alpha_{2}(q)=q_{5}\in P_{2}^{+}}$ entail that ${q\in\vec{o}(\alpha_{2})}$.
Because ${\lambda_{1}\unrhd\lambda_{2}}$, it is true that
${\alpha_{1}(\vec{o}(\alpha_{2}))=P_{1}^{-}}$ and, consequently, that
${\alpha_{1}(q)=q_{4}\in P_{1}^{-}}$. But ${\lambda_{1}}$ is also a connected
computon, so ${q_{4}\in P_{1}^{+}\cap P_{1}^{-}}$ cannot hold (see Proposition
1). As this contradicts our initial assumption, we have that there is no
${q_{5}\in P_{2}^{+}}$ where ${\beta_{2}(q_{5})=q_{3}\in P_{3}^{+}}$. That is,
${q_{3}\notin\beta_{2}(P_{2}^{+})}$.

Proving (1) and disproving (2) and (3) entails that ${q_{3}\in
P_{3}^{+}\implies[q_{3}\in\beta_{1}(P_{1}^{+})\setminus\beta_{2}(P_{2}^{+})]}$,
i.e., ${P_{3}^{+}\subseteq\beta_{1}(P_{1}^{+})}$, as required. ∎

Although Figure 6 shows an example of partial sequential composition, the same
computon operands can be used to perform total sequential composition. This is
because, in this case, there exists an apex computon that can be inserted into
all the e-outports of $\lambda_{1}$ and into all the e-inports of
$\lambda_{2}$. Such an apex does not always exist so partiality does not imply
totality and, thus, the reverse of Proposition 11 does not hold. Proposition
11 combined with Theorem 1 states that if any two connected computons can be
composed totally, they can also be composed partially.

###  6.2 Parallel Computons

Parallel composition is an operation that combines coproduct and pushout
constructions for defining a parallel computon in
$\textbf{Set}^{\textbf{Comp}}$. As per Proposition 14, the coproduct of two
computons can always be computed in this category.

######  Proposition 14.

The coproduct ${\lambda_{1}+\lambda_{2}}$ of computons ${\lambda_{1}}$ and
${\lambda_{2}}$ exists in ${\textbf{Set}^{\textbf{Comp}}}$.

###### Proof.

The coproduct ${\lambda_{3}}$ of a computon ${\lambda_{1}}$ and a computon
${\lambda_{2}}$, written ${\lambda_{1}+\lambda_{2}}$, is obtained by computing
the following in Set: ${P_{3}=P_{1}+P_{2}}$, ${U_{3}=U_{1}+U_{2}}$,
${E_{3}=E_{1}+E_{2}}$, ${F_{3}=F_{1}+F_{2}}$ and
${\Sigma_{3}=\Sigma_{1}+_{\Sigma_{1}\cap\Sigma_{2}}\Sigma_{2}}$. Particularly,
the pushout operation to obtain ${\Sigma_{3}}$ is valid since the span
${\Sigma_{1}\hookleftarrow\Sigma_{1}\cap\Sigma_{2}\hookrightarrow\Sigma_{2}}$
of inclusion functions always exists in Set (because
${\Sigma_{1},\Sigma_{2}\subset\mathbb{N}}$). Thus,
${\Sigma_{3}=\Sigma_{1}+_{\Sigma_{1}\cap\Sigma_{2}}\Sigma_{2}=\Sigma_{1}\cup\Sigma_{2}}$.
As ${c_{3}}$ is canonically the mapping
${P_{1}+P_{2}\rightarrow\Sigma_{1}\cup\Sigma_{2}}$ and ${(\forall
i\in\\{1,2\\})(\forall p\in P_{i})(\exists!x\in\Sigma_{i})[c_{i}(p)=x]}$, it
follows that ${c_{3}}$ is surjective. All the functions of ${\lambda_{3}}$,
including ${c_{3}}$, are defined in the obvious way to make the corresponding
squares commute. For example: $\forall e_{3}\in
E_{3},\sigma_{3}(e_{3})=\begin{cases}(\beta_{1}\circ\sigma_{1})(e_{1})&\text{if
}e_{3}=\beta_{1}(e_{1})\text{ for some }e_{1}\in E_{1}\\\
(\beta_{2}\circ\sigma_{2})(e_{2})&\text{if }e_{3}=\beta_{2}(e_{2})\text{ for
some }e_{2}\in E_{2}\end{cases}$

The existence of each component of
${\beta_{j}:\lambda_{j}\rightarrow\lambda_{1}+\lambda_{2}}$ (for ${j=1,2}$)
follows directly from the fact that Set has all coproducts and all pushouts.
Particularly, the ${\Sigma}$-component of $\beta_{j}$ is an inclusion map
because ${\Sigma_{j}\subseteq\Sigma_{1}\cup\Sigma_{2}}$. Furthermore,
${\vec{i}(\beta_{j})\cup\vec{o}(\beta_{j})=\emptyset\subseteq P_{j}^{+}\cup
P_{j}^{-}}$ because ${U_{3}}$ is computed as the disjoint union of ${U_{1}}$
and ${U_{2}}$.

Coproduct and pushout satisfy the universal property in Set so coproduct in
${\textbf{Set}^{\textbf{Comp}}}$ also satisfies it. This means that, if there
is a computon ${\lambda_{4}}$ with morphisms
${\gamma_{1}:\lambda_{1}\rightarrow\lambda_{4}}$ and
${\gamma_{2}:\lambda_{2}\rightarrow\lambda_{4}}$, there is a unique morphism
${\gamma_{3}:\lambda_{3}\rightarrow\lambda_{4}}$ such that
${\gamma_{3}\circ\beta_{1}=\gamma_{1}}$ and
${\gamma_{3}\circ\beta_{2}=\gamma_{2}}$. To preserve commutativity, an
${A}$-component of ${\gamma_{3}}$ is given as follows:

$\forall a_{3}\in A,\gamma_{3}(a_{3})=\begin{cases}\gamma_{1}(a_{1})&\text{if
}a_{3}=\beta_{1}(a_{1})\text{ for some }a_{1}\in A_{1}\\\
\gamma_{2}(a_{2})&\text{if }a_{3}=\beta_{2}(a_{2})\text{ for some }a_{2}\in
A_{2}\end{cases}$

By the above and by the fact that the ${\Sigma}$-components of $\gamma_{1}$
and $\gamma_{2}$ are both inclusion functions, it is easy to see that the
${\Sigma}$-component of ${\gamma_{3}}$ is also an inclusion. We just now have
to prove ${\vec{i}(\gamma_{3})\cup\vec{o}(\gamma_{3})\subseteq P_{3}^{+}\cup
P_{3}^{-}}$. Below we provide the proof of ${\vec{i}(\gamma_{3})\subseteq
P_{3}^{+}\cup P_{3}^{-}}$ since the other is completely analogous.

Let ${p_{3}\in\vec{i}(\gamma_{3})}$ so
${\bullet\gamma_{3}(p_{3})\setminus\gamma_{3}(\bullet p_{3})\neq\emptyset}$.
As ${P_{3}=P_{1}+P_{2}}$, we observe that ${p_{3}=\beta_{k}(p_{k})}$ for some
${p_{k}\in P_{k}}$ (${k=1,2}$). Using a similar reasoning as the proof of
Proposition 8, we deduce ${p_{k}\in\vec{i}(\gamma_{k})}$ which implies
${p_{k}\in P_{k}^{+}\cup P_{k}^{-}}$ because ${\gamma_{k}}$ is a computon
morphism with ${\vec{i}(\gamma_{k})\subseteq P_{k}^{+}\cup P_{k}^{-}}$ (see
Definition 7). As ${\vec{i}(\beta_{k})\cup\vec{o}(\beta_{k})=\emptyset}$,
${P_{k}\cap\vec{i}(\beta_{k})=\emptyset=P_{k}\cap\vec{o}(\beta_{k})}$ and,
consequently, ${\beta_{k}^{-1}(P_{3}^{+})=P_{k}^{+}}$ and
${\beta_{k}^{-1}(P_{3}^{-})=P_{k}^{-}}$ (see Proposition 3). That is,
${p_{k}\in P_{k}^{+}\cup P_{k}^{-}}$ $\iff$
${p_{k}\in\beta_{k}^{-1}(P_{3}^{+})\cup\beta_{k}^{-1}(P_{3}^{-})}$. Using the
fact ${p_{3}=\beta_{k}(p_{k})}$, we conclude that ${p_{3}\in P_{3}^{+}\cup
P_{3}^{-}}$. ∎

Structurally, a parallel computon consists of a fork computon, two connected
computons (i.e., the operands) and one join computon. The role of the fork and
join computons is to split and synchronise control to/from the operands,
respectively. Definition 20 formalises this construction.

######  Definition 20 (Parallel Computon).

Let $\lambda_{i}$ be a computon and $\alpha_{j}$ be a computon morphism for
${i=0,\ldots,16}$ and ${j=1,\ldots,26}$. We say that the pushout of
$\alpha_{23}$ and $\alpha_{24}$ forms a parallel computon if the following
diagram commutes in $\textbf{Set}^{\textbf{Comp}}$:

${\lambda_{7}}$${\lambda_{5}}$${M}$${\lambda_{6}}$${\lambda_{2}}$${S}$${\lambda_{3}}$${S}$${\lambda_{4}}$${\lambda_{0}}$${\lambda_{1}}$${\lambda_{2}+\lambda_{10}}$${M}$${\lambda_{16}}$${\lambda_{8}}$${\lambda_{9}}$${\lambda_{10}}$${S}$${\lambda_{11}}$${S}$${\lambda_{12}}$${\lambda_{13}}$${M}$${\lambda_{14}}$${\lambda_{15}}$$\scriptstyle{\alpha_{25}}$$\scriptstyle{\alpha_{9}}$$\scriptstyle{\alpha_{10}}$$\scriptstyle{\alpha_{21}}$$\scriptstyle{\alpha_{5}}$$\scriptstyle{\alpha_{6}}$$\scriptstyle{\alpha_{7}}$$\scriptstyle{\alpha_{8}}$$\scriptstyle{\alpha_{1}}$$\scriptstyle{\alpha_{2}}$$\scriptstyle{\alpha_{3}}$$\scriptstyle{\alpha_{4}}$$\scriptstyle{\alpha_{23}}$$\scriptstyle{\alpha_{24}}$$\scriptstyle{\alpha_{11}}$$\scriptstyle{\alpha_{12}}$$\scriptstyle{\alpha_{13}}$$\scriptstyle{\alpha_{14}}$$\scriptstyle{\alpha_{22}}$$\scriptstyle{\alpha_{15}}$$\scriptstyle{\alpha_{16}}$$\scriptstyle{\alpha_{17}}$$\scriptstyle{\alpha_{18}}$$\scriptstyle{\alpha_{19}}$$\scriptstyle{\alpha_{20}}$$\scriptstyle{\alpha_{26}}$

provided that:

  1. 1.

$\lambda_{i}\cong\Lambda$ for all $i\in\\{0,1,8,9\\}$,

  2. 2.

$\lambda_{3}$ and $\lambda_{11}$ are connected computons,

  3. 3.

$\lambda_{4}$ and $\lambda_{10}$ are fork computons,

  4. 4.

$\lambda_{2}$ and $\lambda_{12}$ are join computons,

  5. 5.

$\lambda_{5}$ is a sequential computon with $\lambda_{3}\rhd\lambda_{2}$,

  6. 6.

$\lambda_{6}$ is a sequential computon with $\lambda_{4}\rhd\lambda_{3}$,

  7. 7.

$\lambda_{13}$ is a sequential computon with $\lambda_{10}\rhd\lambda_{11}$,

  8. 8.

$\lambda_{14}$ is a sequential computon with $\lambda_{11}\rhd\lambda_{12}$,

  9. 9.

$\vec{o}(\alpha_{23})\cap\vec{o}(\alpha_{24})=\emptyset$ and

  10. 10.

$\vec{i}(\alpha_{23})\cap\vec{i}(\alpha_{24})=\emptyset$.

######  Notation 4.

Considering the construction described in Definition 20, we write
$\lambda_{3}\mid\lambda_{11}$ for the parallel computon $\lambda_{16}$. Here,
$\lambda_{3}$ and $\lambda_{11}$ are called the computon operands.

A glance at the diagram presented in Definition 20, reveals that there are
four pushout operations producing a sequential computon each (as per
Definition 18). If a pushout does not follow the restrictions imposed by such
a definition (i.e., it freely behaves as in Definition 16), then it just
“merges” two computons via some common object. The apex computon represents
the common part between the computons being merged. In the commutative diagram
of Definition 20, the squares marked with $M$ are pushouts of this sort,
whereas the squares marked with $S$ represent pushouts constructing a
sequential computon.

Figure 7 depicts the commutative diagram resulting from composing the
morphisms of the above diagram. This simplification is useful to understand
the building blocks that are needed to construct a parallel computon, namely
four trivial computons, a fork computon, a join computon and two connected
computons. Specifically, the simplified diagram shows that
$\lambda_{0},\lambda_{1},\lambda_{8}$ and $\lambda_{9}$ are isomorphic to the
unit computon, i.e., they are trivial computons with only one ec-inoutport
each (see Definition 11). The symbols $\lambda_{3}$ and $\lambda_{11}$
represent connected computons (i.e., the operands) being put in parallel via a
fork and a join computon. As every fork computon is trivially isomorphic to
any other fork computon, we have that $\lambda_{4}\cong\lambda_{10}$. The same
being true for the join computons $\lambda_{2}$ and $\lambda_{12}$. The
coproduct $\lambda_{2}+\lambda_{10}$ is then a yuxtaposition of a fork
computon and a join computon, which represents the common part between
$\lambda_{7}$ and $\lambda_{15}$. This coproduct serves as a common object for
the pushout of $\alpha_{23}$ and $\alpha_{24}$, i.e., for constructing the
parallel computon $\lambda_{16}$ (also written $\lambda_{3}\mid\lambda_{11}$ —
see Notation 4).

${\lambda_{8}\cong\Lambda}$${\lambda_{11}}$${\lambda_{9}\cong\Lambda}$${\lambda_{4}\cong\lambda_{10}}$${\lambda_{16}}$${\lambda_{2}\cong\lambda_{12}}$${\lambda_{1}\cong\Lambda}$${\lambda_{3}}$${\lambda_{0}\cong\Lambda}$$\scriptstyle{\alpha_{12}}$$\scriptstyle{\alpha_{11}}$$\scriptstyle{\alpha_{25}\circ\alpha_{23}\circ\alpha_{22}\circ\alpha_{11}}$$\scriptstyle{\alpha_{26}\circ\alpha_{24}\circ\alpha_{22}\circ\alpha_{11}}$$\scriptstyle{\alpha_{26}\circ\alpha_{19}\circ\alpha_{16}}$$\scriptstyle{\alpha_{26}\circ\alpha_{20}\circ\alpha_{17}}$$\scriptstyle{\alpha_{13}}$$\scriptstyle{\alpha_{14}}$$\scriptstyle{\alpha_{26}\circ\alpha_{19}\circ\alpha_{15}}$$\scriptstyle{\alpha_{25}\circ\alpha_{10}\circ\alpha_{8}}$$\scriptstyle{\alpha_{26}\circ\alpha_{20}\circ\alpha_{18}}$$\scriptstyle{\alpha_{25}\circ\alpha_{9}\circ\alpha_{5}}$$\scriptstyle{\alpha_{3}}$$\scriptstyle{\alpha_{4}}$$\scriptstyle{\alpha_{25}\circ\alpha_{9}\circ\alpha_{6}}$$\scriptstyle{\alpha_{25}\circ\alpha_{10}\circ\alpha_{7}}$$\scriptstyle{\alpha_{2}}$$\scriptstyle{\alpha_{1}}$$\scriptstyle{\alpha_{25}\circ\alpha_{23}\circ\alpha_{21}\circ\alpha_{1}}$$\scriptstyle{\alpha_{26}\circ\alpha_{24}\circ\alpha_{21}\circ\alpha_{1}}$
Figure 7: Commutative diagram resulting from composing the morphisms of the
Diagram of Definition 20. For increased clarity, some composite morphisms are
ommited, e.g.,
${\alpha_{26}\circ\alpha_{19}\circ\alpha_{15}\circ\alpha_{11}:\lambda_{8}\rightarrow\lambda_{16}}$.

Figure 8 provides a complete, self-descriptive example for constructing a
parallel computon from the connected computons used in our example of
sequential composition (see Figure 6).

$\lambda_{1}$$1$$2$$3$$4$$\lambda_{1}$$1$$2$$3$$4$$\lambda_{1}$$1$$2$$3$$4$$\lambda_{1}$$1$$2$$3$$4$$\lambda_{1}$$1$$2$$3$$4$$\lambda_{2}$$3$$4$$5$$\lambda_{2}$$3$$4$$5$$\lambda_{2}$$3$$4$$5$$\lambda_{2}$$3$$4$$5$$\lambda_{2}$$3$$4$$5$
Figure 8: Constructing a parallel computon $\lambda_{1}|\lambda_{2}$ where
$\lambda_{1}$ and $\lambda_{2}$ are the operands presented in Figure 6.

A glance at Figure 8 reveals that $\lambda_{1}|\lambda_{2}$ is constructed
from pushouts that rely on unit computons as apices. Consequently, only an ec-
inport ${p_{1}\in Q_{1}^{+}}$, an ec-outport ${p_{2}\in Q_{1}^{-}}$, an ec-
inport $q_{1}\in Q_{2}^{+}$ and an ec-outport $q_{2}\in Q_{2}^{-}$ become
i-ports in $\lambda_{1}|\lambda_{2}$. The rest of e-inports and e-outports of
the operands become e-inports and e-outports in $\lambda_{1}|\lambda_{2}$,
respectively. This structural implication is derived from the fact that fork
and join computons have control ports only; so, unlike sequential composition,
$\lambda_{1}$ and $\lambda_{2}$ do not exchange data when composed in
parallel. To ensure a consistent construction of the parallel computon
$\lambda_{1}|\lambda_{2}$, Condition 9 of Definition 20 intuitively says that
$p_{1}$ and $q_{1}$ cannot be mapped to the same ec-outport of the fork
computon. A similar constraint is imposed by Condition 10 which states that
$p_{2}$ and $q_{2}$ cannot be mapped to the same ec-inport of the join
computon.

Another difference with respect to sequential composition is that the order of
the operands does not matter. So, even if $\lambda_{1}$ and $\lambda_{2}$ are
interchanged in the construction of Definition 20, we would have the same
result as before, i.e.,
$(\lambda_{1}|\lambda_{2})\cong(\lambda_{2}|\lambda_{1})$. Although
commutativity differs in sequential and parallel composition, the result in
both operations is always a connected computon (see Proposition 15). Also,
like sequential composition, any two computons can be put in parallel
regardless of the data they require or produce (see Theorem 2).

######  Proposition 15.

A parallel computon is a connected computon.

###### Proof.

Let $\lambda_{3}|\lambda_{11}$ be the parallel computon constructed from the
commutative diagram presented in Definition 20. By Proposition 7, we have that
$\lambda_{2}$, $\lambda_{4}$, $\lambda_{10}$ and $\lambda_{12}$ are connected
computons (see Conditions 3 and 4). As $\lambda_{3}$ and $\lambda_{11}$ are
also connnected (see Condition 2), Proposition 9 entails that $\lambda_{7}$
and $\lambda_{15}$ are connected too. Even though $\lambda_{2}+\lambda_{10}$
is not a connected computon, we use Proposition 9 again to deduce that
$\lambda_{3}|\lambda_{11}$ is. ∎

######  Theorem 2.

$\lambda_{1}$ and $\lambda_{2}$ are connected computons $\iff$ the computons
$\lambda_{1}|\lambda_{2}$ and $\lambda_{2}|\lambda_{1}$ exist.

###### Proof.

${(\impliedby)}$ This part of the proof follows directly from Definition 20.

${(\implies)}$ Let ${\lambda_{3}}$ and ${\lambda_{11}}$ be two connected
computons, ${\lambda_{4}}$ and ${\lambda_{10}}$ be two fork computons,
${\lambda_{2}}$ and ${\lambda_{12}}$ be two join computons, and
$\lambda_{i}\cong\Lambda$ for all $i\in\\{0,1,8,9\\}$. We first construct
computon morphisms ${\alpha_{1}:\lambda_{0}\rightarrow\lambda_{2}}$,
${\alpha_{2}:\lambda_{0}\rightarrow\lambda_{3}}$,
${\alpha_{3}:\lambda_{1}\rightarrow\lambda_{3}}$,
${\alpha_{4}:\lambda_{1}\rightarrow\lambda_{4}}$,
${\alpha_{11}:\lambda_{8}\rightarrow\lambda_{10}}$,
${\alpha_{12}:\lambda_{8}\rightarrow\lambda_{11}}$,
${\alpha_{13}:\lambda_{9}\rightarrow\lambda_{11}}$ and
$\alpha_{14}:\lambda_{9}\rightarrow\lambda_{12}$. As their domain is a unit
computon, each morphism is a diagram with the following shape:

${1}$${1}$${\emptyset}$${\emptyset}$${\emptyset}$${1}$${1}$${\Sigma}$${P}$${E}$${U}$${F}$${P}$${\Sigma}$

In the above diagram, it is evident that the only morphism components that are
not empty functions are those mapping ports and colours, respectively. As the
set of colours of ${\Lambda}$ is ${\\{0\\}}$ and $0$ is in the set of colours
of every computon, the $\Sigma$-component can be defined in the obvious way to
yield an inclusion function. Now, if ${p_{i}\in P_{i}}$, the $P$-component of
each morphism is given as follows: ${\alpha_{1}(p_{0})\in Q_{2}^{+}}$,
${\alpha_{2}(p_{0})\in Q_{3}^{-}}$, ${\alpha_{3}(p_{1})\in Q_{3}^{+}}$,
${\alpha_{4}(p_{1})\in Q_{4}^{-}}$, ${\alpha_{11}(p_{8})\in Q_{10}^{-}}$,
${\alpha_{12}(p_{8})\in Q_{11}^{+}}$, ${\alpha_{13}(p_{9})\in Q_{11}^{-}}$ and
${\alpha_{14}(p_{9})\in Q_{12}^{+}}$.

Since ${\lambda_{10}}$ and ${\lambda_{11}}$ are connected computons and
$\lambda_{8}$ is trivial (see Proposition 1), it follows that
${p_{8}\in\vec{i}(\alpha_{11})\cap\vec{o}(\alpha_{12})}$ and, consequently,
that ${P_{8}=\vec{i}(\alpha_{11})\cap\vec{o}(\alpha_{12})}$ because
${P_{8}=\\{p_{8}\\}}$. The facts
${p_{8}\in\vec{i}(\alpha_{11})\cap\vec{o}(\alpha_{12})}$,
${\alpha_{11}(p_{8})\in Q_{10}^{-}}$ and ${\alpha_{12}(p_{8})\in Q_{11}^{+}}$
allow us to further deduce ${\alpha_{11}(\vec{o}(\alpha_{12}))\subseteq
Q_{10}^{-}\subseteq P_{10}^{-}}$ and
${\alpha_{12}(\vec{i}(\alpha_{11}))\subseteq Q_{11}^{+}\subseteq P_{11}^{+}}$.
In particular, ${\alpha_{11}(\vec{o}(\alpha_{12}))\subset P_{10}^{-}}$ because
${\alpha_{11}}$ is monic, ${|P_{8}|=1}$ and ${|P_{10}^{-}|=|Q_{10}^{-}|=2}$
(see Remark 1 and Definitions 11 and 13).

Since ${\alpha_{11}(p_{8})\in Q_{10}^{-}}$ and ${\alpha_{12}(p_{8})\in
Q_{11}^{+}}$,
${\alpha_{11}(p_{8})\bullet=\emptyset=\bullet\alpha_{12}(p_{8})}$ so
${p_{8}\notin\vec{o}(\alpha_{11})\cup\vec{i}(\alpha_{12})}$. The fact
${P_{8}=\\{p_{8}\\}}$ allow us to derive
${\vec{o}(\alpha_{11})\cup\vec{i}(\alpha_{12})=\emptyset}$ so that
${\alpha_{11}(\vec{i}(\alpha_{12}))=\emptyset\subset P_{10}^{+}\cup
P_{10}^{-}}$ and ${\alpha_{12}(\vec{o}(\alpha_{11}))=\emptyset\subset
P_{11}^{+}\cup P_{11}^{-}}$. Above we showed that
${\alpha_{11}(\vec{o}(\alpha_{12}))\subset P_{10}^{-}\subset P_{10}^{+}\cup
P_{10}^{-}}$ and that ${\alpha_{12}(\vec{i}(\alpha_{11}))\subseteq
P_{11}^{+}\subset P_{11}^{+}\cup P_{11}^{-}}$. Therefore,
${\lambda_{10}\xleftarrow{\alpha_{11}}\lambda_{8}\xrightarrow{\alpha_{12}}\lambda_{11}}$
is pushable (see Definition 17). By Proposition 8 and Definition 18, the
pushout
${(\alpha_{15}:\lambda_{10}\rightarrow\lambda_{13},\lambda_{13},\alpha_{16}:\lambda_{11}\rightarrow\lambda_{13})}$
of ${\alpha_{11}}$ and ${\alpha_{12}}$ can be constructed to form a sequential
computon with ${\lambda_{10}\rhd\lambda_{11}}$. A similar reasoning can be
used to deduce the existence of
${(\alpha_{6}:\lambda_{3}\rightarrow\lambda_{5},\lambda_{5},\alpha_{5}:\lambda_{2}\rightarrow\lambda_{5})}$
from
${\lambda_{3}\xleftarrow{\alpha_{2}}\lambda_{0}\xrightarrow{\alpha_{1}}\lambda_{2}}$,
${(\alpha_{8}:\lambda_{4}\rightarrow\lambda_{6},\lambda_{6},\alpha_{7}:\lambda_{3}\rightarrow\lambda_{6})}$
from
${\lambda_{4}\xleftarrow{\alpha_{4}}\lambda_{1}\xrightarrow{\alpha_{3}}\lambda_{3}}$
and $({\alpha_{17}:\lambda_{11}\rightarrow\lambda_{14},}$
${\lambda_{14},\alpha_{18}:\lambda_{12}\rightarrow\lambda_{14})}$ from
${\lambda_{11}\xleftarrow{\alpha_{13}}\lambda_{9}\xrightarrow{\alpha_{14}}\lambda_{12}}$
such that ${\lambda_{3}\rhd\lambda_{2}}$, ${\lambda_{4}\rhd\lambda_{3}}$ and
${\lambda_{11}\rhd\lambda_{12}}$.

Now, as ${\alpha_{13}(p_{9})\in Q_{11}^{-}}$ and ${\alpha_{14}(p_{9})\in
Q_{12}^{+}}$, it is routine to show that
${\lambda_{13}\xleftarrow{\alpha_{16}}\lambda_{11}\xrightarrow{\alpha_{17}}\lambda_{14}}$
is pushable too. So, the pushout
${(\alpha_{19}:\lambda_{13}\rightarrow\lambda_{15},\lambda_{15},\alpha_{20}:\lambda_{14}\rightarrow\lambda_{15})}$
of $\alpha_{16}$ and $\alpha_{17}$ can be constructed. A similar approach can
be used to prove that the span
${\lambda_{6}\xleftarrow{\alpha_{7}}\lambda_{3}\xrightarrow{\alpha_{6}}\lambda_{5}}$
yields
${(\alpha_{10}:\lambda_{6}\rightarrow\lambda_{7},\lambda_{7},\alpha_{9}:\lambda_{5}\rightarrow\lambda_{7})}$.
Evidently, these two pushouts do not produce sequential computons by the fact
that ${\lambda_{3}}$ and ${\lambda_{11}}$ are not trivial computons.

The fact that ${\lambda_{2}}$ and ${\lambda_{12}}$ are both join computons
entails that ${\lambda_{2}\cong\lambda_{12}}$; consequently, there is a
computon isomorphism ${\alpha_{27}:\lambda_{2}\rightarrow\lambda_{12}}$. By
composing morphisms, we obtain the composites
${\alpha_{19}\circ\alpha_{15}:\lambda_{10}\rightarrow\lambda_{15}}$ and
${\alpha_{20}\circ\alpha_{18}\circ\alpha_{27}:\lambda_{2}\rightarrow\lambda_{15}}$.
As the coproduct ${\lambda_{2}+\lambda_{10}}$ exists (as per Proposition 14),
we know that there also are computon morphisms
${\alpha_{21}:\lambda_{2}\rightarrow\lambda_{2}+\lambda_{10}}$ and
${\alpha_{22}:\lambda_{10}\rightarrow\lambda_{2}+\lambda_{10}}$. The existence
of ${\alpha_{19}\circ\alpha_{15}}$ and
${\alpha_{20}\circ\alpha_{18}\circ\alpha_{27}}$ allows us to use the universal
property of coproducts to deduce that there is a unique computon morphism
${\alpha_{24}:\lambda_{2}+\lambda_{10}\rightarrow\lambda_{15}}$. A similar
reasoning can be used to deduce a unique
${\alpha_{23}:\lambda_{2}+\lambda_{10}\rightarrow\lambda_{7}}$. Again, it is
routine to show that the span
${\lambda_{15}\xleftarrow{\alpha_{24}}\lambda_{2}+\lambda_{10}\xrightarrow{\alpha_{23}}\lambda_{7}}$
is pushable. So, using Proposition 8 we deduce that the pushout
$(\alpha_{25}:\lambda_{7}\rightarrow\lambda_{3}|\lambda_{11},\lambda_{3}|\lambda_{11},\alpha_{26}:\lambda_{15}\rightarrow\lambda_{3}|\lambda_{11})$
of ${\alpha_{23}}$ and ${\alpha_{24}}$ can be constructed. This pushout does
not form a sequential computon because ${\lambda_{2}+\lambda_{10}}$ is not a
trivial computon.

Since ${\lambda_{3}}$ is a connected computon and ${\alpha_{3}(p_{1})\in
Q_{3}^{+}}$, ${p_{1}\in\vec{o}(\alpha_{3})}$ so
${\alpha_{3}(p_{1})\bullet\neq\emptyset}$. By commutativity,
${\alpha_{7}(\alpha_{3}(p_{1}))=\alpha_{8}(\alpha_{4}(p_{1}))}$ so
${\alpha_{8}(\alpha_{4}(p_{1}))\bullet\neq\emptyset}$ and, thereby,
${\alpha_{10}(\alpha_{8}(\alpha_{4}(p_{1})))\bullet\neq\emptyset}$. As
${\lambda_{4}\cong\lambda_{10}}$, there exists an isomorphism
${\alpha_{28}:\lambda_{4}\rightarrow\lambda_{10}}$ where
${\alpha_{23}\circ\alpha_{22}\circ\alpha_{28}\circ\alpha_{4}=\alpha_{10}\circ\alpha_{8}\circ\alpha_{4}}$
so
${\alpha_{23}(\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1}))))\bullet\neq\emptyset}$.
Since ${p_{1}\bullet=\emptyset}$ and
${\vec{o}(\alpha_{4})=\vec{o}(\alpha_{28})=\vec{o}(\alpha_{22})=\emptyset}$,
it follows that
${\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1})))\bullet=\emptyset}$. Hence,
${\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1})))\in\vec{o}(\alpha_{23})}$.

The fact ${\lambda_{1}\cong\lambda_{8}}$ allows us to deduce the existence of
a unique isomorphism ${\lambda_{29}:\lambda_{1}\rightarrow\lambda_{8}}$ where
${\alpha_{11}\circ\alpha_{29}\neq\alpha_{28}\circ\alpha_{4}}$, i.e.,
${\alpha_{11}(\alpha_{29}(p_{1}))=\alpha_{11}(p_{8})\neq\alpha_{28}(\alpha_{4}(p_{1}))}$.
Using again ${p_{1}\bullet=\emptyset}$ and
${\vec{o}(\alpha_{4})=\vec{o}(\alpha_{28})=\emptyset}$, we have
${\alpha_{28}(\alpha_{4}(p_{1}))\bullet=\emptyset}$ and, consequently,
${\alpha_{15}(\alpha_{28}(\alpha_{4}(p_{1})))\bullet=\emptyset}$.

By the above and since
${\alpha_{16}(\alpha_{12}(p_{8}))\neq\alpha_{15}(\alpha_{28}(\alpha_{4}(p_{1})))}$,
${\alpha_{19}(\alpha_{15}(\alpha_{28}(\alpha_{4}(p_{1}))))\bullet=\emptyset}$.
Using commutativity, we obtain
${\alpha_{24}\circ\alpha_{22}\circ\alpha_{28}\circ\alpha_{4}=\alpha_{19}\circ\alpha_{15}\circ\alpha_{28}\circ\alpha_{4}}$
and, consequently,
${\alpha_{24}(\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1}))))\bullet=\emptyset}$.
As ${\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1})))\bullet=\emptyset}$,
${\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1})))\notin\vec{o}(\alpha_{24})}$.

A similar reasoning can show
${\alpha_{22}(\alpha_{11}(\alpha_{29}(p_{1})))\in\vec{o}(\alpha_{24})}$ and
${\alpha_{22}(\alpha_{11}(\alpha_{29}(p_{1})))\notin\vec{o}(\alpha_{23})}$. As
${\alpha_{22}(\alpha_{11}(\alpha_{29}(p_{1})))\neq\alpha_{22}(\alpha_{28}(\alpha_{4}(p_{1})))}$
(because ${\alpha_{11}\circ\alpha_{29}\neq\alpha_{28}\circ\alpha_{4}}$) and
every fork computon has exactly two ec-outports,
${\vec{o}(\alpha_{23})\cap\vec{o}(\alpha_{24})=\emptyset}$. The proof for
${\vec{i}(\alpha_{23})\cap\vec{i}(\alpha_{24})=\emptyset}$ follows
analogously.

Since our construction satisfies all the conditions of Definition 20, the
proof of existence of ${\lambda_{3}|\lambda_{11}}$ is complete. To prove that
${\lambda_{11}|\lambda_{3}}$ also exists, we just need to repeat all the steps
of this proof by writing ${\lambda_{3}}$ for ${\lambda_{11}}$ and
${\lambda_{11}}$ for ${\lambda_{3}}$. Doing this is completely valid since, by
Definition 1, every connected computon has at least one ec-inport and least
one ec-outport. ∎

##  7 Related Work

In this section, we present the related work of our proposal, namely related
compositional approaches and component models that separate concerns.

Prosave [18] is a design language built on top of the ProCom component model,
which was inspired on [19] to allow the definition of nested structures of
interconnected components. Like computons, Procom components are passive units
of computation with explicit separation of control ports and data ports.
Despite of this similarity, Procom is not compositional since it does not
provide algebraic operators to perform control-based composition, but just
informal programming constructs for connecting ports either directly or
indirectly. Indirect connection is done through so-called connectors which
establish control or data flow interaction between components via message
passing. As the model is not compositional, Procom composites do not offer a
clear separation of concerns like their internal components. They rather have
data ports only where both control flow and data flow terminate.

SCADE [20] is a similar component model which integrates an imperative
language (i.e., Esterel [21]) and a functional language (i.e., Lustre [22]) to
define control flow and data flow, respectively. Particularly, so-called Safe-
State Machines (SSMs) model the discrete control part of a system, whereas
Lustre blocks serve to continuously process data. Like Prosave, SCADE does not
provide formal operators for defining control-based composite blocks, but just
programming constructs to non-compositionally assemble a system.

In the same line of work, [9, 23, 24] describe a component model that provides
two orthogonal dimensions to manage control flow and data flow separately. The
model encapsulates control since it offers composition operators to define
sequential, parallel or branchial composites in a hierarchical, bottom-up
manner. Unfortunately, the semantics of the model is semi-formal [4] so it is
not possible to precisely determine whether the model is fully compositional
or not. Also, components do not have separate ports for data and control, but
just control ports. Consequently, the data dimension is implicitly defined in
the underlying composition mechanism whose goal is to build complex workflows
from simpler ones.

Workflow Nets (WF-nets) [25, 26] provide support for modelling workflow
processes in the form of control-driven computations. As they offer well-
founded semantics, WF-nets formalise the notion of workflow graphs which are
traditionally specified through industry-oriented languages such as UML
diagrams, Event-driven Process Chains or the Business Process Modelling
Notation (BPMN). WF-nets do not separate control from data and do not provide
operators for explicitly and compositionally defining parallel or sequential
composites. The issue of the separation of concerns is solved by RWFN-nets
[27] which unify extended WF-nets and so-called resource nets for separating
the process and resource perspectives of a workflow. Although the model
provides a clear separation of concerns, it is difficult to see the
relationship between data flow and control flow. In fact, the nets for both
perspectives are disconected from each other and synchronisation between them
is required. Also, there is not a clear distinction between input and output
data, and composition is not algebraically defined. Therefore, like WF-nets,
RWFN-nets are not compositional. Other Petri net based approaches, for
workflow construction, that non-compositionally separate control flow and data
flow are the functor model [28], extended-time nets [29], the FunState model
[30] and dual flow nets [7].

Existing compositional approaches built upon Petri net foundations rely on the
notion of open places which collectively form an interface to the external
world. These specially designated places are particularly used by open Petri
nets (ONets) [31] to construct complex behaviours from simpler ones. In this
framework, ONet composition is realised by gluing the output places of one net
with the input places of another. As this composition mechanism is
characterised as a pushout in a categorical setting [32], ONets are
compositional. An ONet morphism resembles a computon morphism in the sense
that input and output places can be preserved upon transformation (see
Proposition 2). Nevertheless, like Definition 16, a pushout operation just
serves for merging two ONets via a common object so that there are no specific
operators for explicitly defining sequential or parallel composites (i.e.,
ONets do not encapsulate control flow). Petri box calculus [33], Open WF-nets
[34], Whole-grain Petri nets [16], Petri nets with interface [35], nets with
boundaries [36] and Petri net components [37] also rely on the notion of open
places as interfaces. Like ONets, all these Petri-net-based approaches neither
encapsulate control flow nor separate data from control.

Although they do not separate concerns, Whole-grain Petri nets deserve a more
detailed analysis since, unlike their similars and like computons, they
abolish the traditional notion of multisets of places, typically expressed as
the free monoid $\mathbb{N}[P]$. Accordingly, they also work upon a similar
categorical scheme to Comp, in order to define concrete instances of Whole-
grain nets (cf. [15, 16]). The difference is that Comp has objects that enable
computons to have a clear distinction between control and data ports. Another
difference is that our theory identifies particular classes of computon
objects that can be used as building blocks to define more complex computons
through sequencing or parallelising operations. Although primitive computons
are isomorphic to Whole-grain corollas, Whole-grain Petri nets do not
distinguish between different types of corollas (e.g., join or fork corollas).

Within the realm of related compositional models, we also find string diagrams
[38, 39] which offer well-founded syntax to graphically represent morphisms of
symmetric monoidal categories. A string diagram is made up boxes connected
through wires, where boxes represent processes and wires express inputs or
outputs for those processes. As this model is rooted in category theory,
string diagrams can be composed sequentially via the $\circ$ operator or in
parallel via the tensor product. Since sequential composition is done by
totally matching outputs with inputs (or domain with codomain) and there are
not specifically designed wires for representing control, it follows that,
unlike computons, not every string diagram can be composed sequentially with
one another (cf. Theorem 1). Consequently, there is no distinction between
control flow and data flow.

A glance at Figures 6 and 8 reveals that the structure of a composite computon
is like a membrane in which other computons reside and that can be part of
another membrane/composite. An edge connected to/from a composite e-port is
akin to a fiber. This fiber can traverse other membranes as long as the e-port
it is connected to/from does not become an i-port. This analogy resembles the
structural organisation of a P-system [40] in which membranes are delimiting
compartments where multisets of objects evolve according to bio-inspired
rules. Unfortunately, a P-System is not compositional since there are no
formal operators to compositionally define membranes. Also, the model does not
separate data and control. In fact, such dimensions are implicitly defined in
the evolution of internal objects.

##  8 Conclusions and Future Directions

In this paper, we presented a constructive model of computation in which
computons are first-class semantic entities which structurally possess a
number of computation units that can be connected to/from two types of ports:
control ports and data ports. Such entities are objects in a functor category,
denoted $\textbf{Set}^{\textbf{Comp}}$, where two major classes of objects
reside. The first class is that of trivial computons which have just ports and
no computation units. The second class pertains to primitive computons which
are fully connected entities in the sense they have a unique computation unit
to which all ports are attached. These two classes serve as building blocks to
define complex computons via category-theoretic operations. We particularly
presented operations to inductively form either sequential or parallel
composite computons. As the model is compositional, composites exhibit the
same properties as their constituents, i.e., they have the same structure with
a clear separation of control flow and data flow.

Generally speaking, both control flow and data flow are inextricably present
in any classical computation, so it is crucial to separately reason about them
for verification, maintainability and optimisation purposes. For example, by
leveraging the fact that the behaviour of a computon can be expressed as a
token game, it is possible to use standard Petri net tools or relevant graph-
based analysis techniques to separately verify computing properties, such as
reachability of control flow and data flow. Taking advantage of graph-based
techniques can also enable an optimal implementation in which functional
computons exchange data decentrally while composites coordinate control flow
hierarchically [9]. Although we decided not to include explicit structures for
data processing (e.g., map-reduce or filter constructs), because data flow is
ultimately governed by control flow, we acknowledge that introducing them is
important to increase the expressivity of composite computons. However, doing
this in a compositional manner requires further investigation.

Enabling compositionality is also important to induce modularity which is a
well-known feature for reusing computations at scale. Modularity does not
imply compositionality because modules can be constructed in many different
ways (not necessarily algebraically). When an algebraic composition mechanism
is used to realise this feature, computation properties are preserved across
all composition levels. In our proposal, the separation of control flow and
data flow is one of such properties. Thus, as computons only interact through
their respective e-ports, composite computons can be perceived as modular
black-boxes that encapsulate some precise control-flow structure. At the
moment, we only consider sequential and parallel control flow. In the future,
we would like to prove the universality of our model by providing category-
theoretic constructions for defining iterative and branchial computons.
Branching and iteration are merely processes for choosing and repeating
sequential computations, so we conjecture that the yet-to-be-defined
categorical constructions could be built upon sequential pushouts (see
Definition 18).

In Sections 6.1 and 6.2, we proved that any pair of connected computons in
$\textbf{Set}^{\textbf{Comp}}$ can always be composed sequentially (see
Theorem 1) or in parallel (see Theorem 2) regardless of the data they require
or produce. This is because, intuitively, a computon has at least an ec-
outport that can always be matched with the ec-inport of another one. Matching
all the e-outports of one computon with all the e-inports of another one gives
rise to total sequential composition which, to the best of our knowledge, is
the _de facto_ way of sequencing computations nowadays (cf. [41]).

In this paper, we argue that sequencing is a particular form of merging
because the former can be expressed in terms of the latter. Particularly, in
our proposal, merging corresponds to a pushout operation in
$\textbf{Set}^{\textbf{Comp}}$ (see Definition 16), while sequencing is
characterised as a pushout with restrictions in the same category (see
Definition 18). As sequencing cannot only be done totally but also partially
(see Definition 19), our sequencing mechanism is more general than those
prevailing in the existing literature. Partial composition entails that non-
matching e-ports are preserved across every composition level (see Figures 6
and 8).

If computons are seen as relations from e-inports to e-outports, our
composition mechanism provides the basis to redefine the current notion of
composition of relations which states that the composite $S\circ R$ of
$R\subseteq X\times Y$ and $S\subseteq Y\times Z$ is given by
$\\{(x,z)\mid\exists y[R(x,y)~{}\land~{}S(y,z)]\\}$. Since $(S\circ R)$ is a
subset of $X\times Z$, it is evident that some relations in $X\times Y$ and in
$Y\times Z$ are lost. By resorting to the foundations laid in this paper, a
preservative definition emerges: ${(S\circ R)\cup[(X\times Y)\setminus(S\circ
R)]\cup[(Y\times Z)\setminus(S\circ R)]}$. Thus, rather than being a subset of
$X\times Z$, a composite relation would be a subset of $(X\cup Y)\times(Y\cup
Z)$. In the future, we would like to further investigate this preservative
notion.

Defining computons as preorders in a categorical setting can be achieved by
borrowing ideas from resource theories [39]. We hypothesize that there are
symmetric monoidal categories in which computons are morphisms and ports are
objects. Defining categories of this sort can be helpful to study the
operational semantics of composite computons through the arrow of time.
Particularly, _v-categories_ and _v-profunctors_ can provide theoretical
underpinnings for formally answering questions about the execution of
computons.

## Appendix A

Table 1 presents a mapping from Petri net syntax to computon syntax, which is
useful to discuss the operational semantics of computons. A glance at this
table reveals that, in general, places with no incoming arrows correspond to
e-inports, whereas places with no outgoing arrows correspond to e-outports.
This reflects the fact that e-inports and e-outports receive and send
information from/to the external world.

Table 1: Mapping from Petri net syntax to computon syntax where ${n,n_{i}\in\mathbb{N}^{>}}$ for all ${i=1,\ldots,4}$. $\mathbb{N}^{>}$ denotes the set of all natural numbers greater than zero. |  | Petri net syntax | Computon syntax
---|---|---|---
Control | ec-inport | $0$ |
ec-outport | $0$ |
ec-inoutport | $0$ |
| ic-port | $0$ |
Data | ed-inport | $n$ | $n$
ed-outport | $n$ | $n$
ed-inoutport | $n$ | $n$
| id-port | $n$ | $n$
Functional Computon | $0$$n_{1}$$\vdots$$n_{2}$$0$$n_{3}$$\vdots$$n_{4}$ | $\lambda_{1}$$n_{1}$$\vdots$$n_{2}$$n_{3}$$\vdots$$n_{4}$
Fork Computon | $0$$0$$0$ |
Join Computon | $0$$0$$0$ |
Composite Computon | $0$$n_{1}$$\vdots$$n_{2}$$\cdots$$0$$n_{3}$$\vdots$$n_{4}$ | $n_{1}$$\vdots$$n_{2}$$n_{3}$$\vdots$$n_{4}$

## References

  * [1] S. Tripakis, C. Stergiou, C. Shaver, E. A. Lee, A modular formal semantics for Ptolemy, Mathematical Structures in Computer Science 23 (4) (2013) 834–881.
  * [2] F. Arbab, Composition of Interacting Computations, in: D. Goldin, S. A. Smolka, P. Wegner (Eds.), Interactive Computation: The New Paradigm, Springer, Berlin, Heidelberg, 2006, pp. 277–321.
  * [3] K.-K. Lau, S. Di Cola, An Introduction to Component-based Software Development, 1st Edition, World Scientific, Singapore, 2017.
  * [4] D. Arellanes, K.-K. Lau, Evaluating IoT service composition mechanisms for the scalability of IoT systems, Future Generation Computer Systems 108 (2020) 827–848.
  * [5] F. Arbab, Reo: a channel-based coordination model for component composition, Mathematical Structures in Computer Science 14 (3) (2004) 329–366.
  * [6] R. Message, Programming for humans: a new paradigm for domain-specific languages, Technical Report UCAM-CL-TR-843, University of Cambridge (2013).
  * [7] M. Varea, B. M. Al-Hashimi, L. A. Cortés, P. Eles, Z. Peng, Dual Flow Nets: Modeling the control/data-flow relation in embedded systems, ACM Transactions on Embedded Computing Systems 5 (1) (2006) 54–81.
  * [8] E. Clarke, A. Gupta, H. Jain, H. Veith, Model Checking: Back and Forth between Hardware and Software, in: B. Meyer, J. Woodcock (Eds.), Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2008, pp. 251–255.
  * [9] D. Arellanes, K.-K. Lau, R. Sakellariou, Decentralized Data Flows for the Functional Scalability of Service-Oriented IoT Systems, The Computer Journal 66 (6) (2023) 1477–1506.
  * [10] W. Vanderbauwhede, Separation of Data flow and Control flow in Reconfigurable Multi-core SoCs using the Gannet Service-based Architecture, in: Second NASA/ESA Conference on Adaptive Hardware and Systems (AHS 2007), 2007, pp. 326–333.
  * [11] D. Arellanes, K.-K. Lau, Analysis and Classification of Service Interactions for the Scalability of the Internet of Things, in: IEEE ICIOT, 2018, pp. 80–87.
  * [12] D. Arellanes, K.-K. Lau, Algebraic Service Composition for User-Centric IoT Applications, in: D. Georgakopoulos, L.-J. Zhang (Eds.), Internet of Things – ICIOT 2018, Vol. 10972 of Lecture Notes in Computer Science, Springer International Publishing, Cham, 2018.
  * [13] R. W. Sebesta, Concepts of Programming Languages, 12th Edition, Pearson, NY, 2018.
  * [14] D. Arellanes, Composition Machines: Programming Self-Organising Software Models for the Emergence of Sequential Program Spaces, Tech. Rep. arXiv:2108.05402, arXiv (2021).
  * [15] E. Patterson, O. Lynch, J. Fairbanks, Categorical Data Structures for Technical Computing, Compositionality 4 (2022) 5.
  * [16] J. Kock, Whole-grain Petri Nets and Processes, Journal of the ACM 70 (1) (2022) 1–58.
  * [17] D. Arellanes, K.-K. Lau, Exogenous Connectors for Hierarchical Service Composition, in: International Conference on Service-Oriented Computing and Applications (SOCA), IEEE, 2017, pp. 125–132.
  * [18] T. Bures, J. Carlson, I. Crnkovic, S. Sentilles, A. Vulgarakis, ProCom — the Progress Component Model Reference Manual (2008).
  * [19] K. Hanninen, J. Maki-Turja, M. Nolin, M. Lindberg, J. Lundback, K.-L. Lundback, The Rubus component model for resource constrained real-time systems, in: 2008 International Symposium on Industrial Embedded Systems, 2008, pp. 177–183.
  * [20] J.-L. Colaço, B. Pagano, M. Pouzet, SCADE 6: A formal language for embedded critical software development (invited paper), in: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), 2017, pp. 1–11.
  * [21] G. Berry, G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming 19 (2) (1992) 87–152.
  * [22] N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud, The synchronous data flow programming language LUSTRE, Proceedings of the IEEE 79 (9) (1991) 1305–1320.
  * [23] K.-K. Lau, L. Safie, P. Stepan, C. Tran, A component model that is both control-driven and data-driven, in: Proceedings of the 14th international ACM Sigsoft symposium on Component based software engineering, CBSE ’11, Association for Computing Machinery, New York, NY, USA, 2011, pp. 41–50.
  * [24] P. Štěpán, Design pattern solutions as explicit entities in component-based software development, in: Proceedings of the 16th international workshop on Component-oriented programming, Association for Computing Machinery, New York, NY, USA, 2011, pp. 9–16.
  * [25] W. M. P. Van der Aalst, The application of Petri-nets to workflow management, Journal of Circuits, Systems and Computers 8 (1) (1998) 21–66.
  * [26] W. M. P. Van der Aalst, K. M. Van Hee, A. H. M. Ter Hofstede, N. Sidorova, H. M. W. Verbeek, M. Voorhoeve, M. T. Wynn, Soundness of workflow nets: classification, decidability, and analysis, Formal Aspects of Computing 23 (3) (2011) 333–363.
  * [27] O. O. Prisecaru, Resource workflow nets: an approach to workflow modelling and analysis, Enterprise Information Systems 2 (2) (2008) 101–120.
  * [28] M. Ohba, Y. Tanitsu, N. Takimoto, H. Kadota, Functor: A higher-level co-operating program model, Annual Review in Automatic Programming 11 (1981) 21–28.
  * [29] Z. Peng, K. Kuchcinski, Automated transformation of algorithms into register-transfer level implementations, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13 (2) (1994) 150–166.
  * [30] L. Thiele, K. Strehl, D. Ziegengein, R. Ernst, J. Teich, FunState-an internal design representation for codesign, in: IEEE/ACM International Conference on Computer-Aided Design. Digest of Technical Papers, 1999, pp. 558–565.
  * [31] J. C. Baez, J. Master, Open Petri nets, Mathematical Structures in Computer Science 30 (3) (2020) 314–341.
  * [32] P. Baldan, A. Corradini, H. Ehrig, R. Heckel, Compositional semantics for open Petri nets based on deterministic processes, Mathematical Structures in Computer Science 15 (1) (2005) 1–35.
  * [33] E. Best, R. Devillers, M. Koutny, The Box Algebra=Petri Nets+Process Expressions, Information and Computation 178 (1) (2002) 44–100.
  * [34] K. Wolf, Does My Service Have Partners?, in: K. Jensen, W. M. P. van der Aalst (Eds.), Transactions on Petri Nets and Other Models of Concurrency II: Special Issue on Concurrency in Process-Aware Information Systems, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2009, pp. 152–171.
  * [35] P. Baldan, F. Bonchi, F. Gadducci, G. V. Monreale, Modular encoding of synchronous and asynchronous interactions using open Petri nets, Science of Computer Programming 109 (2015) 96–124.
  * [36] R. Bruni, H. Melgratti, U. Montanari, P. Sobocinski, Connector algebras for C/E and P/T nets’ interactions, Logical Methods in Computer Science Volume 9, Issue 3 (2013).
  * [37] E. Kindler, A compositional partial order semantics for Petri net components, in: P. Azéma, G. Balbo (Eds.), Application and Theory of Petri Nets 1997, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1997, pp. 235–252.
  * [38] R. Hinze, D. Marsden, Introducing String Diagrams: The Art of Category Theory, Cambridge University Press, Cambridge, 2023.
  * [39] B. Coecke, T. Fritz, R. W. Spekkens, A mathematical theory of resources, Information and Computation 250 (2016) 59–86.
  * [40] G. Păun, Computing with Membranes, Journal of Computer and System Sciences 61 (1) (2000) 108–143.
  * [41] B. Fong, The algebra of open and interconnected systems, PhD Thesis, University of Oxford (2016).