locus · bigraph tutorial · Chapter V
To show that two agents behave alike, Jensen and Milner proposed checking only the transitions in which the agent itself takes part. Their theorem fails for a rule that copies its parameter twice, as Jensen found, and holds for linear rules, which copy each parameter at most once. This chapter re-derives Jensen's counterexample, checks it in the kernel, and mechanises the repair. Every figure is computed from a Lean term and every result is kernel-checked.
Chapter IV, Contexts, Labels and Locations, derived labelled transitions from reaction rules and showed that bisimilarity on them is a congruence. Proving two agents bisimilar still means matching every transition of each, and an agent has many transitions in which it plays no part: a context brings a redex of its own, and the agent sits by. Jensen and Milner's engaged transitions leave those out [JM04, Def 13.5]. Their adequacy theorem says that, when every redex is simple, matching the engaged transitions alone already gives bisimilarity on prime agents [JM04, Thm 13.7].
What is known, and what is new here. The theorem fails as the report states it, and this is not a new finding. The counterexample is Ole Jensen's: Milner's book gives it, "due to Ole Jensen" [Mil08, Example 8.17]. The repair, for rules that copy no parameter twice, is Jensen's theorem [Jen06, Thm 5.30(2)] and Milner's [Mil08, Thm 8.19]. Both are proved there on paper. This chapter re-derives the counterexample in the report's setting, which locus did before checking it against the book, and checks it in the kernel; and it mechanises the repair, following the report's proof.
How this chapter is made. As in the other chapters, no figure is drawn by
hand. The rules and agents are concrete bigraphs, terms of
Bigraph/Concrete/AdequacyCounter.lean. lake exe bigraphdraw maps each
one into the library's bigraphs by Big.toBg, reads it off with
Bg.describe, and labels it with its Lean source. Each node is labelled with its
control and its number, as in Chapter IV: K₀ is node
0, with control K. The one name, the number 0, is drawn
as x.
The theory is the library Bigraph/Concrete/ of
Chapter IV, with parametric rules and the proof of the theorem added. It follows
Jensen and Milner's report [JM04].
Numbering is separate for definitions, figures and theorems, and the generator checks every reference and every citation.
A transition a —L▷ a' rests on an IPO square L ∘ a = D ∘ r, where
r is a ground redex generated by a parametric rule. The ground redex has two
parts: the nodes of the rule's own redex, and the parameter that fills its sites. The
transition is engaged when the agent shares a node or an edge with the first part.
The agent then takes part in the reaction itself, and is not merely carried along inside a
parameter or left beside the redex.
Definition 1 (Engaged transition, FPE). A standard transition is
engaged if it can be based on a ground rule whose parametric redex shares support with the
agent [JM04, Def 13.5]. Rs is the part of the
ground redex's support that the parametric redex contributes. FPE keeps the engaged transitions
between prime interfaces.
def Engaged (rules : PRule S → Prop) : (BRS rules).SubTS := fun {_ J} a L loc a' =>
∃ (K : (BRS rules).Obj) (r r' : (BRS rules).Hom (BRS rules).origin K)
(D : (BRS rules).Hom K J) (y : (BRS rules).Hom (BRS rules).origin J) (Rs : Nat → Bool),
GenRule rules r r' Rs ∧ (BRS rules).Active D ∧ (BRS rules).IsIPO a r L D ∧
loc = (fun j => ∃ i, (BRS rules).wid D i = j) ∧ (BRS rules).Comp D r' y ∧
(BRS rules).SuppEquiv a' y ∧ ∃ v, (BRS rules).supp a v = true ∧ Rs v = true
def FPE (rules : PRule S → Prop) : (BRS rules).SubTS := fun {I J} a L loc a' =>
(BRS rules).width I = 1 ∧ (BRS rules).width J = 1 ∧ Engaged rules a L loc a'
Definition 2 (Relative bisimilarity). A relation is a bisimulation
relative to a set M of transitions if it is symmetric and every transition of
a in M is matched by a standard transition of b, at the
same label and location, with the residuals again related
[JM04, Def 5.8]. Only the transitions of M
need matching, but the matching transitions may be any.
def IsRelBisim (M : SubTS W) (S : W.ARel) : Prop :=
(∀ {I : W.Obj} (a b : W.Hom W.origin I), S a b → S b a) ∧
∀ {I J : W.Obj} (a b : W.Hom W.origin I) (L : W.Hom I J) (loc : Fin (W.width J) → Prop)
(a' : W.Hom W.origin J), S a b → W.Trans a L loc a' → M a L loc a' → (∃ x, W.Comp L b x) →
∃ b', W.Trans b L loc b' ∧ S a' b'
def RelBisim (M : SubTS W) {I : W.Obj} (a b : W.Hom W.origin I) : Prop :=
∃ S : W.ARel, IsRelBisim M S ∧ S a b
Every bisimulation is a relative one, so a ∼ b implies
a ∼^FPE b. The adequacy theorem claims the converse for prime agents. If it held,
a proof of bisimilarity could ignore every transition in which the agent plays no part.
The rules of Chapter II already had parameters. A parametric rule has a
redex R with m sites, a reactum R' with m'
sites, and an instantiation η that tells each site of the reactum which parameter
it receives [JM04, Def 12.1]. A ground instance fills the
redex's sites with a discrete parameter d, one region per site, and the reactum's
site j with a copy of the region η j of d. Copying keeps
the parameter's wiring outside the copies
[JM04, Def 9.18]: two copies of a region whose nodes are
linked to a name stay linked to that one name.
Definition 3 (Parametric rule, generated ground rules). A rule
ρ generates the ground rule (r, r') with
r = π • ((R ⊗ id_X) ∘ d) and r' = σ • ((R' ⊗ id_X) ∘ τ • η̄(d)),
for a discrete hard parameter d, names X and renamings
π, σ, τ of the nodes and edges.
structure PRule where
/-- The width of the redex's inner face. -/
m : Nat
/-- The width of the reactum's inner face. -/
m' : Nat
/-- The common outer face. -/
J : Face
/-- The parametric redex. -/
R : BigH S ⟨m, NSet.empty⟩ J
/-- The parametric reactum. -/
R' : BigH S ⟨m', NSet.empty⟩ J
/-- The instantiation. -/
η : Fin m' → Fin m
inductive GenRule (rules : PRule S → Prop) :
{J : Face} → BigH S Face.origin J → BigH S Face.origin J → (Nat → Bool) → Prop
| mk {ρ : PRule S} (hρ : rules ρ) {X : NSet} (hX : ρ.J.names.Disjoint X)
{d : BigH S Face.origin (Face.tensor ⟨ρ.m, NSet.empty⟩ ⟨0, X⟩)} (hd : d.big.Discrete)
{r₀ y : BigH S Face.origin (Face.tensor ρ.J ⟨0, X⟩)}
(hr₀ : (BIGH S).Comp (ρ.redexX X hX) d r₀) (τ : Perm)
(hy : (BIGH S).Comp (ρ.reactumX X hX) ((BigH.inst ρ.η d).tr τ) y) (π σ : Perm)
{r r' : BigH S Face.origin (Face.tensor ρ.J ⟨0, X⟩)} (hr : r₀.tr π = r) (hr' : y.tr σ = r')
{Rs : Nat → Bool} (hRs : ∀ v, Rs v = ρ.R.big.L.supp (π.g v)) :
GenRule rules r r' Rs
Definition 4 (Simple redex). No idle names and no barren region, no two sites siblings, prime, open (no edges) and guarding (no site at a root) [JM04, Def 13.1]. The adequacy theorem asks every parametric redex to be simple.
structure Simple {m : Nat} {J : Face} (R : BigH S ⟨m, NSet.empty⟩ J) : Prop where
/-- No idle names: every outer name is linked to. -/
noIdleNames : R.big.NoIdleNames
/-- No barren region. -/
noBarren : ∀ r, ¬ R.big.P.Barren (.inr r)
/-- No two sites are siblings. -/
noSiblings : ∀ s s' : Fin m, R.big.P.prnt (.inl s) = R.big.P.prnt (.inl s') → s = s'
/-- Prime: the outer face has width one. -/
prime : J.width = 1
/-- Open: every link is an outer name. -/
isOpen : R.big.IsOpen
/-- Guarding: no site has a root as its parent. -/
guarding : ∀ (s : Fin m) (r : Fin J.width), R.big.P.prnt (.inl s) ≠ .inr r
The counterexample uses three controls: A, which has one site inside it and no
ports; K, an atom with one port; and W, an atom with none. It has
two rules. The first, dup, opens an A and makes two copies of what
was inside it.
dup : A.(p) —▷ p | p. The redex
A.□ has one site; the reactum merges two sites into one region. Its
instantiation sends both sites to the redex's one parameter, so the parameter is copied
twice.The second rule, link2, has no parameter: two K atoms on one name
react to one.
link2 : K_x | K_x —▷ K_x. Both
redexes are simple.def dup : PRule sig where m := 1 m' := 2 J := ⟨1, NSet.empty⟩ R := RA R' := merge η := fun _ => 0 def link2 : PRule sig where m := 0 m' := 0 J := ⟨1, N0⟩ R := RK2 R' := RK1 η := Fin.elim0
The agents are a₀ = /e K_e, one K whose port is on a closed link
e, and a₁ = W.
a₀ = /e K_e and
a₁ = W. The port of K₀ is on the edge 3, which nothing
outside a₀ can reach.Neither agent has an engaged transition. A parametric redex contributes an A
(dup) or two Ks on one link (link2). W is
neither. The K of a₀ could be one of link2's two, but
then the other K would have to come from the label and share a₀'s
closed edge, which no label can reach. So the relation that pairs agents without engaged
transitions is a relative bisimulation, and a₀ ∼^FPE a₁ holds vacuously.
They are not bisimilar. Put both in the context A.□.
A.(a₀) is dup's redex
composed with a₀: the context A.□ above, the agent below, their
composite on the right (comp_x₀).A.(a₀) reacts by dup. The ground redex's parameter is the discrete
K_x; the closure of x lies in the context. Both copies of
K are therefore closed into the one edge.
A.(/e K_e) —▷ /e(K_e | K_e), a transition
with the identity label (trans_x₀). The two copies K₁ and
K₂ share the edge 3, so link2 applies next./e(K_e | K_e) reacts again by link2. Every reaction of
A.W leads to an agent made only of Ws, which cannot react. If
a₀ ∼ a₁, the congruence of Chapter IV would give
A.(a₀) ∼ A.(a₁), and the second reaction could not be matched. So
a₀ ≁ a₁.
Theorem 1 (The adequacy theorem fails as stated). A BRS over hard
bigraphs whose redexes are simple, and two prime agents that are FPE-bisimilar relative to the
standard transitions but not bisimilar. This refutes
[JM04, Thm 13.7] as the report states it. It is
Jensen's counterexample [Mil08, Example 8.17], whose
controls L, M and N are A,
K and W here.
theorem adequacy_fails : (∀ ρ, rules ρ → Simple ρ.R) ∧ WRS.RelBisim (FPE rules) a₀ a₁ ∧
¬ (BRS rules).Bisim a₀ a₁
The source's proof divides into three cases, and the third covers an agent that lies inside the parameter. It relies on a lemma that rewrites an instance as a context applied to separate copies of the agent, each with its own closed links [JM04, Prop 9.22]. Copies made by instantiation share the closed links of what they copy.
Theorem 2 (Copies share closed links). Instantiating
/e K_e along the map 2 → 1 gives two Ks whose ports are
linked to one and the same edge.
theorem inst_shares_edge : ∃ u₀ u₁ e : Nat, u₀ ≠ u₁ ∧
(Big.inst (fun _ : Fin 2 => (0 : Fin 1)) a₀.big).L.link (.port u₀ 0) = some (.edge e) ∧
(Big.inst (fun _ : Fin 2 => (0 : Fin 1)) a₀.big).L.link (.port u₁ 0) = some (.edge e)
The counterexample needs a rule that copies its parameter twice. A rule whose instantiation is injective copies each parameter at most once, and may discard it.
Definition 5 (Linear rule). η is injective: no two
sites of the reactum receive the same parameter. In linear-logic terms such a rule is affine,
since a parameter may also be dropped.
def Linear (ρ : PRule S) : Prop := ∀ i j : Fin ρ.m', ρ.η i = ρ.η j → i = j
Two linear variants of dup keep its redex. unwrap copies the
parameter once; drop discards it and leaves a W.
unwrap : A.(p) —▷ p: the reactum
is the identity, its one site receiving the parameter once.drop : A.(p) —▷ W: the reactum
has no site, so the parameter is discarded.def unwrap : PRule sig where m := 1 m' := 1 J := ⟨1, NSet.empty⟩ R := RA R' := (BIGH sig).id ⟨1, NSet.empty⟩ η := fun j => j def drop : PRule sig where m := 1 m' := 0 J := ⟨1, NSet.empty⟩ R := RA R' := a₁ η := Fin.elim0
Theorem 3 (Adequacy for linear rules). In a BRS over hard bigraphs whose parametric redexes are simple and whose rules are linear, FPE-bisimilarity relative to the standard transitions coincides with bisimilarity on prime agents. On paper this is Jensen's theorem for affine rules [Jen06, Thm 5.30(2)] and Milner's [Mil08, Thm 8.19]; here it is checked in the report's setting.
theorem adequacy_of_linear {rules : PRule S → Prop} (hs : ∀ ρ, rules ρ → Simple ρ.R)
(hl : ∀ ρ, rules ρ → ρ.Linear) {I : Face} (hI : I.width = 1)
(a b : BigH S Face.origin I) :
WRS.RelBisim (FPE rules) a b ↔ (BRS rules).Bisim a b
Theorem 3 contains the earlier result for rules without parameters
(adequacy_of_m): a rule with no parameter has nothing to copy, so it is linear.
Theorem 1's rule dup is not linear, so the counterexample lies outside
Theorem 3.
theorem linear_of_m {ρ : PRule S} (hm : ρ.m = 0) : ρ.Linear := fun i _ _ => by
have := (ρ.η i).isLt
omega
theorem dup_not_linear : ¬ dup.Linear := fun h =>
absurd (h ⟨0, by decide⟩ ⟨1, by decide⟩ rfl) (by decide)
The proof follows the source's. Take the relation P that holds of
(a₀, a₁) when both are prime and a₀ ∼^FPE a₁, or when
a₀ ≎ a₁ (lean-support equivalence, which ignores idle edges). It is enough to show
that every transition a₀ —L▷ a₀', with L ∘ a₁ defined, is matched by
a transition a₁ —L▷ a₁' whose residual is linked to a₀' by a chain
of pairs (C ∘ b₀, C ∘ b₁) with P b₀ b₁, up to renaming
(WRS.bisim_of_match). Three cases cover every transition.
a₀ ∼^FPE a₁,
a₁ matches it with residuals again FPE-bisimilar.a₁ makes the same reaction beside the redex. The residuals are
G ∘ a₀ and G ∘ a₁ for one context G.Where the agent sits. Since the redex is simple and the agent is prime,
every node of a₀ is a node of the parameter d. They all lie in one
region of d, under one parent q, and the wiring D of the
square has no nodes [JM04, Lemma 13.6].
The replay. Replace a₀ by a₁ inside the
parameter, each port of a₁ on a fresh name of the new parameter
d₁. The new wiring D₁ sends each fresh name where
L ∘ a₁ links that port. The new square L ∘ a₁ = D₁ ∘ r₁ is an IPO.
The proof does not build the IPO from a characterisation of link-graph IPOs, which the library
lacks. It transfers the property: a relative bound for the new square becomes one for the old
square by putting a₀'s links back, and the old IPO gives the unique mediator
(Replay.Data.ipo₁).
The residuals. If the agent's region is copied by the reactum (once, since
the rule is linear), both residuals contain one copy of their agent. Cutting a₀
out of its residual and a₁ out of the replay's leaves the same context
G. If the region is discarded, the residuals differ only in idle edges:
a₀'s in one, a₁'s in the other. Then a₀' ≎ a₁', which
is in P, and ≎ respects the transitions when redexes are simple.
Theorem 4 (The third case). A transition of a prime
a₀ that is not engaged but whose redex meets a₀ is replayed by any
prime a₁ with L ∘ a₁ defined. The residuals are
G ∘ π•a₀ and G ∘ π•a₁ up to renaming when the agent's region is
copied, and lean-support equivalent when it is discarded.
theorem param_match {rules : PRule S → Prop} (hs : ∀ ρ, rules ρ → Simple ρ.R)
(hl : ∀ ρ, rules ρ → ρ.Linear) {I K₀ K : Face} (hI : I.width = 1)
{a₀ a₁ : BigH S Face.origin I} {L : BigH S I K} {r₀ r₀' : BigH S Face.origin K₀}
{Rs : Nat → Bool} {D₀ : BigH S K₀ K} {y₀ : BigH S Face.origin K}
(hg : GenRule rules r₀ r₀' Rs) (hD : (BRS rules).Active D₀)
(hipo : (BIGH S).IsIPO a₀ r₀ L D₀) (hy : (BIGH S).Comp D₀ r₀' y₀)
(hne : ∀ v, a₀.big.L.supp v = true → Rs v = false)
(hov : ∃ v, a₀.big.L.supp v = true ∧ r₀.big.L.supp v = true)
(hL : ∃ x, (BIGH S).Comp L a₁ x) :
∃ a₁', (BRS rules).Trans a₁ L (fun j => ∃ i, (BRS rules).wid D₀ i = j) a₁' ∧
((∃ (π : Perm) (G : BigH S I K) (z₀ z₁ : BigH S Face.origin K),
(BRS rules).SuppEquiv y₀ z₀ ∧ (BIGH S).Comp G (a₀.tr π) z₀ ∧
(BIGH S).Comp G (a₁.tr π) z₁ ∧ (BRS rules).SuppEquiv z₁ a₁') ∨
y₀.big.LeanEquiv a₁'.big)
The cut is the converse of composition. An occurrence of a ground agent a in a
ground z records that a's nodes, parents, edges and links are
z's, that its roots sit at one place p of z, that its
outer names go to the links f, and that nothing else in z has a
parent in a or a link to an edge of a.
Definition 6 (Occurrence). Occurs a z p f, with one
field for each of the conditions above.
structure Occurs {I K : Face} (a : Big S Face.origin I) (z : Big S Face.origin K)
(p : Nat ⊕ Fin K.width) (f : Nat → Option Lk) : Prop
Theorem 5 (The cut). An occurrence cuts out a context:
z = cut a z p f ∘ a, hard when z is. The context reads
z only off a, so two occurrences that agree off their agents, at the
same place along the same links, cut out the same context.
theorem comp_cut (h : Occurs a z p f) : (BIG S).Comp (cut a z p f h) a z
theorem cut_eq {a₀ a₁ : Big S Face.origin I} {z₀ z₁ : Big S Face.origin K}
(h₀ : Occurs a₀ z₀ p f) (h₁ : Occurs a₁ z₁ p f)
(hc : ∀ v, offCtrl a₀.P.ctrl z₀.P.ctrl v = offCtrl a₁.P.ctrl z₁.P.ctrl v)
(hp : ∀ v, cPrnt a₀ z₀ p (.inr v) = cPrnt a₁ z₁ p (.inr v))
(he : ∀ e, cEdge a₀ z₀ e = cEdge a₁ z₁ e)
(hl : ∀ v i, cLink a₀ z₀ f (.port v i) = cLink a₁ z₁ f (.port v i)) :
cut a₀ z₀ p f h₀ = cut a₁ z₁ p f h₁
To cut a₀ out of its residual, the copy of a₀ must sit at
a₀'s own node numbers, and everything else beyond them. A renaming does this, and
it is the one place where the proof uses linearity. If two copies were made of one node, both
would have to be renamed to that node.
Theorem 6 (Placing the copies). When η is injective
and the agent's nodes lie below F, one renaming sends each copy of an agent node
to that node and every other kept copy c to F + c.
theorem exists_place (hlin : ∀ i j : Fin m', η i = η j → i = j)
(hF : ∀ v, A.ctrl v ≠ none → v < F) :
∃ Θ : Perm, ∀ c p, Inst.keep P η c = some p → Θ.f c = placeF P η A F c
Weakening linearity would mean replacing this step alone. Copies would then be allowed, for instance, when the copied region has no closed link, which is what the counterexample needed.
Replace dup by either linear variant and keep link2. Neither agent
has an engaged transition under the new rules either, so a₀ ∼^FPE a₁ still holds,
and Theorem 3 now gives a₀ ∼ a₁. With unwrap, A.(a₀)
reacts to a₀ and A.(a₁) to a₁. With drop,
both react to W, and a₀'s edge is left idle.
Theorem 7 (The agents of Theorem 1 are bisimilar under linear
rules). Under unwrap and link2, and under drop
and link2, /e K_e ∼ W.
theorem repaired_unwrap : (BRS rulesU).Bisim a₀ a₁ :=
(adequacy_of_linear (fun ρ h => allRules_simple ρ (rulesU_all ρ h))
(fun _ h => h.elim (fun e => e ▸ unwrap_linear) (fun e => e ▸ PRule.linear_of_m rfl))
rfl a₀ a₁).1 (relBisim_of rulesU_all)
theorem repaired_drop : (BRS rulesD).Bisim a₀ a₁ :=
(adequacy_of_linear (fun ρ h => allRules_simple ρ (rulesD_all ρ h))
(fun _ h => h.elim (fun e => e ▸ drop_linear) (fun e => e ▸ PRule.linear_of_m rfl))
rfl a₀ a₁).1 (relBisim_of rulesD_all)
PROVED means sorry-free in Lean, with the axioms checked: every result below rests on
propext and Quot.sound at most. REFUTED means a kernel-checked
countermodel. The gate LocusGate/Behaviour.lean fixes the refutation, the result
for rules without parameters and Theorem 3. Theorem 3 was watched failing with the hypothesis of
linearity removed. The gate also checks that Theorem 3 gives the result without parameters and
that Theorem 1's rule is not linear.
| What | Where | Status |
|---|---|---|
| Engaged transitions, FPE, relative bisimilarity (Definitions 1, 2) | Concrete/Parametric, Concrete/Relative | PROVED |
| The adequacy theorem for simple rules, as the source states it (Theorem 1): Jensen's counterexample, kernel-checked | Concrete/AdequacyCounter | REFUTED |
| Copies made by instantiation share closed links (Theorem 2) | Concrete/AdequacyCounter | PROVED |
| The adequacy theorem for rules without parameters | Concrete/Adequacy | PROVED |
| The adequacy theorem for linear simple rules (Theorem 3), Jensen's and Milner's theorem mechanised, with the third case, the cut and the placement (Theorems 4 to 6) | Concrete/AdequacyLinear, Concrete/ParamCase, Concrete/ParamReplay, Concrete/ParamIPO, Concrete/Cut, Concrete/ParamResidual | PROVED |
| The counterexample's agents are bisimilar under linear rules (Theorem 7) | Concrete/AdequacyRepaired | PROVED |
Rules that copy a parameter more than once, under some further hypothesis. On paper, Jensen proves the theorem for any number of copies when the agents are open, with his own definition of simple [Jen06, Thm 5.30(1)]; Theorem 1's agent /e K_e is not open. Not mechanised here. | — | OPEN |
The quotations are checked against transcriptions of the sources in
docs/sources/.