Central groupoids

Stream: Equational

[Bhavik Mehta]

One equation which may come up is (xy)(yz) = y, since it contains three multiplications. This is the equation defining so-called "central groupoids", and has been studied - among other places - in a note by Knuth (Notes on Central Groupoids) in 1970. For instance, finite magmas satisfying this equation must have a square number of elements.
I have a formalisation of the majority of this paper (all of it except for parts of sections 4 and 7), but the equations in sections 5 and 6 are particularly interesting from an equational logic point of view. If some part of this is deemed relevant, I can make a PR to the repo. Unfortunately some of the more interesting results in section 6 are conditioned on a more complex expression (x((yz)w)) (zw) = z or two equations.

[Terence Tao]

Bhavik Mehta said:

One equation which may come up is (xy)(yz) = y, since it contains three multiplications. This is the equation defining so-called "central groupoids", and has been studied - among other places - in a note by Knuth (Notes on Central Groupoids) in 1970. For instance, finite magmas satisfying this equation must have a square number of elements.
I have a formalisation of the majority of this paper (all of it except for parts of sections 4 and 7), but the equations in sections 5 and 6 are particularly interesting from an equational logic point of view. If some part of this is deemed relevant, I can make a PR to the repo. Unfortunately some of the more interesting results in section 6 are conditioned on a more complex expression (x((yz)w)) (zw) = z or two equations.

This is equation 168 in the list. Given its interest, I will add it to the queue. I suppose it can't hurt to have some theorems about this equation in the repo.

[Bhavik Mehta]

It could be useful to have the fact about cardinality being a square, as it allows arguments of the form "equation X does not imply equation 168, as there is a finite magma of non-square size satisfying equation X". This works for a decent chunk of the existing equations actually, even with or on Bool. Although one could argue that a direct proof is easier, in these cases!

[Bhavik Mehta]

I've finished adapting this to the notation in the repo, and a draft PR is here: https://github.com/teorth/equational_theories/pull/492. This contains all the results I mentioned having proved above, as well as the fact that there are infinite central groupoids with no idempotents.

The construction for this is to give the confluent rewriting system for the central groupoid law, prove it is confluent and terminating, and thus normalising, and then deduce that there is no way in which x * x and x can be unified.

This same method should be usable - although I haven't worked out the details yet - to automatically prove every implication and nonimplication from 168: an implication is true iff the rewrite system normalises both sides to the same thing. (There's a slight hiccup in that the reduction as I've implemented it in this PR is not computable, although simp can implement it anyway... the method still works without computable reduction however).

I've also added the fact that a finite central groupoid of size n exists if and only if n is a square. In addition, Knuth's paper shows that equation 26302 is equivalent to being a natural central groupoid, which follows from my PR. Indeed, he shows that in the presence of equation 168, seven additional equations are equivalent, and each of these are further equivalent to the central groupoid being natural. My PR shows this as well. (I haven't yet figured out which numbers those seven are though!)

[Bhavik Mehta]

Finally I want to mention one of the many reasons I enjoy central groupoids: the question of showing that 26302 implies naturality (or more specifically, that 168 and 3915 imply 3522) is the reason Knuth invented the Knuth-Bendix algorithm.

It appears to be very difficult to derive (11) from (22), and initial attempts by the author to do this were unsuccessful. This provided the motivation to study more general problems of the same nature, and consequently the author developed an algorithm to work with identities in universal algebras (see [2])

[2] D. E. KNUTH AND P. B. BENDIX, Simple Word-Problems in Universal Algebras, in "Computational Problems in Abstract Algebra" (J. Leech, ed.), pp. 263-297, Pergamon, London/New York, 1969

[David Renshaw]

I noticed that Wikipedia has a page about central groupoids, and it was apparently newly created today!

[David Renshaw]

On the talk page the author says they "saw a post about it [the Equational Theories project] and learned of this subject through it".

[David Renshaw]

I would guess that they are referring to yesterday's blog post.