Higher-Dimensional Rewriting and Applications

June 28-29, 2015, Warsaw, Poland
Co-located with RDP/RTA/TLCA 2015.


Over recent years, rewriting methods have been generalized from strings and terms to richer algebraic structures such as operads, monoidal categories, and more generally higher-dimensional categories. These extensions of rewriting fit in the general scope of higher-dimensional rewriting theory, which has emerged as a unifying algebraic framework. This approach allows one to perform homotopical and homological analysis of rewriting systems (Squier theory). It also provides new computational methods in combinatorial algebra (Artin-Tits monoids, Coxeter and Garside structures), in homotopical and homological algebra (construction of cofibrant replacements, Koszulness properties). The workshop is open to all topics concerning higher-dimensional generalizations and applications of rewriting theory, including

Invited Speakers


Sunday, June 28

9:00–10:00John BaezCategories in Control
10:30–11:15Jovana ObradovićThe Bénabou-Roubaud monadic descent theorem via string diagrams
11:15–11:30Short break
11:30–12:15Jason Morton and David SpivakA operad-based normal form for morphism expressions in a closed compact category
14:30–15:30Eugenia ChengLawvere theories and distributive laws
16:00–16:45Krzysztof Bar, Aleks Kissinger and Jamie VicaryGlobular: a proof assistant for semistrict higher rewriting
16:45–17:00Short break
17:00–17:45Eric FinsterOpetopic Diagrams and Higher Categorical Proof Theory

Monday, June 29

9:15–10:15Eugenia ChengLawvere theories and distributive laws
10:45–11:30Cyrille ChenavierConfluence algebras and acyclicity of the Koszul complex
11:30–11:45Short break
11:45–12:30Clément AlleaumeRewriting in the category of Bott-Samelson bimodules
14:30–15:30John BaezCircuits, categories, and rewrite rules
16:00–16:45Lucius Meredith and Mike StayHigher category models of the π-calculus
16:45–17:00Short break
17:00–17:45Aleks Kissinger and Jamie VicarySemistrict n-categories via rewriting


John Baez, Categories in Control

Control theory is the branch of engineering that studies dynamical systems with inputs and outputs, and seeks to stabilize these using feedback. Control theory uses "signal-flow diagrams" to describe processes where real-valued functions of time are added, multiplied by scalars, differentiated and integrated, duplicated and deleted. In fact, these are string diagrams for the symmetric monoidal category of finite-dimensional vector spaces, but where the monoidal structure is direct sum rather than the usual tensor product. Jason Erbele has given a presentation for this symmetric monoidal category, which amounts to saying that it is the PROP for bicommutative bimonoids with some extra structure.

A broader class of signal-flow diagrams also includes "caps" and "cups" to model feedback. This amounts to working with a larger symmetric monoidal category where objects are still finite-dimensional vector spaces but the morphisms are linear relations. Erbele also found a presentation for this larger symmetric monoidal category. It is the PROP for a remarkable thing: roughly speaking, an object with two special commutative dagger-Frobenius structures, such that the multiplication and unit of either one and the comultiplication and counit of the other fit together to form a bimonoid.

Eugenia Cheng, Lawvere theories and distributive laws

Lawvere Theories and monads are two ways of handling algebraic theories. They are related but subtly different; one way in which they differ is that models for a given Lawvere Theory can automatically be taken in many different base categories, whereas monads have a fixed base category. Distributive laws give a way of combining two algebraic structures expressed as monads, so one might naturally ask whether something analogous can be done for Lawvere Theories; in fact Benabou asked me this after I had given a talk on distributive laws for monads. In this series of two talks I will discuss three ways of doing this which are equivalent but provide different points of view, arising from three different approaches to Lawvere Theories. In the first talk I will cover background as desired by the audience, on Lawvere Theories, distributive laws, or both.

Jovana Obradović, The Bénabou-Roubaud monadic descent theorem via string diagrams

Due to the technically complicated calculations involving Grothendieck's cocycle condition, the categorical equivalence encompassed by the Bénabou-Roubaud theorem is usually not worked out in complete detail in the literature. We give a complete proof of the Bénabou-Roubaud theorem in the language of string diagrams. Indeed, we notice that this proof essentially deals with constructing natural transformations and rewriting them (the latter requiring an alert bookkeeping action), i.e. that it (presumably) constitutes a suitable environment to make the most of the string diagrammatic approach (primarily of its "free" bookkeeping virtue). We link the monadic and the original viewpoint via another possible definition of the category of descent data. This intermediate step involves constructions in internal categories and it provides an interesting illustration on how can one stay in the world of string diagrams even when dealing with morphisms which do not have an explicit string diagram definition. We start by representing Grothendieck's cocycle condition in the special case of the basic fibration of a category, and we ultimately show how should our arguments be "lifted" in order to derive the proof for the general case of an arbitrary fibration.

Cyrille Chenavier, Confluence algebras and acyclicity of the Koszul complex

The N-Koszul algebras are N-homogeneous algebras which satisfy a homological property. These algebras are characterised by their Koszul complex: an N-homogeneous algebra is N-Koszul if and only if its Koszul complex is acyclic. Methods based on computational approaches were used to prove N-Koszulness: an algebra admitting a side-confluent presentation is N-Koszul if and only if the extra-condition holds. However, in general, these methods do not provide an explicit contracting homotopy for the Koszul complex. We present a way to construct such a contracting homotopy. The property of side-confluence enables us to define specific representations of confluence algebras. These representations provide a candidate for the contracting homotopy. When the extra-condition holds, it turns out that this candidate works.

Jason Morton and David Spivak, A operad-based normal form for morphism expressions in a closed compact category

We consider the linked problems of (1) finding a normal form for morphism expressions in a closed compact category and (2) the word problem, that is deciding if two morphism expressions are equal up to the axioms of a closed compact category. These are important ingredients for a practical monoidal category computer algebra system. Previous approaches to these problems include rewriting and graph-based methods. Our approach is to re-interpret a morphism expression in terms of an operad, and thereby obtain a single composition which is strictly associative and applied according to the abstract syntax tree. This yields the same final operad morphism regardless of the tree representation of the expression or order of execution, and solves the normal form problem up to automorphism.

Clément Alleaume, Rewriting in the category of Bott-Samelson bimodules

The category of Bott-Samelson bimodules is a category studied in representation theory introduced by Soergel. Elias and Williamson introduce a diagrammatic language to present it by generators and relations. Our objective is to compute by rewriting methods relations between relations. For this, we introduce in this work (3,2)-linear polygraphs to take the structure of this category, which is monoidal with a vector space structure on its morphism spaces into account. New difficulties arise from this object. Termination is harder to prove and local confluence has a more restrictive criterion.

John Baez, Circuits, categories, and rewrite rules

We describe a category where a morphism is an electrical circuit made of resistors, inductors and capacitors, with marked input and output terminals. In this category we compose morphisms by attaching the outputs of one circuit to the inputs of another. There is a functor called the "black box functor" that takes a circuit, forgets its internal structure, and remembers only its external behavior. Two circuits have the same external behavior if and only if they impose same relation between currents and potentials at their terminals. This is a linear relation, so the black box functor goes from the category of circuits to the category of finite-dimensional vector spaces and linear relations. Constructing this functor makes use of Brendan Fong's theory of "decorated cospans" – and the question of whether two circuits map to the same relation has an interesting answer in terms of rewrite rules.

Lucius Meredith and Mike Stay, Higher category models of the π-calculus

We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the π-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an explicit interpretation of the rewrite rules of standard operational presentations as 2-morphisms. One of the key contributions, inspired by catalysis in chemical reactions, is a method of restricting the application of 2-morphisms interpreting rewrites to specific contexts.

Eric Finster, Opetopic Diagrams and Higher Categorical Proof Theory

We propose opetopic diagrams as a concrete method for studying problems in higher dimensional rewriting theory and demonstrate a prototype implementation of a system built for manipulating them.

Aleks Kissinger and Jamie Vicary, Semistrict n-categories via rewriting

We sketch an approach to semistrict n-categories, in which interchangers and other weak structures are expressed as a coinductively-generated rewriting system on an ∞-globular set. We give diagrammatic depictions of some of the resulting structures, and show that we recover strict bicategories in dimension 2, Gray categories in dimension 3, and in a degenerate case, symmetric strict monoidal categories in dimension 4.

Krzysztof Bar, Aleks Kissinger and Jamie Vicary, Globular: a proof assistant for semistrict higher rewriting

This article is a progress report on Globular, an online proof assistant for semistrict higher-dimensional rewriting. We aim to produce a tool which can visualize higher-dimensional categorical diagrams, assist in their construction with a point-and-click interface, perform type checking to prevent incorrect composites, and automatically handle the interchanger data at each dimension. Hosted on the web, it will have a low barrier to use, and allow hyperlinking of formalized proofs directly from research papers. We outline the theoretical basis for the tool, and describe the challenges we have overcome in its design.


The events on Sunday, June 28 will take place at Faculty of Mathematics, Informatics and Mechanics, Banacha 2 while those on weekday days at CeNT II (Facylty of Physics), ul. Pasteura 5. These buildings are one opposite to the other and are marked on the map of the venue:

Organization Committee

Program Committee