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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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.