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.