II Problems: Rules, Reactions and CCS

Solution.

1. Follow the parents up from s in G ◦ F (Definition I.6). First come the nodes of F above s, up to region r of F. That region fills site r of G, so next come the nodes of G above site r. These are all the nodes above s, and Definition II.1 asks that every one be active. The region r exists, since every chain of parents ends at a region, by acyclicity.
2. G is not active: its site 1 lies inside B. In G ◦ F, the one site lies inside F's A, in region 0 of F; that region fills site 0 of G, inside G's A. Both are active, so by (a) G ◦ F is active. Site 1 of G is filled by region 1 of F, which is empty, so nothing ends up inside B (Figure 1).

Activity of a composite depends only on the sites of the outer factor that the inner one actually fills with something. A passive node with nothing below it blocks nothing.

abbrev F : Bg Examples.sig (Iface.ofWidth (Name := Nat) 1) (Iface.ofWidth 1 ⊗ᵢ Iface.ofWidth 1) :=
  A ⊗ (merge Examples.sig 0 : Bg Examples.sig (Iface.ofWidth (Name := Nat) 0) (Iface.ofWidth 1))

abbrev G : Bg Examples.sig (Iface.ofWidth (Name := Nat) 1 ⊗ᵢ Iface.ofWidth 1) (Iface.ofWidth 1) :=
  merge Examples.sig 2 ◦ (A ⊗ B)

Uses Definitions I.5, I.6, I.8, I.12 and II.1. In Lean: (b), as Problem II.23 (G_not_active, GF_active), and one half of (a) for all sites at once (Active.comp: if F and G are active, so is G ◦ F). On paper: (a) in full.

Solution.

1. By Definition II.2, a = ⟪D ◦ r⟫ and b = ⟪D ◦ r′⟫ for a rule (r, r′) and an active D. By Law I.1, E ◦ (D ◦ r) = (E ◦ D) ◦ r, and likewise with r′. By Problem II.1(a), E ◦ D is active: each site of D is active in D, and the region it lies in fills a site of E, active in E. So the same rule, in the context E ◦ D, gives E ◦ a ⊿ E ◦ b. When the faces of E and a are the same only as sets, a renaming wiring goes between, and it has no nodes, so it changes no activity.
2. ping ⊿ pong by the ping rule, in the identity context. Put the ping in the hidden panel: the only occurrence of the redex now has the passive hidden above it, so it is no reaction. The chapter's run shows it: the hidden ping waits until a toggle makes its panel active.

Uses Definitions I.6, II.1 and II.2, Law I.1, Theorem II.1 and Problem II.1. In Lean: (a), as the library's React.comp, and as Problem II.24 for contexts that compose on the nose; (b), as the chapter's hidden_waits.

Solution.

1. As abstract bigraphs, a ∣ c is (𝟙 ⟨1, X⟩ ∣ c) ◦ a: the context 𝟙 ⟨1, X⟩ ∣ c holds a site beside c, in one region, and a fills the site (Definitions I.11 and I.12). The context is active: its one site has no node above it. So Theorem II.1 gives (𝟙 ∣ c) ◦ a ⊿ (𝟙 ∣ c) ◦ b.
2. Suppose a set of rules made add v react in an agent a with no cell v. By (a) it would react in a ∣ cell v too, where a cell v is present. A rule applies where its redex occurs and says nothing about what does not occur. The list does not test absence: it tests presence, of the sentinel stop, at the end of a walk along the links. The walk passes every cell of the list, and the rule that moves on exists only for cells w ≠ v, so reaching stop shows that no cell of the list holds v. A cell v beside the list, not linked into it, does not stop the append, and should not: the set is the list.

Uses Definitions I.11, I.12 and II.2, and Theorem II.1. On paper: (a), whose first step is the abstract equation a ∣ c = (𝟙 ∣ c) ◦ a, and (b).

Solution.

1. Region j of ϱ(d) holds a copy of region ϱ j of d (Definition II.4), so ϱ(d) = d₀ ∥ d₀ ∥ d₁. The body d₀ is copied: one copy stays in the server, one runs. The continuation d₁ is kept, and d₂, the other summands, is discarded.
2. Two sums, ϱ = (0, 2): the chosen continuations, regions 0 and 2, are kept once; the other summands, 1 and 3, are discarded. Server and sum, ϱ = (0, 0, 1): as in (a). Two servers, ϱ = (0, 1, 0, 1): both bodies are copied, each server keeping one copy, and nothing is discarded.
3. Region k of ϱ(ϱ′(d)) holds a copy of region ϱ k of ϱ′(d), which holds a copy of region ϱ′ (ϱ k) of d. So the composite instantiation is k ↦ ϱ′ (ϱ k), that is ϱ′ ∘ ϱ. An instantiation maps the sites of the reactum back to the sites of the redex, so maps compose the other way round from the instantiations, as substitutions do.

theorem inst_maps :
    (List.ofFn Bigraph.Shapes.ssInst).map Fin.val = [0, 2] ∧ (List.ofFn rsInst).map Fin.val = [0, 0, 1] ∧
    (List.ofFn rrInst).map Fin.val = [0, 1, 0, 1] := by decide

Uses Definitions II.3–II.5 and II.8, and Theorem II.2. In Lean: the three maps (inst_maps), and (c) in general (the library's inst_comp). On paper: (a) and the reading of (b).

Solution.

1. For each name x, with one site each and ϱ = (0):

   leave_x : room.(agent_x ∣ □₀)  ⟶  agent_x ∣ room.□₀
   enter_x : agent_x ∣ room.□₀  ⟶  room.(agent_x ∣ □₀)

   The site keeps the rest of the room's contents in the room. The rules are families indexed by the name, like the list's families indexed by a value.
2. Among others: the building, the rooms and the laptops are never created, destroyed or moved; there are always three agents; each agent keeps its name, since neither rule touches a link; every agent is in the building, directly or in a room, since the rules move an agent only between a room and its parent, which is the building; and no node is ever inside an agent, since agents are atoms.

3. hangUp_x : room.(agent_x ∣ □₀)  ⟶  /e(agent_e) ∣ room.□₀

   The reactum keeps x as an idle outer name (its outer face is the redex's), and the agent's port goes to a new edge. "Each agent keeps its name" fails. A new invariant holds: an agent on an edge is never again on a name, since no rule links a port to a name. An agent that hangs up never rejoins its call.

Uses Definitions I.5, I.9, I.12 and II.1–II.5. On paper: all of it. The rules are not in Lean.

Solution.

1. In D ◦ r, a point of D is linked as D links it, and the inner names p and q of D go wherever D sends them (Chapter I, how names meet). Reaction replaces r by r′ and keeps D, so the points of D keep their links in D. The reactum can put its own points on p and q, but cannot make p and q one link: they are distinct outer names of r′. So rm v ∣ cell v[p, q] ⟶ 1 would cut the list: the predecessor stays on p's link, the successor on q's.
2. Put the predecessor in the redex, so that the reactum can relink it. For every w:

   rm v ∣ head[p] ∣ cell v[p, q]       ⟶  head[q]
   rm v ∣ cell w[o, p] ∣ cell v[p, q]  ⟶  cell w[o, q]

   In the reactum p is idle, and the edge the context gave it is left with no points, which abstract bigraphs forget.
3. Removing needs a cell v, which is a presence, so a redex can find it directly. Adding needed an absence, which only the walk to stop establishes (Problem II.3). When v is absent, rm v never reacts: the request waits. To make it disappear instead, it would need the scan of add after all.

Uses Definitions I.6, I.9, I.15 and II.2, and Problem II.3. On paper: all of it. The rules are not in Lean.

Solution. The two-sums rule on a, the first sum sending:

R  = alt.(snd_a.□₀ ∣ □₁) ∣ alt.(rcv_a.□₂ ∣ □₃) : ⟨4, ∅⟩ → ⟨1, {a}⟩
R′ = a ∣ □₀ ∣ □₁                                : ⟨2, ∅⟩ → ⟨1, {a}⟩,   ϱ = (0, 2)

Here a in R′ is the empty substitution of Theorem I.3: the reactum keeps a as an idle outer name (Definition II.2). The parameter d = d₀ ∥ d₁ ∥ d₂ ∥ d₃ : ε → ⟨4, {b, c}⟩ has: d₀ empty, the continuation of ā; d₁ the other summand, a rcv node on b; d₂ the continuation c̄.0, an alt node holding a snd node on c; and d₃ empty, since the second sum has no other summand. Then, by Definition II.5,

r  = (R ∥ 𝟙 ⟨0, {b, c}⟩) ◦ d             : ε → ⟨1, {a, b, c}⟩
r′ = (R′ ∥ 𝟙 ⟨0, {b, c}⟩) ◦ (d₀ ∥ d₂)     : ε → ⟨1, {a, b, c}⟩

The whole process is the redex, so the context is the identity on ⟨1, {a, b, c}⟩. The parameter uses no edge, as Definition II.5 asks.

theorem rule_faces :
    (ssRule true 0).m = 4 ∧ (ssRule true 0).m' = 2 ∧ (ssRule true 0).J.width = 1 ∧
      (ssRule true 0).J.names.names = [0] ∧ (rsRule true 0).m = 3 ∧ (rsRule true 0).m' = 3 ∧
      (rrRule true 0).m = 2 ∧ (rrRule true 0).m' = 4 := by decide

Uses Definitions II.2–II.5, II.7 and II.8, and Theorem II.7. In Lean: the faces of the rule (rule_faces, with a the channel 0), and the reaction itself (the chapter's react_choice, by Theorem II.7). On paper: the parameter.