locus: Blueprint

6.4. The matcher🔗

Definition6.4.1
uses 1used by 1✓L∃∀N
Tagsbridgednew

For a finite list of rules, \mathrm{step}(a) lists the triples (k, o, r) in which o is a candidate occurrence of the k-th rule in a, found by search, that passes the check, and r is its result. An agent a is good when it is checked and ground.

Class: Match.step BRIDGED; Run.Good NEW.

Lean code for Definition6.4.1●2 definitions
  • defdefined in BigraphSim/Match.lean
    complete
    def step {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl)
  (rules : List (RuleD Ctrl)) (a : BD Ctrl) :
  List (Nat × Occ Ctrl × BD Ctrl)
    def step {Ctrl : Type} [DecidableEq Ctrl]
  (S : Sig Ctrl)
  (rules : List (RuleD Ctrl))
  (a : BD Ctrl) :
  List (Nat × Occ Ctrl × BD Ctrl)
    **The one-step successors** of an agent: for each rule (by index), each
checked occurrence and its result.
  • defdefined in BigraphSim/Run.lean
    complete
    def Good {Ctrl : Type} (S : Sig Ctrl) (a : BD Ctrl) : Prop
    def Good {Ctrl : Type} (S : Sig Ctrl)
  (a : BD Ctrl) : Prop
    An agent: a good ground description (no sites, no inner names).
Theorem6.4.2
Statement uses 2
Statement dependency previews
Preview
Theorem 6.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 6.4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Every step the matcher returns is a reaction: for a good and \mathcal{R} the rules of the list,

(k, o, r) \in \mathrm{step}(a) \;\Longrightarrow\; o \checkmark a \;\wedge\; r = \mathrm{result}(o) \;\wedge\; \llbracket a \rrbracket \longrightarrow_{\mathcal{R}} \llbracket r \rrbracket .

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

Lean code for Theorem6.4.2●1 theorem
  • theoremdefined in BigraphSim/Match.lean
    complete
    theorem step_sound {Ctrl : Type} [DecidableEq Ctrl] {S : Sig Ctrl}
  {rules : List (RuleD Ctrl)} {a : BD Ctrl} (ha : a.check S = true)
  (has : a.sites = []) (hai : a.inner = []) {k : Nat} {o : Occ Ctrl}
  {r : BD Ctrl} (h : (k, o, r) ∈ Match.step S rules a) :
  ∃ hc,
    r = o.result ∧
      ⟦a⟧ ⟶[BRS
          (rulesOf fun r' => (fun r => rules.contains r) r' = true)]
        ⟦o.result⟧
    theorem step_sound {Ctrl : Type}
  [DecidableEq Ctrl] {S : Sig Ctrl}
  {rules : List (RuleD Ctrl)}
  {a : BD Ctrl} (ha : a.check S = true)
  (has : a.sites = [])
  (hai : a.inner = []) {k : Nat}
  {o : Occ Ctrl} {r : BD Ctrl}
  (h : (k, o, r) ∈ Match.step S rules a) :
  ∃ hc,
    r = o.result ∧
      ⟦a⟧ ⟶[BRS
          (rulesOf fun r' =>
            (fun r => rules.contains r)
                r' =
              true)]
        ⟦o.result⟧
    **Every successor the simulator offers is a reaction** of the library's
bigraphical reactive system of the rule list, by `Occ.sound`.
Theorem6.4.3
uses 1used by 1✓L∃∀N

The matcher is complete under guard G1: every root of every redex has a node child. For every signature, every rule list satisfying G1 and every good agent a, each reaction of the library is found up to support equivalence (the r found is checked and fits the outer face of a):

\llbracket a \rrbracket \longrightarrow_{\mathcal{R}} a' \;\Longrightarrow\; \exists (k, o, r) \in \mathrm{step}(a).\;\; a' \bumpeq \llbracket r \rrbracket .

Whether G1 can be dropped is OPEN.

Rests on NEW: Par, RuleG.g1.

Lean code for Theorem6.4.3●3 declarations
  • theoremdefined in Logic/COccG1.lean
    complete
    theorem cocc_G1 {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl) : COccG1 S
    theorem cocc_G1 {Ctrl : Type} [DecidableEq Ctrl]
  (S : Sig Ctrl) : COccG1 S
    **Matcher completeness under G1** (C-occ″).
  • defdefined in Logic/COcc.lean
    complete
    def COcc {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl)
  (rules : List (RuleD Ctrl)) (a : BD Ctrl) (ha : a.check S = true)
  (has : a.sites = []) (hai : a.inner = []) : Prop
    def COcc {Ctrl : Type} [DecidableEq Ctrl]
  (S : Sig Ctrl)
  (rules : List (RuleD Ctrl))
  (a : BD Ctrl) (ha : a.check S = true)
  (has : a.sites = [])
  (hai : a.inner = []) : Prop
    **C-occ for a rule list and a good agent `a`**: every reaction of the
library from `a` is `≏` to the result of a successor in
`Match.step S rules a`.
  • defdefined in Logic/COcc.lean
    complete
    def g1 {Ctrl : Type} (r : RuleD Ctrl) : Bool
    def g1 {Ctrl : Type} (r : RuleD Ctrl) : Bool
    **G1**: every redex root has a node child.
Theorem6.4.4
uses 1used by 0✓L∃∀N

REFUTED for the first matcher (\mathrm{step}_1, kept frozen in the library): completeness fails already for a rule that satisfies G1. The countermodel is the rule k \mid \square_0 \to k, which discards its parameter, and the agent a_0 with, at its root, a k and two rooms, each room holding a k (every k on an edge of its own): the library's context may keep a room, and that matcher put every sibling into the parameter. For the current matcher this rule and agent are covered by Theorem 6.4.3.

\neg\, \forall a'.\;\; \llbracket a_0 \rrbracket \longrightarrow_{\mathcal{R}} a' \;\Longrightarrow\; \exists (k, o, r) \in \mathrm{step}_1(a_0).\;\; a' \bumpeq \llbracket r \rrbracket .

Rests on NEW: BD.Fits, BD.outFace, COccCounter.agentA, COccCounter.dropR, Item, Match.embeds, Occ, Par; not audited: COccV1, Test.T, Test.sig.

Lean code for Theorem6.4.4●1 theorem
  • theoremdefined in Logic/COcc.lean
    complete
    theorem cocc_refuted :
  ¬COccV1 Test.sig [COccCounter.dropR] COccCounter.agentA
      COccCounter.agentA_check ⋯ ⋯
    theorem cocc_refuted :
  ¬COccV1 Test.sig [COccCounter.dropR]
      COccCounter.agentA
      COccCounter.agentA_check ⋯ ⋯
    **C-occ, unrestricted, is REFUTED**: `agentA` reacts in the library to
an agent that is support equivalent to no successor the matcher
offers.