3.1. The algebra🔗

Definition3.1.1

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 3.1.2

Loading preview

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

✓L∃∀N

Tagsfrom sourcebridgedunbridged

A bigraph G : I \to J from inner face I to outer face J is a place graph (a forest of nodes, roots and sites) and a link graph (a hypergraph of ports, edges and names) on the same nodes. Composition H \circ G and tensor G \otimes H (on faces with disjoint names) act on both. Two bigraphs are support equivalent, G \bumpeq H, when they differ only by a renaming of nodes and edges.

Class: Bg, Bg.comp, Bg.tensor FROM SOURCE; Bg.SupportEquiv BRIDGED and UNBRIDGED.

Lean code for Definition3.1.1●4 definitions

structure(9 fields)defined in Bigraph/Basic.lean

complete

structure Bg {Ctrl Name : Type} (S : Sig Ctrl) (I J : Iface Name) : Type 1

structure Bg {Ctrl Name : Type} (S : Sig Ctrl)
  (I J : Iface Name) : Type 1

A concrete pure bigraph `G : I → J` (Def 6.2).

The node set and control map are shared between the two constituents by
construction, discharging §6's combination condition definitionally.

Fields

V : Type

E : Type

finV : Finite self.V

finE : Finite self.E

ctrl : self.V → Ctrl

prnt : Place I.width self.V → Parent self.V J.width

link : I.names.Elt ⊕ Port S self.V self.ctrl → self.E ⊕ J.names.Elt

acyclic : ∀ (v : self.V), Acc (Above self.prnt) v

atomic_childless : ∀ (v : self.V) (w : Place I.width self.V), self.prnt w = Sum.inl v → S.atomic (self.ctrl v) = false

defdefined in Bigraph/Spm.lean

complete

def comp {Ctrl Name : Type} {S : Sig Ctrl} {I J K : Iface Name}
  (H : Bg S J K) (G : Bg S I J) : Bg S I K

def comp {Ctrl Name : Type} {S : Sig Ctrl}
  {I J K : Iface Name} (H : Bg S J K)
  (G : Bg S I J) : Bg S I K

`H ◦ G` (Def 9.1).

defdefined in Bigraph/Tensor.lean

complete

def tensor {Ctrl Name : Type} {S : Sig Ctrl} [DecidableEq Name]
  {I₀ J₀ I₁ J₁ : Iface Name} (G₀ : Bg S I₀ J₀) (G₁ : Bg S I₁ J₁)
  (hI : I₀.names.Disjoint I₁.names) (hJ : J₀.names.Disjoint J₁.names) :
  Bg S (I₀ ⊗ᵢ I₁) (J₀ ⊗ᵢ J₁)

def tensor {Ctrl Name : Type} {S : Sig Ctrl}
  [DecidableEq Name]
  {I₀ J₀ I₁ J₁ : Iface Name}
  (G₀ : Bg S I₀ J₀) (G₁ : Bg S I₁ J₁)
  (hI : I₀.names.Disjoint I₁.names)
  (hJ : J₀.names.Disjoint J₁.names) :
  Bg S (I₀ ⊗ᵢ I₁) (J₀ ⊗ᵢ J₁)

`G₀⊗G₁ ≝ ⟨G₀ᴾ⊗G₁ᴾ, G₀ᴸ⊗G₁ᴸ⟩ : I₀⊗I₁ → J₀⊗J₁` (Def 9.3) — the two
constituents tensored, sharing the node set as §6 requires.

structure(11 fields)defined in Bigraph/Spm.lean

complete

structure SupportEquiv {Ctrl Name : Type} {S : Sig Ctrl} {I J : Iface Name}
  (G H : Bg S I J) : Type

structure SupportEquiv {Ctrl Name : Type}
  {S : Sig Ctrl} {I J : Iface Name}
  (G H : Bg S I J) : Type

**Support equivalence, `G ≏ H`** — TR-580 Def 9.12, BiCoq §4.1.

Bijections of the node set AND the edge set — TR-580 gives identity to
links as well as nodes (TR-580 footnote 5 to §8) — commuting with the
control map, the parent map and the link map.  Ten conditions, which
is what BiCoq reports.

Fields

nodeTo : G.V → H.V

nodeFrom : H.V → G.V

edgeTo : G.E → H.E

edgeFrom : H.E → G.E

node_left : ∀ (v : G.V), self.nodeFrom (self.nodeTo v) = v

node_right : ∀ (v : H.V), self.nodeTo (self.nodeFrom v) = v

edge_left : ∀ (e : G.E), self.edgeFrom (self.edgeTo e) = e

edge_right : ∀ (e : H.E), self.edgeTo (self.edgeFrom e) = e

ctrl_eq : ∀ (v : G.V), H.ctrl (self.nodeTo v) = G.ctrl v

prnt_eq : ∀ (w : Place I.width G.V), H.prnt (PlaceGraph.mapPlace self.nodeTo w) = PlaceGraph.mapParent self.nodeTo (G.prnt w)

link_eq : ∀ (p : I.names.Elt ⊕ Port S G.V G.ctrl) (q : I.names.Elt ⊕ Port S H.V H.ctrl),
  Bg.SamePoint self.nodeTo p q → H.link q = Bg.mapLink self.edgeTo (G.link p)

**The link map is constrained too.**  Without this the relation says
nothing about the link graph, and a "support equivalence" that
ignores half the bigraph is not one.

Theorem3.1.2

uses 1used by 0✓L∃∀N

Bigraphs form a category up to support equivalence: for f : I \to J, g : J \to K, h : K \to L,

h \circ (g \circ f) \;\bumpeq\; (h \circ g) \circ f, \qquad \mathrm{id}_J \circ f \;\bumpeq\; f \;\bumpeq\; f \circ \mathrm{id}_I .

Rests on UNBRIDGED: Bg.SupportEquiv.

Lean code for Theorem3.1.2●3 definitions

defdefined in Bigraph/Spm.lean

complete

def assoc {Ctrl Name : Type} {S : Sig Ctrl} {I J K L : Iface Name}
  (h : Bg S K L) (g : Bg S J K) (f : Bg S I J) : h ◦ g ◦ f ≏ (h ◦ g) ◦ f

def assoc {Ctrl Name : Type} {S : Sig Ctrl}
  {I J K L : Iface Name} (h : Bg S K L)
  (g : Bg S J K) (f : Bg S I J) :
  h ◦ g ◦ f ≏ (h ◦ g) ◦ f

**(C2)** — associativity of composition.

defdefined in Bigraph/Spm.lean

complete

def idComp {Ctrl Name : Type} {S : Sig Ctrl} {I J : Iface Name}
  (f : Bg S I J) : 𝟙 J ◦ f ≏ f

def idComp {Ctrl Name : Type} {S : Sig Ctrl}
  {I J : Iface Name} (f : Bg S I J) :
  𝟙 J ◦ f ≏ f

**(C3)** — the identity is neutral on the left.

defdefined in Bigraph/Spm.lean

complete

def compId {Ctrl Name : Type} {S : Sig Ctrl} {I J : Iface Name}
  (f : Bg S I J) : f ◦ 𝟙 I ≏ f

def compId {Ctrl Name : Type} {S : Sig Ctrl}
  {I J : Iface Name} (f : Bg S I J) :
  f ◦ 𝟙 I ≏ f

**(C3)** — and on the right.

Theorem3.1.3

uses 1used by 0✓L∃∀N

Tensor and composition interchange: when the faces of the two columns have disjoint names,

(B_0 \circ A_0) \otimes (B_1 \circ A_1) \;\bumpeq\; (B_0 \otimes B_1) \circ (A_0 \otimes A_1) .

Rests on UNBRIDGED: Bg.SupportEquiv; not audited: NameSet.Disjoint.

Lean code for Theorem3.1.3●1 definition

defdefined in Bigraph/Spm.lean

complete

def tensorCompInterchange {Ctrl Name : Type} {S : Sig Ctrl}
  [DecidableEq Name] {I₀ J₀ K₀ I₁ J₁ K₁ : Iface Name} (B₀ : Bg S J₀ K₀)
  (A₀ : Bg S I₀ J₀) (B₁ : Bg S J₁ K₁) (A₁ : Bg S I₁ J₁)
  (hI : I₀.names.Disjoint I₁.names) (hJ : J₀.names.Disjoint J₁.names)
  (hK : K₀.names.Disjoint K₁.names) :
  B₀ ◦ A₀ ⊗ B₁ ◦ A₁ ≏ (B₀ ⊗ B₁) ◦ (A₀ ⊗ A₁)

def tensorCompInterchange {Ctrl Name : Type}
  {S : Sig Ctrl} [DecidableEq Name]
  {I₀ J₀ K₀ I₁ J₁ K₁ : Iface Name}
  (B₀ : Bg S J₀ K₀) (A₀ : Bg S I₀ J₀)
  (B₁ : Bg S J₁ K₁) (A₁ : Bg S I₁ J₁)
  (hI : I₀.names.Disjoint I₁.names)
  (hJ : J₀.names.Disjoint J₁.names)
  (hK : K₀.names.Disjoint K₁.names) :
  B₀ ◦ A₀ ⊗ B₁ ◦ A₁ ≏
    (B₀ ⊗ B₁) ◦ (A₀ ⊗ A₁)

**(M3) — the tensor is a bifunctor**, on bigraphs:
`(B₀ ◦ A₀) ⊗ (B₁ ◦ A₁) ≏ (B₀ ⊗ B₁) ◦ (A₀ ⊗ A₁)`.

The place half is `PlaceGraph.tensor_comp_interchange`.  The link half
follows a point through both sides: an inner name, or a port of an
`A`, links through `A` and, if it reaches an outer name of `A`, on
through the `B` beside it; a port of a `B` links through that `B`
alone.  The node and edge maps are the same middle-four interchange.

Theorem3.1.4

uses 1used by 0✓L∃∀N

The symmetries are involutive and natural: for f : I_0 \to I_1 and g : J_0 \to J_1,

\gamma_{J,I} \circ \gamma_{I,J} \;\bumpeq\; \mathrm{id}_{I \otimes J}, \qquad \gamma_{I_1,J_1} \circ (f \otimes g) \;\bumpeq\; (g \otimes f) \circ \gamma_{I_0,J_0} .

Rests on UNBRIDGED: Bg.SupportEquiv; not audited: NameSet.Disjoint.

Lean code for Theorem3.1.4●2 definitions

defdefined in Bigraph/Spm.lean

complete

def symmetry_symmetry {Ctrl Name : Type} {S : Sig Ctrl} [DecidableEq Name]
  (I J : Iface Name) (hIJ : I.names.Disjoint J.names)
  (hJI : J.names.Disjoint I.names) : γ J I ◦ γ I J ≏ 𝟙 (I ⊗ᵢ J)

def symmetry_symmetry {Ctrl Name : Type}
  {S : Sig Ctrl} [DecidableEq Name]
  (I J : Iface Name)
  (hIJ : I.names.Disjoint J.names)
  (hJI : J.names.Disjoint I.names) :
  γ J I ◦ γ I J ≏ 𝟙 (I ⊗ᵢ J)

**(S2)** — `γ_{J,I} ◦ γ_{I,J} = id_{I⊗J}`.

No interface isomorphism is needed here: both sides live at
`I⊗J → I⊗J` already.  (S1) and (S4) are not so lucky.

defdefined in Bigraph/Spm.lean

complete

def symmetryNatural {Ctrl Name : Type} {S : Sig Ctrl} [DecidableEq Name]
  {I₀ I₁ J₀ J₁ : Iface Name} (f : Bg S I₀ I₁) (g : Bg S J₀ J₁)
  (hI : I₀.names.Disjoint J₀.names) (hI' : J₀.names.Disjoint I₀.names)
  (hJ : I₁.names.Disjoint J₁.names) (hJ' : J₁.names.Disjoint I₁.names) :
  γ I₁ J₁ ◦ (f ⊗ g) ≏ (g ⊗ f) ◦ γ I₀ J₀

def symmetryNatural {Ctrl Name : Type}
  {S : Sig Ctrl} [DecidableEq Name]
  {I₀ I₁ J₀ J₁ : Iface Name}
  (f : Bg S I₀ I₁) (g : Bg S J₀ J₁)
  (hI : I₀.names.Disjoint J₀.names)
  (hI' : J₀.names.Disjoint I₀.names)
  (hJ : I₁.names.Disjoint J₁.names)
  (hJ' : J₁.names.Disjoint I₁.names) :
  γ I₁ J₁ ◦ (f ⊗ g) ≏ (g ⊗ f) ◦ γ I₀ J₀

**(S3)** — `γ_{I₁,J₁} ◦ (f⊗g) ≏ (g⊗f) ◦ γ_{I₀,J₀}`.

The one spm axiom whose two sides already live at the SAME interfaces,
so it is a plain `≏` with no interface isomorphism in sight — which is
itself informative: what forced `SupportEquivI` on (M1), (M2) and (S1)
was arithmetic on interfaces, not anything about symmetry.

Both sides reduce to the same two facts, one per layer: the tensor is
natural in the swap (`tensorPrnt_swap`, `tensorLink_swap_name`), and
lifting a factor's result through `γ` is the same as swapping it.

Theorem3.1.5

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.2.1

Loading preview

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

✓L∃∀N

Abstract bigraphs are classes under lean-support equivalence \Bumpeq (support equivalence after discarding idle edges, here across faces with the same widths and the same names as sets), and composition is well defined on them:

G \Bumpeq G' \;\wedge\; H \Bumpeq H' \;\Longrightarrow\; H \circ G \;\Bumpeq\; H' \circ G' .

Rests on NEW: Bg.LeanSetEquiv.

Lean code for Theorem3.1.5●1 theorem

theoremdefined in Bigraph/Abstract.lean

complete

theorem leanComp_congr {Ctrl Name : Type} {S : Sig Ctrl} [DecidableEq Name]
  {I J K I' J' K' : Iface Name} {G : Bg S I J} {H : Bg S J K}
  {G' : Bg S I' J'} {H' : Bg S J' K'}
  (hG :
    Bg.LeanSetEquiv { inner := I, outer := J, bg := G }
      { inner := I', outer := J', bg := G' })
  (hH :
    Bg.LeanSetEquiv { inner := J, outer := K, bg := H }
      { inner := J', outer := K', bg := H' }) :
  Bg.LeanSetEquiv { inner := I, outer := K, bg := H ◦ G }
    { inner := I', outer := K', bg := H' ◦ G' }

theorem leanComp_congr {Ctrl Name : Type}
  {S : Sig Ctrl} [DecidableEq Name]
  {I J K I' J' K' : Iface Name}
  {G : Bg S I J} {H : Bg S J K}
  {G' : Bg S I' J'} {H' : Bg S J' K'}
  (hG :
    Bg.LeanSetEquiv
      { inner := I, outer := J, bg := G }
      { inner := I', outer := J',
        bg := G' })
  (hH :
    Bg.LeanSetEquiv
      { inner := J, outer := K, bg := H }
      { inner := J', outer := K',
        bg := H' }) :
  Bg.LeanSetEquiv
    { inner := I, outer := K,
      bg := H ◦ G }
    { inner := I', outer := K',
      bg := H' ◦ G' }

**≎ is a congruence for composition.**  Lean each composite, lean its
factors first (`leanComp`), compose the equivalences of the leaned
factors (`compCongrI`), lean again (`leanCongrI`).