6.1. Bigraphs as data🔗

Definition6.1.1

uses 0

Used by 6

Reverse dependency previews

Preview

Theorem 6.1.2

Loading preview

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

✓L∃∀N

Tagsbridgednew

A description d is a finite record: the number of roots, the parent of each site, a list of items (nodes and edges, numbered by position), the inner names with their links, and the outer names. The decidable check \mathrm{ok}(d) tests the invariants of a hard bigraph on the items, sites and links; it does not test that a name is listed once (Definition 6.2.4). A checked description whose widths and names are those of the faces I, J (it fits I \to J) builds a hard concrete bigraph \llbracket d \rrbracket : I \to J of the library.

Class: BD, BD.check, BD.toBigAt BRIDGED; BD.Fits NEW.

Lean code for Definition6.1.1●4 definitions

structure(5 fields)defined in BigraphSim/Data.lean

complete

structure BD (Ctrl : Type) : Type

structure BD (Ctrl : Type) : Type

**A bigraph as finite data.**

Fields

width : Nat

The outer width: the number of roots.

sites : List Par

The parent of each site; the inner width is the length.

items : List (Item Ctrl)

The support, numbered by position.

inner : List (Nat × Lk)

Each inner name with its link.

outer : List Nat

The outer names.

defdefined in BigraphSim/Data.lean

complete

def check {Ctrl : Type} (d : BD Ctrl) (S : Sig Ctrl) : Bool

def check {Ctrl : Type} (d : BD Ctrl)
  (S : Sig Ctrl) : Bool

**The check**: every invariant of a hard bigraph, decided on the data.

structure(4 fields)defined in BigraphSim/Data.lean

complete

structure Fits {Ctrl : Type} (d : BD Ctrl) (I J : Face) : Prop

structure Fits {Ctrl : Type} (d : BD Ctrl)
  (I J : Face) : Prop

**The data fits the faces `I → J`**: the same widths and the same names.

Fields

sites : d.sites.length = I.width

inner : ∀ (x : Nat), I.names.mem x = (List.map (fun x => x.fst) d.inner).contains x

width : d.width = J.width

outer : ∀ (y : Nat), J.names.mem y = d.outer.contains y

defdefined in BigraphSim/Data.lean

complete

def toBigAt {Ctrl : Type} {S : Sig Ctrl} (I J : Face) (d : BD Ctrl)
  (h : d.check S = true) (hf : d.Fits I J) : BigH S I J

def toBigAt {Ctrl : Type} {S : Sig Ctrl}
  (I J : Face) (d : BD Ctrl)
  (h : d.check S = true)
  (hf : d.Fits I J) : BigH S I J

**The builder**: a checked description fitting `I → J`, as the library's
hard bigraph `I → J`.

Theorem6.1.2

uses 1used by 0✓L∃∀N

The built bigraph is the data: for d checked and fitting I \to J, the control map, parent map, edge predicate and link map agree,

\mathrm{ctrl}_{\llbracket d \rrbracket} = \mathrm{ctrl}_d, \qquad \mathrm{prnt}_{\llbracket d \rrbracket} = \mathrm{prnt}_d, \qquad \mathrm{edge}_{\llbracket d \rrbracket} = \mathrm{edge}_d, \qquad \mathrm{link}_{\llbracket d \rrbracket} = \mathrm{link}_d .

That every hard bigraph is \llbracket d \rrbracket for some d, up to support translation, is OPEN.

Rests on NEW: BD.Fits, Item, Par; not audited: BD.ctrl, BD.isEdge, BD.link, BD.prnt, Big, LiG, PlG.

Lean code for Theorem6.1.2●1 theorem

theoremdefined in BigraphSim/Data.lean

complete

theorem toBig_faithful {Ctrl : Type} {S : Sig Ctrl} {d : BD Ctrl} {I J : Face}
  (h : d.check S = true) (hf : d.Fits I J) :
  ⟦d⟧.big.P.ctrl = d.ctrl ∧
    ⟦d⟧.big.P.prnt = d.prnt I.width J.width ∧
      ⟦d⟧.big.L.edge = d.isEdge ∧ ⟦d⟧.big.L.link = d.link

theorem toBig_faithful {Ctrl : Type}
  {S : Sig Ctrl} {d : BD Ctrl}
  {I J : Face} (h : d.check S = true)
  (hf : d.Fits I J) :
  ⟦d⟧.big.P.ctrl = d.ctrl ∧
    ⟦d⟧.big.P.prnt =
        d.prnt I.width J.width ∧
      ⟦d⟧.big.L.edge = d.isEdge ∧
        ⟦d⟧.big.L.link = d.link

**(S1a)** The bigraph built from `d` has `d`'s nodes and controls, `d`'s
parents, `d`'s edges and `d`'s links: what the data says is what the
bigraph is, so a picture of the data is a picture of the bigraph.

Theorem6.1.3

uses 1used by 1✓L∃∀N

Composition on data, B \circ_{\mathrm d} A, is the library's composition. For checked A fitting I \to J and B fitting J \to K, with B \circ_{\mathrm d} A checked, and \rho the rotation that moves the support of A past that of B,

\llbracket B \circ_{\mathrm d} A \rrbracket \;=\; \llbracket B \rrbracket \circ (\rho \bullet \llbracket A \rrbracket) .

Here \pi \bullet G is the support translation of G by \pi. In Lean the conclusion is stated as the composition relation Comp of the bigraph precategory (composition is partial there), not as an equation.

Rests on NEW: BD.Fits, Item, Perm, rot; not audited: BD.n, BigH.tr.

Lean code for Theorem6.1.3●2 declarations

defdefined in BigraphSim/Comp.lean

complete

def comp {Ctrl : Type} (B A : BD Ctrl) : BD Ctrl

def comp {Ctrl : Type} (B A : BD Ctrl) :
  BD Ctrl

**The composite `B ∘ A`, on data.**

theoremdefined in BigraphSim/Comp.lean

complete

theorem comp_sound {Ctrl : Type} {B A : BD Ctrl} {S : Sig Ctrl} {I J K : Face}
  (hA : A.check S = true) (hB : B.check S = true) (hfA : A.Fits I J)
  (hfB : B.Fits J K) (hC : (B.comp A).check S = true) :
  ⟦B⟧ ◦ BigH.tr (rot B.n A.n) ⟦A⟧ ≃ ⟦B.comp A⟧

theorem comp_sound {Ctrl : Type} {B A : BD Ctrl}
  {S : Sig Ctrl} {I J K : Face}
  (hA : A.check S = true)
  (hB : B.check S = true)
  (hfA : A.Fits I J) (hfB : B.Fits J K)
  (hC : (B.comp A).check S = true) :
  ⟦B⟧ ◦ BigH.tr (rot B.n A.n) ⟦A⟧ ≃
    ⟦B.comp A⟧

**(S1c) Composition on data is the library's composition.**  For checked
descriptions `A : I → J` and `B : J → K` whose composite passes the check,
the bigraph built from `B.comp A` is `B ∘ (π • A)` in ´BIG_h, `π` the
rotation moving `A`'s support past `B`'s.

Theorem6.1.4

uses 1used by 1✓L∃∀N

Instantiation on data, \bar\eta_{\mathrm d}(d), is the library's instantiation \bar\eta up to a checked renumbering. For d checked, discrete on data and fitting \varepsilon \to \langle m, Y \rangle, a list \eta with entries below m, the computed renumbering \tau passing its bijection check, and \bar\eta_{\mathrm d}(d) checked,

\llbracket \bar\eta_{\mathrm d}(d) \rrbracket \;=\; \tau \bullet \bar\eta(\llbracket d \rrbracket) .

Rests on NEW: BD.Fits, Item, Par, Perm; not audited: BD.cpyN, BD.etaFin, BD.kept, BD.n, BigH.tr.

Lean code for Theorem6.1.4●2 declarations

defdefined in BigraphSim/Inst.lean

complete

def inst {Ctrl : Type} (d : BD Ctrl) (eta : List Nat) : BD Ctrl

def inst {Ctrl : Type} (d : BD Ctrl)
  (eta : List Nat) : BD Ctrl

**`η̄(d)` on data.**

theoremdefined in BigraphSim/Inst.lean

complete

theorem inst_sound {Ctrl : Type} {d : BD Ctrl} {S : Sig Ctrl} {m : Nat}
  {Y : NSet} (hd : d.check S = true)
  (hf : d.Fits Face.origin { width := m, names := Y }) {eta : List Nat}
  (heta : ∀ (x : Nat), x ∈ eta → x < m)
  (hτ : (d.instRen eta).check (d.instBound eta) = true)
  (hdisc : d.discrete = true) (hI : (d.inst eta).check S = true) :
  ⟦d.inst eta⟧ =
    BigH.tr ((d.instRen eta).perm (d.instBound eta) hτ)
      (BigH.inst (BD.etaFin eta heta) ⟦d⟧)

theorem inst_sound {Ctrl : Type} {d : BD Ctrl}
  {S : Sig Ctrl} {m : Nat} {Y : NSet}
  (hd : d.check S = true)
  (hf :
    d.Fits Face.origin
      { width := m, names := Y })
  {eta : List Nat}
  (heta : ∀ (x : Nat), x ∈ eta → x < m)
  (hτ :
    (d.instRen eta).check
        (d.instBound eta) =
      true)
  (hdisc : d.discrete = true)
  (hI : (d.inst eta).check S = true) :
  ⟦d.inst eta⟧ =
    BigH.tr
      ((d.instRen eta).perm
        (d.instBound eta) hτ)
      (BigH.inst (BD.etaFin eta heta) ⟦d⟧)

**(S2c) Instantiation on data is the library's instantiation**, up to the
checked renumbering `instRen`: for a discrete parameter `d : ε → ⟨m, Y⟩`
and any `η`, the bigraph built from `d.inst eta` is `π • η̄(d)`.