Hey John,

> Do you know any other good applications of left and right residuated monoidal posets that aren't commutative?

The ones I've encountered are [*action algebras*](https://en.wikipedia.org/wiki/Action_algebra).

These extend [*regular expressions*](https://en.wikipedia.org/wiki/Regular_expression), which are insanely common in computer programming. For instance, if you try to sign up for a website, programmers do not want you to give an invalid email. The programmer will check that your email matches a pattern like

^[a-zA-Z0-9_.+-]+@[a-zA-Z0-9-]+\.[a-zA-Z0-9-.]+$


(I lifted that from this [stack overflow](https://stackoverflow.com/a/719543))

Suppose I had three regular expression:

- one called \\(\mathtt{email}\\) for checking emails
- one called \\(\mathtt{comma}\\) for checking there's a comma
- one called \\(\mathtt{phone}\\) for checking phone numbers

I can combine these to match a line of text where there's an email, a comma, and a phone number (lots of files are like this). This is done using a *monoidal tensor*. I've seen this tensor denoted \\(;\\) in [Propositional Dynamic Logic](https://plato.stanford.edu/entries/logic-dynamic/) and programming language design courses so I'll use that notation.

So we can make a new regular expression like this:

\[\mathtt{email} ; \mathtt{comma} ; \mathtt{phone}\]

Composition here is *not* commutative so this will not match a phone followed by a comma follows by an email.

There's also a regular expression \\(I\\) that just matches an empty string, and plays the role of identity \\(I ; R = R ; I = R\\).

We can pre-order regular expressions too: \\(A \leq B\\) if any text \\(A\\) matches then \\(B\\) matches it.

Action algebras explore what programming is like if \\((;)\\) had left and right adjoints such that

\[(- \leftarrow A) \dashv (A ; -) \dashv (A \to -) \]

Real world regular expressions never implement this, but these residuals are still useful for understanding regular expressions. For instance, action algebras are finitely axiomatizable and form a variety. Regular expressions correspond to a fragment of this variety. Regular expressions are remarkably *not* finitely axiomatizable! One proof of this comes from none other than [John Conway](https://en.wikipedia.org/wiki/Kleene_algebra#History) of surreal-numbers and game-of-life fame.