Bigraphical Nets
Maribel Fernández
Ian Mackie
Matthew Walker
École Normale Supérieure, Paris, France
École Polytechnique, Palaiseau, France
King’s College London, Dept. of Informatics, London WC2R 2LS, UK

Interaction nets are a graphical model of computation, which has been used to define efficient evaluators for functional calculi, and specifically λ -calculi with patterns. However, the flat structure of
interaction nets forces pattern matching and functional behaviour to be encoded at the same level,
losing some potential parallelism. In this paper, we introduce bigraphical nets, or binets for short, as
a generalisation of interaction nets using ideas from bigraphs and port graphs, and we present a formal notation and operational semantics for binets. We illustrate their expressive power by examples
of applications.
Keywords: Interaction Net, Port Graph, Bigraph, Rewriting Calculus.

1

Introduction

Interaction nets [15] are graphical rewrite systems used for the specification of logical proof systems
(e.g., [1, 16]), for the implementation of efficient evaluators for the λ -calculus (e.g., [12, 4, 18]), and for
visual programming (e.g., [13, 20, 19]).
The visual nature of interaction nets makes them well suited as a specification tool, and, since all
the computation steps are explicit and expressed in the same formalism (there is no external machinery), interaction nets are also well suited for the study of the dynamics of programming languages and
rewriting systems [9, 7, 22]. However, interaction nets have some drawbacks. When the nets are large or
growing during reduction, being able to structure the graph is crucial to understand the system modelled,
but interaction nets lack mechanisms to structure the system. Moreover, to formally prove properties of
the system modelled or implement reduction, a formal, algebraic notation, with a precise operational
semantics, should also be available. In this paper, we address these two points:
• First, inspired by Milner’s bigraphs [21], we define a generalisation of interaction nets, which we
call bigraphical nets, or simply binets, where not only the connectivity but also the hierarchical
structure of the system is taken into account. Binets borrow from bigraphs a notion of locality that
is missing in interaction nets.
• Then, we present a formal algebraic notation for binets, with an operational semantics which can
serve as a basis for their implementation.
Related Work. Binets can be seen as hierarchical graph rewriting systems that permit links between
nested nets and external subgraphs (like bigraphs, and unlike hierarchical graphs [6]). Rewriting can take
place across boundaries. Both of these features will be of use in our encoding of the ρ -calculus.
Binets inherit from interaction nets the notion of principal port. But, in contrast with interaction nets,
binets do not force all interactions to be binary, and in contrast with bigraphs, they place restrictions on
reactions to simplify the implementation of rule application.
R. Echahed and D. Plump (Eds.): 7th International Workshop on
Computing with Terms and Graphs
EPTCS 110, 2013, pp. 74–81, doi:10.4204/EPTCS.110.8

c M. Fernández, I. Mackie & M. Walker
This work is licensed under the
Creative Commons Attribution License.

M. Fernández, I. Mackie & M. Walker

75

Interaction nets have been used as an implementation language for functional calculi, and as a tool
to understand their dynamics [12, 4, 17, 18, 8, 7, 11]. Interaction net encodings of the ρ -calculus [5],
an extension of the λ -calculus where we can abstract on patterns, not just on variables, shed light on the
implicit parallelism present in the ρ -calculus, and at the same time, motivate a generalisation of interaction nets, as shown in [10]. In this paper, we develop and formalise this idea. Our main contribution is a
formal syntax and operational semantics for binets, via a textual calculus.
The class of portgraphs defined by Andrei and Kirchner [3] can also be seen as a generalisation of
interaction nets, but although binets are graphs with ports, due to their hierarchical nature they cannot be
defined as portgraphs. It would be interesting to consider a generalisation of portgraphs with a notion of
locality; the inclusion of this feature in PORGY [2] could serve as a starting point for the development
of a specification environment based on binets.

2

Background

Interaction Nets. A system of interaction nets is specified by a set Σ of symbols with fixed arities, and
a set R of interaction rules. An occurrence of a symbol α ∈ Σ is called an agent. If the arity of α is
n, then the agent has n + 1 ports: a principal port depicted by an arrow, and n auxiliary ports. Such an
agent will be drawn in the following way:
xn
x1
···
❅✓✏
α
✒✑
❄

A net N is a graph (not necessarily connected) with agents at the vertices and each edge connecting at
most 2 ports. The ports that are not connected to another agent are free. There are two special instances
of a net: an empty net, and a net consisting only of edges (no agents). The interface of a net is the set of
free ports of agents and free extremes of wires. We refer to [15] for more details.
An interaction rule ((α , β ) =⇒ N) ∈ R replaces a pair of agents (α , β ) ∈ Σ × Σ connected together
on their principal ports (an active pair or redex and written α ⊲⊳ β ) by a net N with the same interface.
Rules must satisfy two conditions: all free ports are preserved during reduction (there are no global
operations: only the part of the net involved in the rewrite is modified), and there is at most one rule
for each pair of agents (such a rule will thus be sometimes denoted by α ⊲⊳ β ). The following diagram
shows the format of interaction rules (N can be any net built from Σ).
y1
xn ✓✏✓✏
xn
❅
..
..
..
✲✛
=⇒
α
β
.
.
.
✒✑✒✑
x1
❅ ym
x1

..
.

N

y1
ym

We use the notation =⇒ for the one-step reduction relation, or ==⇒ if we want to be explicit about
α ⊲⊳β

the rule used, and =⇒∗ for its transitive and reflexive closure. If a net does not contain any active pairs
then we say that it is in normal form. The key property of interaction nets is that reduction is strongly
confluent. We refer the reader to [15] for more details and examples.
Bigraphs. In [21, 14] a notion of graph transformation system is defined, using nested (or hierarchical)
graphs called bigraphs. Bigraphs represent two kinds of structure: locality (nodes may occur inside

Binets

76

other nodes) and connectivity (nodes have ports that may be connected by links). We recall the basic
terminology of bigraphs and refer the reader to [21] for details and examples.
A bigraph is a pair of a place graph and a link graph over the same set of nodes. It has interfaces,
which define the way in which it can be composed with other bigraphs. The place graph, or placing, is
a set of trees with interfaces, and the link graph, or linking, is a hypergraph with interfaces. A placing
has inner and outer interfaces. The inner interface corresponds to the sites where other graphs can be
placed, and the outer interface corresponds to the roots of the trees. The linking also has inner and outer
interfaces, which are names of ports, that is, the points where edges can be attached.
Nodes are labelled by controls with fixed arities; the arity of a control corresponds to the number of
ports of the node. A control is atomic if it cannot contain a nested graph, otherwise it is non-atomic.
The reduction relation is defined by a set of reaction rules, which are pairs of bigraphs (called redex
and reactum). The redex has a width, corresponding to the number of sites it occupies in the outer
bigraph [14]. A non-atomic control K can be specified as active, in which case reactions can occur
inside, or passive, in which case reactions in the internal bigraph can only occur after the control K has
been destroyed.
Interaction nets can be seen as a particular kind of bigraphs without nesting: all controls (called
agents in interaction nets) are atomic, and have a distinguished port (the principal port). Interaction rules
can be seen as reactions in which both redex and reactum have width 1, and redexes are restricted to just
two controls connected by one link through the distinguished ports.

3

Binets

3.1 Informal presentation
Bigraphs [14] introduce a notion of locality (using nesting to indicate that a graph is local to a certain
node) which is missing in interaction nets. In this section, we define binets as a generalisation of interaction nets to incorporate this feature. We start with an informal definition of binets, contrasting them with
interaction nets, before presenting a formal syntax and semantics for them.
A binet is a labelled graph consisting of a set of nodes (also called agents) and a set of edges, which
are attached to nodes at connection points called ports. Each edge connects at most two ports. The label
of a node (i.e., the agent’s name) determines its arity, that is, the number of ports it has. Each agent has a
distinguished port, called the principal port, and a (possibly empty) set of auxiliary ports. An agent can
be located inside another agent, and edges can connect ports of agents situated at different nesting levels
(i.e., edges can cross node boundaries).
Interaction rules, also called reaction rules, define interactions between two agents connected by
their principal ports, or interactions of an agent with its local subnets, preserving the interfaces.
Figure 1 shows a binet representing a ρ -term. Ovals and circles represent agents, their names are
written inside; principal ports are marked with an arrow, the free port at the top is marked by a dangling
edge. The ε -agent is drawn outside the →-agent to exploit a non-strict semantics as early in the reduction
process as possible.
In contrast with interaction nets, the left-hand side of a reaction rule can specify the location in which
the reacting agents are, or the locations contained in these controls, and reactions can take place across
boundaries. However, reduction is still local in the sense that it only affects the nodes that match the left
hand side (no global conditions or updates are specified). The latter point is relevant for implementation.
Agents in binets correspond to the notion of control in bigraphs, and binet reaction rules are a particular class of bigraph reaction rules. Each binet has an associated place graph and link graph, similarly to

M. Fernández, I. Mackie & M. Walker

77

@
@

→

→

ε

G

F
H
I

Figure 1: Binet for the ρ -term (x → H)((F → I)G).
bigraphs. All the examples of bigraphs for the π -calculus and ambient calculus given in [14] (part I) can
be recast as binets by adding principal ports and copy/erase agents (controls) to preserve the interface of
the reactions.
Comparing with the properties of interaction nets, we remark that confluence does not hold in general
for binets, because of the possibility of interactions across boundaries. To study the formal properties of
binet reduction, below we give a calculus for binets.

3.2 A calculus for binets
As Milner [21] stated: “Diagrams are valuable for rapid appreciation of a system’s structure. On the
other hand, algebra is essential to express [...] the ways in which a system may be resolved into components.” In this section we give a formal, algebraic presentation for binets. First we give the syntax of the
language, and then we present an operational semantics for programs written in this language.
Syntax. A textual syntax for binets has to capture, dually, the connections between agents (including
where those connections are principal ports), differentiating between internal or external with respect to
the originating agent and also the locality of agents within a system, i.e., their physical position within
other agents. It is the intention of this syntax to unambiguously state these three properties without
over-complication.
We define below agents and binets over a signature A , L, where A is a set of agent names, each
with an associated arity (n, m) corresponding to the number of ports in its internal and external interface,
respectively, and L is a set of port labels. We assume L ∩ A = 0.
/
Definition 3.1 (Agent) An agent over the signature A , L is written Al hE | I | Ni, where A ∈ A is the
agent name, which determines its arity (n, m), l ∈ L is the label given to the principal port of A, and
the lists I, E of lengths n, m respectively, whose elements are port labels in L, denote the internal and
external agent interfaces; the order denotes the geographic position of the ports (in similar fashion to
interaction nets reading in a clockwise direction from the principal port for external ports and, without
loss of precision, in an arbitrary clockwise direction for interior ports). N is a (possibly empty) list
corresponding to the set of agents located within the agent.
The definition above is inductive (due to the inclusion of the set N within A) but not recursive; agents are
not permitted to be located within themselves.
Definition 3.2 (Binet) A binet over the signature A , L is defined as a set of agents and wires over A ,
L. Agents have already been defined. A wire is an edge joining two ports, written a−b where a, b are the

Binets

78

labels of the ports. Each port label in L occurs at most twice in a binet; the net interface of the binet is
defined as the subset of labels occurring only once.
The binet containing no agents and wires is a special case. For brevity, agents of the form Ai hX | 0/ | 0i
/
will be denoted Ai hX i and the particular case when X = 0/ will be written Ai hi.
A binet, similar to a bigraph, can be decomposed into a place graph and a link graph. The link
graph is explicit in the definition of binet (a binet is a set of agents and wires); the place graph can be
reconstructed from the nesting of agents.
Reduction in binets occurs on active pairs, which are pairs of agents connected via their principal
ports, similarly to interaction nets although significantly rules in binets must be aware of locality context.
More precisely, a rule may affect the agents in the place graph of the active pair. We illustrate it with an
example: the interaction rule presented in [10] between the matching agent, M and any other agent α is
one such occurrence and would be written:
b
hY | 0/ | X i
M a hb | 0/ | X i , α a hY i ⇒ αM

The metavariables X and Y denote a subnet and series of labels respectively that remain unchanged under
graph reduction. Here, the interaction between the agents M and α causes the subgraph located within
the agent M (denoted by X ) to move to the new agent named αM with principal port b.
Contrary to interaction nets, binets permit reductions to occur on certain graph configurations despite
the nonexistence of an active pair, called inactive rewriting in the sequel. See for example the configuration in [10] of an empty matching agent, M, where the net is rewritten to a wire without interaction
through active pairs. This is written as follows (the arrow explicitly shows the type of rule being applied):
M a hbi =⇒inactive a−b
The reduction calculus is defined below, but first we give an example: a reduction sequence for
the binet shown in the previous subsection, representing the ρ -term (x → H)((F → I)G). The textual
representation of each binet is shown in the table below.
@
@

→

⇒∗

⇒∗

⇒∗

M
⊥
→

ε

F

G
M

ε

H

F

ε

H

I

First Binet
→ x ha | b | 0i
/
ε b hi
H a hi
@x hc, di
@y hd, ei
→ y h f | g | F g hii
I f hi
Ge hi

G

I

Second Binet
M a hci
H a hi

Third Binet
H chi

ε d hi

⊥d hi
ε d hi

M f hd | 0/ | F e hii
I f hi
Ge hi

I f hi
ε f hi

H

ε
I

Fully Reduced
H c hi

H

M. Fernández, I. Mackie & M. Walker

79

The second binet contains three active pairs but parallel firing of the rule for agents M f and I f with
the rule for F e and Ge would clearly be incorrect; the general rule for M with α involves a rewriting
that affects all of the nested nets within M, hence a reduction strategy is required. Informally, there is
a choice to delay either active pair until the other has had the opportunity to reduce (although in this
instance either derivation will eventually lead to the intended destruction of this disjoint net). A strategy
is also required in the same configuration to either fire the rule for M a and H a or, as in the example, to
perform an inactive rewrite on M a and reduce it to the wire a − c (see the second textual rule above).
Reduction Rules. Rewrite rules follow the simplicity of interaction nets when the reductum has no
rewrite implications for any agent except for the agent (in the case of inactive rewriting) or agents (active
pair rewriting) directly involved. However, due to the more expressive graph rewriting allowed by binets,
rewrite rules require additional machinery to resolve rewriting of nested agents within the place graph of
the net. Unlike interaction net rules they incorporate metavariables and an additional strategy language.
A priori knowledge of how a rule may affect the surrounding subnet is essential when the rule is
defined. For example, the ε rule within the ρ -calculus scheme is the garbage collection agent responsible
for deleting nets. This agent propagates through subnets, terminating when it forms an active pair with
another ε -agent, hence when defining the interaction of ε and M, the subnets within M should also be
reduced, as follows:

ε a hi, M a hb | 0/ | X i =⇒ ε b hi, X , foreach x in I(X ): ε x hi and ε x̄ hi
where I(X ) is the collection of labelled ports that constitute the interface of the nested net X and x̄ is a
fresh label for the port outside of M that was connected to the interface at x.
The ability of binets to rewrite over agent boundaries means the efficiency (measured in the number
of interactions: typical of interaction nets although cruder for binets) can be improved by rephrasing the
rule to propagate ε only over the wires that are free in this subnet (i.e., those wires that extend beyond
the locality of the M-agent). Each of these wires can be identified by a label appearing only once in the
subnet X and so the above rule can be reinterpreted as follows, where X is removed in one step:

ε a hi, M a hb | 0/ | X i =⇒ ε b hi, foreach x in LX where x is unique: ε x hi
where LX is the multiset of labelled ports in X .
The strategy language is left informal at this stage with full details to be provided in later technical
reports.
Reduction Calculus. The reduction calculus comprises four main parts: firstly populating a set of the
active pairs within a binet and also those (sub)nets that are configured in a way that permits inactive
rewriting. This collection of active pairs and nets is then prioritised according to a given reduction
strategy and, crucially, a collection of agents and nets that can safely be rewritten in parallel is identified.
Then, both active and inactive rewriting is performed and, lastly, a tidying stage is performed to eliminate
every explicitly written wire in the net.
Collect Let CA be the set of labels of principal ports involved in active pairs (these are easily computed:
scan the graph and identify each label l that appears twice as a principal port) and CI be the set of
binets that are isomorphic to the left hand side of inactive rewriting rules (computed using standard
subgraph matching algorithms that can be optimised due to occurrence of principal ports).

Binets

80

Prioritise According to the reduction strategy implemented (weighted, stochastic, typed and so on) group all
safe nets, Cs . A collection of safe nets is one where rewriting (either active or inactive) can occur
in parallel without conflict. The safety, or otherwise, of potential net rewriting is inferred by the
rules: any rule of the form α m h− | − | X i, . . . =⇒ β n h− | − | X ′ i where X 6= X ′ cannot safely be
rewritten at the same time (or in the same pass) as any rule that rewrites within X .
Rewrite For each active pair and agent within Cs , apply rule. For simple rules where rewriting does not
occur within agent borders and there are no internal edges:

α x hu1 , . . . , um i, β x hv1 , . . . , vm i =⇒Γw1 1 hw2 , . . . , w p i, . . . ,
Γwq r hwr+1 , . . . , ws i,
u1 − wi, . . . , um − wi′ ,
v1 − wi′′ , . . . , vn − wi′′′
where Γw are the (possibly empty) agents that are produced on rewriting and w are the intermediary
labels given to the wires of the produced net. Note that the size of w is potentially larger than
the number of ports to the left hand side of the rule. The cases for rules whose agents have
internal ports and rewriting occurs across borders incorporates a richer programmatic syntax and
the resulting operational calculus is more complex.
Tidy If w is a label within Γ and there exists u − w then substitute w by u within Γ (Γ[w/u]).

4

Conclusion

We have presented a new visual language generalising interaction nets to incorporate features from bigraphs. Domains of application include concurrent and reactive systems. Not only can binets model
these systems both graphically and textually, but they are also directly implementable. We are currently
working on the implementation of an abstract machine for binets, inspired by the interaction net machines
defined in [22].

References
[1] Sandra Alves, Maribel Fernández & Ian Mackie (2011): A new graphical calculus of proofs. In Echahed,
editor: Proceedings of TERMGRAPH 2011, EPTCS, pp. 69–84. Available at http://dx.doi.org/10.
4204/EPTCS.48.8.
[2] Oana Andrei, Maribel Fernández, Hélène Kirchner, Guy Melan¸con, Olivier Namet & Bruno Pinaud (2011):
PORGY: Strategy-Driven Interactive Transformation of Graphs. In Echahed, editor: Proceedings of TERMGRAPH 2011, EPTCS, pp. 54–68. Available at http://dx.doi.org/10.4204/EPTCS.48.7.
[3] Oana Andrei & Hélène Kirchner (2008): A Rewriting Calculus for Multigraphs with Ports. Electr. Notes
Theor. Comput. Sci. 219, pp. 67–82. Available at http://dx.doi.org/10.1016/j.entcs.2008.10.
035.
[4] Andrea Asperti, Cecilia Giovannetti & Andrea Naletto (1996): The Bologna Optimal Higher-order Machine. Journal of Functional Programming 6(6), pp. 763–810. Available at http://dx.doi.org/10.1017/
S0956796800001994.
[5] Horatiu Cirstea & Claude Kirchner (2001): The rewriting calculus — Part I and II. Logic Journal of the
Interest Group in Pure and Applied Logics 9(3), pp. 427–498. Available at http://dx.doi.org/10.1093/
jigpal/9.3.339.

M. Fernández, I. Mackie & M. Walker

81

[6] Frank Drewes, Berthold Hoffmann & Detlef Plump (2000): Hierarchical Graph Transformation. In Tiuryn,
editor: Proc. Foundations of Software Science and Computation Structures (FOSSACS 2000), Lecture Notes
in Computer Science 1784, pp. 98–113. Available at http://dx.doi.org/10.1007/3-540-46432-8_7.
[7] M. Fernández & L. Khalil (2003): Interaction nets with McCarthy’s amb: Properties and Applications. Nordic Journal of Computing 10(2), pp. 134–162. Available at http://dx.doi.org/10.1016/
S1571-0661(05)80363-9.
[8] M. Fernández & I. Mackie (1996): From Term Rewriting to Generalised Interaction Nets. In: Proceedings of
PLILP’96. Programming Languages: Implementations, Logics, and Programs, Lecture Notes in Computer
Science 1140, Springer-Verlag. Available at http://dx.doi.org/10.1007/3-540-61756-6_94.
[9] Maribel Fernández & Ian Mackie (1998): Interaction Nets and Term Rewriting Systems. Theoretical Computer Science 190(1), pp. 3–39. Available at http://dx.doi.org/10.1016/S0304-3975(97)00082-0.
[10] Maribel Fernández, Ian Mackie & Fran¸cois Régis Sinot (2006): Interaction Nets vs. the rho-calculus: Introducing Bigraphical Nets. Electr. Notes Theor. Comput. Sci. 154(3), pp. 19–32. Available at http://dx.
doi.org/10.1016/j.entcs.2006.05.004.
[11] Fabien Fleutot (2004): Encoding an Object Calculus into Interaction Nets. In M. Fernandez, editor: Proc.
of the 2nd Int. Workshop on Term Graph Rewriting (TERMGRAPH 2004), ENTCS, Rome. Available at
http://dx.doi.org/10.1016/j.entcs.2005.03.024.
[12] Georges Gonthier, Martı́n Abadi & Jean-Jacques Lévy (1992): The Geometry of Optimal Lambda Reduction.
In: Proceedings of the 19th ACM Symposium on Principles of Programming Languages (POPL’92), ACM
Press, pp. 15–26. Available at http://dx.doi.org/10.1145/143165.143172.
[13] Abubakar Hassan, Ian Mackie & Jorge Sousa Pinto (2008): Visual Programming with Interaction Nets. In
Gem Stapleton, John Howse & John Lee, editors: Diagrams, Lecture Notes in Computer Science 5223,
Springer, pp. 165–171. Available at http://dx.doi.org/10.1007/978-3-540-87730-1_17.
[14] O. Jensen & R. Milner (2004): Bigraphs and mobile processes (revised). Technical Report 580, Computer
Laboratory, University of Cambridge.
[15] Yves Lafont (1990): Interaction Nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL’90), ACM Press, pp. 95–108. Available at http://dx.doi.org/10.1145/
96709.96718.
[16] Yves Lafont (1995): From Proof Nets to Interaction Nets. In J.-Y. Girard, Y. Lafont & L. Regnier, editors:
Advances in Linear Logic, London Mathematical Society Lecture Note Series 222, Cambridge University
Press, pp. 225–247. Available at http://dx.doi.org/10.1017/CBO9780511629150.012.
[17] Ian Mackie (1994): The Geometry of Implementation. Ph.D. thesis, Department of Computing, Imperial
College of Science, Technology and Medicine.
[18] Ian Mackie (2004): Efficient λ -evaluation with interaction nets. In V. van Oostrom, editor: Proc. 15th Int.
Conference on Rewriting Techniques and Applications (RTA’04), Lecture Notes in Computer Science 3091,
Springer-Verlag, pp. 155–169. Available at http://dx.doi.org/10.1007/978-3-540-25979-4_11.
[19] Ian Mackie (2009): A rewriting paradigm for program and algorithm animation. In: VL/HCC, IEEE, pp.
170–173. Available at http://doi.ieeecomputersociety.org/10.1109/VLHCC.2009.5295272.
[20] Ian Mackie (2010): A Visual Model of Computation. In Jan Kratochvı́l, Angsheng Li, Jirı́ Fiala & Petr
Kolman, editors: TAMC, Lecture Notes in Computer Science 6108, Springer, pp. 350–360. Available at
http://dx.doi.org/10.1007/978-3-642-13562-0_32.
[21] Robin Milner (2001): Bigraphical Reactive Systems. In Kim Guldstrand Larsen & Mogens Nielsen, editors:
CONCUR, Lecture Notes in Computer Science 2154, Springer, pp. 16–35. Available at http://dx.doi.
org/10.1007/3-540-44685-0_2.
[22] Jorge Sousa Pinto (2000): Sequential and Concurrent Abstract Machines for Interaction Nets. In J. Tiuryn,
editor: Proceedings of Foundations of Software Science and Computation Structures (FOSSACS), Lecture
Notes in Computer Science 1784, Springer-Verlag, pp. 267–282. Available at http://dx.doi.org/10.
1007/3-540-46432-8_18.

