locus: Blueprint

9.1. Syntax and soundness🔗

Definition9.1.1
uses 0
Used by 5
Reverse dependency previews
Preview
Definition 9.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom source

Types over base types B are built from a unit I, the tensor a \otimes b and the modality \bigcirc a. A morphism f : a \to b over a signature of primitive boxes is a string diagram: built by composition f ; g (in diagrammatic order) and tensor f \otimes g from boxes, identities, symmetries, explicit associators and unitors, the unit \eta, multiplication \mu, functorial action and strength \mathrm{str} : a \otimes \bigcirc b \to \bigcirc(a \otimes b) of the modality, and \mathrm{copy}_a : a \to a \otimes a, \mathrm{del}_a : a \to I; \bigcirc f is the functorial action and \alpha the associator. Derivable equality f \equiv g is the congruence generated by the laws of a symmetric monoidal category; functoriality of \bigcirc, the unit and associativity laws of \eta and \mu, and five laws of the strength (naturality of \eta and \mu is not among them); and the laws of a cocommutative comonoid on every type, uniform in \otimes and I.

Lean code for Definition9.1.1●3 definitions
  • inductive(4 constructors, 1 parameter)defined in Locus/Core.lean
    complete
    inductive Ty (B : Type) : Type
    inductive Ty (B : Type) : Type
    Types.

`tensor` and `unit` give the monoidal structure at the level of types
rather than at the level of objects, which is what lets `circ` apply to
a tensor.  (Listing objects and taking `⊗` to be append would strictify
the monoidal structure and kill the coherence obligations, but then
`◯(A ⊗ B)` is not expressible and the monad's monoidal structure map
has nowhere to live.  Strictification is a decision still to be taken —
see `docs/canonical-form.md`.)

`circ` is the lax modality ◯: *holds up to a constraint left unstated*,
read here as a zoom boundary with the detail suppressed.

    Constructors

    base {B : Type} : B → Ty B
    unit {B : Type} : Ty B
    tensor {B : Type} : Ty B → Ty B → Ty B
    circ {B : Type} : Ty B → Ty B
  • inductive(17 constructors, 4 parameters)defined in Locus/Core.lean
    complete
    inductive Mor {B : Type} (S : Sig B) : Ty B → Ty B → Type
    inductive Mor {B : Type} (S : Sig B) :
  Ty B → Ty B → Type
    Morphisms.  The diagram reading: `comp` is vertical juxtaposition,
`tens` horizontal, `id` a bare wire, `swap` a crossing, and `circ` a
bubble drawn round a sub-diagram whose interior is not shown at this
zoom level.

Associators and unitors are explicit because the structure here is NOT
strict; `Mac Lane` coherence says they may be suppressed, but that is a
theorem to prove, not an assumption to help oneself to.

    Constructors

    box {B : Type} {S : Sig B} {a b : Ty B} :
  S.Box a b → Mor S a b
    id {B : Type} {S : Sig B} (a : Ty B) : Mor S a a
    comp {B : Type} {S : Sig B} {a b c : Ty B} :
  Mor S a b → Mor S b c → Mor S a c
    tens {B : Type} {S : Sig B} {a b c d : Ty B} :
  Mor S a b → Mor S c d → Mor S (a ⊗ c) (b ⊗ d)
    swap {B : Type} {S : Sig B} (a b : Ty B) :
  Mor S (a ⊗ b) (b ⊗ a)
    assoc {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor S ((a ⊗ b) ⊗ c) (a ⊗ b ⊗ c)
    assoc' {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor S (a ⊗ b ⊗ c) ((a ⊗ b) ⊗ c)
    lunit {B : Type} {S : Sig B} (a : Ty B) :
  Mor S (Ty.unit ⊗ a) a
    lunit' {B : Type} {S : Sig B} (a : Ty B) :
  Mor S a (Ty.unit ⊗ a)
    runit {B : Type} {S : Sig B} (a : Ty B) :
  Mor S (a ⊗ Ty.unit) a
    runit' {B : Type} {S : Sig B} (a : Ty B) :
  Mor S a (a ⊗ Ty.unit)
    eta {B : Type} {S : Sig B} (a : Ty B) : Mor S a ◯a
    mu {B : Type} {S : Sig B} (a : Ty B) : Mor S ◯◯a ◯a
    cmap {B : Type} {S : Sig B} {a b : Ty B} :
  Mor S a b → Mor S ◯a ◯b
    str {B : Type} {S : Sig B} (a b : Ty B) :
  Mor S (a ⊗ ◯b) ◯(a ⊗ b)
    copy {B : Type} {S : Sig B} (a : Ty B) : Mor S a (a ⊗ a)
    del {B : Type} {S : Sig B} (a : Ty B) : Mor S a Ty.unit
  • inductive(43 constructors, Prop, 6 parameters)defined in Locus/Core.lean
    complete
    inductive MEq {B : Type} {S : Sig B} {a b : Ty B} : Mor S a b → Mor S a b → Prop
    inductive MEq {B : Type} {S : Sig B} {a b : Ty B} :
  Mor S a b → Mor S a b → Prop
    Equality of morphisms, carried as an inductive relation rather than by
quotienting — the technique proved out in `fairflow/lax-logic-in-lean`,
and the one `docs/canonical-form.md` argues for here.  What is NOT
stated is listed at the foot of this file, so that the denominator
stays visible.

    Constructors

    interchange {B : Type} {S : Sig B} {a b c d e f' : Ty B}
  (p : Mor S a b) (q : Mor S b c) (r : Mor S d e)
  (s : Mor S e f') : p ≫ q ⊗ r ≫ s ≡ (p ⊗ r) ≫ (q ⊗ s)
    Interchange.  THE law of simultaneity: doing `f` then `h` beside
doing `g` then `k` is the same as doing `f` beside `g`, then `h`
beside `k`.  Note it is an EQUATION here, where Concurrent Kleene
Algebra has only an inequation — see `docs/canonical-form.md`. 
    swapswap {B : Type} {S : Sig B} (a b : Ty B) :
  Mor.swap a b ≫ Mor.swap b a ≡ Mor.id (a ⊗ b)
    Symmetry is an involution: two crossings undo each other. 
    idl {B : Type} {S : Sig B} {a b : Ty B} (f : Mor S a b) :
  Mor.id a ≫ f ≡ f
    idr {B : Type} {S : Sig B} {a b : Ty B} (f : Mor S a b) :
  f ≫ Mor.id b ≡ f
    compAssoc {B : Type} {S : Sig B} {a b c d : Ty B}
  (f : Mor S a b) (g : Mor S b c) (h : Mor S c d) :
  f ≫ g ≫ h ≡ f ≫ (g ≫ h)
    tensId {B : Type} {S : Sig B} (a b : Ty B) :
  Mor.id a ⊗ Mor.id b ≡ Mor.id (a ⊗ b)
    swapNat {B : Type} {S : Sig B} {a b c d : Ty B}
  (f : Mor S a b) (g : Mor S c d) :
  (f ⊗ g) ≫ Mor.swap b d ≡ Mor.swap a c ≫ (g ⊗ f)
    The symmetry is natural: sliding a crossing past a pair of morphisms
swaps which side each acts on. 
    assocIso {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor.assoc a b c ≫ Mor.assoc' a b c ≡ Mor.id ((a ⊗ b) ⊗ c)
    assocIso' {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor.assoc' a b c ≫ Mor.assoc a b c ≡ Mor.id (a ⊗ b ⊗ c)
    lunitIso {B : Type} {S : Sig B} (a : Ty B) :
  Mor.lunit a ≫ Mor.lunit' a ≡ Mor.id (Ty.unit ⊗ a)
    lunitIso' {B : Type} {S : Sig B} (a : Ty B) :
  Mor.lunit' a ≫ Mor.lunit a ≡ Mor.id a
    runitIso {B : Type} {S : Sig B} (a : Ty B) :
  Mor.runit a ≫ Mor.runit' a ≡ Mor.id (a ⊗ Ty.unit)
    runitIso' {B : Type} {S : Sig B} (a : Ty B) :
  Mor.runit' a ≫ Mor.runit a ≡ Mor.id a
    pentagon {B : Type} {S : Sig B} (a b c d : Ty B) :
  Mor.assoc (a ⊗ b) c d ≫ Mor.assoc a b (c ⊗ d) ≡
    (Mor.assoc a b c ⊗ Mor.id d) ≫ Mor.assoc a (b ⊗ c) d ≫
      (Mor.id a ⊗ Mor.assoc b c d)
    Mac Lane's pentagon: the two ways of reassociating four objects
agree. 
    triangle {B : Type} {S : Sig B} (a b : Ty B) :
  Mor.assoc a Ty.unit b ≫ (Mor.id a ⊗ Mor.lunit b) ≡
    Mor.runit a ⊗ Mor.id b
    Mac Lane's triangle: the unit is coherent with the associator. 
    cmapId {B : Type} {S : Sig B} (a : Ty B) :
  (Mor.id a).cmap ≡ Mor.id ◯a
    cmapComp {B : Type} {S : Sig B} {a b c : Ty B}
  (f : Mor S a b) (g : Mor S b c) :
  (f ≫ g).cmap ≡ f.cmap ≫ g.cmap
    muEtaL {B : Type} {S : Sig B} (a : Ty B) :
  Mor.eta ◯a ≫ Mor.mu a ≡ Mor.id ◯a
    muEtaR {B : Type} {S : Sig B} (a : Ty B) :
  (Mor.eta a).cmap ≫ Mor.mu a ≡ Mor.id ◯a
    muAssoc {B : Type} {S : Sig B} (a : Ty B) :
  Mor.mu ◯a ≫ Mor.mu a ≡ (Mor.mu a).cmap ≫ Mor.mu a
    hexagon {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor.assoc a b c ≫ (Mor.swap a (b ⊗ c) ≫ Mor.assoc b c a) ≡
    (Mor.swap a b ⊗ Mor.id c) ≫
      (Mor.assoc b a c ≫ (Mor.id b ⊗ Mor.swap a c))
    assocNat {B : Type} {S : Sig B} {a a' b b' c c' : Ty B}
  (f : Mor S a a') (g : Mor S b b') (h : Mor S c c') :
  ((f ⊗ g) ⊗ h) ≫ Mor.assoc a' b' c' ≡
    Mor.assoc a b c ≫ (f ⊗ g ⊗ h)
    lunitNat {B : Type} {S : Sig B} {a b : Ty B}
  (f : Mor S a b) :
  (Mor.id Ty.unit ⊗ f) ≫ Mor.lunit b ≡ Mor.lunit a ≫ f
    runitNat {B : Type} {S : Sig B} {a b : Ty B}
  (f : Mor S a b) :
  (f ⊗ Mor.id Ty.unit) ≫ Mor.runit b ≡ Mor.runit a ≫ f
    strNat {B : Type} {S : Sig B} {a a' b b' : Ty B}
  (f : Mor S a a') (g : Mor S b b') :
  (f ⊗ g.cmap) ≫ Mor.str a' b' ≡ Mor.str a b ≫ (f ⊗ g).cmap
    strUnit {B : Type} {S : Sig B} (b : Ty B) :
  Mor.str Ty.unit b ≫ (Mor.lunit b).cmap ≡ Mor.lunit ◯b
    Strength over the unit is the unitor: nothing to carry, nothing
carried. 
    strAssoc {B : Type} {S : Sig B} (a b c : Ty B) :
  Mor.assoc a b ◯c ≫
      ((Mor.id a ⊗ Mor.str b c) ≫ Mor.str a (b ⊗ c)) ≡
    Mor.str (a ⊗ b) c ≫ (Mor.assoc a b c).cmap
    Strength is compatible with reassociation: absorbing a constraint
into a pair and then regrouping is absorbing it into the regrouped
pair. 
    strEta {B : Type} {S : Sig B} (a b : Ty B) :
  (Mor.id a ⊗ Mor.eta b) ≫ Mor.str a b ≡ Mor.eta (a ⊗ b)
    Strength over a trivially-constrained factor is trivial. 
    strMu {B : Type} {S : Sig B} (a b : Ty B) :
  (Mor.id a ⊗ Mor.mu b) ≫ Mor.str a b ≡
    Mor.str a ◯b ≫ ((Mor.str a b).cmap ≫ Mor.mu (a ⊗ b))
    Strength commutes with collapsing two layers of constraint. 
    copyDelL {B : Type} {S : Sig B} (a : Ty B) :
  Mor.copy a ≫ ((Mor.del a ⊗ Mor.id a) ≫ Mor.lunit a) ≡
    Mor.id a
    copyDelR {B : Type} {S : Sig B} (a : Ty B) :
  Mor.copy a ≫ ((Mor.id a ⊗ Mor.del a) ≫ Mor.runit a) ≡
    Mor.id a
    copyAssoc {B : Type} {S : Sig B} (a : Ty B) :
  Mor.copy a ≫ ((Mor.copy a ⊗ Mor.id a) ≫ Mor.assoc a a a) ≡
    Mor.copy a ≫ (Mor.id a ⊗ Mor.copy a)
    Coassociativity: forking then forking the left prong is forking then
forking the right one, up to reassociation. 
    copyComm {B : Type} {S : Sig B} (a : Ty B) :
  Mor.copy a ≫ Mor.swap a a ≡ Mor.copy a
    Cocommutativity: the two prongs of a fork are interchangeable.  This
is what makes a locus a locus and not a pair of distinct positions —
the second reference to a referent is not a different thing from the
first. 
    copyTens {B : Type} {S : Sig B} (a b : Ty B)
  {m : Mor S ((a ⊗ a) ⊗ b ⊗ b) ((a ⊗ b) ⊗ a ⊗ b)}
  (hm : m = mix a a b b) :
  Mor.copy (a ⊗ b) ≡ (Mor.copy a ⊗ Mor.copy b) ≫ m
    delTens {B : Type} {S : Sig B} (a b : Ty B) :
  Mor.del (a ⊗ b) ≡
    (Mor.del a ⊗ Mor.del b) ≫ Mor.lunit Ty.unit
    copyUnit {B : Type} {S : Sig B} :
  Mor.copy Ty.unit ≡ Mor.lunit' Ty.unit
    delUnit {B : Type} {S : Sig B} :
  Mor.del Ty.unit ≡ Mor.id Ty.unit
    refl {B : Type} {S : Sig B} {a b : Ty B} (f : Mor S a b) :
  f ≡ f
    symm {B : Type} {S : Sig B} {a b : Ty B} {f g : Mor S a b} :
  f ≡ g → g ≡ f
    trans {B : Type} {S : Sig B} {a b : Ty B}
  {f g h : Mor S a b} : f ≡ g → g ≡ h → f ≡ h
    congComp {B : Type} {S : Sig B} {a b c : Ty B}
  {f f' : Mor S a b} {g g' : Mor S b c} :
  f ≡ f' → g ≡ g' → f ≫ g ≡ f' ≫ g'
    congTens {B : Type} {S : Sig B} {a b c d : Ty B}
  {f f' : Mor S a b} {g g' : Mor S c d} :
  f ≡ f' → g ≡ g' → f ⊗ g ≡ f' ⊗ g'
    congCmap {B : Type} {S : Sig B} {a b : Ty B}
  {f f' : Mor S a b} : f ≡ f' → f.cmap ≡ f'.cmap
Definition9.1.2
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 9.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom sourcenew

A frame M gives a type for each base type and a monoid (W, 1, \cdot) of constraints. Types denote types, with \otimes the product, I the one-point type and \llbracket \bigcirc a \rrbracket = W \times \llbracket a \rrbracket (the writer monad). An interpretation \mathcal{I} assigns a function to each box, and \llbracket f \rrbracket_{\mathcal{I}} : \llbracket a \rrbracket \to \llbracket b \rrbracket extends it to all morphisms.

Class: Frame FROM SOURCE; Interp, eval NEW.

Lean code for Definition9.1.2●3 definitions
  • structure(7 fields)defined in Locus/Model.lean
    complete
    structure Frame (B : Type) : Type 1
    structure Frame (B : Type) : Type 1
    A frame: what the base types denote, and the monoid of constraints the
modality accumulates.  The monoid laws are carried because a genuine
writer monad needs them — though, as noted below, neither of the two
theorems here uses them.

    Fields

    base : B → Type
    W : Type
    wone : self.W
    wmul : self.W → self.W → self.W
    wid_l : ∀ (w : self.W), self.wmul self.wone w = w
    wid_r : ∀ (w : self.W), self.wmul w self.wone = w
    wassoc : ∀ (u v w : self.W), self.wmul (self.wmul u v) w = self.wmul u (self.wmul v w)
  • structure(1 field)defined in Locus/Model.lean
    complete
    structure Interp {B : Type} (S : Sig B) (M : Frame B) : Type
    structure Interp {B : Type} (S : Sig B)
  (M : Frame B) : Type
    An interpretation of the primitive boxes.

    Fields

    box : {a b : Ty B} → S.Box a b → den M a → den M b
  • defdefined in Locus/Model.lean
    complete
    def eval {B : Type} {S : Sig B} {M : Frame B} (I : Interp S M)
  {a b : Ty B} : Mor S a b → den M a → den M b
    def eval {B : Type} {S : Sig B} {M : Frame B}
  (I : Interp S M) {a b : Ty B} :
  Mor S a b → den M a → den M b
    Denotation of morphisms.  `∘` is composition, `⊗` is the pairwise map,
`swap` is the twist, and the modality's operations are the writer
monad's: `eta` attaches the empty constraint, `mu` multiplies two
accumulated constraints, `str` carries a value past the boundary.
Theorem9.1.3
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 1✓L∃∀N

The equational theory is sound in every frame and interpretation:

f \equiv g \;\Longrightarrow\; \llbracket f \rrbracket_{\mathcal{I}} = \llbracket g \rrbracket_{\mathcal{I}} .

Rests on NEW: Interp, eval.

Lean code for Theorem9.1.3●1 theorem
  • theoremdefined in Locus/Model.lean
    complete
    theorem sound {B : Type} {S : Sig B} {M : Frame B} (I : Interp S M) {a b : Ty B}
  {f g : Mor S a b} (h : f ≡ g) : ⟦f⟧[I] = ⟦g⟧[I]
    theorem sound {B : Type} {S : Sig B} {M : Frame B}
  (I : Interp S M) {a b : Ty B}
  {f g : Mor S a b} (h : f ≡ g) :
  ⟦f⟧[I] = ⟦g⟧[I]
    **Soundness.**  Every equation `MEq` asserts is true in the model.

Stated over `MEq` as a whole rather than as loose lemmas, so that adding
a constructor without a matching argument breaks this proof.  That has
already earned its keep once: extending `MEq` from two equations to
twenty failed here with eighteen "alternative has not been provided"
errors, which is the obligation working.