locus: Blueprint

6.6. Erasing data, and image-finiteness🔗

Theorem6.6.1
uses 1used by 0✓L∃∀N

Controls may carry data, so a rule family may be infinite. Let \kappa map the controls of S to those of S_K, keeping arity, atomicity and activity, and act on descriptions, rules and certificates by renaming controls. Erasing data is a simulation of checked occurrences (E1), the erased rule being taken from the family of all rule data:

o \checkmark^{S}_{F} a \;\Longrightarrow\; \kappa(o) \checkmark^{S_K}_{\top} \kappa(a) \;\wedge\; \mathrm{rule}(\kappa(o)) = \kappa(\mathrm{rule}(o)) \;\wedge\; \mathrm{result}(\kappa(o)) = \kappa(\mathrm{result}(o)) .

Rests on NEW: Erases, Item, Occ, Par; not audited: BD.mapCtrl, Occ.mapCtrl, RuleD.mapCtrl.

Lean code for Theorem6.6.1●2 declarations
  • theoremdefined in BigraphSim/Erase.lean
    complete
    theorem check_mapCtrl {Ctrl K : Type} {κ : Ctrl → K} {S : Sig Ctrl} {SK : Sig K}
  [DecidableEq Ctrl] [DecidableEq K] (hκ : Erases S SK κ)
  {fam : RuleD Ctrl → Bool} {a : BD Ctrl} {o : Occ Ctrl}
  (h : Occ.check S fam a o = true) :
  Occ.check SK (fun x => true) (BD.mapCtrl κ a) (Occ.mapCtrl κ o) =
      true ∧
    (Occ.mapCtrl κ o).rule = RuleD.mapCtrl κ o.rule ∧
      (Occ.mapCtrl κ o).result = BD.mapCtrl κ o.result
    theorem check_mapCtrl {Ctrl K : Type}
  {κ : Ctrl → K} {S : Sig Ctrl}
  {SK : Sig K} [DecidableEq Ctrl]
  [DecidableEq K] (hκ : Erases S SK κ)
  {fam : RuleD Ctrl → Bool} {a : BD Ctrl}
  {o : Occ Ctrl}
  (h : Occ.check S fam a o = true) :
  Occ.check SK (fun x => true)
        (BD.mapCtrl κ a)
        (Occ.mapCtrl κ o) =
      true ∧
    (Occ.mapCtrl κ o).rule =
        RuleD.mapCtrl κ o.rule ∧
      (Occ.mapCtrl κ o).result =
        BD.mapCtrl κ o.result
    **(E1) Erasing the data is a simulation.**  If the certificate `o`
checks against `a` for the family `fam`, then the erased certificate
checks against the erased agent, for the erased rule given explicitly
(any family containing it), and its result is the erased result.
  • structure(3 fields)defined in BigraphSim/Erase.lean
    complete
    structure Erases {Ctrl K : Type} (S : Sig Ctrl) (SK : Sig K) (κ : Ctrl → K) : Prop
    structure Erases {Ctrl K : Type} (S : Sig Ctrl)
  (SK : Sig K) (κ : Ctrl → K) : Prop
    **`κ` erases `S` to `SK`**: the same arity, atomicity and activity.

    Fields

    ar : ∀ (c : Ctrl), SK.ar (κ c) = S.ar c
    atomic : ∀ (c : Ctrl), SK.atomic (κ c) = S.atomic c
    active : ∀ (c : Ctrl) (h : S.atomic c = false) (h' : SK.atomic (κ c) = false), SK.active (κ c) h' = S.active c h
Theorem6.6.2
uses 1used by 1✓L∃∀N

A generator g is complete for a family F when, for every finite list cs of controls, g(cs) lists every member of F whose redex controls lie in cs. A set of parametric rules is locally finite when, for every such cs, finitely many of its rules have their redex controls in cs.

g \text{ complete for } F \;\Longrightarrow\; \mathcal{R}_F \text{ locally finite} .

Rests on NEW: GenComplete, LocallyFinite, rulesOf.

Lean code for Theorem6.6.2●3 declarations
  • theoremdefined in Logic/ImageFiniteLFData.lean
    complete
    theorem rulesOf_lf {Ctrl : Type} [DecidableEq Ctrl] {S : Sig Ctrl}
  {fam : RuleD Ctrl → Prop} {g : List Ctrl → List (RuleD Ctrl)}
  (hg : GenComplete fam g) : LocallyFinite (rulesOf fam)
    theorem rulesOf_lf {Ctrl : Type}
  [DecidableEq Ctrl] {S : Sig Ctrl}
  {fam : RuleD Ctrl → Prop}
  {g : List Ctrl → List (RuleD Ctrl)}
  (hg : GenComplete fam g) :
  LocallyFinite (rulesOf fam)
    **G2-bridge** (PROVED): a generator complete for `fam` makes `rulesOf fam`
locally finite.
  • defdefined in BigraphSim/Erase.lean
    complete
    def GenComplete {Ctrl : Type} (fam : RuleD Ctrl → Prop)
  (g : List Ctrl → List (RuleD Ctrl)) : Prop
    def GenComplete {Ctrl : Type}
  (fam : RuleD Ctrl → Prop)
  (g : List Ctrl → List (RuleD Ctrl)) :
  Prop
    **A generator complete for a family**: given any finite set of controls,
it lists every member of the family whose redex controls lie in it.
  • defdefined in Logic/ImageFiniteLF.lean
    complete
    def LocallyFinite {Ctrl : Type} {S : Sig Ctrl} (rules : PRule S → Prop) :
  Prop
    def LocallyFinite {Ctrl : Type} {S : Sig Ctrl}
  (rules : PRule S → Prop) : Prop
    **A locally finite family of parametric rules**: for every finite list
of controls, finitely many rules have every control of their redex in
the list.
Theorem6.6.3
uses 1used by 0✓L∃∀N

CLASSICAL. The reactive system of a locally finite rule set is image-finite up to support equivalence: for every agent a, label L and set of locations \lambda there is a finite list l of agents with

a \xrightarrow{L}_{\lambda} a' \;\Longrightarrow\; \exists c \in l.\;\; a' \bumpeq c .

With Theorem 6.6.2, which is choice-free, this holds for every family with a complete generator.

Rests on NEW: ImageFinite, LocallyFinite.

Lean code for Theorem6.6.3●1 theorem
  • theoremdefined in Logic/ImageFiniteLF.lean
    complete
    theorem brs_imageFinite_lf {Ctrl : Type} {S : Sig Ctrl} {rules : PRule S → Prop}
  (hR : LocallyFinite rules) : ImageFinite (BRS rules)
    theorem brs_imageFinite_lf {Ctrl : Type}
  {S : Sig Ctrl} {rules : PRule S → Prop}
  (hR : LocallyFinite rules) :
  ImageFinite (BRS rules)
    **Statement G2** (CLASSICAL): a BRS over ´BIG_h with a locally finite
family of parametric rules is image-finite up to support equivalence.