9.3. The place layer and terms🔗

Definition9.3.1

Statement uses 2

Statement dependency previews

Preview

Definition 9.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 9.3.2

Loading preview

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

✓L∃∀N

Tagsunbridgednew

The place layer adds to the types a former \mathrm{ctrl}_k\, a, a node of control k with interior a, and to the morphisms its functorial action and an inward strength a \otimes \mathrm{ctrl}_k\, b \to \mathrm{ctrl}_k(a \otimes b); there is no outward map. Derivable equality f \equiv_{\mathrm{B}} g is that of the core together with functoriality of each control. A frame now carries a type of regions for each control and an arbitrary lax monad T on types (a functor with unit, multiplication and strength satisfying the monad and strength laws, without naturality of the unit and multiplication; every strong monad on types is one), with \llbracket \bigcirc a \rrbracket = T \llbracket a \rrbracket and \llbracket \mathrm{ctrl}_k\, a \rrbracket = \mathrm{Region}_k \times \llbracket a \rrbracket; from here on \llbracket f \rrbracket_{\mathcal{I}} is this layer's evaluation.

Class: BTy UNBRIDGED; BMor, BMEq, BFrame, beval NEW.

Lean code for Definition9.3.1●5 definitions

inductive(5 constructors, 2 parameters)defined in Locus/Bigraph.lean

complete

inductive BTy (C B : Type) : Type

inductive BTy (C B : Type) : Type

Three layers in one type former set: `circ` is the MODALITY (type
layer), `ctrl k` is a PLACE node (place layer), and tensor/base carry
the link layer as before.

Constructors

base {C B : Type} : B → BTy C B

unit {C B : Type} : BTy C B

tensor {C B : Type} : BTy C B → BTy C B → BTy C B

circ {C B : Type} : BTy C B → BTy C B

ctrl {C B : Type} : C → BTy C B → BTy C B

inductive(19 constructors, 5 parameters)defined in Locus/Bigraph.lean

complete

inductive BMor {C B : Type} (S : BSig C B) : BTy C B → BTy C B → Type

inductive BMor {C B : Type} (S : BSig C B) :
  BTy C B → BTy C B → Type

Constructors

box {C B : Type} {S : BSig C B} {a b : BTy C B} :
  S.Box a b → BMor S a b

id {C B : Type} {S : BSig C B} (a : BTy C B) : BMor S a a

comp {C B : Type} {S : BSig C B} {a b c : BTy C B} :
  BMor S a b → BMor S b c → BMor S a c

tens {C B : Type} {S : BSig C B} {a b c d : BTy C B} :
  BMor S a b → BMor S c d → BMor S (a ⊗ᵦ c) (b ⊗ᵦ d)

swap {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMor S (a ⊗ᵦ b) (b ⊗ᵦ a)

assoc {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMor S ((a ⊗ᵦ b) ⊗ᵦ c) (a ⊗ᵦ b ⊗ᵦ c)

assoc' {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMor S (a ⊗ᵦ b ⊗ᵦ c) ((a ⊗ᵦ b) ⊗ᵦ c)

lunit {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S (BTy.unit ⊗ᵦ a) a

lunit' {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S a (BTy.unit ⊗ᵦ a)

runit {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S (a ⊗ᵦ BTy.unit) a

runit' {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S a (a ⊗ᵦ BTy.unit)

eta {C B : Type} {S : BSig C B} (a : BTy C B) : BMor S a ◯ᵦa

mu {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S ◯ᵦ◯ᵦa ◯ᵦa

cmap {C B : Type} {S : BSig C B} {a b : BTy C B} :
  BMor S a b → BMor S ◯ᵦa ◯ᵦb

str {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMor S (a ⊗ᵦ ◯ᵦb) ◯ᵦ(a ⊗ᵦ b)

copy {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S a (a ⊗ᵦ a)

del {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMor S a BTy.unit

cmapC {C B : Type} {S : BSig C B} (k : C) {a b : BTy C B} :
  BMor S a b → BMor S (BTy.ctrl k a) (BTy.ctrl k b)

strC {C B : Type} {S : BSig C B} (k : C) (a b : BTy C B) :
  BMor S (a ⊗ᵦ BTy.ctrl k b) (BTy.ctrl k (a ⊗ᵦ b))

inductive(46 constructors, Prop, 7 parameters)defined in Locus/Bigraph.lean

complete

inductive BMEq {C B : Type} {S : BSig C B} {a b : BTy C B} :
  BMor S a b → BMor S a b → Prop

inductive BMEq {C B : Type} {S : BSig C B}
  {a b : BTy C B} :
  BMor S a b → BMor S a b → Prop

The equational theory: every law of `MEq`, transcribed to `BMor`, plus
the three that govern a control.

NOT STATED, deliberately and in the same spirit as `Locus/Core.lean`:
any law relating `strC` to the rest.  A control admits links inward
(`no_discharge_without_costrength` shows that is safe) but what that
admission must satisfy is the next question, not this one.

Constructors

interchange {C B : Type} {S : BSig C B}
  {a b c d e f' : BTy C B} (p : BMor S a b) (q : BMor S b c)
  (r : BMor S d e) (s : BMor S e f') :
  BMEq ((p.comp q).tens (r.comp s))
    ((p.tens r).comp (q.tens s))

swapswap {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq ((BMor.swap a b).comp (BMor.swap b a))
    (BMor.id (a ⊗ᵦ b))

idl {C B : Type} {S : BSig C B} {a b : BTy C B}
  (f : BMor S a b) : BMEq ((BMor.id a).comp f) f

idr {C B : Type} {S : BSig C B} {a b : BTy C B}
  (f : BMor S a b) : BMEq (f.comp (BMor.id b)) f

compAssoc {C B : Type} {S : BSig C B} {a b c d : BTy C B}
  (f : BMor S a b) (g : BMor S b c) (h : BMor S c d) :
  BMEq ((f.comp g).comp h) (f.comp (g.comp h))

tensId {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq ((BMor.id a).tens (BMor.id b)) (BMor.id (a ⊗ᵦ b))

swapNat {C B : Type} {S : BSig C B} {a b c d : BTy C B}
  (f : BMor S a b) (g : BMor S c d) :
  BMEq ((f.tens g).comp (BMor.swap b d))
    ((BMor.swap a c).comp (g.tens f))

assocIso {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMEq ((BMor.assoc a b c).comp (BMor.assoc' a b c))
    (BMor.id ((a ⊗ᵦ b) ⊗ᵦ c))

assocIso' {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMEq ((BMor.assoc' a b c).comp (BMor.assoc a b c))
    (BMor.id (a ⊗ᵦ b ⊗ᵦ c))

lunitIso {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.lunit a).comp (BMor.lunit' a))
    (BMor.id (BTy.unit ⊗ᵦ a))

lunitIso' {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.lunit' a).comp (BMor.lunit a)) (BMor.id a)

runitIso {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.runit a).comp (BMor.runit' a))
    (BMor.id (a ⊗ᵦ BTy.unit))

runitIso' {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.runit' a).comp (BMor.runit a)) (BMor.id a)

pentagon {C B : Type} {S : BSig C B} (a b c d : BTy C B) :
  BMEq
    ((BMor.assoc (a ⊗ᵦ b) c d).comp
      (BMor.assoc a b (c ⊗ᵦ d)))
    ((((BMor.assoc a b c).tens (BMor.id d)).comp
          (BMor.assoc a (b ⊗ᵦ c) d)).comp
      ((BMor.id a).tens (BMor.assoc b c d)))

triangle {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq
    ((BMor.assoc a BTy.unit b).comp
      ((BMor.id a).tens (BMor.lunit b)))
    ((BMor.runit a).tens (BMor.id b))

cmapId {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq (BMor.id a).cmap (BMor.id ◯ᵦa)

cmapComp {C B : Type} {S : BSig C B} {a b c : BTy C B}
  (f : BMor S a b) (g : BMor S b c) :
  BMEq (f.comp g).cmap (f.cmap.comp g.cmap)

muEtaL {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.eta ◯ᵦa).comp (BMor.mu a)) (BMor.id ◯ᵦa)

muEtaR {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.eta a).cmap.comp (BMor.mu a)) (BMor.id ◯ᵦa)

muAssoc {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.mu ◯ᵦa).comp (BMor.mu a))
    ((BMor.mu a).cmap.comp (BMor.mu a))

hexagon {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMEq
    ((BMor.assoc a b c).comp
      ((BMor.swap a (b ⊗ᵦ c)).comp (BMor.assoc b c a)))
    (((BMor.swap a b).tens (BMor.id c)).comp
      ((BMor.assoc b a c).comp
        ((BMor.id b).tens (BMor.swap a c))))

assocNat {C B : Type} {S : BSig C B}
  {a a' b b' c c' : BTy C B} (f : BMor S a a')
  (g : BMor S b b') (h : BMor S c c') :
  BMEq (((f.tens g).tens h).comp (BMor.assoc a' b' c'))
    ((BMor.assoc a b c).comp (f.tens (g.tens h)))

lunitNat {C B : Type} {S : BSig C B} {a b : BTy C B}
  (f : BMor S a b) :
  BMEq (((BMor.id BTy.unit).tens f).comp (BMor.lunit b))
    ((BMor.lunit a).comp f)

runitNat {C B : Type} {S : BSig C B} {a b : BTy C B}
  (f : BMor S a b) :
  BMEq ((f.tens (BMor.id BTy.unit)).comp (BMor.runit b))
    ((BMor.runit a).comp f)

strNat {C B : Type} {S : BSig C B} {a a' b b' : BTy C B}
  (f : BMor S a a') (g : BMor S b b') :
  BMEq ((f.tens g.cmap).comp (BMor.str a' b'))
    ((BMor.str a b).comp (f.tens g).cmap)

strUnit {C B : Type} {S : BSig C B} (b : BTy C B) :
  BMEq ((BMor.str BTy.unit b).comp (BMor.lunit b).cmap)
    (BMor.lunit ◯ᵦb)

strAssoc {C B : Type} {S : BSig C B} (a b c : BTy C B) :
  BMEq
    ((BMor.assoc a b ◯ᵦc).comp
      (((BMor.id a).tens (BMor.str b c)).comp
        (BMor.str a (b ⊗ᵦ c))))
    ((BMor.str (a ⊗ᵦ b) c).comp (BMor.assoc a b c).cmap)

strEta {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq (((BMor.id a).tens (BMor.eta b)).comp (BMor.str a b))
    (BMor.eta (a ⊗ᵦ b))

strMu {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq (((BMor.id a).tens (BMor.mu b)).comp (BMor.str a b))
    ((BMor.str a ◯ᵦb).comp
      ((BMor.str a b).cmap.comp (BMor.mu (a ⊗ᵦ b))))

copyDelL {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq
    ((BMor.copy a).comp
      (((BMor.del a).tens (BMor.id a)).comp (BMor.lunit a)))
    (BMor.id a)

copyDelR {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq
    ((BMor.copy a).comp
      (((BMor.id a).tens (BMor.del a)).comp (BMor.runit a)))
    (BMor.id a)

copyAssoc {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq
    ((BMor.copy a).comp
      (((BMor.copy a).tens (BMor.id a)).comp
        (BMor.assoc a a a)))
    ((BMor.copy a).comp ((BMor.id a).tens (BMor.copy a)))

copyComm {C B : Type} {S : BSig C B} (a : BTy C B) :
  BMEq ((BMor.copy a).comp (BMor.swap a a)) (BMor.copy a)

copyTens {C B : Type} {S : BSig C B} (a b : BTy C B)
  {m : BMor S ((a ⊗ᵦ a) ⊗ᵦ b ⊗ᵦ b) ((a ⊗ᵦ b) ⊗ᵦ a ⊗ᵦ b)}
  (hm : m = bmix a a b b) :
  BMEq (BMor.copy (a ⊗ᵦ b))
    (((BMor.copy a).tens (BMor.copy b)).comp m)

delTens {C B : Type} {S : BSig C B} (a b : BTy C B) :
  BMEq (BMor.del (a ⊗ᵦ b))
    (((BMor.del a).tens (BMor.del b)).comp
      (BMor.lunit BTy.unit))

copyUnit {C B : Type} {S : BSig C B} :
  BMEq (BMor.copy BTy.unit) (BMor.lunit' BTy.unit)

delUnit {C B : Type} {S : BSig C B} :
  BMEq (BMor.del BTy.unit) (BMor.id BTy.unit)

refl {C B : Type} {S : BSig C B} {a b : BTy C B}
  (f : BMor S a b) : BMEq f f

symm {C B : Type} {S : BSig C B} {a b : BTy C B}
  {f g : BMor S a b} : BMEq f g → BMEq g f

trans {C B : Type} {S : BSig C B} {a b : BTy C B}
  {f g h : BMor S a b} : BMEq f g → BMEq g h → BMEq f h

congComp {C B : Type} {S : BSig C B} {a b c : BTy C B}
  {f f' : BMor S a b} {g g' : BMor S b c} :
  BMEq f f' → BMEq g g' → BMEq (f.comp g) (f'.comp g')

congTens {C B : Type} {S : BSig C B} {a b c d : BTy C B}
  {f f' : BMor S a b} {g g' : BMor S c d} :
  BMEq f f' → BMEq g g' → BMEq (f.tens g) (f'.tens g')

congCmap {C B : Type} {S : BSig C B} {a b : BTy C B}
  {f f' : BMor S a b} : BMEq f f' → BMEq f.cmap f'.cmap

cmapCId {C B : Type} {S : BSig C B} (k : C) (a : BTy C B) :
  BMEq (BMor.cmapC k (BMor.id a)) (BMor.id (BTy.ctrl k a))

cmapCComp {C B : Type} {S : BSig C B} (k : C)
  {a b c : BTy C B} (f : BMor S a b) (g : BMor S b c) :
  BMEq (BMor.cmapC k (f.comp g))
    ((BMor.cmapC k f).comp (BMor.cmapC k g))

congCmapC {C B : Type} {S : BSig C B} (k : C)
  {a b : BTy C B} {f f' : BMor S a b} :
  BMEq f f' → BMEq (BMor.cmapC k f) (BMor.cmapC k f')

structure(3 fields)defined in Locus/BigraphModel.lean

complete

structure BFrame (C B : Type) : Type 1

structure BFrame (C B : Type) : Type 1

A frame for the three-layer calculus: a carrier for each base type, a
carrier for each control, and — the parameter this structure exists to
carry — WHICH MONAD `◯` is.

It used to be a monoid, and `◯` was the writer built from it.  That
made every model of the calculus a writer model.  `Locus/Monad.lean`
has seven readings; `writerFrame` below recovers the old one.

Fields

base : B → Type

region : C → Type

mon : LaxMonad

defdefined in Locus/BigraphModel.lean

complete

def beval {C B : Type} {S : BSig C B} {M : BFrame C B} (I : BInterp S M)
  {a b : BTy C B} : BMor S a b → bden M a → bden M b

def beval {C B : Type} {S : BSig C B}
  {M : BFrame C B} (I : BInterp S M)
  {a b : BTy C B} :
  BMor S a b → bden M a → bden M b

Theorem9.3.2

uses 1used by 1✓L∃∀N

The place layer is sound in every frame, for every such T, and every interpretation:

f \equiv_{\mathrm{B}} g \;\Longrightarrow\; \llbracket f \rrbracket_{\mathcal{I}} = \llbracket g \rrbracket_{\mathcal{I}} .

Rests on UNBRIDGED: BTy; NEW: BFrame, BInterp, BMEq, BMor, BSig, bden, beval.

Lean code for Theorem9.3.2●1 theorem

theoremdefined in Locus/BigraphModel.lean

complete

theorem soundB {C B : Type} {S : BSig C B} {M : BFrame C B} (I : BInterp S M)
  {a b : BTy C B} {f g : BMor S a b} (h : BMEq f g) :
  beval I f = beval I g

theorem soundB {C B : Type} {S : BSig C B}
  {M : BFrame C B} (I : BInterp S M)
  {a b : BTy C B} {f g : BMor S a b}
  (h : BMEq f g) : beval I f = beval I g

**Soundness for the three-layer calculus.**  All forty-six `BMEq`
constructors hold in the model, the three place-layer rules included.

This is step 1 of `docs/bigraph-integration.md`: the place layer now has
equational content and that content is consistent.

Definition9.3.3

uses 1used by 1✓L∃∀N

Tagsfrom sourcenew

Terms \Gamma \vdash t : a have typed variables, the unit value, pairs and projections, let, the unit of the modality, Moggi's computational let (the only way to open a \bigcirc), applied boxes, and a binder for working inside a control. Compilation sends t to a morphism \mathrm{compile}(t) : \bigotimes \Gamma \to a, where \bigotimes \Gamma = a_1 \otimes (\cdots \otimes I): a variable is a projection built from discard and the unitors, and the context is copied where two subterms share it. The interpreter \mathrm{evalTm}_{\mathcal{I}}(t, \gamma) evaluates t directly in an environment \gamma for \Gamma.

Class: Tm, compile FROM SOURCE; evalTm NEW.

Lean code for Definition9.3.3●3 definitions

inductive(10 constructors, 5 parameters)defined in Locus/Term.lean

complete

inductive Tm {C B : Type} (S : BSig C B) : TCtx C B → BTy C B → Type

inductive Tm {C B : Type} (S : BSig C B) :
  TCtx C B → BTy C B → Type

Constructors

var {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a : BTy C B} : Var Γ a → Tm S Γ a

star {C B : Type} {S : BSig C B} {Γ : TCtx C B} :
  Tm S Γ BTy.unit

pair {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} : Tm S Γ a → Tm S Γ b → Tm S Γ (a ⊗ᵦ b)

fst {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} : Tm S Γ (a ⊗ᵦ b) → Tm S Γ a

snd {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} : Tm S Γ (a ⊗ᵦ b) → Tm S Γ b

letIn {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} : Tm S Γ a → Tm S (a :: Γ) b → Tm S Γ b

`let x = s in t` — cartesian binding.

ret {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a : BTy C B} : Tm S Γ a → Tm S Γ ◯ᵦa

`η` — a value as a trivially-constrained computation.

bind {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} :
  Tm S Γ ◯ᵦa → Tm S (a :: Γ) ◯ᵦb → Tm S Γ ◯ᵦb

`x ⇐ s ; t` — Moggi's computational let.  The only way to open a
`◯`, and it is monad-general by construction.

prim {C B : Type} {S : BSig C B} {Γ : TCtx C B}
  {a b : BTy C B} : S.Box a b → Tm S Γ a → Tm S Γ b

A primitive of the signature, applied.

inCtrl {C B : Type} {S : BSig C B} {Γ : TCtx C B} {k : C}
  {a b : BTy C B} :
  Tm S Γ (BTy.ctrl k a) →
    Tm S (a :: Γ) b → Tm S Γ (BTy.ctrl k b)

Work inside a control node, with the context carried in by `strC`.
There is no rule the other way: a variable bound inside a node does
not escape it.

defdefined in Locus/Term.lean

complete

def compile {C B : Type} {S : BSig C B} {Γ : TCtx C B} {a : BTy C B} :
  Tm S Γ a → BMor S (tyOf Γ) a

def compile {C B : Type} {S : BSig C B}
  {Γ : TCtx C B} {a : BTy C B} :
  Tm S Γ a → BMor S (tyOf Γ) a

defdefined in Locus/Term.lean

complete

def evalTm {C B : Type} {S : BSig C B} {M : BFrame C B} (I : BInterp S M)
  {Γ : TCtx C B} {a : BTy C B} : Tm S Γ a → Env M Γ → bden M a

def evalTm {C B : Type} {S : BSig C B}
  {M : BFrame C B} (I : BInterp S M)
  {Γ : TCtx C B} {a : BTy C B} :
  Tm S Γ a → Env M Γ → bden M a

Theorem9.3.4

Statement uses 2

Statement dependency previews

Preview

Theorem 9.3.2

Loading preview

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

used by 0✓L∃∀N

Compilation agrees with the interpreter in every frame and interpretation: for every term \Gamma \vdash t : a and environment \gamma, with \hat\gamma \in \llbracket \bigotimes \Gamma \rrbracket the tuple of \gamma,

\llbracket \mathrm{compile}(t) \rrbracket_{\mathcal{I}}(\hat\gamma) = \mathrm{evalTm}_{\mathcal{I}}(t, \gamma) .

Rests on UNBRIDGED: BTy; NEW: BFrame, BInterp, BSig, Env, bden, beval, envTup, evalTm.

Lean code for Theorem9.3.4●1 theorem

theoremdefined in Locus/Term.lean

complete

theorem compile_sound {C B : Type} {S : BSig C B} {M : BFrame C B}
  (I : BInterp S M) {Γ : TCtx C B} {a : BTy C B} (t : Tm S Γ a)
  (γ : Env M Γ) : beval I (compile t) (envTup γ) = evalTm I t γ

theorem compile_sound {C B : Type} {S : BSig C B}
  {M : BFrame C B} (I : BInterp S M)
  {Γ : TCtx C B} {a : BTy C B}
  (t : Tm S Γ a) (γ : Env M Γ) :
  beval I (compile t) (envTup γ) =
    evalTm I t γ

**Compilation is sound, for every choice of `◯`.**  The categorical
semantics of the compiled morphism and the direct interpreter agree,
with no hypothesis on the monad beyond the eleven laws.