June 25-26, 2016, Porto, Portugal
Co-located with FSCD 2016.
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
|9:00–10:00||Gérard Huet||FSCD keynote|
|10:30–11:15||Jamie Vicary||Coherence for swallowtailators and Frobenius pseudomonoids|
|11:30–12:15||Amar Hadzihasanovic||A topological perspective on interacting algebraic theories|
|14:00–15:00||Michael Batanin||Formal theory of operadic categories and operads|
|15:15–16:00||Nachum Dershowitz, Jean-Pierre Jouannaud and Jian-Qi Li||Well founded Path Orderings for Drags|
|16:30–17:15||Nohra Hage||Column presentations of plactic monoids|
|9:00–10:00||Pawel Sobocinski||Circuits, diagrams, (graphical) linear algebra and control theory|
|10:30–11:15||Maxime Lucas||A Cubical Squier's Theorem|
|11:30–12:15||Cyrille Chenavier||Reduction Operators: Rewriting Properties and Completion|
|14:00–15:00||Joachim Kock||Open graphs and hypergraphs|
|15:15–16:00||Lars Hellström||Ordered and Combinatorial Structures for Higher-Dimensional Rewriting|
|16:30–17:15||Clément Alleaume||Completion method in higher dimensional polygraphs|
In this note, we introduce a generalization of Knuth-Bendix's procedure for higher dimensional polygraphs. We discuss of when this procedure does not fail and when it gives us a confluent (n+1)-polygraph. We give an example of application of this procedure to topological rewriting.
We propose an approach on abstract rewriting where applications of rewriting rules are replaced by applications of specific linear maps, called reduction operators relative to a well-ordered set. This notion extends the one introduced by Berger who considered reduction operators relative to totally ordered finite sets. We equip the set of reduction operators with a lattice structure. We use this structure to define a notion of confluence. We formulate the Church-Rosser property for reduction operators, the notion being equivalent to the one of confluence. The lattice structure also enables us to give an algebraic status to the completion. This completion provides a way to construct Gröbner bases using reduction operators.
The definition herein of the Graph Path Ordering (GPO) on certain graph expressions is inspired by that of the Recursive Path Ordering (RPO), and enjoys all those properties that have made RPO popular, in particular, well-foundedness and monotonicity on variable-free terms. We are indeed interested in a generalization of algebraic expressions called operadic expressions, which are finite graphs each vertex of which is labelled by a function symbol, the arity of which governs the number of vertices it relates to in the graph. These graphs are seen here as terms with sharing and back-arrows. Operadic expressions are themselves multiplied (an associative operation) to form monomials, which are in turn summed up (an associative commutative operation) to form polynomials. Operadic expressions and their polynomials occur in algebraic topology, and in various areas of computer science, notably concurrency and type theory. Rewriting basic operadic expressions is very much like rewriting algebraic expressions, while rewriting their monomials and polynomials is very much like the Groebner basis theory. GPO provides an initial building block for computing with operadic expressions and their polynomials.
The structure of plactic monoid appears in numerous areas of algebra and representation theory. In this note, we study presentations of plactic monoids for any semisimple Lie algebra by rewriting methods. A presentation of these monoids was introduced by Littelmann using the Lakshmibai--Seshadri paths. Thanks to the shapes of standard tableaux, we show that this presentation is finite and convergent. The latter presentation called the column presentation is a first step to construct resolutions of these monoids and to compute their homological invariants.
Techniques from higher categories and higher-dimensional rewriting are becoming increasingly important for understanding the finer, computational properties of higher algebraic theories that arise, among other fields, in quantum computation. These theories have often the property of containing simpler sub-theories, whose interaction is regulated in a limited number of ways, which reveals a topological substrate when pictured by string diagrams. By exploring the double nature of computads as presentations of higher algebraic theories, and combinatorial descriptions of "directed spaces", we develop a basic language of directed topology for the compositional study of algebraic theories. We present constructions of computads, all with clear analogues in standard topology, that capture in great generality such notions as homomorphisms and actions, and the interactions of monoids and comonoids that lead to the theory of Frobenius algebras and of bialgebras. After a number of examples, we sketch how a fragment of the ZX calculus, the theory of interacting bialgebras, can be reconstructed in this framework.
We explore the toolbox of ordered and combinatorial structures that are used to guide and control higher-dimensional rewriting.
I will explain a categorical formalism for open graphs and hypergraphs in which gluings and substitutions can be described in terms of colimits.
Starting from a convergent presentation of a Monoid, Squier's homotopical Theorem constructs a set of syzygies, or relations between the relations. This construction was later extended into the construction of a polygraphic resolution of the monoid. However, the construction of the polygraphic resolution has proved to be too complicated to be effectively computed on non-trivial examples. Cubical categories appear to be a promising framework where Squier's theorem and the construction of the polygraphic resolution would be more straightforward. In this paper, we express and prove a cubical version of Squier's Theorem, achieving the first step of this goal.
We prove a coherence result for swallowtailators, and use it to prove a coherence result for Frobenius pseudomonoids. This is an extended abstract for Section 4 of arXiv:1601.05372.
Submission should consist in an extended abstract, in pdf format, approximatively 6 pages long, in standard article format. The submissions should be uploaded through the Easychair site.
See the FSCD 2016 webpage.