3.2. Reaction🔗

Definition3.2.1

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 3.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsfrom source

Given a set \mathcal{R} of ground rules (r, r'), an abstract bigraph reacts, a \longrightarrow_{\mathcal{R}} a', when a = D \circ r and a' = D \circ r' for a rule in \mathcal{R} and an active context D.

Lean code for Definition3.2.1●1 definition

defdefined in Bigraph/React.lean

complete

def React {Ctrl Name : Type} {S : Sig Ctrl} (R : Bg.Rules S Name)
  (a b : Bg.Abstract S Name) : Prop

def React {Ctrl Name : Type} {S : Sig Ctrl}
  (R : Bg.Rules S Name)
  (a b : Bg.Abstract S Name) : Prop

**Reaction**, `a ⊿ b` (Def 12.1): `a` is the class of `D ◦ r` and `b`
the class of `D ◦ r'` for a rule `(r, r')` and an active context `D`.
Closure under ≏ and ≎ is the quotient's.

Theorem3.2.2

uses 1used by 0✓L∃∀N

Reaction is closed under active contexts: for E active, whenever both composites are defined (composition of abstract bigraphs is partial),

a \longrightarrow_{\mathcal{R}} b \;\Longrightarrow\; E \circ a \longrightarrow_{\mathcal{R}} E \circ b .

Lean code for Theorem3.2.2●1 theorem

theoremdefined in Bigraph/React.lean

complete

theorem comp {Ctrl Name : Type} {S : Sig Ctrl} {J K : Iface Name}
  [DecidableEq Name] {R : Bg.Rules S Name}
  {a b a' b' : Bg.Abstract S Name} (h : a ⟶[R] b) (E : Bg S J K)
  (hE : E.Active) (ha : ⟪E⟫ ⊚ a = some a') (hb : ⟪E⟫ ⊚ b = some b') :
  a' ⟶[R] b'

theorem comp {Ctrl Name : Type} {S : Sig Ctrl}
  {J K : Iface Name} [DecidableEq Name]
  {R : Bg.Rules S Name}
  {a b a' b' : Bg.Abstract S Name}
  (h : a ⟶[R] b) (E : Bg S J K)
  (hE : E.Active) (ha : ⟪E⟫ ⊚ a = some a')
  (hb : ⟪E⟫ ⊚ b = some b') : a' ⟶[R] b'

**Reaction is closed under active contexts** (the closure Def 12.1
builds in): if `a ⊿ b` and `E` is active, then `E ◦ a ⊿ E ◦ b`, where
both composites are defined.

Theorem3.2.3

uses 1used by 0✓L∃∀N

In any reactive system whose redexes have relative pushouts (Leifer and Milner 2000), bisimilarity of the derived labelled transitions is a congruence: for every context C,

a \sim b \;\Longrightarrow\; C \circ a \sim C \circ b .

The theorem is generic in the category, and it is not applied to bigraphs here: concrete bigraphs form a precategory, not a category, and the chapter on concrete bigraphs proves the congruence there by the route of TR-580.

Rests on UNBRIDGED: Bisimilar, Reactive.

Lean code for Theorem3.2.3●1 theorem

theoremdefined in Bigraph/Reactive.lean

complete

theorem bisim_cong.{u, v} {𝒞 : Cat} (R : Reactive 𝒞) (hR : HasRedexRPOs R)
  {m n : 𝒞.Obj} (C : 𝒞.Hom m n) {a b : 𝒞.Hom R.zero m} (h : a ∼ b) :
  𝒞.comp C a ∼ 𝒞.comp C b

theorem bisim_cong.{u, v} {𝒞 : Cat}
  (R : Reactive 𝒞) (hR : HasRedexRPOs R)
  {m n : 𝒞.Obj} (C : 𝒞.Hom m n)
  {a b : 𝒞.Hom R.zero m} (h : a ∼ b) :
  𝒞.comp C a ∼ 𝒞.comp C b

**Theorem 1 (strong congruence)**: with all redex-RPOs, bisimilarity is
preserved by every context.