The Comonad.Readertypes, (co)monads, substructural logic
Lambda World · Talk

There and Back Again: Regular and Inverse Semigroups

Edward Kmett

Watch on YouTube · 47 minutes

This keynote by Edward Kmett took place at Lambda World Seattle on September 18th, 2018 at the Living Computers Museum in Washington.

Opening Keynote: There and Back Again

Mathematicians usually teach abstract algebra from groups and build up from there. Having inverses allows them to prove many non-trivial results. Functional programmers more often descend to working with monoids, or even semigroups. They give up the power of inverses to gain many more examples. You don't often hear about the shadowy realm between. Perfect inverses don't always exist, nor do we want them to. Going on a journey and returning rarely leaves the protagonist unchanged. If it does, this is usually taken as a poor example of the author's craft. We'll explore the middle-ground of regular and inverse semigroups, inverse monoids, even inverse categories. In this space where inverses may not invert, we'll develop examples and counter-examples. We'll gain some insight into spoken Australian English along the way. Join us.

Materials

Related recording: Live Coding — Session 4.1: Regular and Inverse Semigroups

From the original discussion

Edward Kmett · Original reply

Selected paragraphs from the original reply; wording preserved.

(+) on the naturals simply isn't a semilattice. max on the natural numbers, on the other hand is.

When working with a semilattice, inv m = m passes all of the laws for an inverse semigroup, and it is the only such choice that passes the laws. Why?

  • m <> inv m <> m = m, because m <> m <> m = m
  • inv m <> m <> inv m = inv m by the same logic.

Given a semilattice, all elements are of the form x = x <> inv x and all idempotents (in this case, all elements) commute.

Every group is an inverse semigroup. It has exactly one idempotent element e, which commutes with every idempotent element (itself), ee = ee. All idempotents are of the form x <> inv x for some x, indeed e = x <> inv x for all x. The x <> inv x <> x = x style laws follow from the unit and inverse laws for the group.

Regular semigroups are saying that every element of your semigroup is 'regular', which is to say that there is some "pseudo-inverse" for it.

Inverse semigroups add the further constraint that the inverse is unique. From that all the rest of this stuff follows.