key: cord-0054925-8dw472ks authors: Kura, Satoshi title: Graded Algebraic Theories date: 2020-04-17 journal: Foundations of Software Science and Computation Structures DOI: 10.1007/978-3-030-45231-5_21 sha: a407a7b77ee9dc08623d218baf5994f18a1fa8a9 doc_id: 54925 cord_uid: 8dw472ks 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 finitary graded monads are equivalent via equivalence of categories, which extends the equivalence for monads. We also give sums and tensor products of graded algebraic theories to combine computational effects as an example of importing techniques based on algebraic theories to graded monads. In the field of denotational semantics of programming languages, monads have been used to express computational effects since Moggi's seminal work [18] . They have many applications from both theoretical and practical points of view. Monads correspond to algebraic theories [5] . This correspondence gives natural presentations of many kinds of computational effects by operations and equations [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 effects [23] . Graded monads [27] are a refinement of monads and defined as a monadlike 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 some kind of "abstraction" of effectful computations. For example, graded monads are used to give denotational semantics of effect systems [12] , which are type systems designed to estimate scopes of computational effects caused by programs. f ∈ Σ n,m t i ∈ T Σ m (X) for each i ∈ {1, . . . , n} f (t 1 , . . . , t n ) ∈ T Σ m⊗m (X) This paper provides a graded extension of algebraic theories that corresponds to monads graded by small strict monoidal categories. This generalizes Ngraded theories in [17] . The main ideas of this extension are the following. First, we assign to each operation a grade, i.e., an object in a monoidal category that represents effects. Second, our extension provides a mechanism (Fig 1) to keep track of effects in the same way as graded monads. That is, if an operation f with grade m is applied to terms with grade m , then the grade of the whole term is the product m ⊗ m . For example, graded algebraic theories enable us to estimate (an overapproximation of) the set of memory locations computations may access. The sideeffects theory [21] is given by operations lookup l and update l,v for each location l ∈ L and value v ∈ V together with several equations, and each term represents a computation with side-effects. Since lookup l and update l,v only read from or write to the location l, we assign {l} ∈ 2 L as the grade of the operations in the graded version of the side-effects theory where 2 L is the join-semilattice of subsets of locations L. The grade of a term is (an overapproximation of) the set of memory locations the computations may access thanks to the rule in Fig 1. We also provide graded Lawvere theories that correspond to graded algebraic theories. The intuition of a Lawvere theory is a category whose arrows are terms of an algebraic theory. We use this intuition to define 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 computational effects, we expect that the proposed graded algebraic theories will do the same for effect 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 theories of [17] to M-graded algebraic theories and also provide M-graded Lawvere theories where M is a small strict monoidal category. We show that there exist translations between these notions and finitary graded monads, which yield equivalences of categories. -We extend sums and tensor products of algebraic theories [9] to graded algebraic theories. We define sums in the category of M-graded algebraic 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 of these constructions. We review enriched category theory and introduce notations. See [13] for details. Let V 0 = (V 0 , ⊗, I) be a (not necessarily symmetric) monoidal category. t is right closed if and only if V 0 is left closed. We define V 0 -category, V 0 -functor and V 0 -natural transformation as in [13] . If V 0 is right closed, then V 0 itself enriches to a V 0 -category V with homobject given by V(X, Y ) := [X, Y ]. We use the subscript (−) 0 to distinguish the enriched category V from its underlying category V 0 . Assume that V 0 is biclosed and let A be a V 0 -category. The opposite cat- For each X ∈ V 0 and C ∈ A, a tensor X ⊗ C is an object in A together with a counit morphism ν : For example, if V 0 = Set, then tensors X ⊗ C are copowers X · C, and cotensors X C are powers C X . for each X ∈ Φ and C ∈ obA. We review the notion of graded monad in [12, 7] , and then define the category GMnd M of finitary M-graded monads. Throughout this section, we fix a small strict monoidal category M = (M, ⊗, I). Definition 1 (graded monads). An M-graded monad 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-graded monad is a tuple ( * , η, µ) of a functor * : M × C → C and natural transformations η X : X → I * X and µ m1,m2,X : m 1 * (m 2 * X) → (m 1 ⊗ m 2 ) * X such that the following diagrams commute. A morphism of M-graded monad is a monoidal natural transformation α : ( * , η, µ) → ( * , η , µ ), i.e. a natural transformation α : * → * that is compatible with η and µ. An intuition of graded monads is a refinement of monads: m * X is a computation whose scope of effect is indicated by m and whose result is in X. The monoidal category M defines the granularity of the refinement, and a 1-graded monad is just an 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 25. A finitary functor is a functor that preserves filtered colimits. In this paper, we focus on finitary graded monads on Set. A morphism in GMnd M 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 finitary M-graded monads. There exists one-to-one correspondence between the following. is the inclusion functor) such that the following diagrams commute for each n, n ∈ ℵ 0 , m 1 , m 2 ∈ M and f : n → m 2 * n . Proof. By the equivalence [Set, Set] f [ℵ 0 , Set] induced by restriction and the left Kan extension along the inclusion i : ℵ 0 → Set. We describe a monoidal biclosed structure on the (covariant) presheaf category Note that since we do not assume M to be symmetric, neither is [M, Set] 0 . Note also that the twisting and the above construction commute: there is an isomorphism [M, Set] 0 t ∼ = [M t , Set] 0 of monoidal categories. We rephrase the definitions of [M, Set] 0 -enriched category, functor and natural transformation in elementary terms. An [M, Set] 0 -category is, so to say, an "Mgraded" 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 -natural transformations can be also understood as an "M-graded" version of ordinary functors and natural transformations. Specifically, the following lemma holds [2] . There is a one-to-one correspondence between (1) an [M, Set] 0category C and (2) the following data satisfying the following conditions. -A class of objects obC. -For each X, Y ∈ obC, a hom objects -For each X ∈ obC, an element 1 X ∈ C(X, X)I. -For each X, Y, Z ∈ obC, a family of morphisms • m1,m2 : These data must satisfy the identity law Proof. The identity 1 X : y(I) → C(X, X) in C corresponds to 1 X ∈ C(X, X)I by the Yoneda lemma, and the composition • : The definition of C T is similar to the definition of the Kleisli categories for ordinary monads. Actually, C T can be constructed via the Kleisli category C T for the graded monad T presented in [7] (although C T itself is not enriched). This can be observed by C T ((I, X), (m, Y )) ∼ = C T (X, Y )m. We explain a framework of universal algebra for graded monads, which is a natural extension of [27, 17] . The key idea of this framework is that each term is associated with not only an arity but also a "grade", which is represented by an object in a 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 of variables X and returns the set of terms with grade m (modulo the equational axioms) yields a graded monad. We fix a small strict monoidal category M = (M, ⊗, I) throughout this section. We sometimes identify n ∈ N with {1, . . . , n}, or {x 1 , . . . , x n } if it is used as a set of variables. 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 define a sufficient structure to interpret operations in a category C as follows. Definition 8. M-model condition is defined by the following conditions on a tuple (C, ( , η , µ )). -C is a category with finite power. -( , η , µ ) is a strong M t -action (i.e. an M t -graded monad whose unit and multiplication are invertible). A model A = (A, | · | A ) of Σ in a category C satisfying M-model condition consists of an object A ∈ C and an interpretation |f Definition 10. Let X be a set of variables. The set of (M-graded) Σ-terms T Σ m (X) for each m ∈ M is defined inductively as follows. That is, we build Σ-terms from variables by applying operations in Σ and coercions c w while keeping track of the grade of terms. When applying operations, Definition 11. Let A be a model of a signature Σ. For each m ∈ M and s ∈ T Σ m (n), the interpretation |s| A : A n → m A is defined as follows. -For any variable When we interpret a term t ∈ T Σ m (X), we need to pick a finite set n such that fv(t) ⊆ n ⊆ X where fv(t) is the set of free variables in t, but the choice of the finite set does not matter when we consider only equality of interpretations by the following fact. If σ : n → n is a renaming of variables and σ : T Σ m (n) → T Σ m (n ) is a mapping induced by the renaming σ, then for each t ∈ T Σ m (n), |σ(t)| A = |t| A • A σ , which implies that equality of the interpretations of two terms s, t is preserved by renaming: |s| = |t| implies |σ(s)| = |σ(s)|. An equational axiom is a family of sets E = (E m ) m∈M where E m is a set of pairs of terms in T Σ m (X). We sometimes identify E with its union m∈M E m . A presentation of an M-graded algebraic theory (or an M-graded algebraic theory) is a pair T = (Σ, E) of a signature and an equational axiom denote the category of models of T in C and homomorphisms between them. To obtain a graded monad on Set from T , we need a strict left action of M on Mod T ([M, Set] 0 ) and an adjunction between Mod T ([M, Set] 0 ) and Set. The former is defined by the following, while the latter is described in §3.2. Proof. for M-graded Σ-terms can be defined as usual, but we have to take care of grades: given s ∈ T Σ m (k) and t 1 , . . . , t k ∈ T Σ m (n), the substitution s[t 1 /x 1 , . . . , t k /x k ] is defined as a term in T Σ m⊗m (n). We obtain an equational logic for graded theories by adding some additional rules to the usual equational logic. Definition 14. The entailment relation T s = t (where s, t ∈ T m (X)) for an M-graded theory T is defined by adding the following rules to the standard rules i.e. reflexivity, symmetry, transitivity, congruence, substitution and axiom in E (see e.g. [26] for the standard rules of equational logic). It is easy to verify that the equational logic in Definition 14 is sound. We describe a construction of a free model F T X ∈ Mod T ([M, Set] 0 ) of a graded theory T generated by a set X, which induces an adjunction between Mod T ([M, Set] 0 ) and Set. This adjunction, together with the M-action of Corollary 13, gives a graded monad as described in [7] . The model F T X, together with the mapping η X : X → F T XI defined by x → [x] I , has the following universal property as a free model generated by X. By considering the interpretation in the free model, we obtain the following completeness theorem. Recall that Mod T ([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 Mod T ([M, Set] 0 ) and the Eilenberg-Moore construction is as follows. In [7] , the Eilenberg-Moore category C T for any graded monad T on C is introduced together with a left action : M × C T → C T . If C = Set and T is the graded monad obtained from an M-graded theory T , then the Eilenberg-Moore category Set T is essentially the same as Mod T ([M, Set] 0 ). Theorem 20. The comparison functor K : Mod T ([M, Set] 0 ) → Set T (see [7] for the definition) where T is an M-graded theory and T is the graded monad induced from the graded theory T is isomorphic. Moreover, K preserves the Maction: We define the category GS M of graded algebraic theories as follows. Definition 21. 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 that the equations in E are preserved by α, i.e. for each Definition 23. We write GS M for the category of graded algebraic theories and morphisms between them. The identity morphisms are defined by 1 Example 24 (graded modules). Let M = (N, +, 0) where N is regarded as a discrete category. Given a graded ring A = n∈N A n , 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) and the unary scalar multiplication operation a · (−) (arity: 1, grade: n) for each a ∈ A n . Let E be the equational axiom for modules. A model (F, | · |) of the M-graded theory (Σ, E) in [M, Set] 0 consists of a set F n for each n ∈ N and functions |+| n : (F n ) 2 → F n , |−| n : F n → F n , |0| n ∈ F n and |a · (−)| n : F n → F m+n for each n ∈ N and each a ∈ A m , and these interpretations satisfy E. Therefore models of (Σ, E) in [M, Set] 0 correspond one-to-one with graded modules. µ 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 defined by (Σ ex , ∅) where Σ ex is the set that consists of an operation raise e (arity: 0, grade: {e}) for each e ∈ Ex. The graded monad induced by T ex coincides with the graded exception monad. Indeed, the free model functor F T ex for T ex is given by F T ex Xm = m * X. Here, the operations raise e are interpreted by e ∈ Ex. Intuitively, this can be understood as follows. Since all the operations are of grade I, coercions c w in a term can be moved to the innermost places where variables occur by repeatedly applying c w (f (t 1 , . . . , t n )) = f (c w (t 1 ), . . . , c w (t n )) (see Definition 14) . Therefore, we can consider terms of T M as terms of T whose variables are of the form c w (x). An M-graded monad ( * , η, µ) obtained from T M is as follows. We present a categorical formulation of graded algebraic theories of §3 in a similar fashion to ordinary Lawvere theories. For ordinary (single-sorted) finitary algebraic theories, a Lawvere theory is defined as a small category L with finite products together with a strict finiteproduct preserving identity-on-objects functor 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 are exactly the objects in obℵ 0 , are arities. According to the above intuition, it is expected that a graded Lawvere theory is also defined as a category whose objects are natural numbers and morphisms are graded terms. However, since terms in a graded algebraic theory are stratified by a monoidal category M, mere sets are insufficient to express hom-objects of graded Lawvere theories. Instead, we take hom-objects from the functor category 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 is biclosed, ⊗ t preserves colimits in both arguments. Therefore, (n · y(I)) ⊗ t (n · y(I)) ∼ = (n · n ) · y(I). The condition that ν is isomorphic can be rephrased as follows. 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)) ∼ = [M, Set] 0 (y(I), A(n C, C)) n ∼ = A(n C, C)I n . The The latter part of the lemma follows from the former part. If (π 1 , . . . , π n ) ∈ (A(n C, C)I) n satisfies the condition in Lemma 29, 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 N op 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 ∈ obN op M and C ∈ obA. We also assume that 1 X = X without loss of generality. Proof. For any X ∈ C T op and n, the cotensor n X is given by finite power X n , and the i-th projection is given by η • π i ∈ C T op I where π i : X n → X is the i-th projection of the finite power X n . The rest of the proof is routine. We have shown three graded notions: graded algebraic theories, graded Lawvere theories and finitary graded monads, which give rise to categories GS M , GLaw M and GMnd M , respectively. This section is about the equivalence of these three notions. We give only a sketch of the proof of the equivalence, and the details are deferred to [14, Appendix A]. We prove that the category of graded algebraic theories GS M and the category of graded Lawvere theories GLaw M are equivalent by showing the existence of an adjoint equivalence Th U : Let M be a small strict monoidal category and T = (Σ, E) be an M-graded algebraic theory. We define ThT (the object part of Th) as an M-graded Lawvere theory whose morphisms are terms of T modulo equational axioms. It is easy to show that ThT has N op M -cotensors (by Lemma 29) . Therefore, Th is a mapping from an object in GS M to an object in GLaw M . We define a functor U : GLaw M → GS M by taking all the morphism f ∈ L(n, 1)m in L ∈ GLaw M as operations and all the equations that hold in L as equational axioms. Moreover, the unit and the counit of Th U are isomorphic. Therefore: Theorem 37. Two categories GS M and GLaw M are equivalent. We can also prove the equivalence of the categories of models. Lemma 38. If C is a category satisfying M-model condition, then Mod T (C) is equivalent to Mod(ThT , C T ) where T is the M t -action on C. We prove that the category of graded Lawvere theories GLaw M and the category of finitary graded monads GMnd M are equivalent. Given a graded Lawvere theory, a finitary graded monad is obtained as a coend that represents the set of terms. On the other hand, given a finitary graded monad, a graded Lawvere theory is obtained from taking the full sub-[M, Set] 0 -category on arities ob(N op M ) of the opposite category of the Kleisli(-like) category in Definition 7. These constructions give rise to an equivalence of categories. An M-graded Lawvere theory yields a finitary graded monad by letting m * X be the set of terms of grade m whose variables range over X. Definition 39. Let L be an M-graded Lawvere theory. We define T L = ( * , η, µ) by a (finitary) M-graded monad whose functor part is given as follows. Given a graded monad, a graded Lawvere theory is obtained as follows. Since L T has N M -cotensors n 1 = n whose projections are given by π i = ( * → η(i)) ∈ Set(1, I * n), L T is a graded Lawvere theory. Given a morphism α : T → T in GMnd M , we define L α : L T → L T by (L α ) n,n ,m = Set(n , α n,m ) : L T (n, n )m → L T (n, n )m. It is easy to prove that L α is a morphism in GLaw M and L (−) : GMnd M → GLaw M is a functor. Theorem 41. Two categories GLaw M and GMnd M are equivalent. Proof. L (−) is an essentially surjective fully faithful functor. Under the correspondence to algebraic theories, combinations of computational effects can be understood as combinations of algebraic theories. In particular, sums and tensor products are well-known constructions [9] . In this section, we show that these constructions can be adapted to graded algebraic theories. By the equivalence GMnd M GLaw M GS M in §5, constructions like sums and tensor products in one of these categories induce those in the other two categories. So, we choose GS M and describe sums as colimits in GS M and tensor products as a mapping GS M1 × GS M2 → GS M1×M2 . We prove that GS M has small colimits. Lemma 42. The category GS M has small coproducts. Proof. Given a family {(Σ (i) , E (i) )} i∈I of objects in GS M , the coproduct is obtained by the disjoint union of operations and equations: i∈I (Σ (i) , E (i) ) = i∈I Σ (i) , i∈I E (i) . Lemma 43. The category GS M has coequalizers. Proof. Let T = (Σ, E) and T = (Σ , E ) be graded algebraic theories and α, β : T → T be a morphism. The coequalizer T of α and β is given by adding the set of equations induced by α and β to T , that is, Since a category has all small colimits if and only if it has all small coproducts and coequalizers, we obtain the following corollary. A free model functor F for T ex + T M is given by F Xm = T (m * ex X). For each n-ary operation f in T , |f | F X m : (T (m * ex X)) n → T (m * ex X) is induced by free models of T , and for each e ∈ Ex, |raise e | F X m : 1 → T ({e} * ex X) is defined by η T {e} * ex X (e) ∈ T ({e} * ex X). It is easy to see that F X defined above is indeed a model of T ex + T M . Therefore, we obtain a graded monad m * X = T (m * ex X). The tensor product of two ordinary algebraic theories (Σ, E) and ) for each f ∈ Σ and g ∈ Σ . However, when we extend tensor products to graded algebraic theories, the grades of the both sides are not necessarily equal. If the grade of f is m and the grade of g is m , then the grades of f (λi.g(λj.x ij )) and g(λj.f (λi.x ij )) are m ⊗ m and m ⊗ m, respectively. Therefore, we have to somehow guarantee that the grade of f ∈ Σ and the grade of g ∈ Σ commute. We solve this problem by taking the product of monoidal categories. That is, we define the tensor product of an M 1 -graded algebraic theory and an M 2 -graded algebraic theory as an M 1 × M 2 -graded algebraic theory. Before defining 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 define 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) defined inductively as follows: if x is a variable, then G * (x) := c η G (x); for each w : m → m and term t, G * (c w (t)) := c Gw (G * (t)); for each f ∈ Σ n,m and terms t 1 , . . . , t n with grade m , G * (f (t 1 , . . . , t n )) := c µ G m,m (f (G * (t 1 ), . . . , G * (t n ))). The tensor product of T 1 ∈ GS M1 and T 2 ∈ GS M2 is defined by first extending T 1 and T 2 to M 1 ×M 2 -graded theories and then adding commutation equations. Definition 46 (tensor product). That is, if f is an operation in T 1 with grade m 1 ∈ M 1 , then T 1 ⊗ T 2 has the operation f with grade (m 1 , I 2 ) ∈ M 1 × M 2 and similarly for operations in T 2 . The tensor products satisfy the following fundamental property. Example 48. We exemplify the tensor product by showing a graded version of [9, Corollary 6] , which claims that the L-fold tensor product of the side-effects theory in [21] with one location is the side-effects theory with L locations. First, we consider the situation where there is only one memory cell whose value ranges over a finite set V . Let 2 the preordered monoid (join-semilattice) ({⊥, }, ≤, ∨, ⊥) where ≤ is the preorder defined by ⊥ ≤ . Intuitively, ⊥ represents pure computations, and represents (possibly) stateful computations. Let T st be a 2-graded theory of two types of operations lookup (arity: V , grade: ) and update v (arity: 1, grade: ) for each v ∈ V and the four equations in [21] for the interaction of lookup and update. Note that we have to insert coercion to arrange the grade of the equation lookup(λv ∈ V.update v (x)) = c ⊥≤ (x). The graded monad ( * , η, µ) induced by T st is as follows. The middle equation can be explained as follows: any term with grade can be presented by a canonical form t f := lookup(λv.update f V (v) (f X (v))) where f = f V , f X : V → V × X is a function, and therefore, the mapping f → t f gives a bijection between (V × X) V and * X = T Σ (X)/∼. The L-fold tensor product of T st , which we denote by T ⊗L st , is a 2 L -graded theory where 2 L = (2 L , ⊆, ∪, ∅) is the join-semilattice of subsets of L. Specifically, T ⊗L st consists of operations lookup l and update l,v with grade {l} for each l ∈ L and v ∈ V with additional three commutation equations in [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 that touch only memory locations in L . 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 treatment of trace semantics. However, these work only deal with N-graded monads where N is regarded as a discrete monoidal category, while we deal with general monoidal categories. The Kleisli construction and the Eilenberg-Moore construction for graded monads are presented in [7] by adapting the 2-categorical argument on resolutions of monads [29] . Algebraic operations for graded monads are introduced in [12] and classified into two types, which are different in how to integrate the grades of subterms. One is operations that take terms with the same grade, and these are what we treated in this paper. The other is operations that take terms with different grades: the grade of f (t 1 , . . . , t n ) is determined by an effect function : M n → M associated to f . Although the latter type of operations is also important to give natural presentations of computational effects, we leave it for future work. Enriched Lawvere theories. There are many variants of Lawvere theories [25, 11, 24, 10, 19, 15, 1, 16, 28] , and most of them share a common pattern: they are defined as an identity-on-objects functor from a certain category (e.g., ℵ op 0 ) which represents arities, and the functor must preserve a certain class of products (or cotensors if enriched). Among the most relevant work to ours are enriched Lawvere theories [24] and discrete Lawvere theories [10] . For a given monoidal category V, a Lawvere V-theory is defined as an identity-on-objects finite cotensor (i.e. V fp -cotensor) preserving V t -functor J : V op fp → L where V fp is the full subcategory of V spanned by finitely presentable objects. If V = [M, Set] 0 t , Lawvere [M, Set] 0 t -theories are analogous to our graded Lawvere theories except that we used N op M instead of ([M, Set] 0 ) fp . Since n · y(I) ∈ N op M is finitely presentable, we can say that the notion of graded Lawvere theory is obtained from enriched Lawvere theories by restricting arities to N op M ⊆ ([M, Set] 0 ) fp . However, the correspondence to finitary graded monads on Set is an interesting point of our graded Lawvere theories compared to Lawvere V-theories, which correspond to finitary V-monads on V. Discrete Lawvere theories restrict arities of Lawvere V-theories to ℵ 0 , that is, a discrete Lawvere V-theory is defined as a (Set-enriched) finite-product preserving functor J : ℵ op 0 → L 0 where L is a V t -category. Actually, discrete Lawvere [M, Set] 0 t -theories are equivalent to graded Lawvere theories because there is a finite-product preserving functor ι : ℵ op 0 → N op M such that the composition with ι gives a bijection between graded Lawvere theories J : N op M → L and discrete Lawvere [M, Set] 0 t -theories J 0 • ι : ℵ op 0 → L 0 . However, we considered not only symmetric monoidal categories but also nonsymmetric ones, which cause a nontrivial problem when we define 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 and defining the tensor product of an M 1 -graded theory and an M 2 -graded theory as an M 1 × M 2 -graded theory, and the use of two different monoidal categories is new to the best of our knowledge. To extend the correspondence between algebraic theories, Lawvere theories, and (finitary) monads, we introduced notions of graded algebraic theory and graded Lawvere theory and proved their correspondence with finitary graded monads. We also provided sums and tensor products for graded algebraic theories, which are natural extensions of those for ordinary algebraic theories. Since we do not assume monoidal categories to be symmetric, our tensor products are a bit different from the ordinary ones in that this combines two theories graded by (or enriched in) different monoidal categories. We hope that these results will lead us to apply many kinds of techniques developed for monads to graded monads. As future work, we are interested in "change-of-effects", 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 define tensor products, but we want to look for more properties of this operation. We are also interested in integrating a more general framework for notions of algebraic theory [6] and obtaining a graded version of the framework. Another direction is exploiting models of graded algebraic theories as modalities in the study of coalgebraic modal logic [17, 4] or weakest precondition semantics [8] . Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. Monads with arities and their associated theories special Issue devoted to the International Conference in Category Theory 'CT2010 A theory of effects and resources: adjunction models and polarised calculi On closed categories of functors Graded monads and graded logics for the linear time -branching time spectrum Some aspects of equational categories A unified framework for notions of algebraic theory Towards a formal theory of graded monads Generic weakest precondition semantics from monads enriched with order Combining effects: Sum and tensor Discrete Lawvere theories and computational effects The category theoretic understanding of universal algebra: Lawvere theories and monads Parametric effect monads and semantics of effect systems Lecture note series / London mathematical society Graded algebraic theories Gabriel-Ulmer duality and Lawvere theories enriched over a general base Enriched algebraic theories and monads for a system of arities Generic trace semantics and graded monads Computational lambda-calculus and monads Lawvere theories enriched over a general base Adequacy for algebraic effects Notions of computation determine monads A logic for algebraic effects Handling algebraic effects Enriched Lawvere theories Countable Lawvere theories and computational effects A course in universal algebra Graded monads and rings of polynomials Freyd categories are enriched Lawvere theories proceedings of the Workshop on Algebra, Coalgebra and Topology The formal theory of monads Acknowledgement. We thank Soichiro Fujii, Shin-ya Katsumata, Yuichi Nishiwaki, Yoshihiko Kakutani and the anonymous referees for useful comments. This work was supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).