IV Contexts, Labels and Locations

Theorem 1 (Place graphs have RPOs). Whenever two place graphs with a common domain have a bound, they have an RPO relative to it [JM04, Thm 7.8]. The proof builds Jensen and Milner's candidate [JM04, Construction 7.7]. Its roots are classes of an equivalence generated by a decidable relation on a finite set, computed in Lean without choice (Bigraph/Concrete/Classes.lean).

theorem plg_rpo {Ctrl : Type} {S : Sig Ctrl} {ℓ m₀ m₁ p : Nat} (A₀ : PlG S ℓ m₀)
    (A₁ : PlG S ℓ m₁) (D₀ : PlG S m₀ p) (D₁ : PlG S m₁ p) (hD : (PLG S).IsBound A₀ A₁ D₀ D₁) :
    ∃ b : (PLG S).RelBound A₀ A₁ D₀ D₁, (PLG S).IsRPO b

Theorem 2 (IPO pasting). Two IPO squares side by side make an IPO rectangle, given an RPO for the left-hand span [JM04, Prop 3.10]. The source supposes that "the diagram commutes", as Leifer and Milner do [LM00, p. 6]. In a category that follows from the two squares. In a precategory it does not, because the rectangle's composite need not be defined. The first Lean statement left the hypothesis out and was refuted by a six-object countermodel in which every other hypothesis holds; the statement proved carries it as hrc.

theorem ipo_paste {k m m₂ m' n' n : 𝒞.Obj} {a : 𝒞.Hom k m} {l : 𝒞.Hom k m'}
    {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n} {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n}
    {FC : 𝒞.Hom m n} {ED' : 𝒞.Hom m' n} {Ca : 𝒞.Hom k m₂}
    (hFC : 𝒞.Comp F C FC) (hED : 𝒞.Comp E D' ED') (hCa : 𝒞.Comp C a Ca)
    (hrc : 𝒞.IsBound Ca l F ED')
    (P : 𝒞.RelBound a l FC ED') (hP : 𝒞.IsRPO P)
    (hleft : 𝒞.IsIPO a l F' D') (hright : 𝒞.IsIPO C F' F E) :
    𝒞.IsIPO Ca l F ED'

The refutation of the first statement:

theorem ipo_paste_needs_commuting : ¬ ∀ (𝒞 : PreCat.{0, 0}) {k m m₂ m' n' n : 𝒞.Obj}
    {a : 𝒞.Hom k m} {l : 𝒞.Hom k m'}
    {C : 𝒞.Hom m m₂} {F' : 𝒞.Hom m n'} {F : 𝒞.Hom m₂ n} {D' : 𝒞.Hom m' n'} {E : 𝒞.Hom n' n}
    {FC : 𝒞.Hom m n} {ED' : 𝒞.Hom m' n} {Ca : 𝒞.Hom k m₂},
    𝒞.Comp F C FC → 𝒞.Comp E D' ED' → 𝒞.Comp C a Ca →
    ∀ (P : 𝒞.RelBound a l FC ED'), 𝒞.IsRPO P →
    𝒞.IsIPO a l F' D' → 𝒞.IsIPO C F' F E → 𝒞.IsIPO Ca l F ED'

Theorem 3 (Wide bisimilarity is a congruence). In a wide reactive system with RPOs, if a₀ ∼ a₁ then C ∘ a₀ ∼ C ∘ a₁ for every context C [JM04, Thm 5.5]. The proof is theirs, along the lines of Leifer's [Lei01, Thm 3.9], as they say [JM04, p. 32]: the pairs (C ∘ a₀, C ∘ a₁) form a bisimulation up to renaming of nodes. A transition of C ∘ a₀ is split by an RPO into a transition of a₀ and an IPO for C; a₁ answers the first, and IPO pasting (Theorem 2) puts the answer back together. TR-580 does not define "with RPOs" separately; here it is HasRPOs, every pair with a bound has an RPO relative to it.

def HasRPOs : Prop :=
  ∀ {H I₀ I₁ K : W.Obj} (f₀ : W.Hom H I₀) (f₁ : W.Hom H I₁) (g₀ : W.Hom I₀ K)
    (g₁ : W.Hom I₁ K), W.IsBound f₀ f₁ g₀ g₁ → ∃ b : W.RelBound f₀ f₁ g₀ g₁, W.IsRPO b

theorem bisim_congr (hR : W.HasRPOs) {I J : W.Obj} {a₀ a₁ : W.Hom W.origin I}
    (C : W.Hom I J) {x₀ x₁ : W.Hom W.origin J} (h : W.Bisim a₀ a₁) (h₀ : W.Comp C a₀ x₀)
    (h₁ : W.Comp C a₁ x₁) : W.Bisim x₀ x₁

Theorem 4 (For place graphs). Theorem 1 supplies the RPOs, so wide bisimilarity of place-graph agents is a congruence, for every set of ground rules closed under renaming.

theorem plg_bisim_congr (R : {J : Nat} → PlG S 0 J → PlG S 0 J → Prop)
    (hR : ∀ {J : Nat} {r r' : PlG S 0 J} (π σ : Perm), R r r' → R (r.tr π) (r'.tr σ))
    {I J : Nat} {a₀ a₁ : PlG S 0 I} (C : PlG S I J) {x₀ x₁ : PlG S 0 J}
    (h : (PLGW S R hR).Bisim a₀ a₁) (h₀ : (PLGW S R hR).Comp C a₀ x₀)
    (h₁ : (PLGW S R hR).Comp C a₁ x₁) : (PLGW S R hR).Bisim x₀ x₁

Theorem 5 (The same reaction, in different places). Both agents turn their K into an L under the identity label: a in region 0, b in region 1. Every identity-labelled transition of b is in region 1.

theorem a_trans : W.Trans a (PlG.id 2) (fun (j : Fin 2) => j = 0) a₁

theorem b_trans : W.Trans b (PlG.id 2) (fun (j : Fin 2) => j = 1) b₁

theorem b_trans_loc (loc : Fin 2 → Prop) (b' : PlG sig 0 2)
    (h : W.Trans b (PlG.id 2) loc b') : loc = fun j => j = 1

Theorem 6 (a and b are not bisimilar). The transition of a in region 0 has no answer from b in region 0.

theorem a_not_bisim : ¬ W.Bisim a b := by
  rintro ⟨S, ⟨_, hS⟩, hab⟩
  obtain ⟨b', hb, _⟩ := hS a b (PlG.id 2) _ a₁ hab a_trans ⟨b, W.id_left b⟩
  have h01 : (0 : Fin 2) = 1 := (congrFun (b_trans_loc _ b' hb) 0).mp rfl
  exact nomatch congrArg Fin.val h01

Theorem 7 (One reacts, the other is stuck). C ∘ b reacts under the identity label. C ∘ a has no identity-labelled transition at all: its only K lies under the passive M, and the context of any redex would have to be active there.

theorem ctx_b_trans : W.Trans cb (PlG.id 1) (fun (j : Fin 1) => j = 0) cb₁

theorem ctx_a_stuck (loc : Fin 1 → Prop) (y : PlG sig 0 1) : ¬ W.Trans ca (PlG.id 1) loc y

Theorem 8 (The context separates them). C ∘ a and C ∘ b are not bisimilar. With Theorem 4 this gives Theorem 6 a second time, from transitions of C ∘ a and C ∘ b only: were a ∼ b, the congruence would give C ∘ a ∼ C ∘ b.

theorem ctx_not_bisim : ¬ W.Bisim ca cb := by
  rintro ⟨S, ⟨hsymm, hS⟩, h01⟩
  obtain ⟨b', hb', _⟩ := hS cb ca (PlG.id 1) _ cb₁ (hsymm _ _ h01) ctx_b_trans ⟨ca, W.id_left ca⟩
  exact ctx_a_stuck _ b' hb'

theorem a_not_bisim_of_ctx : ¬ W.Bisim a b := fun h =>
  ctx_not_bisim (plg_bisim_congr rule rule_tr ctx h ⟨disj_ca, rfl⟩ ⟨disj_cb, rfl⟩)

Theorem 9 (Without locations, bisimilarity is not a congruence). Forgetting the location does not help C ∘ a, which has no identity-labelled transition anywhere. And a and b are bisimilar on unlocated transitions. The proof relates agents whose K-nodes sit directly in roots, the same number in each, and classifies every IPO of such an agent with a redex. Both members of each such pair have no barren root, so an IPO is a pushout followed by an iso, the case TR-580 singles out after its characterisation of place-graph IPOs [JM04, p. 42]. If the redex's node is the agent's K, the labels are the permutations of the regions; if it is fresh, they add a region holding a K. Either way the other agent has a transition with the same label.

theorem ctx_not_ubisim : ¬ W.UBisim ca cb := by
  rintro ⟨S, ⟨hsymm, hS⟩, h01⟩
  obtain ⟨b', ⟨_, hb'⟩, _⟩ :=
    hS cb ca (PlG.id 1) cb₁ (hsymm _ _ h01) ⟨_, ctx_b_trans⟩ ⟨ca, W.id_left ca⟩
  exact ctx_a_stuck _ b' hb'

theorem ubisim_not_congr : W.UBisim a b ∧ ¬ W.UBisim ca cb :=
  ⟨a_ubisim_b, ctx_not_ubisim⟩

Theorem 10 (RPOs for links and for bigraphs). Link graphs have RPOs [JM04, Thm 8.9]. The construction gives the legs the nodes and edges of the other side outside the shared part, and the top the rest of the bound, just as for place graphs; so a place-graph RPO and a link-graph RPO for the two halves of a bigraph pair into an RPO of bigraphs [JM04, Cor 9.6]. By Theorem 3, bisimilarity of bigraph agents is a congruence, for any ground rules [JM04, Cor 12.4]. The source prints the interface of the link-graph construction with the ports of the bound, P₃, where its proofs use the edges, E₃; the edges are what is formalised.

theorem lig_rpo {Ctrl : Type} {S : Sig Ctrl} {W X₀ X₁ Z : NSet} (A₀ : LiG S W X₀)
    (A₁ : LiG S W X₁) (D₀ : LiG S X₀ Z) (D₁ : LiG S X₁ Z) (hD : (LIG S).IsBound A₀ A₁ D₀ D₁) :
    ∃ b : (LIG S).RelBound A₀ A₁ D₀ D₁, (LIG S).IsRPO b

theorem big_rpo {I I₀ I₁ K : Face} (A₀ : Big S I I₀) (A₁ : Big S I I₁) (D₀ : Big S I₀ K)
    (D₁ : Big S I₁ K) (hD : (BIG S).IsBound A₀ A₁ D₀ D₁) :
    ∃ b : (BIG S).RelBound A₀ A₁ D₀ D₁, (BIG S).IsRPO b

theorem big_bisim_congr (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
    (hR : ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm), R r r' → R (r.tr π) (r'.tr σ))
    {I J : Face} {a₀ a₁ : Big S Face.origin I} (C : Big S I J) {x₀ x₁ : Big S Face.origin J}
    (h : (BIGW S R hR).Bisim a₀ a₁) (h₀ : (BIGW S R hR).Comp C a₀ x₀)
    (h₁ : (BIGW S R hR).Comp C a₁ x₁) : (BIGW S R hR).Bisim x₀ x₁

Theorem 11 (Behaviour passes to abstract bigraphs). Suppose every redex is lean and has no idle names. Then lean-support equivalence respects the transitions: equivalent agents have equivalent transitions, with the same labels and locations. Hence two agents are bisimilar iff their abstract classes are, and bisimilarity of abstract classes is a congruence [JM04, Cor 12.6]. The proof is Jensen and Milner's: a quotient that respects the transitions reflects and preserves bisimilarity [JM04, Thm 5.7], and adding fresh idle edges to one side of an IPO and to the opposite leg gives an IPO again [JM04, Prop 9.11].

theorem lean_transfer
    (hRl : ∀ {J} {r r' : Big S Face.origin J}, R r r' → r.IsLean ∧ r.NoIdleNames)
    {I : Face} (a b : Big S Face.origin I) :
    (BIGW S R hR).Bisim a b ↔
      (BIGW S R hR).QBisim (leanCong R hR) ((BIGW S R hR).cls (leanCong R hR) a)
        ((BIGW S R hR).cls (leanCong R hR) b)

theorem lean_congr (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
    (hR : ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm), R r r' → R (r.tr π) (r'.tr σ))
    (hRl : ∀ {J} {r r' : Big S Face.origin J}, R r r' → r.IsLean ∧ r.NoIdleNames)
    {I J : Face} {p q : (BIGW S R hR).Q (leanCong R hR) Face.origin I}
    (G : (BIGW S R hR).Q (leanCong R hR) I J) {x y : (BIGW S R hR).Q (leanCong R hR) Face.origin J}
    (h : (BIGW S R hR).QBisim (leanCong R hR) p q) (hx : (BIGW S R hR).QComp (leanCong R hR) G p x)
    (hy : (BIGW S R hR).QComp (leanCong R hR) G q y) : (BIGW S R hR).QBisim (leanCong R hR) x y

Theorem 12 (Lean redexes alone are not enough). Take two atomic controls K and L with no ports, and the rule that turns a K-atom into an L-atom under the outer face ⟨1, {0}⟩, with the name 0 idle. Every redex is lean. Let b be a K-node and a the same with one idle edge. The context that links the name 0 to that edge makes a react under the identity label, and b has no such transition, since it has no edge to link the name to. So a and b are lean-support equivalent, and not bisimilar.

theorem redex_lean : ∀ {J : Face} {r r' : Big sig Face.origin J}, R r r' → r.IsLean

theorem leanEquiv_not_bisim : Big.LeanEquiv a b ∧ ¬ W.Bisim a b

Theorem 13 (Abstract bigraphs are the library's). The map's kernel, and the transfer to Abstract, under the hypothesis of Theorem 11.

theorem abs_eq_iff {I J : Face} (A B : Big S I J) : A.abs = B.abs ↔ Big.LeanEquiv A B

theorem cor_12_6 (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
    (hR : ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm), R r r' → R (r.tr π) (r'.tr σ))
    (hRl : ∀ {J} {r r' : Big S Face.origin J}, R r r' → r.IsLean ∧ r.NoIdleNames)
    {I : Face} (a b : Big S Face.origin I) :
    (BIGW S R hR).Bisim a b ↔ WRS.RBisim (absRep R hR) a.abs b.abs

theorem cor_12_6_congr (R : {J : Face} → Big S Face.origin J → Big S Face.origin J → Prop)
    (hR : ∀ {J : Face} {r r' : Big S Face.origin J} (π σ : Perm), R r r' → R (r.tr π) (r'.tr σ))
    (hRl : ∀ {J} {r r' : Big S Face.origin J}, R r r' → r.IsLean ∧ r.NoIdleNames)
    {p q G x y : Abstract S Nat} (h : WRS.RBisim (absRep R hR) p q)
    (hx : Abstract.comp G p = some x) (hy : Abstract.comp G q = some y) :
    WRS.RBisim (absRep R hR) x y

Theorem 14 (Composition of place graphs is preserved). toPlace is the library's place graph of a concrete one, and toBg the library's bigraph, with no edges, when the signature has no ports.

theorem toPlace_comp {m n p : Nat} (B : PlG S n p) (A : PlG S m n) (h : A.Disjoint B) :
    Nonempty (PlaceGraph.Iso (B.comp A h).toPlace (PlaceGraph.comp B.toPlace A.toPlace))

def toBg {m n : Nat} (A : PlG S m n) (har : ∀ c, S.ar c = 0) :
    Bg S (Iface.ofWidth m : Iface Nat) (Iface.ofWidth n) where
  V := A.Node
  E := Empty
  finV := A.toPlace.fin
  finE := PlaceGraph.emptyFin
  ctrl := A.toPlace.ctrl
  prnt := A.toPlace.prnt
  link := fun
    | .inl x => absurd x.property List.not_mem_nil
    | .inr ⟨_, i⟩ => (Fin.cast (har _) i).elim0
  acyclic := A.toPlace.acyclic
  atomic_childless := A.toPlace.atomic_childless