Turi-Plotkin
(Thanks to Harrison Grodin for explaining this to me)
If p,q:\mathbf{Poly} are polynomial interfaces for program and operating system respectively, and \mathfrak{m}_p and \mathfrak{c}_q are the associated free monad and cofree comonad, then a rewriting system (operational semantics) is a map of the form
\Psi\colon p\lhd\mathfrak{c}_q\to q\lhd\mathfrak{m}_p.
The idea is that for a single step P:p(1) and system state S:\mathfrak{c}_q(1), we get a next system output J:q(1), and for every input j:q[J] there, a “rewritten” program T:\mathfrak{m}_p(1), and for every way t:\mathfrak{m}_p[T] that the program can return, a return for the original p and a way to update the operating system state.
Turi-Plotkin prove that this yields a distributive law of the form
\mathfrak{m}_p\lhd\mathfrak{c}_q\to\mathfrak{c}_q\lhd\mathfrak{m}_p.
I’d guess this isn’t too hard to prove.
This all relates to my work with Owen [video] [blog post], on what he called effect handlers, which we defined to be maps of the form
s\lhd c\to d\lhd s
where s:\mathbf{Poly} is any polynomial, and c,d:\mathbf{Cat}^\sharp are polynomial comonads. In particular, we saw no reason that c and d had to be the same; d could ``handle’’ the effects from c.
1 Like
@HarrisonGrodin, @dspivak can you give a reference for this, or an example of this for specific polynomials?
Wait, slight issue - I think it should be:
\Psi : p \triangleleft qy \to q \triangleleft \mathfrak{m}_p
From Turi-Plotkin, these extend to distributive laws.
According to results by Klin and Nachyla, not every “biGSOS law” p \triangleleft \mathfrak{c}_q \to q \triangleleft \mathfrak{m}_p extends (at all/uniquely) to a distributive law \mathfrak{m}_p \triangleleft \mathfrak{c}_q \to \mathfrak{c}_q \triangleleft \mathfrak{m}_p.
Towards a mathematical operational semantics (Turi-Plotkin) is the original reference, but this summary by Klin is longer/has more examples.
In the simplest case, it’s useful to consider laws p \triangleleft q \to q \triangleleft p, where p represents syntax and q represents “behavior”. For example, let p = \mathbb{N} + y^2 (two syntactic forms, a natural number and a binary operator) and q = \mathbb{N}y (behavior is emitting a natural number). You can define a map p \triangleleft q \to q \triangleleft p that sends
- \iota_1 n to (n, \iota_1 (n + 1)) - the number syntax for n emits n and transitions to the syntactic form n + 1
- \iota_2((m, x'), (n, y')) to (m + n, \iota_2 (x', y')) - the binary operator syntax emits m + n when the subterms transition to m and n, repsectively
This corresponds to the following set of operational semantics transition/rewrite rules:
\frac{}{\texttt{counter}_n \xrightarrow{n} \texttt{counter}_{n+1}} \qquad
\frac{x \xrightarrow{m} x' \quad y \xrightarrow{n} y'}{\texttt{sum}(x,y) \xrightarrow{m + n} \texttt{sum}(x',y')}