Graded Algebraic Theories

Satoshi Kura
National Institute of Informatics, Tokyo, JapanThe Graduate University for Advanced Studies (SOKENDAI), Kanagawa, Japan

Outline
Algebraic theory for graded monads• Graded algebraic theory• Graded Lawvere theory
Application: combining effects (see my paper)• Sum• Tensor

Satoshi Kura (NII, Tokyo)

1Monads• Semantics for computational effects[Moggi, LICS’89]• Monads correspond to• algebraic theories (= operations + equations)• Lawvere theories [Lawvere, PhD thesis](finitary)monadsSatoshi Kura (NII, Tokyo)'algebraic
theories'Lawveretheories

2

Algebraic presentation
Computational effects can be algebraicallypresented.
• Arity = number of continuations
lookupl (λu.xu )“choose xu by value u in l”• Executed from outermost operation
updatel,v (lookupl (λu.xu ))“update l with v and then lookup l”
Satoshi Kura (NII, Tokyo)

3An example of algebraic theories
State monad S → (−) × S
where
S = V Loc
Algebraic theory T st :• updatel,v : unary• lookupl : V -ary
• with several equational axioms• e.g. updatel,v (lookupl (λu.xu )) = xv

terms in T st = stateful computations
Satoshi Kura (NII, Tokyo)

4Effect systems• estimate the scope of computational effects• accessed memory locations• raised exceptions• via type systemsΓ ` M : T (e, τ )Γ, x : τ ` N : T (e0 , σ)Γ ` let x be M in N : T (e · e0 , σ)
• semantics by graded monads[Katsumata, POPL’14]
Satoshi Kura (NII, Tokyo)

5Graded monads
M = (M, I, ⊗): monoidal category.
M-graded monad on category C consists of• a functor

T : M → [C, C]• two natural transformations
η : IdC → TI
µm1 ,m2 : (Tm1 ) ◦ (Tm2 ) → Tm1 ⊗m2• satisfying monad laws.
Satoshi Kura (NII, Tokyo)

6

Algebraic theories for graded monads
Only a few pieces of work.
• When M = (N, 0, +): [Milius, CALCO’15]
Why not consider• more general M?
• “subeffecting” m ≤ m0 ?

• “graded” Lawvere theories?

Satoshi Kura (NII, Tokyo)

7

Extending algebraic/Lawvere theories(finitary)monads'algebraic
theories'Lawveretheories

generalizing[Milius, CALCO’15](finitary)
M-gradedmonads[Smirnov’08]'M-graded
algebraic
theories'M-graded
Lawveretheories

M: small strict monoidal category(M is not necessarily symmetric)
Satoshi Kura (NII, Tokyo)

8Graded algebraic theories

Graded algebraic theories

T = (Σ, E)• Σ: operations (equipped with grade)• E: equational axioms

Satoshi Kura (NII, Tokyo)

9

Operations
Each operation has its grade m ∈ M.
Σ = (Σn,m )n∈N,m∈M
Example (graded state monad).
grade: accessed memory locationsLoc

M = ((2Satoshi Kura (NII, Tokyo), ⊆), ∅, ∪)operation arity grade
lookuplV{l}updatel,v 1{l}10TermsWe define the set of terms with grade m ∈ M
ΣTm(X)

where X is a set of variables.
Three rules of term formation:• Variables: x• Operations: f (t1 , . . . , tn )• Coercions (or subeffecting): cw:m→m0 (t)Satoshi Kura (NII, Tokyo)

11

Grade of Terms

x
|{z}
Im
m0z}|{ z }| {f ( t1 , . . . , tn )|{z}0m⊗mmz}|{cw:m→m0 ( t )|{z}0mSatoshi Kura (NII, Tokyo)

12Equational Axioms
Grades of both sides must be equal.
ΣΣ
E = Em ⊆ Tm (X) × Tm (X)m∈M

Example (graded state monad).
∅z}|{updatel,v (lookupl (λu.xu )) = c∅⊆{l} ( xv )|{z}{l}(+ several other equations)
Satoshi Kura (NII, Tokyo)

13

Equivalencetermscomputations=with grade mwith effect mTheorem.
category ofM-gradedalgebraic theories

1'

category offinitary1 M-gradedmonads on Set

graded monad T where Tm : Set → Set is finitary for each m ∈ M

Satoshi Kura (NII, Tokyo)14

Graded Lawvere theories

Why Lawvere theories?
Independent from specific choice of operations• because we consider all terms generated
by algebraic theories
Independent from base category• compared to monads, which are defined on
one base category
Satoshi Kura (NII, Tokyo)

15

Intuition of Lawvere theories
A Lawvere theory is a category L where• objects: arities
obL = N• arrows: terms (modulo equational axioms)(t1 ,...,tk )n −−−−→ k• composition: substitution(t1 ,...,tk )sn −−−−→ k −→1
Satoshi Kura (NII, Tokyo)=s[t1 /x1 ,...,tk /xk ]n−−−−−−−−−→116

Lawvere theories
Definition.
A Lawvere theory is a pair of• a category L with finite products and• a strict finite-product preserving
identity-on-objects functor J : ℵop
0 → L.
Here, ℵ0 is the full subcategory of Set on naturalnumbers.

Satoshi Kura (NII, Tokyo)

17

Graded Lawvere theories?
Different terms have different grades.
tgrade m◦t0
grade m0◦..
.

Take hom-objects not from Set
but from [M, Set].
Satoshi Kura (NII, Tokyo)

18

Graded Lawvere theories?
How to express the mathematical structure ofgrades?
(t1 ,...,tk )sm

mn −−−−→ k −→10=s[t1 /x1 ,...,tk /xk ]n−−−−−0 −−−−→1m ⊗mConsider [M, Set]-enriched categories
using the Day tensor monoidal structure.

Satoshi Kura (NII, Tokyo)

19[M, Set]-categories
If C is an [M, Set]-category,• hom-object:

C(X, Y ) : M → Setf

X −−−−→ Y⇐⇒grade mf ∈ C(X, Y )m

• composition:
fgm

mX−→ Y −→Z0
Satoshi Kura (NII, Tokyo)=g◦f

X −−0 −→ Zm ⊗m

20

Graded Lawvere Theories
Definition.
A graded Lawvere theory is a pair of• an [M, Set]-category L withop
NM-cotensors andop• a NM-cotensor preserving
opidentity-on-objects functor J : NM→ L.

NM is the full sub-[M, Set]-category of [M, Set]
on {n · y(I) | n ∈ N} (if M is symmetric).
Satoshi Kura (NII, Tokyo)

21

Equivalence
Theorem.
category ofM-graded
Lawvere theories

2'category offinitary2 M-gradedmonads on Set

graded monad T where Tm : Set → Set is finitary for each m ∈ M

Satoshi Kura (NII, Tokyo)

22

Conclusions• Graded algebraic theories: by assigning agrade to each term.
• Graded Lawvere theories: by considering
enrichment in [M, Set].
• They correspond to graded monads.
• Sums and tensors can be extended tograded algebraic theories.

Satoshi Kura (NII, Tokyo)

23

Appendix

Combining effects
For ordinary algebraic theories[Hyland & Power, TCS’06]

Sum: add operations with no additional equation
T1

T2

7→

T 1 + T2

Tensor: allow commutation f (g(x)) = g(f (x))
between two theories
T1
Satoshi Kura (NII, Tokyo)

T2

7→

T1 ⊗ T2

Combining effects
For graded algebraic theories:
SumM-graded
T1T27→

M-graded
T1 + T2Tensor
M1 -graded M2 -gradedM1 ×M2 -graded
T1
T2
7→
T1 ⊗ T2
Satoshi Kura (NII, Tokyo)

Sums
Given two M-graded algebraic theories
T = (Σ, E),

T 0 = (Σ0 , E 0 )where• Σ, Σ0 : sets of operations• E, E 0 : sets of equations
The sum is
T + T 0 := (Σ ∪ Σ0 , E ∪ E 0 )Satoshi Kura (NII, Tokyo)

Example of Sums

finitary monad
graded exception monad+T : Set → Set
T ex : M → [Set, Set]
=T T ex : M → [Set, Set]

Cf.
finitary monad
exception monad+T(−) + Ex=T ((−) + Ex)

Satoshi Kura (NII, Tokyo)

Tensors in [Hyland & Power, TCS’06]
Tensors are defined by(Σ, E) ⊗ (Σ0 , E 0 ) := (Σ ∪ Σ0 , E ∪ E 0 ∪ E⊗ )where E⊗ consists off (λi.g(λj.xij )) = g(λj.f (λi.xij ))for any f ∈ Σ and g ∈ Σ0 .

Satoshi Kura (NII, Tokyo)Problem of commutativity
M-graded
TT07→

M-graded
T ⊗T0(?)

We cannot definef (λi. g (λj.xij )) = g (λj. f (λi.xij ))|{z}|{z}|{z}|{z}00mmmmbecause M is not necessarily symmetric.
m ⊗ m0 6= m0 ⊗ m
Satoshi Kura (NII, Tokyo)

Tensors
M-graded M0 -graded
M×M0 -graded
TT07→
T ⊗T0
Idea: embed M and M0 into M × M0 by
m 7→ m, I 0: M → M × M0

m0 7→ I, m0: M 0 → M × M0
Then, we can definef (λi. g (λj.xij )) = g (λj. f (λi.xij ))
|{z}
|{z}
|{z}
|{z}
000(m, I ) (I, m )(I, m ) (m, I 0 )Satoshi Kura (NII, Tokyo)

Example of Tensors
Example: theories for graded state monadSuppose• T1 : 2-graded theory with #Loc = 1• Tn : 2n -graded theory with #Loc = n• 2 = {⊥ ≤ >} and 2n are join-semilattices
We have
Tn = T1 ⊗ · · · ⊗ T 1|{z}n-fold tensor
Satoshi Kura (NII, Tokyo)