Talks
- "Extensions of the Todd-Coxeter algorithm via automata theory"
-
Contributed Talk: SAMSA Workshop 2026Warsaw, Poland, June 2026
Abstract
The well known Todd-Coxeter algorithm is widely used to construct transformation representations of finitely presented monoids. It can be seen, in some sense, as computing the direct limit of a sequence of semiautomata approximating the right Cayley graph of the underlying monoid. This algorithm can also be used for finitely presented groups and, perhaps more surprisingly, there exists an analogue of the Todd-Coxeter algorithm for inverse monoids due to J. B. Stephen (1987). This is despite the fact that the free inverse monoid is not finitely presented as a monoid. Could it be possible to extend the Todd-Coxeter algorithm to other classes of monoids, such as finitely based varieties of monoids?
In this talk I will briefly describe a category theory based approach to modeling the Todd-Coxeter algorithm and I will present an extension of the Todd-Coxeter algorithm to presentations in finitely based varieties of monoids, motivated by a recent NL-space algorithm for deciding if a monoid identity is modelled by a given finitely generated transformation monoid due to L. Fleisher and T. Jack (2020).
- "Certifying the decidability of the word problem in monoids, at large"
-
Conference Talk: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '26)Rennes, France, January 2026
Abstract
While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large monoids from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations upon the Rocq formalization, so that its formal proof could be checked in a reasonable amount of time.
- "Off with the head! Termination provers and the word problem for 1-relation monoids"
-
Conference Talk: 20th International Workshop on TerminationLeipzig, Germany, September 2025
Abstract
In this talk I will showcase a new set of SRS termination problems arising from the word problem in 1-relation monoids. The word problem is a central object of study in combinatorial semigroup theory. Despite being undecidable in general, its decidability is open when restricted to 1-relation monoids. Motivated by recent efforts in solving this problem, we launched a quantitative investigation with the goal of formally proving as many small instances of the 1-relation monoid word problem as possible. This naturally lead us to utilize termination provers to solve SRS arising from many challenging instances.
This is joint work with Florent Hivert (Université Paris Saclay), Assia Mahboubi (Nantes Université), Guillaume Melquiond (Université Paris Saclay), James D. Mitchell (University of St Andrews) and Finn L. Smith (University of St Andrews).
- "Maximal one-sided congruences of full transformation monoids"
-
Conference Talk: Semigroups Day VISt Andrews, United Kingdom, June 2025
Abstract
In 1952 Mal’cev showed that the two-sided congruences of a full transforma- tion monoid form a chain. It is now 2025, more than half a century later, and we have almost no idea of what the right or left congruence lattice of the full transformation monoids looks like. What gives!? In this talk, aiming to improve the situation somewhat, I will attempt to give a description of the maximal one-sided congruences of the full transformation monoid.
Joint work with Dr Yann Peresse (University of Hertfordshire) and Prof. James D. Mitchell.
- "Computing finite-index congruences"
-
Contributed Talk: 75th British Mathematical ColloquiumManchester, United Kingdom, June 2024
Abstract
Finitely presented semigroups are computationally intractable. Even the simplest problems, such as checking if a f.p. semigroup is trivial, are undecidable. Finite semigroups on the other hand are rather amenable to computational stufy. In this talk we introduce an algorithm for computing finite-index congruences of f.p. monoids. This effectively allows us to perform computational analysis of the original, possibly infinite semigroup, by considering its images into finite semigroups, allowing for much more effective semidecision of many intractable problems.
This is joint work with M. Anagnostopoulou-Merkouri, J. D. Mitchell and M. Tsalakou. The algorithms presented are implemented in the libsemigroups C++ library.
- "Computing in free bands"
-
Seminar talk: York Semigroup seminarYork, United Kingdom, November 2023
Abstract
A band is a semigroup whose elements are all idempotent. Perhaps surprisingly, it turns out that all finitely generated bands are finite. Despite this, existing methods for computing with finite or finitely generated semigroups, such as the Todd-Coxeter and Knuth-Bendix algorithms, are inefficient or inapplicable to bands. In this talk we will focus on the special case of free bands and showcase a way of solving the word problem and computing minimal representatives by using coloured binary trees.
- "Making the Knuth-Bendix algorithm exponentially slower"
-
Contributed talk: Semigroups DaySt Andrews, United Kingdom, June 2023
Abstract
The Knuth-Bendix algorithm takes as input a semigroup presentation and, if the algorithm terminates, produces a complete rewriting system and hence a solution to the word problem. But what can we do in cases where the algorithm does not seem to terminate? In this talk we will utilize termination provers to augment the Knuth-Bendix algorithm with a backtrack search. We will then apply this new version of the algorithm to solve hard instances of the one relation monoid word problem. This is joint work with prof. James Mitchell and Finn Smith.