Categorical Descriptional Composition
Shin-ya Katsumata
Research Institute for Mathematical Sciences
Kyoto University, Kyoto, 606-8502, Japansinya@kurims.kyoto-u.ac.jp

Abstract. Descriptional composition is a method to fuse two term transformation algorithms described by attribute couplings (AC, attribute grammars overterms) into one. In this article, we provide a general categorical framework forthe descriptional composition based on traced symmetric monoidal categories andthe Int construction by Joyal et al. We demonstrate that this framework can handle the descriptional composition of SSUR-ACs, nondeterministic SSUR-ACs,quasi-SSUR ACs and quasi-SSUR stack ACs.

1 Introduction
Descriptional composition [6–8] is a method to fuse two term transformation algorithms
described by attribute couplings (ACs; attribute grammars over terms) into one. The ACyielded by the descriptional composition computes the composition of two ACs without constructing the intermediate data structure passed between two ACs; hence it saves
time and space in many cases. The descriptional composition was first introduced as an
optimisation method for compilers described by ACs [7]. Around the same time Bartha
introduced a similar composition method for linear attributed tree transformations [1].
Later, it was realised that ACs can be used to represent functional programs with accumulating parameters [10], and the descriptional composition inspired various fusiontransformations of such functional programs [19, 22].
The descriptional composition was first given for the ACs consisting only of term
constructors [7]. Later, extensions of the ACs have been studied in [18, 20, 3]. In [3],Boyland considered an extension of ACs with conditional expressions. In [18], Nakano
introduces stacks to ACs so that complex parsing functions can be expressed. In each
work, the descriptional composition was also considered to these extended ACs. In
general, the descriptional composition is sensitive on the language describing ACs, andformulating the descriptional composition verifying its correctness tend to be involved
when expressive power of the language increases.
The question we address here is to find a mathematical framework that can uniformly treat these extensions of ACs and the descriptional composition of them. In thispaper, we propose such a general categorical framework based on the theory of traced
symmetric monoidal categories (TSMCs) and the Int construction by Joyal et al. The
key observation in the categorical treatment of ACs and the descriptional compositionis that every attribute grammar determines a traced symmetric strict monoidal functor

F : L(Σ) → Int(C) where L(Σ) is a free TSMC over a signature Σ, and especially every
AC satisfying syntactic single use condition (SSUR), which is the essential condition forthe descriptional composition to work, determines a traced symmetric monoidal functor
G : L(Σ) → Int(L(∆)). With this functorial presentation, the descriptional composition
becomes the composition of functors, and its associativity can be easily verified. This
story scales up to the TSMCs with extra structures, provided that the Int constructionis also extended to such TSMCs; examples include nondeterministic ACs, quasi-SSUR
ACs (an affine version of SSUR AC), and ACs with stacks [18].
In this paper we do not exclude circular terms and recursive computation as meaningless things. Hence every AG assigns some meaning to a given term.
Conventions and Notations Signatures are all many-typed and first-order. We reserve∆, Σ, Ξ for ranging over signatures. By ρ ∈ Σ and o ∈ Σ ρ1 ···ρn →ρ we mean that ρ is a typeof Σ and o is an operator of type ρ1 · · · ρn → ρ, respectively. We declare the signaturefor binary trees, cons-lists and natural numbers byΣtree = ({∗}, L∗ , N∗∗→∗ ), Σlist = ({∗}, []∗ , a :: (−)∗→∗ ), Σnat = ({∗}, Z∗ , S∗→∗ ).
For a type σ ∈ Σ and sequence of Σ-types ρ1 · · · ρn , by T Σσ (ρ1 · · · ρn ) we mean the setof open Σ-terms that may contain some variables xi of type ρi (1 ≤ i ≤ n). We thenextend this notation by T Σσ1 ···σm (ρ1 · · · ρn ) = T Σσ1 (ρ1 · · · ρn ) × · · · × T Σσm (ρ1 · · · ρn ). By Σ +we mean that Σ contains a special type #; such signature is called rooted. We assume
that the readers are familiar with the concept of symmetric monoidal categories [17].
We also employ the 2-category theory and the theory of pseudo-monads and pseudodistributive laws; see e.g. [21].

2 Classical Attribute Couplings and Descriptional Composition
A classical attribute grammar (AG) for a signature ∆ is a triple A = (I, S , a) where foreach type ρ ∈ ∆, Iρ and S ρ are resp. sets of inherited and synthesised attribute values,
and for each operator o ∈ ∆ρ1 ,··· ,ρn →ρ , ao is a function called the attribute calculation
rule1 :
ao : S ρ1 × · · · × S ρn × Iρ → S ρ × Iρ1 × · · · × Iρn .
(1)
This function captures the input-output relation of a computation unit that processes
bidirectional information flow (Figure 1, left). Given a ∆-term M, we connect the assigned computation units according to the shape of M (Figure 1, right). The function
corresponding to the entire circuit is the meaning A[[M]] assigned to M by the AG A.
Depending on the configuration of the attribute calculation rules, such function may
not exist in general, but if any combination of attribute calculation rules does not yield
cyclic information dependency (such AGs are called non-circular), the function A[[M]]uniquely exists for any M. See [14, 15] for the detail.
An attribute coupling (AC) from ∆ to Σ is a special AG such that the set assigned
to Iρ (resp. S ρ) is a set T Σσ1 ,··· ,σn of tuples of Σ-terms for some σ1 , · · · , σn ∈ Σ, and1This form of attribute calculation rule is called Bochmann normal form.

Fig. 1. Attribute Grammars

each attribute calculation rule comprises only of Σ-operators rather than arbitrary functions. Briefly speaking, ACs are AGs constructing Σ-terms. We can extract the essential
information from such AGs and redefine ACs from ∆ to Σ as the tuple A = (I, S , a),where for each type ρ ∈ ∆, Iρ and S ρ are sequences of Σ-types, and for each operatoro ∈ ∆ρ1 ,··· ,ρn →ρ , ao is a tuple of (open) Σ-terms:
ao ∈ T ΣS ρ,Iρ1 ,··· ,Iρn (S ρ1 , · · · , S ρn , Iρ).
We write AC(∆, Σ) for the set of ACs from ∆ to Σ. We assume that ACs (I, S , a) between
the signatures containing the special type # satisfy I# = ǫ and S # = #. With this convention we can view every non-circular AC A from ∆+ to Σ + as a term transformation
function T A : T ∆#+ → T Σ# + , defined by T A(M) = A[[M]].
Let A ∈ AC(∆+ , Σ + ) and B ∈ AC(Σ + , Ξ + ) be non-circular ACs. We seek for an AC
B c A such that T (B c A) = T B ◦ T A. In general such AC may not exist, but when A
satisfies a condition called syntactic single-use restriction (SSUR), we can build B c A
by the descriptional composition, which we illustrate below.
Suppose that the attribute calculation rules of A and B look like the left of Figure
2. There, A assigns to a ∆+ -operator f a computation unit that constructs Σ + -terms,

Fig. 2. The descriptional composition

which is drawn as a circuit. Similarly, B assigns to a Σ + -operator a a computation unitb, which is just drawn as a round box. We now replace each wire in the right hand sideof the attribute calculation rule of A with bidirectional wire, and replace each Σ + -term
constructor with the computation unit assigned by B. The result of this replacement isdrawn on the right of Figure 2, which is a new attribute coupling from ∆+ to Ξ + . This is
the descriptional composition B c A.
The hidden point in the above process is that the computation unit (circuit) assigned
by A should not contain any branching wires nor terminals. This is because we do notknow how to make branches and terminals bidirectional (Figure 3). This suggests that?

?

Fig. 3. How to Make Branches and Terminals Bidirectional?

each attribute calculation rule assigned by A should use each variable exactly once, andan AC satisfying this linearity condition is called syntactic single use restriction (SSUR)
AC. We will see its precise definition in Section 2.2, and reformulate it as an AG in a
linear recursive language, which we introduce below.

2.1 The Linear Recursive Language L(Σ)
We introduce a simply-typed first-order linear language with recursive declarations
called L(Σ). It has only one form of raw-expressions:
λx1 , · · · , xn . let y1 = M1 , · · · , yl = Ml in z1 , · · · , zm ,and they are given a type σ1 , · · · , σn → τ1 , · · · , τm by the type system in Figure 4,
where U and D are typing contexts defined by
U = Γ1 ∪ · · · ∪ Γn ∪ {z1 : τ1 , · · · , zm : τm }D = {x1 : σ1 , · · · , xn : σn , y1 : ρ1 , · · · , yl : ρl },such that xi , y j , zk and variables in Γ1 , · · · , Γn are different from each other. The leading
λ of expressions is a formal binder for x1 , · · · , xn , rather than the lambda abstraction in
the lambda calculus. Expressions are treated modulo α-equivalence.
Expressions of L(Σ) are identified by the rules in Figure 4, where the sequence ofvariable declarations after let is abbreviated as D. The first axiom allows us to permute
D without affecting the meaning of expressions. In the second axiom, D[w/v] denotes
the sequence of variable declarations obtained by replacing v in D with w. This axiom
allows us to forward v to w when v = w is contained in D.
Here are some examples of L(Σtree )-expressions:⊢ M λx . let y = N(l, x), l = L in y : ∗ → ∗⊢ M λx, y, z . let w = N(x, w), l = L, v = N(l, z) in y, v : ∗∗∗ → ∗∗.

(2)

Note that in (2) the variable w can not be used for output due to the linearity constraint.
This means that when the underlying signature has a binary operator then there is a way
to discard inputs.

ρ∈Σo ∈ Σ ρ1 ···ρn →ρ
x : ρ ⊢E x : ρ x1 : ρ1 , · · · , xn : ρn ⊢E o(x1 , · · · , xn ) : ρΓ1 ⊢E M1 : ρ1 · · · Γl ⊢E Ml : ρl U = D⊢M λx . let y1 = M1 , · · · , yl = Ml in z : σ1 , · · · , σn → τ1 , · · · , τm
(λx . let D in z) = (λx . let π(D) in z)(λx . let v = w, D in z) = (λx . let D[w/v] in z[w/v]) (v , w)
Fig. 4. Type System and Axiom for L(Σ)

2.2 SSUR-ACs as Attribute Grammars in L(Σ)
An AC (I, S , a) ∈ AC(∆, Σ) satisfies the syntactic single use restriction (SSUR) [6] ifeach attribute calculation rule satisfies the following linearity condition. We let l be
the length of the concatenation S ρ, Iρ1 , · · · , Iρn , and write τi (1 ≤ i ≤ l) for the i-thcomponent of this sequence. We prepare sequences Γi (1 ≤ i ≤ l) of Σ-types suchthat S ρ1 , · · · , S ρn , Iρ is a permutation of the concatenation Γ1 , · · · , Γl . We then ask theattribute calculation rule to be in the following set:ao ∈ T Στ1 (Γ1 ) × · · · × T Στl (Γl ),(3)and, moreover, in the i-th component of ao , each variable occurs exactly once.
We observe that there is a one-to-one correspondence between such a tuple and aL(Σ)-expression of type S ρ1 , · · · , S ρn , Iρ → S ρ, Iρ1 , · · · , Iρn . We exploit this correspondence to redefine the concept of SSUR-AC.
Definition 1. An SSUR-AC from ∆ to Σ is a triple (I, S , a) where for each type ρ ∈ ∆, Iρ
and S ρ are sequences of Σ-types, and for each o ∈ ∆ρ1 ,··· ,ρn →ρ , ao is an L(Σ)-expressionof type ao : S ρ1 , · · · , S ρn , Iρ → S ρ, Iρ1 , · · · , Iρn . We write SSUR-AC(∆, Σ) for the setof SSUR-ACs from ∆ to Σ. When ∆, Σ contains the special type #, we assume that every
SSUR-AC (I, S , a) from ∆ to Σ satisfies I# = ǫ and S # = #.
We note that this correspondence is not surjective, as L(Σ) permits recursively defined
variables that can not be expressed by SSUR-ACs.

3 Categorical Aspect of Attribute Couplings
3.1 L(Σ) as a Traced Symmetric Monoidal Category
We next view L(Σ) as a category. We regard a sequence ρ = ρ1 · · · ρn of types in Σ asan object, and an equivalence class of expressions of type ρ → σ as a morphism fromρ to σ. The composition is defined by(λx . let D in y) ◦ (λz . let D′ in w) = λz . let D[w/x], D′ in y[w/x];

here we assume that every bound variable in the above expression is distinct from eachother. The category L(Σ) has an evident symmetric strict monoidal structure. The unit
object is the empty sequence and the tensor product of two objects is the concatenationof them. The tensor product of two morphisms is defined by merging two expressions:(λx . let D in y) ⊗ (λz . let D′ in w) = λx, z . let D, D′ in y, w.
The symmetry morphism is given by λx, y . let ǫ in y, x.
In addition to this, the following trace operator constructs recursive declarations in
expressions. Let x, y, z, w be sequences of different variables, and ρ, σ, τ be sequencesof types such that |x| = |ρ|, |z| = |σ|, |y| = |w| = |τ|. We define the trace operator trτρ,σ asfollows:trτρ,σ (λx, y . let D in z, w) = λx . let y = w, D in z.
A pair of a symmetric monoidal category and a trace operator is called traced symmetric monoidal category (see Appendix B). In this article we only consider the traced
symmetric strict monoidal categories, and call them TSMC. 2 The above discussion issummarised as follows:
Proposition 1. The above data make L(Σ) a TSMC.
We call a symmetric strong monoidal functor between TSMCs traced if it preserves thetrace operator in an evident way (see Appendix B). We write TSMC for the 2-categoryof TSMCs, traced symmetric strong monoidal functors and monoidal natural isomorphisms. Its 2-subcategory consisting of traced symmetric strict monoidal functors will
be denoted by TSMC s .
F
From a traced strong monoidal functor (F, φǫF , φρ,σ) ∈ TSMC(L(Σ), C), we canconstruct a traced strict monoidal functor Str(F) ∈ TSMC s (L(Σ), C) which is naturally
isomorphic to F. The strict functor is constructed as follows:
Str(F)(ρ1 · · · ρn ) = Fρ1 ⊗ · · · ⊗ FρnStr(F)( f : ρ → σ) = (φσF )−1 ◦ F f ◦ φρF .

The assignment F 7→ Str(F), which we will call strictification operator, extends toan equivalence of categories Str : TSMC(L(Σ), C) → TSMC s (L(Σ), C). It satisfies the following property: for any F ∈ TSMC s (L(Σ), D), G ∈ TSMC(D, E), H ∈TSMC(E, F), we have Str(F) = F and Str(H ◦ G ◦ F) = Str(H ◦ Str(G ◦ F)).
3.2 Monoidal Attribute Grammar
We generalise the underlying semantic domain of AGs to arbitrary C ∈ TSMC. This
generalisation is done by replacing sets with objects and attribute calculation rules with
C-morphisms.
Definition 2 ([12]). Let C ∈ TSMC. A monoidal attribute grammar (MAG) for ∆ in C
is a triple (I, S , a) where for each type ρ ∈ Σ, Iρ and S ρ are C-objects (of domains ofinherited and synthesised attributes), and for each operator o ∈ ∆ρ1 ···ρn →ρ , ao is a Cmorphism of type ao : S ρ1 ⊗ · · · ⊗ S ρn ⊗ Iρ → S ρ ⊗ Iρ1 ⊗ · · · ⊗ Iρn . We write MAG(∆, C)
for the collection of MAGs for ∆ in C.
2

Every traced symmetric monoidal category is equivalent to a traced symmetric strict monoidal
category (coherence theorem).

Some instances of MAGs are studied in [12]; in the category ωCPPO of pointed CPOs
and ω-continuous functions, monoidal attribute grammars are equivalent to Chirica andMartin’s K-systems [4]. The category Rel of sets and relations has traced biproducts[11], and MAGs in this traced symmetric monoidal category are local dependency
graphs, which are the standard tool to represent dependencies between the attributes
in attribute calculation rules. MAGs over the compact closed structure on Rel are relational attribute grammars [5]. In addition to this, by comparing Definition 1 and 2, weconclude that SSUR-ACs are exactly MAGs in L(Σ).
Proposition 2. SSUR-AC(∆, Σ) = MAG(∆, L(Σ)).
3.3 MAGs as Algebras in Int(C)Below we give two concepts that are equivalent to MAG: one is algebras in the categories obtained by Joyal, Street and Verity’s Int construction [11], and the other istraced symmetric strict monoidal functors of type L(Σ) → Int(C).
Let C ∈ TSMC. The category Int(C) is defined by the following data: an object isa pair (A+ , A− ) of C-objects, and homsets are defined by
Int(C)((A+ , A− ), (B+, B− )) = C(A+ ⊗ B− , B+ ⊗ A− ).
In category Int(C) we can naturally model computation over bidirectional information
flow. An object (A+ , A− ) denotes the type of upward and downward information; in thecontext of attribute grammar, they correspond to the type of synthesised and inherited
attributes, respectively. A morphism f : (A+ , A− ) → (B+, B− ) then represents a computation that processes bidirectional information flow.
We give a symmetric strict monoidal structure to Int(C) byIInt(C) = (IC , IC ),(A+ , A− ) ⊗Int(C) (B+, B− ) = (A+ ⊗C B+ , A− ⊗C B− ).

The category Int(C) has a compact closed structure [11], which yields the canonicaltrace operator with respect to the above symmetric monoidal structure. The mapping
C 7→ Int(C) extends to a 2-endofunctor over TSMC, and moreover, to a pseudo-monad(Int, (N, n), (M, m), τ, λ, ρ) over TSMC; see Appendix B for the detail.
We extend the concept of Σ-algebra from the set-theoretic one to the categoricalone. A Σ-algebra in a monoidal category C is a pair (A, a) where A is a family of Cobjects indexed by Σ-types and a is a family of C-morphisms indexed by Σ-operators,
such that the type of ao is Aρ1 ⊗· · ·⊗Aρn → Aρ for each operator o ∈ Σ ρ1 ···ρn →ρ . We write
AlgΣ (C) for the collection of Σ-algebras in C. The concept of Σ-algebras has anotherpresentation: there is a natural bijection between Σ-algebras in C and traced symmetric
strict monoidal functors from L(Σ) to C:
AlgΣ (C) ≃ TSMC s (L(Σ), C)(4)

Let (I, S , a) be a MAG for ∆ in C ∈ TSMC. We define Aρ to be the pair (S ρ, Iρ) of
C-objects (note that it is an object in Int(C)). Then for each operator o ∈ Σ ρ1 ···ρn →ρ , theC-morphism ao can be seen as an Int(C)-morphism:ao ∈ C(S ρ1 ⊗ · · · ⊗ S ρn ⊗ Iρ, S ρ ⊗ Iρ1 ⊗ · · · ⊗ Iρn ) = Int(C)(Aρ1 ⊗ · · · ⊗ Aρn , Aρ).

This means that every MAG determines a ∆-algebra (A, a) in Int(C), and the other way
around. We summarise these concepts by the following bijective correspondences:
MAG(∆, C) ≃ Alg∆ (Int(C)) ≃ TSMC s (L(∆), Int(C))
SSUR-AC(∆, Σ) ≃ TSMC s (L(∆), Int(L(Σ))).

(5)
(6)

These three equivalent forms have different advantages. The first form is the actual
data we give when defining AGs. The second form is used to explain the initial algebra semantics of AGs [12]. The third form is suitable for discussing the descriptional
composition. We mainly adopt the functorial representation of AGs and ACs below.

4 Descriptional Composition
We begin with a categorical formulation of the descriptional composition of SSURACs. Let A ∈ SSUR-AC(∆, Σ) and B ∈ MAG(Σ, C), regarded as functors. We define
their (categorical) descriptional composition B c A by
B c A = Str(B# ◦ A),
where B# = MC ◦ Int(B) is the Kleisli lifting of B by the pseudo-monad Int. We
insert the strictification operator Str (Section 3.1) as B# is not strict monoidal.3 The
SSUR-AC A constructs bidirectional networks of Σ-operators, while B can only accept
single-directional networks of them. The Kleisli lifting extends the domain of B to thebidirectional network of Σ-operators (see Figure of 5) so that this mismatch is resolved.

Fig. 5. Kleisli Lifting of B

Theorem 1. 1. SSUR-ACs are closed under the descriptional composition.
2. The descriptional composition is associative up to a natural isomorphisms; for
any A ∈ SSUR-AC(∆, Σ), B ∈ SSUR-AC(Σ, Ξ) and C ∈ MAG(Ξ, C), there is anatural isomorphism between (C c B) c A and C c (B c A).
We do not prove this theorem as it is subsumed by Theorem 2. We note that the associativity of the descriptional composition holds only up to a natural isomorphism. This
isomorphism has no computational meaning; it just permutes the order of arguments.
This permutation is invisible in the syntactic study of the descriptional composition
because arguments are passed by records rather than tuples.
3

This is because the multiplication MC : Int2 (C) → Int(C) is not strict monoidal.

We extend this formulation of the descriptional composition to a more general setting where TSMCs are equipped with some extra structures, such as nondeterminism,
undefined values, stacks, etc. To capture such extensions, we introduce the concept ofextension of TSMC.
Definition 3. We call the following situation an extension of TSMC.
1. There is a 2-category TSMC′ and its 2-subcategory TSMC′s .
2. There is a 2-functor U : TSMC′ → TSMC that can be restricted to a 2-functor
U s : TSMC′s → TSMC s . Furthermore, U s , as an ordinary functor, has a left
adjoint F. We write (−) : |TSMC(FC, D)| → |TSMC(C, U s D)| for the bijection
between homsets, and (−) for its inverse.
3. There is a pseudo-monad (Int′ , (N ′ , n′ ), (M ′ , m′ ), τ′ , λ′ , ρ′ ) over TSMC′ such thatInt′ is a 2-functor, and is a strict lifting of the pseudo-monad Int along U, that is,
U ◦ Int′ = Int ◦ U, U(NF′ ) = NUF , Uτ′C = τUC , etc. We note that the Kleisli lifting(−)♭ of Int′ also commutes with U, that is, U((A)♭ ) = (UA)# .
4. There is an equivalence Str′ : TSMC′ (FL(Σ), C) → TSMC′s (FL(Σ), C) suchthat Str′ (F) = Str(F), and for any functor F ∈ TSMC′s and G, H ∈ TSMC′ ofappropriate type, Str′ (F) = F and Str′ (H ◦ G ◦ F) = Str′ (H ◦ Str′ (G ◦ F)).
We express such a situation by a tuple E = (F, U, Int′ ).
Definition 4. Let E = (F, U, Int′ ) be an extension of TSMC. We define the collection of
E-MAG for ∆ in C ∈ TSMC′ and E-AC from ∆ to Σ by
E-MAG(∆, C) = TSMC s (L(∆), Int(UC)) ≃ MAG(∆, UC)
E-AC(∆, Σ) = TSMC s (L(∆), Int(UFL(Σ))) ≃ MAG(∆, UFL(Σ)).
Let A ∈ E-AC(∆, Σ) and B ∈ E-MAG(Σ, C). We define their descriptional composition B c A by
B c A = Str(U((B)♭ ) ◦ A).
We write HC : C → FU s C for the unit of the adjunction F ⊣ U s . We assume that any
E-AC A between rooted signatures satisfies A(#) = (I, H(#)). We define the translation
T A : UFL(∆+ )(I, H#) → UFL(Σ + )(I, H#) induced by A ∈ E-AC(∆+ , Σ + ) as follows:
T A( f ) = unique g such that UA( f ) = NUFL(Σ) (g).
This is well-defined as N is full and faithful [11]. When we do not consider the extension(F = U = Id), the translation T A is just a mapping of f ∈ L(∆+ )(ǫ, #) to a morphismin L(Σ + )(ǫ, #). Under the identification of terms and morphisms in a free TSMC, T A
represents the term translation induced by the attribute coupling A.
Theorem 2. Let E be an extension of TSMC.
1. E-ACs are closed under descriptional composition.
2. For any A ∈ E-AC(∆, Σ), B ∈ E-AC(Σ, Ξ) and C ∈ E-MAG(Ξ, C), there is anatural isomorphism between (C c B) c A and C c (B c A).

3. For any A ∈ E-AC(∆+ , Σ + ), B ∈ E-AC(Σ + , Ξ + ) and f ∈ L(∆+ )(ǫ, #), we have
T (B c A) ◦ HL(∆+ ) ( f ) = T B ◦ T A ◦ HL(∆+ ) ( f ).
The proof is in Appendix A.
Corollary 1. For any composable SSUR-ACs A, B, we have T (B c A) = T B ◦ T A.
In the subsequent sections, we show that some useful extensions of (SSUR)-ACs
can be captured as attribute couplings in extensions of TSMC. From the above general
theorem, the associativity of the descriptional composition and the closure property ofextended ACs under the descriptional composition.
4.1 Descriptional Composition for Nondeterministic ACs
We look at an example of an extension of TSMC arising from a symmetric monoidal
monad (T, η, µ, φI, φA,B ) over Set. 4 Given such a monad, for a category C, we define a
new category T ∗ (C) by the following data: |T ∗ (C)| = |C| and T ∗ (C)(A, B) = T (C(A, B)).
The identity and composition of T ∗ (C) defined as follows:
1

φI

/ T1

T (idCA )/ T ∗ (C)(A, A)

T ∗ (C)(B, C) × T ∗ (C)(A, B)

C

φC(B,C),C(A,B)/ T (C(B, C) × C(A, B)) T (comp ) / T ∗ (C)(A, C).

This construction is well-known as change-of-base in enriched category theory. The
mapping C 7→ T ∗ C extends to a 2-monad (T ∗ , µ∗ , η∗ ) over TSMC and TSMC s . We write
TSMCT ∗ for the 2-category of strict T ∗ -algebras (which are exactly T -algebra enriched
TSMCs), strict T ∗ -algebra morphisms and T ∗ -algebra transformations; see [2] for thedetail. We also write TSMCTs ∗ for its 2-subcategory such that T ∗ -algebra morphisms
belong to TSMC s . The Eilenberg-Moore 2-adjunction F ⊣ U : TSMCT ∗ → TSMC canbe restricted to F s ⊣ U s : TSMCTs ∗ → TSMC s . One can easily extend the strictification
operator Str to the one satisfying the condition 4 of Definition 3.
To lift the pseudo-monad Int to the 2-category TSMCT ∗ , we (necessarily) give a
pseudo-distributive law [21] of T ∗ over Int. In fact, it consists only of identities, as thecomponents of Int and T ∗ commutes with each other, such as Int(T ∗ (C)) = T ∗ (Int(C)),
T ∗ (NC ) = NT ∗ C , Int((µ∗ )C ) = (µ∗ )Int(C) , etc. Thus the above data determine an extensionof TSMC.
Example 1. We write P : Set → Set for the covariant powerset monad. Let C ∈ TSMC.
A monoidal attribute grammar (I, S , a) for Σ in P∗ (C) assigns C-objects Iρ, S ρ to eachtype ρ ∈ Σ, and a P∗ (C)-morphismao ∈ P∗ (C)(S ρ1 ⊗ · · · ⊗ S ρn ⊗ Iρ, S ρ ⊗ Iρ1 ⊗ · · · ⊗ Iρn )to each operator o ∈ Σ ρ1 ···ρn →ρ ; this means that a P∗ -MAG assigns an attribute calculation rule nondeterministically to each operator in Σ. For instance, we consider thefollowing P∗ -AC from Σnat to Σlist :I(∗) = ǫ,
4S (∗) = ∗,This is equivalent to a commutative monad [16].

aZ = {[]},

aS = {(λx . let y = 0 :: x in y), (λx . let y = 1 :: x in y)}.

This AC maps each natural number S(n) (Z) to the set of all binary digit with length n,
represented as morphisms of type ǫ → ∗ in P∗ (L(Σlist )).

4.2 Descriptional Composition for quasi-SSUR ACs
In [20], Nishimura and Nakano introduced a relaxation of SSUR called quasi-SSUR. It
relaxes the linear use (exactly once) of variables to affine use (at most once), and introduces a constant denoting the undefined value to the language for attribute calculation
rules. We formulate their quasi-SSUR ACs and the descriptional composition of themin our categorical framework.
First, we introduce the language A(Σ) that modifies the typing rules of L(Σ) sothat variables can be discarded, and that has an extra constant ⊥ρ for each type ρ ∈ Σ.
These features directly correspond to Nishimura and Nakano’s modification of SSUR.
The detail of A(Σ) is the following:
1. We replace the typing rule of L(Σ) in Figure 4 as follows:Γ1 ⊢E M1 : ρ1 · · · Γl ⊢E Ml : ρl U ⊆ D⊢ M λx . let y1 = M1 , · · · , yl = Ml in z : σ1 , · · · , σn → τ1 , · · · , τm
What is new to L(Σ) is that some defined variables may be unused (U ⊆ D). For
instance, the following is now a valid derivation in A(Σ):⊢ M λx1 · · · xn . let ǫ in ǫ : ρ1 · · · ρn → ǫ
We write this expression ⊤ρ1 ···ρn .
2. We add to L(Σ) a constant ⊥ρ : ρ for each type ρ ∈ Σ, corresponding to undef in[20]. We then extend this to any sequence of Σ-types by⊥ρ1 ···ρn = (λǫ . let x1 = ⊥ρ1 , · · · , xn = ⊥ρn in x1 , · · · , xn ).
Definition 5. A quasi-SSUR AC from ∆ to Σ is a triple (I, S , a) where for each type
ρ ∈ ∆, Iρ and S ρ are sequences of Σ-types, and for each o ∈ ∆ρ1 ,··· ,ρn →ρ , ao is anA(Σ)-expression of type ao : S ρ1 , · · · , S ρn , Iρ → S ρ, Iρ1 , · · · , Iρn .
We next introduce the concept of bipointed TSMC. It is a triple (C, ⊤, ⊥) whereC ∈ TSMC and ⊤, ⊥ are C-object indexed families of morphisms ⊤A : A → I and⊥A : I → A such that
⊤I = idI ,⊤A⊗B = ⊤A ⊗ ⊤B ,⊥I = idI ,⊥A⊗B = ⊤A ⊗ ⊤B .

(7)

Discarding variables is modelled by the morphism ⊤. We say that a traced symmetricstrong monoidal functor (F, φI, φA,B ) preserves bipoints if it satisfies F(⊥A ) ◦ φI = ⊥FA
and φI ◦ ⊤FA = F(⊤A ). We write TSMC• for the 2-category of bipointed TSMCs,
traced symmetric strong monoidal functors preserving bipoints and monoidal natural
isomorphisms. We write TSMC•s for its 2-subcategory consisting of traced symmetricstrict monoidal functors. There is an evident forgetful functor U • : TSMC• → TSMC
that can be restricted to U s• : TSMC•s → TSMC s , and it has an ordinary left adjoint
F • : TSMC s → TSMC•s that freely adds morphisms ⊥A : I → A and ⊤A : A → I,
subject to the equations in (7).
The Int construction can be lifted over TSMC• . For a bipointed TSMC (C, ⊥, ⊤),byand ⊤Int(C)we define Int(C)-morphisms ⊥Int(C)A
A⊥Int(C)= ⊥ A+ ⊗ ⊤ A− ,A

⊤Int(C)= ⊤ A+ ⊗ ⊥ A− .
A

Then we define Int• (C, ⊥, ⊤) to be the tuple (Int(C), ⊥Int(C) , ⊤Int(C) ). One can easily
check that this is a bipointed TSMC. The mapping (C, ⊥, ⊤) 7→ Int• (C, ⊥, ⊤) extends
to a 2-functor over TSMC• , and the pseudo-monad structure of Int also makes Int• a
pseudo-monad. Furthermore, it is a strict lifting of Int along U.
Proposition 3. The triple E• = (F • , U • , Int• ) forms an extension of TSMCs.
Proposition 4. The tuple (A(Σ), ⊥, ⊤) is a bipointed TSMC, and it is equivalent to
F(L(Σ)). Therefore, quasi-SSUR ACs are E• -ACs.

4.3 Descriptional Composition for Stack AGs
In [18], Nakano introduced an extension of AC called stack AC, where we can use
stacks in attribute calculation rules. He then showed that the stack ACs satisfying certain linearity condition are closed under the descriptional composition. Inspired by his
extension, below we express his theory of stack ACs in our categorical framework by
setting-up an appropriate extension of TSMC. Our approach differs from Nakano’s
work as follows: 1) the concept of stack ACs given below allow stacks to be stackelements, and 2) we represent the empty stack by undefined stack ⊥, and combine stack
deconstructors (head, tail) into single operator dec.
We introduce a language S(Σ) and capture the stack ACs satisfying a linearity condition as AGs in S(Σ). In this language we can use a stack of type ρ, whose type is denoted by ρ∞ . Stacks are then manipulated by two operators: constructor cons : ρ, ρ∞ →
ρ∞ and deconstructor dec : ρ∞ → ρ, ρ∞ . The operator cons pushes a given value on agiven stack, while dec separates the top value of a given stack from the rest of it.
We move on to the formal definition of S(Σ). First, we define S(Σ)0 to be the setof pairs of the form (n, ρ) where n is a natural number and ρ is a Σ-type. We identify atype ρ ∈ Σ and the pair (0, ρ) ∈ S(Σ)0 . We denote a pair (n, ρ) by ρ∞...∞ , where n is thelength of ∞’s on the shoulder. Next, we define |S(Σ)| to be the set of finite sequencesof S(Σ)0 . Below we use metavariables B and C to denote elements in S(Σ)0 and |S(Σ)|,
respectively. The set of raw terms of S(Σ) is defined by
M ::= λx. let D in x
D ::= x = x | x = o(x) | x = ⊥B | x = consB (x, x) | x, x = decB (x).
The typing rules of S(Σ) extends the one for A(Σ) with cons and dec:x : B ⊢E x : B⊢E ⊥ B : Bo ∈ Σ ρ1 ···ρn →ρ
x1 : ρ1 , · · · , xn : ρn ⊢E o(x1 , · · · , xn ) : ρ

x : B, y : B∞ ⊢E cons B (x, y) : B∞

x : B∞ ⊢E decB (x) : B, B∞

Γ1 ⊢E M1 : C1 · · · Γl ⊢E Ml : Cl U ⊆ D⊢ M λx . let y1 = M1 , · · · , yl = Ml in z : C ′ → C ′′where U = Γ1 ∪ · · · ∪ Γl ∪ {z : C ′′ } and D = {x : C ′ , y1 : C1 , · · · , yl : Cl }, and eachvariable in Γ1 , · · · , Γn , x, y, z is different from the other. The set of axioms for S(Σ)expressions extends the one for A(Σ) with the following rules (leading λ is omitted):(let x, y = decB (z), z = cons B (x′ , y′ ), D in v) = (let x = x′ , y = y′ , D in v)(let x, y = decB (z), z = ⊥B∞ , D in v) = (let x = ⊥B , y = ⊥B∞ , D in v)(let z = consB (x, y), D in v) = (let D in v (z < FV(D) ∪ v ∪ {y})).
Definition 6. A quasi-SSUR stack AC from ∆ to Σ is a triple (I, S , a) where for each type
ρ ∈ ∆, Iρ, S ρ ∈ |S(Σ)|, and for each operator o ∈ ∆ρ1 ,··· ,ρn →ρ , ao is an S(Σ)-expressionof type ao : S ρ1 , · · · , S ρn , Iρ → S ρ, Iρ1 , · · · , Iρn .
Example 2. This example is from [18]. We consider a stack AC that converts reversepolish notations to ordinary expressions. Let Σ p and Σe be signatures defined as follows:∗→∗, m∗→∗ , r→∗ }) (n ∈ N),
Σ p = ({∗}, {p∗→∗
n ,a
∗,∗→∗
Σe = ({∗}, {num→∗, mul∗,∗→∗ }) (n ∈ N).
n , add

The signature Σ p is for the reverse-polish notation of expressions. For instance, a Σ p expression p3 (p2 (p5 (a(m(r))))) denotes (5 + 2) ∗ 3. The stack AC (I, S , a) that constructs
Σe -terms from reverse-polish expressions is the following (type annotations are omitted):I∗ = (∗)∞ , O∗ = ∗
apn = λs1 , i . let i1 = cons(numn , i) in s1 , i1
aa = λs1 , i . let h1 , t1 = dec(i), h2 , t2 = dec(t1 ), i1 = cons(add(h1 , h2 ), t2 ) in s1 , i1
am = λs1 , i . let h1 , t1 = dec(i), h2 , t2 = dec(t1 ), i1 = cons(mul(h1 , h2 ), i2 ) in s1 , i1
ar = λi . let h, t = dec(i) in h.
Definition 7. A TSMC with stack is a tuple (C, ⊥, ⊤, (−)∞, cons, dec) where– (C, ⊥, ⊤) is a bipointed TSMC,– (−)∞ : |C| → |C| is a mapping such that I∞ = I and (A ⊗ B)∞ = A∞ ⊗ B∞ ,– consA : A ⊗ A∞ → A∞ and decA : A∞ → A ⊗ A∞ are C-object indexed families ofmorphisms such thatdecA ◦ consA = idA⊗A∞ ,decI = consI = idI ,decA ◦ ⊥A = ⊥A ⊗ ⊥A∞ ,⊤A ◦ consA = ⊤A ⊗ ⊤A∞ ,consA⊗B = (consA ⊗ consB ) ◦ (A ⊗ σB⊗A∞ ⊗ B∞ ),decA⊗B = (A ⊗ σA∞ ⊗B ⊗ B∞ ) ◦ (decA ⊗ decB ).

A stack-preserving functor between TSMCs with stack is a traced symmetric strong
monoidal functor (F, φI, φA,B ) such that it preserves bipoints, F(A∞ ) = (FA)∞ andF(consA ) ◦ φA,A∞ = consFA

φA,A∞ ◦ decFA = F(decA ).

We define TSMCS to be the 2-category of TSMCs with stack, stack-preserving functors
and monoidal natural isomorphisms. Its 2-subcategory consisting of traced symmetric
strict monoidal functors is denoted by TSMCSs . We write U S : TSMCS → TSMC for
the canonical forgetful functor.
Next, U S can be restricted to a 2-functor U sS : TSMCSs → TSMC s , and when viewed
as an ordinary functor, it has a left adjoint F S : TSMC s → TSMCSs . This left adjoint
constructs a syntactic TSMC with stacks from a given category. We omit its detail, but
an object of the category F S C is an element of the countably infinite coproduct of themonoid (|C|, I, ⊗), that is, a sequence (k1 , C1 ) · · · (kn , Cn ) such that ki ∈ N, Ci ∈ |C|(1 ≤ i ≤ n) and ki , k j if i , j. The unit HC and counit EC of the adjunction is definedNn∞(ki ). The categoryby (on objects) HC (C) = (0, C) and HC (k1 , C1 ) · · · (kn , Cn ) =i=1 CiF S L(C) admits the strictification operator StrS satisfying thecondition
4of DefinitionN∞(ki )(Fρ
.
3; on objects it is defined by StrS (F)((k1 , ρ1 ) · · · (kn , ρn )) =i j)
1≤i≤n,1≤ j≤|ρi |S
Let (C, ⊥, ⊤, (−)∞, cons, dec) ∈ TSMC , which we just write C. We define theInt(C)
tuple IntS (C) = (Int(C), ⊥Int(C) , ⊤Int(C) , (−)∞ , consInt(C) , decInt(C) ) by⊥Int(C)= ⊥ A+ ⊗ ⊤ A− ,A

⊤Int(C)= ⊤ A+ ⊗ ⊥ A− ,A

= consA+ ⊗ decA− ,consInt(C)A

A∞

Int(C)= ((A− )∞ , (A+ )∞ ),= decA+ ⊗ consA− .
decInt(C)A

We define IntS of 1-cells and 2-cells in TSMCS to be Int of them. In this way IntS
becomes a 2-functor. One can check that we can adopt the structure of the pseudomonad Int to make IntS a pseudo-monad over TSMCS . Thus we obtain a pseudomonad IntS : TSMCS → TSMCS which is a strict lifting of the pseudo-monad Int
along U S .
Proposition 5. The triple ES = (F S , U S , IntS ) forms an extension of TSMC.
Proposition 6. The tuple (S(Σ), ⊥, ⊤, (−)∞, cons, dec) is a TSMC with stack, and isequivalent to F S (L(Σ)). Therefore, quasi-SSUR stack ACs are ES -ACs.

5 Conclusion and Discussion
We presented a categorical framework for capturing various extensions of ACs andtheir descriptional composition. By setting up appropriate extensions of TSMCs, thedescriptional composition of non-deterministic ACs, quasi-SSUR ACs and quasi-SSUR
stack ACs are covered by our framework. The framework uniformly guarantees theassociativity of the descriptional composition and the closure property of extended ACs
under the descriptional composition.
We strongly believe that our framework will contribute to extending the fusion transformation of functions with accumulating parameters. In attribute grammar framework,the fusion problem is reformulated as the descriptional composition of attribute couplings that represent functions with accumulating parameters. Extending this approachwith extra language features is a delicate task (see e.g. [18]), and our categorical framework indicates the direction of the extension of ACs so that the descriptional composition works. For instance, one may consider introducing the map operator to stackACs. In our framework, this is done by promoting the operator (−)∞ in Section 4.3 to afunctor, then form a suitable extension of TSMCs.
We also expect that our framework can provide an alternative account for the existing fusion methods that use circular let bindings to express fusion results as first-orderfunctional programs [22, 19, 13]. An interesting connection between these transformations and the category theory is that, these fusion results, when viewed as morphisms,
often have the same pattern as the composition of morphisms in Int(C); this is also observed in [13]. Through this similarity, our categorical view of the descriptional composition will be helpful to understand these fusion methods, and hopefully provide anequational proof of their correctness.
One possible future work is to implement the descriptional composition based on
our categorical framework. The major task will be to define the data structure representing TSMCs and implement the Int construction on them. The implementation task
breaks down the descriptional composition into fundamental operations on categories
and functors, each of which will be easily verifiable.
Acknowledgement The author is grateful to Susumu Nishimura and Craig Pastro for
discussions, and Masahito Hasegawa for his encouragement and helpful feedback.

References
1. Miklós Bartha. Linear deterministic attributed transformations. Acta Cybern., 6:125–147,
1983.
2. R. Blackwell, G. M. Kelly, and A. J. Power. Two-dimentional monad theory. Journal of pureand applied algebra, 59:1–41, 1989.
3. John Boyland. Conditional attribute grammars. ACM Trans. Program. Lang. Syst., 18(1):73–
108, 1996.
4. Laurian M. Chirica and David F. Martin. An order-algebraic definition of Knuthian semantics. Mathematical Systems Theory, 13:1–27, 1979.
5. Bruno Courcelle and Pierre Deransart. Proofs of partial correctness for attribute grammars
with applications to recursive procedures and logic programming. Inf. Comput., 78(1):1–55,
1988.
6. Harald Ganzinger. Increasing modularity and language-independency in automatically generated compilers. Sci. Comput. Program., 3(3):223–278, 1983.
7. Harald Ganzinger and Robert Giegerich. Attribute coupled grammars. In SIGPLAN Symposium on Compiler Construction ’84, pages 157–170. ACM, 1984.
8. Robert Giegerich. Composition and evaluation of attribute coupled grammars. Acta Inf.,
25(4):355–423, 1988.
9. Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec.
Springer-Verlag, 1999.
10. Thomas Johnsson. Attribute grammars as a functional programming paradigm. In Gilles
Kahn, editor, FPCA, volume 274 of Lecture Notes in Computer Science, pages 154–173.
Springer, 1987.

11. Andre Joyal, Ross Street, and Dominc Verity. Traced monoidal categories. Mathematical
Proceedings of the Cambridge Philosophical Society, 119(3):447–468, 1996.
12. Shin-ya Katsumata. Attribute grammars and categorical semantics. In Luca Aceto, Ivan
Damgrd, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor
Walukiewicz, editors, ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages
271–282. Springer, 2008.
13. Shin-ya Katsumata and Susumu Nishimura. Algebraic fusion of functions with an accumulating parameter and its improvement. In John H. Reppy and Julia L. Lawall, editors, ICFP,
pages 227–238. ACM, 2006.
14. Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory,2(2):127–145, 1968.
15. Donald E. Knuth. Correction: Semantics of context-free languages. Mathematical Systems
Theory, 5(1):95–96, 1971.
16. Anders Kock. Strong functors and monoidal monads. Archiv der Math., 23(1):113–120,
1972.
17. Saunders MacLane. Categories for the Working Mathematician (Second Edition), volume 5of Graduate Texts in Mathematics. Springer, 1998.
18. Keisuke Nakano. Composing stack-attributed tree transducers. Theory Comput. Syst.,
44(1):1–38, 2009.
19. Susumu Nishimura. Deforesting in accumulating parameters via type-directed transformations. In APLAS ’02, pages 145–159, 2002.
20. Susumu Nishimura and Keisuke Nakano. XML stream transformer generation through program composition and dependency analysis. Sci. Comput. Program., 54(2-3):257–290, 2005.
21. Miki Tanaka and John Power. Pseudo-distributive laws and axiomatics for variable binding.
Higher-Order and Symbolic Computation, 19(2-3):305–337, 2006.
22. Janis Voigtländer. Using circular programs to deforest in accumulating parameters. HigherOrder and Symbolic Computation, 17(1-2):129–163, 2004.

A

Proof of Theorem 2

1) Obvious. 2) First, we introduce an auxiliary binary operator c ′ . For functors A ∈TSMC′s (FL(∆), Int′ FL(Σ)) and B ∈ TSMC′s (FL(Σ), Int′ (C)), we define B c ′ A to
be Str′ ((B)♭ ◦ A). It is associative up to an isomorphism:
C c ′ (B c ′ A) = Str′ ((C)♭ ◦ (B)♭ ◦ A)  Str′ (((C)♭ ◦ B)♭ ◦ A)  (C c ′ B) c ′ A.
Let A ∈ TSMC s (L(∆), IntUFL(Σ)) and B ∈ TSMC s (L(Σ), IntUC). Then we have
B c A = Str(U((B)♭ ) ◦ A) = Str((B)♭ ◦ A) = Str′ ((B)♭ ◦ A) = (B c ′ A).
The bijection (−) : |TSMC′s (FC, D)| → |TSMC s (C, UD)| extends to an ordinary functor TSMC′s (FC, D) → TSMC s (C, UD), because it is defined as F = UF ◦ HC . Therefore if F and G are naturally isomorphic, so are F and G. Then we haveC c (B c A) = C c ′ (B c ′ A)  (C c ′ B) c ′ A = C c (B c A).
3) Note that N(T A(H( f ))) = A( f ). Since N is faithful, it is sufficient to show N ◦T (B c A) ◦ H( f ) = N ◦ T B ◦ T A ◦ H( f ).
N(T (B c A)(H( f ))) = Str((UB)# ◦ A)( f ) = (UB)# (N(T A(H( f ))))= (UB)(T A(H( f ))) = N(T B(T A(H( f )))).

B Traced Symmetric Monoidal Categories and the Int
Construction
Traced Symmetric Monoidal Category We recall the concept of trace operator [11].
A trace operator on a symmetric strict monoidal category (C, I, ⊗, σ) is a mapping
trAB,C : C(B ⊗ A, C ⊗ A) → C(B, C) satisfying the following equations.
(Naturality)h ◦ trAB,C ( f ) ◦ g = trAB′ ,C′ ((h ⊗ A) ◦ f ◦ (g ⊗ A))′
A(Dinaturality) trB,C ((C ⊗ g) ◦ f ) = trAB,C ( f ◦ (B ⊗ g))(Vanishing I)
trIA,B ( f ) = f
A⊗BA
B(Vanishing II)
trC,D(g) = trC,D(trC⊗A,D⊗A(g))
AA(Superposing) trB⊗C,B⊗D (B ⊗ f ) = B ⊗ trC,D f(Yanking)
trAA,A (σA,A ) = id.
We simplify the superposing axiom in [11] using naturality and dinaturality [9]. A
traced symmetric strict monoidal category (TSMC) is a pair of a symmetric strict
monoidal category and a trace operator on it. We say that a symmetric strong monoidal
functor (F, φI, φA,B ) : C → D between TSMCs C, D is traced if it satisfies F(trCA,B ( f )) =−1
trFC
FA,FB (φ B,C ◦ F f ◦ φA,C ).

The Int Construction Joyal, Street and Verity showed that the forgetful functor from the2-category of tortile monoidal categories to that of traced (braided) monoidal categories
has a left biadjoint, which they called Int [11]. This biadjunction can be restricted tothe one between TSMC and the 2-category of strict compact closed categories, strong
monoidal functors and monoidal natural isomorphisms. Like the usual construction ofmonads from adjunctions, we obtain a pseudo-monad over TSMC, which we also writeInt. Below we give an explicit definition of this pseudo-monad Int.
Let C ∈ TSMC. We define the TSMC Int(C) by the following data. An object isa pair (A+ , A− ) of C-objects. Below, when A is declared as an Int(C)-object, by A+
and A− we mean its first and second component. A morphism from A to B is a Cmorphism f : A+ ⊗ B− → B+ ⊗ A− . The identity is defined by idInt(C)= idA+ ⊗A− , and theA−composition of f : A → B and g : B → C is defined by g ◦Int(C) f = trAB+ ⊗C− ,C+ ⊗A− (h)
−
+
−
+
+
where h = (C ⊗ σB− ,A− ) ◦ (g ⊗ A ) ◦ (B ⊗ σA− ,C− ) ◦ ( f ⊗ C ) ◦ (A ⊗ σC− ,B− ). The(strict) tensor product in Int(C) is given by A ⊗Int(C) B = (A+ ⊗ B+ , A− ⊗ B− ) andf ⊗Int(C) g = (B+ ⊗ σA− ,D+ ⊗ C − ) ◦ ( f ⊗ g) ◦ (A+ ⊗ σC+ ,B− ⊗ D− ). The unit object of thistensor product is given by (I, I). The symmetry morphism is σInt(C)= σA+ ,B+ ⊗ σA− ,B− .
A,B
We give the trace operator with respect to the above symmetric monoidal structure by
+
⊗C−
−
−
+
+
(trInt(C) )CA,B ( f ) = trCA+ ⊗B− ,B+ ⊗A− ((B ⊗ σC+ ,A− ⊗ C ) ◦ f ◦ (A ⊗ σ B− ,C+ ⊗ C )).
We next give a functor IntC,D : TSMC(C, D) → TSMC(Int(C), Int(D)), which
we simply write by Int. We define Int of a traced symmetric strong monoidal functor(F, φI, φA,B ) : C → D to be the tuple (Int(F), φInt(F), φInt(F)A,B ) : Int(C) → Int(D) definedI+−−1= φI ⊗ φ−1
by Int(F)(A) = (FA , FA ), Int(F)( f ) = φB+ ,B− ⊗ F f ⊗ φA+ ,A− , φInt(F)I
I
Int(F)and φA,B = φA+ ,B+ ⊗ φ−1
A− ,B− . For a monoidal natural isomorphism α : F → G, we
define Int(α) : Int(F) → Int(G) by Int(α)A = αA+ ⊗ α−1
A− . These data determine a
2-endofunctor Int : TSMC → TSMC.
Let C ∈ TSMC. A calculation shows that the homset Int2 (C)(A, B) is identical toC(A++ ⊗ B−+ ⊗ B+− ⊗ A−− , B++ ⊗ A−+ ⊗ A+− ⊗ B−− ); thus we manipulate morphisms
in Int2 (C) as C-morphisms. The unit of the pseudo-monad Int is the traced symmetric
strict monoidal functor NC : C → Int(C) defined by NC (A) = (I, A) and NC ( f ) = f ,while the multiplication of Int is the traced symmetric strong monoidal functor MC :Int2 (C) → Int(C) defined by MC (A) = (A−− ⊗A++ , A−+ ⊗A+− ) and MC ( f ) = r−1
B,A ◦ f ◦rA,B ,where rA,B is the symmetry morphism σA−− ,A++ ⊗B−+ ⊗B+− in C. We also define monoidal
natural isomorphisms nF : Int(F) ◦ NC → ND ◦ F and mF : Int2 (F) ◦ MC → MD ◦Int(F)−+ +−for (F, φI , φA,B) ∈ TSMC(C, D) by (nF )A = idFA ⊗ φI and (mF )A = φ−1
A−− ,A++ ⊗ φA ,A .
These data determine pseudo-natural transformations (N, n) : Id → Int and (M, m) :Int2 → Int.
Finally, we define modifications λC : MC ◦ Int(NC ) → IdInt(C) and ρC : MC ◦NInt(C) → IdInt(C) to be identities, and τC : MC ◦ Int(MC ) → MC ◦ MInt(C) by (τC )A =++−).
(σA−−+ ,A−+− ⊗A+−− ⊗ A+++ ) ⊗ (σ−1
A−−− ,A−++ ⊗A+−+ ⊗ A
Theorem 3. The tuple (Int, (N, n), (M, m), τ, λ, ρ) forms a pseudo-monad on TSMC.