日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

Graded Algebraic Theories
Satoshi Kura

We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and ﬁnitary graded monads areequivalent via equivalence of categories, which extends the equivalence for monads. We also give sums andtensor products of graded algebraic theories to combine computational eﬀects as an example of importing
techniques based on algebraic theories to graded monads.

f ∈ Σn,m

1 Introduction
In the ﬁeld of denotational semantics of programming languages, monads have been used to express computational eﬀects since Moggi’s seminal
work [18]. They have many applications from boththeoretical and practical points of view.
Monads correspond to algebraic theories [5]. This
correspondence gives natural presentations of manykinds of computational eﬀects by operations andequations [21], which is the basis of algebraic effect [20]. The algebraic perspective of monads
also provides ways of combining [9], reasoning
about [22], and handling computational eﬀects [23].
Graded monads [27] are a reﬁnement of monads and deﬁned as a monad-like structure indexed
by a monoidal category (or a preordered monoid).
The unit and multiplication of graded monads are
required to respect the monoidal structure. This
structure enables graded monads to express somekind of “abstraction” of eﬀectful computations. For
example, graded monads are used to give denotational semantics of eﬀect systems [12], which aretype systems designed to estimate scopes of computational eﬀects caused by programs.
次数付き代数理論
The original version of this paper has been published in FoSSaCS 2020.
内藏 理史, 総合研究大学院大学複合科学研究科情報学専
攻 & 国立情報学研究所, The Graduate University for
Advanced Studies (SOKENDAI) & National Institute of Informatics.

Σti ∈ Tm′ (X) for each i ∈ {1, . . . , n}Σf (t1 , . . . , tn ) ∈ Tm⊗m
′ (X)Fig. 1

A rule of term formation.

This paper provides a graded extension of algebraic theories that corresponds to monads gradedby small strict monoidal categories. This generalizes N-graded theories in [17]. The main ideas ofthis extension are the following. First, we assign toeach operation a grade, i.e., an object in a monoidal
category that represents eﬀects. Second, our extension provides a mechanism (Fig. 1) to keep track ofeﬀects in the same way as graded monads. That is,
if an operation f with grade m is applied to termswith grade m′ , then the grade of the whole term isthe product m ⊗ m′ .
For example, graded algebraic theories enable
us to estimate (an overapproximation of) the setof memory locations computations may access.
The side-eﬀects theory [21] is given by operations
lookupl and updatel,v for each location l ∈ L
and value v ∈ V together with several equations,and each term represents a computation with sideeﬀects. Since lookupl and updatel,v only read fromor write to the location l, we assign {l} ∈ 2L as thegrade of the operations in the graded version of theside-eﬀects theory where 2L is the join-semilatticeof subsets of locations L. The grade of a term is (anoverapproximation of) the set of memory locations
the computations may access thanks to the rule inFig 1.

We also provide graded Lawvere theories that correspond to graded algebraic theories. The intuitionof a Lawvere theory is a category whose arrows areterms of an algebraic theory. We use this intuition
to deﬁne graded Lawvere theories. In graded algebraic theories, each term has a grade, and substitution of terms must respect the monoidal structure of grades. To characterize this structure of“graded” terms, we consider Lawvere theories enriched in a presheaf category.
Like algebraic theories brought many concepts
and techniques to the semantics of computationaleﬀects, we expect that the proposed graded algebraic theories will do the same for eﬀect systems.
We look into one example out of such possibilities:
combining graded algebraic theories.
The main contributions of this paper are summarized as follows.
• We generalize (N-)graded algebraic theoriesof [17] to M-graded algebraic theories and also
provide M-graded Lawvere theories where M
is a small strict monoidal category. We showthat there exist translations between these notions and ﬁnitary graded monads, which yield
equivalences of categories.
• We extend sums and tensor products of algebraic theories [9] to graded algebraic theories.
We deﬁne sums in the category of M-gradedalgebraic theories, and tensor products as an
M × M′ -graded algebraic theory made from an
M-graded and an M′ -graded algebraic theory.
We also show a few properties and examples ofthese constructions.

We deﬁne V0 -category, V0 -functor and V0 natural transformation as in [13].
If V0 is right closed, then V0 itself enriches
to a V0 -category V with hom-object given by
V(X, Y ) := [X, Y ]. We use the subscript (−)0 to
distinguish the enriched category V from its underlying category V0 .
Assume that V0 is biclosed and let A be a
V0 -category. The opposite category Aop is theV0 t -category deﬁned by Aop (X, Y ) = A(Y, X).
For any X ∈ obA, A(X, −) : A → V0 isa V0 -functor where A(X, −)Y,Z : A(Y, Z) →[A(X, Y ), A(X, Z)] is deﬁned by transposing thecomposition law ◦ of A. A V0 t -functor A(−, X) is
deﬁned by Aop (X, −) : Aop → V0 t .
Let A be a V0 -category. For each X ∈ V0
and C ∈ A, a tensor X ⊗ C is an object in
A together with a counit morphism ν : X →A(C, X ⊗ C) such that a V0 -natural transformation A(X ⊗ C, −) → JX, A(C, −)K obtained bytransposing (◦) ◦ (A(X ⊗ C, B) ⊗ ν) is isomorphic where ◦ is the composition in the V0 -category
A. A cotensor X ⋔ C is a tensor in Aop . For example, if V0 = Set, then tensors X ⊗ C are copowers
X · C, and cotensors X ⋔ C are powers C X .
A V0 -functor F : A → B is said to preserve atensor X ⊗ C if FC,X⊗C ◦ ν : X → B(F C, F (X ⊗C)) is again a counit morphism. F preserves cotensors if F op preserves tensors.
Let Φ be a collection of objects in V0 . A V0 functor F : A → B is said to preserve Φ-(co)tensors
if F preserves (co)tensors of the form X ⊗ C(X ⋔ C) for each X ∈ Φ and C ∈ obA.

2 Preliminaries
2. 1 Enriched Category Theory
We review enriched category theory and introduce notations. See [13] for details.
Let V0 = (V0 , ⊗, I) be a (not necessarily symmetric) monoidal category. V0 is right closed if(−) ⊗ X : V0 → V0 has a right adjoint [X, −]for each X ∈ obV0 . Similarly, V0 is left closed
if X ⊗ (−) has a right adjoint JX, −K for eachX ∈ obV0 . V0 is biclosed if V0 is left and rightclosed.
Let V0 t denote the monoidal category (V0 , ⊗t , I)
where ⊗t is deﬁned by X ⊗t Y := Y ⊗ X. Notethat V0 t is right closed if and only if V0 is left
closed.

2. 2 Graded Monads
We review the notion of graded monad in [12] [7],and then deﬁne the category GMndM of ﬁnitary
M-graded monads. Throughout this section, we ﬁx
a small strict monoidal category M = (M, ⊗, I).
Deﬁnition 1 (graded monads). An M-gradedmonad on C is a lax monoidal functor M → [C, C]
where [C, C] is a monoidal category with composition as multiplication. That is, an M-gradedmonad is a tuple (∗, η, µ) of a functor ∗ : M × C →C and natural transformations ηX : X → I ∗ X andµm1 ,m2 ,X : m1 ∗ (m2 ∗ X) → (m1 ⊗ m2 ) ∗ X suchthat the following diagrams commute.

η

m∗X

I ∗ (m ∗ X)m∗ηµm ∗ (I ∗ X)
m1 ∗(m2 ∗(m3 ∗X))

µ
m1 ∗µ

µ

(m1 ⊗m2 )∗(m3 ∗X)

ηn

n

β

′
ηn

m∗X
m1 ∗((m2 ⊗m3 )∗X)
µ

µ

I ∗n

(m1 ⊗m2 ⊗m3 )∗X

A morphism of M-graded monad is a monoidal natural transformation α : (∗, η, µ) → (∗′ , η ′ , µ′ ), i.e. anatural transformation α : ∗ → ∗′ that is compatible with η and µ.
An intuition of graded monads is a reﬁnement ofmonads: m ∗ X is a computation whose scope ofeﬀect is indicated by m and whose result is in X.
The monoidal category M deﬁnes the granularityof the reﬁnement, and a 1-graded monad is justan ordinary monad. Note that we do not assume
that M is symmetric because some of graded monads in [12] require M to be nonsymmetric. We also
deal with such a nonsymmetric case in Example 26.
A ﬁnitary functor is a functor that preserves ﬁltered colimits. In this paper, we focus on ﬁnitary
graded monads on Set.
Deﬁnition 2. A ﬁnitary M-graded monad on
Set is a lax monoidal functor M → [Set, Set]f
where [Set, Set]f denotes the full subcategory of[Set, Set] on ﬁnitary functors. Let GMndM denote the category of ﬁnitary M-graded monads andmonoidal natural transformations between them.
A morphism in GMndM is determined by the
restriction to ℵ0 ⊆ Set where ℵ0 is the full subcategory of Set on natural numbers.
Lemma 3. Let T = (∗, η, µ) and T ′ = (∗′ , η ′ , µ′ )be ﬁnitary M-graded monads. There exists one-toone correspondence between the following.
1. Morphisms α : T → T ′ .
2. Natural transformations β : ∗ ◦ (M × i) →∗′ ◦ (M × i) (where i : ℵ0 → Set is the inclusion functor) such that the following diagrams
commute for each n, n′ ∈ ℵ0 , m1 , m2 ∈ M andf : n → m2 ∗ n′ .

′

I∗ n
β

m1 ∗ nm1 ∗′ nm1 ∗′ fm1 ∗′ (m2 ∗ n′ )

m1 ∗f
′

m1 ∗ (m2 ∗ n )m1 ∗m1 ∗′ β(m2 ∗′ n′ )µ′µ(m1 ⊗ m2 ) ∗ n′′β

(m1 ⊗ m2 ) ∗′ n′

Proof. By the equivalence [Set, Set]f ' [ℵ0 , Set]
induced by restriction and the left Kan extension
along the inclusion i : ℵ0 → Set.
2. 3 Day Convolution
We describe a monoidal biclosed structure onthe (covariant) presheaf category [M, Set]0 whereM = (M, ⊗, I) is a small monoidal category [3].
Here, we use the subscript (−)0 to indicate that
[M, Set]0 is an ordinary (not enriched) category
since we also use the enriched version [M, Set]
later.
The external tensor product F ⊠ G : M × M →Set is deﬁned by (F ⊠ G)(m1 , m2 ) = F m1 × Gm2
for any F, G : M → Set.
Deﬁnition 4. Let F, G : M → Set be functors.
ˇ G : M → Set is the
The Day tensor product F ⊗left Kan extension Lan⊗ (F ⊠G) of the external tensor product F ⊠G : M×M → Set along the tensor
product ⊗ : M × M → M.
ˇNote that a natural transformation θ : F ⊗G → H is equivalent to a natural transformation
θm1 ,m2 : F m1 × Gm2 → H(m1 ⊗ m2 ) by the universal property.
The Day convolution induces a monoidal biclosed
structure in [M, Set]0 [3].
Proposition 5. The Day tensor product makesˇ y(I)) a monoidal biclosed category([M, Set]0 , ⊗,where y : Mop → [M, Set]0 is the Yoneda embedding y(m) := M(m, −).
The left and the right closed structure are
given by JF, GK m = [M, Set]0 (F, G(m⊗−)) and[F, G] m = [M, Set]0 (F, G(−⊗m)) for each m ∈M, respectively.
Note that since we do not assume M to besymmetric, neither is [M, Set]0 . Note also thatthe twisting and the above construction commute:there is an isomorphism [M, Set]0 t ∼= [Mt , Set]0 of
monoidal categories.
2. 4 Categories Enriched in a Presheaf
Category
We rephrase the deﬁnitions of [M, Set]0 -enrichedcategory, functor and natural transformation in elementary terms. An [M, Set]0 -category is, so to
say, an “M-graded” category: each morphism has
a grade m ∈ obM and the grade of the composite of two morphisms with grades m and m′ is the
product m ⊗ m′ of the grades of each morphism.
Likewise, [M, Set]0 -functors and [M, Set]0 -naturaltransformations can be also understood as an “Mgraded” version of ordinary functors and naturaltransformations. Speciﬁcally, the following lemma
holds [2].
Lemma 6. There is a one-to-one correspondence
between (1) an [M, Set]0 -category C and (2) the
following data satisfying the following conditions.
• A class of objects obC.
• For each X, Y ∈ obC, a hom objects
C(X, Y ) ∈ [M, Set]0 .
• For each X ∈ obC, an element 1X ∈C(X, X)I.
• For each X, Y, Z ∈ obC, a family of morphisms ◦m1 ,m2 : C(Y, Z)m1 × C(X, Y )m2 →C(X, Z)(m1 ⊗ m2 ) m ,m ∈M which is natural1
2
in m1 and m2 . The subscripts m1 and m2 areoften omitted.
These data must satisfy the identity law 1Y ◦ f =f = f ◦ 1X for each f ∈ C(X, Y )m and the associativity (h ◦ g) ◦ f = h ◦ (g ◦ f ) for each f ∈C(X, Y )m1 , g ∈ C(Y, Z)m2 and h ∈ C(Z, W )m3 .
Proof. The identity 1X : y(I) → C(X, X) in C corresponds to 1X ∈ C(X, X)I by the Yoneda lemma,
ˇ C(X, Y ) →and the composition ◦ : C(Y, Z) ⊗C(X, Z) in C corresponds to the natural transformation ◦m1 ,m2 : C(Y, Z)m1 × C(X, Y )m2 →C(X, Z)(m1 ⊗ m2 ) by the universal property of theDay convolution. The rest of the proof is easy.
An [M, Set]0 -functor F : C → D consists ofa mapping X 7→ F X and a natural transformation FX,Y : C(X, Y ) → D(F X, F Y ) (for each
X, Y ) that preserves identities and compositionsof morphisms. An [M, Set]0 -natural transformation α : F → G is a family of elements αX ∈D(F X, GX)I X∈ob(C) that satisﬁes αY ◦ F f =Gf ◦ αX for each f ∈ C(X, Y )m. Vertical andhorizontal compositions of [M, Set]0 -natural transformations are deﬁned as expected.
We introduce a useful construction of [M, Set]0 t categories. Given an M-graded monad (in otherwords, a lax left M-action) on C, we can deﬁne an[M, Set]0 t -enriched category as follows.
Deﬁnition 7. Let T = (∗, η, µ) be an M-gradedgmonad on C. An [M, Set]0 t -category C
T is deﬁnedgg
by obCT := obC and CT (X, Y )m := C(X, m ∗ Y ).
The identity morphisms are the unit morphismsgηX ∈ C
T (X, X)I, and the composite of f ∈′gg
CT (Y, Z)m and g ∈ C
T (X, Y )m is µ ◦ (m ∗ g) ◦ f .
g
The deﬁnition of CT is similar to the deﬁnitionof the Kleisli categories for ordinary monads. Acg
tually, C
T can be constructed via the Kleisli category CT for the graded monad T presented in [7](although CT itself is not enriched). This can begobserved by CT ((I, X), (m, Y )) ∼=C
T (X, Y )m.

3 Graded Algebraic Theories
We explain a framework of universal algebra
for graded monads, which is a natural extensionof [27] [17]. The key idea of this framework is thateach term is associated with not only an arity but
also a “grade”, which is represented by an object ina monoidal category M. We also add coercion construct for terms that changes the grade of terms
along a morphism of the monoidal category M.
Then, a mapping that takes m ∈ M and a set ofvariables X and returns the set of terms with grade
m (modulo the equational axioms) yields a gradedmonad.
We ﬁx a small strict monoidal category M =(M, ⊗, I) throughout this section. We sometimes
identify n ∈ N with {1, . . . , n}, or {x1 , . . . , xn } if it
is used as a set of variables.
3. 1 Equational Logic
A signature is a family of sets of symbols Σ =(Σn,m )n∈N,m∈M . An element f ∈ Σn,m is called
an operation with arity n and grade m. We deﬁne
a suﬃcient structure to interpret operations in a
category C as follows.
Deﬁnition 8. M-model condition is deﬁned by thefollowing conditions on a tuple (C, (⊛, η ⊛ , µ⊛ )).
• C is a category with ﬁnite power.
• (⊛, η ⊛ , µ⊛ ) is a strong Mt -action (i.e. an Mt -

graded monad whose unit and multiplication
are invertible).
• For each m ∈ M, m ⊛ (−) preserves ﬁnite
powers: m ⊛ cn ∼= (m ⊛ c)n .
Example 9. If A is a category with ﬁnite powers, then the functor category [M, A] has strong
Mt -action deﬁned by m ⊛ F := F (m ⊗ (−)) andsatisﬁes M-model condition. Especially, [M, Set]0
satisﬁes M-model condition.
A model A = (A, | · |A ) of Σ in a category C
satisfying M-model condition consists of an object
A ∈ C and an interpretation |f |A : An → m ⊛ A
for each f ∈ Σn,m . A homomorphism α : A → B
between two models A, B is a morphism α : A → B
in C such that (m ⊛ α) ◦ |f |A = |f |B ◦ αn for eachf ∈ Σn,m .
Deﬁnition 10. Let X be a set of variables. TheΣ
set of (M-graded) Σ-terms Tm(X) for each m ∈ M
is deﬁned inductively as follows.
x∈Xx ∈ TIΣ (X)f ∈ Σn,mΣ (X)t ∈ Tmw : m → m′

Σ (X)
cw (t) ∈ Tm′
Σ (X)∀i ∈ {1, . . . , n}, ti ∈ Tm′

Σf (t1 , . . . , tn ) ∈ Tm⊗m
′ (X)That is, we build Σ-terms from variables by applying operations in Σ and coercions cw while keeping track of the grade of terms. When applying
operations, we sometimes write f (λi ∈ n.ti ) orf (λi.ti ) instead of f (t1 , . . . , tn ).
Deﬁnition 11. Let A be a model of a signature Σ.
ΣFor each m ∈ M and s ∈ Tm(n), the interpretationAn|s| : A → m ⊛ A is deﬁned as follows.
• For any variable xi , |xi |A = η ⊛ ◦ πi whereπi : An → A is the i-th projection.
• For each w : m′ → m and s ∈ΣA= (w ⊛ A) ◦ |s|A .
Tm′ ({x1 , . . . , xn }), |cw (s)|Σ• If f ∈ Σk,m′ and ti ∈ Tm′′ ({x1 , . . . , xn }) for
each i ∈ {1, . . . , k}, then |f (t1 , . . . , tk )|A is deﬁned by the following composite.
An⟨|t1 |,...,|tk |⟩(m′′ ⊛A)k
∼
=
′′

m ⊛Ak
′′

m′′ ⊛|f |′m ⊛(m ⊛A)µ(m′ ⊗m′′ )⊛AΣWhen we interpret a term t ∈ Tm
(X), we needto pick a ﬁnite set n such that fv(t) ⊆ n ⊆ X

where fv(t) is the set of free variables in t, but
the choice of the ﬁnite set does not matter when
we consider only equality of interpretations by thefollowing fact. If σ : n → n′ is a renaming of variΣΣ(n) → Tm(n′ ) is a mapping inables and σ : TmΣ
duced by the renaming σ, then for each t ∈ Tm
(n),
A
A
σ
|σ(t)| = |t| ◦ A , which implies that equality of
the interpretations of two terms s, t is preserved byrenaming: |s| = |t| implies |σ(s)| = |σ(s)|.
An equational axiom is a family of sets E =(Em )m∈M where Em is a set of pairs of terms inΣTm(X). We sometimes identify E with its unionSm∈M Em . A presentation of an M-graded algebraic theory (or an M-graded algebraic theory) is apair T = (Σ, E) of a signature and an equational
axiom. A model A of (Σ, E) is a model of Σ thatsatisﬁes |s|A = |t|A for each (s = t) ∈ E. Let
ModT (C) denote the category of models of T in C
and homomorphisms between them.
To obtain a graded monad on Set from T , weneed a strict left action of M on ModT ([M, Set]0 )and an adjunction between ModT ([M, Set]0 ) and
Set. The former is deﬁned by the following, while
the latter is described in §3. 2.
Lemma 12. Let C be a category satisfying M1 ×
M2 -model condition. If T is an M1 -graded algebraic theory, then C satisﬁes M1 -model condition
and ModT (C) satisﬁes M2 -model condition.
Proof. An Mt1 -action on C is obtained by thecomposition of Mt1 × Mt2 -action and the strong
monoidal functor Mt1 → Mt1 × Mt2 deﬁned by
m 7→ (m, I). Finite powers and an Mt2 -action for
ModT (C) are induced by those for C.
Corollary 13. ModT ([M, Set]0 ) has an M-action,
which is given by the precomposition of m ⊗ (−)
like the M-action of Example 9.
Proof. [M, Set]0 has Mt × M-action deﬁned by(m1 , m2 ) ∗ F = F (m1 ⊗ (−) ⊗ m2 ). Thus,
M-action for ModT ([M, Set]0 ) is obtained by
Lemma 12.
Substitution s[t1 /x1 , . . . , tk /xk ] for M-graded Σterms can be deﬁned as usual, but we have to takeΣ
care of grades: given s ∈ Tm(k) and t1 , . . . , tk ∈
ΣTm′ (n), the substitution s[t1 /x1 , . . . , tk /xk ] is deΣ
ﬁned as a term in Tm⊗m
′ (n).
We obtain an equational logic for graded theories by adding some additional rules to the usual
equational logic.
Deﬁnition 14. The entailment relation T ` s = t

(where s, t ∈ Tm (X)) for an M-graded theory T isdeﬁned by adding the following rules to the standard rules i.e. reﬂexivity, symmetry, transitivity,
congruence, substitution and axiom in E (see e.g.
[26] for the standard rules of equational logic).
Σ (X)s, t ∈ Tm

T ⊢s=tw : m → m′

T ⊢ cw (s) = cw (t)Σ (X)t ∈ TmT ⊢ c1m (t) = t
Σ (X)t ∈ Tmw : m → m′w′ : m′ → m′′

T ⊢ cw′ (cw (t)) = cw′ ◦w (t)f ∈ Σn,m

Σ (X) for each iti ∈ Tm′w : m′ → m′′

T ⊢ f (cw (t1 ), . . . , cw (tn )) = cm⊗w (f (t1 , . . . , tn ))Deﬁnition 15. Given a model A of T , we deΣnote A ⊩ s = t if s, t ∈ Tm(n) (for some n) andAA|s| = |t| . If C is a category satisfying M-model
condition, we denote T , C ⊩ s = t if A ⊩ s = t forany model A of T in C.
It is easy to verify that the equational logic in
Deﬁnition 14 is sound.
Theorem 16 (soundness). T ` s = t implies
T , C ⊩ s = t.
3. 2 Free Models
We describe a construction of a free modelF T X ∈ ModT ([M, Set]0 ) of a graded theory T
generated by a set X, which induces an adjunction
between ModT ([M, Set]0 ) and Set. This adjunction, together with the M-action of Corollary 13,
gives a graded monad as described in [7].
Deﬁnition 17 (free model F T X). Let T = (Σ, E)
be an M-graded theory. We deﬁne a functorΣ
F T X : M → Set by F T Xm := Tm(X)/∼mfor each m ∈ M and any X ∈ Set wheres ∼m t is the equivalence relation deﬁned byT ` s = t and F T Xw([t]m ) := [cw (t)]m′ for any
w : m → m′ where [t]m is the equivalence classTΣof t ∈ Tm(X). For each f ∈ Σn,m′ , let |f |F X :Tn′T(F X) → m ⊛ F X be a mapping deﬁned
FT X
by |f |m([t1 ]m , . . . , [tn ]m ) = [f (t1 , . . . , tn )]m′ ⊗mfor each m ∈ M. We deﬁne a model of T byT
F T X = (F T X, | · |F X ).
The model F T X, together with the mappingηX : X → F T XI deﬁned by x 7→ [x]I , has thefollowing universal property as a free model generated by X.
Lemma 18. For any model A in [M, Set]0 andany mapping v : X → AI, there exists a unique

homomorphism v : F T X → A satisfying v I ◦ ηX =v.
Corollary 19. Let U : ModT ([M, Set]0 ) → Set
be the forgetful functor deﬁned by the evaluation
at I, that is, U A = AI and U α = αI . The freemodel functor F T : Set → ModT ([M, Set]0 ) is aleft adjoint of U .
By considering the interpretation in the freemodel, we obtain the following completeness theorem.
Theorem 20 (completeness). T , [M, Set]0 ⊩ s =t implies T ` s = t.
Recall that ModT ([M, Set]0 ) has a left action(Corollary 13). Therefore the above adjunction induces an M-graded monad as described in [7].
The relationship between ModT ([M, Set]0 ) andthe Eilenberg–Moore construction is as follows.
In [7], the Eilenberg–Moore category CT for any
graded monad T on C is introduced together witha left action ⊛ : M × CT → CT . If C = Set andT is the graded monad obtained from an M-gradedtheory T , then the Eilenberg–Moore category SetT
is essentially the same as ModT ([M, Set]0 ).
Theorem 21. The comparison functor K :ModT ([M, Set]0 ) → SetT (see [7] for the deﬁnition) where T is an M-graded theory and T is thegraded monad induced from the graded theory T isisomorphic. Moreover, K preserves the M-action:⊛ ◦ (M × K) = K ◦ ⊛.
We deﬁne the category GSM of graded algebraic
theories as follows.
Deﬁnition 22. Let T = (Σ, E) and T ′ = (Σ′ , E ′ ).
A morphism α : T → T ′ between graded algebraic
theories is a family of mappings αn,m : Σn,m →′F T nm from operations in Σ to Σ′ -terms such thatthe equations in E are preserved by α, i.e. for eachT′Σs, t ∈ Tm(X), (s, t) ∈ E implies |s|(F X,α) =′T′|t|(F X,α) where (F T X, α) is a model of T induced by α.
Deﬁnition 23. Given a morphism α : T → T ′ , let′
F α : F T → F T be a naturaltransformation deT′
Σﬁned by F α ([t]) = |t|(F X,α) for each t ∈ Tm
(X).
Deﬁnition 24. We write GSM for the categoryof graded algebraic theories and morphisms between them. The identity morphisms are deﬁned
by 1T (f ) = [f (x1 , . . . , xn )] for each f ∈ Σn,m . The
composition of α : T → T ′ and β : T ′ → T ′′ isdeﬁned by β ◦ α(f ) = F β (α(f )).

3. 3 Examples
Example 25 (graded modules). Let M = (N, +, 0)
where N is regarded as a discrete category. GivenL
a graded ring A = n∈N An , let Σ be a set of operations which consists of the binary addition operation + (arity: 2, grade: 0), the unary inverse
operation − (arity: 1, grade: 0), the identity element (nullary operation) 0 (arity: 0, grade: 0) andthe unary scalar multiplication operation a · (−)(arity: 1, grade: n) for each a ∈ An . Let E be theequational axiom for modules.
A model (F, | · |) of the M-graded theory (Σ, E)
in [M, Set]0 consists of a set Fn for each n ∈ N
and functions |+|n : (Fn )2 → Fn , |−|n : Fn → Fn ,|0|n ∈ Fn and |a · (−)|n : Fn → Fm+n for eachn ∈ N and each a ∈ Am , and these interpretations
satisfy E. Therefore models of (Σ, E) in [M, Set]0
correspond one-to-one with graded modules.
Example 26 (graded exception monad [12, Example 3.4]). We give an algebraic presentation of thegraded exception monad.
Let M and (∗, η, µ) be a preordered monoid andthe graded monad deﬁned as follows. Let P + (X)denote the set of nonempty subsets of X. Let
Ex be a set of exceptions and M = ((P + (Ex ∪{Ok}), ⊆), I, ⊗) be a preordered monoid where I ={Ok} and the multiplication ⊗ is deﬁned by m ⊗m′ = (m \ {Ok}) ∪ m′ if Ok ∈ m and m ⊗ m′ = motherwise (note that this is not commutative). The
graded exception monad (∗, η, µ) is the M-gradedmonad given as follows.
m ∗ X = {Er(e) | e ∈ m \ {Ok}}∪ {Ok(x) | x ∈ X ∧ Ok ∈ m}
ηX (x) = Ok(x)µm1 ,m2 ,X (Er(e)) = Er(e)µm1 ,m2 ,X (Ok(x)) = x
The M-graded theory T ex for the graded exception monad is deﬁned by (Σex , ∅) where Σex is theset that consists of an operation raisee (arity: 0,
grade: {e}) for each e ∈ Ex.
The graded monad induced by T ex coincides withthe graded exception monad. Indeed, the freeexexmodel functor F T for T ex is given by F T Xm =m ∗ X. Here, the operations raisee are interpreted
by e ∈ Ex.
T ex|raisee |FmX= Er(e) ∈ F T

ex

X({e} ⊗ m)

Example 27 (extending an ordinary monad to an
M-graded monad). We consider the problem of extending an M′ -graded theory to an M-graded theory along a lax monoidal functor of type M′ → M,
but here we restrict ourselves to the case of M′ = 1
and the strict monoidal functor of type 1 → M.
Let M = (M, I, ⊗) be an arbitrary small strict
monoidal category. Let T = (Σ, E) be a (1-graded)theory and (T, η T , µT ) be the corresponding ordinary monad. Let T M = (ΣM , E M ) be the Mgraded theory obtained when we regard each operation in T as an operation with grade I ∈ M,
M
that is, ΣMn,m := Σn if m = I and Σn,m := ∅ otherMwise, and E := E.
M
The free model functor for T M is F T X =TT
F (M(I, −) × X) where F : Set → ModT (Set)is the free model functor for T as a 1-graded theory,and the interpretation of an operation f ∈ Σn inM
F T X is deﬁned by the interpretation in the freemodels of T .
TM

T

X
|f |F
= |f |F (M(I,m)×X)m
n
T: F (M(I, m) × X) → F T (M(I, m) × X)

Intuitively, this can be understood as follows.
Since all the operations are of grade I, coercions
cw in a term can be moved to the innermost
places where variables occur by repeatedly applyingcw (f (t1 , . . . , tn )) = f (cw (t1 ), . . . , cw (tn )) (see Definition 14). Therefore, we can consider terms ofT M as terms of T whose variables are of the formcw (x).
An M-graded monad (∗, η, µ) obtained from T M
is as follows.
m ∗ X = T (M(I, m) × X)
η = η T (1I , −)T
µ = T (⊗ × X) ◦ µ ◦ T st
Here, ⊗ : M(I, m1 )×M(I, m2 ) → M(I, m1 ⊗ m2 )is induced by ⊗: M × M → M and stX,Y :X × T Y → T (X × Y ) is the strength for T .

4 Graded Lawvere Theories
We present a categorical formulation of gradedalgebraic theories of §3 in a similar fashion to ordinary Lawvere theories.
For ordinary (single-sorted) ﬁnitary algebraic
theories, a Lawvere theory is deﬁned as a small category L with ﬁnite products together with a strictﬁnite-product preserving identity-on-objects func-

tor J : ℵop
0 → L where ℵ0 is the full subcategory of
Set on natural numbers. Intuitively, morphisms in
the Lawvere theory L are terms of the corresponding algebraic theory, and objects of L, which areexactly the objects in obℵ0 , are arities.
According to the above intuition, it is expectedthat a graded Lawvere theory is also deﬁned as acategory whose objects are natural numbers andmorphisms are graded terms. However, since terms
in a graded algebraic theory are stratiﬁed by amonoidal category M, mere sets are insuﬃcient
to express hom-objects of graded Lawvere theories.
Instead, we take hom-objects from the functor category [M, Set]0 and deﬁne graded Lawvere theories using [M, Set]0 -categories where [M, Set]0 is
equipped with the Day convolution monoidal structure. Speciﬁcally, ℵ0 (in ordinary Lawvere theories)
is replaced with an [M, Set]0 -category NM , L withan [M, Set]0 -category, and “ﬁnite products” with“Nop
M -cotensors”.
So, we ﬁrst provide an enriched category NM
that we use as arities. Since we do not assume
that M is symmetric, NM is deﬁned to be an[M, Set]0 t -category so that the opposite categoryt
Nop
M is an [M, Set]0 -category. Let [M, Set] be ant[M, Set]0 -category induced by the closed structureof [M, Set]0 t . That is, hom-objects of [M, Set]t are
given by [M, Set]t (G, H)m = [M, Set]0 (G, H(− ⊗m)).
Deﬁnition 28. An [M, Set]0 t -category NM isdeﬁned by the full sub-[M, Set]0 t -category of[M, Set]t whose set of objects is given by obNM ={n · y(I) | n ∈ N} ⊆ ob[M, Set]t where N is theset of natural numbers and n · y(I) is the n-foldcoproduct of y(I). We sometimes identify obNM
with N via the mapping n 7→ n := n · y(I).
op
Lemma 29. The [M, Set]0 -category Nop
M has NM cotensors, which are given by n ⋔ n′ = n · n′ foreach n and n′ .
Proof. A cotensor (n · y(I)) ⋔ (n′ · y(I)) is a tensor(n · y(I)) ⊗t (n′ · y(I)) in [M, Set]t . Since ⊗t isbiclosed, ⊗t preserves colimits in both arguments.
Therefore, (n·y(I)) ⊗t (n′ ·y(I)) ∼= (n·n′ )·y(I).
op
NM -cotensors (i.e. n · y(I) ⋔ C) behave like anenriched counterpart of ﬁnite powers (−)n . Weshow that Nop
M -cotensors in a general [M, Set]0 category A are characterized by projections satisfying a universal property. Given a unit morphism ν : n → A(n ⋔ C, C) of the cotensor n ⋔ C,

an [M, Set]0 -natural transformation ν : A(B, n ⋔C) → [n, A(B, C)] is given by f 7→ (x 7→ ν(x) ◦ f ).
The condition that ν is isomorphic can be rephrased
as follows.
Lemma 30. An [M, Set]0 -category A has Nop
Mcotensors if and only if for any n ∈ N and C ∈obA, there exist an object n ⋔ C ∈ obA and(π1 , . . . , πn ) ∈ (A(n ⋔ C, C)I)n such that the following condition holds: for each m, the function
f 7→ (π1 ◦ f, . . . , πn ◦ f ) of type A(B, n ⋔ C)m →(A(B, C)m)n is bijective.
An [M, Set]0 -functor F : A → B preserves Nop
M -cotensors if and only if (Fn⋔C,C,I ◦π1 , . . . , Fn⋔C,C,I ◦ πn ) ∈ (B(F (n ⋔ C), F C)I)nsatisﬁes the same condition for each n and C.
Proof. The essence of the proof is that the unit
morphism ν : n · y(I) → A(n ⋔ C, C)
corresponds to elements π1 , . . . , πn ∈ A(n ⋔C, C)I by [M, Set]0 (n · y(I), A(n ⋔ C, C)) ∼=A(n ⋔[M, Set]0 (y(I), A(n ⋔ C, C))n ∼=nC, C)I . The [M, Set]0 -natural transformation
ν is isomorphic if and only if each component
ν m : A(B, n ⋔ C)m → [n, A(B, C)] m of ν is isomorphic, which is moreover equivalent to the condition that f 7→ (π1 ◦ f, . . . , πn ◦ f ) : A(B, n ⋔C)m → (A(B, C))n is isomorphic since we have[n, A(B, C)] m ∼= (A(B, C)m)n .
The latter part of the lemma follows from theformer part.
If (π1 , . . . , πn ) ∈ (A(n ⋔ C, C)I)n satisﬁes
the condition in Lemma 30, we call the element
πi ∈ A(n ⋔ C, C)I the i-th projection of n ⋔ C.
Note that the choice of projections is not necessarily unique. However, when we say that A
is an [M, Set]0 -category with Nop
M -cotensors, we
implicitly assume that there are a chosen cotensor n ⋔ C and chosen projections (π1 , . . . , πn ) ∈(A(n ⋔ C, C)I)n for each n ∈ obNop
M and C ∈ obA.
We also assume that 1 ⋔ X = X without loss ofgenerality. Given n-tuple (f1 , . . . , fn ) of elementsin A(B, C)m, we denote by hf1 , . . . , fn i an element in A(B, n ⋔ C)m obtained by the inverseof f 7→ (π1 ◦ f, . . . , πn ◦ f ) and call this a tupling.
Tuplings and projections for Nop
M -cotensors behave
like those for ﬁnite products.
The following proposition claims that Nop
M is afree [M, Set]0 -category with chosen Nop-cotensors
M
generated by one object.
Proposition 31. Let A be an [M, Set]0 -category

with Nop
M -cotensors and C be an object in A.
Then there exists a unique Nop
M -cotensor preserving [M, Set]0 -functor F : Nop
M → A such thatF n = n ⋔ C and F πi = πi .
We deﬁne M-graded Lawvere theories in a similar fashion to enriched Lawvere theories.
Deﬁnition 32. An M-graded Lawvere theory is atuple (L, J) where L is an [M, Set]0 -category withopNop
M -cotensors and J : NM → L is an identity-onop
objects NM -cotensor preserving [M, Set]0 -functor.
A morphism F : (L, J) → (L′ , J ′ ) between two
graded Lawvere theories is an [M, Set]0 -functor
F : L → L′ such that F J = J ′ . We denote the category of graded Lawvere theories and morphisms
between them by GLawM .
By Proposition 31, the existence of the above
J : Nop
M → L is equivalent to requiring thatobL = N and projections in L are chosen in someway. So, we sometimes leave J implicit and justwrite L ∈ GLawM for (L, J) ∈ GLawM .
Deﬁnition 33. A model of graded Lawvere theory
L in an [M, Set]0 -category A with Nop
M -cotensor
is an Nop
-cotensor
preserving[M,Set]-functor of0Mtype L → A. A morphism α : F → G between
two models F, G of graded Lawvere theory L is an[M, Set]0 -natural transformation. Let Mod(L, A)
be the category of models of graded Lawvere theory
L in the [M, Set]0 -category A.
In §3, we use a category C satisfying M-model
condition to deﬁne a model of graded algebraic theory. Actually, M-model condition is suﬃcient togive an [M, Set]0 -category with Nop
M -cotensors.
Lemma 34. If C satisﬁes M-model condition,
opgthen the [M, Set]0 -category C
deﬁned in DeﬁT
nition 7 has Nop-cotensors.
M
opg
Proof. For any X ∈ C
and n, the cotensor
Tn ⋔ X is given by ﬁnite power X n , and the i-th
opgprojection is given by η ⊛ ◦ πi ∈ C
I whereTnπi : X → X is the i-th projection of the ﬁnite
power X n . The rest of the proof is routine.
If we apply Lemma 34 to [M, Set]0 equippedwith the Mt -action in Example 9 (here denotedopby T ), then ([M,^Set]0 )T coincides with [M, Set]
(i.e. the [M, Set]0 -category obtained by the closed
structure of [M, Set]0 ).

5 Equivalence
We have shown three graded notions: graded algebraic theories, graded Lawvere theories and ﬁnitary graded monads, which give rise to categories
GSM , GLawM and GMndM , respectively. Thissection is about the equivalence of these three notions. We give only a sketch of the proof of theequivalence, and the details are deferred to [14, Appendix A].
5. 1 Graded Algebraic Theories and Graded
Lawvere Theories
We prove that the category of graded algebraic
theories GSM and the category of graded Lawvere theories GLawM are equivalent by showing
the existence of an adjoint equivalence Th ` U :GLawM → GSM .
Let M be a small strict monoidal category andT = (Σ, E) be an M-graded algebraic theory. We
deﬁne ThT (the object part of Th) as an M-graded
Lawvere theory whose morphisms are terms of T
modulo equational axioms.
Deﬁnition 35. An [M, Set]0 -category ThT is deﬁned by ob(ThT ) := N and (ThT )(n, n′ )m :=′(F T nm)n with composition deﬁned by substitution.
It is easy to show that ThT has Nop
M -cotensors(by Lemma 30). Therefore, Th is a mapping froman object in GSM to an object in GLawM .
We deﬁne a functor U : GLawM → GSM by taking all the morphism f ∈ L(n, 1)m in L ∈ GLawM
as operations and all the equations that hold in L
as equational axioms.
Deﬁnition 36. A functor U : GLawM → GSM
is deﬁned as follows.
• For each L ∈ obGLawM , U L = (Σ, E) whereΣn,m = L(n, 1)m, E = {(s, t) | |s|L = |t|L }Σ
and | · |L : Tm(n) → L(n, 1)m is an interpretation of terms deﬁned in the same way as Deﬁnition 11.
• Given G : L → L′ , let U G : U L → U L′ be afunctor deﬁned by U G(f ) = [G(f )(x1 , . . . , xn )]for each f ∈ L(n, 1)m.
Then, ThT has the following universal property
as a left adjoint of U .
Lemma 37. For each T , let ηT : T → U ThT be afamily of functions ηT ,n,m : Σn,m → F U ThT nm de-ﬁned by ηT ,n,m (f ) = [[f (x1 , . . . , xn )](x1 , . . . , xn )].
For any α : T → U L, there exists a unique morphism α : ThT → L such that α = U α ◦ ηT .
Moreover, the unit and the counit of Th a U are
isomorphic. Therefore:
Theorem 38. Two categories GSM and GLawM
are equivalent.
We can also prove the equivalence of the categories of models.
Lemma 39. If C is a category satisfying Mmodel condition, then ModT (C) is equivalent totgMod(ThT , C
T ) where T is the M -action onC.
5. 2 Graded Lawvere theories and Finitary Graded Monads
We prove that the category of graded Lawvere theories GLawM and the category of ﬁnitary
graded monads GMndM are equivalent. Given a
graded Lawvere theory, a ﬁnitary graded monad is
obtained as a coend that represents the set of terms.
On the other hand, given a ﬁnitary graded monad,a graded Lawvere theory is obtained from taking
the full sub-[M, Set]0 -category on arities ob(NopM)
of the opposite category of the Kleisli(-like) category in Deﬁnition 7. These constructions give riseto an equivalence of categories.
An M-graded Lawvere theory yields a ﬁnitary
graded monad by letting m ∗ X be the set of termsof grade m whose variables range over X.
Deﬁnition 40. Let L be an M-graded Lawvere
theory. We deﬁne TL = (∗, η, µ) by a (ﬁnitary)
M-graded monad whose functor part is given as
follows.
Z n∈ℵ0m ∗ X :=
L(n, 1)m × X n
Note that L(−, 1) : ℵ0 → [M, Set]0 is a Setfunctor here.
Given a graded monad, a graded Lawvere theory
is obtained as follows.
Deﬁnition 41. Let T = (∗, η, µ) be an M-gradedmonad on Set. Let LT be the full sub-[M, Set]0 ]T )op with ob(LT ) = N.
category of (Set
Since LT has NM -cotensors n ⋔ 1 = n whose projections are given by πi = (∗ 7→ η(i)) ∈ Set(1, I∗n),
LT is a graded Lawvere theory.
Given a morphism α : T → T ′ in GMndM ,we deﬁne Lα : LT → LT ′ by (Lα )n,n′ ,m =Set(n′ , αn,m ) : LT (n, n′ )m → LT ′ (n, n′ )m. It iseasy to prove that Lα is a morphism in GLawM
and L(−) : GMndM → GLawM is a functor.
Theorem 42. Two categories GLawM and
GMndM are equivalent.
Proof. L(−) is an essentially surjective fully faithful
functor.

6 Combining Eﬀects
Under the correspondence to algebraic theories,
combinations of computational eﬀects can be understood as combinations of algebraic theories. In
particular, sums and tensor products are wellknown constructions [9]. In this section, we showthat these constructions can be adapted to gradedalgebraic theories. By the equivalence GMndM 'GLawM ' GSM in §5, constructions like sums
and tensor products in one of these categories induce those in the other two categories. So, wechoose GSM and describe sums as colimits in
GSM and tensor products as a mapping GSM1 ×
GSM2 → GSM1 ×M2 .
6. 1 Sums
We prove that GSM has small colimits.
Lemma 43. The category GSM has small coproducts.
Proof. Given a family {(Σ(i) , E (i) )}i∈I of objects in GSM , the coproduct is obtained by
the disjoint union of operations and equations:
`
S
(i)
(i)
(i) S
(i)
)=
.
i∈I (Σ , Ei∈I Σ ,i∈I E
Lemma 44. The category GSM has coequalizers.
Proof. Let T = (Σ, E) and T ′ = (Σ′ , E ′ ) be
graded algebraic theories and α, β : T → T ′ bea morphism. The coequalizer T ′′ of α and β is
given by adding the set of equations induced by α
and β to T ′ , that is, T ′′ := (Σ′ , E ′ ∪ E ′′ ) where
E ′′ = {(s, t) | ∃f ∈ Σ, α(f ) = [s] ∧ β(f ) = [t]}.
Since a category has all small colimits if and only
if it has all small coproducts and coequalizers, we
obtain the following corollary.
Corollary 45. Three equivalent categories GSM ,GMndM and GLawM are cocomplete.
Example 46. It is known that the sum of an ordinary monad T and the exception monad (−) + Ex
(where Ex is a set of exceptions) is given by
T ((−) + Ex) [9, Corollary 3]. We show that a similar result holds for the graded exception monad.
Let T ex be the theory in Example 26 and M
be the preordered monoid used there. We denote(∗ex , η ex , µex ) for the graded exception monad. Let
T = (Σ, E) be a (1-graded) theory and (T, η T , µT )be the corresponding ordinary monad. Let T M =(ΣM , E M ) be the M-graded theory obtained fromT as in Example 27. We consider a graded monadobtained as the sum of T ex and T M .
A free model functor F for T ex + T M is given
by F Xm = T (m ∗ex X). For each n-ary operaX
extion f in T , |f |FX))n → T (m ∗ex X)
m : (T (m ∗is induced by free models of T , and for eachX
e ∈ Ex, |raisee |F: 1 → T ({e} ∗ex X) is dem
Tﬁned by η{e}∗ex X (e) ∈ T ({e} ∗ex X). It is easy
to see that F X deﬁned above is indeed a model ofT ex + T M . Therefore, we obtain a graded monadm ∗ X = T (m ∗ex X).
6. 2 Tensor Products
The tensor product of two ordinary algebraic
theories (Σ, E) and (Σ′ , E ′ ) is constructed as(Σ ∪ Σ′ , E ∪ E ′ ∪ E⊗ ) where E⊗ consists off (λi.g(λj.xij )) = g(λj.f (λi.xij )) for each f ∈ Σ
and g ∈ Σ′ . However, when we extend tensor products to graded algebraic theories, the grades of theboth sides are not necessarily equal. If the gradeof f is m and the grade of g is m′ , then the gradesof f (λi.g(λj.xij )) and g(λj.f (λi.xij )) are m ⊗ m′
and m′ ⊗ m, respectively. Therefore, we have tosomehow guarantee that the grade of f ∈ Σ and thegrade of g ∈ Σ′ commute. We solve this problem bytaking the product of monoidal categories. That is,
we deﬁne the tensor product of an M1 -graded algebraic theory and an M2 -graded algebraic theory
as an M1 × M2 -graded algebraic theory.
Before deﬁning tensor products, we consider extending an M-graded theory to M′ -graded theory
along a lax monoidal functor G = (G, η G , µG ) :M → M′ . Given an M-graded theory T =(Σ, E), we deﬁne the M′ -graded theory G∗ T =(G∗ Σ, G∗ E) by (G∗ Σ)n,m′ := {f ∈ Σn,m | Gm =m′ } and G∗ E := {G∗ (s) = G∗ (t) | (s = t) ∈E} where for each term t of T (with grade m),G∗ (t) is the term of G∗ T (with grade Gm) deﬁned inductively as follows: if x is a variable, thenG∗ (x) := cηG (x); for each w : m → m′ and termt, G∗ (cw (t)) := cGw (G∗ (t)); for each f ∈ Σn,m andterms t1 , . . . , tn with grade m′ , G∗ (f (t1 , . . . , tn )) :=cµG ′ (f (G∗ (t1 ), . . . , G∗ (tn ))).
m,m
The tensor product of T1 ∈ GSM1 and T2 ∈ GSM2

is deﬁned by ﬁrst extending T1 and T2 to M1 ×M2 graded theories and then adding commutation
equations.
Deﬁnition 47 (tensor product). Let T1 =(Σ, E) ∈ GSM1 and T2 = (Σ′ , E ′ ) ∈ GSM2 .
The tensor product T1 ⊗ T2 is deﬁned by (K∗ Σ ∪K∗′ Σ′ , K∗ E ∪ K∗′ E ′ ∪ ET1 ⊗T2 ) ∈ GSM1 ×M2 where
K : M1 → M1 × M2 and K ′ : M2 → M1 × M2 arelax monoidal functors deﬁned by Km1 := (m1 , I2 )and K ′ m2 := (I1 , m2 ), andET1 ⊗T2 := {f (λi.g(λj.xij )) = g(λj.f (λi.xij ))| f ∈ (K∗ Σ)n,m , g ∈ (K∗′ Σ′ )n′ ,m′ }.
That is, if f is an operation in T1 with grade
m1 ∈ M1 , then T1 ⊗ T2 has the operation f withgrade (m1 , I2 ) ∈ M1 × M2 and similarly for operations in T2 .
The tensor products satisfy the following fundamental property.
Proposition 48. Let C be a category satisfying
M1 ×M2 -model condition. Let Ti be an Mi -gradedalgebraic theory for i = 1, 2. Then we have an isomorphism ModT1 (ModT2 (C)) ∼= ModT1 ⊗T2 (C).
Proof. Let ((A, | · |′ ), | · |) ∈ ModT1 (ModT2 (C)) be amodel. For each operation f in T1 , |f | : (A, |·|′ )n →m ⊛ (A, | · |′ ) is a homomorphism. This condition is equivalent to satisfying the equations in
ET1 ⊗T2 .
Example 49. We exemplify the tensor product byshowing a graded version of [9, Corollary 6], whichclaims that the L-fold tensor product of the sideeﬀects theory in [21] with one location is the sideeﬀects theory with L locations.
First, we consider the situation where there is
only one memory cell whose value ranges over aﬁnite set V . Let 2 the preordered monoid (joinsemilattice) ({⊥, >}, ≤, ∨, ⊥) where ≤ is the preorder deﬁned by ⊥ ≤ >. Intuitively, ⊥ represents pure computations, and > represents (possibly) stateful computations. Let Tst be a 2-gradedtheory of two types of operations lookup (arity: V ,grade: >) and updatev (arity: 1, grade: >) for eachv ∈ V and the four equations in [21] for the interaction of lookup and update. Note that we have toinsert coercion to arrange the grade of the equation
lookup(λv ∈ V.updatev (x)) = c⊥≤⊤ (x).
The graded monad (∗, η, µ) induced by Tst is asfollows.

⊥∗X =X> ∗ X = (V × X)V((⊥ ≤ >) ∗ X)(x) = λv.(v, x)
The middle equation can be explained as follows:
any term with grade > can be presented by a canonical form tf := lookup(λv.updatefV (v) (fX (v)))
where f = hfV , fX i : V → V × X is a function,and therefore, the mapping f 7→ tf gives a bijection between (V × X)V and > ∗ X = T⊤Σ (X)/∼.
The L-fold tensor product of Tst , which we denote by Tst⊗L , is a 2L -graded theory where 2L =(2L , ⊆, ∪, ∅) is the join-semilattice of subsets of L.
Speciﬁcally, Tst⊗L consists of operations lookupl andupdatel,v with grade {l} for each l ∈ L and v ∈V with additional three commutation equationsin [21]. The induced graded monad is L′ ∗⊗L X ={f : V L → (V L × X) | read(L′ , f ) ∧ write(L′ , f )}where L′ ⊆ L, and read(L′ , f ) and write(L′ , f ) assert that f depends only on values at locations in
L′ and does not change values at locations outside
L′ . That is, L′ ∗⊗L X represents computations thattouch only memory locations in L′ .
read(L′ , f ) := ∀σ, σ ′ ∈ V n , (∀l ∈ L′ , σ(l) = σ ′ (l))=⇒ f (σ) = f (σ ′ )write(L′ , f ) := ∀σ, σ ′ ∈ V n , x ∈ X, (σ ′ , x) = f (σ)=⇒ ∀l ∈
/ L′ , σ(l) = σ ′ (l)7 Related Work
Algebraic theories for graded monads.
Graded monads are introduced in [27], and notions of graded theory and graded Eilenberg–Moore
algebra appear in [17] [4] for coalgebraic treatmentof trace semantics. However, these work only deal
with N-graded monads where N is regarded as adiscrete monoidal category, while we deal with general monoidal categories. The Kleisli construction
and the Eilenberg–Moore construction for gradedmonads are presented in [7] by adapting the 2categorical argument on resolutions of monads [29].
Algebraic operations for graded monads are introduced in [12] and classiﬁed into two types, which
are diﬀerent in how to integrate the grades of subterms. One is operations that take terms with thesame grade, and these are what we treated in thispaper. The other is operations that take terms with
diﬀerent grades: the grade of f (t1 , . . . , tn ) is deter-

mined by an eﬀect function ϵ : Mn → M associatedto f . Although the latter type of operations is also
important to give natural presentations of computational eﬀects, we leave it for future work.
Enriched Lawvere theories.
There are many variants of Lawvere theories [1,10, 11, 15, 16, 19, 24, 25, 28], and most of them share
a common pattern: they are deﬁned as an identityon-objects functor from a certain category (e.g.,ℵop0 ) which represents arities, and the functor must
preserve a certain class of products (or cotensors
if enriched). Among the most relevant work toours are enriched Lawvere theories [24] and discrete
Lawvere theories [10].
For a given monoidal category V, a Lawvere Vtheory is deﬁned as an identity-on-objects ﬁnite
cotensor (i.e. Vfp -cotensor) preserving Vt -functorop
J : Vfp→ L where Vfp is the full subcategoryof V spanned by ﬁnitely presentable objects. If
V = [M, Set]0 t , Lawvere [M, Set]0 t -theories areanalogous to our graded Lawvere theories exceptthat we used Nop
M instead of ([M, Set]0 )fp . Sincen · y(I) ∈ Nop
isﬁnitely presentable, we can say
Mthat the notion of graded Lawvere theory is obtained from enriched Lawvere theories by restricting arities to Nop
M ⊆ ([M, Set]0 )fp . However, thecorrespondence to ﬁnitary graded monads on Set isan interesting point of our graded Lawvere theories
compared to Lawvere V-theories, which correspondto ﬁnitary V-monads on V.
Discrete Lawvere theories restrict arities of Lawvere V-theories to ℵ0 , that is, a discrete Lawvere V-theory is deﬁned as a (Set-enriched) ﬁniteproduct preserving functor J : ℵop→ L0 where0
L is a Vt -category. Actually, discrete Lawvere[M, Set]0 t -theories are equivalent to graded Lawvere theories because there is a ﬁnite-product preop
serving functor ι : ℵop
0 → NM such that the composition with ι gives a bijection between graded Lawvere theories J : Nop
M → L and discrete Lawvere[M, Set]0 t -theories J0 ◦ ι : ℵop
0 → L0 . However, weconsidered not only symmetric monoidal categories
but also nonsymmetric ones, which cause a nontrivial problem when we deﬁne tensor products of algebraic theories. The problem is that adding commutation equations requires some kind of commutativity of monoidal categories. We solved this problem
by considering product monoidal categories anddeﬁning the tensor product of an M1 -graded theory

and an M2 -graded theory as an M1 × M2 -gradedtheory, and the use of two diﬀerent monoidal categories is new to the best of our knowledge.

8 Conclusions and Future WorkTo extend the correspondence between algebraic
theories, Lawvere theories, and (ﬁnitary) monads,
we introduced notions of graded algebraic theory
and graded Lawvere theory and proved their correspondence with ﬁnitary graded monads. We also
provided sums and tensor products for graded algebraic theories, which are natural extensions of thosefor ordinary algebraic theories. Since we do not assume monoidal categories to be symmetric, our tensor products are a bit diﬀerent from the ordinary
ones in that this combines two theories graded by(or enriched in) diﬀerent monoidal categories. We
hope that these results will lead us to apply manykinds of techniques developed for monads to gradedmonads.
As future work, we are interested in “changeof-eﬀects”, that is, changing the monoidal category M in M-graded algebraic theory along a (lax)monoidal functor F : M → M′ . The problem already appeared in §6. 2 to deﬁne tensor products,
but we want to look for more properties of thisoperation. We are also interested in integrating
a more general framework for notions of algebraic
theory [6] and obtaining a graded version of theframework. Another direction is exploiting models of graded algebraic theories as modalities in the
study of coalgebraic modal logic [4, 17] or weakest
precondition semantics [8].
Acknowledgement. We thank Soichiro Fujii,
Shin-ya Katsumata, Yuichi Nishiwaki, Yoshihiko
Kakutani and the anonymous referees for usefulcomments. This work was supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).
References[ 1 ] Berger, C., Melliès, P.-A., and Weber, M.:
Monads with arities and their associated theories,
Journal of Pure and Applied Algebra, Vol. 216,
No. 8(2012), pp. 2029 – 2048. Special Issue devoted
to the International Conference in Category Theory‘CT2010’.
[ 2 ] Curien, P., Fiore, M. P., and MunchMaccagnoni, G.: A theory of eﬀects and resources:

adjunction models and polarised calculi, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Bodı́k, R. and Majumdar,R.(eds.), ACM, 2016, pp. 44–56.
[ 3 ] Day, B.: On closed categories of functors, Reports of the Midwest Category Seminar IV, Lecture
Notes in Mathematics, Vol. 137, Berlin, Heidelberg,
Springer, 1970, pp. 1–38.
[ 4 ] Dorsch, U., Milius, S., and Schröder, L.: Graded
Monads and Graded Logics for the Linear Time Branching Time Spectrum, 30th International Conference on Concurrency Theory, CONCUR 2019,
August 27-30, 2019, Amsterdam, the Netherlands,
Fokkink, W. and van Glabbeek, R.(eds.), LIPIcs,
Vol. 140, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2019, pp. 36:1–36:16.
[ 5 ] E. J. Linton, F.: Some Aspects of Equational
Categories, Proceedings of the Conference on Categorical Algebra, 01 1966, pp. 84–94.
[ 6 ] Fujii, S.: A uniﬁed framework for notions of algebraic theory, 2019.
[ 7 ] Fujii, S., Katsumata, S., and Melliès, P.: Towards a Formal Theory of Graded Monads, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS
2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS
2016, Eindhoven, The Netherlands, April 2-8,
2016, Proceedings, Jacobs, B. and Löding, C.(eds.),
Lecture Notes in Computer Science, Vol. 9634,
Springer, 2016, pp. 513–530.
[ 8 ] Hasuo, I.: Generic weakest precondition semantics from monads enriched with order, Theor. Comput. Sci., Vol. 604(2015), pp. 2–29.
[ 9 ] Hyland, M., Plotkin, G. D., and Power, J.: Combining eﬀects: Sum and tensor, Theor. Comput.
Sci., Vol. 357, No. 1-3(2006), pp. 70–99.
[10] Hyland, M. and Power, J.: Discrete Lawvere theories and computational eﬀects, Theoretical Computer Science, Vol. 366, No. 1(2006), pp. 144 – 162.
Algebra and Coalgebra in Computer Science.
[11] Hyland, M. and Power, J.: The Category Theoretic Understanding of Universal Algebra: Lawvere
Theories and Monads, Electronic Notes in Theoretical Computer Science, Vol. 172(2007), pp. 437–458.
Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin.
[12] Katsumata, S.: Parametric eﬀect monads andsemantics of eﬀect systems, The 41st Annual ACM
SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL ’14, San Diego,
CA, USA, January 20-21, 2014, Jagannathan, S.
and Sewell, P.(eds.), ACM, 2014, pp. 633–646.
[13] Kelly, M.: Basic Concepts of Enriched Category
Theory, Lecture note series / London mathematicalsociety, Cambridge University Press, 1982.

[14] Kura, S.: Graded Algebraic Theories, 2020.
[15] Lack, S. and Power, J.: Gabriel-Ulmer duality
and Lawvere theories enriched over a general base,
Journal of Functional Programming, Vol. 19, No. 34(2009), pp. 265–286.
[16] Lucyshyn-Wright, R. B. B.: Enriched algebraic theories and monads for a system of arities,
Theory and Applications of Categories, Vol. 31,
No. 5(2016), pp. 101–137.
[17] Milius, S., Pattinson, D., and Schröder, L.:
Generic Trace Semantics and Graded Monads, 6th
Conference on Algebra and Coalgebra in Computer
Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands, Moss, L. S. and Sobocinski, P.(eds.), LIPIcs, Vol. 35, Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2015, pp. 253–
269.
[18] Moggi, E.: Computational Lambda-Calculus
and Monads, Proceedings of the Fourth Annual
Symposium on Logic in Computer Science (LICS’89), Paciﬁc Grove, California, USA, June 5-8,
1989, IEEE Computer Society, 1989, pp. 14–23.
[19] Nishizawa, K. and Power, J.: Lawvere theories
enriched over a general base, Journal of Pure andApplied Algebra, Vol. 213, No. 3(2009), pp. 377 –
386.
[20] Plotkin, G. D. and Power, J.: Adequacy for
Algebraic Eﬀects, Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Partof the Joint European Conferences on Theory andPractice of Software, ETAPS 2001 Genova, Italy,
April 2-6, 2001, Proceedings, Honsell, F. and Miculan, M.(eds.), Lecture Notes in Computer Science,Vol. 2030, Springer, 2001, pp. 1–24.
[21] Plotkin, G. D. and Power, J.: Notions of Com-

putation Determine Monads, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as
Part of the Joint European Conferences on Theory
and Practice of Software, ETAPS 2002 Grenoble,
France, April 8-12, 2002, Proceedings, Nielsen, M.
and Engberg, U.(eds.), Lecture Notes in Computer
Science, Vol. 2303, Springer, 2002, pp. 342–356.
[22] Plotkin, G. D. and Pretnar, M.: A Logic for
Algebraic Eﬀects, Proceedings of the Twenty-Third
Annual IEEE Symposium on Logic in Computer
Science, LICS 2008, 24-27 June 2008, Pittsburgh,
PA, USA, IEEE Computer Society, 2008, pp. 118–
129.
[23] Plotkin, G. D. and Pretnar, M.: Handling Algebraic Eﬀects, Logical Methods in Computer Science,Vol. 9, No. 4(2013).
[24] Power, J.: Enriched Lawvere Theories, Theory
and Applications of Categories, Vol. 6, No. 7(1999),
pp. 83–93.
[25] Power, J.: Countable Lawvere Theories andComputational Eﬀects, Electr. Notes Theor. Comput. Sci., Vol. 161(2006), pp. 59–71.
[26] Sankappanavar, H. P. and Burris, S.: A course
in universal algebra, Springer-Verlag, 1981.
[27] Smirnov, A.: Graded monads and rings ofpolynomials, Journal of Mathematical Sciences,Vol. 151, No. 3(2008), pp. 3032–3051.
[28] Staton, S.: Freyd categories are Enriched Lawvere Theories, Electronic Notes in Theoretical Computer Science, Vol. 303(2014), pp. 197 – 206. Proceedings of the Workshop on Algebra, Coalgebra
and Topology (WACT 2013).
[29] Street, R.: The formal theory of monads,
Journal of Pure and Applied Algebra, Vol. 2,
No. 2(1972), pp. 149 – 168.