locus: Blueprint

9.2. What is not derivable🔗

Definition9.2.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 9.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom source

The left strength \mathrm{strL} : \bigcirc a \otimes b \to \bigcirc(a \otimes b) is the strength conjugated by the symmetry. The two distributions \mathrm{dstL}_{a,b}, \mathrm{dstR}_{a,b} : \bigcirc a \otimes \bigcirc b \to \bigcirc(a \otimes b) absorb the left, respectively the right, constraint first:

\mathrm{dstL}_{a,b} = \mathrm{strL}_{a,\bigcirc b} \,;\, \bigcirc\mathrm{str}_{a,b} \,;\, \mu_{a \otimes b}, \qquad \mathrm{dstR}_{a,b} = \mathrm{str}_{\bigcirc a,b} \,;\, \bigcirc\mathrm{strL}_{a,b} \,;\, \mu_{a \otimes b} .

Lean code for Definition9.2.1●3 definitions
  • defdefined in Locus/Core.lean
    complete
    def strL {B : Type} {S : Sig B} (a b : Ty B) : Mor S (◯a ⊗ b) ◯(a ⊗ b)
    def strL {B : Type} {S : Sig B} (a b : Ty B) :
  Mor S (◯a ⊗ b) ◯(a ⊗ b)
    Left strength, derived from the right one by conjugating with `swap`.
  • defdefined in Locus/Core.lean
    complete
    def dstL {B : Type} {S : Sig B} (a b : Ty B) : Mor S (◯a ⊗ ◯b) ◯(a ⊗ b)
    def dstL {B : Type} {S : Sig B} (a b : Ty B) :
  Mor S (◯a ⊗ ◯b) ◯(a ⊗ b)
    Absorb the LEFT factor's constraint first.
  • defdefined in Locus/Core.lean
    complete
    def dstR {B : Type} {S : Sig B} (a b : Ty B) : Mor S (◯a ⊗ ◯b) ◯(a ⊗ b)
    def dstR {B : Type} {S : Sig B} (a b : Ty B) :
  Mor S (◯a ⊗ ◯b) ◯(a ⊗ b)
    Absorb the RIGHT factor's constraint first.
Theorem9.2.2
Statement uses 2
Statement dependency previews
Preview
Theorem 9.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

REFUTED: commutativity of the modality (Kock 1972) is not derivable. Over the empty signature, at the unit type,

\mathrm{dstL}_{I,I} \;\not\equiv\; \mathrm{dstR}_{I,I} .

The countermodel is the frame whose constraints are the lists of Booleans under concatenation, in which \llbracket \mathrm{dstL}_{I,I} \rrbracket \neq \llbracket \mathrm{dstR}_{I,I} \rrbracket.

Rests on NEW: Interp, eval; not audited: U, emptyInterp, emptySig, listFrame.

Lean code for Theorem9.2.2●2 theorems
  • theoremdefined in Locus/Independence.lean
    complete
    theorem comm_not_derivable : ¬dstL U U ≡ dstR U U
    theorem comm_not_derivable : ¬dstL U U ≡ dstR U U
    **Commutativity is not derivable.**  If `MEq` proved the two routes
equal, soundness would make them equal in every model, and the
countermodel says otherwise.

This is the whole value of having proved soundness: a soundness theorem
is a tool for showing things are NOT provable, and that is the use it is
being put to here.
  • theoremdefined in Locus/Independence.lean
    complete
    theorem dstL_ne_dstR :
  ⟦dstL U U⟧[emptyInterp Unit] ≠ ⟦dstR U U⟧[emptyInterp Unit]
    theorem dstL_ne_dstR :
  ⟦dstL U U⟧[emptyInterp Unit] ≠
    ⟦dstR U U⟧[emptyInterp Unit]
    **The two routes are different maps.**  Kernel-checked: the witness is
`pt`, and the two traces differ.
Theorem9.2.3
Statement uses 2
Statement dependency previews
Preview
Definition 9.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The gap is exactly commutativity of the constraint monoid. In every frame and interpretation, for all types a, b,

(\forall u\, v \in W.\; u \cdot v = v \cdot u) \;\Longrightarrow\; \llbracket \mathrm{dstL}_{a,b} \rrbracket_{\mathcal{I}} = \llbracket \mathrm{dstR}_{a,b} \rrbracket_{\mathcal{I}},

and conversely

\llbracket \mathrm{dstL}_{I,I} \rrbracket_{\mathcal{I}} = \llbracket \mathrm{dstR}_{I,I} \rrbracket_{\mathcal{I}} \;\Longrightarrow\; \forall u\, v \in W.\; u \cdot v = v \cdot u .

Whether the calculus should adopt the equation is OPEN: it is a design decision about what a constraint is.

Rests on NEW: Interp, eval.

Lean code for Theorem9.2.3●2 theorems
  • theoremdefined in Locus/Independence.lean
    complete
    theorem dst_agree_of_comm {B : Type} {S : Sig B} {M : Frame B} (I : Interp S M)
  (hcomm : ∀ (u v : M.W), M.wmul u v = M.wmul v u) (a b : Ty B) :
  ⟦dstL a b⟧[I] = ⟦dstR a b⟧[I]
    theorem dst_agree_of_comm {B : Type} {S : Sig B}
  {M : Frame B} (I : Interp S M)
  (hcomm :
    ∀ (u v : M.W),
      M.wmul u v = M.wmul v u)
  (a b : Ty B) :
  ⟦dstL a b⟧[I] = ⟦dstR a b⟧[I]
    **The two routes agree iff the constraints commute.**  One direction,
the useful one: commutativity of `wmul` is enough.  So the equation is
INDEPENDENT of the present `MEq`, not false — and the price of adding it
is a commutativity field on `Frame`, which is a claim about what a
constraint IS, not a technical convenience.
  • theoremdefined in Locus/Independence.lean
    complete
    theorem comm_of_dst_agree {B : Type} {S : Sig B} {M : Frame B} (I : Interp S M)
  (h : ⟦dstL Ty.unit Ty.unit⟧[I] = ⟦dstR Ty.unit Ty.unit⟧[I])
  (u v : M.W) : M.wmul u v = M.wmul v u
    theorem comm_of_dst_agree {B : Type} {S : Sig B}
  {M : Frame B} (I : Interp S M)
  (h :
    ⟦dstL Ty.unit Ty.unit⟧[I] =
      ⟦dstR Ty.unit Ty.unit⟧[I])
  (u v : M.W) : M.wmul u v = M.wmul v u
    The converse direction, read off the same normal form: if the two
routes agree at a frame, its constraints commute.  Stated for
`Ty.unit`, where the values carry no information and only the
constraints can differ.
Theorem9.2.4
uses 1used by 0✓L∃∀N

REFUTED: naturality of copy and of discard is not derivable. By Fox's theorem (1976, not formalised here) the calculus is therefore not cartesian: it is a copy-discard category. Over the signature with one base type A and one primitive box at every pair of types, for the box x : A \to A,

x \,;\, \mathrm{copy}_A \;\not\equiv\; \mathrm{copy}_A \,;\, (x \otimes x), \qquad x \,;\, \mathrm{del}_A \;\not\equiv\; \mathrm{del}_A .

The countermodels are relational (RelModel.lean): x read as the total relation on the Booleans for the first, as the empty relation for the second.

Rests on not audited: A, bx, oneSig.

Lean code for Theorem9.2.4●3 theorems
  • theoremdefined in Locus/Independence.lean
    complete
    theorem not_cartesian :
  ¬bx ≫ Mor.copy A ≡ Mor.copy A ≫ (bx ⊗ bx) ∧
    ¬bx ≫ Mor.del A ≡ Mor.del A
    theorem not_cartesian :
  ¬bx ≫ Mor.copy A ≡
        Mor.copy A ≫ (bx ⊗ bx) ∧
    ¬bx ≫ Mor.del A ≡ Mor.del A
    **The category is not cartesian.**  Fox's theorem makes a symmetric
monoidal category with a uniform comonoid cartesian exactly when every
morphism is a comonoid homomorphism.  The two theorems above say `MEq`
does not prove that of `bx`, so the syntax is a copy-discard category
and not a cartesian one — which is the position `Core.lean` takes and
this is its certificate.
  • theoremdefined in Locus/Independence.lean
    complete
    theorem copyNat_not_derivable : ¬bx ≫ Mor.copy A ≡ Mor.copy A ≫ (bx ⊗ bx)
    theorem copyNat_not_derivable :
  ¬bx ≫ Mor.copy A ≡
      Mor.copy A ≫ (bx ⊗ bx)
    **Naturality of `copy` is not derivable.**  Under the total reading,
running `bx` and forking the result can only produce a pair of EQUAL
values, while forking first and running `bx` on each prong produces any
pair at all.  The witness is `(true, false)`, which the right-hand side
reaches and the left-hand side cannot.

So copying a computation is not copying its result, and `MEq` does not
claim otherwise.
  • theoremdefined in Locus/Independence.lean
    complete
    theorem delNat_not_derivable : ¬bx ≫ Mor.del A ≡ Mor.del A
    theorem delNat_not_derivable :
  ¬bx ≫ Mor.del A ≡ Mor.del A
    **Naturality of `del` is not derivable.**  Under the empty reading,
running `bx` and then discarding relates nothing to anything, while
discarding directly relates everything to the point.

So discarding a computation is not the same as never having run it, and
`MEq` does not claim otherwise.  Note this needs the opposite pathology
from the previous theorem: `copy` fails on too MANY outputs, `del` on
too few.
Theorem9.2.5
uses 1used by 0✓L∃∀N

A Frobenius (hypergraph) structure admits only trivial function models. Adjoin boxes \mathrm{mrg}_a : a \otimes a \to a and I \to a to a signature. For every frame and interpretation \mathcal{J} of the extended signature and every type a, if both Frobenius laws hold in the model,

\llbracket (\mathrm{copy}_a \otimes \mathrm{id}_a) \,;\, \alpha \,;\, (\mathrm{id}_a \otimes \mathrm{mrg}_a) \rrbracket_{\mathcal{J}} = \llbracket \mathrm{mrg}_a \,;\, \mathrm{copy}_a \rrbracket_{\mathcal{J}} = \llbracket (\mathrm{id}_a \otimes \mathrm{copy}_a) \,;\, \alpha^{-1} \,;\, (\mathrm{mrg}_a \otimes \mathrm{id}_a) \rrbracket_{\mathcal{J}},

then \llbracket a \rrbracket has at most one element:

\forall x\, y \in \llbracket a \rrbracket.\; x = y .

Hence, over the one-box signature of calc_not_cartesian extended with these boxes, and the frame whose base type is the Booleans, no interpretation in functions validates every equation of the Frobenius theory. The relational model, reading the two new boxes as the converses of copy and discard, validates them all.

Rests on NEW: Interp, eval, hyperRInterp; not audited: boolFrame, oneSig.

Lean code for Theorem9.2.5●3 theorems
  • theoremdefined in Locus/Hyper.lean
    complete
    theorem frobenius_forces_subsingleton {B : Type} {S : Sig B} {M : Frame B}
  (J : Interp (hyperSig S) M) (a : Ty B)
  (hL : ⟦frobL a⟧[J] = ⟦mrgCopy a⟧[J])
  (hR : ⟦frobR a⟧[J] = ⟦mrgCopy a⟧[J]) (x y : den M a) : x = y
    theorem frobenius_forces_subsingleton {B : Type}
  {S : Sig B} {M : Frame B}
  (J : Interp (hyperSig S) M) (a : Ty B)
  (hL : ⟦frobL a⟧[J] = ⟦mrgCopy a⟧[J])
  (hR : ⟦frobR a⟧[J] = ⟦mrgCopy a⟧[J])
  (x y : den M a) : x = y
    **A function model of the Frobenius laws has subsingleton denotations.**
Stated for an arbitrary interpretation into the writer model, so that it
covers every `Frame` at once rather than a chosen one.
  • theoremdefined in Locus/Independence.lean
    complete
    theorem no_sound_function_model (J : Interp (hyperSig oneSig) boolFrame)
  (hs :
    ∀ {x y : Ty Unit} {f g : Mor (hyperSig oneSig) x y},
      HMEq f g → ⟦f⟧[J] = ⟦g⟧[J]) :
  False
    theorem no_sound_function_model
  (J : Interp (hyperSig oneSig) boolFrame)
  (hs :
    ∀ {x y : Ty Unit}
      {f g : Mor (hyperSig oneSig) x y},
      HMEq f g → ⟦f⟧[J] = ⟦g⟧[J]) :
  False
    **No sound interpretation of the hypergraph layer into functions**, once
a base type has two elements.  `boolFrame`'s base type is `Bool`, so
`true ≠ false` finishes it.

Set is not a hypergraph category, and this is that fact in the form the
development can use.
  • theoremdefined in Locus/Hyper.lean
    complete
    theorem soundRelH {B : Type} {S : Sig B} {M : Frame B} (I : RInterp S M)
  {a b : Ty B} {f g : Mor (hyperSig S) a b} (h : HMEq f g) :
  evalRel (hyperRInterp I) f = evalRel (hyperRInterp I) g
    theorem soundRelH {B : Type} {S : Sig B}
  {M : Frame B} (I : RInterp S M)
  {a b : Ty B}
  {f g : Mor (hyperSig S) a b}
  (h : HMEq f g) :
  evalRel (hyperRInterp I) f =
    evalRel (hyperRInterp I) g