1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
\Section{Algebraic operations}\sectionlabel{lawvere operations}
We define algebraic operations for
Lawvere theories:
\begin{definition}
Let $\mL$ be a $\regcard$-Lawvere $\SymMonCat$-theory, and $\Ar$,
$\Pa$ be $\regcard$-presentable objects. An \defterm{operation
$\mop$ of type $\arity\Ar\Pa$ in $\mL$} is a morphism $\mop \of \Ar \to \Pa$
in ${\LawCat\mL}$, i.e., a $\SymMonCat$-morphism ${\mop \of
\oI \to \homset[\LawCat\mL]\Ar\Pa}$.
\noindent
Let $\mop$, $\mopv$ be algebraic operations of type $\arity\Ar\Pa$ in
$\mL$, $\mLv$, respectively, and $\LawHomo \of \mL \to \mLv$ a
morphism of Lawvere theories. We say that \defterm{$\LawHomo$ maps
$\mop$ to $\mopv$} if $\LawHomo(\mop) = \mopv$, i.e., when
\inlinediagram{generic-operation-preservation-04}
\end{definition}
Just as in \sectionref{categorical models}, we write $\mop \of
\arity\Ar\Pa$ when $\mop$ is an operation of type $\arity\Ar\Pa$.
In fact, Plotkin and Power's notion of algebraic operations (see
\definitionref{alg ops}) arose from the notion of algebraic operations
in a Lawvere theory. Thus, the correspondence between algebraic
operations and generic effects extends to operations in a Lawvere
theory. It is precisely the well-known bijection between
arrows in a Lawvere theory and Kleisli arrows:
\begin{theorem}\theoremlabel{monad<->theory preserves operations}
Let $\ValCat$ be a $\regcard$-Power category with a cartesian
closed structure.
The equivalence $\Lawvere\SymMonCat \equivalence
\EnrichedRankedMonad\SymMonCat$ given in \theoremref{theory <->
ranked monad} induces a bijection between generic effects $\mgen
\of \arity\Ar\Pa$ for $\regcard$-ranked $\SymMonCat$-enriched
monads and algebraic operations $\mop\of\arity\Ar\Pa$ for $\regcard$-Lawvere
$\SymMonCat$-theories, given by:
\begin{gather*}
\lawoperation\mgen{} \of \oI
\xto{\ilam\Pa{\parent{\terminal\times\Pa \xto{\proj2}\Pa\xto{\mgen}\Monad\Ar}}}
(\Monad\Ar)^{\Pa} = \homset[\LawCat{\MonadTheory\Monad}]\Ar\Pa
\isomorphic \homset[\LawCat\mL]\Ar\Pa
\\
\generic{\mop}\of\Pa \isomorphic \terminal\times\Pa
\xto{\mop\times\Pa}
\homset[\LawCat\mL]\Ar\Pa\times\Pa \isomorphic
(\Monad\Ar)^{\Pa}\times\Pa \xto{\eval}\Monad\Ar
\end{gather*}
Moreover, this bijection respects the mapping relation between
operations: a strong monad morphism $\MonadMorphism$ maps $\mgen$ to $\mgenv$ if and only if
$\MonadTheory\MonadMorphism$ maps $\lawoperation\mgen$ to $\lawoperation\mgenv$.
\end{theorem}
\begin{proof}%
The bijection amounts to internalising the Kleisli arrow $\mgen$ and using
the isomorphisms $\homset[\LawCat\mL]\Ar\Pa \isomorphic
(\Monad\Ar)^{\Pa}$. For establishing that
$\generic{\lawoperation\mgen} = \mgen$, we have
\inlinediagram{monad-theory-operation-bijection-01}
Conversely, for $\lawoperation{\generic{\mop}} = \mop$ we have, by universality,
\inlinediagram{monad-theory-operation-bijection-02}
Similar calculations show that the commutativity of each of the
following two diagrams implies the commutativity of the
other:
\inlinediagram{generic-operation-preservation-05}
Therefore, $\MonadMorphism$ maps $\mgen$ to $\mgenv$ if and and only
if $\MonadTheory\MonadMorphism$ maps $\lawoperation\mgen$ to $\lawoperation\mgenv$.
\end{proof}
\begin{example}\examplelabel{IO to global state morphism}
Take $\ValCat$ to be $\Set$ and $\regcard$ to be
$\aleph_0$. Let $\StorVal$ be any finite set with at least two
elements denoting storable values. Take $\Char$ to be
$\StorVal$. Consider the global state monad $\GlobalStateMonad$, and the
monad $\IOMonad[\parent\StorVal]$ for input/output of `characters'
in $\StorVal$. We define inductively a monad morphism $f\of \IOMonad[\parent\StorVal]\to
\GlobalStateMonad$:
\begin{mapdef*}[2]
f_{\mX} \of& \IOMonad[\parent\StorVal]\mX &\to
\GlobalStateMonad\mX
\\
f_{\mX} \of& \pair
I{\seq{\mterm_{\mval}}} &\mapsto
\ilam \mval{f_{\set\lookupop}(\mterm_{\mval})(\mval)}
\\
& \mx &\mapsto \ilam\mval{\pair\mval\mx}
\qquad\qquad
\\
& \triple O{\mval_0}\mterm
&\mapsto
\ilam \mval{f(\mterm)(\mval_0)}
\end{mapdef*}%
Straightforward calculations show $f$ is indeed a monad morphism,
and that it maps the input operation to the look-up operation and the
output operation to the update operation. Note also that $f$ is
surjective, as
\[
\ilam\mval{\pair{\mvalv_{\mval}}{\mx_{\mval}}}
=
f(\pair I{\seq[\mval\in\StorVal]{\triple O{\mvalv_{\mval}}{\mx_{\mval}}}})
\]
Thus, by \theoremref{monad<->theory preserves operations} we have
input and output operations for the finitary Lawvere theory $\IOTheory$
corresponding to $\IOMonad$, lookup and update operations for the
finitary Lawvere theory $\GlobalStateTheory$, and the monad morphism
$f$ maps the input and output operations to the look-up and update
operations, respectively.
\end{example}
|