Chapter 159Core route

Symmetric Monoidal Categories and Graphical Linear Semantics

Take the file program of section 18.3. A term $Γ; f_{1} : File, f_{2} : File ⊢ close f_{1} \otimes read f_{2} : 1 \otimes (File \otimes Bytes)$ uses two independently owned handles, once each. Suppose its meaning is a map out of a product $[[File]] \times [[File]]$ in a category with finite products. Then the diagonal $Δ : X \to X \times X$ exists, and composing with it produces a map out of one handle that behaves as if it owned two: $[[close f_{1} \otimes read f_{2}]] \circ Δ .$ The typing rule T-TensorI forbids exactly that term, since $Δ_{1} ⊎ Δ_{2}$ is defined only for disjoint domains. A terminal object is no better: it provides $X \to 1$ for every $X$ , a map that discards a live handle, and the calculus has no such term either.

So a semantics of $λ_{lin}$ may not interpret the comma of a linear context as a categorical product. It needs a binary operation on objects that carries no diagonal and no projection. This chapter derives that operation from the equations the file program forces, and then makes the resulting calculus graphical.

The operation forced by rebracketing

Write $X \otimes Y$ for the object interpreting two independently owned resources, with no assumption yet beyond its existence on objects. Three demands follow immediately from the syntax.

Definition 159.1 — Tensor data ¶

A tensor on a category $C$ consists of a functor $\otimes : C \times C \to C$ , an object $I$ , and three families of isomorphisms $\begin{aligned} α_{X, Y, Z} & : (X \otimes Y) \otimes Z \to X \otimes (Y \otimes Z), \\ λ_{X} & : I \otimes X \to X, & ρ_{X} & : X \otimes I \to X, \end{aligned}$ each natural in every argument.

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Functoriality is not decoration: it is the statement that a linear function may be applied inside a tensor without disturbing the other component. In the running example, $read \otimes {id}_{}$ is the map that reads the first handle and leaves the second untouched, and functoriality is $(g \circ f) \otimes (g^{'} \circ f^{'}) = (g \otimes g^{'}) \circ (f \otimes f^{'}), {id}_{X} \otimes {id}_{Y} = {id}_{X \otimes Y},$ which says that operating on the two components in either order or simultaneously gives the same thing.

Example 159.2 — Naturality is a program equation ¶

Let $f : = close$ and $g : = read$ . The two terms $let x \otimes y = (f f_{1}) \otimes (g f_{2}) in \dots and (f \otimes g) applied after regrouping$ are equal by T-TensorI and the $β$ -rule for tensor. Semantically this is naturality of $α$ : the square $α_{X^{'}, Y^{'}, Z^{'}} \circ ((f \otimes g) \otimes h) = (f \otimes (g \otimes h)) \circ α_{X, Y, Z}$ commutes for all $f, g, h$ . Naturality is therefore checked before any coherence axiom is stated: it is a consequence of the calculus, not an assumption about pictures.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proposition 159.3 — The pentagon is forced ¶

Suppose $C$ carries tensor data and that for every four objects the two composites $((W \otimes X) \otimes Y) \otimes Z \to W \otimes (X \otimes (Y \otimes Z))$ built from $α$ agree. Then the pentagon identity $α_{W, X, Y \otimes Z} \circ α_{W \otimes X, Y, Z} = ({id}_{W} \otimes α_{X, Y, Z}) \circ α_{W, X \otimes Y, Z} \circ (α_{W, X, Y} \otimes {id}_{Z})$ holds; conversely the pentagon identity implies the agreement.

Referenced from 6 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Proposition 159.3 — The pentagon is forced

Proof. There are exactly five ways to move one pair of parentheses at a time from $((W \otimes X) \otimes Y) \otimes Z$ to $W \otimes (X \otimes (Y \otimes Z))$ , and they form a pentagon whose two sides are the two displayed composites: the left side reassociates the outer two brackets and then the inner, the right side reassociates innermost first. The hypothesis says the two sides are equal, which is the identity. The converse is immediate. ◻

Proposition 159.4 — The triangle is forced ¶

If the two composites $(X \otimes I) \otimes Y \to X \otimes Y$ built from $α, ρ, λ$ agree, then $({id}_{X} \otimes λ_{Y}) \circ α_{X, I, Y} = ρ_{X} \otimes {id}_{Y}$ , and conversely.

Referenced from 5 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Proposition 159.4 — The triangle is forced

Proof. The two composites are the two sides of the displayed equation; there are no others, since each of $ρ$ and $λ$ can be applied in exactly one position. ◻

Definition 159.5 — Monoidal category ¶

A monoidal category is a category with tensor data (definition 159.1) satisfying the pentagon (proposition 159.3) and the triangle (proposition 159.4).

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Lemma 159.6 — Two derived unit equations ¶

In a monoidal category, $λ_{I} = ρ_{I}$ and ${id}_{X} \otimes λ_{Y}$ determines $λ_{X \otimes Y}$ through $α$ .

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Lemma 159.6 — Two derived unit equations

Proof. For the first, apply the triangle at $X = I$ and use naturality of $λ$ at $λ_{Y}$ to cancel $α$ ; the two resulting arrows $I \otimes I \to I$ agree. For the second, naturality of $λ$ in its argument gives $λ_{X \otimes Y} = (λ_{X} \otimes {id}_{Y}) \circ α^{- 1}$ , and the triangle rewrites the right-hand side as stated. ◻

Exchange, and why symmetry is a further axiom

Two independently owned handles may be presented in either order; a semantics must therefore relate $X \otimes Y$ and $Y \otimes X$ .

Definition 159.7 — Braiding and symmetry ¶

A braiding is a natural isomorphism $γ_{X, Y} : X \otimes Y \to Y \otimes X$ satisfying the two hexagons $\begin{aligned} α_{Y, Z, X} \circ γ_{X, Y \otimes Z} \circ α_{X, Y, Z} & = ({id}_{Y} \otimes γ_{X, Z}) \circ α_{Y, X, Z} \circ (γ_{X, Y} \otimes {id}_{Z}), \\ α_{Z, X, Y}^{- 1} \circ γ_{X \otimes Y, Z} \circ α_{X, Y, Z}^{- 1} & = (γ_{X, Z} \otimes {id}_{Y}) \circ α_{X, Z, Y}^{- 1} \circ ({id}_{X} \otimes γ_{Y, Z}) . \end{aligned}$ It is a symmetry when $γ_{Y, X} \circ γ_{X, Y} = {id}_{X \otimes Y}$ . A symmetric monoidal category is a monoidal category with a symmetry.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proposition 159.8 — Braided but not symmetric ¶

There is a braided monoidal category in which $γ_{X, X} \circ γ_{X, X} \neq {id}_{X \otimes X}$ .

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Proposition 159.8 — Braided but not symmetric

Proof. Let $B$ have one object $*$ with $\otimes$ the unique operation, and let ${hom}_{B} (*, *)$ be the group $Z$ under addition, with composition addition and $\otimes$ on arrows also addition. This is a strict monoidal category: associativity and units are the group laws. Put $γ : = 1 \in Z$ . Naturality is automatic, since the group is abelian; both hexagons reduce to $1 + 0 + 0 = 0 + 0 + 1$ , which holds. But $γ \circ γ = 2 \neq 0 = {id}_{}$ . So the braiding is not a symmetry: a crossing composed with itself is a nontrivial arrow, not the identity. ◻

Remark 159.9 — What the counterexample models ¶

In a braided setting the two ways of exchanging two resources — passing the first in front of the second, or behind — are different arrows. For linear programs no such distinction is available: the calculus of definition 18.5 identifies a linear context with a finite map, so exchange is equality of maps and applying it twice is the identity. Hence the symmetric axiom, and not merely the braided one, is what $λ_{lin}$ requires.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Free constructions and normal forms

Definition 159.10 — Typed signature ¶

A signature $S$ consists of a set of generating objects and, for each pair of finite lists $\vec{X}, \vec{Y}$ of generating objects, a set of generating arrows $f : \vec{X} \to \vec{Y}$ .

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Construction 159.11 — The free strict symmetric monoidal category ¶

Let $FS (S)$ have as objects the finite lists of generating objects, with $\otimes$ concatenation and $I$ the empty list. Arrows are generated by the $f \in S$ , the identities, a symmetry $γ_{\vec{X}, \vec{Y}}$ for each pair of lists, composition and $\otimes$ , modulo the equations of a strict symmetric monoidal category — associativity and units on the nose, functoriality of $\otimes$ , naturality of $γ$ , the hexagons and the symmetry axiom.

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Theorem 159.12 — Normal form and decidable equality ¶

Every arrow of $FS (S)$ is equal to one of the form $σ_{k} \circ (g_{k} \otimes {id}_{}) \circ \dots \circ σ_{1} \circ (g_{1} \otimes {id}_{}) \circ σ_{0},$ in which each $g_{i}$ is a single generator and each $σ_{i}$ is a permutation built from symmetries; and two such forms denote the same arrow if and only if they have the same sequence of generators up to the equivalence generated by exchanging adjacent generators acting on disjoint parts of the list together with the induced permutation. Consequently equality of arrows in $FS (S)$ is decidable when $S$ is finite and the arrows are given by finite expressions.

Referenced from 14 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Theorem 159.12 — Normal form and decidable equality

Proof. Existence. Any expression is a composite of layers, each of which is a tensor of generators, identities and symmetries. Using functoriality of $\otimes$ , split a layer containing two generators into two consecutive layers, one generator each; using naturality of $γ$ , move every symmetry past a generator layer, at the cost of relabelling which positions the generator acts on. Repeating drives all symmetries into the interleaving permutations $σ_{i}$ , giving the displayed form. The procedure terminates because each step strictly decreases the number of generators occurring in a common layer, and the number of layers is bounded by the number of generators.

Uniqueness. Interpret $FS (S)$ in the category whose objects are lists and whose arrows $\vec{X} \to \vec{Y}$ are pairs of a sequence of generators and a bijection recording positions — this is a symmetric monoidal category, and the interpretation sends the displayed normal form to its own data. Hence two normal forms with different generator sequences up to the stated equivalence have different images and are not equal. Conversely, exchanging adjacent generators on disjoint positions is derivable from functoriality, so the equivalence is sound.

Decidability. Normalisation is effective and the equivalence on generator sequences is decidable, being generated by finitely many adjacent exchanges on a finite sequence. ◻

Remark 159.13 — Scope of the coherence used ¶

Theorem 159.12 is a statement about the free strict symmetric monoidal category on a signature, which is all this chapter needs: every arrow of a monoidal category is, by proposition 159.3 and proposition 159.4, equal to one in which the bracketing is immaterial, so the strict free category computes the equations of the non-strict one. The stronger topological coherence theorems — that a diagram of a certain shape in the plane determines an arrow up to isotopy — are not proved here and are not used; where a diagram below is called a proof, it is because it abbreviates a composite already shown equal by the equations above.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

String diagrams

Definition 159.14 — Diagrams ¶

A diagram over a signature $S$ consists of a finite set of boxes, each labelled by a generator $f : \vec{X} \to \vec{Y}$ and carrying $| \vec{X} |$ input ports and $| \vec{Y} |$ output ports typed accordingly; a list of free input ports and a list of free output ports; and a bijection wiring each output port (of a box or free input) to exactly one input port (of a box or free output) with matching type, such that the directed graph on boxes induced by the wiring is acyclic. Two diagrams are equal when there is a type-preserving bijection of boxes and ports respecting the wiring. Sequential composition plugs the free outputs of one into the free inputs of another; parallel composition places two diagrams side by side and concatenates the free lists.

Referenced from 9 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Theorem 159.15 — Soundness and completeness for the free fragment ¶

Sending a diagram to the arrow of $FS (S)$ obtained by reading it in any order compatible with the acyclic structure is well defined, and it is a bijection between diagrams from $\vec{X}$ to $\vec{Y}$ and arrows $\vec{X} \to \vec{Y}$ of $FS (S)$ .

Referenced from 8 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Theorem 159.15 — Soundness and completeness for the free fragment

Proof. Well defined. Two compatible orders differ by transpositions of adjacent boxes acting on disjoint ports, and by theorem 159.12 those give equal arrows.

Surjective. Given a normal form, build the diagram with one box per generator, wired according to the interleaving permutations.

Injective. A diagram is recovered from the normal form of its arrow: by the uniqueness clause of theorem 159.12 the arrow determines the sequence of generators up to disjoint exchange and the accompanying bijection on positions, which is exactly the data of the wiring up to the bijection allowed in definition 159.14. ◻

Remark 159.16 — What a picture is allowed to prove ¶

Theorem 159.15 licenses one kind of argument: two diagrams that are equal as combinatorial objects denote equal arrows, and conversely. It licenses nothing about deformations of a drawing on paper — an ambient isotopy argument requires a topological coherence theorem, which remark 159.13 does not supply. Where a proof below reasons diagrammatically, the diagram is used as notation for a normal form.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Closure, and the interpretation of the linear calculus

The tensor interprets the comma of a linear context. Linear implication needs one more operation.

Definition 159.17 — Monoidal closed ¶

A symmetric monoidal category is closed when for every object $Y$ the functor $- \otimes Y$ has a right adjoint $Y ⊸ -$ ; that is, there are natural bijections $Λ : {hom}_{C} (X \otimes Y, Z) ≅ {hom}_{C} (X, Y ⊸ Z),$ with counit ${ev}_{Y, Z} : (Y ⊸ Z) \otimes Y \to Z$ .

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Lemma 159.18 — The two inverse laws ¶

In a symmetric monoidal closed category, $ev \circ (Λ (f) \otimes {id}_{Y}) = f$ for every $f : X \otimes Y \to Z$ , and $Λ (ev \circ (g \otimes {id}_{Y})) = g$ for every $g : X \to Y ⊸ Z$ .

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Lemma 159.18 — The two inverse laws

Proof. The first is the triangle identity of the adjunction at $f$ , the second its mate; naturality of $Λ$ in $X$ is what makes both statements hold for all $f$ and $g$ rather than for the identity alone. ◻

Definition 159.19 — Interpretation of λ _ lin ¶

Fix a symmetric monoidal closed category $C$ and an object $[[b]]$ for each atomic type. Extend by $[[1]] : = I, [[A \otimes B]] : = [[A]] \otimes [[B]], [[A ⊸ B]] : = [[A]] ⊸ [[B]],$ and interpret a linear context $Δ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ by $[[A_{1}]] \otimes \dots \otimes [[A_{n}]]$ , bracketed to the right. A derivation of $Γ; Δ ⊢ e : A$ with $Γ$ empty is interpreted by an arrow $[[Δ]] \to [[A]]$ : T-LVar by an identity; T-TensorI by $\otimes$ of the two subarrows precomposed with the associativity and symmetry isomorphism realising the split $Δ_{1} ⊎ Δ_{2}$ ; T-TensorE by composing with the subarrow for $e_{1}$ in the first component; T-LolliI by $Λ$ ; T-LolliE by $ev$ after $\otimes$ of the two subarrows; and T-OneI, T-OneE by $λ$ and $ρ$ .

Referenced from 6 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Lemma 159.20 — Independence of the split isomorphism ¶

The isomorphism $[[Δ]] \to [[Δ_{1}]] \otimes [[Δ_{2}]]$ used in definition 159.19 is uniquely determined by the split $Δ = Δ_{1} ⊎ Δ_{2}$ .

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Lemma 159.20 — Independence of the split isomorphism

Proof. Any two such isomorphisms are built from $α$ , $λ$ , $ρ$ and $γ$ and induce the same permutation of the variables, since both realise the same split. Two arrows of $FS (S)$ built from structural isomorphisms with the same underlying permutation are equal by the uniqueness clause of theorem 159.12, which has no generators to distinguish them. The claim then transfers to $C$ along the interpretation of the free category. ◻

Theorem 159.21 — Semantic substitution and soundness ¶

Let $Γ$ be empty throughout. If $Δ_{1} ⊢ e_{1} : A$ and $Δ_{2}, x : A ⊢ e_{2} : C$ then $[[e_{2} [e_{1} / x]]] = [[e_{2}]] \circ ({id}_{[[Δ_{2}]]} \otimes [[e_{1}]]) \circ s,$ where $s$ is the split isomorphism of lemma 159.20. Consequently, if $e ⟶ e^{'}$ by the $β$ - and $η$ -rules of definition 18.4 then $[[e]] = [[e^{'}]]$ .

Referenced from 6 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Theorem 159.21 — Semantic substitution and soundness

Proof. Substitution. Induction on the derivation of $e_{2}$ . In the variable case $e_{2} = x$ and both sides are $[[e_{1}]]$ after the unit isomorphism. In the tensor-introduction case the linear context splits, $x$ lies in exactly one part by the disjointness condition of definition 18.1, and the induction hypothesis applies there while the other component is untouched — this is functoriality of $\otimes$ . In the abstraction case the claim follows from naturality of $Λ$ in its first argument. In the application case it follows from naturality of $ev$ , which is the counit of the adjunction. Lemma 159.20 guarantees that the structural isomorphisms produced by the two sides agree.

Soundness. Each reduction rule is now an equation already available. The $β$ -rule for $⊸$ is the first law of lemma 159.18 combined with the substitution equation; the $β$ -rule for $\otimes$ is the substitution equation applied twice, using functoriality to see that the two components are substituted independently; the $β$ -rule for $1$ is naturality of $λ$ ; and the $η$ -rule for $⊸$ is the second law of lemma 159.18. Compatibility with evaluation contexts is functoriality of $\otimes$ and of composition. ◻

Example 159.22 — The file program, twice ¶

Interpret $File$ and $Bytes$ by objects $F$ and $B$ , and take $open : I \to F$ , $read : F \to F \otimes B$ and $close : F \to I$ as generators. The term $let f \otimes b = read (open *) in (close f) \otimes b$ is interpreted by the composite $I \overset{open}{\to} F \overset{read}{\to} F \otimes B \overset{close \otimes {id}_{B}}{\to} I \otimes B \overset{λ_{B}}{\to} B .$ As a diagram in the sense of definition 159.14 it is a single line entering the $open$ box, continuing into $read$ , which has two output wires; the $F$ -wire enters $close$ and terminates, and the $B$ -wire is the free output. The two readings agree by theorem 159.15. The program that forgets to close is the diagram with a dangling $F$ -wire, which is not a diagram from $I$ to $B$ at all, because definition 159.14 requires every output port to be wired; the term is likewise not typable, because T-TensorE would leave $f$ unused.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

The unrestricted context

The interpretation of definition 159.19 assumed $Γ$ empty. A variable in $Γ$ may be used any number of times, including none, so its interpretation must admit duplication and discarding — exactly the maps a tensor lacks.

Proposition 159.23 — Declaring objects copyable is not enough ¶

Suppose $C$ is symmetric monoidal closed and $X$ is an object equipped with $d : X \to X \otimes X$ and $e : X \to I$ satisfying the comonoid laws. Then $X$ need not admit a natural such structure, and choosing one for each object of a subclass does not make the interpretation of T-UVar well defined unless the choice is natural in $X$ and compatible with $\otimes$ .

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Proposition 159.23 — Declaring objects copyable is not enough

Proof. A comonoid structure on a single object is data, not a property, and different choices give different interpretations of a term that duplicates that variable twice in different orders — unless $d$ is coassociative and cocommutative, which is part of the comonoid laws, and unless $d$ is natural, which the hypothesis does not require. Without naturality the substitution equation of theorem 159.21 fails: substituting a term for a duplicated variable would have to commute $d$ past the substituted arrow, and that is precisely a naturality square. Compatibility with $\otimes$ is needed for the same reason at a variable of tensor type. ◻

Definition 159.24 — Linear–nonlinear adjunction ¶

A linear–nonlinear adjunction consists of a cartesian closed category $X$ , a symmetric monoidal closed category $C$ , and a symmetric monoidal adjunction $L : X ⇄ C : R, L ⊣ R,$ in which $L$ is strong monoidal — the comparisons $L (A \times B) \to L A \otimes L B$ and $L (1) \to I$ are isomorphisms — and $R$ is lax monoidal.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Theorem 159.25 — The exponential comonad ¶

Let $L ⊣ R$ be a linear–nonlinear adjunction and put $! : = L \circ R : C \to C$ . Then $!$ is a comonad, and every object $! X$ carries natural maps ${contr}_{X} :! X \to! X \otimes! X, {weak}_{X} :! X \to I$ making it a commutative comonoid, natural in $X$ and compatible with the comonad structure.

Referenced from 6 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Theorem 159.25 — The exponential comonad

Proof. $!$ is a comonad because it is $L R$ for an adjunction, with counit the counit of the adjunction and comultiplication $L η R$ . For the comonoid structure, $X$ is cartesian, so every object $A$ carries the diagonal $Δ_{A} : A \to A \times A$ and the unique map $A \to 1$ , and these are natural and form a commutative comonoid. Apply $L$ and use that $L$ is strong monoidal: $\begin{aligned} {contr}_{X} & : = (L (A \times A) \overset{≅}{\to} L A \otimes L A) \circ L (Δ_{A}), \\ {weak}_{X} & : = (L (1) \overset{≅}{\to} I) \circ L (!_{A}), \end{aligned}$ with $A : = R X$ . Naturality is naturality of $Δ$ and of the monoidal comparisons; the comonoid laws are the images under a strong monoidal functor of the corresponding laws in $X$ , which hold because $X$ is cartesian. Compatibility with the comonad structure is the statement that the comparisons are compatible with $η$ and $ε$ , which is part of a monoidal adjunction. ◻

Corollary 159.26 — Interpretation of the full calculus ¶

With $!$ as in theorem 159.25, extend definition 159.19 by $[[! A]] : =! [[A]]$ and interpret $Γ; Δ ⊢ e : A$ by an arrow $! [[Γ]] \otimes [[Δ]] \to [[A]]$ , using $contr$ for a variable of $Γ$ used twice and $weak$ for one used not at all. Then theorem 159.21 holds for the full calculus of definition 18.5.

Referenced from 4 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Corollary 159.26 — Interpretation of the full calculus

Proof. The substitution induction acquires two new cases, both settled by naturality: duplicating a $Γ$ -variable and then substituting equals substituting and then duplicating, by naturality of $contr$ ; and discarding commutes with substitution by naturality of $weak$ . The rules for $!$ — introduction at a value and elimination by a $let$ — are the unit and counit of the comonad, and their $β$ -rule is a triangle identity. ◻

Definition 159.27 — Lax, oplax, strong ¶

A functor $F : C \to D$ between monoidal categories is lax monoidal when it carries $m_{X, Y} : F X \otimes F Y \to F (X \otimes Y)$ and $m_{I} : I \to F I$ , natural and compatible with $α, λ, ρ$ ; oplax when the comparisons point the other way; and strong when they are isomorphisms.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Example 159.28 — Three translations that fail differently ¶

Let $X$ be sets and functions with $\times$ , and $C$ a symmetric monoidal category. The functor sending a set $A$ to a chosen coproduct of $A$ copies of $I$ is strong monoidal when $C$ has coproducts distributing over $\otimes$ . The forgetful functor $R$ of definition 159.24 is lax and not strong: there is a map $R X \times R Y \to R (X \otimes Y)$ given by the adjunction, but no inverse, since a map into $X \otimes Y$ need not split. The functor sending a comonoid to its carrier is oplax: the comultiplication provides $F (X \otimes Y) \to F X \otimes F Y$ , not the reverse. Each direction of failure is the direction in which the corresponding structural map exists.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proposition 159.29 — Preservation equations for the interpretation ¶

In a linear–nonlinear adjunction, the interpretation of corollary 159.26 satisfies $\begin{aligned} [[! (A \otimes B)]] & ≅ [[! A]] \otimes [[! B]] & is not asserted, \\ L (A \times B) & ≅ L A \otimes L B & is . \end{aligned}$ Precisely: $L$ strong monoidal is used exactly in the construction of $contr$ and $weak$ in theorem 159.25, and $R$ lax monoidal is used exactly in verifying that the adjunction is monoidal.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Proof of Proposition 159.29 — Preservation equations for the interpretation

Proof. Inspect the proof of theorem 159.25: the comparisons of $L$ are inverted there, and nowhere else; the comparisons of $R$ appear only in the compatibility of unit and counit with the monoidal structure. The non-assertion is genuine: $! (A \otimes B)$ and $! A \otimes! B$ are related by a canonical map that need not be invertible, and no step above uses one. ◻

Four extensions this chapter does not make

Each of the following is a natural next demand on the file example, and each requires structure that has not been constructed.

An external category acting on the model. Suppose one wants a family of resources indexed by an external parameter, with the parameter category acting on $C$ . This is an action of a monoidal category on a category, with its own coherence conditions; nothing above supplies it, and $\otimes$ alone does not, since one of its arguments would have to leave $C$ .

Feedback. A protocol that loops — read until end of file — asks for an operation taking $f : X \otimes U \to Y \otimes U$ to $X \to Y$ , hiding $U$ . Such a trace satisfies its own axioms, and it is not derivable: in $FS (S)$ the normal form of theorem 159.12 has no arrow of that shape, since every generator occurrence is on a directed path from a free input to a free output.

A bent input wire. Turning an input into an output asks for maps $I \to X \otimes X^{*}$ and $X^{*} \otimes X \to I$ satisfying the triangle equations. Their presence makes $\otimes$ self-dual in a way that definition 159.17 does not provide: closure gives $X ⊸ I$ , not a dual with a unit.

Reversal. Reversing a computation asks for an involution on arrows fixing objects and compatible with $\otimes$ . The file generators $open$ , $read$ , $close$ have no such reversal, and definition 159.10 attaches none.

These four demands motivate the structures named monoidal action, trace, compact closure and dagger. Their rule tables and their proofs belong to the routes that construct them; nothing in this chapter may be used to assert that $C$ has any of them.

Exercise 159.1 ¶

★☆☆ Normalize the two expressions $((X \otimes Y) \otimes Z) \otimes W$ and $X \otimes (Y \otimes (Z \otimes W))$ to the same list using construction 159.11, and exhibit the two composites of proposition 159.3 between them, showing every object.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.2 ¶

★☆☆ Which of the following are diagrams over the file signature of example 159.22: a box $read$ whose $F$ -output is wired to its own $F$ -input; a box $close$ with an unwired input; a pair of $read$ boxes whose outputs are both wired to a single $close$ ? For each, name the clause of definition 159.14 it violates or exhibit the arrow it denotes.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.3 ¶

★★☆ Translate the derivation of $f_{1} : File, f_{2} : File ⊢ (close f_{1}) \otimes (read f_{2}) : 1 \otimes (File \otimes Bytes)$ into an arrow of $C$ using definition 159.19, showing the split isomorphism explicitly, and draw the corresponding diagram with every wire typed.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.4 ¶

★★☆ Prove one hexagon equation of definition 159.7 algebraically from naturality of $γ$ and the pentagon, and then verify the same equation by comparing the two diagrams of definition 159.14 that the two sides denote. State which of the two arguments remark 159.16 permits as a proof.

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.5 ¶

★★☆ Give categories separating, in order: cartesian from merely monoidal; monoidal from braided; braided from symmetric; and symmetric monoidal from symmetric monoidal closed. For each, name the structural map that exists on one side and not the other.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Boundary and seminar

The endpoint of this chapter is the symmetric monoidal closed interface together with the linear–nonlinear adjunction: definition 159.5, definition 159.7, theorem 159.12, theorem 159.15, definition 159.17, theorem 159.21, theorem 159.25 and corollary 159.26. The boundaries are these. The coherence used is the free-strict normal form of theorem 159.12 and nothing stronger; remark 159.13 and remark 159.16 say exactly what a diagram may be used for. The four structures of section 159.7 are motivated and not constructed. Enriched categories and general bicategories do not appear. And no argument of this chapter is used to modify the syntactic development of chapter 18: theorem 159.21 interprets that calculus and proves nothing new about it.

The proof base divides as follows. The mixed linear/nonlinear calculus, the adjunction of definition 159.24 and the derivation of the exponential comonad are Benton’s [Ben94]; the resource reading of the connectives is Girard’s [Gir87]; the coherence vocabulary and the pentagon and triangle of proposition 159.3, proposition 159.4 are Mac Lane’s [ML98a]; the exact soundness and completeness statement for the graphical language of closed symmetric monoidal categories is [RG26], and theorem 159.15 is stated here only at the free-strict signature it proves; the long proof-theoretic route from linear logic to monoidal semantics is [Mel09]; and the pedagogical synthesis relating these to computation is [BS09]. The mechanized coherence library and diagram editor of [Pou26] is a formal and practical comparison at its own monoidal signature; no theorem above depends on it.

[4]

Suggested first pass.

Begin with exercise 159.6, then exercise 159.7, and finish with exercise 159.9.

Exercise 159.6 ¶

★★★ Implement the normalisation procedure in the proof of theorem 159.12 by hand on an expression with four generators and two symmetries, recording each rewrite and the measure that decreases. Then exhibit two expressions with the same normal form and different-looking diagrams, and explain why theorem 159.15 does not make them different diagrams.

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.7 ¶

★★★ Construct a concrete linear–nonlinear adjunction: take $C$ to be the category of pointed sets with smash product and $X$ to be sets, with $L$ the “add a base point” functor. Verify that $L$ is strong monoidal, compute $!$ , and write out $contr$ and $weak$ explicitly. Then check the comonoid laws on a two-element set.

Referenced from 3 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.8 ¶

★★★ Prove the claim made in section 159.7 that $FS (S)$ admits no trace operator satisfying the usual naturality and vanishing axioms, by using the normal form of theorem 159.12 to show that every arrow’s generator occurrences lie on directed paths from inputs to outputs.

Referenced from 2 locations

Symmetric Monoidal Categories and Graphical Linear Semantics

Exercise 159.9 — Practical: a typed diagram normalizer ¶

★★★ Practical project.monoidal-diagram-normalizer Implement diagrams over a finite typed signature as in definition 159.14: boxes with typed ports, a wiring, and free input and output lists. The program must check well-formedness — every port wired exactly once, types matching, the box graph acyclic — compute the normal form of theorem 159.12, and decide equality of two diagrams by comparing normal forms. The invariant the program must maintain is that it never identifies two diagrams whose normal forms differ, and never distinguishes two that differ only by the port bijection allowed in definition 159.14. The program must print, for each named input, the well-formedness verdict with the violated clause named on failure, the normal form as a sequence of generator layers with its permutations, and an equality verdict for a pair. The acceptance test is: the file program of example 159.22 is accepted and its normal form has three generator layers in the order $open, read, close$ ; the variant that omits the $close$ box is rejected with the unwired-port clause named; the two sides of one hexagon from exercise 159.4 normalize to the same form; and two diagrams differing only by exchanging two boxes on disjoint wires are reported equal, matching the uniqueness clause of theorem 159.12. A normalizer for finite diagrams is evidence on named inputs only: it proves neither theorem 159.12 nor theorem 159.15, and it says nothing about non-free monoidal categories.

Referenced from 3 locations