We denote by ∗ = Í ∈**N** the set of finite sequences of elements of , for any set . In any category C, we tend to write [, ] for the hom-set C(, ) between any two objects and . Finally, for any endofunctor , - alg denotes the usual category of -algebras and morphisms between them.

### 2 De Bruijn monads

In this section, we start by introducing De Bruijn monads. Then, we define lifting of assignments, the binding conditions, and the models of a binding signature in De Bruijn monads, De Bruijn -algebras. Finally, we construct the term De Bruijn -algebra.

### 2.1 Definition of De Bruijn monads

We start by fixing some terminology and notation, and then give the definition.

Definition 1. Given a set , an -assignment is a map **N** → . We sometimes merely use "assignment" when is clear from context.

Notation 21. Consider any map : × **N** → .

$$\begin{aligned} X^{\mathbb{N}} \times Y^{\mathbb{N}} &\to Z^{\mathbb{N}}\\ (f, \mathbf{g}) &\mapsto n \mapsto s(f(n), \mathbf{g}). \end{aligned}$$

We use similar notation for this map, i.e., [] () := () [].

Definition 2. A De Bruijn monad is a set , equipped with

satisfying, for all ∈ , and , : **N** → :

Example 2. The set **N** itself is clearly a De Bruijn monad, with variables given by the identity and substitution **N** × **N N** → **N** given by evaluation. This is in fact the initial De Bruijn monad, as should be clear from the development below.

Example 3. The set Λ := .**N**++ 2 of -terms forms a De Bruijn monad. The variables map **N** → Λ is the obvious one, while the substitution map Λ×Λ **N** → Λ is less obvious but standard. In Example 5, as an application of Theorem 2, we will characterise this De Bruijn monad by a universal property.

### 2.2 Lifting assignments

Given a De Bruijn monad , we define an operation called lifting on its set of assignments **N** → . It is convenient to stress that only part of the structure of De Bruijn monad is needed for this definition.

Definition 3. Consider any set , equipped with maps : × **N** → and : **N** → . For any assignment : **N** → , we define the assignment ⇑ : **N** → by (⇑ ) (0) = (0) (⇑ ) ( + 1) = () [↑],

where ↑: **N** → maps any to ( + 1).

Remark 1. Both ⇑ and ↑ depend on and (part of) (, ). Here, and in other similar situations below, we abuse notation and omit such dependencies for readability.

Of course we may iterate lifting:

Definition 4. Let ⇑ 0 = , and ⇑ +1 =⇑ (⇑ ).

### 2.3 Binding arities and binding conditions

Our treatment of binding arities reflects the separation between the first-order part of the arity, namely its length, which concerns the syntax, and the binding information, namely the binding numbers, which concerns the compatibility with substitution.

### Definition 5.

Let us now axiomatise what we call an operation of a given binding arity.

Definition 6. Let = (1, . . . , ) be any binding arity, be any set, : × **N** → , and : **N** → be any maps. An operation of binding arity is a map : → satisfying the following -binding condition w.r.t. (, ):

$$\forall \sigma: \mathbb{N} \to M, \mathbf{x}\_1, \dots, \mathbf{x}\_p \in M, \quad o(\mathbf{x}\_1, \dots, \mathbf{x}\_p)[\sigma] = o(\mathbf{x}\_1[\mathbb{N}^{n\_1} \ \sigma], \dots, \mathbf{x}\_p[\mathbb{N}^{n\_p} \ \sigma]). \tag{2}$$

Remark 2. Let us emphasise the dependency of this definition on and – which is hidden in the notations for substitution and lifting.

### 2.4 Binding signatures and algebras

In this section, we recall the standard notions of first-order (resp. binding) signatures, and adapt the definition of algebras to our De Bruijn context. Let us first briefly recall the former.

Definition 7. A first-order signature consists of a set of operations, equipped with an arity map ar : → **N**.

Definition 8. For any first-order signature := (, ar ), an -algebra is a set , together with, for each operation ∈ , a map : ar () → .

Let us now generalise this to binding signatures.

### Definition 9.

Example 4. The binding signature for -calculus has two operations lam and app, of respective arities (1) and (0, 0). The associated first-order signature has two operations lam and app, of respective arities 1 and 2.

Let us now present the notion of De Bruijn -algebra:

Definition 10. For any binding signature := (, ar ), a De Bruijn -algebra is a De Bruijn monad (, , ) equipped with an operation of binding arity ar (), for all ∈ .

In order to state our characterisation of the term model, we associate to any binding signature an endofunctor on sets, as follows.

Definition 11. The endofunctor Σ associated to a binding signature (, ar ) is defined by Σ () = Í ∈ |ar () | .

Remark 3. The induced endofunctor just depends on the underlying first-order signature.

Remark 4. As is well known, for any binding signature, the initial (**N** + Σ) algebra has as carrier the least fixed point .**N** + Σ ().

The following theorem defines the term model of a binding signature.

Theorem 1. Consider any binding signature = (, ar ), and let DB denote the initial (**N**+Σ)-algebra, with structure maps : **N** → DB and : Σ (DB) → DB. Then,

	- for all ∈ , the map DB satisfies the ar ()-binding condition w.r.t. (, ).

Proof. We have proved the result in both HOL Light [22] and Coq [20].

Remark 5. Point (i) may be viewed as an abstract form of recursive definition for substitution in the term model. The theorem thus allows us to construct the term model of a signature in two steps: first the underlying set, constructed as the inductive datatype .**N** + Σ (), and then substitution, defined by the binding conditions viewed as recursive equations.

Remark 6. We hope that our mechanisations [22,20] may be useful for future developments based on De Bruijn representation, to automatically generate the correct syntax and substitution from a suitable signature. This will have the advantage of reducing what needs to be read to make sure that the development actually does what is claimed. Normally, this part includes the whole definition of syntax and substitution, while our framework reduces it to only the binding signature. Our mechanisations may in fact be used for this purpose on existing developments, to certify the syntax and substitution, leaving only the binding signature for the reader to check.

Example 5. For the binding signature of -calculus (Example 4), the carrier of the initial model is .**N** + + 2 , and substitution is defined inductively by:

$$\begin{array}{c} \nu(n)[\sigma] = \sigma(n) \\ \lambda(e)[\sigma] = \lambda(e[\uparrow \sigma]) \\ (e\_1 \ e\_2)[\sigma] = e\_1[\sigma] \ e\_2[\sigma]. \end{array}$$

### 3 Initial-algebra semantics of binding signatures in De Bruijn monads

In this section, for any binding signature , we organise De Bruijn -algebras into a category, - DBAlg, and prove that the term De Bruijn -algebra is initial therein.

### 3.1 A category of De Bruijn monads

Let us start by organising general De Bruijn monads into a category:

Definition 12. A morphism (, , ) → (, , ) between De Bruijn monads is a set-map : → commuting with substitution and variables, in the sense that for all ∈ and : **N** → we have ([]) = () [ ◦ ] and ◦ = .

Remark 7. More explicitly, the first axiom says: ((, )) = ( (), ◦ ).

Notation 31. De Bruijn monads and morphisms between them form a category, which we denote by DBMnd.

Let us conclude this subsection by briefly mentioning a categorical point of view on the category of De Bruijn monads for the categorically-minded reader, in terms of relative monads [2].

Proposition 1. The category DBMnd is canonically isomorphic to the category of monads relative to the functor 1 → Set picking **N**.

Remark 8. Canonicity here means that the isomorphism lies over the canonical isomorphism [1, Set] Set.

According to the theory of [2], this yields:

Corollary 1. The tensor product ⊗ := × **N** induces a skew monoidal [28] structure on Set, and DBMnd is precisely the category of monoids therein.

Proof. To see this, let us observe that, by viewing any set , in particular **N**, as a functor 1 → Set, one may compute the left Kan extension of along **N**, which is a functor Lan**N**(): Set → Set. By the standard formula for left Kan extensions [21], we have Lan**N**() () × **N** = ⊗ . The result thus follows by [2, Theorems 4 and 5].

### 3.2 Categories of De Bruijn algebras

In this section, for any binding signature , we organise De Bruijn -algebras into a category - DBAlg.

Let us start by recalling the category of -algebras for a first-order :

Definition 13. For any first-order signature , a morphism → of algebras is a map between underlying sets commuting with operations, in the sense that for each ∈ , letting := ar (), we have ( (1, . . . , )) = ( (1), . . . , ( )).

We denote by - alg the category of -algebras and morphisms between them.

We now exploit this to define De Bruijn -algebras:

Definition 14. For any binding signature , a morphism of De Bruijn -algebras is a map : → between underlying sets, which is a morphism both of De Bruijn monads and of ||-algebras. We denote by - DBAlg the category of De Bruijn -algebras and morphisms between them.

Theorem 2. Consider any binding signature = (, ar ), and let DB denote the initial (**N**+Σ)-algebra. Then, the De Bruijn -algebra structure of Theorem 1 on DB makes it initial in - DBAlg.

Proof. We have proved the result in both HOL Light [22] and Coq [20].

### 4 Relation to presheaf-based models

The classical initial-algebra semantics introduced in [11] associates in particular to each binding signature a category, say Φ - Mon of models, while we have proposed in §3 an alternative category of models - DBAlg. In this section, we are interested in comparing both categories of models.

In fact, we find that both include exotic models, in the sense that we do not see any loss in ruling them out. And when we do so, we obtain equivalent categories.

### 4.1 Trimming down presheaf-based models

First of all, in this subsection, let us recall the mainstream approach we want to relate to, and exclude some exotic objects from it.

Presheaf-based models We start by recalling the presheaf-based approach. The ambient category is the category of functors [**F**, Set], where **F** denotes the category of finite ordinals, and all maps between them. As is well-known, this category is equivalent to the category [Set, Set] of finitary endofunctors on sets, and inherits from it a substitution monoidal structure. By construction, monoids for this monoidal structure are equivalent to finitary monads on sets.

The idea is then to interpret binding signatures as endofunctors Φ on [**F**, Set], and to define models as monoids equipped with Φ-algebra structure, satisfying a suitable compatibility condition.

The definition of Φ relies on an operation called derivation:

### Definition 15 (Endofunctor associated to a binding signature).

Proposition 2. Through the equivalence with finitary functors, derivation becomes 0 () = ( + 1), for any finitary : Set → Set and ∈ Set.

Example 6. For the binding signature of Example 4 for -calculus we get Φ () () = () 2 + ( + 1).

Next, we want to express the relevant compatibility condition between algebra and monoid structure. For this, let us briefly recall the notion of pointed strength, see [11,10] for details.

Definition 16. A pointed strength on an endofunctor : C → C on a monoidal category (C, ⊗, , , , ) is a family of morphisms ,(,) : () ⊗ → ( ⊗ ), natural in ∈ C and (, : → ) ∈ /C, the coslice category below , satisfying two coherence conditions.

The next step is to observe that binding signatures generate pointed strong endofunctors.

Definition 17. The derivation endofunctor ↦→ 0 on [**F**, Set] has a pointed strength, defined through the equivalence with finitary functors by

(() + 1) ( ()+1) −−−−−−−−−−→ (() + (1)) [ (1), (2) ] −−−−−−−−−−−−−−−→ (( + 1)).

Product, coproduct, and composition of endofunctors lift to pointed strong endofunctors, which yields:

Corollary 2 ([11,10]). For all binding signatures , Φ is pointed strong.

At last, we arrive at the definition of models.

Definition 18. For any pointed strong endofunctor on C, an -monoid is an object equipped with -algebra and monoid structure, say : () → , : ⊗ → , and : → , such that the following pentagon commutes.

A morphism of -monoids is a morphism in C which is a morphism both of -algebras and of monoids. We let - Mon denote the category of -monoids and morphisms between them.

Example 7. For the binding signature of Example 4, a Φ -monoid is an object , equipped with maps 0 → and 2 → , and compatible monoid structure. Compatibility describes how substitution should be pushed down through abstractions and applications.

Well-behaved presheaves The exoticness we want to rule out only concerns the underlying functor of a model, so we just have to define well-behaved functors in [**F**, Set].

Well-behavedness for a functor : **F** → Set is about getting closed terms right. More precisely, for some finite sets and , an element of ( + ) which both exists in () and () should also exist in (∅), and uniquely so. This says exactly that should preserve the pullback

Remark 9. The reader might wonder about other, i.e., non-empty pullbacks. But these are automatically preserved, by [29, Proposition 2.1].

### Definition 19.

Example 8. As an example of a non well-behaved finitary monad, consider the monad of -calculus but edited so that (∅) = ∅.

The important result for comparing the presheaf-based approach with ours is the following.

Proposition 3. The subcategory Φ - Monwb includes the initial object.

Proof. Roughly, closed terms are isomorphic to terms in two free variables that use neither the first, nor the second.

Remark 10. In most natural situations, all models are in fact well-behaved [16, Proposition 5.17].

### 4.2 Trimming down De Bruijn monads

Let us now turn to well-behaved De Bruijn algebras. Here well-behavedness is about finitariness. However, it may not be immediately clear how to define finitariness of a De Bruijn monad.

Definition 20. A De Bruijn monad (, , ) is finitary iff each of its elements ∈ has a (finite) support ∈ **N**, in the sense that for all : **N** → **N** fixing the first numbers, the corresponding renaming ◦ fixes .

Example 9. By Proposition 4 below, the initial -algebra is finitary, for any binding signature . For a counterexample, consider the greatest fixed point .**N**+Σ (), for any with at least one operation with more than one argument. E.g., if has an operation of binding arity (0, 0), like application in -calculus, then the term (0) ((1) ((2) . . .)) does not have finite support.

Definition 21. For any binding signature , let - DBAlgwb denote the full subcategory spanning De Bruijn -algebras whose underlying De Bruijn monad is finitary.

Proposition 4. The subcategory - DBAlgwb includes the initial object.

### 4.3 Bridging the gap

We may at last state the relationship between initial-algebra semantics of binding signatures in presheaves and in De Bruijn monads:

Theorem 3. Consider any binding signature . The subcategories Φ - Monwb and - DBAlgwb are equivalent.

Proof. See [16, Appendix A].

Remark 11. The moral of this is that, if one removes exotic objects from both Φ - Mon and - DBAlg, then one obtains equivalent categories, which both retain the initial object. Thus, the two approaches to initial-algebra semantics of binding signatures differ only marginally.

Restricting attention to well-behaved objects, we may thus benefit from the strengths of both approaches. Typically, in De Bruijn monads, free variables need to be computed explicitly, while presheaves come with intrinsic scoping, as terms are indexed by sets of potential free variables. Conversely, in some settings, observational equivalence may relate programs with different sets of free variables [25]. In such cases, it is useful to have all terms collected in one single set. This needs to be computed (and involves non-trivial quotienting) in presheaves, while it is direct in De Bruijn monads.

### 5 Strength-based interpretation of the binding conditions

In the previous section, we have compared the category - DBAlg of models of a binding signature in De Bruijn monads with the standard category of Φ monoids [11]. In this section, we establish a different kind of link, by showing that, for any binding signature , both categories - DBAlg and Φ - Mon are instances of a common categorical construction. We have seen that the standard category Φ - Mon is constructed from the pointed strong endofunctor Φ, so we would like a similar construction of - DBAlg. However, pointed strong endofunctors live on monoidal categories [11,10], while we have seen in Corollary §1 that **N** and the tensor product only equip Set with skew monoidal structure. In order to bridge this gap, we resort to a generalisation of pointed strengths to skew monoidal categories proposed by Borthelle et al. [6].

We give a condensed account: the interested reader is referred to [16, §6].

The starting point is that the endofunctor Σ associated to any given binding signature may be equipped with a family of maps

$$\mathbf{d}\mathbf{b}\mathbf{s}\_S \colon \Sigma\_S(X)\otimes Y \to \Sigma\_S(X\otimes Y)\text{-}\mathbb{N}$$

However, in order for such a map to be well-defined, we need to assume that features variables and renaming, i.e., that it is a pointed **N**-module, as we now introduce:

### Definition 22.

Example 10. Any De Bruijn monad (, , ) (in particular **N** itself) has a canonical structure of pointed **N**-module given by and (, ) = [ ◦ ].

We may now define the map dbs. Lifting of assignments (Definition 3) straightforwardly generalises to pointed **N**-modules. Recalling the definition

$$\Sigma\_S(X) = \sum\_{o \in O} X^{p\_o},$$

where ar () = ( 1 , . . . , ) for all ∈ , we thus simply have:

Definition 23. For any binding signature = (, ar ), the De Bruijn strength dbs of the induced endofunctor Σ is defined by

$$\begin{aligned} \Sigma\_{\mathcal{S}}(X) \otimes Y &\to \Sigma\_{\mathcal{S}}(X \otimes Y) \\ ((o, (\mathbf{x}\_1, \dots, \mathbf{x}\_{p\_o})), \sigma) &\mapsto (o, ((\mathbf{x}\_1, \|\!\|^{\mathfrak{n}\_1}\sigma), \dots, (\mathbf{x}\_{p\_o}, \|\!\|^{\mathfrak{n}\_{p\_o}}\sigma))), \end{aligned}$$

for all sets and pointed **N**-modules , with again ar () = ( 1 , . . . , ).

The fact that any De Bruijn monad is in particular a pointed **N**-module by Example 10 enables the definition of models in the strength-based approach:

Definition 24. For any binding signature , a Σ-monoid is an object , equipped with monoid and Σ-algebra structure, say : ⊗ → , : **N** → , and : Σ () → , making the following pentagon commute.

$$\underbrace{\Sigma\_S(X)\otimes X}\_{a\otimes X}\xrightarrow{\text{dbs}\,X}\underbrace{\Sigma\_S(X\otimes X)\xrightarrow{\Sigma\_S(s)}\Sigma\_S(X)}\_{s}\tag{3}$$

A morphism of Σ-monoids is a map which is both a monoid and a Σ-algebra morphism.

Let Σ - Mon denote the category of Σ-monoids and morphisms between them.

Remark 12. In [16], this definition is framed in a more general context, notably emphasising the fact that dbs is in fact a structural strength on the endofunctor Σ.

We may at last relate the initial-algebra semantics of §3 with the strength-based approach:

Proposition 5. For any binding signature = (, ar ) and De Bruijn monad (, , ) equipped with a map : → for all ∈ with ar () = (1, . . . , ), the following are equivalent:

Corollary 3. For any binding signature , we have an isomorphism Σ - Mon - DBAlg of categories over Set.

This readily entails the following (bundled) reformulation of Theorems 1 and 2.

Corollary 4. Consider any binding signature = (, ar ), and let DB denote the initial (**N**+Σ)-algebra, with structure maps : **N** → DB and : Σ (DB) → DB. Then:

	- the map **N** ⊗ DB ⊗DB −−−−−−→ DB ⊗ DB −→ DB coincides with the left unit of the skew monoidal structure (, ) ↦→ (), and – the pentagon (3) (with Σ := Σ) commutes.

Proof. Let Mon(Set) denote the category of monoids in Set for the skew monoidal structure. We have an equality Mon(Set) = DBMnd of categories, and the algebra structure Σ (DB) → DB is merely the cotupling of the maps DB of Theorem 1. This correspondence translates one statement into the other.

Remark 13. This result hints at a potential push-button proof of Theorems 1 and 2 (and Corollary 4). Indeed, it is almost an instance of [6, Theorem 2.15]: the latter is stated for general skew monoidal categories instead of merely Set, but does not directly apply in the present setting, because it assumes that the tensor product is finitary in the second argument.

### 6 Simply-typed extension

In this section, we extend the framework of §2–3, which is untyped, to the simplytyped case. The development essentially follows the same pattern, replacing sets with families.

We fix in the whole section a set **T** of types, and call **T**-sets the objects of Set**T** . A morphism → is a family (() → ()) ∈**T** of maps.

### 6.1 De Bruijn **T**-monads

In this subsection, we define the typed analogue of De Bruijn monads.

The role of **N** will be played in the typed context by the following **T**-set.

Definition 25. Let N ∈ Set**T** be defined by N() = **N**.

Remark 14. This provides a countable set of variables at each type, which may not quite be what the reader would have called "typed De Bruijn representation". An inconvenience of this representation is that an "erasure" map from typed to untyped terms appears to need to rely on a bijection **T** × **N N** for "renaming" variables. In particular, not all indices can be preserved by such a map.

Definition 26. Given a **T**-set , an -assignment is a morphism N → . We sometimes merely use "assignment" when is clear from context.

The analogue of the tensor product ⊗ = × **N** will be played by [N, ] ·, i.e., the iterated self-coproduct of , with one copy per -assignment.

Notation 61. For coherence with the untyped case, we tend to write an element of ( [N, ] · ) () as (, ), with ∈ () and : N → . Furthermore, Notation 21 straightforwardly adapts to the typed case.

The definition of De Bruijn monads generalises almost mutatis mutandis:

Definition 27. A De Bruijn **T**-monad is a **T**-set , equipped with

– a substitution morphism : [N, ] · → , which takes an element ∈ and an assignment : N → , and returns an element [ ], and – a variables morphism : N → ,

such that for all ∈ , and , : N → , we have

$$\mathbf{x}\begin{bmatrix} f \end{bmatrix}\begin{bmatrix} \mathbf{g} \end{bmatrix} = \mathbf{x}\begin{bmatrix} f\begin{bmatrix} \mathbf{g} \end{bmatrix} \end{bmatrix} \qquad \qquad \mathbf{v}(n)\begin{bmatrix} f \end{bmatrix} = f(n) \qquad \qquad \mathbf{x}\begin{bmatrix} \mathbf{v} \end{bmatrix} = \mathbf{x}\begin{bmatrix} \mathbf{x} \end{bmatrix}$$

Example 11. The set ΛST of simply-typed -terms with free variables of type in **N**× {}, considered equivalent modulo -renaming, forms a De Bruijn monad. Variables N → ΛST are given by mapping, at any , any ∈ **N** to the variable (, ). Substitution [N, ΛST] · ΛST → ΛST is standard, capture-avoiding substitution. One main purpose of this section is to characterise ΛST by a universal property, and reconstruct it categorically.

Morphisms generalise straightforwardly, and we get:

Proposition 6. De Bruijn **T**-monads and morphisms between them form a category DBMnd(**T**).

### 6.2 Initial-algebra semantics

We now adapt the initial-algebra semantics of §3 to the typed case. Let us start by generalising lifting to the typed case. This relies on a typed form of lifting, which acts on all variables of a given type, leaving all other variables untouched.

Definition 28. Let (, , ) denote any De Bruijn **T**-monad. We first define a typed analogue ↑ of the ↑ of Definition 3, as below left, and then the lifting of any assignment : N → as below right.

$$\begin{array}{ll} (\uparrow^{\tau})\_{\tau}(n) = \upsilon\_{\tau}(n+1) & (\uparrow^{\tau} \ \sigma)\_{\tau}(0) = \upsilon\_{\tau}(0) \\ (\uparrow^{\tau})\_{\tau'}(n) = \upsilon\_{\tau'}(n) & (\not\!f\; \tau \neq \tau') \\ & & (\uparrow^{\tau} \ \sigma)\_{\tau'}(n+1) = \sigma\_{\tau}(n)[\uparrow^{\tau}] \\ & & (\uparrow^{\tau} \ \sigma)\_{\tau'}(n) = \sigma\_{\tau'}(n)[\uparrow^{\tau}] & (\not\!f\; \tau \neq \tau'). \end{array}$$

Finally, for any sequence = (1, . . . , ) of types, we define ⇑ inductively, by ⇑ = and ⇑ , =⇑ (⇑ ), where denotes the empty sequence.

We then generalise first-order and binding arities. The main point is:

Definition 29. A binding arity is an element of (**T** ∗ × **T**) ∗ × **T**, i.e., a tuple ( ( (1, 1), . . . , (, )), ), where each ∈ **T** ∗ is a list of types, and each , as well as , are types, thought of as an inference rule 1 ` <sup>1</sup> . . . ` ` ·

Example 12. The binding signature for simply-typed -calculus has two operations lam, 0 and app, 0 for all types and 0 , of respective arities

$$\begin{array}{ccc} \frac{\tau \vdash \tau'}{\vdash \tau \rightarrow \tau'} & & \text{and} \\ \frac{\tau \vdash \tau \rightarrow \tau'}{\vdash \tau'} & & \dagger \vdash \tau' \end{array}$$

This allows us to generalise binding conditions, as follows.

Definition 30. Let = ( ( (1, 1), . . . , (, )), ) be any binding arity, and be any set equipped with morphisms : [N, ] · → and : N → . An operation of binding arity is a map : (1) × . . . × () → () satisfying the following -binding condition w.r.t. (, ):

$$\begin{array}{l} \forall \sigma: \mathbf{N} \to M, \mathbf{x}\_1, \dots, \mathbf{x}\_p \in M(\tau\_1) \times \dots \times M(\tau\_p),\\ o(\mathbf{x}\_1, \dots, \mathbf{x}\_p)[\sigma] = o(\mathbf{x}\_1[\mathbb{M}^{\gamma\_1} \ \sigma], \dots, \mathbf{x}\_p[\mathbb{M}^{\gamma\_p} \ \sigma]). \end{array} \tag{4}$$

·

We may now generalise signatures and their models.

Definition 31. A **T**-binding signature consists of a set of operations, equipped with an arity map → (**T** ∗ × **T**) ∗ × **T**.

Definition 32. Consider any **T**-binding signature := (, ar ). A De Bruijn -algebra consists of a De Bruijn **T**-monad (, , ), together with algebra structure on for the underlying first-order signature ||, in the obvious sense, such that for all ∈ with arity ar () = ( ( (1, 1), . . . , (, )), ), the structural map : (1) × . . . × () → () satisfies the ar ()-binding condition w.r.t. (, ).

We denote by - DBAlg the category of De Bruijn -algebras and (the obvious notion of ) morphisms between them.

Finally, following the untyped case, we may associate to each signature an endofunctor Σ, and we have the following typed extension of the initiality theorem.

Theorem 4. For any **T**-binding signature , let DB denote the initial (N+Σ) algebra, with structure maps : N → DB and : Σ (DB) → DB, inducing maps DB : DB (1) × . . . × DB () → DB () for all ∈ with ar () = ( ( (1, 1), . . . , (, )), ). Then:

Example 13. While we saw in Example 12 that the De Bruijn monad of simplytyped -calculus terms admits a simple signature, there is another relevant, related monad, whose elements at any type are values of that type. (Indeed, values are closed under value substitution.) It is relatively straightforward to design a binding signature for this De Bruijn monad, following [15].

### 7 Equations

In this section, we introduce a notion of equational theory for specifying (typed) De Bruijn monads, following ideas from [8].

### Definition 33. A De Bruijn equational theory consists of

Example 14. Recalling the binding signature Λ for -calculus from Example 4, let us define a De Bruijn equational theory for -equivalence. We take = (1, 0), and for any De Bruijn Λ-algebra ,

– () has as structure map (1, 2) ↦→ app(lam(1), 2) while

– () has as structure map (1, 2) ↦→ 1 [2 · id]. (Here 2 · id denotes the assignment 0 ↦→ 2, + 1 ↦→ ().)

Definition 34. Given an equational theory = (, , , ), a De Bruijn algebra is a De Bruijn -algebra such that () = ().

Let - DBAlg denote the category of -algebras, with morphisms of De Bruijn -algebras between them.

Remark 15. The category - DBAlg is an equaliser of and in CAT.

Let us now turn to characterising the initial De Bruijn -algebra, for any De Bruijn equational theory . For this, we introduce the following relation.

Definition 35. For any De Bruijn equational theory = (, , , ), with = (, ar ) and = ( 0 , ar 0 ), let DB denote the initial (N + Σ)-algebra. We define ∼ to be the smallest equivalence relation on DB satisfying the following rules,

$$\begin{array}{cc} \rho\_{L(\text{DB}\_{\text{S}})}'(e\_1, \dots, e\_p) \sim\_E \rho\_{R(\text{DB}\_{\text{S}})}'(e\_1, \dots, e\_p) \\\\ \hline \\ e\_1 \sim\_E e\_1' & \dots & e\_q \sim\_E e\_q' \\\hline \\ o\_{\text{DB}\_{\text{S}}}(e\_1, \dots, e\_q) \sim\_E o\_{\text{DB}\_{\text{S}}}(e\_1', \dots, e\_q') \end{array}$$

for all , 1, . . . in DB, 0 ∈ 0 with |ar 0 ( 0 )| = , and ∈ with |ar ()| = .

Example 15. For the equational theory of Example 14, the first rule instantiates precisely to the -rule, while the second enforces congruence.

Theorem 5. For any equational theory = (, , , ), - DBAlg admits an initial object, whose carrier set is the quotient DB/∼ .

Proof. This has been mechanised in Coq [20] and HOL [22].

Example 16. The initial model for the equational theory of Example 14 is the quotient of -terms in De Bruijn representation by -equivalence.

Remark 16. In [16, §9], we mention an equivalent way of defining De Bruijn equational theories in terms of modules.

### 8 Conclusion

We have proposed a simple, set-based theory of syntax with variable binding, which associates a notion of model (or algebra) to each binding signature, and constructs a term model following De Bruijn representation. The notion of model features a substitution operation. We have experienced the simplicity of this theory by implementing it in both Coq and HOL Light.

We have furthermore equipped the construction with an initial-algebra semantics, organising the models of any binding signature into a category, and proving that the term model is initial therein.

We have then studied this initial-algebra semantics in a bit more depth, in two directions. We have first established a formal link with the mainstream, presheaf-based approach [11], proving that well-behaved models (in a suitable sense on each side of the correspondence) agree up to an equivalence of categories. We have then recast the whole initial-algebra semantics into the mainstream, abstract framework of [11,10]. Finally, we have shown that our theory extends easily to a simply-typed setting, and smoothly incorporates equations.

### References

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.

### Uniform Guarded Fragments

Reijo Jaakkola()

Tampere University, Tampere, Finland<EMAIL_ADDRESS>https://reijojaakkola.github.io

Abstract. In this paper we prove that the uniform one-dimensional guarded fragment, which is a natural polyadic generalization of guarded two-variable logic, has the Craig interpolation property. We will also prove that the satisfiability problem of uniform guarded fragment is NExpTime-complete.

Keywords: Guarded fragment · Interpolation · Satisfiability problem.

### 1 Introduction

The guarded fragment GF is a well studied fragment of first-order logic FO, which was introduced by Andr´eka, van Benthem and N´emeti [1] as a generalization of modal logic. Informally speaking, GF is obtained from FO by requiring that all quantification must be relativised by FO-atoms, which is motivated by the observation that "quantificaction" in modal logics is relativised by accessability relations. Like modal logic, GF behaves well both computationally and model-theoretically. In particular, it is decidable, it has a (generalized) treemodel property and it satisfies various preservation theorems [1,7].

We say that a logic L has Craig interpolation property (CIP), if for every two formulas ϕ and ψ of L we have that if ϕ |= ψ, then there exists a third formula — the interpolant — χ of L, so that ϕ |= χ, χ |= ψ and χ contains only relation symbols which occur in both ϕ and χ. CIP is widely regarded as a property that a "nice" logic should have and for (reasonable logics with compactness) it implies several other desirable model-theoretic properties such as Projective Beth Definability and Robinson's consistency theorem [1,4,13,19].

It is well-known that various modal logics have CIP [1,6,19], while GF fails to have it [11]. This is somewhat surprising, given that GF is a very natural generalisation of modal logic, and certainly raises the question of how the syntax of GF should be modified so as to obtain a logic which does have CIP, and which also behaves well both computationally and model-theoretically. One option would be to extend further the expressive power of GF, and in this direction we have the guarded negation fragment, which has CIP, is decidable and shares with GF various desirable model-theoretic properties [2].

The other option (and the one which is more relevant for this paper) is to investigate fragments of GF. In this direction we also have a positive result,

P. Bouyer and L. Schr¨oder (Eds.): FoSSaCS 2022, LNCS 13242, pp. 409–427, 2022. https://doi.org/10.1007/978-3-030-99253-8\_21

namely that GF2 — the two-variable fragment of GF — has CIP [11]. Given this result, it is natural to ask whether there exists a polyadic extension of GF2 which would also have CIP, where by a polyadic extension we mean intuitively a logic which contains GF2 and can express non-trivial properties of polyadic relations. Indeed, it seems rather unlikely that there would not be such an extension, since it is well-known that there are polyadic modal logics which have CIP [1].

In [9] the uniform one-dimensional fragment UF1 was introduced, which is a very natural polyadic extension of the two-variable fragment FO2 of FO. Roughly speaking, UF1 is obtained from FO by requiring that each maximal existential (or universal) block of quantifiers leaves at most one variable free and that when forming boolean combinations of formulas with more than one free variable, the formulas need to have exactly the same set of variables. Formulas satisfying the first restriction are called one-dimensional, while formulas satisfying the second restriction are called uniform. In [16] it was proved that UF1 has the finite model property and the complexity of its satisfiability problem is NExpTime-complete, which is the same as for FO2 [8]. The research around UF1 and its variants has been quite active, see for instance [12,14,15,17,18].

Given that UF1 is a polyadic extension of FO2 , the guarded UF1 is a natural candidate for being a polyadic extension of GF2 with CIP. As the first main result of this paper we will prove that guarded UF1 does, in fact, have CIP. Our proof follows closely the argument given in [11] for proving that GF2 has CIP, the main technical difference being that the proof presented in [11] uses crucially the fact that in the case of GF2 we can assume live sets to have size at most two, while in our case we have to deal with live sets of arbitrary size.

Since the research around modal-like fragments of FO is largely motivated by the fact that their satisfiability problems are often decidable, it is natural to also study the complexity of the satisfiability problem of the guarded UF1, which was in fact already done in [15]. More precisely it was proved in [15] that the satisfiability problem of one-dimensional GF is in NExpTime, while it is already NExpTime-hard for guarded UF1. These results left open the problem of determining the complexity of uniform GF and as the second main result of this paper we will prove that the satisfiability problem of uniform GF is also in NExpTime (and hence it is NExpTime-complete).

We also emphasize that as a necessary by-product of this second technical result, we isolate the uniformity restriction imposed to formulas of UF1 as an independent syntactical restriction and provide a formal definition for it (which so far has been missing from the literature). 1 We believe that uniformity is an important and a natural syntactical restriction (at least) in the context of fragments of FO. Indeed, in addition to UF1 there are several known decidable fragments of FO which satisfy this restriction up to some degree, such as the one-binding fragments introduced in [20] and the ordered logic introduced in [10]. We hope that the results presented in this paper provide further motivation for the study of various uniform fragments of FO.

1 To be precise, we only define what it means for a formula to be uniform in the context of GF; however, it is easy to extend this definition for other logics.

The structure of this paper is as follows. After the preliminaries in Section 2, we define a notion of bisimulation for UGF1 and establish its basic properties in Section 3. After this we will prove that UGF1 has CIP in Section 4. In Section 5 we will establish that the complexity of the satisfiability problem of uniform GF is NExpTime-complete. The final Section will list some new problems that the research conducted in this paper raises.

### 2 Preliminaries

### 2.1 Notation

In this paper we will work with vocabularies which do not contain constants and function symbols. We will also assume that there are no relation symbols of arity 0. We will use the Fraktul capital letters to denote structures, and the corresponding Roman letters to denote their domains. Given a model A and C ⊆ A, we will use A C to denote the restriction of A to the set C.  Given two tuples a and b of the same length, we will use a 7→ b and p : a → b to denote the mapping induced by the relation ai 7→ bi . Given a tuple a = (a1, . . . , an) and a unary function f, we will use f(a) to denote the tuple (f(a1), . . . , f(an)). Given a positive integer n we will denote [n] = {1, . . . , n}. Finally, if a = (a1, . . . , an) and k ≥ n and µ : [k] → [n] is a surjection, we will use aµ to denote the tuple (aµ(1), . . . , aµ(k)).

#### 2.2 Types and Tables

The following definitions are standard in the context of UF1 and were first introduced in [16]. Let σ be a vocabulary. Given a set X = {x1, . . . , xn} of distinct variables and a k-ary relation R ∈ σ, we say that an atomic formula R(xi1 , . . . , xik ) is an X-atom over σ, if X = {xi1 , . . . , xik }. If α is an X-atom, then α and ¬α are both X-literals over σ. A 1-type over σ is a maximal satisfiable set of {x}-literals over σ. We identify 1-types π with conjunctions of their elements

$$\bigwedge^{\pi(x)}$$

A k-table is a tuple hρ, π1, . . . , πki, where each π` is a 1-type over σ, while ρ is a maximal satisfiable set of {x1, . . . , xk}-literals over σ.  Given a 1-type π over σ, we say that a ∈ A realizes π if π is the unique 1-type so that A |= π[a]; we denote by tpσ A[a] the (unique) 1-type π over σ which is realized by a in A. For distinct elements a1, . . . , ak ∈ A we will use tpσ A[a1, . . . , ak] to denote the (unique) k-table over σ which is realized by the tuple (a1, . . . , ak).

### 2.3 Syntax of Uniform Fragments of GF

Given a vocabulary σ, we define GF[σ] to be the smallest set F which satisfies the following requirements.

$$
\exists \overline{y} (\alpha(\overline{x}) \land \psi(\overline{x})) \in \mathcal{F},
$$

where y ⊆ x and α is an atomic formula over σ.

If the vocabulary σ is irrelevant or known from the context, then we will simply use GF to denote GF[σ].

 We will start by making the technical remark that we will define recursively the set of subformulas Sf(ϕ) of ϕ ∈ GF otherwise in a standard way, except that for formulas of the form ϕ := ∃y(α(x) ∧ ψ(x)), we define Sf(ϕ) to be

$$\{\exists \overline{y} (\alpha(\overline{x}) \land \psi(\overline{x}))\} \cup \text{Sf}((\alpha(\overline{x}) \land \psi(\overline{x}))).$$

In other words, we treat each maximal sequence of existential quantification as a single logical operator.

Definition 1. Let ϕ ∈ GF be a formula. We say that ϕ is one-dimensional, if every subformula of ϕ of the form

$$\exists \overline{y} (\alpha(\overline{x}) \land \psi(\overline{x})) $$

has at most one free variable. In other words each maximal sequence of (guarded) existential quantification leaves at most one variable free.

Next we will define what it means for a formula of GF to be uniform. The precise definition turns out to be somewhat technical, and we will start with the following auxiliary definition.

Definition 2. Let X be a (possibly empty) set of variables and let σ be a vocabulary. A relative X-atom over σ is a formula ψ of GF[σ] which satisfies one of the following conditions.

With the aid of this definition we are in a position where we can define the notion of uniformity formally.

Definition 3. Let ϕ ∈ GF[σ] be a formula. We say that ϕ is uniform, if every subformula ψ of ϕ is a boolean combination of relative X-atoms, where X is the set of free variables of ψ.

Remark 1. Consider a uniform quantifier-free formula ψ(x1, . . . , xk) of GF[σ]. Let A be a σ-model and let (a1, . . . , ak) be a tuple of not necessarily distinct elements. Then whether or not

$$\mathfrak{A} \mid = \psi(a\_1, \dots, a\_k),$$

holds depends only on the table of (c1, . . . , c`), where (c1, . . . , c`) is an arbitrary enumeration of the set of distinct elements of (a1, . . . , ak).

The definition of uniformity is somewhat technical, but the following examples should clarify the intuition behind it.

Example 1. Let σ = {S, R, P}, where S is a ternary relation symbol, R is a binary relation symbol and P is a unary relation symbol. The formula

∃x∃y(P(x) ∧ R(x, y) ∧ S(x, y, y) ∧ R(y, x) ∧ P(y)))

is both uniform and one-dimensional. On the other hand the formula

∃x∃y(∃z(S(x, y, z) ∧ P(z)) ∧ R(x, y) ∧ S(x, y, x))

is uniform but not one-dimensional. Finally, the formula

∃x∃y∃w(R(x, y) ∧ ∃zS(x, w, z))

is neither one-dimensional nor uniform.

Example 2. The standard translation of polyadic modal logic into FO results in formulas of the form

$$\exists x\_1 \dots \exists x\_k (R(x\_0, x\_1, \dots, x\_k) \land \bigwedge\_{1 \le \ell \le k} \psi\_\ell(x\_\ell))$$

which are uniform and one-dimensional [5].

We will use UGF to denote the set of formulas of GF which are uniform and UGF1 to denote the set of formulas of GF which are both uniform and one-dimensional. Throughout this paper we will use ϕ(x1, . . . , xn), where all the variables in the tuple (x1, . . . , xn) are distinct, to denote a formula of either UGF1 or UGF such that either {x1, . . . , xn} is precisely the set of free variables of ϕ or ϕ has at most one free variable which belongs to {x1, . . . , xn} or ϕ is of the form xi = xj , where 1 ≤ i, j ≤ n.

### 2.4 Interpolation

We start by recalling the definition of the Craig interpolation property.

Definition 4. Given a logic L, we say that L has the Craig interpolation property (CIP), if for every ϕ ∈ L[σ] and ψ ∈ L[τ ] we have that ϕ |= ψ implies that there exists an interpolant χ ∈ L[σ ∩ τ ] for this entailment, i.e., a sentence for which ϕ |= χ and χ |= ψ hold.

It is well-known that the full GF fails to have CIP. The known examples of sentences which demonstrate this can be used to make the following observation.

Proposition 1. The one-dimensional GF does not have CIP.

Proof. Consider the following sentences, which are simple variants of the formulas used in [13].

$$\varphi := \exists x \exists y \exists z (G(x, y, z) \land R(x, y) \land R(y, z) \land R(z, x))$$

$$\psi := \forall x \forall y (R(x, y) \to (A(x) \leftrightarrow \neg A(y)))$$

Notice that both of these sentence are one-dimensional. Now one can show, using essentially the same argument as the one used in Example 1 in [13], that there is no interpolant for the implication ϕ |= ¬ψ.

We remark that, in the context of fragments of FO, CIP is usually defined for formulas instead of sentences (as we have defined it). We could have also formulated it for formulas, but we decided to work with sentences for simplicity.

### 3 Bisimulation for UGF1

Given two models A and B, and tuples c ∈ An and d ∈ Bn we will use

$$(\mathfrak{A}, \mathfrak{c}) \equiv\_{\sigma} (\mathfrak{B}, \overline{d})$$

to denote the fact that for every ϕ(x1, . . . , xn) ∈ UGF1 we have that

$$
\mathfrak{A} \vdash \varphi(c\_1, \dots, c\_n) \iff \mathfrak{B} \vdash \varphi(d\_1, \dots, d\_n).
$$

The purpose of this section is to define a corresponding notion of bisimulation for UGF1 which captures the above equivalence relation. We will start by defining a suitable notion of partial isomorphism.

Definition 5. Let A and B be models, and let X := {a1, . . . , an} ⊆ A and Y ⊆ B. A bijection p : X → Y , is called a uniform partial σ-isomorphism between A and B, if

$$\operatorname{tp}\_{\mathfrak{A}}^{\sigma}[a\_1, \dots, a\_n] = \operatorname{tp}\_{\mathfrak{B}}^{\sigma}[p(a\_1), \dots, p(a\_n)].$$

Quantification in GF over a model A is restricted to live subsets of A, i.e., subsets of A which are either singletons or are contained in a single tuple a ∈ RA, for some R ∈ σ. In the case of UGF1 we will need the following modified version of the notion of live set, which takes into account the requirement that our formulas are uniform.

Definition 6. Let A be a model and let X ⊆ A.

We are now ready to define the notion of bisimulation for UGF1.

Definition 7. Let Z be a non-empty set of uniform partial σ-isomorphism between two structures A and B. Let c ∈ An and d ∈ Bn be tuples. We say that Z is a uniform guarded σ-bisimulation between (A, c) and (B, d), if for every p : X → Y ∈ Z the following conditions hold:

$$p(a) = q(a).$$

(back) For any b ∈ Y and a σ-live set Y 0 ⊆ B, with b ∈ Y 0 , there exists q : X0 → Y 0 ∈ Z so that

$$p^{-1}(b) = q^{-1}(b).$$

If there exists a guarded σ-bisimulation between (A, c) and (B, d), then we denote this by (A, a) ∼σ (B, b).

In what follows we will often refer to uniform guarded bisimulations simply as guarded bisimulations. The following two lemmas establish that our notion of bisimulation is correct, the first of which can proved in a standard manner by using induction.

Lemma 1. Let A and B be models, and let c ∈ An and d ∈ Bn be tuples so that (A, c) ∼σ (B, d). Then (A, c) ≡σ (B, d).

For the proof of the second lemma we need to recall the definition of ωsaturated model. A elementary n-type over a vocabulary σ is a consistent set of first-order formulas (not necessarily quantifier-free) with free variables in {x1, . . . , xn}. Given a σ-model A, we say that it is ω-saturated, if for every tuple a ∈ An of elements of A we have that each elementary n-type over the extended vocabulary σ ∪ {a1, . . . , an}, where each ai denotes a constant to be interpreted as the element ai , which is finitely consistent with the FO-theory of (A, a), is realized in (A, a). It is well-known that every σ-model, where σ is finite and relational, has an ω-saturated elementary extension [3].

Lemma 2. Let A and B be two ω-saturated models, and let c ∈ An and d ∈ Bn be tuples so that (A, c) ≡σ (B, d). Then (A, c) ∼σ (B, d).

Proof. Consider the following set

$$\mathcal{Z} := \{ p: \overline{a} \to \overline{b} \mid (\mathfrak{A}, \overline{a}) \equiv\_{\sigma} (\mathfrak{B}, \overline{b}) \}\dots$$

We claim that Z is a guarded σ-bisimulation between (A, c) and (B, d). We first note that by assumption c 7→ d ∈ Z, and hence Z satisfies (cover). Z also clearly consists of uniform partial σ-isomorphism between A and B. What remains to be proved is that Z also satisfies (forth) and (back). Since these two cases are analogous, we will concentrate on (forth).

Let p : a → b ∈ Z, a ∈ X and X0 := {c1, . . . , cm} ⊆ A be a σ-live set so that a ∈ X0 . For simplicity we will assume that a = c1. Consider now the following elementary m-type

$$\Sigma := \{ \varphi(p(a), x\_2, \dots, x\_m) \in \mathcal{U}\mathcal{G}\mathcal{F}\_1[\sigma \cup \{p(a)\}] \mid \mathfrak{A} \mid = \varphi(a, c\_2, \dots, c\_m) \}.$$

We claim that Σ is realized in (B, p(a)). Since B is ω-saturated, it suffices to show that each finite subset of Σ is realized in (B, p(a)). Let

$$
\psi\_1(p(a), x\_2, \dots, x\_m), \dots, \psi\_r(p(a), x\_2, \dots, x\_m) \in \Sigma.
$$

Since X0 is σ-live, there exists an atomic formula α(x1, . . . , xm) over σ with the property that

$$\mathfrak{A} \models \exists x\_2 \dots \exists x\_m (\alpha(a, x\_2, \dots, x\_m) \land \bigwedge\_{1 \le i \le r} \psi\_i(a, x\_2, \dots, x\_m)).$$

Note that Definition 6 guarantees that this is indeed a formula of UGF1[σ].  Now c 7→ d ∈ Z is the mapping we were after.

Remark 2. Using the two previous lemmas one prove in a standard manner that UGF1 is the maximal fragment of FO which is invariant under uniform guarded bisimulation, see for example [2].

### 4 Proof that UGF1 has CIP

In this section we will prove that UGF1 has CIP. We will start with the following lemma.

Lemma 3. Let σ and τ be signatures, and let ϕ ∈ UGF1[σ] and ψ ∈ UGF1[τ ]. Suppose that there is no χ ∈ UGF1[σ ∩ τ ] with the property that ϕ |= χ and χ |= ψ. Then there is a σ-model A and a τ -model B with the property that A |= ϕ, B 6|= ψ and A ≡σ∩τ B.

Proof. Essentially the same argument as the one used in the proof of Theorem 4.1 in [2] gives the result.

To give a high level overview of the rest of the proof, suppose that the assumption of Lemma 3 holds for sentences ϕ and ψ, which implies in particular that there are models A and B so that A ∼σ∩τ B. Now, what we want to prove is that ϕ ∧ ¬ψ is satisfiable. To do this, we will follow a standard approach in modal logic [2,11] by constructing an amalgam U which has the property that U ∼σ A and U ∼τ B. In particular, it will be a model of ϕ ∧ ¬ψ, since A |= ϕ and B |= ¬ψ.

Suppose now that A ∼σ∩τ B and let Z be a guarded (σ ∩ τ )-bisimulation which witnesses it. Given a pair (a, b) we will use (a, b) ∈ Z to denote the fact that there exists p ∈ Z with the property that a = dom(p) and p(a) = b. In other words the relation ai 7→ bi induces a uniform partial (σ ∩ τ )-isomorphism which belongs to Z.

Before describing the construction of U, we need to introduce some additional notation. Given two tuples a and b of the same length, we will let (a ⊗ b) denote the following tuple:

$$((a\_1, b\_1), \dots, (a\_n, b\_n))$$

Given (a ⊗ b), we say that it is left-good, if for every 1 ≤ i < j ≤ n we have that if ai = aj , then bi = bj . 2 Similarly we say that (a ⊗ b) is right-good, if for every 1 ≤ i < j ≤ n we have that if bi = bj , then ai = aj . Finally we say that (a ⊗ b) is good if it is left-good and right-good. Note that if (a ⊗ b) is of length n, k ≥ n and µ : [k] → [n] is a surjection, then we have that if (a ⊗ b) is left-good, then so is (a ⊗ b)µ. Analogous observation of course holds for right-good and good.

As the domain of the amalgam U we will take the set U = {(a, b) ∈ A × B | (a, b) ∈ Z}, while the interpretations of relation symbols will be defined as follows. First, for every R ∈ σ ∩ τ we define that

$$(\overline{a}\otimes\overline{b})\in R^{\mathfrak{A}}\text{ iff }\overline{a}\in R^{\mathfrak{A}}\text{ and }(\overline{a},\overline{b})\in \mathcal{Z}$$

Then, for every R ∈ (σ\τ ) we define that (a ⊗ b) ∈ RU iff a ∈ RA and one of the following conditions holds:

– (a, b) ∈ Z. – (a ⊗ b) is left-good and a is not (σ ∩ τ )-live.

Similarly, for every R ∈ (τ\σ) we define that (a ⊗ b) ∈ RU iff b ∈ RB and one of the following conditions holds:

– (a, b) ∈ Z. – (a ⊗ b) is right-good and b is not (σ ∩ τ )-live.

This concludes the construction of U. This construction is similar to the one given in [11] with the exception that we require tuples that are not (σ ∩ τ )-live to be either right-good or left-good.

2 In other words, if (a⊗b) is left-good, then the projection (a⊗b) 7→ a is an injection. We now define

$$\mathcal{Z}\_1 := \{ (\overline{a} \otimes \overline{b}) \mapsto \overline{a} \mid (\overline{a} \otimes \overline{b}) \text{ is } \sigma\text{-live in } \mathfrak{U}. \}$$

and

$$\mathcal{Z}\_2 := \{ (\overline{a} \otimes \overline{b}) \mapsto \overline{b} \mid (\overline{a} \otimes \overline{b}) \text{ is } \tau\text{-live in } \mathfrak{U}. \}$$

Note that if (a ⊗ b) is σ-live, then by construction it is also left-good (and an analogous observation obviously holds for τ -live tuples in U).

Lemma 4. Z1 consists of uniform partial σ-isomorphism between U and A, and Z2 consists of uniform partial τ -isomorphism between U and B.

Proof. We will only consider the case of Z1, since the case of Z2 is analogous. Let (a ⊗ b) 7→ a ∈ Z1, where the length of (a ⊗ b) is n. We will separately check that this mapping preserves 1-types and n-ary atomic formulas.

Let 1 ≤ i ≤ n and suppose that

$$((a\_i, b\_i), \dots, (a\_i, b\_i)) \in R^{\mathfrak{A}},$$

where R ∈ σ. By construction we know that (ai , . . . , ai) ∈ RU. Suppose then that

$$(a\_i, \ldots, a\_i) \in R^{\mathfrak{A}}.$$

Since by definition of U we have that (ai , bi) ∈ Z, we can conclude that

$$((a\_i, b\_i), \dots, (a\_i, b\_i)) \in R^{\mathfrak{U}}.$$

Thus (ai , bi) and ai have the same 1-types over σ.

We will then verify that the mapping preserves n-ary atomic formulas. Let R ∈ σ be a k-ary relation, where k ≥ n, and let µ : [k] → [n] be a surjection. We need to show that (a ⊗ b)µ ∈ RU iff aµ ∈ RA. Again, the left to right direction follows immediately from the definition of U, so we will concentrate on the direction from right to left. First we note that if a is not (σ ∩ τ )-live, then we are done, since then also aµ is not (σ ∩ τ )-live.

Thus we can assume that a is (σ ∩ τ )-live. Now, due to the definition of Z1, we know that (a⊗b) is σ-live in U. Hence, by definition of U, and the fact that a is (σ ∩ τ )-live, we know that (a, b) ∈ Z, which is the same as (aµ, bµ) ∈ Z. Now we can deduce, due to the definition of U, that (a ⊗ b)µ ∈ RU. This, together with the fact that (a ⊗ b) 7→ a preserves 1-types over σ, allows us to conclude that tpσ U [a ⊗ b] = tpσ A[a].

Lemma 5.  Again, we will only consider the case of Z1, since the case of Z2 is analogous. Due to Lemma 4 we just need to verify (back) and (forth) conditions. Let (a ⊗ b) 7→ a ∈ Z1, where the length of a and b is n.

that (ai , bi) ∈ Z. Since Z is a guarded (σ ∩τ )-bisimulation, there exists a set {d1, . . . , dm} ⊆ B so that (c, d) ∈ Z and (ai , bi) ∈ (c ⊗ d). In particular (c ⊗ d) is σ-live in U, and hence (c ⊗ d) 7→ d ∈ Z1, which is the mapping we were after.

### Theorem 1. UGF1 has Craig interpolation property.

Proof. Let ϕ ∈ UGF1[σ] and ψ ∈ UGF1[τ ] be sentences so that ϕ |= ψ, but there is no interpolant for this entailment. By lemma 3 there exists a σ-model A and a τ -model B such that A |= ϕ, B 6|= ψ and A ≡σ∩τ B. Take ω-saturated elementary extensions Aˆ and Bˆ of A and B. Since Aˆ ≡σ∩τ Bˆ , by lemma 2 we have that Aˆ ∼σ∩τ Bˆ . Using the construction presented in this section there exists a (σ∪τ )-model U with the property that U ∼σ Aˆ and U ∼τ Bˆ . Thus U |= ϕ∧¬ψ, i.e. ϕ∧¬ψ is consistent, which is a contradiction with the assumption that ϕ |= ψ.

### 5 Complexity of uniform GF

In this section we will prove that the complexity of the satisfiability problem of uniform GF is in NExpTime. Since it was proved in [15] that the complexity of the satisfiability problem of UGF1 is NExpTime-hard, this upper bound is sharp.

#### 5.1 Scott normal form

As usual, we will start by arguing that we can restrict our attention to sentences which are in a certain normal form. The normal form that we will use here has a somewhat awkward form, but the proof of Lemma 6 should clarify why we chose to use it.

Definition 8. Let ϕ be a sentence of UGF. We say that ϕ is in normal form, if it has the following shape

$$\bigwedge\_{t \in T} \exists z \lambda\_t(z) \land \bigwedge\_{i \in I} \forall \overline{x}(\alpha\_i(\overline{x}) \to \exists \overline{y}(\beta\_i(\overline{x}, \overline{y}) \land \psi\_i(\overline{x}, \overline{y})))$$

$$\bigwedge\_{j \in J} \forall \overline{x}(\kappa\_j(\overline{x}) \to (\theta\_j(\overline{x}) \to \forall \overline{y}(\gamma\_j(\overline{x}, \overline{y}) \to \psi\_j(\overline{x}, \overline{y})))),$$

where T, I, J are non-empty (finite) sets, λt, αi, βi, κj and γj are atomic formulas and ψi, θj and ψj are quantifier-free formulas.

Remark 3. In the definition of the normal form we do not require that the tuples y are necessarily non-empty, i.e., we allow formulas of the form ∀x(αi(x) → ψi(x)) in our normal forms. However, we do require that the tuples x are nonempty, and hence we do not allow formulas of the form ∃y(βi(y) ∧ ψi(y)), where the length of y is more than one.

If ϕ is a sentence of UGF in normal form, then we refer to its conjuncts of the form

$$\forall \overline{x} (\alpha\_i(\overline{x}) \to \exists \overline{y} (\beta\_i(\overline{x}, \overline{y}) \land \psi\_i(\overline{x}, \overline{y})))$$

as the existential requirements and we will use ϕ ∃ i to denote them. Given a model A, an existential requirement ϕ ∃ i and a ∈ α A i we say that a tuple c is a witness for ϕ ∃ i and a if

$$\mathfrak{A} \mid = \beta\_i(\overline{a}, \overline{c}) \wedge \psi\_i(\overline{a}, \overline{c}) .$$

Conjuncts of the form

$$\forall \overline{x} (\kappa\_j(\overline{x}) \to (\theta\_j(\overline{x}) \to \forall \overline{y} (\gamma\_j(\overline{x}, \overline{y}) \to \psi\_j(\overline{x}, \overline{y}))))$$

will be referred to as the universal requirements and we will use ϕ ∀ j to denote them.

Using standard renaming techniques one can establish the following.

Lemma 6. There is a polynomial nondeterministic procedure, taking as its input a sentence ϕ ∈ UGF[σ] and producing a sentence ϕ 0 ∈ UGF[σ 0 ] in normal form, where σ 0 ⊃ σ, such that

Proof. We will essentially follow the proof of lemma 1 in [15], with some small technical modifications. Let ϕ ∈ UGF[σ] be a sentence, which w.l.o.g contains only existential quantification. Let ψ be the innermost formula of ϕ which starts with a block of existential quantifiers. If ψ is a sentence, we will nondeterministically either replace it with ⊥ or > and add ψ or ¬ψ (depending on our guess) as a conjunct to the resulting formula. Suppose then that ψ is a formula of the form

$$
\exists \overline{y} (\alpha(\overline{x}, \overline{y}) \land \psi(\overline{x}, \overline{y})) .
$$

Since ϕ was a sentence, ψ occurs in a scope of another formula of the form

$$
\exists \overline{z} (\alpha'(\overline{x}) \land \psi'(\overline{x})),
$$

where z ⊆ x. Let α 0 be the guard of the innermost such formula. We will now replace ϕ with the following formula

$$
\varphi[\psi(\overline{x})/R(\overline{x})] \land \forall \overline{x} (R(\overline{x}) \to \exists \overline{y} (\alpha(\overline{x}, \overline{y}) \land \psi(\overline{x}, \overline{y})))
$$

$$
\land \forall \overline{x} (\alpha'(\overline{x}) \to (\neg R(\overline{x}) \to \forall \overline{y} (\alpha(\overline{x}, \overline{y}) \to \neg \psi(\overline{x}, \overline{y})))),
$$

where ϕ[ψ(x)/R(x)] is the sentence obtained from ϕ by replacing the previously mentioned subformula ψ(x) with the atomic formula R(x) which has a fresh relation symbol R. It is straightforward to verify that the resulting sentence is equi-satisfiable with ϕ.

Now one can repeat the above procedure until one is left with a sentence of the form

$$\bigwedge\_{t \in T} \exists \overline{x} (\alpha\_t(\overline{x}) \land \psi\_t(\overline{x})) \land \bigwedge\_{i \in I} \varphi\_i^{\exists} \land \bigwedge\_{j \in J} \varphi\_j^{\forall},$$

where each ϕ ∃ i is an existential requirement, while each sentence ϕ ∀ j is an universal requirement. Now one can replace each conjunct ∃x1 . . . ∃xn(α(x1, . . . , xn) ∧ ψt(x1 . . . xn)) with a sentence of the form

$$
\exists x \lambda\_t(x) \land \forall x\_1 (\lambda\_t(x\_1) \to \exists x\_2 \dots \exists x\_n (\alpha\_t(x\_1, \dots, x\_n) \land \psi\_t(x\_1, \dots, x\_n))),
$$

where λt is a fresh unary relation symbol. The resulting sentence is clearly equisatisfiable with the original sentence and furthermore it is in normal form.

### 5.2 Satisfiability Witnesses

A standard technique in proving that the complexity of the satisfiability problem of a given fragment of FO is in NExpTime is to show that each satisfiable sentence of this fragment has a finite model of size at most exponential with respect to the length of the sentence [8,12,15,16]. However, in the case of UGF it seems to be easier to show that we can associate to each of its sentences ϕ a different type of certificate, which is still at most exponential with respect to the length of the sentence, and which can be used to construct a (potentially infinite) model for ϕ.

Definition 9. Let ϕ ∈ UGF[σ] be a sentence in normal form, P be a set of 1-types over σ and π ∈ P. A pair (A, c), where c ∈ A, is called a (P, π)-witness for ϕ, if it satisfies the following requirements.

$$
\mathfrak{A} \vdash \gamma\_j(\overline{a}, \overline{b}) \to \psi\_j(\overline{a}, \overline{b}) .
$$

Here the intuition is that a (P, π)-witness (A, c) is a local certificate; it certifies that we can provide witnesses for tuples which contain the element c. The main idea now is that if we have a (P, π)-witness for each π ∈ P, then we can use them to construct a proper model for ϕ.

Definition 10. Let ϕ ∈ UGF[σ] be a sentence in normal form. A set of 1-types P over σ is a witness for ϕ, if it satisfies the following two requirements.

The following lemmas prove that an existence of a witness for ϕ is equivalent with the satisfiability of ϕ.

Lemma 7. Let ϕ ∈ UGF be a sentence in normal form. If ϕ is satisfiable, then there exists a witness for it.

Proof. Suppose that A |= ϕ. As the set of 1-types P we can take the set

$$\{\text{tp}\_{\mathfrak{A}}[a] \mid a \in A\}.$$

Clearly for every conjunct ∃zλt(z) there exists a suitable 1-type in P. Towards verifying the second requirement let π ∈ P and let c ∈ A be an element which realizes π. Then (A, c) is clearly a (P, π)-witness for ϕ.

Lemma 8. Let ϕ ∈ UGF be a sentence in normal form. If there exists a witness for ϕ, then it is satisfiable.

Proof. For simplicity we will assume that ϕ contains exactly one conjunct of the form ∃zλt(z). Let P be a witness for ϕ. Thus for every π ∈ P there exists a pair (A π , c) which is a (P, π)-witness for ϕ. Our goal is to use these witnesses to construct a sequence of models

$$
\mathfrak{A}\_1 \le \mathfrak{A}\_2 \le \mathfrak{A}\_3 \le \dots
$$

so that their union is a model of ϕ.

Let π ∈ P be a 1-type so that π |= λt. As the model A1 we will take the model which contains a single element with 1-type π. Suppose then that we have defined An in such a way that each 1-type realized in An belongs to P. To define the model An+1 we will proceed as follows. Given a ∈ An, we will use Wa to denote the set Aπ − {c}, where Aπ refers to the domain of the model in the (P, π)-witness (A π , c) of π := tpAn [a]. Without loss of generality we will assume that the sets Wa are pairwise disjoint. Now we will define An+1 as follows.

– The domain of the model is

$$A\_n \cup \bigcup\_{a \in A\_n} W\_a^\*$$

– An+1 An is defined to be isomorphic with An.

– For each a ∈ An and for each {c1, . . . , cm} ⊆ Wa, we define that

$$\operatorname{tp}\_{\mathfrak{A}\_{n+1}}[a, c\_1, \dots, c\_m] := \operatorname{tp}\_{\mathfrak{A}^\pi}[c, c\_1, \dots, c\_m],$$

where π is the 1-type of a.

– For every tuple (a1, . . . , am) and a m-ary relation R for which we have not yet defined whether (a1, . . . , am) belongs to RAn+1 , we will simply define that it does not belong to it.

The last step guarantees that if a tuple, which contains more than one element, is live in An+1, then it was already alive in one of the models A π . It is straightforward to verify that the union of the models (An)n<ω is indeed a model of ϕ.

### 5.3 Complexity of UGF

Although the size of a witness for ϕ is clearly only exponential with respect to |ϕ|, we do not yet have any upper bounds on the time it takes to verify that it really is a witness for ϕ. The following lemma gives us such a bound.

Lemma 9. Let ϕ ∈ UGF be a sentence in normal form and let σ denote the vocabulary of ϕ. Let P be a set of 1-types over σ and π ∈ P. If there exists a (P, π)-witness for ϕ, then there exists one in which the size of the model is at most 2 |ϕ| O(1) .

Proof. Let (A, c) be a (P, π)-witness for ϕ and let m = max{ar(R) | R ∈ σ}. Note that m ≤ |ϕ|. Our goal is to construct a sequence

$$
\mathfrak{B}\_1 \le \cdots \le \mathfrak{B}\_m
$$

of models so that (Bm, c) is a (P, π)-witness for ϕ and |Bm| ≤ 2 |ϕ| O(1) . As the model B1 we will take the model which contains a single element with 1-type π; let e denote this element.

Before moving forward, we will introduce one auxiliary definition.  Let {c1, . . . , cm} denote the set of distinct elements in a. We say that a and b are similar, if the mapping p : a → b, which was the mapping induced by the relation ai 7→ bi , is a bijection and furthermore

$$\text{tp}\_{\mathfrak{A}}[c\_1, \dots, c\_n] = \text{tp}\_{\mathfrak{B}}[p(c\_1), \dots, p(c\_n)].$$

Suppose now that we have defined Bk, where k < m, and in such a way that for each σ-live tuple b for which tpBk [b] has been defined, there exists a similar tuple a which consists of elements of A. Given an existential requirement ϕ ∃ i of ϕ and a tuple b ∈ α Bk i , which contains the element e, we say that b is a i-defect if there exists no witness for ϕ ∃ i and b in the model Bk. By construction, for each i-defect b we can find a tuple a of elements of A so that b and a are similar. In particular a ∈ α A i , and hence there exists a witness c for ϕ ∃ i and a in A; let Wb,i

denote the set of elements in c which were not contained in a. Without loss of generality we will assume that the sets Wb,i are pairwise disjoint. Now we will define Bk+1 as follows.

– The domain of the model is

$$B\_k \cup \bigcup\_{i \in I} \bigcup\_{\mathfrak{F}\_{\text{an } i \text{-defect}}} W\_{\mathfrak{F}\_{\mathfrak{F}\_i}}$$

$$\text{tp}\_{\mathfrak{B}\_{k+1}}[d\_1, \dots, d\_r, c\_1, \dots, c\_n] = \text{tp}\_{\mathfrak{A}}[p(d\_1), \dots, p(d\_r), c\_1, \dots, c\_n],$$

where (d1, . . . , dr) enumerates all the elements occurring in b and p : b → a. – For every tuple (b1, . . . , bn) and a n-ary relation R for which we have not yet defined whether (b1, . . . , bn) belongs to RBk+1 , we will simply define that it does not belong to it.

This completes the construction of the models B1, . . . , Bm. To bound the size of Bm, we first note that |Bk+1| ≤ |Bk| + |ϕ||Dk|, where Dk denotes the number of defects in Bk. By construction, for every defect (d1, . . . , dr) of Bk the set {d1, . . . , dr} is a σ-live set which is not contained in B`, for any ` < k. If k = 1, then the number of such σ-live sets is one, and if k > 1, then the number of such σ-live sets is Dk−1. Since each σ-live set is of size at most |ϕ|, there are at most |ϕ||ϕ| |ϕ|Dk−1 = 2|ϕ| O(1)Dk−1 defects in Bk, i.e., Dk ≤ 2 |ϕ| O(1)Dk−1. Since m ≤ |ϕ|, we have that Dk ≤ 2 |ϕ| O(1) , for any k < m, and hence |Bm| ≤ 2 |ϕ| O(1) .

Thus what remains to be proven is that (Bm, e) is a (P, π)-witness for ϕ. Here the only non-trivial requirement that we need to verify is that Bm satisfies the second item in definition 9. So, let ϕ ∃ i be an existential requirement and let b = (b1, . . . , bn) ∈ α Bm i be a tuple which contains e. We can clearly assume that n < m. It suffices to show that b is contained in Bk, for some k < m, since then by construction we know that it has a witness in Bm.

Aiming for a contradiction, suppose that b is contained in Bm, but it is not contained in Bk for any k < m. By construction we know that, since b is σ-live, we assigned a table to some tuple (b 0 1 , . . . , b0 r ), where (b 0 1 , . . . , b0 r ) enumerates the set of distinct elements of (b1, . . . , bn). Again, by construction we know that we assigned a table to the tuple (b 0 1 , . . . , b0 r ), because we wanted to provide a witness for some tuple (d1, . . . , ds), which contains e and for which {d1, . . . , ds} is a strict subset of {b 0 1 , . . . , b0 r}. 3

Now observe that (d1, . . . , ds) is a σ-live tuple containing e, which is contained in Bm−1 but is not contained in Bk for any k < m−1. Indeed, if it were contained in Bk, for some k < m−1, then by construction we would have provided a witness for it in the model Bk+1, i.e., (b1, . . . , bn) would have been contained in Bk+1. But now we are in a position which is the same as the one that we started in; in

3 If it were not, there would have been no need to provide a witness for it.

particular, we can repeat the above argument. After repeating the argument (at least) (n − 1)-times we would end up with the conclusion that e is contained in some Bk, where k > 1, but it is not contained in B1, which would be an obvious contradiction.

Now we can prove the main theorem of this section.

Theorem 2. The satisfiability problem of UGF is NExpTime-complete.

Proof. The lower bound follows from the proof of Theorem 3 in [15]. We will give an informal description of a non-deterministic procedure running in exponential time which determines whether a given sentence ϕ ∈ UGF is satisfiable. It starts by converting ϕ into an equi-satisfiable sentence ϕ 0 ∈ UGF in normal form, after which it guesses a set of 1-types P over the vocabulary of ϕ 0 and for each π ∈ P a (P, π)-witness (A, c) for ϕ, where the size of A is at most 2|ϕ| O(1) . Lemmas 6, 7, 8 and 9 guarantee that this procedure is correct. Since |P| ≤ 2 |ϕ| , the algorithm runs in exponential time with respect to |ϕ|.

### 6 Conclusions

In this paper we have proved two results of quite distinct flavour on uniform guarded fragments. The first result was that although GF fails to have Craig interpolation, its one-dimensional uniform fragment does have it. The second result was that the complexity of the satisfiability problem of the uniform guarded fragment is NExpTime-complete. The results presented in this paper suggest several new research questions, but here we will mention just two of them.

The first question is whether or not the uniform GF has Craig interpolation property. While the correctness of the amalgam construction presented in Section 4 rests on the assumption of one-dimensionality, we have not been able to show that uniform GF would not have Craig interpolation property. This has led the author to conjecture that the uniform GF does in fact have Craig interpolation property.

The second question is whether or not uniform GF has the exponential model property (note that if uniform GF would have an exponential model property, then one would obtain Theorem 2 for free). As we saw in the proof of Lemma 9, the requirement of uniformity essentially prevents uniform GF from enforcing long paths, and this seems to suggest that uniform GF can only enforce exponentially long paths (which it can enforce, since it contains standard modal logic with the global diamond). Because of this, the author conjectures that uniform GF has the exponential model property.

### Acknowledgements

The author wishes to thank Bartosz Bednarczyk for several helpful discussions on interpolation and fragments of first-order logic, and for suggesting the problem of determining the complexity of the satisfiability problem of uniform guarded fragment. The author also wishes to thank Antti Kuusisto for pointing out rather silly mistakes in the original definitions of uniformity and the uniform guarded bisimulation. Finally, the author wishes to thank the anonymous reviewers for their useful remarks which improved the presentation of this paper.

### References

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.

### Sweedler Theory of Monads

Dylan McDermott1 () , Exequiel Rivas2 , and Tarmo Uustalu1,2

1 Dept. of Computer Science, Reykjavik University, Reykjavik, Iceland 2 Dept. of Software Science, Tallinn University of Technology, Tallinn, Estonia<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
Abstract. Monad-comonad interaction laws are a mathematical concept for describing communication protocols between efectful computations and coefectful environments in the paradigm where notions of efectful computation are modelled by monads and notions of coefectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the fnal interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monadcomonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.

Keywords: (co)monads · (co)algebras · interaction laws · runners · duoidal categories · Sweedler operations

### 1 Introduction

The monad-comonad interaction laws of Katsumata et al. [16] are a mathematical concept for formalizing ways in which efectful programs (e.g., programs reading from and writing to a store, programs making nondeterministic choices) can be run. The idea is that efectful programs issue requests to the outside world; they can thus run on machines that can service such requests. Programs denote computations, machines implement environments. Notions of computation are modelled by monads in the manner frst explained by Moggi [23], while notions of environment can be modelled by comonads. Interaction laws model protocols of cooperation between computations and environments. Ideally, interaction should result in a return value and a fnal state. But it may be that some efects cannot be serviced, in which case interaction yields a residual computation of a return value and a fnal state; another monad is then needed to model the suitable notion of residual computation. A monad-comonad interaction law is therefore given by a monad T, a comonad D and a monad R on a symmetric monoidal category with a family of maps T X ⊗ DY → R(X ⊗ Y ) natural in X and Y and agreeing with the (co)units and (co)multiplications. If R = Id, we have a non-residual interaction law.

It is natural to ask for useful methods for recognizing and constructing monad-comonad interaction laws. Specifcally, it would be useful to fnd: a fnal monad for a given interacting comonad and residual monad; a fnal interacting comonad for a given monad and residual monad; or an initial residual monad for a given monad and interacting comonad.

In this paper, we show how to fnd these universal (co)monads, elaborating on some ideas and results from prior work on interaction [16,33]. We emphasize that the most important structural foundation for interaction laws is the duoidal [10,2] interrelationship of the composition and Day convolution monoidal structures in endofunctor categories. It is so signifcant that some central statements about interaction laws can be made on the level of monoids and comonoids in general symmetric closed duoidal categories, completely suppressing any specifcs about monads and comonads. In fact, it turns out that monad-comonad interaction laws are an instance of measuring maps from the Sweedler theory for duoidal categories as developed by L´opez Franco and Vasilakopoulou [20]. The universal (co)monads are instances of the operations studied in this theory. In particular, the fnal interacting comonad is an instance of the Sweedler hom and the initial residual monad is an instance of the Sweedler copower.

To obtain results about monad-comonad interaction specifcally, we combine this general perspective with the characterization of monad-comonad interaction laws by Uustalu and Voorneveld [33] as functors between the categories of (co)algebras of the (co)monads involved. This allows us to describe the Sweedler hom and the Sweedler power via their categories of (co)algebras in terms of what we call stateful and continuation-based runners.

We also discuss an enriched version of monad-comonad interaction laws, of which strong monad-comonad interaction laws are a special case. In this case, both kinds of runners of an enriched monad on a self-enriched category can be viewed as its algebras in another enriched category.

The paper is organized as follows. First, in Sect. 2, we review the basics of monad-comonad interaction laws. In Sect. 3, we show that monad-comonad interaction laws, the universal interacting comonad and the universal residual monad are an instance of measuring maps, the Sweedler hom and the Sweedler copower in symmetric closed duoidal categories. We then review the (co)algebraic perspective on monad-comonad interaction laws in Sect. 4, and apply it to derive (co)algebraic characterizations of the Sweedler hom and the Sweedler copower in Sect. 5. In Sect. 6, we comment on enriched monad-comonad interaction laws. We review some background category theory literature and related semantics work in Sect. 7. New material is primarily in Sects. 5, 6; some statements in Sect. 4 are also new.

We assume from the reader familiarity with the use of (strong) monads in mathematical semantics to model notions of efectful computation, and familiarity with the basics of the categorical machinery we need (monads and comonads, symmetric monoidal closed categories, accessibility [21,1], enrichment [17]).

### 2 Monad-Comonad Interaction Laws

We begin by reviewing the basics of monad-comonad interaction laws [16].

Consider a symmetric monoidal closed category (C, I, ⊗,⊸), e.g., a Cartesian monoidal closed category, e.g., Set.

A (residual) functor-functor interaction law is given by endofunctors F, G, H on C together with a family of maps

$$
\phi\_{X,Y}: FX \otimes GY \to H(X \otimes Y),
$$

natural in X, Y . We speak of a non-residual interaction law when H = Id. A map between (residual) functor-functor interaction laws (F, G, H, ϕ) and (F ′ , G′ , H′ , ϕ′ ) is given by natural transformations f : F → F ′ , g : G′ → G and h : H → H′ satisfying the equation

$$F\_{FX\otimes G'Y} \xrightarrow{FX\otimes g\_{Y}} \sum\_{f\_X\otimes G'Y}^{\psi\_{X,Y}} H(X\otimes Y)$$

$$\sum\_{f\_X\otimes G'Y} \overbrace{F'X\otimes G'Y}^{\psi'\_{X,Y}} \xrightarrow{\psi'\_{X,Y}} H'(X\otimes Y)$$

Functor-functor interaction laws form a category that has a monoidal structure based on endofunctor composition.

 When R = Id, we speak of a non-residual interaction law. A map between (residual) monad-comonad interaction laws (T, D, R, ψ) and (T ′ , D′ , R′ , ψ′ ) is given by a monad map T → T ′ , a comonad map D′ → D and a monad map R → R′ that make a map between the underlying functor-functor interaction laws. Monadcomonad interaction laws form a category isomorphic to the category of monoid objects in the category of functor-functor interaction laws.

Example 1. Let C = Set (or any SMCC). Take T X = S ⇒ (S × X) (the state monad) and DX = S0 × (S0 ⇒ X) (the costate monad). There is a non-residual monad-comonad interaction law of T, D when S = S0 and more generally when S, S0 come with a lens structure get : S0 → S, put : S0 × S → S0; in fact, these laws are in bijection with lenses.

Let C = Set (or any extensive category that also has the relevant initial algebras and fnal coalgebras). Take F X = 1 + X2 and T the free monad on F, so T X ∼= µX′ .X + 1 + X′2 (leaf-labelled nullary-binary trees). The only comonad D that can interact with T non-residually is DY ∼= 0. If we take RZ = 1 + Z, we have an R-residual interaction law of T and D for example for DY ∼= νY ′ .Y × (2 × Y ′ ) (node-labelled bitstreams), i.e., the cofree comonad for GY = 2 × Y .

See [16,33] for further examples and their intuitive meaning for semantics.

Some equivalent formulations of interaction laws will be useful. Due to the bijections

$$\begin{array}{c} FX \otimes GY \to H(X \otimes Y) \text{ nat. in } X, Y\\ \hline \overline{\mathbb{C}(X \otimes Y, Z) \to \mathbb{C}(FX \otimes GY, HZ) \text{ nat. in } X, Y, Z} \\\ \overline{\mathbb{C}(X, Y \multimap Z) \to \mathbb{C}(FX, GY \multimap HZ) \text{ nat. in } X, Y, Z} \\\hline \overline{F(Y \multimap Z) \to GY \multimap HZ \text{ nat. in } Y, Z} \end{array}$$

an H-residual functor-functor interaction law of F, G is the same as a family of maps

$$
\phi\_{Y,Z} : F(Y \multimap Z) \to GY \multimap HZ
$$

natural in Y , Z. Under this view, the equation required of a functor-functor interaction law map (f, g, h) between (F, G, H, ϕ) and (F ′ , G′ , H′ , ϕ′ ) becomes

$$F(Y \to Z) \xrightarrow{\phi\_{Y,Z}} GY \to HZ$$

$$\begin{array}{c|c} \downarrow & & \\ F'(Y \to Z) \xrightarrow{\phi'\_{Y,Z}} G'Y \to H'Z \end{array}$$

An R-residual monad-comonad interaction law of T, D is the same as a family of maps

$$
\psi\_{Y,Z} : T(Y \multimap Z) \to DY \multimap RZ
$$

natural in Y , Z satisfying

Y ⊸ Z ηY ⊸Z Y ⊸ Z εY ⊸ηR Z T(Y ⊸ Z) ψY,Z/DY ⊸ RZ T T(Y ⊸ Z) µY ⊸Z T ψY,Z/T(DY ⊸ RZ) ψDY,RZ/DDY ⊸ RRZ δY ⊸µR Z T(Y ⊸ Z) ψY,Z /DY ⊸ RZ

Suppose F, G, H : C → C are such that the coends and ends

$$\begin{array}{ll} (F \star G) \, Z = \int^{X,Y} \mathbb{C}(X \otimes Y, Z) \bullet (FX \otimes GY) & = \int^{Y} F(Y \multimap Z) \otimes GY\\ (G \multimap H) \, X = \int\_{Y,Z} \mathbb{C}(X, Y \multimap Z) \, \bigwedge (GY \multimap HZ) = \int\_{Y} GY \multimap H(X \otimes Y) \end{array}$$

exist. (F ⋆ G is called the Day convolution.) Then, because of the bijections

$$\begin{array}{l} \frac{\int^{X,Y} \mathbb{C}(X \otimes Y, Z) \bullet (FX \otimes GY) \to HZ \text{ nat. in } Z}{\mathbb{C}(X \otimes Y, Z) \to \mathbb{C}(FX \otimes GY, HZ) \text{ nat. in } X, Y, Z} \\ \hline \frac{\mathbb{C}(X, Y \multimap Z) \to \mathbb{C}(FX, GY \multimap HZ) \text{ nat. in } X, Y, Z}{\mathbb{C}X \multimap \int\_{Y,Z} \mathbb{C}(X, Y \multimap Z) \oplus (GY \multimap HZ) \text{ nat. in } X} \end{array}$$

an H-residual functor-functor interaction law of F, G turns out to be the same as a natural transformation F ⋆ G → H or F → G −⋆ H. An R-residual monad-comonad interaction law of T, D is the same as a natural transformation UT ⋆ UD → UR satisfying certain equations and also—by way of a particularly concise characterization—the same as a monad map T → D −⋆ R where D −⋆ R is a certain canonical monad with UD −⋆ UR as the underlying functor.

Now, if C is locally presentable and F, G, H are accessible, then F ⋆ G and G−⋆H are guaranteed to exist and be accessible. Writing [C, C]a for the category of accessible endofunctors on C, we obtain functors ⋆ : [C, C]a×[C, C]a → [C, C]a and −⋆ : [C, C] op a ×[C, C]a → [C, C]a. Together with J ∈ [C, C]a defned by JZ = C(I, Z) • I, the functor ⋆ equips [C, C]a with a symmetric monoidal structure. We also get that − ⋆ G ⊢ G −⋆ −, i.e., this structure is closed.3 The functor −⋆ : [C, C] op a × [C, C]a → [C, C]a is lax monoidal wrt. the composition monoidal structure on [C, C]a. That UD −⋆ UR carries a monad structure if D is an accessible comonad and R is an accessible monad is a consequence of this.

These observations suggest the possibility of abstraction by switching to a more general setting. Instead of considering [C, C]a, we can consider an arbitrary category D equipped with a monoidal structure and a symmetric monoidal structure that suitably agree. The appropriate notion of agreement is duoidality [10,2]. We will next consider this abstraction and see that monad-comonad interaction laws are the measuring maps of an instance of L´opez Franco and Vasilakopoulou's Sweedler theory for duoidal categories [20].

### 3 Sweedler Theory for Duoidal Categories

We review the Sweedler theory for duoidal categories [20] and show that monads provide an instance.

Assume a symmetric duoidal category (D, I, ⋄, J, ⋆), i.e., a symmetric monoidal category in MonCAToplax, that is also closed in the sense that − ⋆ G has a right adjoint G −⋆ − in CAT. Explicitly, this means that we have a category D equipped with a monoidal structure (I, ⋄), a symmetric monoidal closed structure (J, ⋆, −⋆) and structural laws

$$\begin{array}{ccc} J \to I & & J \to J \diamond J \\ I \star I \to I & & (F \diamond G) \star (H \diamond K) \to (F \star H) \diamond (G \star K) \end{array}$$

satisfying appropriate equations witnessing oplax monoidality of J : 1 → D and ⋆ : D × D → D as functors between monoidal categories for the (I, ⋄) monoidal structure on D.

3 If C is locally κ-presentable with the κ-presentable objects closed under I and ⊗, then the κ-accessible endofunctors on C form a monoidal category with ⋆ as tensor. Garner and L´opez Franco [13, Sect. 8.1] show that this monoidal category is closed, but their closed structure is diferent from ours. Our G −⋆ H has the property that natural transformations F → G−⋆H are H-residual functor-functor interaction laws of F, G even if F is not accessible; this is not the case for Garner and L´opez Franco's. This is why we do not restrict to fxed κ, and instead use all of [C, C]a.

The internal hom object F −⋆ I is called the dual of F. Stretching this terminology, the object F −⋆ H can be called the dual of F wrt. H.

We write Mon(D) (respectively Comon(D)) for the categories of monoids (resp. comonoids) in D wrt. the (I, ⋄) monoidal structure.

The composition monoidal and Day convolution symmetric monoidal closed structures (Id, ·) and (J, ⋆, −⋆) on [C, C]a yield an example of such a symmetric duoidal category D. The categories Mon([C, C]a) and Comon([C, C]a) are those of accessible monads and comonads.

The object J has a comonoid structure J → I, J → J ⋄ J, and the functor −⋆ : D op × D → D is lax monoidal wrt. the (I, ⋄) monoidal structure. The operations

$$\begin{array}{c} \star: \mathbb{D} \times \mathbb{D} \to \mathbb{D} \\ \rightsquigarrow: \mathbb{D}^{\textup{op}} \times \mathbb{D} \to \mathbb{D} \end{array}$$

lift to

$$\begin{array}{ll} \star : \mathbf{Comon}(\mathbb{D}) \times \mathbf{Comon}(\mathbb{D}) \to \mathbf{Comon}(\mathbb{D}) & \text{tensor of commands} \\ \rightarrow : (\mathbf{Comon}(\mathbb{D}))^{\mathrm{op}} \times \mathbf{Mon}(\mathbb{D}) \to \mathbf{Mon}(\mathbb{D}) & \text{power of a monoid} \end{array}$$

in the sense that

via

$$\varepsilon = \begin{array}{c} D\_0 \star D\_1 \xrightarrow{\varepsilon\_0 \star \varepsilon\_1} I \star I \xrightarrow{\begin{array}{c} \varepsilon\_0 \star \varepsilon\_1 \end{array}} I \end{array}$$

$$\delta = \begin{array}{c} D\_0 \star D\_1 \xrightarrow{\delta\_0 \star \delta\_1} (D\_0 \diamond D\_0) \star (D\_1 \diamond D\_1) \xrightarrow{\begin{array}{c} \varepsilon\_0 \star \varepsilon\_1 \end{array}} (D\_0 \star D\_1) \diamond (D\_0 \star D\_1) \end{array}$$

$$\eta = \begin{array}{c} I \xrightarrow{\begin{array}{c} \varepsilon \end{array}} I \to I \xrightarrow{\begin{array}{c} \varepsilon \star \eta \xrightarrow{R}} D \to \end{array}} D \to R$$

$$\mu = \begin{array}{c} (D \to R) \diamond (D \to R) \xrightarrow{\begin{array}{c} \varepsilon \end{array} \text{---} \begin{array}{c} (D \diamond D) \xrightarrow{\begin{array}{c} \delta \end{array} \star \mu \xrightarrow{R}} D \to \star R \end{array}}$$

Comonoid maps D0 ⋆ D1 → D are the same as maps ψ : UD0 ⋆ UD1 → UD satisfying

$$\begin{array}{c} D\_0 \star D\_1 \xrightarrow{\psi} \begin{array}{c} D \\ \downarrow \\ \downarrow \\ \end{array} \end{array} \xrightarrow{D} D\_0 \star D\_1 \xrightarrow{D\_0 \star D\_1} \xrightarrow{\psi} \begin{array}{c} \downarrow \\ \downarrow \\ \end{array} \xrightarrow{D} D$$

(omitting the Us in the equations). Such maps ψ could be called D-residual comonoid-comonoid interaction laws of D0, D1.

Monoid maps T → D −⋆ R are in bijection with maps ψ : UT ⋆ UD → UR that satisfy

(again omitting the Us in the equations), which are known as measuring maps from T to R by D and which we can also call R-residual monoid-comonoid interaction laws of T, R.

The three Sweedler operations

$$\begin{array}{ccc} \mathcal{L}: (\mathbf{Comon}(\mathbb{D}))^{\mathrm{op}} \times \mathbf{Comon}(\mathbb{D}) \to \mathbf{Comon}(\mathbb{D}) & \text{internal hom of commands} \\ \rhd: \mathbf{Comon}(\mathbb{D}) \times \mathbf{Mon}(\mathbb{D}) \to \mathbf{Mon}(\mathbb{D}) & \text{Sweedler copper of a monoid} \\ \mathcal{M}: (\mathbf{Mon}(\mathbb{D}))^{\mathrm{op}} \times \mathbf{Mon}(\mathbb{D}) \to \mathbf{Comon}(\mathbb{D}) & \text{Sweedler hom ofmonoids} \\ & & \text{(univ. measuring command)} \end{array}$$

are everywhere defned by the following adjunctions if the adjoints exist.

$$\begin{array}{ccc} \mathbf{Comon}(\mathbb{D}) & \mathbf{Mon}(\mathbb{D}) & \mathbf{Comon}(\mathbb{D}) \\ \huge{\qquad} \mathrm{-\*}D\_{1} \left\{ \begin{array}{c} \mathrm{+} \\ \mathrm{\qquad} \end{array} \right\} \mathcal{C}(D\_{1}, -) & \mathrm{D} \flat - \left\{ \begin{array}{c} \mathrm{+} \\ \mathrm{\qquad} \end{array} \right\} \mathrm{D} \cdot \star- & \huge{\qquad} \mathcal{T} \left\{ \begin{array}{c} \mathrm{+} \\ \mathrm{\qquad} \end{array} \right\} \mathcal{M}(T, -) \\ \mathbf{Comon}(\mathbb{D}) & \mathbf{Mon}(\mathbb{D}) & \mathbf{Mon}(\mathbb{D}) \end{array}$$

They are defned for specifc pairs of (co)monoids if the universal objects specifed by the following bijections exist.

$$\begin{array}{c} \begin{array}{c} \begin{array}{c} UT \star UD \rightarrow UR \text{ means.} \\ \hline T \rightarrow D \rightarrow \ast R \end{array} \\ \begin{array}{c} \begin{array}{c} T \rightarrow D \rightarrow T \rightarrow R \end{array} \\ \hline D \rightarrow T \rightarrow R \end{array} \end{array} \end{array}$$

The comonoid M(T, I) is called the Sweedler dual of the monoid T.

By defnition, the comonoid C(D1, D) is the fnal comonoid interacting with the comonoid D1 D-residually. The Sweedler hom M(T, R) is the fnal Rresidually interacting comonoid for the monoid T. The Sweedler copower D ▷ T is the initial residual monoid for monoid-comonoid interactions of T and D.

If the Sweedler operations are everywhere defned, for which it sufces that D is locally presentable [20, Thm. 20], then the category (Comon(D), J, ⋆, C) is symmetric monoidal closed and the category (Mon(D), ▷, −⋆,M) is copowered, powered and enriched over (Comon(D), J, ⋆, C). However, local presentability of C is not enough for local presentability (or even accessibility) of [C, C]a (for example, [Set, Set]a is not accessible). In Sect. 5, we return to the question of everywhere-defnedness of the Sweedler operations for [C, C]a.

The Sweedler theory perspective allows us to establish some facts about interaction laws of free monads very easily. For example, we can straightforwardly derive a characterization of measuring maps from the free monoid F ∗ on F (assuming it exists).

Proposition 1. Measuring maps U(F ∗ )⋆UD → UR are in bijection with maps F ⋆ UD → UR.

Proof. This is witnessed by the following chain of bijections.

$$\begin{array}{c} \overbrace{F \to UD \to UR}^{F \star UD \to UR} \\ \overbrace{F \to U(D \to R)}^{} \\ \overbrace{F^\* \to D \to R}^{} \\ \overbrace{U(F^\*) \star UD \to UR \text{ means.}}^{} \end{array}$$

Similarly, we can calculate closed-form expressions for the Sweedler hom from a free monoid and the Sweedler copower of a free monoid. Here G† denotes the cofree comonoid on G (if it exists).

#### Proposition 2. (i) M(F ∗ , R) ∼= (F −⋆ UR) † . (ii) D ▷ F ∗ ∼= (F ⋆ UD) ∗ .

Proof. (i) As witnessed by the chain of bijections on the left below, comonoid maps D → M(F ∗ , R) and comonoid maps D → (F −⋆ UR) † are in bijection naturally in D. (ii) The chain of bijections on the right below composes to a bijection natural in R between monoid maps D ▷ F ∗ → R and monoid maps (F ⋆ UD) ∗ → R.

$$\begin{array}{ll} \frac{D \to (F \to UR)^{\dagger}}{UD \to F \to UR} \\ \frac{\overline{F \to UD \to UR}}{\overline{F \to U(D \to R)}} \\ \frac{\overline{F^{\*} \to D \to R}}{\overline{D^{\*} \to D \to R}} \\ \end{array} \qquad\qquad \begin{array}{ll} \frac{(F \star UD)^{\*} \to R}{\overline{F \to UD \to UR}} \\ \frac{\overline{F^{\*} \to UD \to UR}}{\overline{F \to U(D \to R)}} \\ \frac{\overline{F^{\*} \to D \to R}}{\overline{F^{\*} \to D \to R}} \\ \frac{\overline{F^{\*} \to D \to R}}{\overline{D \to F^{\*} \to R}} \end{array}$$

Example 2. Let C = Set. (i) Take F = 0, then F ∗ ∼= Id. We can calculate F −⋆ UR ∼= 1, therefore M(F ∗ , R) ∼= Id, for any monad R.

Next take F X = X2 , then F ∗X ∼= µX′ . X + X′2 (these are leaf-labelled binary trees). We can calculate (F −⋆ UR)Y ∼= R (2 × Y ), hence M(F ∗ , R) Y ∼= νY ′ . Y × R (2 × Y ′ ) (node-labelled streams of bits for R = Id, node-labelled nonempty colists of bits for RZ = 1 + Z).

Finally, take F X = 1 + X2 , then F ∗X ∼= µX′ . X + 1 + X′2 (leaf-labelled nullary-binary trees). We calculate (F −⋆ UR)Y ∼= R 0 × R (2 × Y ), hence M(F ∗ , R) Y ∼= νY ′ . Y × R 0 × R (2 × Y ′ ). For R = Id and any R such that R 0 ∼= 0, this means that M(F ∗ , R) ∼= 0. For RZ = 1 + Z, we get M(F ∗ , R) Y ∼= νY ′ . Y × (1 + 2 × Y ′ ) (node-labelled nonempty colists of bits).

(ii) Take F = 0, then F ⋆ ∼= Id. We can calculate (F ⋆ UD) ∼= 0, hence D ▷ F ∗ ∼= Id, for any comonad D.

Take F X = X2 , then F ∗X ∼= µX′ . X + X′2 . We can calculate (F ⋆ UD)Z ∼= D (Z 2 ), therefore (D ▷ F ∗ )Z ∼= µZ′ . Z + D (Z ′2 ).

Take F X = 1 + X2 , then F ∗X ∼= µX′ . X + 1 + X′2 . We can calculate (F ⋆ UD)Z ∼= D 1 + D (Z 2 ), therefore (D ▷ F ∗ )Z ∼= µZ′ . Z + D 1 + D (Z ′2 ).

These examples generalize to any wellpointed, locally presentable C with exponentials, when R and D are strong.

In exactly the same way as above, comonoid maps D0 ⋆ D1 → G† are in bijection with maps UD0 ⋆ UD1 → G, and C(D1, G† ) ∼= (UD1 −⋆ G) † .

In the rest of this paper, we ignore comonad-comonad interaction laws and the internal hom of comonads since they are not our main focus. But developments similar to those for monad-comonad interaction laws and the Sweedler hom of monads and the Sweedler copower of a monad in Sects. 4, 5) below can be carried out for them as well.

### 4 Monad-comonad Interaction Laws (Co)algebraically

We now return to monad-comonad interaction laws specifcally and explain the (co)algebraic perspective developed in [33]. (Props. 4 and 6 did not appear in [33].) First, monad-comonad interaction laws admit the following useful characterization in terms of (co)algebras of the (co)monads involved.

Proposition 3. R-residual monad-comonad interaction laws ψ of T, D are in bijection with functors Ψ : (Coalg(D))op ×Alg(R) → Alg(T) that internal-hom carriers, i.e., satisfy

$$\begin{array}{c} (\mathsf{Coolg}(D))^{\mathrm{op}} \times \mathsf{Alg}(R) \xrightarrow{\Psi} \begin{array}{c} \mathsf{Alg}(T) \\ \longrightarrow \\ \mathsf{C^{op}} \times \mathbb{C} \xrightarrow{\begin{array}{c} \\ \end{array} \\ \end{array}} \end{array} \xrightarrow{\begin{array}{c} \mathsf{Alg}(T) \\ \longrightarrow \\ \end{array}} \begin{array}{c} \mathsf{Alg}(T) \\ \longrightarrow \\ \end{array}$$

Proof (sketch). Given an interaction law ψ, the functor Ψ is defned by

$$\Psi((Y,\chi),(Z,\zeta)) = (Y \multimap Z,\ T(Y \multimap Z) \xrightarrow{\psi} DY \multimap RZ \xrightarrow{\chi \multimap \zeta} Y \multimap Z),$$

Conversely, given a functor Ψ, the corresponding interaction law ψ is defned by

$$\psi = \ T(Y \rightharpoonup Z) \xrightarrow{T(\epsilon\_Y \rightharpoonup \eta\_Z^R)} T(DY \rightharpoonup RZ) \xrightarrow{\xi} \xrightarrow{\xi} DY \rightharpoonup RZ$$

where (DY ⊸ RZ, ξ) = Ψ((DY, δY ),(RZ, µR Z )). ⊓⊔

We remark that such functors Ψ are completely determined by their action on (co)free (co)algebras. To be precise, there is a bijection between these functors and functors Ψ ′ : (CoKl(D))op × Kl(R) → Alg(T) that satisfy

$$\begin{array}{c} (\mathbf{CoKl}(D))^{\mathrm{op}} \times \mathbf{Kl}(R) \xrightarrow{\Psi'} \mathbf{Alg}(T) \\ \sideset{ $\mathbb{C}^{\mathrm{op}} \times \mathbb{K}$ } \\ \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \xrightarrow{\cdots} \xrightarrow{\cdots} \mathbb{C} \end{array}$$

where K : CoKl(D) → C is the left adjoint of the coKleisli adjunction of D and K : Kl(R) → C is the right adjoint of the Kleisli adjunction of R.

The following reformulations of Prop. 1 enable a smooth derivation of further characterizations of monad-comonad interaction laws in terms of what we call runners, introduced next.

Corollary 1.  Stateful runners form a category SRunR(T).

R-residual stateful runners of T with carrier Y are in bijection with monad maps T → StR Y where StR Y is the R-transformed state monad for state object Y defned by StR Y X = Y ⊸ R(X ⊗ Y ).

They are also in bijection with functors Θ : Alg(R) → Alg(T) that internalhom Y with the carrier, i.e., satisfy

$$\begin{array}{c} \mathsf{Alg}(R) \xrightarrow{\partial} \mathsf{Alg}(T) \\ \upsilon \bigvee\_{Y \hookrightarrow -} \qquad \bigvee\_{U}^{U} \\ \mathbb{C} \xrightarrow{Y \hookrightarrow -} \end{array}$$

Proof (sketch). Given a stateful runner θ, the functor Θ is defned by

$$\Theta(Z,\zeta) = \ T(Y \multimap Z) \xrightarrow{\theta\_Y \multimap Z} Y \multimap R((Y \multimap Z) \otimes Y) \xrightarrow{Y \multimap R\mathfrak{a}\lhd} Y \multimap RZ \xrightarrow{Y \multimap \zeta} Y \multimap Z$$

Conversely, given a functor Θ, the stateful runner θ is

$$\theta\_X = \begin{array}{ccccc} \text{T} & \xrightarrow{T \text{coay}} \text{T} (Y \rightharpoonup X \otimes Y) \xrightarrow{T(Y \rightharpoonup \eta\_X^R \otimes Y)} \text{T} (Y \rightharpoonup R(X \otimes Y)) \xrightarrow{\xi} & \xrightarrow{\xi} \text{Y} \multimap \text{R} (X \otimes Y) \\\\ \cdot & \xrightarrow{\cdot} & \cdots & \cdots & \cdots & \cdots & \text{ $\\_D$  } \cdot \end{array}$$

where (Y ⊸ R(X ⊗ Y ), ξ) = Θ(R(X ⊗ Y ), µR X⊗Y ). ⊓⊔

This observation is strengthened by the following proposition that also talks about stateful runner maps.

Proposition 4. The following is pullback square:

$$\begin{array}{c} \mathsf{SRun}\_{R}(T) \xrightarrow{\begin{subarray}{c} \\ \begin{subarray}{c} U \end{subarray}} \end{subarray}} \xrightarrow{\begin{subarray}{c} \mathrm{[Alg}(R), \mathrm{Alg}(T)]^{\text{op}} \\ \end{subarray}} \begin{subarray}{c} \big[\begin{subarray}{c} \mathrm{[I,C]^{\text{op}}} \end{subarray}} \xrightarrow{\begin{subarray}{c} \big[\begin{subarray}{c} \mathrm{[Mg}(R),U]^{\text{op}} \end{subarray} \end{subarray} \end{array} \end{array}} \begin{array}{} [\mathrm{Alg}(R), \mathrm{Alg}(T)]^{\text{op}} \\ \big[\begin{subarray}{c} \mathrm{[Mg}(R),U]^{\text{op}} \end{subarray} \right]} \xrightarrow{\begin{subarray}{c} \big[\begin{subarray}{c} \mathrm{[Mg}(R),U]^{\text{op}} \end{subarray} \right]} \end{array}} [\mathrm{Alg}(R), \mathrm{U}]^{\text{op}} $$

Combining Prop. 4 with Cor. 1, we obtain a characterization of monadcomonad interaction laws in terms of stateful runners.

Proposition 5. R-residual monad-comonad interaction laws T, D are in a bijection with functors Ψ : Coalg(D) → SRunR(T) preserving carriers, i.e., satisfying

### Continuation-Based Runners

A D-fuelled continuation-based runner of T is an object Z ∈ C together with a family of maps

$$\theta\_X: D(X \multimap Z) \to TX \multimap Z$$

natural in X satisfying

$$\begin{array}{c} D(X \multimap Z) \xrightarrow{\theta\_X} TX \multimap Z \\ \hfil X \multimap Z \xrightarrow{\begin{subarray}{c} \theta\_X \\ \end{subarray}} X \xrightarrow{\begin{subarray}{c} \operatorname{\reflectbox{ $D$ }} \\ \end{subarray}} X \xrightarrow{\begin{subarray}{c} \operatorname{\reflectbox{ $D$ }} \\ \end{subarray}} \begin{array}{c} T \multimap Z \\ \end{array}} \begin{array}{c} TX \multimap Z \\ \hfil X \multimap Z \\ \end{array} \end{array} \xrightarrow{\begin{array}{c} TX \multimap Z \\ \hline \end{array}} TX \multimap Z \\ \hfil X \multimap Z \end{array}$$

These runners form a category CRunD(T).

D-fuelled continuation-based runners of T with carrier Z are in bijection with monad maps T → CntD Z , where CntD Z is the D-transformed continuation monad for answer object Z defned by CntD Z X = D(X ⊸ Z) ⊸ Z.

Continuation-based runners are also in bijection with functors Θ : (Coalg(D))op → Alg(T) that internal-hom the carrier with Z, i.e., that satisfy

$$\begin{array}{c} (\mathsf{Coalg}(D))^{\operatorname{op}} \xrightarrow{\partial} \mathsf{Alg}(T) \\ \mathsf{C}^{\operatorname{op}} \xrightarrow{\operatorname{\,}\_{\operatorname{\,}^{\operatorname{op}}}} \xrightarrow{\operatorname{\,}\_{\operatorname{\,}^{\operatorname{\,}}}} \mathsf{C} \end{array}$$

Moreover:

Proposition 6. The following is a pullback square:

$$\begin{array}{c} \mathbf{CRun}\_{D}(T) \xrightarrow{\begin{subarray}{c} \\ \mathbf{U} \end{subarray}} \begin{subarray}{c} \\ \end{subarray}} \xrightarrow{\begin{subarray}{c} \left[ (\mathbf{Coalg}(D))^{\operatorname{op}}, \operatorname{Alg}(T) \right] \end{subarray}} \begin{subarray}{c} \left[ (\mathbf{Coalg}(D))^{\operatorname{op}}, \operatorname{Alg}(T) \right] \end{subarray} \\ \begin{subarray}{c} \left[ (\mathbf{CCoalg}(D))^{\operatorname{op}}, \mathbb{C} \right] \end{subarray} \xrightarrow{\begin{subarray}{c} \left[ (\mathbf{Coalg}(D))^{\operatorname{op}}, U \right] \end{subarray}} \begin{subarray}{c} \left[ (\mathbf{Coalg}(D))^{\operatorname{op}}, \mathbb{C} \right] \end{subarray} \end{array}$$

Combining this proposition with Cor. 1, we obtain:

Proposition 7. R-residual monad-comonad interaction laws of T, D are in bijection with functors Ψ : Alg(R) → CRunD(T) that preserve carriers, i.e., that satisfy

### 5 Combining Sweedler Theory and the (Co)algebraic Perspective

We now combine our (co)algebraic observations with Sweedler theory.

### Sweedler Hom

By defnition, the Sweedler hom between monads T, R, if it exists, is the comonad M(T, R) together with an monad-comonad interaction law υ such that, for any other comonad D and monad-comonad interaction law ψ, there exists a unique comonad map g : D → M(T, R) satisfying

$$\underbrace{\epsilon\_{X\otimes Y}}\_{TX\otimes DY\_{TX\otimes g\_Y}^{\omega\_{X,Y}}}\wedge\cdots\wedge\wedge\wedge\wedge\wedge\wedge\wedge$$

Comonad maps D → D′ are in bijection with functors Coalg(D) → Coalg(D′ ) that preserve carriers. Therefore, by Prop. 5, the Sweedler hom, if it exists, is the comonad M(T, R) together with a carrier-preserving functor Υ : Coalg(M(T, R)) → SRunR(T) such that, for any other comonad D and carrier-preserving functor Ψ : Coalg(D) → SRunR(T), there exists a unique carrier-preserving functor Γ : Coalg(D) → Coalg(M(T, R)) such that

It follows that, if (SRunR(T), U) is strictly comonadic, then M(T, R) exists and (Coalg(M(T, R)), U) ∼= (SRunR(T), U). (Should (SRunR(T), U) fail to be strictly comonadic, then M(T, R) may still exist, but with diferent algebras.) Easy calculations show that U strictly creates equalizers of U-split pairs. Hence, by the dual of Beck's monadicity theorem, U is strictly comonadic if it is a left adjoint. Under our assumptions on C, T and R from Sect. 2, all is well.

Theorem 1. If C is locally presentable and T and R are accessible monads on C, then SRunR(T) is locally presentable and the forgetful functor U : SRunR(T) → C is a left adjoint. Hence the Sweedler hom M(T, R) exists, is accessible, and satisfes (Coalg(M(T, R)), U) ∼= (SRunR(T), U).

Proof (sketch). We frst show that SRunR(T) is locally presentable. The functor U : SRunR(T) → C strictly creates colimits by easy calculations, and hence SRunR(T) is cocomplete. For local presentability, it therefore remains to show that SRunR(T) is accessible, which we do by appealing to the fact that accessible categories are closed under inserters and equifers. The category of Fcoalgebras, for any accessible endofunctor F on C, is an inserter of accessible functors, and is therefore accessible by [1, Thm. 2.72]. For each Y , families of maps θX : T X ⊗ Y → R(X ⊗ Y ) natural in X are in bijection with maps χ : Y → (T −⋆ R)Y , so that R-residual stateful runners of T are equivalently coalgebras (Y, χ) of the functor T −⋆ R, satisfying two equations. One equation is an equality between two maps Y → (Id −⋆ R)Y , the other between two maps Y → ((T · T) −⋆ R)Y . It follows that SRunR(T) is isomorphic to a full subcategory of the category coalg(T −⋆ R) of (T −⋆ R)-coalgebras, and that this full subcategory is the joint equifer of two natural transformations of accessible functors coalg(T −⋆ R) → coalg(Id −⋆ R) and of two natural transformations of accessible functors coalg(T −⋆ R) → coalg((T · T) −⋆ R). Accessible categories are closed under equifers of natural transformations of accessible functors [1, Lemma 2.76], so SRunR(T) is accessible and hence locally presentable.

As a colimit-preserving functor between locally presentable categories, U is a left adjoint by Freyd's special adjoint functor theorem, thus strictly comonadic. The induced comonad is the Sweedler hom M(T, R). Accessibility of M(T, R) follows from accessibility of the adjoints (the right adjoint by [1, Prop. 2.23]). ⊓⊔

Example 3. Let C = Set. Take T X = XS (the reader monad for state object S). R-residual stateful runners of T are objects Y with families of maps XS × Y → R(X ×Y ) natural in X or, equivalently, maps Y → R(S ×Y ) constrained by two equations. For R = Id or R = 1+−, these are in bijection with maps Y → S. The comonad with such structured objects Y as coalgebras, which is the Sweedler hom of T and R, is DY = S × Y (the coreader monad for S). For a general accessible monad R, the Sweedler hom can be described as a subcomonad of the cofree comonad DY = νY ′ . Y × R(S × Y ′ ).

Take T X = X+ = µX′ .X × (1 + X′ ) (the nonempty list monad with concatenation as multiplication, free semigroup monad). R-residual stateful runners of T are objects Y with families of maps X+ × Y → R(X × Y ) natural in X satisfying two equations or, equivalently, maps (X × X) × Y → R(X × Y ) constrained by one equation or, equivalently, maps Y → R(Y + Y ) coassociative wrt. the coproduct monoidal structure of Kl(R), i.e., making Y into a cosemigroup. For R = Id, the corresponding comonad is the cofree cosemigroup (wrt. the coproduct monoidal structure on Set) comonad. Its underlying functor is DY ∼= Y × (Y + Y ).

These examples generalize to any wellpointed, locally presentable C with exponentials, when R is a strong monad.

### Sweedler Copower

The Sweedler copower of a monad T by a comonad D, if it exists, is by defnition the monad D ▷ T together with a monad-comonad interaction law υ such that, for any other monad R and monad-comonad interaction law ψ, there exists a unique monad map g : D ▷ T → R satisfying

$$\|\xi\|\_{T\otimes DY\xrightarrow[\upsilon\_{X,Y}\to\{D\not\simeq T\}\backslash X\otimes Y\rangle\atop\mathcal{B}X\otimes Y}}\lesssim\|\xi\|\_{Y\otimes Y}$$

Monad maps R′ → R are in bijection with functors Alg(R) → Alg(R′ ) that preserve carriers. Therefore, by Prop. 7, the Sweedler copower, if it exists, is the monad D ▷ T together with a carrier-preserving functor Υ : Alg(D ▷ T) → CRunD(T) such that, for any other monad R and carrier-preserving functor Ψ : Alg(R) → CRunD(T), there exists a unique carrier-preserving functor Γ : Alg(R) → Alg(D ▷ T) such that

Consequently, if (CRunD(T), U) is strictly monadic, then D ▷ T exists and (Alg(D ▷ T), U) ∼= (CRunD(T), U). This is the case as soon as U is a right adjoint by Beck's strict monadicity theorem, because U is easily verifed to strictly create U-split coequalizers.

Theorem 2. If C is locally presentable and T and D are accessible, then CRunD(T) is locally presentable and the forgetful functor U : CRunD(T) → C is a right adjoint. Hence the Sweedler copower D ▷ T exists, is accessible, and satisfes (Alg(D ▷ T), U) ∼= (CRunD(T), U).

Proof (sketch). The proof is similar to that of Thm. 1. The functor U strictly creates limits, so CRunD(T) is complete. The category CRunD(T) is isomorphic to a full subcategory of the category of algebras of the functor D ⋆ T, forming a joint equifer. Categories of algebras of accessible endofunctors on C are inserters of accessible functors, and hence form accessible categories. It follows that CRunD(T) is also accessible, and hence locally presentable. The functor U strictly creates κ-fltered colimits, where κ is such that Id ⋆ T, D ⋆ T, and (D · D) ⋆ T are κ-accessible; in particular, U is accessible. Since U also strictly creates limits, it is therefore a right adjoint by [1, Theorem 1.66]. The induced monad is the Sweedler copower D ▷T, which is accessible because both adjoints are. ⊓⊔

Example 4. Let C = Set. Take T X = M × X where (M, u, ∗) is a monoid (the writer monad) and DY = S×Y (the coreader comonad). D-fuelled continuationbased runners of T are objects Z with families of maps S×Z X → ZM×X natural in X or, equivalently, maps (S × M) × Z → Z, subject to two equations. The monad with such structured objects Z as algebras, which is the Sweedler copower of T and D, is the writer monad for the free monoid on S × M quotiented by (s, a) ∗ (s, b) = (s, a ∗ b) and u = (s, u).

### 6 Enriched Interaction Laws

In Sects. 2, 4, 5 above, we worked with (a full subcategory of) the category [C, C] of endofunctors on a SMCC C and natural transformations between them, and abstracted it to a duoidal category D in Sect. 3.

An alternative is to proceed from an SMCC (V, I, ⊗,⊸) (copowered over itself by ⊗ and enriched and powered by ⊸) and another category C that is at least copowered or enriched over V, or possibly both or even powered too. In this setting, a V-enriched functor-functor interaction law is given by V-enriched endofunctors F on V and G and H on C together with either a family of maps ϕX,Y : F X • GY → H(X • Y ) in C that are V-natural in X ∈ V and Y ∈ C or, equivalently, a family of maps ϕY,Z : F(C(Y, Z)) → C(GY, HZ) in V that are V-natural in Y, Z ∈ C.

Two cases are of special interest.

The only case where the enriched setting agrees with the main one of this paper of Sects. 2–5, i.e., the concept of interaction law where there are no nonvacuous enrichment requirements and the endofunctors involved are all on the same category, is the intersection of the above two: V = C = Set.

A more general situation in which the two settings do not difer too much is when V = C and C is monoidally wellpointed. Then all functors with codomain C are uniquely C-enriched (but may fail to admit an enrichment) and all natural transformations between C-enriched functors with codomain C are C-enriched.

In the case V = C, which is probably the most interesting case for mathematical semantics applications, the duoidal abstraction of Sect. 3 still applies. We can take D to be (a suitable full subcategory of) C-[C, C], where C-[C, C] is the ordinary category of C-functors C → C (strong endofunctors).

In the case of a general V, the simple duoidal abstraction ceases to apply. We need to switch to an action ⋆ : W × D → D (in MonCAToplax) of a symmetric duoidal category (W, IW, ⋄W, JW, ⋆W) on a monoidal category (D, I, ⋄) together with a functor −⋆ : D op ×D → W such that −⋆ G ⊢ G−⋆− (in CAT). Crucially, the action ⋆ comes with structural laws

$$I \vdash\_{\mathcal{W}} \star I \to I \qquad (F \diamond\_{\mathcal{W}} G) \star (H \diamond K) \to (F \star H) \diamond (G \star K).$$

witnessing oplaxity of ⋆. Similarly to the simple duoidal situation, we get that ⋆ and −⋆ lift to functors ⋆ : Comon(W) × Comon(D) → Comon(D) and −⋆ : (Comon(D))op × Mon(D) → Mon(W) and can then defne measuring maps and Sweedler-like operations and ask if they are everywhere defned.

The instantiation is given by (suitable full subcategories of) W = V-[V, V], D = V-[C, C] and

$$\begin{array}{ll} (F \star G) \ Z = \int^{X,Y} \mathbb{C}(X \bullet Y, Z) \bullet (FX \bullet GY) & = \int^{Y} F(\mathbb{C}(Y, Z)) \bullet GY\\ (G \to H) \ X = \int\_{Y,Z} (X \multimap \mathbb{C}(Y, Z)) \to \mathbb{C}(GY, HZ) & = \int\_{Y} \mathbb{C}(GY, H(X \bullet Y)) \end{array}$$

where the integral signs now stand for V-enriched coends and ends.

### Runners as Generalized Algebras

Enriched monad-comonad interaction laws can be characterized as enriched functors between categories of (co)algebras analogously to Props. 3, 5, 7. But one pleasant feature of the enriched setting is that enriched versions of both stateful and continuation-based runners of T can be described as algebras of T in a generalized sense.

Suppose we are given an SMCC V (copowered over itself by ⊗ and enriched and powered by ⊸) and a V-enriched monad T on V. For a category K that is enriched and powered over V, we say that an algebra of T in K as an object Y of K together with family of maps χX : X ⋔ Y → T X ⋔ Y in K that is V-enriched natural in X ∈ V and satisfes the equations

$$X \nrightarrow Y \xrightarrow{\times X} TX \nrightarrow Y \quad \begin{tabular}{c} \times X \nrightarrow Y \\ \searrow X \\ X \nrightarrow Y \end{tabular} \xrightarrow{\times X} \begin{tabular}{c} TX \nrightarrow Y \\ \searrow \\ TX \nrightarrow Y \end{tabular}$$

If V has enough limits, then these form a V-category Alg(T, K), and there is a forgetful V-functor U : Alg(T, K) → C. (The limits are required to carve out the object of algebra maps (Y, χ) → (Y ′ , χ′ ) from the hom-object K(Y, Y ′ ).)

An algebra like this is equivalently an object Y ∈ K together with a Venriched monad map T → KntY where KntY X = K(X ⋔ Y, Y ). If V = K, an algebra of T in this sense is the same as an algebra in the standard sense. In this case, we have KntY X = (X ⊸ Y ) ⊸ Y .

Enriched runners of T turn out to be algebras of T in this generalized sense. Given a category C enriched and copowered over V and a V-enriched monad R on C, an V-enriched R-residual stateful runner of T is an object Y ∈ C together with a family of maps θX : T X • Y → R(X • Y ) in C V-natural in X ∈ V and satisfying two equations. Enriched stateful runners of T are in bijection with algebras of T in (Kl(R))op .

Proof (sketch). The statement is wellformed since, as soon as C is V-enriched and copowered by a functor • : V ⊗ C → C, we have that Kl(R) is V-enriched and copowered by a functor V ⊗ Kl(R) → Kl(R) that agrees with • on objects. Therefore (Kl(R))op is V-enriched and powered by the opposite of that functor. We have the following chain of bijections:

$$\frac{TX \bullet Y \to R(X \bullet Y) \text{ in } \mathbb{C} \text{ } \mathbb{V}\text{-nat. in } X}{TX \bullet Y \to X \bullet Y \text{ in } \mathbf{Kl}(R) \text{ } \mathbb{V}\text{-nat. in } X}$$

$$\frac{\begin{array}{l} X \wedge Y \to TX \wedge Y \text{ in } (\mathbf{Kl}(R))^{\text{op}} \text{ } \mathbb{V}\text{-nat. in } X \end{array}}{\Box} \end{array}$$

The statement about the category of enriched stateful runners is:

Proposition 8. If Alg(T,(Kl(R))op) exists as a V-category, then so does V-SRunR(T), and the following is a pullback square (in V-CAT).

$$\begin{array}{c} \mathbb{V}\text{-SRun}\_{R}(T) \longrightarrow \begin{array}{c} (\textbf{Alg}(T,(\textbf{Kl}(R))^{\text{op}})^{\text{op}})\\ \cdot\\ \mathbb{C} \xrightarrow{J} \end{array} \end{array} \biguplus \begin{array}{c} \downarrow\\ U^{\text{op}}\\ \end{array}$$

In the special case when V = C and R = IdC, we get (Coalg(MC(T, Id), U) ∼= ((Alg(T, C op))op, Uop) ("coalgebras" of the C-monad T).

By the same token, given a V-enriched and powered category C and a Venriched comonad D on C, we can defne what an V-enriched D-fuelled continuation based runner of T is: an object Z ∈ C together with a family of maps θX : D(X ⋔ Z) → T X ⋔ Z in C that is V-natural in X ∈ V and satisfes two equations. Enriched continuation-based runners of T are in bijection with algebras of T in the coKleisli category of D. Moreover:

Proposition 9. If Alg(T, CoKl(D)) exists as a V-category, then so does V-CRunD(T), and the following is a pullback square:

$$\begin{array}{c} \mathbb{V}\text{-CR}\mathbf{un}\_{D}(T) \longrightarrow \text{Alg}(T, \mathbf{CoKl}(D)) \\ U \\ \mathbb{C} \xrightarrow{U} \xrightarrow{J} \mathbf{CoKl}(D) \end{array}$$

### 7 Related Work

In semantics work, the use of monads as notions of computation was pioneered by Moggi [23], but the frst to study comonads (or algebraic theories comodelled) as notions of environment (not under that name) were Shkaravska and Power [29]. This work was developed further by Plotkin and Power [24] and then Møgelberg and Staton [22] (who considered the enriched setting). Stateful runners appeared in Uustalu's paper [32], who noticed that nonresidual stateful runners of a set monad induced by an algebraic theory are in bijection with coalgebras of the comonad induced by the same theory (comodels). The concept of monad-comonad interaction law was distilled by Katsumata et al. [16], who also noticed that the universal interacting comonad of a monad is an instance of the Sweedler hom from Sweedler theory for duoidal categories; they calculated the dual and Sweedler dual for a number of cases. Uustalu and Voorneveld [33] noticed the bijection between monad-comonad interaction laws and suitable functors between categories of (co)algebras and that, in addition to stateful runners, monad-comonad interaction laws relate to continuation-based runners. Garner [12,11] further developed this thread. In particular, he gave a formula for the Sweedler duals of polynomial monads, and demonstrated properties of the dual/Sweedler dual (costructure/cosemantics) adjunction for accessible Set- (co)monads, such as its idempotency. He also pointed out that, when T and R are accessible Set-monads, the coalgebras of the Sweedler hom M(T, R) are algebras of T in (Kl(R))op with, as maps between them, maps in Set that J : Set → Kl(R) sends to algebra maps.

Independently, and earlier than in the semantics community, monad-comonad interaction laws were discovered among functional programmers by Kmett [19] and Freeman [8].

There is a disconnected and more mature thread of work in universal algebra started by Freyd [9] (or even Kan [15]), and continued by Tall and Wraith [31,34] and Bergman and Hausknecht [5], studying functors from coalgebras of a covariety to algebras (like those of our Prop. 3) in the case V = Set, R = IdC of our enriched setting. (There are also textbook expositions, by Popescu and Popescu [26, Ch. 3] and Bergman [4, Ch. 10].) Strangely, this thread seems to have never been picked up in semantics work. It was not cited in the work by Power and coauthors [29,24], and the later authors (except Garner) have been unaware of it.

Sweedler's original work [30] was for (co)algebras over a feld. Anel and Joyal [3] studied the Sweedler theory in great detail for dg-(co)algebras [3]. It was abstracted for (co)monoids in symmetric monoidal closed categories by Porst and Street [28] and Hyland et al. [14] (the internal hom of comonoids is older and goes back to Porst [27]) and then generalized for duoidal categories by L´opez Franco and Vasilakopoulou [20]. A typical example duoidal structure on a functor category is given by the Day convolution and pointwise tensor. Garner and L´opez Franco [13] considered the example of composition and the Day convolution of endofunctors (κ-accessible for a fxed κ).

We do not know the earliest reference to generalized algebras of a monad, in particular, coalgebras of a monad. The latter were considered by Poinsot and Porst [25] (and models of algebraic theories elsewhere than Set are standard).

### 8 Conclusion and Future Work

We have studied universal (co)monads for monad-comonad interactions. We have shown that an elegant setting for such a study on a more general level is provided by Sweedler theory for general duoidal categories as developed by L´opez Franco and Vasilakopoulou [20]. But for results about monad-comonad interaction specifcally it is fruitful to combine it with the (co)algebraic perspective on monad-comonad interaction laws [33]. This makes it possible to characterize the universal (co)monads defned by Sweedler operations via their categories of (co)algebras in terms of diferent favors of runners.

We have witnessed that there is the choice of whether to work with ordinary monad-comonad interaction laws or with the enriched version. It remains to be seen which option yields a richer or more useful theory. An issue with the enriched option is that we know little about accessibility for enriched categories, although some studies exist (e.g., [18,6,7]).

We refrained from discussing it in this paper altogether, but of course one can specifcally study interaction laws of monads and comonads specifed by algebraic theories. We intend to do this in a sequel paper. We also plan to explain properly the signifcance for semantics of the constructions of this paper by describing in detail how they work on semantics-motivated examples and what this means.

Acknowledgements We thank Niels Voorneveld for many useful discussions. Richard Garner's work is an endless source of inspiration. D.M. and T.U. were supported by the Icelandic Research Fund project grant no. 196323-053, T.U. also by the Estonian Research Council team grant no. PRG1210. E.R. was supported by the Estonian Research Council personal grant no. PSG659.

### References

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.

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. 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

## Model Checking Temporal Properties of Recursive Probabilistic Programs

Tobias Winkler , Christina Gehnen , and Joost-Pieter Katoen

RWTH Aachen University, Aachen, Germany<EMAIL_ADDRESS><EMAIL_ADDRESS>
Abstract. Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on ω-regular and LTL properties. In this paper, we study the model checking problem of pPDA against ω-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than ω-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.

Keywords: Probabilistic Recursive Programs · Model Checking · Probabilistic Pushdown Automata · Visibly Pushdown Languages · CaRet.

### 1 Introduction