1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
\Chapter{Algebraic models}{Now the teacher would say to learn your
algebra}{Johnny Cash}
\chapterlabel{algebraic-models}
\cats{}The semantic structures we considered so far, namely for global state, exceptions,
I/O, and recursion, arise from algebraic descriptions using Plotkin and Power's algebraic
theory of effects. We now restrict our attention to
such algebraic models. We present a construction that builds
an entire hierarchical model from a single \cbpv{} model at the top of
the hierarchy. Thus, a refined semantics that takes type-and-effect information
into account can be \emph{derived} from an unrefined semantics. Our
construction uses \defterm{factorisation systems} of categories.
First, in \sectionref{cat alg mod}, we present our notion of algebraic
models for effect analysis. Next, in \sectionref{fact sys}, we recall
some notions about factorisation systems, and apply them to enriched
Lawvere theories. With this machinery at hand, in \sectionref{cat cons
rest}, we present the categorical conservative restriction
construction.
\Include{categorical-algebraic-models}
\Include{factorisation-systems}
\Include{categorical-conservative-restriction}
|