locus · bigraph tutorial · Problems for Chapter I
Solved and supplementary problems on Chapter I, at the level of a graduate
course, with problems in Lean. Every computed answer is a theorem in
Bigraph/Problems/ChI.lean, every figure is drawn from a Lean term, and each solution
says what it argues on paper only.
How to read this page. "Definition I.6" means the sixth definition of Chapter I, and likewise for its theorems, figures and laws. A problem uses only what Chapter I defines or proves, and says so in its last line. Several problems follow exercises of Milner's book, cited from his draft of December 2008 [Mil08]; the problems here are restated for the office of Chapter I, and their solutions are our own.
What is checked. Every computed answer is a Lean theorem, and so is every instance a solution works. A general argument is checked when the library proves its statement; otherwise the solution says what is argued on paper only, in its last line.
This version holds the solved problems, I.1 to I.8; the supplementary problems, I.9 to I.28, with their answers at the end; and the problems in Lean, I.29 to I.36.
Problem I.1 (Decomposing the office). The office of Figure I.11 has
four atomic nodes inside its rooms: two agents on x in the meeting room, the laptop
on y in the study, and an agent on z in the lobby.
D (one whose inner face is ε) holding exactly
those four nodes, each in a region of its own.C with office = C ◦ D, and give the interface the
two share.After [Mil08, Exercise 1.1], where the bigraph is a built environment with three agents in rooms.
Solution.
⊗: the two
agents share the name x, and the tensor refuses shared names (Definition I.8). The
parallel product joins them into one link (Definition I.11):
D = ((agent x ∥ agent x) ∥ laptop y) ∥ agent z : ε → ⟨4, {x, y, z}⟩.C must put sites 0 and 1 together in one room,
site 2 in a second room and site 3 in a third, and the three rooms side by side in the building.
The merge of Definition I.12 puts two sites in one region, and nesting (Definition I.13) puts
that region in a room: room ⋅ merge 2. The merge product makes the three rooms
siblings, and nesting puts them in the building:
building ⋅ (((room ⋅ merge 2) ∣ room) ∣ room) : ⟨4, ∅⟩ → ⟨1, ∅⟩.D has outer
names x, y, z, and composition needs the faces to agree
exactly (Definition I.6). So C carries them through, beside it:
C = (building ⋅ (((room ⋅ merge 2) ∣ room) ∣ room)) ∥ 𝟙 ⟨0, {x, y, z}⟩. The shared
interface is ⟨4, {x, y, z}⟩. In Lean, and in Figure 1, D is
atoms and C is host. By Theorem I.4, C ◦ D
is the nesting (building ⋅ …) ⋅ D, which Lean accepts by unfolding alone.office and C ◦ D are
built in different orders, so their node sets are different types: the agent in the lobby is a
different element of a different sum. They are equal as abstract bigraphs (Definition I.16):
there is a bijection of nodes, and one of edges (there are none), preserving controls, parents
and links. Figure 1 draws both sides.C (host) above D
(atoms), unplugged, and the office. The shared face is ⟨4, {x, y, z}⟩: regions 0 and 1 of D fill
the meeting room's two sites, region 2 the study's and region 3 the lobby's, and each name passes
up through C.In Lean. The bijection is found by a search and checked by the kernel
(Bigraph/Problems/Check.lean). The search proposes a certificate, a table of
positions in the two node lists. check computes whether the certificate preserves
controls, parents and links, and same_of_check proves that a certificate that
passes gives the abstract equation. Nothing here trusts the search.
abbrev atoms : Bg Office ε ⟨4, atomNames⟩ := ((agent .x ∥ agent .x) ∥ laptop .y) ∥ agent .z
abbrev rooms4 : Bg Office (Iface.ofWidth (Name := Nm) 4) (Iface.ofWidth 1) :=
((room ⋅ merge Office 2) ∣ room) ∣ room
abbrev host : Bg Office ⟨4, atomNames⟩ ⟨1, atomNames⟩ :=
(building ⋅ rooms4 : Bg Office (Iface.ofWidth (Name := Nm) 4) (Iface.ofWidth 1)) ∥ 𝟙 (Iface.ofNames atomNames)
theorem atomNames_list : atomNames.names = [.x, .y, .z] := rfl
theorem host_comp_atoms : host ◦ atoms = (building ⋅ rooms4) ⋅ atoms := rfl
theorem office_decomposed : ⟪office⟫ = ⟪host ◦ atoms⟫ :=
same_of_check _ _ ⟨rfl, fun _ => Iff.rfl⟩ ⟨rfl, fun a => by cases a <;> decide⟩
⟨[0, 1, 4, 2, 5, 3, 6, 7], [0, 1, 3, 5, 2, 4, 6, 7], [], []⟩ (by decide)
theorem same_of_check {I J I' J' : Iface Name} (G : Bg S I J) (H : Bg S I' J')
(hI : SameIface I I') (hJ : SameIface J J') (c : Cert)
(h : check (IfaceIso.ofMem hI.1 hI.2) (IfaceIso.ofMem hJ.1 hJ.2) G H c = true) :
(⟪G⟫ : Abstract S Name) = ⟪H⟫
Remark. The decomposition is not unique. Putting the two agents in one
region, agent x ∣ agent x, gives a D with three regions and a host
without the merge. In Milner's version the three agents are in three rooms, one to a region, and
his D has the interface ⟨3, {w, x, y, z}⟩
[Mil08, Solution 1.1].
theorem office_decomposed₃ : ⟪office⟫ = ⟪(building ⋅ rooms₃) ⋅ atoms₃⟫ :=
same_of_check _ _ ⟨rfl, fun _ => Iff.rfl⟩ ⟨rfl, fun a => by cases a <;> decide⟩
⟨[0, 1, 4, 2, 5, 3, 6, 7], [0, 1, 3, 5, 2, 4, 6, 7], [], []⟩ (by decide)
Uses Definitions I.5, I.6, I.8, I.11, I.12, I.13 and I.16, Theorem I.4 and Figure I.11.
Problem I.2 (Composition is associative). For
A : I → J, B : J → K and C : K → L, prove that
C ◦ (B ◦ A) and (C ◦ B) ◦ A have the same place graph and the same link
graph, once their node sets and edge sets are identified. Work out the link graphs point by point;
the place graphs go the same way.
After [Mil08, Exercise 2.1].
Solution. Both composites have the nodes of A,
B and C and the edges of all three, bracketed differently. Identify
them in the evident way; what remains is to compare links and parents.
Recall how a composite links a point (Definition I.6, and §5 of
Chapter I). In H ◦ G a point of G keeps G's link if that is
an edge. If G links it to an outer name y, it takes H's link
of the inner name y. A point of H keeps H's link. There are
three kinds of point.
C. On both sides it is a point of the outermost
factor, and its link is C's.B. If B links it to an edge, both sides
keep that edge. If B links it to a name z of K, both sides
give C's link of z: on the left because C is composed onto
B ◦ A, on the right because C ◦ B already sends z there.A, or a port of A. If
A links it to an edge, both sides keep it. If A links it to a name
y of J, both sides give B's link of y when that
is an edge, and otherwise, when B sends y to a name z of
K, C's link of z.Places go the same way. A site or node of A whose parent is a root
j of A takes the parent of site j of B, and if
that is a root k of B, the parent of site k of
C. The chain is the same on both sides. So the two composites differ only in how
their node and edge sets are bracketed, and they are support equivalent (Definition I.14). This
is Law I.1.
theorem C2 : ⟪h ◦ (g ◦ f)⟫ = ⟪(h ◦ g) ◦ f⟫ := comp_assoc h g f theorem C3_left : ⟪𝟙 J ◦ f⟫ = ⟪f⟫ := id_comp f theorem C3_right : ⟪f ◦ 𝟙 I⟫ = ⟪f⟫ := comp_id f
Uses Definitions I.6 and I.14, and Law I.1. In Lean: Law I.1
(Laws.C2), which the library proves from a support equivalence between the two
composites (Bg.assoc). On paper: the case
analysis above.
Problem I.3 (Linkings). A linking is a bigraph
⟨0, X⟩ → ⟨0, Y⟩ with no nodes: it has no places, only links from its inner names to
its outer names and its edges. The substitutions y/X and the closures
/x of Definition I.9 are the elementary linkings.
λ can be written (𝟙 ⟨0, Y⟩ ⊗ /W) ◦ σ,
where σ is a tensor product of substitutions and /W a tensor product
of closures.x and y into one edge
and passes z through.After [Mil08, Exercise 3.1].
Solution.
λ by where they are linked. For each outer name
y let Xy be the inner names linked to y, and
for each edge e let Xe be those linked to e.
These sets partition X; some may be empty. Choose a fresh name
we for each edge, and let W be the set of them. Then
σ = ⊗y y/Xy ⊗ ⊗e we/Xe is
defined, because the X's are disjoint and the y's and
w's are distinct. It sends every inner name to the right outer name or to the
right we. Composing 𝟙 ⟨0, Y⟩ ⊗ /W passes each
y through and closes each we into an edge of its own. The
result links exactly as λ does, up to the bijection that sends e to
the edge of /we. An idle edge of λ comes out too: its
Xe is empty, and we/∅ closed is
Theorem I.3's idle edge./x stands, and
that edge holds one point, x. So a closed link holding two points needs a
composition. In Milner's words, "this use of composition is the only way to close a
substitution" [Mil08, Solution 3.1].λ = (/y ⊗ 𝟙 ⟨0, {z}⟩) ◦ (y/{x, y} ⊗ z/{z}): the substitution sends
x and y to y and z to itself, and the
closure turns y into an edge (Figure 2).y of the substitution. Both x and
y were sent to y, so both end on that edge. z passes
straight through.abbrev sigma3 := subst Office Nm.y xy ⊗ subst Office Nm.z (NameSet.singleton Nm.z)
abbrev link3 := (closure Office Nm.y ⊗ 𝟙 (nm .z)) ◦ sigma3
theorem link3_shape : link3.finV.elems.length = 0 ∧ link3.finE.elems.length = 1 := by decide
theorem link3_links :
link3.link (.inl ⟨.x, by decide⟩) = link3.link (.inl ⟨.y, by decide⟩) ∧
(link3.link (.inl ⟨.x, by decide⟩)).isLeft = true ∧
(link3.link (.inl ⟨.z, by decide⟩)).isRight = true := ⟨rfl, rfl, rfl⟩
Uses Definitions I.6, I.8, I.9 and I.15, and Theorem I.3. In Lean: part (c)
(link3_shape, link3_links). On paper: parts (a) and (b).
Problem I.4 (Nesting is associative). For
F : I → ⟨k, X⟩, G : ⟨k, ∅⟩ → ⟨m, Y⟩ and
H : ⟨m, ∅⟩ → ⟨n, Z⟩, prove that H ⋅ (G ⋅ F) and
(H ⋅ G) ⋅ F are the same abstract bigraph. Use Theorem I.4, and follow places and
links.
After [Mil08, Exercise 3.3]. Milner's solution expands the nestings and uses a bifunctorial property of the parallel product. Chapter I does not state that property, and Jensen and Milner remark that the parallel product "has fewer algebraic properties than the tensor (categorically, it is not a bifunctor)" [JM04, p. 49]. So the proof here goes through places and links instead.
Solution. By Theorem I.4, G ⋅ F = (G ∥ 𝟙 ⟨0, X⟩) ◦ F: the
identity beside G carries F's names up. The identities have no nodes
and no edges, so both sides have the nodes and edges of F, G and
H, bracketed differently. Identify them, and compare.
F whose parent is a root i of
F takes the parent of site i of G. If that is a root
j of G, it takes the parent of site j of H.
This is so on both sides: on the left G ⋅ F is nested in H, and on the
right F is nested in H ⋅ G, whose sites are G's. Places
of G and of H behave the same way.F linked to x in
X passes up through every identity and ends on x on both sides. A
point of G linked to y in Y likewise ends on
y, and a point of H keeps H's link. Edges are kept.⟨n, Z ∪ (Y ∪ X)⟩ and
⟨n, (Z ∪ Y) ∪ X⟩: the same set of names, which is all an abstract bigraph asks of
its faces (Definition I.16).So the two are support equivalent across faces that are the same as sets, and they are one abstract bigraph. This is Law I.16.
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₃)⟫ :=
nest_assoc' G₁ G₂ G₃
Uses Definitions I.11, I.13, I.14 and I.16, Theorem I.4 and Law I.16. In Lean: Law
I.16 (Laws.nest_assoc). On paper: the argument above.
Problem I.5 (Nesting never hides a name).
G₂ is an outer name of
G₁ ⋅ G₂.y is an outer name of G₂ but not of H,
then G₁ ⋅ G₂ and H are different abstract bigraphs.agent x is
hidden.Solution.
G₁ ⋅ G₂ is ⟨n, K ∪ Y⟩, where Y is
the outer names of G₂ (Definition I.13). A union keeps both its parts.LeanSetEquiv.outer. So
y would be an outer name of H.x is an outer name of agent x, and hidden has no
outer names. Apply (b) with any container G₁.theorem nest_ne_of_name {Ctrl Name : Type} [DecidableEq Name] {S : Sig Ctrl}
{I J K I' L : Iface Name} (G₁ : Bg S ⟨J.width, ∅⟩ K) (G₂ : Bg S I J) (H : Bg S I' L)
(y : Name) (hy : y ∈ J.names.names) (hL : y ∉ L.names.names) : ⟪G₁ ⋅ G₂⟫ ≠ ⟪H⟫ := by
intro h
exact hL (((LeanSetEquiv.outer (Quotient.exact h)).2 y).mp (NameSet.mem_union_right hy))
theorem no_nesting_hides {K : Iface Nm} (G₁ : Bg Office ⟨1, ∅⟩ K) : ⟪G₁ ⋅ agent .x⟫ ≠ ⟪hidden⟫ :=
nest_ne_of_name G₁ (agent .x) hidden .x (by decide) (by decide)
Uses Definitions I.13 and I.16, and Theorem I.5. In Lean: all three parts
(nest_ne_of_name, no_nesting_hides).
Problem I.6 (One agent, one name). How many abstract bigraphs
ε → ⟨1, {x}⟩ have exactly one node, and that node an agent? Write each as a term
built from the cast of Chapter I and the elementary bigraphs.
Solution. Two.
x or to an edge. Any other edge has no point
on it, since the inner face ε has no names. So it is idle, and abstract bigraphs
forget it (Definition I.15).x, the bigraph is agent x. Linked to an edge, the name
x has no point: it is an idle name. Abstract bigraphs keep idle names,
because they keep the faces. Built from the cast, this one is
hidden ⊗ x, where x : ε → ⟨0, {x}⟩ is the empty substitution of
Theorem I.3. A support equivalence is a bijection of edges, and after the idle edges are
discarded, agent x has no edge while the other has one, used by the agent's port.
So they differ.The contrast is the point of the problem. An idle edge reaches nothing outside and
is forgotten. An idle name is part of the interface and is kept: the second answer still
has the outer name x, though nothing is linked to it. That is why it is a bigraph
ε → ⟨1, {x}⟩ at all, and why it is not hidden, which is
ε → ⟨1, ∅⟩.
x. On the right it ends on an edge (the dot), and the name
x is idle.abbrev idleX := hidden ⊗ subst Office Nm.x ∅ theorem agent_ne_idleX : ⟪agent .x⟫ ≠ ⟪idleX⟫ := by intro h obtain ⟨_, _, ⟨e⟩⟩ := Quotient.exact h have hpos : 0 < (Bg.lean idleX).finE.elems.length := by decide obtain ⟨u, -⟩ := List.exists_mem_of_length_pos hpos have hu := (Bg.lean (agent Nm.x)).finE.complete (e.edgeFrom u) have h0 : (Bg.lean (agent Nm.x)).finE.elems.length = 0 := by decide rw [List.length_eq_zero_iff] at h0 rw [h0] at hu exact List.not_mem_nil hu
Uses Definitions I.1, I.4, I.9, I.14, I.15 and I.16, and Theorem I.3. In Lean: the
two answers differ (agent_ne_idleX). On paper: that there are no others (steps 1 and
2).
Problem I.7 (A context is a composition). A bigraph is
ground when its inner face is ε. Context expressions are built by
C ::= [·] | g ⊗ C | C ⊗ g | h ◦ C, with g ground and every operation
defined. C[a] is C with the ground a in the hole. Prove
that for every C there is an f with f ◦ a = C[a] for every
such a, as abstract bigraphs. Which laws does the proof use?
After [Mil08, Exercise 2.2].
Solution. By induction on C.
[·]: take f = 𝟙. Law I.2 gives 𝟙 ◦ a = a.h ◦ C, with f for C: take h ◦ f. Then
(h ◦ f) ◦ a = h ◦ (f ◦ a) = h ◦ C[a] by Law I.1.g ⊗ C: take g ⊗ f. Then
(g ⊗ f) ◦ a = (g ⊗ f) ◦ (𝟙 ε ⊗ a) by Law I.4, which is
(g ◦ 𝟙 ε) ⊗ (f ◦ a) by Law I.5 (interchange). That is g ⊗ C[a] by Law
I.2. The tensors are defined because g ⊗ C[a] is.C ⊗ g: the same, with the other forms of Laws I.4 and I.2.The laws used are I.1, I.2, I.4 and I.5: associativity and identity for composition, the unit of the tensor and the interchange law. Milner's answer names the same four [Mil08, Solution 2.2].
theorem context_is_comp :
⟪laptop .y ⊗ (roomOn .x ◦ agent .x)⟫ = ⟪(laptop .y ⊗ roomOn .x) ◦ agent .x⟫ :=
same_of_search _ _ (by decide) (by decide) (by decide)
Uses Laws I.1, I.2, I.4 and I.5. In Lean: an instance
(context_is_comp), for C = laptop y ⊗ (roomOn x ◦ [·]) and
f = laptop y ⊗ roomOn x, by search and check. On paper: the induction.
Problem I.8 (Occurrence). Say that F occurs in
G when G = C₁ ◦ (F ⊗ 𝟙 I) ◦ C₀ for some interface I and
bigraphs C₀, C₁, as abstract bigraphs.
F occurs in F ◦ C, C ◦ F,
F ⊗ C and C ⊗ F.a occurs in a ground g exactly when
g = D ◦ a for some D.D with office = D ◦ agent z; give D.I = ⟨0, {x}⟩, but not with
I = ε. So the identity is needed when F is not ground.After [Mil08, Exercise 3.2]. The identity
beside F lets the nodes of C₁ have children in C₀ as well
as in F, and lets C₁ and C₀ share links that do not
involve F.
Solution. Let F : J → K.
F ◦ C: take I = ε, C₀ = C, C₁ = 𝟙, using
Law I.4 and Law I.2. C ◦ F: take I = ε, C₀ = 𝟙,
C₁ = C. F ⊗ C, with C : J′ → I: take
C₁ = 𝟙 and C₀ = 𝟙 J ⊗ C, since
(F ⊗ 𝟙 I) ◦ (𝟙 J ⊗ C) = (F ◦ 𝟙 J) ⊗ (𝟙 I ◦ C) = F ⊗ C by Laws I.5 and I.2.
C ⊗ F: swap, then use the last case. Naturality (Law I.8) and Law I.7 give
C ⊗ F = γ K I ◦ (F ⊗ C) ◦ γ J′ J, so take C₁ = γ K I and
C₀ = (𝟙 J ⊗ C) ◦ γ J′ J.g = D ◦ a, take I = ε, C₀ = 𝟙 ε and
C₁ = D. Conversely, let g = C₁ ◦ (a ⊗ 𝟙 I) ◦ C₀. C₀ is
ground, since g is; call it b. Interchange gives
(a ⊗ 𝟙 I) ◦ b = a ⊗ b = (𝟙 ⊗ b) ◦ a, both because a and
b are ground. So g = D ◦ a with
D = C₁ ◦ (𝟙 ⊗ b).F = C₁ ◦ (E ⊗ 𝟙 I) ◦ C₀ and G = D₁ ◦ (F ⊗ 𝟙 I′) ◦ D₀.
Tensoring the first equation with 𝟙 I′ = 𝟙 ◦ 𝟙 ◦ 𝟙 and using interchange twice,
then associativity of ⊗ (Law I.3), gives
G = B₁ ◦ (E ⊗ (𝟙 I ⊗ 𝟙 I′)) ◦ B₀, with B₁ = D₁ ◦ (C₁ ⊗ 𝟙 I′) and
B₀ = (C₀ ⊗ 𝟙 I′) ◦ D₀. Finally 𝟙 I ⊗ 𝟙 I′ = 𝟙 (I ⊗ᵢ I′). This is
not one of the sixteen laws, but both sides have no nodes and no edges, put each site in the
root of the same number and pass each name through.C₀ = (agent x ∥ agent x) ∥ laptop y be the other three. Let
C₁ be the building around three rooms with holes: the lobby first, holding site 0,
then the meeting room, merging sites 1 and 2, then the study, holding site 3, all beside the
names. Then, as in (b), D = C₁ ◦ (𝟙 ⟨1, {z}⟩ ⊗ C₀), the office with a hole in
the lobby (Figure 4). The general form holds too, with I = ⟨3, {x, y}⟩:
office = C₁ ◦ (agent z ⊗ 𝟙 I) ◦ C₀. By (b), the identity is not needed
here.(room ⊗ 𝟙 ⟨0, {x}⟩) ◦ (agent x ∣ agent x). So take
I = ⟨0, {x}⟩, C₀ = agent x ∣ agent x and C₁ = 𝟙. With
I = ε there are no such C₀ and C₁; by Law I.4 the
equation would be meeting = C₁ ◦ room ◦ C₀. The meeting room has one room, so it
is the room of F. The two agents are its children, so they come from
C₀, through the room's site, since no node of C₁ is inside
F. C₀'s outer face is the room's inner face ⟨1, ∅⟩,
which has no names, so the agents' ports end on edges of C₀. In the meeting room
they reach the outer name x. The identity is what carries x past
the room: a link that C₀ and C₁ share without involving
F.D above
agent z, unplugged, and the office. D is the office with a hole in
the lobby, and the agent's region fills it.abbrev occC0 : Bg Office ε ⟨3, xxy⟩ := (agent .x ∥ agent .x) ∥ laptop .y
abbrev rooms4' : Bg Office (Iface.ofWidth (Name := Nm) 4) (Iface.ofWidth 1) :=
(room ∣ (room ⋅ merge Office 2)) ∣ room
abbrev occC1 : Bg Office ((⟨1, NameSet.singleton Nm.z⟩ : Iface Nm) ⊗ᵢ ⟨3, xxy⟩) ⟨1, occN⟩ :=
(building ⋅ rooms4' : Bg Office (Iface.ofWidth (Name := Nm) 4) (Iface.ofWidth 1)) ∥
𝟙 (Iface.ofNames occN)
abbrev occD := occC1 ◦ (𝟙 (reg .z) ⊗ occC0)
theorem office_ground : ⟪office⟫ = ⟪occD ◦ agent .z⟫ :=
same_of_search _ _ (by decide) (by decide) (by decide)
theorem agent_z_occurs :
⟪office⟫ = ⟪occC1 ◦ (agent .z ⊗ 𝟙 (⟨3, xxy⟩ : Iface Nm)) ◦ occC0⟫ :=
same_of_search _ _ (by decide) (by decide) (by decide)
theorem room_in_meeting :
⟪meeting⟫ = ⟪𝟙 (Iface.ofWidth 1 ⊗ᵢ nm .x) ◦ (room ⊗ 𝟙 (nm .x)) ◦ (agent .x ∣ agent .x)⟫ :=
same_of_search _ _ (by decide) (by decide) (by decide)
Uses Definitions I.6, I.7, I.8, I.10–I.13 and I.16, Laws I.1–I.5, I.7, I.8 and
I.10, Theorem I.4, and Problem I.1. In Lean, by search and check: part (d) and its general form
(office_ground, agent_z_occurs), and the decomposition in (e)
(room_in_meeting). On paper: parts (a)–(c), including the step
𝟙 I ⊗ 𝟙 I′ = 𝟙 (I ⊗ᵢ I′), and that (e) fails with I = ε.
Answers are at the end of the page. A problem marked ⋆ asks for a proof, and its
answer gives the outline. As in Problem I.6, x : ε → ⟨0, {x}⟩ is the empty
substitution of Theorem I.3, the name x linked to nothing.
Problem I.9 (Defined or not). For each expression, say whether it is defined. If it is, give its interfaces; if not, say which condition fails.
agent x ⊗ laptop yagent x ⊗ laptop xroom ◦ agent xroomOn x ◦ agent xagent x ∥ laptop xProblem I.10 (Into the origin). Let G : I → ε.
G has no nodes, and that I has width 0.G is an edge.G have no nodes and no edges?After [Mil08, Exercise 2.3].
Problem I.11 (The bijection behind a law). The composite
𝟙 (reg x) ◦ agent x has node set Unit ⊕ Empty, and its one node is
.inl (). Write down the two bijections of Definition I.14 between it and
agent x, and check that they preserve controls, parents and links.
Problem I.12 (Edges, used and idle). For each of joined,
hidden, /x and /x ◦ x, list the edges, and the points
linked to each. Which edges are idle?
Problem I.13 (A symmetry on three places).
γ ⟨2, ∅⟩ ⟨1, ∅⟩ put each of its three sites?γ ⟨1, ∅⟩ ⟨2, ∅⟩ ◦ γ ⟨2, ∅⟩ ⟨1, ∅⟩ site by site, and compare
the result with Law I.7.Problem I.14 (What a closed link forgets).
hidden and (𝟙 ⟨1, ∅⟩ ⊗ /y) ◦ agent y are the same
abstract bigraph.hidden ⊗ (/x ◦ x) and hidden are the same abstract
bigraph.Problem I.15 (Linkings on two names). Linkings are as in Problem I.3.
⟨0, {x, y}⟩ → ⟨0, {x, y}⟩ have no edges? Write each as a
term built from substitutions and identities with ⊗.x and y the symmetry
γ (nm x) (nm y)?⟨0, {x, y}⟩ → ⟨0, {x, y}⟩ are there, edges
allowed?Problem I.16 (Placings on two places). A placing is a bigraph with no nodes whose faces have no names.
⟨2, ∅⟩ → ⟨2, ∅⟩ are there? Write each as a term
built from merges, 𝟏 = merge 0, symmetries and identities with
⊗.⟨m, ∅⟩ → ⟨n, ∅⟩ are there?Problem I.17 (Tensor and parallel product).
agent x ∥ agent x is defined and agent x ⊗ agent x
is not. What are the interfaces of the first?y/{x} ∥ z/{x} is not defined.G₁ ∣ G₂ is defined exactly when G₁ ∥ G₂ is.Problem I.18 (Interchange, read from left to right).
(room ⊗ roomOn x) ◦ (agent x ⊗ hidden) is defined, but that
(room ◦ agent x) ⊗ (roomOn x ◦ hidden) is not.∥, with
(roomOn x ∥ room) ◦ (agent x ∥ laptop x).Problem I.19 (The study and the lobby without nesting).
study = room ⋅ laptop y and lobby = room ⋅ agent z as
compositions, without ⋅.study is also roomOn y ◦ laptop y.Problem I.20 ⋆ (Where edges come from).
◦, ⊗, ∥, ∣ and
⋅ has no edges.Problem I.21 ⋆ (≏ and ≎ are preserved by composition). Suppose
G ≏ G′ and H ≏ H′, and H ◦ G is defined.
H ◦ G ≏ H′ ◦ G′.≎. Hint: Chapter I's leanComp says
lean (H ◦ G) ≏ lean (lean H ◦ lean G).After [Mil08, Exercise 7.2].
Problem I.22 (More bigraphs with one agent). As in Problem I.6, how
many abstract bigraphs (a) ε → ⟨1, ∅⟩ and (b) ε → ⟨1, {x, y}⟩ have
exactly one node, and that node an agent? Write each as a term.
Problem I.23 (Which abstract composites are defined). Which of
⟪room⟫ ⊚ ⟪laptop y⟫, ⟪roomOn x⟫ ⊚ ⟪laptop y⟫ and
⟪roomOn y⟫ ⊚ ⟪laptop y⟫ are defined?
Problem I.24 (A symmetry after a parallel product).
γ (reg x) (reg y) ◦ (agent x ∥ laptop y) = laptop y ∥ agent x.agent x ∥ laptop y and laptop y ∥ agent x the same abstract
bigraph?Problem I.25 (Merging in stages). Show that
merge 2 ◦ (merge 2 ⊗ 𝟙 ⟨1, ∅⟩) and merge 2 ◦ (𝟙 ⟨1, ∅⟩ ⊗ merge 2)
are both merge 3. Which law of Chapter I do these equations come from?
Problem I.26 (Interchange by hand). Chapter I's instance of
Law I.5 is
(roomOn x ◦ agent x) ⊗ (roomOn y ◦ laptop y) = (roomOn x ⊗ roomOn y) ◦ (agent x ⊗ laptop y).
For each node on each side, give its parent and the link of each of its ports. Then give the
bijections of Definition I.14.
Problem I.27 (Nesting needs matching places).
room ⋅ (agent x ∥ laptop x) not defined?Problem I.28 (The meeting room, unfolded). Show that
meeting = roomOn x ◦ (merge 2 ⊗ 𝟙 ⟨0, {x}⟩) ◦ (agent x ∥ agent x), using
Theorem I.4 and Definition I.12.
The problems
below are stated in Lean in the exercise file
ChI.lean, each with sorry for
its proof. The statements are there to read; working them needs the library, which is not public.
The file is cut mechanically from the solutions, so its statements are exactly the ones below,
which are checked. Every solution uses the axioms propext and Quot.sound
at most. A problem marked ⋆ is longer.
Problem I.29 (Controls are kept). Prove that an agent is not a laptop, even on the same name.
theorem agent_ne_laptop : ⟪agent .x⟫ ≠ ⟪laptop .x⟫
Hint: Quotient.exact turns the equation into an equivalence of the
representatives (Definition I.16), and its node bijection preserves controls
(ctrl_eq). The agent's one node is ().
Uses Definitions I.5 and I.14–I.16. Solution: agent_ne_laptop,
8 lines.
Problem I.30 (Idle names are kept). Prove that the second answer to
Problem I.6 is not hidden.
theorem idleX_ne_hidden : ⟪idleX⟫ ≠ ⟪hidden⟫
Hint: equivalent representatives have faces that are the same as sets
(LeanSetEquiv.outer), and decide settles whether a name lies in a
concrete name set.
Uses Definitions I.9 and I.16, and Theorem I.1. Solution:
idleX_ne_hidden, 3 lines.
Problem I.31 (Which rooms take which laptops). Prove that the room
carrying a takes the laptop on b exactly when a = b.
theorem roomOn_takes_laptop (a b : Nm) : (⟪roomOn a⟫ ⊚ ⟪laptop b⟫).isSome ↔ a = b
Hint: split both names into cases. Each case is then a computation, as in Problem I.23.
Uses Definition I.16 and Theorem I.1. Solution:
roomOn_takes_laptop, 1 line.
Problem I.32 (Certificates by hand). Prove both equations with
same_of_check, writing the certificate yourself rather than calling the search
same_of_search. A certificate lists, for each node of the left side in the order
of its Finite.elems, the position of its image on the right; then the inverse; then
the same two lists for edges. (a) is Problem I.11's equation, (b) Problem I.24(a)'s.
theorem cert_id_agent : ⟪𝟙 (reg .x) ◦ agent .x⟫ = ⟪agent .x⟫ theorem cert_gamma_par : ⟪γ (reg .x) (reg .y) ◦ (agent .x ∥ laptop .y)⟫ = ⟪laptop .y ∥ agent .x⟫
Hint: the nodes of a composite list those of the inner factor first, and the nodes of a parallel product those of its left factor first.
Uses Definitions I.6, I.11 and I.14, and Problems I.11 and I.24. Solution:
cert_id_agent, cert_gamma_par, 1 line each.
Problem I.33 (Places are kept). Prove that the symmetry on two regions is not the identity, even as abstract bigraphs.
theorem gamma_ne_id : ⟪γ (reg .x) (reg .y)⟫ ≠ (⟪𝟙 (reg .x ⊗ᵢ reg .y)⟫ : Abstract Office Nm)
Hint: compare the parents of site 0 (prnt_eq). The maps on
places reduce by definition, so change the equation into one between two regions,
and the regions differ.
Uses Definitions I.10, I.14 and I.16, and Problem I.16. Solution:
gamma_ne_id, 5 lines.
Problem I.34 (Idle edges vanish beside anything). Prove that for
every G, G ⊗ (/x ◦ x) is G.
abbrev idleEdge : Bg Office (ε : Iface Nm) ε := closure Office Nm.x ◦ subst Office Nm.x ∅
theorem idle_beside {I J : Iface Nm} (G : Bg Office I J) : ⟪G ⊗ idleEdge⟫ = ⟪G⟫
Hint: Theorem I.3 (close_idle) gives
⟪/x ◦ x⟫ = ⟪𝟙 ε⟫; the equivalence of Definition I.15 is a congruence for
⊗ (leanTensor_congr); and Law I.4 (M2_right) removes
𝟙 ε.
Uses Definitions I.8, I.15 and I.16, Theorem I.3 and Law I.4. Solution:
idle_beside, 3 lines.
Problem I.35 ⋆ (No region, no nodes). Prove that a bigraph whose
outer face has width 0 has no nodes and no sites. This generalises Problem I.10(a), whose
statement into_origin then follows in one line.
theorem no_place {Ctrl Name : Type} {S : Sig Ctrl} {I J : Iface Name} (G : Bg S I J)
(hJ : J.width = 0) : (G.V → False) ∧ I.width = 0
Hint: G.acyclic v is an accessibility proof; induct on it. A region
of a face of width 0 is an element of Fin 0. For the sites, look at the parent of
site 0.
Uses Definitions I.2–I.4 and Problem I.10. Solution: no_place,
15 lines.
Problem I.36 ⋆ (One name, no edges: the identity). Prove that a
linking ⟨0, {x}⟩ → ⟨0, {x}⟩ with no edges is the identity. This is the one-name
case of Problem I.15(a).
theorem edgeless_linking (G : Bg Office (nm .x) (nm .x)) (hE : G.E → False) :
⟪G⟫ = ⟪𝟙 (nm .x)⟫
Hint: Problem I.35 disposes of the nodes. Build the support equivalence of
Definition I.14 field by field: every field about nodes or edges is vacuous, and the link of
the inner name x must be the outer name x, since there are no edges.
Then StrictEquiv.toSetEquiv, SetEquiv.toLean and
Quotient.sound.
Uses Definitions I.7, I.9 and I.14–I.16, and Problems I.15 and I.35. Solution:
edgeless_linking, 27 lines.
Each answer ends, as the solutions do, with what Lean checks and what is argued on paper only.
I.9 (a) ε → ⟨2, {x, y}⟩.
(b) Not defined: the outer names are not disjoint (Definition I.8). (c) Not defined: the room's
inner face ⟨1, ∅⟩ is not the agent's outer face ⟨1, {x}⟩
(Definition I.6). (d) ε → ⟨1, {x}⟩. (e) ε → ⟨2, {x}⟩: the shared
name is one name (Definition I.11).
In Lean: (a), (d) and (e) are stated at these types (ans9a,
ans9d, ans9e), and the failed conditions of (b) and (c) are proved
(ans9b, ans9c).
I.10 (a) A node's parent is a node or a
region, and ε has no regions. So following parents up from a node never stops,
against acyclicity. A site's parent would also be a node or a region, and there are neither.
(b) ε has no outer names. (c) Only those with I = ε: by (b), an
inner name would need an edge. Such a G is 𝟙 ε up to the identities
of its empty node and edge sets. Milner's answer is the same
[Mil08, Solution 2.3].
In Lean: (a) for every signature and every G
(into_origin, the instance at ε of Problem I.35). On paper: (b) and
(c).
I.11 On nodes, .inl () ↦ (). On
edges, the empty map, since both edge sets are empty. Both nodes are agents. In the composite
the agent's parent is region 0 of the identity, which holds the site that the agent's region
filled; in agent x it is region 0. The agent's port goes to x, meets
the identity's inner name x, and goes straight up to x; in
agent x it goes to x.
In Lean: the equation, by search (id_agent). The certificate the
search finds sends node 0 to node 0 and has no edges: it is this bijection.
I.12 joined: no edges; both
ports go to the outer name z. hidden: one edge, from the closure,
with the agent's port on it. /x: one edge, with the inner name x on
it. /x ◦ x: one edge, and nothing on it. The closure's inner name has met the
outer name x of the empty substitution, which has no points, and it is no longer a
point of the composite. Only that last edge is idle.
In Lean: the edge counts, before and after discarding idle edges
(joined_hidden_edges, idle_by_composition).
I.13 (a) Sites 0 and 1, the first block, go
to regions 1 and 2; site 2 goes to region 0. (b) γ ⟨1, ∅⟩ ⟨2, ∅⟩ puts site 0 in
region 2, and sites 1 and 2 in regions 0 and 1. Region r of the lower symmetry
fills site r of the upper, so site 0 goes to 1 and then to 0, site 1 to 2 and
then to 1, and site 2 to 0 and then to 2. Every site ends in the region with its own number:
the composite is 𝟙 ⟨3, ∅⟩, as Law I.7 says.
In Lean: (a) (gamma21); (b) is Law I.7. On paper: the trace in
(b).
I.14 (a) Both have one agent in one region,
with its port on an edge, and neither has a name on either face. The name a link was closed
under is not part of the result, so even BiCoq's equivalence relates the two, without
discarding idle edges. (b) /x ◦ x adds one idle edge (Problem I.12), and abstract
bigraphs forget idle edges (Definition I.15).
In Lean: both, by search (hidden_rename, and
hidden_idle after discarding idle edges).
I.15 (a) Four, one for each map from
{x, y} to {x, y}: 𝟙 ⟨0, {x, y}⟩;
y/{x} ⊗ x/{y}, which exchanges the names; and x/{x, y} ⊗ y and
y/{x, y} ⊗ x, which join both names on one and leave the other idle.
(b) No. γ (nm x) (nm y) sends each name to itself, and is the identity
(Theorem I.2). Exchanging two names takes substitutions. (c) Ten. An abstract linking is
fixed by which inner names share a link, and by where each link goes: to an outer name or to an
edge. If x and y share a link, it goes to x, to
y or to an edge: 3. If not, their two links go to two different places, writing
e and e′ for edges: (x, y), (y, x),
(x, e), (e, x), (y, e), (e, y) and
(e, e′): 7.
On paper: all of it.
I.16 (a) Four, one for each map from the two
sites to the two regions: 𝟙 ⟨2, ∅⟩; γ ⟨1, ∅⟩ ⟨1, ∅⟩, which crosses
them; merge 2 ⊗ 𝟏, both in region 0; and 𝟏 ⊗ merge 2, both in
region 1. They are different abstract bigraphs, because the equivalences carry every site and
region number to itself (Definition I.14). (b) nᵐ: abstractly a placing is just a
map from sites to regions.
In Lean: where the last three put each site (placings). On paper:
that they differ, and the count.
I.17 (a) The tensor needs disjoint outer
names (Definition I.8), and both are {x}. The side condition of ∥ is
about shared inner names, and there are none. agent x ∥ agent x : ε → ⟨2, {x}⟩,
with both ports on x. (b) Both factors have the inner name x, and the
side condition of Definition I.11 asks that they link it to a common outer name. One links it
to y, the other to z. (c) G₁ ∣ G₂ is
G₁ ∥ G₂ followed by a merge (Definition I.12), and there is a merge for every
width.
In Lean: (a) (twoAgents; the tensor fails by ans9b),
(b) (par_refused), and (c) by definition: mergeProd takes the side
condition of par and nothing else.
I.18 (a) ⟨1, {x}⟩ ⊗ᵢ ⟨1, ∅⟩ and
⟨1, ∅⟩ ⊗ᵢ ⟨1, {x}⟩ are the same interface, ⟨2, {x}⟩. So the composite
is defined: the agent goes into the plain room, its x meets the name that
roomOn x carries through, and hidden goes into the other room
(Figure 5). But neither room ◦ agent x nor roomOn x ◦ hidden is
defined (Problem I.9(c)). (b) roomOn x ∥ room has inner face
⟨2, {x}⟩, the outer face of agent x ∥ laptop x; but
room ◦ laptop x is not defined. (c) The face ⟨m + n, X ⊎ Y⟩ does not
record how it was split. The interchange law is required only "when both sides exist"
[JM04, Def 3.2], and Law I.5 is stated for factors whose
faces match one by one.
x is carried up beside the other room.In Lean: (a) and (b) are stated (swapTensor,
swapPar), and the face mismatch of the refused factors is proved
(ans9c). On paper: (c).
I.19 (a) By Theorem I.4,
study = (room ∥ 𝟙 ⟨0, {y}⟩) ◦ laptop y and
lobby = (room ∥ 𝟙 ⟨0, {z}⟩) ◦ agent z. (b) room and
𝟙 ⟨0, {y}⟩ share no name, so their parallel product is their tensor (Law I.10),
which is roomOn y.
In Lean: (a) by unfolding (study_lobby_comp); (b) by search
(study_roomOn).
I.20 (a) By induction on the expression. Of
the elementary bigraphs only the closure has an edge (Definitions I.5, I.7, I.9, I.10 and
I.12). Composition and tensor take the edges of both factors (Definitions I.6 and I.8), and so
does ∥. ∣ and ⋅ compose a parallel product with a merge
or an identity, neither of which has edges (Definition I.12, Theorem I.4). (b) The same
induction counts the closures. The abstract bigraph keeps only the used edges, and there may be
fewer: /x ◦ x has one edge, and its abstract bigraph none (Problem I.12).
In Lean: the instances (joined_hidden_edges,
idle_by_composition). On paper: the induction.
I.21 (a) Put the bijections together. The
nodes of H ◦ G are those of G and of H (Definition I.6),
so the two node bijections together are a bijection onto the nodes of H′ ◦ G′,
and likewise for edges. Controls are preserved at once. For parents and links, take each point
in turn. A link of G to an outer name continues as H links that inner
name, and the bijections carry every name to itself. (b) G ≎ G′ means
lean G ≏ lean G′. By (a), lean H ◦ lean G ≏ lean H′ ◦ lean G′.
Discarding idle edges preserves ≏, since the edge bijection carries used edges to
used edges. Then use the hint on both sides. This is Milner's argument
[Mil08, Solution 7.2].
In Lean: both, for ⊗ too, and across faces that are the same as
sets (leanCompSet_congr, leanTensor_congr, from Chapter I). On paper:
the argument above.
I.22 (a) One, hidden: with no
outer names the port must go to an edge. (b) Three. The port goes to x, to
y or to an edge: agent x ⊗ y, agent y ⊗ x and
hidden ⊗ x ⊗ y. They differ for the reason given in Problem I.6.
On paper: all of it.
I.23 Only the third, which is
⟪roomOn y ◦ laptop y⟫. The first fails because the room's inner face has no names,
the second because it has x where y is needed. By Theorem I.1 the
answer does not depend on the representatives.
In Lean: all three (meets).
I.24 (a) The names are disjoint, so both
parallel products are tensors (Law I.10). Then use naturality (Law I.8), and
γ ε ε = 𝟙 ε (Law I.6). Both sides put the laptop in region 0 and the agent in
region 1. (b) No. Region 0 holds an agent in one and a laptop in the other, and the
equivalences preserve controls and region numbers.
In Lean: (a), by search (gamma_par). On paper: (b).
I.25 Every site ends in the one region on
each side, and there are no nodes or names. The equations come from Law I.14 with
G₁ = G₂ = G₃ = 𝟙 ⟨1, ∅⟩: unfold ∣ (Definition I.12), and use
𝟙 I ⊗ 𝟙 J = 𝟙 (I ⊗ᵢ J) as in Problem I.8.
In Lean: both equations, by search (merge_stages). On paper: the
link to Law I.14.
I.26 On both sides, region 0 holds the room of
roomOn x, which holds the agent, whose port is on x; region 1 holds
the room of roomOn y, which holds the laptop, whose port is on y. Rooms
have no ports. The node bijection sends each node to the node of the same factor, and there are
no edges.
In Lean: the equation is Law I.5 (Chapter I's ex_M3). On paper: the
table of parents and links.
I.27 (a) room has one site and
agent x ∥ laptop x has two regions; Definition I.13 asks for as many sites as
regions. (b) room ⋅ (agent x ∣ laptop x) : ε → ⟨1, {x}⟩. The merge product puts
both in one region.
In Lean: (b) is stated (nestMerged); (a) is a type error.
I.28 By Theorem I.4,
meeting = (room ∥ 𝟙 ⟨0, {x}⟩) ◦ (agent x ∣ agent x). The first factor is
roomOn x (Problem I.19(b)). By Definition I.12 the second is
agent x ∥ agent x followed by merge 2 beside the name
x. Then regroup (Law I.1).
In Lean: the equation, by search (meeting_unfolded). On paper: the
steps.
docs/sources/10a-tr580-rpos.md.docs/sources/11-milner-exercises.md.
The book was published by Cambridge University Press in 2009.