Skip to Main content Skip to Navigation
Conference papers

Functorial boxes in string diagrams

Abstract : String diagrams were introduced by Roger Penrose as a handy notation to manipulate morphisms in a monoidal category. In principle, this graphical notation should encompass the various pictorial systems introduced in proof-theory (like Jean-Yves Girard's proof-nets) and in concurrency theory (like Robin Milner's bigraphs). This is not the case however, at least because string diagrams do not accomodate boxes -- a key ingredient in these pictorial systems. In this short tutorial, based on our accidental rediscovery of an idea by Robin Cockett and Robert Seely, we explain how string diagrams may be extended with a notion of functorial box to depict a functor separating an inside world (its source category) from an outside world (its target category). We expose two elementary applications of the notation: first, we characterize graphically when a faithful balanced monoidal functor C -> D transports a trace operator from the category D to the category C, and we then exploit this to construct well-behaved fixpoint operators in cartesian closed categories generated by models of linear logic; second, we explain how the categorical semantics of linear logic induces that the exponential box of proof-nets decomposes as two enshrined functorial boxes.
Complete list of metadatas

Cited literature [49 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00154243
Contributor : Paul-André Melliès <>
Submitted on : Wednesday, June 13, 2007 - 9:54:17 AM
Last modification on : Saturday, March 28, 2020 - 2:13:15 AM
Document(s) archivé(s) le : Friday, September 21, 2012 - 4:26:10 PM

File

functorial-boxes-2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Paul-André Melliès. Functorial boxes in string diagrams. Computer Science Logic 2006, Sep 2006, Szeged, Hungary. pp.1-30, ⟨10.1007/11874683⟩. ⟨hal-00154243⟩

Share

Metrics

Record views

494

Files downloads

1578