locus: Blueprint

4.4. Parametric rules and engaged transitions🔗

Definition4.4.1
Statement uses 2
Statement dependency previews
Preview
Definition 4.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 4.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom sourcenot audited

A parametric rule is a redex R : m \to J, a reactum R' : m' \to J and an instantiation \eta : m' \to m; it is linear when \eta is injective. A set \mathcal{R} of parametric rules generates the ground rules r = \pi \bullet ((R \otimes \mathrm{id}_X) \circ d), r' \bumpeq (R' \otimes \mathrm{id}_X) \circ \bar\eta(d) for discrete parameters d, and so a wide reactive system over hard bigraphs (no barren root and no barren non-atomic node). A redex is simple when it has no idle names and no barren region, no two sites are siblings, and it is prime, open and guarding. A transition is engaged when the support of the agent meets that of the parametric redex; FPE is the set of engaged transitions between prime interfaces, and a \sim^{\mathrm{FPE}} b is the largest symmetric relation in which the FPE transitions are matched by transitions.

Class: PRule, BRS, Simple, FPE, WRS.RelBisim FROM SOURCE; PRule.Linear not audited.

Lean code for Definition4.4.1●6 definitions
  • structure(6 fields)defined in Bigraph/Concrete/Parametric.lean
    complete
    structure PRule {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Type
    structure PRule {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Type
    **A parametric reaction rule** (TR-580 Def 12.1, pure; Milner Def 8.5):
a parametric redex `R : m → J`, a parametric reactum `R' : m' → J`, and
an instantiation `η : m' → m`, the site `j` of the reactum receiving a
copy of the parameter `η j` of the redex.

    Fields

    m : Nat
    The width of the redex's inner face. 
    m' : Nat
    The width of the reactum's inner face. 
    J : Face
    The common outer face. 
    R : BigH S { width := self.m, names := NSet.empty } self.J
    The parametric redex. 
    R' : BigH S { width := self.m', names := NSet.empty } self.J
    The parametric reactum. 
    η : Fin self.m' → Fin self.m
    The instantiation.
  • defdefined in Bigraph/Concrete/Parametric.lean
    complete
    def Linear {Ctrl : Type} {S : Bigraph.Sig Ctrl} (ρ : PRule S) : Prop
    def Linear {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} (ρ : PRule S) :
  Prop
    **A linear rule**: its instantiation `η : m' → m` is injective, so each
parameter is copied at most once (it may be discarded; in linear-logic
terms the rule is affine; Jensen 2006 and Milner's book, Def 8.18, call
it affine).  The hypothesis of Theorem 13.7's repair
(`docs/g4-campaign.md` round 10), and a standing rule for every model
built on this library (HANDOVER, 2026-10-03).
  • defdefined in Bigraph/Concrete/Parametric.lean
    complete
    def BRS {Ctrl : Type} {S : Bigraph.Sig Ctrl} (rules : PRule S → Prop) : WRS
    def BRS {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (rules : PRule S → Prop) : WRS
    **A bigraphical reactive system** over ´BIG_h from parametric rules
(TR-580 Def 12.2, Prop 12.3, pure and hard).
  • structure(6 fields)defined in Bigraph/Concrete/Parametric.lean
    complete
    structure Simple {Ctrl : Type} {S : Bigraph.Sig Ctrl} {m : Nat} {J : Face}
  (R : BigH S { width := m, names := NSet.empty } J) : Prop
    structure Simple {Ctrl : Type}
  {S : Bigraph.Sig Ctrl} {m : Nat}
  {J : Face}
  (R :
    BigH S
      { width := m, names := NSet.empty }
      J) :
  Prop
    **A simple redex** (TR-580 Def 13.1, pure): no idle names and no barren
region; no two sites siblings; prime, open and guarding.  With no inner
names (the inner face is `⟨m, ∅⟩`) and every link free, the clauses "no
two inner names are peers", "free" and "no inner name is open" hold
of every pure redex.

    Fields

    noIdleNames : R.big.NoIdleNames
    No idle names: every outer name is linked to. 
    noBarren : ∀ (r : Fin J.width), ¬R.big.P.Barren (Sum.inr r)
    No barren region. 
    noSiblings : ∀ (s s' : Fin m), R.big.P.prnt (Sum.inl s) = R.big.P.prnt (Sum.inl s') → s = s'
    No two sites are siblings. 
    prime : J.width = 1
    Prime: the outer face has width one. 
    isOpen : R.big.IsOpen
    Open: every link is an outer name. 
    guarding : ∀ (s : Fin m) (r : Fin J.width), R.big.P.prnt (Sum.inl s) ≠ Sum.inr r
    Guarding: no site has a root as its parent.
  • defdefined in Bigraph/Concrete/Parametric.lean
    complete
    def FPE {Ctrl : Type} {S : Bigraph.Sig Ctrl} (rules : PRule S → Prop) :
  (BRS rules).SubTS
    def FPE {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (rules : PRule S → Prop) :
  (BRS rules).SubTS
    **The free prime engaged transition system FPE** (TR-580 Def 13.5,
pure, where every interface is free): the engaged transitions between
prime interfaces.
  • defdefined in Bigraph/Concrete/Relative.lean
    complete
    def RelBisim.{u, v} {W : WRS} (M : W.SubTS) {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    def RelBisim.{u, v} {W : WRS} (M : W.SubTS)
  {I : W.Obj} (a b : W.Hom W.origin I) :
  Prop
    **Relative bisimilarity** `∼^M`.
Theorem4.4.2
Statement uses 2
Statement dependency previews
Preview
Theorem 4.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

In the bigraphical reactive system of any set of parametric rules, for C \circ a_0 and C \circ a_1 defined,

a_0 \sim a_1 \;\Longrightarrow\; C \circ a_0 \sim C \circ a_1 .

Lean code for Theorem4.4.2●1 theorem
  • theoremdefined in Bigraph/Concrete/Parametric.lean
    complete
    theorem brs_bisim_congr {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  (rules : PRule S → Prop) {I J : (BRS rules).Obj}
  {a₀ a₁ : (BRS rules).Hom (BRS rules).origin I}
  (C : (BRS rules).Hom I J)
  {x₀ x₁ : (BRS rules).Hom (BRS rules).origin J} (h : a₀ ∼ a₁)
  (h₀ : C ◦ a₀ ≃ x₀) (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    theorem brs_bisim_congr {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  (rules : PRule S → Prop)
  {I J : (BRS rules).Obj}
  {a₀ a₁ :
    (BRS rules).Hom (BRS rules).origin I}
  (C : (BRS rules).Hom I J)
  {x₀ x₁ :
    (BRS rules).Hom (BRS rules).origin J}
  (h : a₀ ∼ a₁) (h₀ : C ◦ a₀ ≃ x₀)
  (h₁ : C ◦ a₁ ≃ x₁) : x₀ ∼ x₁
    **TR-580 Corollary 12.4 (congruence of wide bisimilarity)**, for a BRS
over ´BIG_h.
Theorem4.4.3
Statement uses 2
Statement dependency previews
Preview
Definition 4.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Engaged transitions are adequate for linear rules (TR-580 Thm 13.7 with linearity added; compare Jensen 2006, Thm 5.30(2), for affine rules and his own definition of simple, and Milner 2009, Thm 8.19, for nice systems). If every rule of \mathcal{R} has a simple redex and is linear, then for agents a, b of a prime interface,

a \sim^{\mathrm{FPE}} b \iff a \sim b .

Rests on not audited: PRule.Linear.

Lean code for Theorem4.4.3●1 theorem
  • theoremdefined in Bigraph/Concrete/AdequacyLinear.lean
    complete
    theorem adequacy_of_linear {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {rules : PRule S → Prop} (hs : ∀ (ρ : PRule S), rules ρ → Simple ρ.R)
  (hl : ∀ (ρ : PRule S), rules ρ → ρ.Linear) {I : Face}
  (hI : I.width = 1) (a b : BigH S Face.origin I) :
  WRS.RelBisim (fun {I J} => FPE rules) a b ↔ a ∼ b
    theorem adequacy_of_linear {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {rules : PRule S → Prop}
  (hs :
    ∀ (ρ : PRule S), rules ρ → Simple ρ.R)
  (hl :
    ∀ (ρ : PRule S), rules ρ → ρ.Linear)
  {I : Face} (hI : I.width = 1)
  (a b : BigH S Face.origin I) :
  WRS.RelBisim (fun {I J} => FPE rules) a
      b ↔
    a ∼ b
    **TR-580 Theorem 13.7 for linear simple rules**: in a BRS over ´BIG_h
whose parametric redexes are simple and whose instantiations are
injective (each parameter copied at most once), relative
FPE-bisimilarity coincides with bisimilarity on prime agents.
$$\frac{\forall\rho.\ \rho.R\ \text{simple},\ \rho.\eta\ \text{injective}
  \qquad \mathrm{width}(I) = 1}{a \sim^{\mathrm{FPE}} b \iff a \sim b}$$
Supersedes `adequacy_of_m`: `ρ.m = 0` makes `η` injective
(`PRule.linear_of_m`). The source's statement, without linearity, is
REFUTED by Jensen's counterexample (`AdequacyCounter.lean`). On paper
the theorem is Jensen's (2006, Thm 5.30(2)) and Milner's (book,
Thm 8.19); here it is mechanised. The proof is TR-580's, through the frame
`WRS.bisim_of_match`, with `P = (prime ∧ ∼^FPE) ∨ ≎`: an engaged
transition is in FPE (Case 1); a redex missing the agent is replayed
with `G ∘ a₀`, `G ∘ a₁` (Case 2, `disjoint_match`); a redex meeting the
agent only in the parameter is replayed by `param_match` (Case 3), with
`G ∘ π•a₀`, `G ∘ π•a₁` when the agent's region is copied and `≎` when it
is discarded; `≎` is matched by `leanH_respects`.
Theorem4.4.4
uses 1used by 0✓L∃∀N

REFUTED: adequacy for all simple rules, as TR-580 Thm 13.7 states it. The counterexample is Ole Jensen's (Milner 2009, Example 8.17). With the rules A.\square \to \square \mid \square, which is not linear, and K_x \mid K_x \to K_x, both redexes simple, and the prime agents a_0 = /e\, K_e and a_1 = W,

a_0 \sim^{\mathrm{FPE}} a_1 \;\text{ but }\; a_0 \not\sim a_1 .

Rests on not audited: AdequacyCounter.Ctl, AdequacyCounter.a₀, AdequacyCounter.a₁, AdequacyCounter.dup, AdequacyCounter.rules, AdequacyCounter.sig, NSet.empty, PRule.Linear.

Lean code for Theorem4.4.4●2 theorems
  • theoremdefined in Bigraph/Concrete/AdequacyCounter.lean
    complete
    theorem adequacy_fails :
  (∀ (ρ : PRule AdequacyCounter.sig),
      AdequacyCounter.rules ρ → Simple ρ.R) ∧
    WRS.RelBisim (fun {I J} => FPE AdequacyCounter.rules)
        AdequacyCounter.a₀ AdequacyCounter.a₁ ∧
      ¬AdequacyCounter.a₀ ∼ AdequacyCounter.a₁
    theorem adequacy_fails :
  (∀ (ρ : PRule AdequacyCounter.sig),
      AdequacyCounter.rules ρ →
        Simple ρ.R) ∧
    WRS.RelBisim
        (fun {I J} =>
          FPE AdequacyCounter.rules)
        AdequacyCounter.a₀
        AdequacyCounter.a₁ ∧
      ¬AdequacyCounter.a₀ ∼
          AdequacyCounter.a₁
    **TR-580 Theorem 13.7, REFUTED**, by Jensen's counterexample (Milner's
book, Example 8.17), kernel-checked: a BRS over ´BIG_h whose redexes
are simple, and two prime agents that are FPE-bisimilar relative to the
standard transitions but not bisimilar.
  • theoremdefined in Bigraph/Concrete/AdequacyRepaired.lean
    complete
    theorem dup_not_linear : ¬AdequacyCounter.dup.Linear
    theorem dup_not_linear :
  ¬AdequacyCounter.dup.Linear
    **`dup` is not linear**: it copies its parameter twice.

Adequacy without linearity for agents with no closed link (Jensen 2006, Thm 5.30(1), with his definition of simple) is OPEN: it has not been formalised.