locus · bigraph tutorial · Chapter I
Milner's bigraphs as they now stand in Lean: what a bigraph is, how the operations build one, when two are the same, and the sixteen laws they obey. Each law is shown on a small office and each is kernel-checked.
A bigraph holds two structures over one set of nodes. The place graph says what is inside what. The link graph says what is connected to what. The two are independent: an agent can be in one room and on a call with someone in another. That independence is the whole idea, and every figure below keeps the two visibly apart.
This is the first of six chapters. The later ones put the bigraphs built here into motion, and test the theory on calculi and on an application:
How this chapter is made. No figure is drawn by hand. Each is computed by
lake exe bigraphdraw from a Lean term. Its regions, nodes, sites, links and names
are read off the bigraph Lean holds (Bg.describe, in
Bigraph/Render.lean). A node is labelled with its kind (its control,
Definition 1) and a name with itself, each exactly as Lean prints them. The label under a figure
is the Lean source of the term drawn, captured as written.
Where a figure outlines part of a bigraph (a room, or one side of a law), the outlined nodes
are that part's own nodes, followed into the whole. Every block of Lean is cut from its source
file by the generator. Every equation drawn is a theorem in Bigraph/Tutorial.lean.
Numbering. Definitions, figures, laws and theorems are numbered separately, and the generator checks every reference. Sources are cited by key and linked to the references: a definition in Jensen and Milner's report as [JM04, Def 9.1], a section of BiCoq as [MAP+25, §6.1]. The generator checks these too: every citation has an entry, and every entry is cited.
Definition 1 (Signature). A signature fixes the kinds of node there may be. Each kind is a control. A control has an arity: the number of ports a node of that control has, by which it is linked to other things. A control is also either atomic (its nodes contain nothing) or not. The activity flag is for reaction rules and plays no part here. [JM04, Def 6.1].
structure Sig (Ctrl : Type) where
/-- `ar K` — the arity, a finite ordinal. -/
ar : Ctrl → Nat
/-- Which controls are atomic. -/
atomic : Ctrl → Bool
/-- Which of the NON-ATOMIC controls are active. The hypothesis is
TR-580's: activity is predicated only of non-atomic controls. -/
active : (K : Ctrl) → atomic K = false → Bool
This chapter uses four controls:
inductive Ctl | building | room | agent | laptop deriving DecidableEq, Repr abbrev Office : Sig Ctl where ar := fun | .building => 0 | .room => 0 | .agent => 1 | .laptop => 1 atomic := fun | .building => false | .room => false | .agent => true | .laptop => true active := fun _ _ => true
building and room have no ports and may contain things.
agent and laptop are atomic and have one port each. Lean writes a
control as Ctl.room, or .room where the type is already known.
Definition 2 (Name set). Names are where links reach the outside
of a bigraph. A name set is a finite set of names, stored as a list without duplicates (BiCoq's
NoDupList, [MAP+25, §3.1]). NameSet.Elt X is the type of the names in
X. In prose a name set is written {x, y}, and
NameSet.singleton a is {a}.
structure NameSet (Name : Type) where
names : List Name
nodup : names.Nodup
deriving Repr
abbrev Elt (X : NameSet Name) : Type := { x : Name // x ∈ X.names }
As lists, [x, y] and [y, x] are different values for the same set.
That matters in §8. The names in this chapter are three, written .x for
Nm.x and so on:
inductive Nm | x | y | z deriving DecidableEq, Repr
Definition 3 (Interface). An interface ⟨m, X⟩ is a
width m and a name set X. [JM04, Def 9.1].
structure Iface (Name : Type) where width : Nat names : NameSet Name
A bigraph has two interfaces, an inner one and an outer one (Definition 4). On the outer face, the width counts the bigraph's regions (its roots), numbered from 0, and the names are its outer names. On the inner face, the width counts its sites, numbered from 0: holes waiting to be filled from below. The names there are its inner names. The abbreviations of [JM04, §9]:
def origin : Iface Name := ⟨0, NameSet.empty⟩ def ofNames (X : NameSet Name) : Iface Name := ⟨0, X⟩ def ofWidth (m : Nat) : Iface Name := ⟨m, NameSet.empty⟩
So ε = ⟨0, ∅⟩ is the origin, with no regions and no names
(Iface.origin, written ε). Iface.ofNames X is
⟨0, X⟩ and Iface.ofWidth m is ⟨m, ∅⟩. This chapter adds
two of its own:
abbrev nm (a : Nm) : Iface Nm := ⟨0, NameSet.singleton a⟩
/-- `⟨1,{a}⟩` — one region, and the name `a`. -/
abbrev reg (a : Nm) : Iface Nm := ⟨1, NameSet.singleton a⟩
nm a = ⟨0, {a}⟩ is the name a alone, with no region.
reg a = ⟨1, {a}⟩ is one region and the name a.
Definition 4 (Bigraph). Bg S I J is the type of
bigraphs over the signature S with inner interface I and outer
interface J. Jensen and Milner write G : I → J
[JM04, Def 6.2].
structure Bg {Ctrl Name : Type} (S : Sig Ctrl) (I J : Iface Name) where
V : Type
E : Type
finV : Finite V
finE : Finite E
ctrl : V → Ctrl
prnt : Place I.width V → Parent V J.width
link : I.names.Elt ⊕ Port S V ctrl → E ⊕ J.names.Elt
acyclic : ∀ v, Acc (Above prnt) v
atomic_childless :
∀ (v : V) (w : Place I.width V),
prnt w = .inl v → S.atomic (ctrl v) = false
V is the set of nodes and E the set of edges. Both are finite:
Finite is an enumeration with decidable equality, BiCoq's
finType [MAP+25, §3.2].ctrl gives each node its control.prnt is the place graph. Every place (a site, or
a node) has a parent, which is a node or a region.link is the link graph. Every point (an inner
name, or a port of a node) is linked either to an edge or to an outer name. A port is a
node together with one of its port numbers, below its arity.acyclic says that following parents upward always ends at a region.
atomic_childless says that an atomic node is nobody's parent.abbrev Place (m : Nat) (V : Type) : Type := Fin m ⊕ V
abbrev Parent (V : Type) (n : Nat) : Type := V ⊕ Fin n
abbrev Port {Ctrl : Type} (S : Sig Ctrl) (V : Type) (ctrl : V → Ctrl) : Type :=
(v : V) × Fin (S.ar (ctrl v))
structure Finite (V : Type) where
elems : List V
complete : ∀ v : V, v ∈ elems
nodup : elems.Nodup
decEq : DecidableEq V
Definition 5 (Atom and ion). Two elementary shapes [JM04, §9]:
atom S K y : ε → ⟨1, {y}⟩ is one node of control
K in one region, with every port linked to the outer name y.ion S K : ⟨1, ∅⟩ → ⟨1, ∅⟩ is one node of control
K in one region, with site 0 inside it. Its two hypotheses say that
K has no ports and is not atomic.def ion (K : Ctrl) (h0 : S.ar K = 0) (hK : S.atomic K = false) :
Bg S (Iface.ofWidth (Name := Name) 1) (Iface.ofWidth 1)
def atom (K : Ctrl) (y : Name) : Bg S Iface.origin ⟨1, NameSet.singleton y⟩
The cast of this chapter is one atom or ion per control. Lean checks the ions' hypotheses by
computation (rfl):
abbrev building : Bg Office (Iface.ofWidth (Name := Nm) 1) (Iface.ofWidth 1) := ion Office .building rfl rfl abbrev room : Bg Office (Iface.ofWidth (Name := Nm) 1) (Iface.ofWidth 1) := ion Office .room rfl rfl abbrev agent (a : Nm) : Bg Office Iface.origin ⟨1, NameSet.singleton a⟩ := atom Office .agent a abbrev laptop (a : Nm) : Bg Office Iface.origin ⟨1, NameSet.singleton a⟩ := atom Office .laptop a
agent .x : ε → ⟨1, {x}⟩ is one region holding an agent node, whose port is linked
to the outer name x. laptop .y is the same shape on y.
room and building : ⟨1, ∅⟩ → ⟨1, ∅⟩ each hold one node with site 0
inside it.Reading a figure. Every figure in this chapter uses the same marks:
⟨m, X⟩ at the right: outer at the top, inner at the bottom
Containment is place; teal is link. Nothing else in a figure carries meaning.
Definition 6 (Composition). For H : Bg S J K and
G : Bg S I J, the composite H ◦ G : Bg S I K plugs G
into H. [JM04, Def 9.1].
def comp {K : Iface Name} (H : Bg S J K) (G : Bg S I J) : Bg S I K
The composite's nodes are those of G and of H together, and so
are its edges. Two things happen at the face they share, J = ⟨m, X⟩:
i of G fills site
i of H, for each i < m. Whatever G
had placed in region i now has as its parent whatever H gave
site i.y of G meets the inner
name y of H. §5 says exactly what that means.The plugged face disappears. H ◦ G is comp H G.
building stands above room, and the dotted line between them is their
shared face ⟨1, ∅⟩. The room's region 0 fills the building's site 0 (dashed
amber). Plugged, building ◦ room is a room in a building. The room's site 0 is now
the composite's only site.Definition 7 (Identity). For every interface
I = ⟨m, X⟩, the identity 𝟙 I : I → I has no nodes and no edges. It
puts site i in region i for each i < m, and links
each inner name x in X to the outer name x. [JM04, Def 9.1].
𝟙 I is id' S I.
def id' (S : Sig Ctrl) (I : Iface Name) : Bg S I I
There is one identity for each interface, and it is shaped by that interface. It has exactly
m regions, each one a hole, and it carries exactly the names in X.
When m = 0 it has no region at all. So 𝟙 (nm .x) = 𝟙 ⟨0, {x}⟩ creates
no region: it is the name x passing from the inner face to the outer, and nothing
else. Composing with an identity changes nothing (Law 2). Here is the identity on two regions and
two names:
abbrev xy : NameSet Nm := ⟨[.x, .y], by decide⟩ abbrev id2 : Bg Office ⟨2, xy⟩ ⟨2, xy⟩ := 𝟙 ⟨2, xy⟩
𝟙 ⟨2, {x, y}⟩: two regions, each holding
the site with the same number, and the names x and y running straight
from the inner face to the outer. It has no nodes and no edges.Definition 8 (Tensor product). Two interfaces whose name sets are
disjoint have a tensor ⟨m, X⟩ ⊗ᵢ ⟨n, Y⟩ = ⟨m + n, X ⊎ Y⟩, where
X ⊎ Y is the union of two disjoint sets (NameSet.dunion). Two bigraphs
G₀ : I₀ → J₀ and G₁ : I₁ → J₁ have a tensor
G₀ ⊗ G₁ : I₀ ⊗ᵢ I₁ → J₀ ⊗ᵢ J₁, which sets them side by side. The regions and sites
of G₁ are numbered after those of G₀, and the names are pooled.
[JM04, Def 9.3].
def tensor (I J : Iface Name) (h : NameSet.Disjoint I.names J.names) : Iface Name :=
⟨I.width + J.width, NameSet.dunion I.names J.names h⟩
def tensor [DecidableEq Name] {I₀ J₀ I₁ J₁ : Iface Name}
(G₀ : Bg S I₀ J₀) (G₁ : Bg S I₁ J₁)
(hI : NameSet.Disjoint I₀.names I₁.names)
(hJ : NameSet.Disjoint J₀.names J₁.names) :
Bg S (I₀.tensor I₁ hI) (J₀.tensor J₁ hJ)
The tensor needs the inner names to be disjoint, and the outer names too. That is
Milner's partiality of the tensor. Here the condition is a class, Apart, and
G₀ ⊗ G₁ is tensor', which leaves both proofs to instance search
([MAP+25, §5.1]; §12 below). The tensor of interfaces has its own symbol, I ⊗ᵢ J
(Iface.tensor'), so ⊗ alone always means bigraphs.
class Apart (I J : Iface Name) : Prop where
out : Disjoint I.names J.names
abbrev tensor' (G₀ : Bg S I₁ J₁) (G₁ : Bg S I₂ J₂) [Apart I₁ I₂] [Apart J₁ J₂] :
Bg S (tensor' I₁ I₂) (tensor' J₁ J₂)
agent .x ⊗ laptop .y : ε → ⟨2, {x, y}⟩.
The agent's region becomes region 0 and the laptop's becomes region 1. The two share no
name.Composition needs the faces to match exactly, so a room cannot take an agent on
x until it carries the name x on its inner face. The tensor provides
it, for a room and likewise for a building:
abbrev roomOn (a : Nm) := room ⊗ 𝟙 (nm a) abbrev buildingOn (a : Nm) := building ⊗ 𝟙 (nm a)
roomOn .x = room ⊗ 𝟙 (nm .x). The room
contributes a region with a site inside it. 𝟙 (nm .x) = 𝟙 ⟨0, {x}⟩ contributes
no region, only the name x passing straight through (Definition 7). Together:
roomOn .x : ⟨1, {x}⟩ → ⟨1, {x}⟩, a room with a hole, and x on both
faces.roomOn .x ◦ agent .x, unplugged and then
plugged. The shared face is ⟨1, {x}⟩. The agent's region 0 fills the room's
site 0 (dashed amber). The agent's outer name x meets the room's inner name
x (dashed teal), which roomOn .x links straight up to its own outer
name x. In the composite the agent is in the room, and its port is linked to
x.In H ◦ G, a point of G linked to an outer name y does
not stop there. It carries on as if it were linked to H's inner name y,
and ends wherever H links that name. That is the whole of “meeting”, and
the Lean says it in one clause:
def liftE0 {E₀ : Type} (A₁ : LinkGraph S Y Z) : E₀ ⊕ Y.Elt → (E₀ ⊕ A₁.E) ⊕ Z.Elt
| .inl e₀ => .inl (.inl e₀)
| .inr y => liftE1 A₁ (A₁.link (.inl y))
Here A₀ is the link graph of G and A₁ that of
H. A link of G to an edge stays as it is. A link of G to
an outer name y is replaced by H's link of its inner name
y, which liftE1 re-tags as a link of the composite. So:
H ◦ G is defined only when
G's outer face is H's inner face: the same width and the
same names. Lean checks this in the types, and refuses a mismatch (the message is pinned in
LocusGate/Bigraph.lean):
/-- error: Application type mismatch: The argument
agent Nm.x
has type
Bg Office ε { width := 1, names := NameSet.singleton Nm.x }
but is expected to have type
Bg Office ?m.4 (Iface.ofWidth 1 ⊗ᵢ nm Nm.y)
in the application
roomOn Nm.y ◦ agent Nm.x -/
#guard_msgs (whitespace := lax) in
#check roomOn .y ◦ agent .xx (Figure 10). Whatever H does with x, it does
to all of them together.H. H can link the
name straight up to the same name (an identity, Figure 6), or to another name, joining it with
others (a substitution, Figure 7). Or it can close the name into an edge (a closure,
Figure 8).Definition 9 (Substitution and closure). These are two of the elementary bigraphs [JM04, §9, §10].
y/X : ⟨0, X⟩ → ⟨0, {y}⟩ links every inner name in
X to the single outer name y./x : ⟨0, {x}⟩ → ε links the inner name x
to an edge, so that x is not visible outside.Neither has nodes or regions.
def subst (S : Sig Ctrl) (y : Name) (X : NameSet Name) :
Bg S (Iface.ofNames X) (Iface.ofNames (NameSet.singleton y))
def closure (S : Sig Ctrl) (x : Name) :
Bg S (Iface.ofNames (NameSet.singleton x)) Iface.origin
abbrev joined := (𝟙 (Iface.ofWidth 2) ⊗ subst Office Nm.z xy) ◦ (agent .x ⊗ laptop .y) abbrev hidden := (𝟙 (Iface.ofWidth 1) ⊗ closure Office Nm.x) ◦ agent .x
agent .x ⊗ laptop .y, with outer names x and y. Above
is the substitution z/{x, y}, set beside 𝟙 ⟨2, ∅⟩ to pass the two
regions through. Each lower name meets the upper name with the same spelling, and the
substitution sends both to z. In joined the agent and the laptop
share one link, z./x
(beside 𝟙 ⟨1, ∅⟩) links its inner name x to an edge, shown as a dot.
The agent's x meets it and goes into the edge. hidden : ε → ⟨1, ∅⟩
has no outer names. The agent's link is still there, but private.Definition 10 (Symmetry). For interfaces I and
J with disjoint names, γ I J : I ⊗ᵢ J → J ⊗ᵢ I has no nodes. Its
sites come in two blocks, I's first and then J's. Its regions come in
the opposite order, J's first and then I's. Each site sits in the
matching region of its own block, and each name goes to itself. [JM04, §10]. γ I J is symmetry S I J with both
disjointness proofs found by search.
def symmetry [DecidableEq Name] (S : Sig Ctrl) (I J : Iface Name)
(hIJ : NameSet.Disjoint I.names J.names) (hJI : NameSet.Disjoint J.names I.names) :
Bg S (I.tensor J hIJ) (J.tensor I hJI)
γ (reg .x) (reg .y). Site 0 (the
reg .x block) sits in region 1, and site 1 sits in region 0: the two blocks of
places have changed sides. The names pass straight through. A name set has no order, so names
have nothing to swap.The tensor refuses shared names, but models share names all the time: two agents on one call.
BiCoq [MAP+25, §6] builds three more operations from ◦ and ⊗ that allow
sharing.
Definition 11 (Parallel product). On interfaces,
⟨m, X⟩ ∥ ⟨n, Y⟩ = ⟨m + n, X ∪ Y⟩: an ordinary union, not a disjoint one.
G₁ ∥ G₂ sets the two side by side like ⊗, but names may be shared,
and a name both have is one name: their links to it are joined. Its side condition is
BiCoq's iToO. If G₁ and G₂ share an inner name, both
must link it to a common outer name. [MAP+25, §6.1].
def par (I J : Iface Name) : Iface Name :=
⟨I.width + J.width, NameSet.union I.names J.names⟩
def ITO (G₁ : Bg S I₁ J₁) (G₂ : Bg S I₂ J₂) : Prop :=
∀ (x₁ : I₁.names.Elt) (x₂ : I₂.names.Elt), x₁.val = x₂.val →
∃ (y₁ : J₁.names.Elt) (y₂ : J₂.names.Elt), y₁.val = y₂.val ∧
G₁.link (.inl x₁) = .inr y₁ ∧ G₂.link (.inl x₂) = .inr y₂
def par (G₁ : Bg S I₁ J₁) (G₂ : Bg S I₂ J₂) (_hito : ITO G₁ G₂) :
Bg S (Iface.par I₁ I₂) (Iface.par J₁ J₂)
As with Apart, the side condition is a class, IToO, and
∥ is par', which leaves it to search.
class IToO (G₁ : Bg S I₁ J₁) (G₂ : Bg S I₂ J₂) : Prop where out : ITO G₁ G₂
Definition 12 (Merge product). merge S n : ⟨n, ∅⟩ → ⟨1, ∅⟩
puts all n sites in one region. 𝟏 is merge S 0: one
region with nothing in it. The merge product G₁ ∣ G₂ is
G₁ ∥ G₂ followed by a merge, so that everything ends up as siblings in one
region. [MAP+25, §6.2].
def merge (S : Sig Ctrl) (n : Nat) :
Bg S (Iface.ofWidth (Name := Name) n) (Iface.ofWidth 1)
def mergeProd (G₁ : Bg S I₁ J₁) (G₂ : Bg S I₂ J₂) (h : ITO G₁ G₂) :
Bg S (Iface.par I₁ I₂) ⟨1, NameSet.union J₁.names J₂.names⟩ :=
comp (J := Iface.par J₁ J₂)
(mergeWrap S (J₁.width + J₂.width) (NameSet.union J₁.names J₂.names)) (par G₁ G₂ h)
Definition 13 (Nesting). For G₁ : ⟨r, ∅⟩ → K and
G₂ : I → ⟨r, Y⟩, the nesting G₁ ⋅ G₂ puts G₂ inside
G₁ and passes G₂'s outer names Y up to the top. Its
side conditions are in the type of G₁: no inner names, and as many sites as
G₂ has regions. [MAP+25, §6.3]. In Lean, G₁ ⋅ G₂ is
nest' G₂ G₁, with the arguments the other way round so that the elaborator meets
the inner factor first.
def nestCtx {J K : Iface Name} (G₁ : Bg S ⟨J.width, NameSet.empty⟩ K) :
Bg S J ⟨K.width, NameSet.union K.names J.names⟩ :=
par G₁ (id' S (Iface.ofNames J.names)) (ITO_of_disjoint (NameSet.disjoint_empty_left _))
def nest {I J K : Iface Name} (G₁ : Bg S ⟨J.width, NameSet.empty⟩ K) (G₂ : Bg S I J) :
Bg S I ⟨K.width, NameSet.union K.names J.names⟩ :=
comp (nestCtx G₁) G₂
The meeting room is two agents merged into one region, nested in a room:
abbrev meeting := room ⋅ (agent .x ∣ agent .x)
∥ they keep separate regions and share the name x; ⊗
would refuse them (§12). With ∣ they also share a region. In
meeting both are inside a room, and x still reaches the top.The office puts three such rooms in a building:
abbrev study := room ⋅ laptop .y abbrev lobby := room ⋅ agent .z abbrev office := building ⋅ ((meeting ∣ study) ∣ lobby)
office : ε → ⟨1, {x, y, z}⟩. Each room is
outlined and labelled with the term it comes from. The outlines are computed: each one encloses
the nodes of meeting, study or lobby, followed into
office through ⋅ and ∣.A bigraph has several kinds of label, and everyday words run them together. Keeping them apart is the whole of this section:
| What | Example | Kept by ⟪G⟫? |
|---|---|---|
Node identity: which element of the node set V a node
is | the agent of agent .x is (); in 𝟙 (reg .x) ◦ agent
.x the same agent is .inl () | no |
| Control: what kind of node it is (Definition 1) | agent,
room: the label on every node in every figure | yes |
Edge identity: which element of the edge set E an edge
is | the dot in Figure 8 | no; idle edges are dropped altogether |
| Name: the label of a link on an interface, inner or outer | x, y, z | yes, as a set |
| Place number: the position of a region or a site | region 0, site 1 | yes |
So a node has an identity and a control, but no name. The two agents in the meeting room are two nodes with the same control, linked to the same name. Names belong to interfaces, never to nodes, and an edge has an identity but no name. The figures draw controls and names and never identities: two bigraphs that differ only in identities are drawn the same.
Two bigraphs that differ only in the identities of their nodes and edges describe the
same thing. For example, 𝟙 (reg .x) ◦ agent .x has node set
Unit ⊕ Empty and its one node is .inl (), while agent .x
has node set Unit and its node is (). Law 2 says they are the same.
Definition 14 (Support equivalence). G ≏ H for
G H : Bg S I J is a bijection between their nodes and one between their edges,
preserving controls, parents and links. The bijections change identities only: every name is
carried to itself, and every place number to itself. [MAP+25, §4.1].
structure SupportEquiv (G H : Bg S I J) where
nodeTo : G.V → H.V
nodeFrom : H.V → G.V
edgeTo : G.E → H.E
edgeFrom : H.E → G.E
node_left : ∀ v, nodeFrom (nodeTo v) = v
node_right : ∀ v, nodeTo (nodeFrom v) = v
edge_left : ∀ e, edgeFrom (edgeTo e) = e
edge_right : ∀ e, edgeTo (edgeFrom e) = e
ctrl_eq : ∀ v, H.ctrl (nodeTo v) = G.ctrl v
prnt_eq : ∀ w, H.prnt (PlaceGraph.mapPlace nodeTo w)
= PlaceGraph.mapParent nodeTo (G.prnt w)
/-- **The link map is constrained too.** Without this the relation says
nothing about the link graph, and a "support equivalence" that
ignores half the bigraph is not one. -/
link_eq : ∀ p q, SamePoint nodeTo p q → H.link q = mapLink edgeTo (G.link p)
mapPlace, mapParent and mapLink apply the
bijections inside places, parents and links. SamePoint says that two points
correspond under the node bijection.
Interfaces need the same care. BiCoq [MAP+25, §4]: “the set of names {a,b} can be represented
as the NoDupList [a,b] as well as [b,a] … even though we do not care about ordering in a
set.” So BiCoq's equivalence, SetEquiv, also relates two bigraphs whose
faces are the same as sets (SameIface), with every site and every name carried to
itself.
def SameIface (I J : Iface Name) : Prop :=
I.width = J.width ∧ ∀ a, a ∈ I.names.names ↔ a ∈ J.names.names
inductive SetEquiv : Packed S Name → Packed S Name → Prop
| mk {I J I' J' : Iface Name} {G : Bg S I J} {H : Bg S I' J'}
(hI : SameIface I I') (hJ : SameIface J J')
(e : Nonempty (SupportEquivI (IfaceIso.ofMem hI.1 hI.2) (IfaceIso.ofMem hJ.1 hJ.2) G H)) :
SetEquiv ⟨I, J, G⟩ ⟨I', J', H⟩
Packed S Name is a bigraph together with its two interfaces, so that bigraphs
of different types can be compared.
Milner's theory goes one step further. An edge that no point links to is idle, and “an idle edge serves no useful purpose, but may be created by composition” [JM04, §8]. Closing a name that nothing uses leaves one behind (Figure 13). So abstract bigraphs forget idle edges as well.
Definition 15 (Idle edge; lean-support equivalence). An edge is
used when some point links to it, and idle otherwise. lean G is
G with its idle edges discarded: the same nodes, places and links, and only the used
edges. Two bigraphs are lean-support equivalent, G ≎ H, when lean G
≏ lean H: in the words of [JM04, Def 9.12], “if after discarding any idle
edges they are support equivalent”. BiCoq leans a bigraph the same way
[MAP+25, §4.2].
def EdgeUsed (G : Bg S I J) (e : G.E) : Prop :=
∃ p : I.names.Elt ⊕ Port S G.V G.ctrl, G.link p = .inl e
def Used (G : Bg S I J) : Type := {e : G.E // G.EdgeUsed e}
def lean (G : Bg S I J) : Bg S I J where
V := G.V
E := G.Used
finV := G.finV
finE := G.usedFin
ctrl := G.ctrl
prnt := G.prnt
link := G.leanLink
acyclic := G.acyclic
atomic_childless := G.atomic_childless
usedFin lists the used edges. It decides whether an edge is used by comparing
edges only, using the decidable equality every Finite carries.
leanLink is G's own link, with each edge now known to be used. Across
set-equal faces, as BiCoq's equivalence is:
def Packed.lean (P : Packed S Name) : Packed S Name := ⟨P.inner, P.outer, P.bg.lean⟩ def LeanSetEquiv (P Q : Packed S Name) : Prop := SetEquiv P.lean Q.lean
The library also states ≎ directly, as a bijection between the used edges
(LeanSupportEquiv). The two definitions are proved to agree, so there is one
relation:
theorem leanSupportEquiv_iff : Nonempty (G ≎ H) ↔ Nonempty (G.lean ≏ H.lean)
[JM04, Def 9.12] calls ≎ “clearly a static congruence”. Here
that is proved.
Leaning a composite gives the same result as composing the leaned factors and leaning again
(leanComp), and likewise for ⊗. So factors equivalent under ≎ give
composites and tensors equivalent under ≎:
theorem leanComp_congr {I J K I' J' K' : Iface Name} {G : Bg S I J} {H : Bg S J K}
{G' : Bg S I' J'} {H' : Bg S J' K'}
(hG : LeanSetEquiv ⟨I, J, G⟩ ⟨I', J', G'⟩) (hH : LeanSetEquiv ⟨J, K, H⟩ ⟨J', K', H'⟩) :
LeanSetEquiv ⟨I, K, comp H G⟩ ⟨I', K', comp H' G'⟩
Definition 16 (Abstract bigraph). An abstract bigraph is an
equivalence class under LeanSetEquiv: the abstract bigraphs of
[JM04, Def 9.12].
⟪G⟫ is the class of G. Abstract composition ⟪H⟫ ⊚ ⟪G⟫ is defined when G's
outer face and H's inner face are the same as sets. It is partial, so its value is
an Option: some of the class of the composite, or
none. leanSetoid is LeanSetEquiv, packaged as an
equivalence relation.
def Abstract (S : Sig Ctrl) (Name : Type) : Type 1 := Quotient (leanSetoid S Name)
def Abstract.mk {I J : Iface Name} (G : Bg S I J) : Abstract S Name :=
Quotient.mk (leanSetoid S Name) ⟨I, J, G⟩
def Abstract.comp : Abstract S Name → Abstract S Name → Option (Abstract S Name)
⟪G⟫ forgets the identities of nodes and edges, and idle edges. It keeps
everything else, both interfaces with their names included. That is what makes abstract
composition definable. ⟪H⟫ ⊚ ⟪G⟫ is defined exactly when G's outer face
and H's inner face have the same width and the same names, and then it is the class
of the composite. Every representative of ⟪G⟫ has the same faces
(LeanSetEquiv.inner, LeanSetEquiv.outer), so whether the composite is
defined does not depend on the representative chosen. When it is defined, different
representatives give the same class (leanCompSet_congr).
Theorem 1 (Abstract bigraphs keep their names). Faces that meet
compose; faces that do not, do not; and an agent on x is not an agent on
y.
theorem ex_meet : ⟪roomOn .x⟫ ⊚ ⟪agent .x⟫ = some ⟪roomOn .x ◦ agent .x⟫ := Abstract.comp_mk _ _ theorem ex_no_meet : ⟪roomOn .x⟫ ⊚ ⟪agent .y⟫ = none := by decide theorem ex_names_kept : ⟪agent .x⟫ ≠ ⟪agent .y⟫ := by intro h have hx := ((LeanSetEquiv.outer (Quotient.exact h)).2 .x).mp (List.mem_singleton_self _) exact absurd hx (by decide)
If ⟪·⟫ forgot names, the second and third would contradict each other.
⟪agent .x⟫ and ⟪agent .y⟫ would be one class, and composing
⟪roomOn .x⟫ with it would be both defined and undefined.
Names have no order in Milner's theory, concrete or abstract: an interface's names are a
set. Order enters only through this Lean encoding, which stores a set as a list without
duplicates (Definition 2). A bigraph's type Bg S I J contains its two interfaces as
values, and ⟨0, [x, y]⟩ and ⟨0, [y, x]⟩ are different values. So list
order shows up in exactly one place: in whether two concrete bigraphs have matching types, and so
in whether they can be composed or compared.
It never shows up in what a bigraph does. A link goes to a name, not to a position in a list,
so listing the names in another order changes no link. That is how γ is defined
(Definition 10). It swaps the two blocks of places, which are positional, and sends every name to
itself. On interfaces with names but no places there is nothing to swap, so γ does
nothing at all: its two faces list the same names in two orders.
γ (nm .x) (nm .y) and
𝟙 (nm .x ⊗ᵢ nm .y). Both pass x and y straight through,
and neither has a place. The faces are printed in the order Lean lists them: γ's
outer face lists y first, because J ⊗ᵢ I lists J's names
first.Concretely the order is part of the type, so the identity cannot follow γ
directly. Lean refuses, and the message shows the two orders (pinned in
LocusGate/Bigraph.lean):
/-- error: Application type mismatch: The argument γ (nm Nm.x) (nm Nm.y) has type Bg ?m.19 (nm Nm.x ⊗ᵢ nm Nm.y) (nm Nm.y ⊗ᵢ nm Nm.x) but is expected to have type Bg Office ?m.4 (nm Nm.x ⊗ᵢ nm Nm.y) in the application 𝟙 (nm Nm.x ⊗ᵢ nm Nm.y) ◦ γ (nm Nm.x) (nm Nm.y) -/ #guard_msgs (whitespace := lax) in #check (𝟙 (nm .x ⊗ᵢ nm .y) : Bg Office _ _) ◦ γ (nm .x) (nm .y)
Abstractly the two orders are one set, so the classes are equal and the composite is defined:
Theorem 2 (Name order is not abstract). γ on two names
is the identity, and the composition refused above is defined.
theorem ex_gamma_names : ⟪γ (nm .x) (nm .y)⟫ = (⟪𝟙 (nm .x ⊗ᵢ nm .y)⟫ : Abstract Office Nm) :=
Quotient.sound (setEquiv_symmetry_id Office (NameSet.singleton Nm.x) (NameSet.singleton Nm.y) _ _).toLean
theorem ex_gamma_compose :
(⟪𝟙 (nm .x ⊗ᵢ nm .y)⟫ ⊚ ⟪γ (nm .x) (nm .y)⟫ : Option (Abstract Office Nm))
= some ⟪𝟙 (nm .x ⊗ᵢ nm .y)⟫ := by
rw [ex_gamma_names, Abstract.comp_mk, Abstract.id_comp]
The general form is setEquiv_symmetry_id: [JM04, §10] defines
γ_{I,J} as γ_{m,n} ⊗ id_{X⊎Y}, the identity on names. Under equality of
the encoded interfaces it fails as soon as both name sets are non-empty
(not_strictEquiv_symmetry_id).
This is why abstract bigraphs are taken across interfaces that are the same as sets
(SameIface), with every name carried to itself. It removes the one thing the list
encoding adds, and nothing more. Renaming x to y is never implicit: it
takes a substitution (Definition 9).
Discarding idle edges makes a real difference. One of the link axioms of [JM04, §10] holds only because of it:
Theorem 3 (Idle edges are forgotten). Milner's link axiom
/y ◦ y = id_ϵ holds for abstract bigraphs. Here y : ε → ⟨0, {y}⟩ is
the empty substitution subst S y ∅: the name y, linked to nothing
(Definition 9). It does not hold under BiCoq's equivalence alone.
theorem close_idle (y : Name) : ⟪closure S y ◦ subst S y ∅⟫ = (⟪𝟙 ε⟫ : Abstract S Name)
theorem ex_close_idle :
⟪closure Office Nm.x ◦ subst Office Nm.x ∅⟫ = (⟪𝟙 ε⟫ : Abstract Office Nm) :=
close_idle _
theorem ex_close_idle_bicoq :
¬ SetEquiv ⟨_, _, closure Office Nm.x ◦ subst Office Nm.x ∅⟩ ⟨_, _, (𝟙 ε : Bg Office ε ε)⟩ :=
not_setEquiv_closure_idle _
x. Unplugged, the
closure /x stands above the empty substitution. The substitution's outer name
x has no points; it meets the closure's inner name x, which the
closure links to an edge. Plugged, that edge (the dot) has nothing linked to it: it is idle.
Discarding it leaves 𝟙 ε, which has nothing to draw. BiCoq's ≏ keeps the edge, so
it cannot identify the two.Every symbol introduced so far, as Lean declares it (open Bigraph brings them
into scope):
scoped infixr:80 " ◦ " => comp scoped infixr:70 " ⊗ " => Bg.tensor' scoped infixr:70 " ⊗ᵢ " => Iface.tensor' scoped infixl:65 " ∥ " => par' scoped infixl:65 " ∣ " => mergeProd' scoped notation:75 G₁:76 " ⋅ " G₂:75 => nest' G₂ G₁ scoped notation:max "𝟙 " I:max => id' _ I scoped syntax:max "γ " term:max ppSpace term:max : term scoped macro_rules | `(γ $I $J) => `(symmetry _ $I $J out out) scoped notation "𝟏" => merge _ 0 scoped notation "ε" => origin scoped notation "⟪" G "⟫" => Abstract.mk G scoped infixr:80 " ⊚ " => Abstract.comp
Nesting is not a new primitive. It is defined as a composition (Definition 13), and Lean accepts the equation by unfolding alone:
Theorem 4 (Nesting is composition). For
G₁ : ⟨r, ∅⟩ → K and G₂ : I → ⟨r, Y⟩,
G₁ ⋅ G₂ = (G₁ ∥ 𝟙 ⟨0, Y⟩) ◦ G₂.
theorem nesting_is_composition {C N : Type} [DecidableEq N] {S : Sig C} {I J K : Iface N}
(G₁ : Bg S ⟨J.width, ∅⟩ K) (G₂ : Bg S I J) :
G₁ ⋅ G₂ = (G₁ ∥ 𝟙 (Iface.ofNames J.names)) ◦ G₂ := rfl
x passing through, is composed with the two merged agents. The agents' region
fills the room's site, and their x meets the passing x and goes to
the top. The generator checks by rfl that this composite is
meeting.So composition can do everything nesting does. The converse fails. Composition can join
names (Figure 7) and close them (Figure 8). Nesting can do neither, because it passes the inner
bigraph's outer names up unchanged: every outer name of G₂ is an outer name of
G₁ ⋅ G₂.
Theorem 5 (Composition is not nesting). No nesting of
agent .x is hidden, even as abstract bigraphs.
theorem nesting_cannot_close {K : Iface Nm} (G₁ : Bg Office ⟨1, ∅⟩ K) :
⟪G₁ ⋅ agent .x⟫ ≠ ⟪hidden⟫ := by
intro h
have hx := ((LeanSetEquiv.outer (Quotient.exact h)).2 .x).mp
(NameSet.mem_union_right (List.mem_singleton_self _))
simp [Iface.tensor', Iface.tensor, NameSet.dunion, Iface.ofWidth, Iface.origin,
NameSet.empty] at hx
The proof reads off the outer names. x is an outer name of every
G₁ ⋅ agent .x, while hidden has none, and ≎ preserves the set of
outer names.
So composition is the primitive, and it must stay. Nesting is a convenience
for the commonest kind of containment, where what is put inside keeps its names visible
outside. With composition alone, that case needs an identity 𝟙 ⟨0, Y⟩ beside the
container every time, sized to the contents' names (as in roomOn, Figure 5).
Nesting writes it once, in its definition, and carries its side conditions in its type.
Each card states a law for all bigraphs, gives an instance on the office's cast, and draws the instance.
Sixteen laws, stated as twenty-one theorems, because five of them have a left and a right form. Laws 1–9 are the axioms of a symmetric partial monoidal category, as BiCoq lists them [MAP+25, §2.3]; for the fact that abstract bigraphs form such a category, BiCoq cites Milner's book [Mil09, Theorem 2.20]. All of the nine except S4 are among the categorical axioms of [JM04, §10]. Laws 10–16 are the laws of the derived operations [MAP+25, §6].
variable (f : Bg S I J) (g : Bg S J K) (h : Bg S K L) theorem C2 : ⟪h ◦ (g ◦ f)⟫ = ⟪(h ◦ g) ◦ f⟫
An agent in a room in a building. Whether the agent goes into the room first, or the room goes into the building first, the result is the same.
theorem ex_C2 :
⟪buildingOn .x ◦ (roomOn .x ◦ agent .x)⟫ = ⟪(buildingOn .x ◦ roomOn .x) ◦ agent .x⟫ :=
C2 _ _ _
theorem C3_left : ⟪𝟙 J ◦ f⟫ = ⟪f⟫ theorem C3_right : ⟪f ◦ 𝟙 I⟫ = ⟪f⟫
Plugging the agent into an identity changes nothing. Plugging nothing into the agent changes nothing either.
theorem ex_C3_left : ⟪𝟙 (reg .x) ◦ agent .x⟫ = ⟪agent .x⟫ := C3_left _ theorem ex_C3_right : ⟪agent .x ◦ 𝟙 ε⟫ = ⟪agent .x⟫ := C3_right _
𝟙 (reg .x) above agent .x,
and the result. The identity's site takes the agent's region, and its x passes
the agent's x straight up.variable (f : Bg S I₀ J₀) (g : Bg S I₁ J₁) (k : Bg S I₂ J₂)
theorem M1 [Apart I₀ I₁] [Apart I₀ I₂] [Apart I₁ I₂] [Apart J₀ J₁] [Apart J₀ J₂] [Apart J₁ J₂] :
⟪(f ⊗ g) ⊗ k⟫ = ⟪f ⊗ (g ⊗ k)⟫
Three things in three regions. Bracketing the first two, or the last two, gives the same row.
theorem ex_M1 : ⟪(agent .x ⊗ laptop .y) ⊗ agent .z⟫ = ⟪agent .x ⊗ (laptop .y ⊗ agent .z)⟫ := M1 _ _ _
theorem M2_left : ⟪𝟙 ε ⊗ f⟫ = ⟪f⟫ theorem M2_right : ⟪f ⊗ 𝟙 ε⟫ = ⟪f⟫
ε has no regions and no names, so its identity has nothing to set beside
anything.
theorem ex_M2_left : ⟪𝟙 ε ⊗ agent .x⟫ = ⟪agent .x⟫ := M2_left _ theorem ex_M2_right : ⟪agent .x ⊗ 𝟙 ε⟫ = ⟪agent .x⟫ := M2_right _
𝟙 ε has no regions, no nodes and no
names. The dotted box marks the empty drawing.variable (A₀ : Bg S I₀ J₀) (B₀ : Bg S J₀ K₀) (A₁ : Bg S I₁ J₁) (B₁ : Bg S J₁ K₁)
theorem M3 [Apart I₀ I₁] [Apart J₀ J₁] [Apart K₀ K₁] :
⟪(B₀ ◦ A₀) ⊗ (B₁ ◦ A₁)⟫ = ⟪(B₀ ⊗ B₁) ◦ (A₀ ⊗ A₁)⟫
Fill each room and then set the rooms side by side, or set the empty rooms side by side and then fill both. BiCoq reports this proof as “the longest, with a lot of variables and cases” [MAP+25, §5.3.1]. Here it took a place half and a link half.
theorem ex_M3 :
⟪(roomOn .x ◦ agent .x) ⊗ (roomOn .y ◦ laptop .y)⟫
= ⟪(roomOn .x ⊗ roomOn .y) ◦ (agent .x ⊗ laptop .y)⟫ :=
M3 _ _ _ _
theorem S1 : ⟪γ I ε⟫ = (⟪𝟙 I⟫ : Abstract S Name)
ε has no places to swap.
theorem ex_S1 : ⟪γ (reg .x) ε⟫ = (⟪𝟙 (reg .x)⟫ : Abstract Office Nm) := S1
γ (reg .x) ε and
𝟙 (reg .x): both put site 0 in region 0 and pass x
through.theorem S2 [Apart I J] : ⟪γ J I ◦ γ I J⟫ = (⟪𝟙 (I ⊗ᵢ J)⟫ : Abstract S Name)
Two crossings pull straight.
theorem ex_S2 : ⟪γ (reg .y) (reg .x) ◦ γ (reg .x) (reg .y)⟫
= (⟪𝟙 (reg .x ⊗ᵢ reg .y)⟫ : Abstract Office Nm) := S2
theorem S3 (f : Bg S I₀ I₁) (g : Bg S J₀ J₁) [Apart I₀ J₀] [Apart I₁ J₁] :
⟪γ I₁ J₁ ◦ (f ⊗ g)⟫ = ⟪(g ⊗ f) ◦ γ I₀ J₀⟫
Make the agent and the laptop and then swap their regions, or swap first and make them the other way round. The links go with the nodes, not with the regions.
theorem ex_S3 : ⟪γ (reg .x) (reg .y) ◦ (agent .x ⊗ laptop .y)⟫
= ⟪(laptop .y ⊗ agent .x) ◦ γ ε ε⟫ := S3 _ _
γ ε ε has no places and no names: it is the empty
drawing.theorem S4 [Apart I J] [Apart I K] [Apart J K] :
(⟪γ I K ⊗ 𝟙 J⟫ ⊚ ⟪𝟙 I ⊗ γ J K⟫ : Option (Abstract S Name)) = some ⟪γ (I ⊗ᵢ J) K⟫
Moving K past I and J in one crossing is the same as
moving it past J and then past I. The two factors meet at
(I ⊗ᵢ K) ⊗ᵢ J and I ⊗ᵢ (K ⊗ᵢ J). These are the same set, listed
differently, so the law composes them with ⊚ (Definition 16).
theorem ex_S4 :
(⟪γ (reg .x) (reg .z) ⊗ 𝟙 (reg .y)⟫ ⊚ ⟪𝟙 (reg .x) ⊗ γ (reg .y) (reg .z)⟫
: Option (Abstract Office Nm)) = some ⟪γ (reg .x ⊗ᵢ reg .y) (reg .z)⟫ := S4
variable (G₁ : Bg S I₁ J₁) (G₂ : Bg S I₂ J₂) (G₃ : Bg S I₃ J₃) theorem par_tensor [Apart I₁ I₂] [Apart J₁ J₂] : ⟪G₁ ∥ G₂⟫ = ⟪G₁ ⊗ G₂⟫
When nothing is shared, ∥ has nothing to join.
theorem ex_par_tensor : ⟪agent .x ∥ laptop .y⟫ = ⟪agent .x ⊗ laptop .y⟫ := par_tensor _ _
theorem par_unit_left : ⟪𝟙 ε ∥ G₁⟫ = ⟪G₁⟫ theorem par_unit_right : ⟪G₁ ∥ 𝟙 ε⟫ = ⟪G₁⟫
As with the tensor, the empty interface adds no region and no name.
theorem ex_par_unit_left : ⟪𝟙 ε ∥ agent .x⟫ = ⟪agent .x⟫ := par_unit_left _ theorem ex_par_unit_right : ⟪agent .x ∥ 𝟙 ε⟫ = ⟪agent .x⟫ := par_unit_right _
theorem par_assoc [IToO G₁ G₂] [IToO G₂ G₃] [IToO G₁ G₃] :
⟪(G₁ ∥ G₂) ∥ G₃⟫ = ⟪G₁ ∥ (G₂ ∥ G₃)⟫
Two agents on the same name x, then a laptop. ⊗ would refuse the
first step. ∥ joins the shared name into one link, and the grouping does not
matter.
theorem ex_par_assoc :
⟪(agent .x ∥ agent .x) ∥ laptop .y⟫ = ⟪agent .x ∥ (agent .x ∥ laptop .y)⟫ :=
par_assoc _ _ _
theorem merge_unit_left {Y : NameSet Name} (G : Bg S I ⟨1, Y⟩) : ⟪𝟏 ∣ G⟫ = ⟪G⟫
theorem merge_unit_right {Y : NameSet Name} (G : Bg S I ⟨1, Y⟩) : ⟪G ∣ 𝟏⟫ = ⟪G⟫
Merging 𝟏 in adds its contents, which are none. The law needs
G to have exactly one region, because a merge always produces one. Its type says
so: G : Bg S I ⟨1, Y⟩.
theorem ex_merge_unit_left : ⟪𝟏 ∣ meeting⟫ = ⟪meeting⟫ := merge_unit_left _ theorem ex_merge_unit_right : ⟪meeting ∣ 𝟏⟫ = ⟪meeting⟫ := merge_unit_right _
𝟏 is one empty region.theorem merge_assoc [IToO G₁ G₂] [IToO G₂ G₃] [IToO G₁ G₃] :
⟪(G₁ ∣ G₂) ∣ G₃⟫ = ⟪G₁ ∣ (G₂ ∣ G₃)⟫
Either way, everything ends up in one region.
theorem ex_merge_assoc :
⟪(agent .x ∣ agent .x) ∣ laptop .y⟫ = ⟪agent .x ∣ (agent .x ∣ laptop .y)⟫ :=
merge_assoc _ _ _
theorem nest_unit_left (G : Bg S I J) : ⟪𝟙 ⟨J.width, ∅⟩ ⋅ G⟫ = ⟪G⟫
theorem nest_unit_right {s : Nat} (G : Bg S ⟨s, ∅⟩ K) : ⟪G ⋅ 𝟙 ⟨s, ∅⟩⟫ = ⟪G⟫
Nesting the agent in an identity leaves the agent. Nesting an identity in the room leaves the room, with its site still there.
theorem ex_nest_unit_left : ⟪𝟙 (Iface.ofWidth 1) ⋅ agent .x⟫ = ⟪agent .x⟫ := nest_unit_left _ theorem ex_nest_unit_right : ⟪room ⋅ 𝟙 (Iface.ofWidth 1)⟫ = ⟪room⟫ := nest_unit_right _
theorem nest_assoc (G₁ : Bg S ⟨J₂.width, ∅⟩ K) (G₂ : Bg S ⟨J₃.width, ∅⟩ J₂) (G₃ : Bg S I J₃) :
⟪(G₁ ⋅ G₂) ⋅ G₃⟫ = ⟪G₁ ⋅ (G₂ ⋅ G₃)⟫
An agent in a room in a building again, this time by nesting. The agent's x
reaches the top whichever way it is grouped. Compare Law 1, where the room and the building had
to carry x through themselves.
theorem ex_nest_assoc : ⟪(building ⋅ room) ⋅ agent .x⟫ = ⟪building ⋅ (room ⋅ agent .x)⟫ := nest_assoc _ _ _
Every instance above is built from the office's own parts: its building and rooms, its three agents, its laptop and its three names. So the office holds all sixteen laws at once, and Lean says so in one theorem.
Theorem 6 (The office obeys every law). The conjunction of the twenty-one instances.
theorem office_obeys_every_law :
-- the category
⟪buildingOn .x ◦ (roomOn .x ◦ agent .x)⟫ = ⟪(buildingOn .x ◦ roomOn .x) ◦ agent .x⟫ ∧
⟪𝟙 (reg .x) ◦ agent .x⟫ = ⟪agent .x⟫ ∧ ⟪agent .x ◦ 𝟙 ε⟫ = ⟪agent .x⟫ ∧
-- the tensor
⟪(agent .x ⊗ laptop .y) ⊗ agent .z⟫ = ⟪agent .x ⊗ (laptop .y ⊗ agent .z)⟫ ∧
⟪𝟙 ε ⊗ agent .x⟫ = ⟪agent .x⟫ ∧ ⟪agent .x ⊗ 𝟙 ε⟫ = ⟪agent .x⟫ ∧
⟪(roomOn .x ◦ agent .x) ⊗ (roomOn .y ◦ laptop .y)⟫
= ⟪(roomOn .x ⊗ roomOn .y) ◦ (agent .x ⊗ laptop .y)⟫ ∧
-- the symmetry
⟪γ (reg .x) ε⟫ = (⟪𝟙 (reg .x)⟫ : Abstract Office Nm) ∧
⟪γ (reg .y) (reg .x) ◦ γ (reg .x) (reg .y)⟫ = (⟪𝟙 (reg .x ⊗ᵢ reg .y)⟫ : Abstract Office Nm) ∧
⟪γ (reg .x) (reg .y) ◦ (agent .x ⊗ laptop .y)⟫ = ⟪(laptop .y ⊗ agent .x) ◦ γ ε ε⟫ ∧
(⟪γ (reg .x) (reg .z) ⊗ 𝟙 (reg .y)⟫ ⊚ ⟪𝟙 (reg .x) ⊗ γ (reg .y) (reg .z)⟫
: Option (Abstract Office Nm)) = some ⟪γ (reg .x ⊗ᵢ reg .y) (reg .z)⟫ ∧
-- parallel, merge, nest
⟪agent .x ∥ laptop .y⟫ = ⟪agent .x ⊗ laptop .y⟫ ∧
⟪𝟙 ε ∥ agent .x⟫ = ⟪agent .x⟫ ∧ ⟪agent .x ∥ 𝟙 ε⟫ = ⟪agent .x⟫ ∧
⟪(agent .x ∥ agent .x) ∥ laptop .y⟫ = ⟪agent .x ∥ (agent .x ∥ laptop .y)⟫ ∧
⟪𝟏 ∣ meeting⟫ = ⟪meeting⟫ ∧ ⟪meeting ∣ 𝟏⟫ = ⟪meeting⟫ ∧
⟪(agent .x ∣ agent .x) ∣ laptop .y⟫ = ⟪agent .x ∣ (agent .x ∣ laptop .y)⟫ ∧
⟪𝟙 (Iface.ofWidth 1) ⋅ agent .x⟫ = ⟪agent .x⟫ ∧ ⟪room ⋅ 𝟙 (Iface.ofWidth 1)⟫ = ⟪room⟫ ∧
⟪(building ⋅ room) ⋅ agent .x⟫ = ⟪building ⋅ (room ⋅ agent .x)⟫ :=
⟨ex_C2, ex_C3_left, ex_C3_right, ex_M1, ex_M2_left, ex_M2_right, ex_M3,
ex_S1, ex_S2, ex_S3, ex_S4,
ex_par_tensor, ex_par_unit_left, ex_par_unit_right, ex_par_assoc,
ex_merge_unit_left, ex_merge_unit_right, ex_merge_assoc,
ex_nest_unit_left, ex_nest_unit_right, ex_nest_assoc⟩
office. Choose a
law: the nodes its instance is about light up.None of the laws mentions a disjointness proof. BiCoq [MAP+25, §5.1]: “All these requirements
are encased in classes so they are discharged by Coq's automated class instance search without
the need to provide explicit proofs.” Locus does the same. The two classes
Apart (Definition 8) and IToO (Definition 11) carry the side
conditions, and instances derive the compound ones:
instance tensor_left {I J K : Iface Name} {h : Disjoint I.names J.names}
[Apart I K] [Apart J K] : Apart (tensor I J h) K :=
⟨fun a ha hk => (mem_append.mp ha).elim (out a · hk) (out a · hk)⟩
instance of_apart [Apart I₁ I₂] : IToO G₁ G₂ := ⟨ITO_of_disjoint Apart.out⟩
instance par_left [IToO G₁ G₂] [IToO G₂ G₃] [IToO G₁ G₃] : IToO (par' G₁ G₂) G₃ :=
⟨ITO_par_left out out out⟩
So agent .x ∥ agent .x is accepted: the two share an outer name, which
∥ allows. But agent .x ⊗ agent .x is refused, and Lean says why. The
message is pinned in LocusGate/Bigraph.lean:
/-- error: failed to synthesize instance of type class
Apart { width := 1, names := NameSet.singleton Nm.x } { width := 1, names := NameSet.singleton Nm.x }
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. -/
#guard_msgs (whitespace := lax) in
#check agent .x ⊗ agent .x
That is the whole message: the missing instance, and nothing else. It is this clean because
⊗ means only the tensor of bigraphs. While ⊗ also named the tensor of
interfaces, Lean reported a failure of that reading first, and the reason came second.
PROVED here means sorry-free in Lean, with the axioms checked.
| What | Where | Status |
|---|---|---|
| Bigraphs, composition and tensor; support equivalence ≏, and lean-support equivalence ≎ stated directly | Basic, Compose, Tensor, Spm | PROVED |
| The spm axioms, Laws 1–9, on concrete bigraphs; Law 5 for both place and link | Spm | PROVED |
| The elementary bigraphs merge, y/X and /x; the derived ∥, ∣ and ⋅, and Laws 10–16 | Derived | PROVED |
Leaning (lean G); ≎ is ≏ after leaning, agrees with the direct definition, and is a congruence for ◦ and ⊗ | Idle, Abstract | PROVED |
Abstract bigraphs ⟪G⟫ [JM04, Def 9.12]: classes under ≎ across set-equal faces; ◦ and ⊗ lifted to them; every law as an equation | Abstract, Laws | PROVED |
| Abstract bigraphs keep their names; name order is an artefact of the encoding, removed by the quotient (Theorems 1, 2) | Abstract, Tutorial | PROVED |
The link axiom /y ◦ y = id_ϵ in Milner's quotient, refuted under BiCoq's ≏ (Theorem 3) | Abstract, Laws | PROVED |
| The instances in this chapter, Theorems 1–6 | Tutorial | PROVED |
| Dynamics, first step: activity [JM04, Def 7.3]; reaction on abstract bigraphs [JM04, Def 12.1], closed under active contexts; parametric rules, with instantiation functorial | React | PROVED |
| The check against finite CCS: structurally congruent processes are one agent; an encoded process reacts exactly as it reduces (sound and complete); CCS's non-confluence reproduced on the two-futures agent | CCS, CCSComplete | PROVED |
The check widened: choice, restriction (as closure, Milner's encoding [Mil05, §11]) and replicated prefixes !α.P (two rules of ours, which copy the replicated body). Structurally congruent processes are one agent; on closed processes with no restriction inside a replicated body, the reactions of an encoded process are exactly the encodings of its reducts (sound and complete) | CCSFull, CCSFullSound, CCSFullComplete, CCSFullCanon, CCSFullIff | PROVED |
The boundary of that fragment: ν !α.P and !α.νP are one agent and are not structurally congruent, the pair behind Milner's remark that closure cannot give each copy of a replicated process its own private name [Mil05, p. 51] | CCSFullIff, LocusGate/Restriction | PROVED |
| The rest of the dynamics: restriction inside replicated bodies (binding bigraphs), data, RPOs, labelled transitions and bisimulation | outside BiCoq's scope too | OPEN |
The ⟪G⟫ of this chapter is Milner's: classes under ≎, which forgets the identity
of nodes and edges and also forgets idle edges. BiCoq's quotient, by ≏ across set-equal faces, is
strictly finer: every class of BiCoq's lies inside one of Milner's (SetEquiv.toLean),
and Theorem 3 is a pair that Milner's identifies and BiCoq's does not.
The check against CCS supplies a proof the literature does not give. For his encoding of
finite CCS, Milner states that CCS reduction and bigraph reaction match exactly, with only the
remark “It is easy to demonstrate”
[Mil05, Prop 11.5]. Jensen proves the corresponding
theorem for a finite π-calculus from a characterisation of reaction that is itself stated
without proof [Jen06, Lemma 7.6, Theorem 7.7]. Here the
proof is kernel-checked, twice: for a fragment with neither sum nor restriction
(react_iff in Bigraph/CCSComplete.lean), and for one with both and with
replicated prefixes, on closed processes (every free channel a name, as in Milner's) with no
restriction inside a replicated body (react_iff in
Bigraph/CCSFullIff.lean). What is proved is that the reactions of the agent of
p are exactly the agents of the reducts of p. Milner's form,
P → P′ iff P_X(P) ▷ P_X(P′), needs in addition that equal agents come
from congruent processes [Mil05, Theorem 11.4(2)], which is
OPEN here. The rules for replication are not Milner's: his encoding is of finite CCS
[Mil05, §11], and he notes that closure cannot encode a
restriction inside a replicated process [Mil05, p. 51]. stage1_boundary in
LocusGate/Restriction.lean exhibits the pair: νy.!a.ȳ and
!a.νy.ȳ are one agent and are not structurally congruent.
Acknowledgement. This library ports BiCoq [MAP+25], the Coq
formalisation of Milner's pure bigraphs by Marcon, Allignol, Picard, Archibald, Sevegnani and
Thirioux, to Lean. The scope and the list of obligations are BiCoq's ([MAP+25, §2.3]; the
ledger is docs/bicoq-port.md), and so are these design choices: name sets as
duplicate-free lists [MAP+25, §3.1]; bigraphs compared across interfaces that are the same
as sets [MAP+25, §4]; support equivalence as ten conditions and leaning by filtering the
edges [MAP+25, §4.1, §4.2]; side conditions discharged by class search
[MAP+25, §5.1]; and the three derived operations with their laws [MAP+25, §6]. The
definitions themselves follow Jensen and Milner's report [JM04, §6–§10]. Where this chapter
departs from BiCoq it says so: its abstract bigraphs are the report's coarser classes
(Definition 16, Theorem 3). The port was made from BiCoq's paper; its Coq development is archived
separately [MT24].
The quotations are checked against transcriptions of the two documents in
docs/sources/.