locus: Blueprint

6.3. Occurrences and the checker🔗

Definition6.3.1
Statement uses 2
Statement dependency previews
Preview
Theorem 6.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 6
Reverse dependency previews
Preview
Theorem 6.3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgednew

A rule on data is a redex R, a reactum R' and a list \eta; a family F of them denotes the set \mathcal{R}_F of parametric rules of its checked members. An occurrence certificate o names a rule, a set of names X, a context D, a parameter d and a renumbering; its result is D \circ_{\mathrm d} ((R' \otimes \mathrm{id}_X) \circ_{\mathrm d} \bar\eta_{\mathrm d}(d)). The check o \checkmark_F a recomputes D \circ_{\mathrm d} ((R \otimes \mathrm{id}_X) \circ_{\mathrm d} d), compares it with the agent a under the renumbering, and tests that the rule is in F, that d is discrete, that D is active, and that every description involved passes its check. It does not test that the names of X are listed once: a certificate with the list doubled is accepted (Definition 6.2.4).

Class: RuleD, Occ.result, Occ.check BRIDGED; rulesOf BRIDGED and NEW; Occ NEW.

Lean code for Definition6.3.1●5 definitions
  • structure(3 fields)defined in BigraphSim/Rule.lean
    complete
    structure RuleD (Ctrl : Type) : Type
    structure RuleD (Ctrl : Type) : Type
    **A parametric reaction rule, on data.**

    Fields

    redex : BD Ctrl
    reactum : BD Ctrl
    eta : List Nat
    `eta[j]` is the redex site whose parameter reactum site `j` receives.
  • defdefined in BigraphSim/Rule.lean
    complete
    def rulesOf {Ctrl : Type} {S : Sig Ctrl} (fam : RuleD Ctrl → Prop) :
  PRule S → Prop
    def rulesOf {Ctrl : Type} {S : Sig Ctrl}
  (fam : RuleD Ctrl → Prop) :
  PRule S → Prop
    **The parametric rules of a family of rule data**: the checked members.
  • structure(5 fields)defined in BigraphSim/Occ.lean
    complete
    structure Occ (Ctrl : Type) : Type
    structure Occ (Ctrl : Type) : Type
    **An occurrence certificate.**

    Fields

    rule : RuleD Ctrl
    names : List Nat
    ctx : BD Ctrl
    param : BD Ctrl
    ren : Ren
  • defdefined in BigraphSim/Occ.lean
    complete
    def result {Ctrl : Type} (o : Occ Ctrl) : BD Ctrl
    def result {Ctrl : Type} (o : Occ Ctrl) :
  BD Ctrl
    **The result** `D ∘ ((R' ⊗ id_X) ∘ η̄(d))`.
  • defdefined in BigraphSim/Occ.lean
    complete
    def check {Ctrl : Type} (S : Sig Ctrl) (fam : RuleD Ctrl → Bool)
  (a : BD Ctrl) (o : Occ Ctrl) [DecidableEq Ctrl] : Bool
    def check {Ctrl : Type} (S : Sig Ctrl)
  (fam : RuleD Ctrl → Bool) (a : BD Ctrl)
  (o : Occ Ctrl) [DecidableEq Ctrl] : Bool
    **The check.**
Theorem6.3.2
uses 1used by 1✓L∃∀N

The checker is sound: a checked occurrence is a reaction of the library's bigraphical reactive system. For a checked and ground (no sites, no inner names),

o \checkmark_F a \;\Longrightarrow\; \llbracket a \rrbracket \longrightarrow_{\mathcal{R}_F} \llbracket \mathrm{result}(o) \rrbracket .

Rests on NEW: BD.outFace, Occ, Par, rulesOf.

Lean code for Theorem6.3.2●1 theorem
  • theoremdefined in BigraphSim/Occ.lean
    complete
    theorem sound {Ctrl : Type} {S : Sig Ctrl} {fam : RuleD Ctrl → Bool}
  {a : BD Ctrl} {o : Occ Ctrl} [DecidableEq Ctrl]
  (ha : a.check S = true) (has : a.sites = []) (hai : a.inner = [])
  (h : Occ.check S fam a o = true) :
  ⟦a⟧ ⟶[BRS (rulesOf fun r => fam r = true)] ⟦o.result⟧
    theorem sound {Ctrl : Type} {S : Sig Ctrl}
  {fam : RuleD Ctrl → Bool} {a : BD Ctrl}
  {o : Occ Ctrl} [DecidableEq Ctrl]
  (ha : a.check S = true)
  (has : a.sites = [])
  (hai : a.inner = [])
  (h : Occ.check S fam a o = true) :
  ⟦a⟧ ⟶[BRS
      (rulesOf fun r => fam r = true)]
    ⟦o.result⟧
    **(S2) The occurrence checker is sound.**  If the certificate `o` checks
against the agent `a`, then `a` reacts to `o.result` in the library's
bigraphical reactive system of the family's rules.