nLab
Trimble rewiring

Contents

Context

Category theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

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(π)S(\pi) where π\pi is a sequent proof).

Definition

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

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

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

Proof(Δ,B)P(UStruct(Δ,B))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

Γ(π:Δ,ΣAΔ,I,ΣAunit )\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 I^- introduced in the last step to any subformula of Δ,ΣA\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 ΔB\Delta \to B are rewiring-equivalent if there is a sequence of unit-extended proof nets γ=γ 0,γ 1,,γ n=γ\gamma = \gamma_0, \gamma_1, \ldots, \gamma_n = \gamma' of type ΔB\Delta \to B such that each successive pair of graphs γ i,γ i+1\gamma_i, \gamma_{i+1} differ only by a single unit edge u(R)u(R).

Theorem that two sequent proofs π,π\pi, \pi' produce the same morphism in the free smc category V[T]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

Last revised on February 6, 2014 at 11:44:59. See the history of this page for a list of all contributions to it.