*Higher-Dimensional Rewriting and Algebra*

4th edition of the workshop

July 7, 2018, Oxford, United Kingdom

Satellite workshop of FSCD 2018, part of FLOC 2018.

## Overview

Rewriting consists in orienting equalities. This seemingly simple point of
view has given rise to a rich theory, which was first developped in
computer science for handling strings and terms, and was then extended
over the recent years to many other settings (operads, monoidal
categories, higher categories, etc.), allowing it to have applications in
algebra, homotopy theory and physics. All these generalizations fit into
the general scope of *higher-dimensional rewriting theory*, which has
emerged as a unifying algebraic framework.

The aim of the workshop is to gather people interested in pushing further rewriting theory, using (higher) category theory as a common language. It is open to all topics concerning higher-dimensional generalizations and applications of rewriting theory, including

*higher-dimensional rewriting*: extensions of rewriting theory to higher-dimensional settings (operads, opetopes, polygraphs/computads, parity complexes, augmented directed complexes, etc.), generalizations of string/term/graph rewriting systems, etc.*higher categorical structures*: weakening, combination and comparison of categorical structures (monoids, bialgebras, Frobenius algebras, Lie algebras, etc.), coherence theorems, etc.*applications of rewriting to algebraic topology*: construction of resolutions, homotopical and homological invariants, linear rewriting (Gröbner bases, applications to algebras and operads), Koszul duality theory, etc.*applications and interactions with other fields*: calculi for quantum computations, proof nets, algebraic lambda-calculi, topological models for concurrency, homotopy type theory, combinatorial group theory, etc.*implementations*: the workshop will also be interested in implementation issues in higher-dimensional rewriting and will allow demonstrations of prototypes of existing and new tools in higher-dimensional rewriting.

## Invited Speakers

- Paige North (Ohio State University), joint with HoTT/UF,
- Emily Riehl (Johns Hopkins University).

## Programme

**9:00–10:00**: invited talk by Emily Riehl, *Homotopy coherent adjunctions and other structures*

Naturally occurring diagrams in algebraic topology are commutative up to homotopy, but not on the nose. It was quickly realized that very little can be done with mere “homotopy commutativity." Homotopy coherent category theory arose out of a desire to catalog the higher homotopical information required to restore constructibility (or more precisely, functoriality) in such "up to homotopy" settings. In this talk we’ll focus on the syntactic categories that index homotopy coherent diagrams, which must satisfy a “freeness” or “cofibrancy” property that we axiomatize under the name “simplicial computads.” We then present as many explicit examples as time permits, including Dwyer-Kan free resolutions (which define the shape of a homotopy coherent diagram indexed by a 1-category), the homotopy coherent simplices (which are special cases), and the homotopy coherent realization of a simplicial set (a common generalization of these notions). A final example is given by the free homotopy coherent adjunction, a simplicial computad supported by a convenient graphical calculus developed in joint work with Dominic Verity.

**10:00–10:30**: Amar Hadzihasanovic, *Merge-bicategories: towards semi-strictification of higher categories*

A 2-polygraph is regular if its 2-cells have non-degenerate, “interval-shaped” input and output boundaries. A merge-bicategory is a regular 2-polygraph with an algebraic composition of 2-cells, where the composable diagrams are the “disk-shaped” ones. A merge-bicategory is representable if it contains enough “divisible” 1-cells and 2-cells, satisfying certain universal properties. I will show that representable merge-bicategories and morphisms that preserve divisible cells are equivalent to bicategories and (pseudo)functors; through a natural monoidal biclosed structure on merge-bicategories, one can also recover higher morphisms. I will use this to develop a semi-strictification argument for bicategories, combining the explicit combinatorial aspects of string-diagram based coherence proofs, with the main features of Hermida's abstract proof based on representable multicategories. All the constructions can be generalised to higher dimensions: I will sketch how this could lead to semi-strictification (excluding weak units) for higher categories, where it is still an open problem.

**10:30–11:00**: *break*

**11:00–11:30**: Cédric Ho Thanh, *The equivalence between opetopic sets and many-to-one polygraphs*

From the polynomial approach to the definition of opetopes of Kock et al., we derive a category of opetopes, and show that its Set-valued presheaves, or opetopic sets, are equivalent to many-to-one polygraphs. As an immediate corollary, we establish that opetopic sets are equivalent to multitopic sets, introduced and studied by Makkai et al..

**11:30–12:00**: Pedro Tamaroff, *Minimal models for monomial algebras*

Using combinatorics of chains going back to works of Anick, Green, Happel and Zacharia, we give, for any monomial algebra A, an explicit description of its minimal model. This also provides us with formulas for a canonical A-infinity-structure on the Ext-algebra of the trivial A-module.

**12:00–12:30**: Benjamin Dupont, *Termination in linear (2,2)-categories with braidings and duals*

This work is part of a research project aiming at developing rewriting methods to study diagrammatic algebras. In particular, we are interested in this work to diagrammatic algebras which can be seen as linear (2,2) categories with an additional structure, for instance given by braidings, adjunctions or duals. We present new termination heuristics for linear (3,2)-polygraphs presenting these linear (2,2)-categories based on the definition of an order similar to a monomial order, but that is not required to be total. This order is defined by counting the generators on the diagrams, and finding characteristics which are stable by contexts. We illustrate these methods by proving termination of a particular linear (3,2)-polygraph presenting a candidate 2-category for categorifying a quantum group.

**12:30–14:00**: *lunch*

**14:00–15:00**: invited talk by Paige North (joint with HoTT/UF), *TBA*

TBA

**15:30–15:30**: Thibaut Benjamin, *Towards a fully formalized definition of syllepsis in weak higher categories*

The aim of this presentation is to illustrate the use of formal methods in order to reason in the theory of weak mega-categories. The formalism considered here is based on the type theory CaTT introduced by Finster and Mimram, extended with some metatheory on top of it, with an implementation We first present how the system works and can be used, and then develop some "real-world" examples, such as the definition of the braidings in k-tuply monoidal omega-categories (following the terminology of Baez), k≥2, with the aim of showing that we have a syllepsis in the case k≤3. These developments have motivated metatheoretical improvements to the proof assistant, which we also present and discuss here, in order to handle and partly automate large proofs.

**15:30–16:00**: *break*

**16:00–16:30**: Richard Statman, *Minimal Bacus FP is Turing Complete*

In his 1977 Turing Award address, John Backus introduced the model of functional programming called "FP". FP is a descendant of the Herbrand-Godel notion of recursive definablity and the ancestor of the programming language Haskell. One reason that FP is attractive is that it provides "an algebra of functional programs" However, Backus did not believe that basic FP was powerful enough; "FP systems have a number of limitations..... If the set of primitive functions and functional forms is weak, it may not be able to express every computable function." and he moved on to stronger systems. It turns out that, in this respect, Backus was mistaken. Here we shall show that FP can compute every partial recursive function. Indeed we shall show that FP can simulate the behavior of an arbitrary Turing machine. Our method for doing this is the following. We first observe that the equational theory of Cartesian monoids is a fragment of FP. Cartesian monoids are rather simple algebraic structures of which you know many examples. They also travel under many assumed names such as Cantor algebras, Jonsson-Tarski algebras, and Freyd-Heller monoids. This theory, together with fixed points for all Cartesian monoid polynomials, is contained in FP. Now Cartesian monoids with fixed points can be studied using rewrite techniques, learned from lambda calculus, including confluence and standarization. Turing machines can then be simulated; transitions corresponding to fixed points and computations corresponding to standard reductions to normal form.

**16:30–17:00**: Nohra Hage, *String data structures for Chinese monoids*

The structure of Chinese monoid appeared in the classification of monoids with the growth function coinciding with that of the plactic monoid. In this work, we deal with the presentations of the Chinese monoid from the rewriting theory perspective using the notion of string data structures. We define a string data structure associated to the Chinese monoid using the insertion algorithm on Chinese staircases. As a consequence, we construct a finite semi-quadratic convergent presentation of the Chinese monoid and we extend it into a finite coherent presentation of this monoid.

**17:00–17:30**: Cyrille Chenavier, Christophe Cordero and Samuele Giraudo, *Generalizations of the associative operad and convergent rewrite systems*

The associative operad is the quotient of the magmatic operad by the operad congruence identifying the two binary trees of degree 2. We introduce here a generalization of the associative operad depending on a nonnegative integer d, called d-comb associative operad, as the quotient of the magmatic operad by the operad congruence identifying the left and the right comb binary trees of degree d. We study the case d=3 and provide an orientation of its space of relations by using rewrite systems on trees and the Buchberger algorithm for operads to obtain a convergent rewrite system.

**17:30–18:00**: Antonin Delpeuch and Jamie Vicary, *Normal forms for planar connected string diagrams*

In the graphical calculus of planar string diagrams, equality is generated by the
left and right exchange moves, which swaps the heights of adjacent vertices. We
show that for connected diagrams the left- and right-handed exchanges each give
strongly normalizing rewrite strategies. We show that these strategies terminate
in O(n^{3}) steps where n is the number of vertices. We also give an algorithm to
directly construct the normal form, and hence determine isotopy, in O(n×m) time,
where m is the number of edges.

## Venue

See FLOC's webpage.

## Important Dates

- Paper Submission: April 20, 2018
- Notification of Acceptance: May 10, 2018
- Final version: May 21, 2018
- Conference:
**July 7, 2018**

## Organization Committee

- Yves Guiraud (INRIA, Université Paris 7)
`yves.guiraud(@)irif.fr` - Philippe Malbos (Université Claude Bernard Lyon 1)
`malbos(@)math.univ-lyon1.fr` - Samuel Mimram (École Polytechnique)
`samuel.mimram(@)lix.polytechnique.fr`

## Program Committee

- Yves Guiraud (INRIA, Université Paris 7)
- Philippe Malbos (Université Claude Bernard Lyon 1)
- Paul-André Melliès (Université Paris Diderot)
- Samuel Mimram (École Polytechnique)
- Tim Porter
- Femke van Raamsdonk (VU University, Amsterdam)
- Pawel Sobocinski (University of Southampton)
- Jamie Vicary (University of Oxford)