nLab Trimble rewiring

Idea

So-called Trimble rewiring refers to a certain type of transformation on graphs which were introduced in Trimble’s thesis, intended to refine Kelly-Mac Lane graphs or classical proof nets in multiplicative linear logic so as to capture properties of the monoidal unit in symmetric closed monoidal categories. These unit-extended proof nets may be interpreted as morphisms in free symmetric monoidal closed categories, and it turns out that two unit-extended proof nets are interpretable as the same morphism if and only if they are “rewiring equivalent”.

Rewirings can be organized into a confluent and strongly normalizing rewrite system, where a rewrite called “directed rewiring”. The normal forms of graphs can then be used to state a full coherence theorem, extending the coherence theorem of Kelly and Mac Lane for symmetric monoidal closed categories.

The concept of rewiring equivalence extends to weakly distributive categories and $\ast$-autonomous categories as well, and likewise is used to give coherence theorems for these structures.

Definition

(For now this is just the very rough idea. More details to come.)

Recall from proof net the notion of (cut-free) proof structure and the notion of (cut-free) proof net (a proof structure of the form $S(\pi)$ where $\pi$ is a sequent proof).

Definition

A unit-extended proof structure of type $\Delta \to B$ is a proof structure of type $\Delta \to B$ equipped with a function $u: Unit^-(\Delta^-, B^+) \to Subform(\Delta^-, B^+)$ from the set of negatively signed subformula occurrences of $I$ to the set of subformulas of $\Delta$ and $B$.

We draw such a unit-extended proof structure as a graph: the graph of the proof structure together with an edge from each occurrence $R$ of $I^-$ to $u(R)$. We think of this unit edge as connoting a subterm of the form $r t$, where $r$ is a variable term of type $I$ (a “scalar”), and $t$ is a term of type $u(R)$.

Let $UStruct(\Delta, B)$ denote the set of unit-extended proof structures of type $\Delta \to B$, and let $Proof(\Delta, B)$ denote the set of sequent proofs of the sequent $\Delta \vdash B$. We define a relation from $Proof(\Delta, B)$ to $UStruct(\Delta, B)$, i.e., a function

$$Proof(\Delta, B) \to P(UStruct(\Delta, B))$$

by induction along the sequent proof, as follows. (Details to be filled in. The most important sequent rule to consider is

$$\Gamma(\frac{\displaystyle \pi: \Delta, \Sigma \vdash A}{\displaystyle \Delta, I, \Sigma \vdash A}\; unit_{-})$$

where a related unit-extended proof net is obtained from a proof net for $\pi$ by introducing a fresh unit edge from the occurrence of $I^-$ introduced in the last step to any subformula of $\Delta, \Sigma \vdash A$. The other rules are straightforward.)

Definition

A unit-extended proof net is a proof structure that is related to some sequent deduction.

Theorem on graphical criterion for a unit-extended proof structure to be a unit-extended proof net, similar to the criterion of Danos-Regnier.

Definition

Two unit-extended proof nets $\gamma, \gamma'$ of type $\Delta \to B$ are rewiring-equivalent if there is a sequence of unit-extended proof nets $\gamma = \gamma_0, \gamma_1, \ldots, \gamma_n = \gamma'$ of type $\Delta \to B$ such that each successive pair of graphs $\gamma_i, \gamma_{i+1}$ differ only by a single unit edge $u(R)$.

Theorem that two sequent proofs $\pi, \pi'$ produce the same morphism in the free smc category $V[T]$ iff any two of their unit-extended proof nets $\gamma, \gamma'$ are rewiring-equivalent.

Notion of directed rewiring…

References

• Todd Trimble, Linear logic, bimodules, and full coherence for autonomous categories. PhD thesis, Rutgers University, 1994

• Max Kelly, Saunders MacLane, Coherence in closed categories, JPAA 1 (1971), 97-140 (web)

• Richard Blute, Robin Cockett, Robert Seely, Todd Trimble, Natural deduction and coherence for weakly distributive categories, JPAA 113 (1996), 229-296. (web)