II Rules, Reactions and CCS

§0 · Overview

This chapter has three threads: a CCS with private names and replication, two different kinds of variable on the bigraph side, and the theorems that tie them together. This section gives each in brief, with the sections that develop it.

The calculus

CCS has restriction: Milner's encoding of CCS in bigraphs includes it, written ν [Mil05, §11]. It also has recursion, and Milner speaks of “CCS with recursion (or replication)” [Mil05, p. 51]. What CCS lacks is name passing, which is the π-calculus. Here recursion takes the form of replicated prefixes !α.P: servers that start a fresh copy of P for each partner.

P ::= 0  |  P | Q  |  νP  |  Σ_i α_i.P_i  |  !α.P    α ::= c  |  c̄    c ::= free n  |  bound i

inductive Chan where
  | free (n : Nat)
  | bound (i : Nat)
deriving DecidableEq, Repr

mutual
inductive Proc where
  | nil : Proc
  | par : Proc → Proc → Proc
  | res : Proc → Proc
  | sum : Sum → Proc
  | rep : Act → Proc → Proc
inductive Sum where
  | pre : Act → Proc → Sum
  | plus : Sum → Sum → Sum
end

A channel bound i names the i-th enclosing ν, so ν is the only binder: a prefix binds nothing, since pure CCS passes no values. There are three communication axioms, closed under |, ν and structural congruence (§7):

(… + a.P + …) | (… + ā.Q + …)  →  P | Q
!a.P | (… + ā.Q + …)  →  !a.P | P | Q
!a.P | !ā.Q  →  !a.P | !ā.Q | P | Q

Pattern variables: the sites of a rule

A parametric rule (R, R′, ϱ) has sites, and its ground instances fill them (§3). For every parameter d = d0 ∥ … ∥ dm−1:

(R ⊗ id_X) ∘ d  ⟶  (R′ ⊗ id_X) ∘ ϱ(d),    ϱ(d) = d_ϱ(0) ∥ … ∥ d_ϱ(m′−1)

The sites are the pattern variables of the rule, as in term rewriting. An index that ϱ hits twice is copied, and one it misses is discarded. The server rule of Figure 9, in the receiving polarity, is

rrcv_a[0] | alt(snd_a[1] | [2])  ⟶  rrcv_a[0] | [1] | [2],    ϱ = (0, 0, 1)

def rsInst : Fin 3 → Fin 3 := fun s => match s.val with
  | 0 => 0
  | 1 => 0
  | _ => 1

The body d0 fills sites 0 and 1: the server keeps it and a copy runs. The continuation d1 fills site 2, and the other summands, d2, are discarded. So the rules are where copying happens, and that is where name binding comes to matter; but the rules bind no names.

Name binding: declared in the signature

Pure bigraphs have no binders: a link is an outer name or an edge. The first encoding makes νy.P a closure, ⟦νy.P⟧ = /y ∘ ⟦P⟧, the name y closed into an edge (§8):

theorem res_mk (X : NameSet Nat) (ρ : Nat → Nat) (s : Shape S) (y : Nat) (hy : y ∉ X.names)
    (h : s.res.Names X ρ) (h' : s.Names (NameSet.union X (NameSet.singleton y)) (consEnv y ρ)) :
    Abstract.mk (s.res.bg X ρ h) =
      Abstract.mk (comp (closeCtx (S := S) ⟨1, NameSet.union X (NameSet.singleton y)⟩ X)
        (s.bg (NameSet.union X (NameSet.singleton y)) (consEnv y ρ) h'))

That fails exactly where a rule copies. The ground rules of pure bigraphs take parameters that use no edge (Definition 5): an edge has no place, so a copy could not tell whether it owns it. A replicated body containing ν holds an edge and is no parameter, the two processes of Theorem 9 have one agent, and the first stage keeps ν out of replicated bodies (Definition 6). Jensen states the cure: “If the effect we want is to create a private link for each replica, then we must use links that are bound rather than closed” [Jen06, p. 74].

The second stage declares binding in the signature, after Jensen [Jen06, §7.3]: one more control, nu, whose one port binds outward. Its scope is the node's parent [Jen06, Def 4.19], so it reaches the uses of y beside it. The encoding becomes νy.P ↦ ν(P | nuy) (§13):

def ob : OutBind sig
  | .nu, _ => true
  | _, _ => false

A parameter may now carry edges, provided it is binding-discrete: every edge it uses is bound by one of its own binders, every binder binds an edge, and every edge lies in one region (Definition 11). The instance copies each region with the edges bound in it. The three rules are the same Lean terms in both stages; only the parameters admitted, and the way they are copied, change:

def ccsRules : Rules sig Nat :=
  PRule.rules (fun P => ∃ b a, P = ssRule b a ∨ P = rsRule b a ∨ P = rrRule b a)

def ccsRulesB : Rules sig Nat :=
  PRule.rulesB ob (fun P => ∃ b a, P = ssRule b a ∨ P = rsRule b a ∨ P = rrRule b a)

In the server rule, d0 now carries its nu node and its edge, and ϱ(d) holds two copies, each with an edge of its own (Figure 16). The rules are where binding is used; the signature is where it is declared.

A toy: activity that changes, and data as a list

Between the rules and the calculus, §4–§5 try the definitions on a toy: two panels whose activity a toggle switches, and a set of numbers kept as a linked list. Chapter VI picks the toy up at full scale, in a model of a language trainer.

What is proved

For the second encoding, writing ⟦·⟧ for the agent of a process and ⊿ for reaction:

P → Q  ⟹  ⟦P⟧ ⊿ ⟦Q⟧    for every P
⟦P⟧ ⊿ b  ⟹  ∃Q. P → Q ∧ b = ⟦Q⟧    for every closed P

theorem react_iffB (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hcl : Closed p)
    (hp : NamesIn X.names ρ p) (b : Abstract sig Nat) :
    React ccsRulesB (agentB X ρ p hp) b ↔
      ∃ q, ∃ hr : Red p q, b = agentB X ρ q (NamesIn.of_red hr hp)

Closedness is needed because the environment names a dangling index, which may then be confused with a free channel (§11). Open processes, and whether equal agents come only from congruent processes, are still open (§14). Every result rests on the axioms propext and Quot.sound only.

§1 · Activity

A signature says, for each control, whether reaction may happen inside a node of that control. A room in which people move about is active; a sealed envelope is passive. Activity of a site is read off the nodes above it.

def NodeActive (G : Bg S I J) (v : G.V) : Prop := S.passive (G.ctrl v) = false

def SiteActive (G : Bg S I J) (s : Fin I.width) : Prop :=
  ∀ v, Anc G v (.inl s) → G.NodeActive v

def Active (G : Bg S I J) : Prop := ∀ s, G.SiteActive s

Activity is what lets a calculus say where computation may happen. In CCS a prefix guards its continuation: nothing inside a.P may move until the prefix is consumed. So every control of the CCS signatures below is passive, and an active context can place a reaction only at the top level of a process, beside other components and never inside one.

§2 · Ground rules and reaction

structure GroundRule (S : Sig Ctrl) (Name : Type) where
  {J : Iface Name}
  redex : Bg S Iface.origin J
  reactum : Bg S Iface.origin J

abbrev Rules (S : Sig Ctrl) (Name : Type) : Type 1 := GroundRule S Name → Prop

def React (R : Rules S Name) (a b : Abstract S Name) : Prop :=
  ∃ (ρ : GroundRule S Name) (K : Iface Name) (D : Bg S ρ.J K),
    R ρ ∧ D.Active ∧ a = Abstract.mk (comp D ρ.redex) ∧ b = Abstract.mk (comp D ρ.reactum)

The relation is stated on abstract bigraphs, the classes ⟪G⟫ of Chapter I. Milner defines it on concrete agents and closes it under equivalence; here the quotient does the closing, because two equivalent agents are one class. A set of rules is any predicate, so a rule set may be infinite. The CCS rules below are one ground rule for each channel, each polarity and each parameter.

theorem React.comp {R : Rules S Name} {a b a' b' : Abstract S Name} (h : React R a b)
    (E : Bg S J K) (hE : E.Active)
    (ha : Abstract.comp (Abstract.mk E) a = some a')
    (hb : Abstract.comp (Abstract.mk E) b = some b') : React R a' b'

§3 · Rules with parameters

A ground rule mentions whole agents. A rule of a calculus needs holes instead: CCS's communication rule works whatever the continuations are. A parametric rule has a redex and a reactum with sites, and a map saying what each site of the reactum is filled with.

structure PRule (S : Sig Ctrl) (Name : Type) where
  {m m' : Nat}
  {J : Iface Name}
  redex : Bg S (Iface.ofWidth m) J
  reactum : Bg S (Iface.ofWidth m') J
  ϱ : Fin m' → Fin m

noncomputable def inst {m m' : Nat} (ϱ : Fin m' → Fin m) (d : Bg S Iface.origin ⟨m, X⟩)
    (hd : d.NoEdges) : Bg S Iface.origin ⟨m', X⟩

noncomputable def PRule.ground (P : PRule S Name) [DecidableEq Name] {X : NameSet Name}
    (d : Bg S Iface.origin ⟨P.m, X⟩) (hd : d.NoEdges) : GroundRule S Name where
  J := Iface.par P.J (Iface.ofNames X)
  redex := comp (par P.redex (id' S (Iface.ofNames X))
    (ITO_of_disjoint (fun _ h => absurd h List.not_mem_nil))) d
  reactum := comp (par P.reactum (id' S (Iface.ofNames X))
    (ITO_of_disjoint (fun _ h => absurd h List.not_mem_nil))) (inst P.ϱ d hd)

def PRule.rules [DecidableEq Name] (Ps : PRule S Name → Prop) : Rules S Name :=
  fun ρ => ∃ (P : PRule S Name) (X : NameSet Name) (d : Bg S Iface.origin ⟨P.m, X⟩)
    (hd : d.NoEdges), Ps P ∧ ρ = P.ground d hd

The condition on d decides what copying means. Milner asks for more, that the parameter be discrete; here it is only asked to use no edge. Either way every port of the parameter is linked to a name, so the copies of a region are linked to the same names: they share every link. Milner's own example is a replicator rep whose rule copies its contents. Without discreteness the rule could also take a parameter with a closed link and give each copy a private one, and he concludes that a link which each copy should own “must be bound —not simply closed—” [JM04, §12]. This matters for CCS with replication, in §12.

theorem inst_comp {m m' m'' : Nat} (ϱ : Fin m'' → Fin m') (ϱ' : Fin m' → Fin m)
    (d : Bg S Iface.origin ⟨m, X⟩) (hd : d.NoEdges) :
    Abstract.mk (inst ϱ (inst ϱ' d hd) (inst_noEdges ϱ' d hd))
      = Abstract.mk (inst (fun j => ϱ' (ϱ j)) d hd)

§4 · Activity that changes

Activity belongs to a control, and the signature fixes it (Definition 1), so no node can become passive. A reaction can do the next best thing: replace a node by a node of another control, in the same place, keeping what it contains. A toy signature shows it. Two controls hold things, shown, which is active, and hidden, which is passive. A toggle request swaps them, and a ping becomes a pong wherever it may react.

inductive Toy where
  | shown | hidden | toggle | ping | pong
  | list | head | cell (v : Nat) | stop | add (v : Nat) | scan (v : Nat)
  deriving DecidableEq

def Toy.active : (c : Toy) → Toy.atomic c = false → Bool
  | .hidden, _ => false
  | _, _ => true

The toy is written in the terms of a simulator, BigraphSim: trees compiled to finite data, which a certified builder turns into the library's bigraphs, and runs whose every step is proved to be a reaction of the concrete theory of Chapter IV. The two rules:

toggle ∣ shown.□₀ ∣ hidden.□₁  ⟶  hidden.□₀ ∣ shown.□₁,    η = [0, 1]
ping  ⟶  pong

def toggleRule : RuleD Toy where
  redex := Tm.compile [] [[at_ .toggle, nd .shown [] [st 0], nd .hidden [] [st 1]]]
  reactum := Tm.compile [] [[nd .hidden [] [st 0], nd .shown [] [st 1]]]
  eta := [0, 1]

def pingRule : RuleD Toy where
  redex := Tm.compile [] [[at_ .ping]]
  reactum := Tm.compile [] [[at_ .pong]]
  eta := []

The toggle's instantiation is the identity, so each panel's contents go with it, and only the two controls change. The panel that was shown is now passive, and whatever it holds can no longer react; the one that was hidden is now active.

Start with two panels, the first shown, each holding a ping. Exactly one reaction is possible: the shown ping. The hidden one has an occurrence too, but the context above it is passive, so it is no reaction (Definition 2 asks for an active context).

theorem shown_reacts : (Match.step toy rules panels).length = 1 ∧ kidsOf pinged .shown = [.pong] ∧
    kidsOf pinged .hidden = [.ping] ∧ (Match.step toy rules pinged).isEmpty = true := by
  decide +kernel

theorem hidden_waits : (Match.whyNot toy (fun r => rules.contains r) pingRule pinged).head? =
    some "a passive control above the match blocks it (the context is not active)" := by
  decide +kernel

A request inside a passive node is not dropped: it waits. Place a toggle beside the panels, and two reactions follow, the toggle and then the ping it released.

theorem toggle_releases : (go toggled).fired.length = 2 ∧ kidsOf (final (go toggled)) .shown = [.pong] ∧
    kidsOf (final (go toggled)) .hidden = [.pong] := by
  decide +kernel

theorem toggle_certified : Run.Chain (Run.Certified toy rules) (go toggled).states :=
  Run.run_sound _ _ 8 _ ⟨by decide +kernel, rfl, rfl⟩

Chapter VI picks this up in the Miolingo model, where the panels are an app's views. There a request clicked inside a hidden view waits in the same way, and a disabled button turns out to be a different thing from a passive control.

§5 · Data as a list

Data goes into a bigraph as parameters of controls. cell 1 and cell 3 are two controls, so the signature is infinite, and a rule that reads a value is a family of rules indexed by it. One thing no single rule can do is test that something is absent. A rule applies where its redex occurs (Definition 2), and says nothing about what does not occur. So “add v unless it is already there” needs a set of rules that turns absence into something positive, and a list does that.

The list holds a head, its cells, and a sentinel stop. A cell has two ports, self and next. The head's port shares a link with the first cell's self, each cell's next with the self of the cell after it, and the last next with stop. A request add v places a scan at the head, and the scan walks the list:

add v ∣ head[p]  ⟶  head[p] ∣ scan v[p]
scan v[p] ∣ cell v[p,q]  ⟶  cell v[p,q]    found: nothing is added
scan v[p] ∣ cell w[p,q]  ⟶  cell w[p,q] ∣ scan v[q]    w ≠ v: move on
scan v[p] ∣ stop[p]  ⟶  cell v[p,q] ∣ stop[q]    the end: append, q a new edge

Equality of values is in the redex: the found rule holds the same v twice. Inequality is in the family's index: the rule that moves on exists only for w ≠ v. A link could not be compared that way, since a context may join two names of a redex, but a value can. The rule that moves on, and the rule set, with the families instantiated at 1, 2 and 3:

def skip (v w : Nat) : RuleD Toy where
  redex := Tm.compile [("p", 0), ("q", 1)] [[at_ (.scan v) ["p"], at_ (.cell w) ["p", "q"]]]
  reactum := Tm.compile [("p", 0), ("q", 1)] [[at_ (.cell w) ["p", "q"], at_ (.scan v) ["q"]]]
  eta := []

def rules : List (RuleD Toy) := [toggleRule, pingRule] ++ vals.flatMap fun v =>
  [start v, hit v, atEnd v] ++ (vals.filter (· != v)).map (skip v)

theorem add_absent : (go add2).fired.length = 4 ∧ walk (final (go add2)) = [1, 3, 2] := by
  decide +kernel

theorem add_present : (go add3).fired.length = 3 ∧ walk (final (go add3)) = [1, 3] := by
  decide +kernel

theorem add_twice : (terminals 8 add2twice).all (walk · == [1, 2]) ∧
    (terminals 8 add2twice).length > 1 := by
  decide +kernel

The last is the point of the list. Two requests to add the same value, made at once, end with one cell in every interleaving, because a scan still behind the sentinel meets the cell the other appended. It is checked on a list of one cell, which keeps the interleavings few enough for the kernel to follow them all. Chapter VI picks this up as well: the Miolingo model's vocabulary table is such a list, its rows keyed by a word, a language and a user.

§6 · The finite check

The first test was the smallest calculus that communicates: finite CCS with prefix, parallel and 0, and no choice, restriction or recursion.

inductive Proc where
  | nil : Proc
  | pre : Act → Proc → Proc
  | par : Proc → Proc → Proc
deriving DecidableEq

inductive Red : Proc → Proc → Prop where
  | comm (α p q) {β} (hβ : β = co α) : Red (.par (.pre α p) (.pre β q)) (.par p q)
  | parL {p p'} (q) : Red p p' → Red (.par p q) (.par p' q)
  | parR (p) {q q'} : Red q q' → Red (.par p q) (.par p q')
  | struct {p p' q' q} : SC p p' → Red p' q' → SC q' q → Red p q

A prefix a.P is a passive node, snd or rcv, with one port linked to its channel and the nodes of P inside it. P | Q puts the nodes of both side by side, and 0 is the empty region. A process is encoded over a set of outer names that contains its channels. The single rule, one for each channel a, is Milner's without the sums:

theorem sc_sound {X : NameSet Nat} {p q : Proc} (h : SC p q) (hp : NamesIn X p)
    (hq : NamesIn X q) : agent X p hp = agent X q hq

theorem sc_not_complete :
    agent X0 (.pre (.snd 0) (.par .nil .nil)) (by decide)
        = agent X0 (.pre (.snd 0) .nil) (by decide)
      ∧ ¬ SC (.pre (.snd 0) (.par .nil .nil)) (.pre (.snd 0) .nil) := by
  refine ⟨(PosIso.preCong _ (.parNil .nil)).agent_eq _ _, fun h => ?_⟩
  have hp := sc_topPres h
  simp [topPres] at hp

theorem react_iff {X : NameSet Nat} {p : Proc} (hp : NamesIn X p) (b : Abstract sig Nat) :
    React ccsRules (agent X p hp) b ↔ ∃ q, ∃ hq : NamesIn X q, Red p q ∧ b = agent X q hq

Locus's own encoding of CCS, the starting point of this work, is confluent: it cannot show two partners competing for one message. Bigraphs show it. In a.0 | ā.0 | ā.(b̄.0 | b.0), two senders compete for one receiver. If the first wins, what is left is 0 | 0 | ā.(b̄.0 | b.0), stuck. If the second wins, it is 0 | (b̄.0 | b.0) | ā.0, which reacts once more.

theorem two_futures :
    React ccsRules (agent X01 Locus.CCS.D (by decide)) (agent X01 Locus.CCS.D1 (by decide))
      ∧ React ccsRules (agent X01 Locus.CCS.D (by decide)) (agent X01 Locus.CCS.D2a (by decide))
      ∧ agent X01 Locus.CCS.D1 (by decide) ≠ agent X01 Locus.CCS.D2a (by decide) := by
  refine ⟨red_sound Locus.CCS.red_D_D1 (by decide), red_sound Locus.CCS.red_D_D2a (by decide), ?_⟩
  intro h
  obtain ⟨v, hc, r, hr⟩ := TopRcv.of_mk_eq h ⟨.inl (.inr (.inr none)), rfl, 0, rfl⟩
  rcases v with ((e | e) | (_ | (_ | e) | (_ | e)))
  · exact e.elim
  · exact e.elim
  · cases hc
  · cases hc
  · exact e.elim
  · cases hr
  · exact e.elim

§7 · CCS with choice, restriction and replication

The second test widens the calculus to Milner's CCS of Pure bigraphs, with choice and restriction [Mil05, §11], and adds recursion in the form of replicated prefixes !α.P. A replicated prefix is a server: each time a partner offers the co-action, a fresh copy of P starts and the server stays.

mutual
inductive Proc where
  | nil : Proc
  | par : Proc → Proc → Proc
  | res : Proc → Proc
  | sum : Sum → Proc
  | rep : Act → Proc → Proc
inductive Sum where
  | pre : Act → Proc → Sum
  | plus : Sum → Sum → Sum
end

A channel is a free name or a de Bruijn index: bound i is the name bound by the i-th enclosing ν. So processes that differ only in the names of bound channels are equal as Lean terms, and scope extrusion, P | νQ ≡ ν(P | Q) when P does not use the bound name, shifts the indices of P instead of renaming. Reduction picks a summand of each partner:

inductive Red : Proc → Proc → Prop where
  | comm {α p m β q n} (h₁ : InSum α p m) (h₂ : InSum β q n) (hβ : β = co α) :
      Red (.par (.sum m) (.sum n)) (.par p q)
  | repSum {α p β q n} (h₂ : InSum β q n) (hβ : β = co α) :
      Red (.par (.rep α p) (.sum n)) (.par (.par (.rep α p) p) q)
  | repRep {α p β q} (hβ : β = co α) :
      Red (.par (.rep α p) (.rep β q)) (.par (.par (.rep α p) (.rep β q)) (.par p q))
  | parL {p p'} (q) : Red p p' → Red (.par p q) (.par p' q)
  | res {p p'} : Red p p' → Red (.res p) (.res p')
  | struct {p p' q' q} : SC p p' → Red p' q' → SC q' q → Red p q

mutual
/-- **The stage-1 fragment**: every replicated body is free of `ν`. -/
def Proc.WF : Proc → Prop
  | .nil => True
  | .par p q => p.WF ∧ q.WF
  | .res p => p.WF
  | .sum m => m.WF
  | .rep _ p => p.ResFree
def Sum.WF : Sum → Prop
  | .pre _ p => p.WF
  | .plus m n => m.WF ∧ n.WF
end

§8 · The encoding

mutual
/-- The shape of a process. -/
def shapeP : Proc → Shape sig
  | .nil => .empty
  | .par p q => (shapeP p).par (shapeP q)
  | .res p => (shapeP p).res
  | .sum m => (shapeS m).node Lab.alt
  | .rep α p => (shapeP p).node (Lab.rep α)
/-- The shape of a sum: its summands side by side, under no node yet. -/
def shapeS : Sum → Shape sig
  | .pre α p => (shapeP p).node (Lab.pre α)
  | .plus m n => (shapeS m).par (shapeS n)
end

Lean builds the encoding in two steps. A Shape is a forest of nodes, a set of edges, and for each port a reference: an edge, a free name, or a dangling index not yet bound. Each process former is an operation on shapes, so shapeP is a structural recursion. The bigraph of a shape, over a set of outer names, gives each dangling index a name from an environment ρ. Shapes are not particular to CCS: they live in Bigraph/Shapes/, generic in the signature (Shape sig is a shape over CCS's), and the π-calculus of Chapter III is built on the same ones. A CCS label becomes a label of that layer by Lab.lab, its channel by Chan.toS.

def enc (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) :
    Bg sig Iface.origin ⟨1, X⟩

def agent (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) :
    Abstract sig Nat :=
  Abstract.mk (enc X ρ p h)

theorem sc_sound {X : NameSet Nat} {ρ : Nat → Nat} {p q : Proc} (h : SC p q)
    (hp : NamesIn X.names ρ p) : agent X ρ p hp = agent X ρ q (NamesIn.of_sc h hp)

§9 · Three rules

CCS has three ways for two top-level components to communicate: two sums, a server and a sum, or two servers. Each is a parametric rule, one for each channel a and each polarity (which partner sends). The figures show the rules on a in one polarity each.

def ssRule (b : Bool) (a : Nat) : PRule sig Nat where
  redex := (ssRedex b).bg a
  reactum := ssReactum.bg a
  ϱ := ssInst

def rsRule (b : Bool) (a : Nat) : PRule sig Nat where
  redex := (rsRedex b).bg a
  reactum := (rsReactum b).bg a
  ϱ := rsInst

def rrRule (b : Bool) (a : Nat) : PRule sig Nat where
  redex := (rrRedex b).bg a
  reactum := (rrReactum b).bg a
  ϱ := rrInst

def ccsRules : Rules sig Nat :=
  PRule.rules (fun P => ∃ b a, P = ssRule b a ∨ P = rsRule b a ∨ P = rrRule b a)

The first is Milner's. The other two are ours: Milner's encoding is of finite CCS, and his text has no rule for replication [Mil05, §11].

§10 · Every reduction is a reaction

theorem red_sound {p q : Proc} (h : Red p q) : ∀ (X : NameSet Nat) (ρ : Nat → Nat), p.WF →
    (hp : NamesIn X.names ρ p) → React ccsRules (agent X ρ p hp) (agent X ρ q (NamesIn.of_red h hp))

Three instances, each a theorem in Bigraph/Dynamics.lean obtained from Theorem 7:

theorem react_choice :
    React ccsRules (agent Xabc ρ0 pChoice (by decide)) (agent Xabc ρ0 qChoice (by decide)) :=
  red_sound red_choice Xabc ρ0 (by simp [pChoice]; wf) (by decide)

Two things in the proof go beyond the finite check. A parameter may have no used edge, so the private names of a continuation cannot travel inside it. They are opened into fresh outer names of the parameter and closed again by the context. And a rule that discards a region leaves the edges that only that region used with no points; the agents agree because idle edges are forgotten.

§11 · Every reaction is a reduction

Completeness is the harder direction. A reaction of an agent comes from some rule, in some active context, with some parameter, and nothing says these line up with the process. They have to be found.

def Closed (p : Proc) : Prop := ∀ (ρ ρ' : Nat → Nat) (n : Nat), n ∈ p.fn ρ 0 → n ∈ p.fn ρ' 0

theorem react_complete (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hwf : p.WF) (hcl : Closed p)
    (hp : NamesIn X.names ρ p) {b : Abstract sig Nat} (h : React ccsRules (agent X ρ p hp) b) :
    ∃ q, ∃ hr : Red p q, b = agent X ρ q (NamesIn.of_red hr hp)

theorem react_iff (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hwf : p.WF) (hcl : Closed p)
    (hp : NamesIn X.names ρ p) (b : Abstract sig Nat) :
    React ccsRules (agent X ρ p hp) b ↔ ∃ q, ∃ hr : Red p q, b = agent X ρ q (NamesIn.of_red hr hp) :=
  ⟨react_complete X ρ hwf hcl hp, fun ⟨_, hr, hb⟩ => hb ▸ red_sound hr X ρ hwf hp⟩

The proof has three parts.

• The occurrence, read back. The equivalence between the agent and the rule instance in its context sends the rule's nodes to nodes of the process. Because every control is passive, they are top-level components and the prefixes directly inside them. Their controls, parents and links are read off: the controls give the polarity, and the links give the channel, which is where closedness is used.
• The process, rearranged. The process is brought to prenex form ν…ν(T | rest), with T the two matched components and the matched summands brought to the front. Every step is a structural congruence together with an isomorphism of shapes that tracks where each node goes, so the matched nodes are known in the rearranged process. The CCS reduction is then read off.
• Occurrence determinacy. For that reduction there is a canonical rule instance, by an explicit equivalence that sends the matched nodes to the rule's nodes. A general lemma says that two rule instances, equivalent by a map that fixes the rule's nodes, have equivalent reactums. So the given reactum is the canonical one, which is the agent of the reduct.

Closedness is a hypothesis because the environment may give a dangling index the name of a free channel. With ρ 0 = n, bound 0 and free n are linked to the same outer name, while CCS keeps them apart. No counterexample for open processes has been built, so whether completeness fails for them is open, not refuted.

Milner states the correspondence for his encoding of finite CCS with the remark that it “is easy to demonstrate” [Mil05, Prop 11.5], and Jensen proves the analogue for a finite π-calculus from a characterisation of reaction stated without proof [Jen06, Lemma 7.6, Theorem 7.7]. Here that step is proved, for a calculus with choice, restriction and replication. It is not quite Milner's form, P → P′ iff ⟦P⟧ ⊿ ⟦P′⟧. That form also needs equal agents to come from congruent processes, which Milner states for finite CCS with an outline of the proof [Mil05, Theorem 11.4], and which is open here.

§12 · Where the fragment stops

The fragment forbids ν inside a replicated body. Here is why. Take νy.!a.ȳ.0, where every copy of the body sends on the same private y, and !a.νy.ȳ.0, where every copy has its own.

theorem boundary :
    agent Xabc ρ0 pOut (by decide) = agent Xabc ρ0 pIn (by decide) ∧ ¬ SC pOut pIn :=
  ⟨res_rep_agent Xabc ρ0 (.rcv a) 0 rfl _ _ _, res_rep_not_sc _ _ trivial⟩

theorem res_rep_agent (X : NameSet Nat) (ρ : Nat → Nat) (α : Act) (n : Nat)
    (hα : α.chan = .free n) (P : Proc) (h₁ : NamesIn X.names ρ (.res (.rep α P)))
    (h₂ : NamesIn X.names ρ (.rep α (.res P))) :
    agent X ρ (.res (.rep α P)) h₁ = agent X ρ (.rep α (.res P)) h₂

So a rule that copies a server's body cannot give each copy its own y: from the agent it cannot tell whether the body owns y. Milner says this of his encoding: “in CCS with recursion (or replication), we cannot encode a restriction νx as name-closure in bigraphs, since this would not meet the requirement that every instance of a replicated process containing νx should have its own ‘private copy’ of x” [Mil05, p. 51]. It is the CCS face of his replicator example in §3.

§13 · Private names that are copied

Lifting the restriction means giving a private name a place, so that copying a region copies the names that belong to it. Milner's answer is binding: a link that each copy is to own must be bound inside the copied region, not simply closed [JM04, §12]. Jensen carries this out for the π-calculus with replication [Jen06, §7.3], and the second stage follows him.

def ob : OutBind sig
  | .nu, _ => true
  | _, _ => false

def nuS : Shape S := Shape.empty.node (nuLab (.bound 0))

mutual
/-- **The shape of a process**, restriction with a binder node. -/
def shapeB : Proc → Shape sig
  | .nil => .empty
  | .par p q => (shapeB p).par (shapeB q)
  | .res p => ((shapeB p).par nuS).res
  | .sum m => (shapeBS m).node Lab.alt
  | .rep α p => (shapeB p).node (Lab.rep α)
def shapeBS : Sum → Shape sig
  | .pre α p => (shapeB p).node (Lab.pre α)
  | .plus m n => (shapeBS m).par (shapeBS n)
end

Every law of structural congruence is again an isomorphism of shapes, so congruent processes are again one agent (sc_soundB). Scope extrusion holds because the nu node's parent is the same on both sides.

structure BDiscrete (ob : OutBind S) {m : Nat} (d : Bg S Iface.origin ⟨m, X⟩) where
  reg : d.E → Fin m
  loc : ∀ (v : d.V) (i : Fin (S.ar (d.ctrl v))) (e : d.E),
    d.link (.inr ⟨v, i⟩) = .inl e → d.root v = reg e
  bound : ∀ e, d.EdgeUsed e →
    ∃ (v : d.V) (i : Fin (S.ar (d.ctrl v))), ob (d.ctrl v) i = true ∧ d.link (.inr ⟨v, i⟩) = .inl e
  binds : ∀ (v : d.V) (i : Fin (S.ar (d.ctrl v))), ob (d.ctrl v) i = true →
    ∃ e, d.link (.inr ⟨v, i⟩) = .inl e

noncomputable def instB (ϱ : Fin m' → Fin m) (d : Bg S Iface.origin ⟨m, X⟩)
    (hb : BDiscrete ob d) : Bg S Iface.origin ⟨m', X⟩

def PRule.rulesB (ob : OutBind S) (Ps : PRule S Name → Prop) : Rules S Name :=
  fun ρ => ∃ (P : PRule S Name) (X : NameSet Name) (d : Bg S Iface.origin ⟨P.m, X⟩)
    (hb : BDiscrete ob d), Ps P ∧ ρ = P.groundB d hb

The three rules are those of §9, unchanged. Only their parameters change: in a server's rule the parameter holds the server's body, binders and all, and the instance gives the copy its own nu nodes and edges.

def ccsRulesB : Rules sig Nat :=
  PRule.rulesB ob (fun P => ∃ b a, P = ssRule b a ∨ P = rsRule b a ∨ P = rrRule b a)

theorem red_soundB {p q : Proc} (h : Red p q) : ∀ (X : NameSet Nat) (ρ : Nat → Nat),
    (hp : NamesIn X.names ρ p) →
      React ccsRulesB (agentB X ρ p hp) (agentB X ρ q (NamesIn.of_red h hp))

theorem react_completeB (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hcl : Closed p)
    (hp : NamesIn X.names ρ p) {b : Abstract sig Nat} (h : React ccsRulesB (agentB X ρ p hp) b) :
    ∃ q, ∃ hr : Red p q, b = agentB X ρ q (NamesIn.of_red hr hp)

theorem react_iffB (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hcl : Closed p)
    (hp : NamesIn X.names ρ p) (b : Abstract sig Nat) :
    React ccsRulesB (agentB X ρ p hp) b ↔
      ∃ q, ∃ hr : Red p q, b = agentB X ρ q (NamesIn.of_red hr hp) :=
  ⟨react_completeB X ρ hcl hp, fun ⟨_, hr, hb⟩ => hb ▸ red_soundB hr X ρ hp⟩

theorem boundaryB : agentB Xabc ρ0 pOut (by decide) ≠ agentB Xabc ρ0 pIn (by decide) :=
  res_rep_agentB_ne Xabc ρ0 (.rcv a) _ _ _

theorem res_rep_agentB_ne (X : NameSet Nat) (ρ : Nat → Nat) (α : Act) (P : Proc)
    (h₁ : NamesIn X.names ρ (.res (.rep α P))) (h₂ : NamesIn X.names ρ (.rep α (.res P))) :
    agentB X ρ (.res (.rep α P)) h₁ ≠ agentB X ρ (.rep α (.res P)) h₂

Two choices differ from Jensen's, and are recorded in docs/dynamics-plan.md. The control nu is not declared atomic: nothing is ever placed inside a nu node, and no theorem here needs the constraint. Contexts are all pure bigraphs, not only those obeying the scope rule, so completeness is stated over more contexts, which is the stronger form. Of the scope rule, a parameter needs only the part that copying uses: each edge lies within one region.

Still open: completeness for open processes, for the reason given in §11, and, for both encodings, whether equal agents come only from congruent processes.

§14 · What has been proved

PROVED means sorry-free in Lean, with the axioms checked: every result below rests on propext and Quot.sound only.

Dynamics is beyond BiCoq, the Coq formalisation this library ports, whose authors name it as their next step [MAP+25, §7].

§15 · References

1. [JM04]Ole Høgh Jensen and Robin Milner. Bigraphs and mobile processes (revised). Technical Report UCAM-CL-TR-580, University of Cambridge Computer Laboratory, February 2004. cl.cam.ac.uk/techreports/UCAM-CL-TR-580.pdf.
2. [Mil05]Robin Milner. Pure bigraphs. Technical Report UCAM-CL-TR-614, University of Cambridge Computer Laboratory, January 2005. Journal version: Pure bigraphs: structure and dynamics, Information and Computation 204(1):60–122, 2006, doi:10.1016/j.ic.2005.07.003. Numbering here is the report's; the journal text was not seen.
3. [Jen06]Ole Høgh Jensen. Mobile Processes in Bigraphs. Dissertation, October 2006, supervised by Robin Milner. cl.cam.ac.uk/archive/rm135/Jensen-monograph.pdf. The PDF does not name the institution.
4. [MAP+25]Cécile Marcon, Cyril Allignol, Celia Picard, Blair Archibald, Michele Sevegnani and Xavier Thirioux. BiCoq : Bigraphs Formalisation with Coq. In SAC '25, the 40th ACM/SIGAPP Symposium on Applied Computing, 2025, article 4, pp. 1982–1989. doi:10.1145/3672608.3707824.

The quotations are checked against transcriptions of the sources in docs/sources/.