Graphical and diagrammatic notations for logic and computation (proof nets, string diagrams, existential graphs, Petri nets, interaction nets, etc.) provide elegant, often canonical representations of proofs and processes that expose structure hidden in linear symbolic presentations. These representations have proven valuable both for foundational questions (identity of proofs, cut-elimination as rewriting, semantics of proofs/programs) and practical concerns (visual proof editors, automated graph rewriting, program compilation and optimisation).
The workshop aims at bringing together researchers with complementary perspectives on the topic—ranging from applied category theory and proof theory to the philosophy of diagrammatic reasoning—in order to encourage collaboration, cross-pollinate ideas, share ongoing work, and allow newcomers to explore current developments in the field.
We welcome contributions on all aspects of diagrams in logic and computation. A non-exhaustive list of topics includes:
All deadlines are AoE - Anywhere on Earth (UTC-12).
The concept of ‘syntax’ is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call ‘terms’. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei.
Most of the material I will discuss is based on the recent tutorial paper “Hierarchical string diagrams and applications” jointly with Fabio Zanasi (https://arxiv.org/abs/2305.18945) about to appear as a CUP monograph.
The objective of this work-in-progress is to give a construction of free symmetric monoidal closed (SMClosed) categories in the form of a graphical calculus based on monoidal substitution diagrams. Our work differs from previous constructions in a certain technical sense (strictness), but it is also quite different in look and feel. As we will show, there is a certain way to read monoidal substitution diagrams that lends a unique visual intuition to an otherwise thorny structure.
Instead of the traditional mathematical formulae for objects of an SMClosed category (e.g. A ⊗ B, C ⊸ D, (E ⊗ F) ⊸ G), our calculus uses labeled directed acyclic graphs called monoidal dependency graphs. There are procedures that translate in both directions between monoidal dependency graphs and the traditional formulae.
In our calculus, morphisms are represented by labeled directed acyclic graphs called monoidal substitution diagrams. A monoidal substitution diagram is produced by augmenting a monoidal dependency graph with extra edges that link together pairs of nodes that share the same label.
This is an abstract for a paper in preparation, soon to appear on arXiv.
Fermionic quantum computing offers an alternative to the standard qubit-based model, in which information is encoded in the occupancy of fermionic modes possibly containing indistinguishable particles that obey Fermi-Dirac statistics. The algebraic structure of such systems, captured by Canonical Anticommutation Relations (CAR) algebras, naturally leads to a premonoidal categorical semantics, reflecting the failure of the exchange law due to the antisymmetry of fermions. Permutation of two fermionic modes in Bravyi-Kitaev's model can be performed through the fermionic swap, which makes this categorical semantics a symmetric premonoidal category. While this structure corresponds to the underlying denotational semantics of Bravyi and Kitaev's early computational model, it is ill-suited for circuit manipulation, as premonoidal categories lack the exchange law enabling intuitive diagrammatic reasoning.
In this work, we address this challenge by embedding the symmetric premonoidal category of fermionic processes into a presymmetric monoidal category via a functor defined using the Jordan-Wigner mapping. Interestingly, this functor does not map the fermionic swap to a symmetry for the Qubit category equipped with the usual tensor product, due to a default of naturality. This allows us to recover a setting where diagrammatic syntax is more reasonable—the categories involved are monoidal categories, and more specifically props, equipped with a non-natural symmetry given by the image of the fermionic swap. We provide axiomatizations for these categories.
We present work in progress towards a combinatorial characterisation of first-order bicategories. These structures provide a categorical setting for studying first-order logic through a string-diagrammatic syntax. Unlike string diagrams for monoidal categories, those of first-order bicategories do not admit a straightforward combinatorial representation in terms of hypergraphs, due to two interacting monoidal structures. Developing such a representation is a necessary step towards a computationally feasible implementation of string diagram rewriting: structurally equivalent string diagrams can then be interpreted as the same hypergraph, substantially simplifying matching procedures.
Interaction nets are a form of graph rewriting, generalising the proof structures of multiplicative linear logic. Introduced as “a new kind of programming language”, they have rather been primarily applied in the optimal and efficient reduction of λ-calculus terms. More recently, the availability of multicore processors has renewed interest in interaction nets as a model of asynchronous parallel computation with emerging industrial implementations and active research languages.
Under their standard operational semantics, interaction nets do not have notions of input or output, and the evaluation result, if any, is its normal form. This creates a number of difficulties in formalising their use as a programming language. We reconsider interaction nets from Lafont’s original programming language perspective by adopting an observational view of semantics. Our contributions are:
This is a proposal for a talk concerning some technically easy yet little-known observations. The key concept is that of combinatorial map: discrete objects that correspond to topological embeddings of graphs on surfaces. Since the 2010s, they have made prominent appearances in the bijective and enumerative combinatorics of linear λ-terms. However, they are virtually never mentioned in conjunction with proof nets. My contention is that combinatorial maps:
We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and is sufficient for sequentialization in the fragment corresponding to the half-polarized typing system for call-by-push-value by Ehrhard.
In this talk, we will describe two different and equivalent diagrammatic ways to describe how effectful programs compose in a possibly non-associative way. The first formalism is a variant of functorial game semantics depicted in the 2-categorical language of string diagrams. The second formalism is based on sequential proof-nets, a new graphical representation of proofs with non-associative composition recently introduced by the three authors for the classical L-calculus.