Andr É Hirschowitz

Tom Hirschowitz

Ambroise Lafont

© A Hirschowitz

MODULES OVER MONADS AND OPERATIONAL SEMANTICS (EXPANDED VERSION)

Keywords:

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as -calculus, -calculus, Positive GSOS specifications, differential -calculus, and the simply-typed, call-by-value -calculus. Moreover, we design a suitable notion of signature for transition monads.

Introduction

The search for a mathematical notion of programming language goes back at least to Turi and Plotkin [START_REF] Turi | Towards a mathematical operational semantics[END_REF], who coined the name "Mathematical Operational Semantics", and explained how known classes of well-behaved rules for structural operational semantics, such as GSOS [START_REF] Bloom | Bisimulation can't be traced[END_REF], can be categorically understood and specified via bialgebras and distributive laws. Their initial framework did not cover variable binding, and several authors have proposed variants which do [START_REF] Fiore | Semantics of name and value passing[END_REF][START_REF] Fiore | A congruence rule format for name-passing process calculi from mathematical structural operational semantics[END_REF][START_REF] Staton | General structural operational semantics through categorical logic[END_REF], treating examples like the -calculus. However, none of these approaches covers higher-order languages like the -calculus.

In recent work, following previous work on modules over monads for syntax with binding [START_REF] Hirschowitz | Modules over monads and linearity[END_REF][START_REF] Ahrens | Modular specification of monads through higher-order presentations[END_REF] (see also [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF]), Ahrens et al. [START_REF] Ahrens | Reduction monads and their signatures[END_REF] introduce reduction monads, and show how they cover several standard variants of the -calculus. Furthermore, as expected in similar contexts, they propose a mechanism for specifying reduction monads by suitable signatures.

Our starting point is the fact that already the call-by-value -calculus does not form a reduction monad. Indeed, in this calculus, variables are placeholders for values but not for general -terms; in other words, reduction, although it involves general terms, is stable under substitution by values only. In the present work, we generalise reduction monads to what we call transition monads. The main new ingredients of our generalisation are as follows.

• We now have two kinds of terms, called placetakers and states: variables are placeholders for our placetakers, while transitions relate states. Typically, in the call-by-value, small-step -calculus, placetakers are values, while states are general terms. • We also have a set of types for placetakers, and a possibly different set of types for transitions and states: transitions of a given type relate states of this type. Typically, in the simply-typed, call-by-value -calculus, both sets of types coincide and are given by simple types; while in pure ¯ -calculus, we have two placetaker types, one for programs and one for stacks, and three transition types, respectively for programs, stacks, and commands. • We in fact have two possibly different kinds of states for each transition type, source states and target states, so that a transition of a given type now relates a source state to a target state of this type. Typically, in the untyped, call-by-value, big-step -calculus, source states (of the unique transition type) are general terms, while target states are values.

• Our variables form a (variable!) family of sets indexed by the placetaker types. To such a variables family , a transition monad assigns -an object ( ) ('of placetakers with free variables in '), which is again a family of sets indexed by the placetaker types, and -two state objects 1 ( ( )) and 2 ( ( )) ('of source (resp. target) states with free variables in '), which are families of sets indexed by transition types; here 1 and 2 are two functors producing state objects out of placetaker objects.

Roughly speaking (see §3), a transition monad consists of three components:

• a placetaker monad ,

• two state functors 1 , 2 ,

• a transition structure consisting of a -module and two -module morphisms src : → 1 and tgt : → 2 , where -modules [START_REF] Hirschowitz | Modules over monads and linearity[END_REF] are objects equipped with substitution by elements of . We view the transition structure ( , src, tgt) as an object of the slice category -Mod / 1 × 2 of (finitary) -modules over 1 × 2 .

Reduction monads [START_REF] Ahrens | Reduction monads and their signatures[END_REF] correspond to the untyped case with 1 = 2 = Id Set . There, reduction monads are identified with suitable relative monads [START_REF] Altenkirch | Monads need not be endofunctors[END_REF], and we provide a similar identification for transition monads (see Proposition 3.6).

We present our series of examples of transition monads in §4:

-calculus, simply-typed -calculus (in its call-by-value, big-step variant), -calculus (as an unlabelled transition system), positive GSOS systems, and differential -calculus.

After defining transition monads, we embark on a second part of the paper, devoted to offering the operational semanticist some hopefully convenient tools for defining programming languages (as transition monads).

Specifically, we propose an approach to the specification of transition monads via signatures, which follows the spirit of Initial Algebra Semantics [START_REF] Goguen | An initial algebra approach to the specification, correctness and implementation of abstract data types[END_REF]. This approach is thus categorical in nature, hence we have to upgrade our sets of transition monads into categories, say TransMnd(P, S), one for each pair (P, S) of sets of placetaker types and transition types (see Definition §5.13). For these categories, we propose what we call a register: for a category C, a register consists of (1) a set Sig of signatures, (2) a semantics mapassigning to each signature in Sig a category -alg of algebras, or models, together with a forgetful1 functor : -alg → C, and (3) a validity proof of the fact that for each , the category -alg has an initial object.

Remark 1.1. This definition is written in type-theoretic style, in the sense that the validity proof is treated as a proper mathematical object. The reader working in a standard, settheoretical logical setting should of course understand this as an additional condition that registers must satisfy.

A register for C yields a "decoding" map spec sending to spec ( ) := (0), where 0 here denotes the initial object in -alg. The efficiency of a register for a category lies in the fact that it allows the expert to easily formalise the informal specification they have in mind for the relevant object. We illustrate in §11 the expressiveness of our register RegTransMnd P,S for transition monads by designing signatures for our examples of §4. For Positive GSOS systems, we even go further by defining a specific register, in which each individual system is more easily specified.

Our register for transition monads is built out from three intermediate registers, corresponding to the three components listed above: • a register RegMnd (Set P ) for monads in the category Set P , • a register Reg[Set P , Set S ] for functors Set P → Set S , and • a register RegTransStruct P,S ( , 1 , 2 ) for transition structures over ( , 1 , 2 ). And as could be expected, a signature for a transition monad in our register RegTransMnd P,S is a record consisting of • a signature of RegMnd (Set P ) specifying the placetaker monad , • two signatures of Reg[Set P , Set S ] specifying the state functors 1 and 2 , and • a signature of RegTransStruct P,S ( , 1 , 2 ) specifying the transition structure.

Here, a crucial feature is that the involved register in the last field of this record depends on the objects specified by previous fields. This contrasts with the approach taken in [START_REF] Ahrens | Reduction monads and their signatures[END_REF], where the corresponding field cannot be expressed in terms of the specified placetaker monad, and must instead be parametric in the models of previous fields. Our choice allows more signatures, and we take advantage of this subtle fact in our treatment (see §11.5) of Ehrhard and Regnier's differential -calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF]. Let us mention that the counterpart for this advantage is that the recursion principle induced by our initial semantics is significantly weaker than could be expected (see Remark 5.14 and §12).

Our signatures for functors and monads incorporate equations similar to those of equational systems: a signature without equations specifies a kind of free object, and adding equations specifies a kind of quotient of this free object, obtained by somehow forcing the added equations to hold. Such a quotienting procedure has already been achieved in a fairly general (and elaborate) way by Fiore and Hur [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]. Under mild additional hypotheses on the ambient category and on equations, we obtain a compact "free+quotient" description of our initial models (Theorems 7.18 and 8.23).

This description roughly goes as follows: we consider a signature augmented with one formal operation for each equation, which yields a new set of terms, say augmented terms.

By interpreting the new operations as prescribed by each side of the equations, we obtain two translations, say and , from augmented terms to plain terms. The initial model is then obtained by identifying any two plain terms of the form ( ) and ( ), for some augmented term .

This description is a crucial ingredient of our treatment of the differential -calculus: as already mentioned, the type of the third field of its signature depends in particular on the monad specified by the first field, and the construction of the signature for this third field relies on our explicit description for that monad (see the proof of Lemma 11.6).

Along the elaboration of our registers, we strive to offer the operational semanticist intuitive notation for defining signatures. They may thus specify programming languages as transition monads by the following procedure:

• Fix sets P and S of placetaker and transition types.

• Pick a signature of RegMnd (Set P ) for specifying the placetaker monad , by operations and equations (e.g., using Notation 7.12). • Choose two signatures of Reg[Set P , Set S ] for specifying the state functors 1 and 2 , again by operations and equations (e.g., using Notation 8.18). • Choose a signature of RegTransStruct P,S ( , 1 , 2 ) for specifying the transition structure, e.g., by giving some rules using the notation of §6.4.

Plan. In §2, we present our notations and give some categorical preliminaries. In §3 we define transition monads and in §4, we present our selected examples (in the traditional way). Then, in §5, we introduce registers and define our register for transition monads, deferring the precise definition of its components to the next sections. We then introduce our registers for transition structures ( §6), monads ( §7), and functors ( §8), stating the announced explicit descriptions of initial algebras along the way. Proofs are dealt with in §9 and §10. In §11, we then revisit all examples from §4, specifying them through signatures of our registers RegTransMnd P,S for transition monads. Finally, we conclude in §12 by summing up our contributions, assessing the scope of our registers RegTransMnd P,S , and giving some perspectives.

Remark 1.2. The reader only interested in using our framework may safely skip §9 and §10.

Related work. As mentioned above, our work refines a recent work [START_REF] Ahrens | Reduction monads and their signatures[END_REF], allowing to cover many new applications with a very similar approach. This approach differs from the bialgebraic one introduced long ago by Plotkin and Turi [START_REF] Turi | Towards a mathematical operational semantics[END_REF]: the positive difference is that it covers higher-order languages like the -calculus, while a negative difference is that it does not recover congruence of bisimilarity.

Regarding syntax with variable binding, we model it using monads, following a standard approach going back to Bellegarde and Hook [START_REF] Bellegarde | Substitution: A formal methods case study using monads and transformations[END_REF] (but see also [START_REF] Altenkirch | Monadic presentations of lambda terms using generalized inductive types[END_REF][START_REF] Hirschowitz | Modules over monads and initial semantics[END_REF][START_REF] Ahrens | Modular specification of monads through higher-order presentations[END_REF]). Because the monad-based approach is essentially equivalent to the presheafbased one [START_REF] Fiore | Abstract syntax and variable binding[END_REF][START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF], we anticipate that our whole framework could be straightforwardly adapted to presheaf models. We are more cautious about nominal sets [START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF], mainly because we would need a better understanding of the status of substitution in the latter approach (see, e.g., Power [Pow07]).

Furthermore, our main register for monads ( §7) is a simply-typed refinement of a known one [START_REF] Ahrens | Modular specification of monads through higher-order presentations[END_REF], close in spirit to [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF]. Its validity proof relies on another, new register ( §9), which combines two standard registers from the literature, respectively based on equational systems [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF] and pointed strong endofunctors [START_REF] Fiore | Abstract syntax and variable binding[END_REF]. We could in fact define a register based on equational systems, and use it directly for specifying monads. Moreover, our explicit description of initial models applies in particular to equational systems (Theorem 10.14).

Concerning our registers for slice categories, we suspect that they could be understood in terms of polynomial functors [START_REF] Kock | Notes on polynomial functors[END_REF], which were recently used in a similar context by Arkor and Fiore [START_REF] Arkor | Algebraic models of simple type theories: A polynomial approach[END_REF].

We are aware of a few notions of signatures for languages with variable binding equipped with some notion of evaluation (or transition) [START_REF] Hamana | Term rewriting with variable binding: An initial algebra approach[END_REF][START_REF] Hamana | Free Σ-monoids: A higher-order syntax with metavariables[END_REF][START_REF] Hirschowitz | Cartesian closed 2-categories and permutation equivalence in higher-order rewriting[END_REF][START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF]. They essentially model rewriting, which implies that transitions are closed under arbitrary contexts. Such approaches cannot cover languages like the -calculus, in which transitions may not occur under inputs or outputs.

As is well-known, evaluation is a directed variant of equality, and transition proofs are a directed form of identity proofs. For this reason, notions of signatures for dependentlytyped languages like type theory may provide an alternative approach to the specification of operational semantics systems. Examples of such notions of signatures include Fiore's simple dependently-sorted signatures [START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF], Altenkirch et al.'s categorical semantics of inductive-inductive definitions [START_REF] Altenkirch | A categorical semantics for inductive-inductive definitions[END_REF], and Garner's combinatorial approach [START_REF] Garner | Combinatorial structure of type dependency[END_REF].

Finally, let us mention that a preliminary version of the present work appears in the third author's PhD thesis [START_REF] Lafont | Signatures and models for syntax and operational semantics in the presence of variable binding[END_REF]Chapter 6].

Differences with conference version.

Here is a list of significant differences w.r.t. the conference version, beyond more detailed proofs.

• Most importantly, we provide an explicit description of the initial algebras of signatures involving equations, in §10. • We also correct a few errors, notably:

-We had omitted the congruence rules for reduction in ¯ -calculus and differentialcalculus. -We had omitted the syntactic equation (

• ) • ≡ ( • ) • from our definition of differential -calculus.
-Again about differential -calculus, we had also erroneously claimed that the method we used for defining unary multiterm substitution applies to partial differentiation. We now rely on the explicit descriptions of §10 for both operations. • Finally, we include a few minor improvements, e.g.:

-We design an abstract version of the original register for slice module categories. In passing, the new version is slightly more expressive. -We design a new register combining the features of equational systems and pointed strong endofunctors into monoidal equational systems ( §9.3). -We provide an alternative way in which to organise the -calculus as a transition monad.

Notations and categorical preliminaries

In this section, we fix some notation, and recall a few categorical notions. We advise the reader to skip it, except perhaps for §2.1, and get back to it when needed. In §2.1, we fix some basic notation. In §2.2, we recall some well-known results about locally finitely presentable categories. Then, in §2.3, we introduce a notion of convenient monoidal category. This is important for us because we will use finitary monads a lot, and these are monoids for the composition monoidal structure on the category of finitary endofunctors. We show in particular that this composition monoidal structure is convenient. We go on in §2.4 by recalling the standard notion of module over a monoid in a monoidal category, and introduce a notion of parametric module, roughly a module definable for all monoids.

We then recall a slightly more general definition of (parametric) modules in the particular case of modules over monads (i.e., when the base category is a functor category). In §2.5, after briefly recalling Beck's monadicity theorem, we state one of its useful (folklore) consequences, a "cancellation" property for monadic functors. In §2.6, we recall the well-known correspondence between finitary monadic functors and finitary monads. Finally, in §2.7, we recall the important fact that equalisers of (finitary) monadic functors are computed as in CAT.

2.1. Basic notation. In the following, Set denotes the category of sets, and CAT denotes the (very large) category of locally small categories. We often implicitly view natural numbers as intervals {1, . . . , } in N, so that, e.g., 2 ∈ 3, 2 ⊆ 3, and so on. Furthermore, in any category with binary products, we denote by , : → × the pairing induced by any morphisms : → and : → . Similarly, when it makes sense, the copairing of : → and : → is denoted by [ , ] : + → . Initial objects are denoted by 0. Given an endofunctor , the category of algebras → is denoted by -alg. When is a monad, the notation -alg rather refers to its category of algebras in the sense of monads, that is, morphisms → satisfying the three standard axioms. Finally, given an object of a category , we denote the slice (resp. coslice) category over (resp. under) by / (resp. / ).

2.2.

Locally finitely presentable categories and finitary functors. We heavily rely on the theory of locally finitely presentable categories [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF]. Very briefly, recall that filtered categories are a categorical generalisation of directed posets.

Definition 2.1. A category is filtered when • it is not empty,

• for any two objects and , there is an object and arrows → and → , and furthermore,

• any two parallel arrows ⇒ are coequalised by some morphism → . A filtered colimit is a colimit of some functor from some small filtered category. Definition 2.2. An object of a category is finitely presentable iff its covariant homfunctor preserves filtered colimits.

Definition 2.3 [AR94, Definition 1.9]. A locally small category is locally finitely presentable iff it is cocomplete and every object is a filtered colimit of objects from a fixed set of finitely presentable generators. • the tensor preserves filtered colimits on the right and all colimits on the left. Proposition 2.9. Any category [C, C] of finitary endofunctors on a locally finitely presentable category C is convenient for the composition monoidal structure.

Proof. By Proposition 2.7, any category of finitary endofunctors on a locally finitely presentable category is locally finitely presentable. Furthermore, since colimits are computed pointwise in functor categories whenever the codomain category is cocomplete [Mac98, §V.4], we have (colim ) • colim ( • ) for any diagram and object , thus the composition tensor product preserves all colimits on the left. Finally, by definition of finitariness, the considered functors preserve filtered colimits, hence for any such diagram and object we have • colim colim ( • ) as desired.

Example 2.10. In particular, all categories of the form [Set P , Set P ] that we will consider below (where P is a set) are convenient for the composition monoidal structure. Definition 2.12. Given a monoid ( , , ) in C, a (right) -module is an object equipped with a morphism : ⊗ → making the following diagrams commute

⊗ ⊗ ⊗ ( ⊗ ) ⊗ ⊗ ( ⊗ ) ⊗ ⊗ , ,

⊗ ⊗

(the axioms for the dual case of left modules are given in [Sea13, §3.2]). We denote by -Mod the category of -modules, with action-preserving morphisms between them.

Remark 2.13. The coherence conditions amount to equipping with algebra structure for the monad -⊗ induced by .

A parametric module will assign a module to any monoid. In order to formally define this, let us introduce the following category, which collects all categories of the form -Mod. In other words, a parametric module functorially assigns to each monoid a module over it.

Example 2.16. If C has products, then we can define the parametric module mapping any monoid to the -module × . It will become clear in §7 how this parametric module can be viewed as the arity of a binary operation, with C = [Set, Set] .

Example 2.17. Any endofunctor on Mon(C) equipped with a natural transformation : Id → induces a parametric module monmod mapping any monoid to ( ), with action given by

( ) ⊗ ( ) ⊗ ---------→ ( ) ⊗ ( ) → ( ),
where the second morphism is the multiplication of ( ) ∈ Mon(C). This construction applies in particular for any monad on Mon(C).

Definition 2.18. A parametric module morphism

→ over C is a natural transformation :

→ between underlying functors Mon(C) → Mod(C), such that U Mod • = id.

Remark 2.19. Concretely, the components of a natural transformation :

→ at any monoid ∈ Mon(C) are pairs of a monoid morphism : → and a suitable natural transformation : ( ) → ( ). The condition U Mod • = id unfolds to = id for all .

2.4.2. (Parametric) modules over monads. The previous definitions of (parametric) modules specialise to the case where C = [E, E] (for the composition monoidal structure). Then, monoids are finitary monads. However, because in this case C is an endofunctor category, there is a slightly more general, "relative", or "heterogeneous" notion of module [START_REF] Hirschowitz | Modules over monads and linearity[END_REF] which will be important for us. Let us recall it now. Definition 2.20. Given a monad on C and a category D, a D-valued -module is a finitary functor : C → D equipped with a right -action • → satisfying coherence conditions analogous to those of Definition 2.12. A morphism of -modules is similarly a natural transformation commuting with action. We denote by -Mod (D) the category of -modules and morphisms between them. Notation 2.22. Given any monad on C, and functor : C → D, we sometimes implicitly equip the functor with its canonical -module structure. This module is free on , in the sense that for any -module and natural transformation : → , there is a unique -module morphism ˜ : → making the following diagram commute.

˜

Of course, ˜ is merely the composite --→ → .

Let us briefly show how to exploit the variability of D.

Definition 2.23. For any in a set P, and any monad on Set P , the functor : Set P → Set mapping any ∈ Set P to ( ) ( ) is a -module, with action given by , : ( ( )) ( ) → ( ) ( ), at any ∈ Set P .

Here is another example construction of -module, which is useful for specifying syntax with variable binding. Definition 2.24. For any sequence 1 , . . . , in a set P, for any monad on Set P and D-valued -module , we denote by ( 1 ,..., ) the D-valued -module defined by

( 1 ,..., ) ( ) = ( + y 1 + . . . + y ),

where y : P → Set P is the embedding defined by y ( ) = 1 if = and ∅ otherwise. If P is a singleton, we abbreviate this to ( ) .

Let us now recall parametric modules over monads (called signatures in [START_REF] Ahrens | High-level signatures and initial semantics[END_REF]). • we denote by Θ the Set P -valued parametric module mapping a monad to itself, as a module over itself; • for any 1 , . . . , ∈ P and D-valued parametric module , let ( 1 ,..., ) associate to each monad the -module ( ) ( 1 ,..., ) as in §2.4, i.e., ( 1 ,..., ) ( ) ( ) = ( ) ( + y 1 + . . . + y ); when P = 1, we merely count the 's and write ( ) ; • for any finitary functor : D → E and D-valued parametric module , the E-parametric module • maps any monad to the -module • ( ); as particular cases: -when D has a terminal object, the terminal D-valued parametric module 1 = 1•Θ maps any monad to the constant -module 1; -for any ∈ P and Set P -valued parametric module , we denote by the Set-valued parametric module mapping any monad to the -module ↦ → ( ) ; -in particular, for any ∈ P, the Set-valued parametric module Θ maps a monad on Set P to the module ↦ → ( ) ; -given a finite family ( ) ∈ of Set-valued parametric modules, let associate to any monad the -module ( ).

In the paper, we will at times use two distinct viewpoints on our signatures for monads. One, more user-friendly, is based on Set-valued, or heterogeneous, parametric modules. The other, more efficient for stating the explicit description of initial algebras, is based on Set P -valued, or homogeneous, modules. The two viewpoints are related by a P-indexed family of adjunctions, which we now recall. For all ∈ P, there is an adjunction (2.1)

[Set P , Set] ⊥ [Set P , Set P ] , (
Proof. Straightforward.
2.5. Creation of (co)limits and monadic functors. In this section, we recall Beck's monadicity theorem [Mac98, Theorem VI.7.1], and state a "cancellation" property for monadic functors. First, we need to recall creation of (co)limits, monadic functors, and absolute (co)limits. We will see in §10 that the main technical notion for our explicit descriptions of initial algebras is creation of (co)limits, so let us briefly recall the basics. We also have the following well-known result: Proposition 2.32. For any monad on a category C, the forgetful functor : -alg → C creates colimits of a given shape whenever preserves them. More concretely, if preserves all colimits of functors with some domain D, then creates them.

Proof. This is a straightforward consequence of [Bor94a, Proposition 4.3.2].

Lemma 2.33. For any category E and functor : C → D with D cocomplete, if creates colimits of shape E, then preserves them.

Proof. Consider any colimiting cocone, say : → of a functor : E → C. We want to show that is colimiting. By cocompleteness of D, has a colimiting cocone, say :

→ . By creation of colimits, has a unique lifting ′ : → ′ to C, which is colimiting. Because colimiting cocones are uniquely isomorphic, there is a unique isomorphism ′ . Finally, functors preserve isomorphisms, so we have ′ = . But is colimiting, hence so is , as desired.

Corollary 2.34. For any monad on a cocomplete category C, and for any category D, the following are equivalent (i) the forgetful functor : -alg → C preserves all colimits of shape D, (ii) the monad preserves all colimits of shape D, and (iii) the forgetful functor : -alg → C creates all colimits of shape D.

Proof. For (i) ⇒ (ii), the left adjoint to is cocontinuous, so = preserves all such colimits by composition. Furthermore, (ii) ⇒ (iii) follows readily from Proposition 2.32. Finally, Lemma 2.33 proves (iii) ⇒ (i).

Definition 2.35. A functor : E → B is monadic if E is isomorphic to a category of algebras -alg for some monad on B, and furthermore, the following diagram commutes. In fact, a lot of our understanding of Monadic /C will follow from the following equivalence. Proof. For any finitary monad , the forgetful functor is finitary by Corollary 2.34, which proves that the functor lifts as claimed. Furthermore, the lifted functor is clearly fully faithful. Finally, it is essentially surjective because if a monadic functor is finitary, then so is the induced monad, again by Corollary 2.34. 2.7. Limits of finitary monadic functors. In this section, we recall a well-known result about limits of (finitary) monadic functors, namely that they are computed as in CAT:

E

Proposition 2.47. The forgetful functor Monadic /C → CAT/C creates limits.

The rest of this section will be devoted to the proof, but first let us record the following.

Corollary 2.48. The forgetful functor Monadic /C → CAT creates equalisers. More precisely, given monadic functors

1 : D 1 → C and 2 : D 2 → C and functors 1 , 2 : D 1 → D 2 such that 2 • = 1 , if A → D 1
is the equaliser of 1 and 2 in CAT, then the composite A → D 1 → C is finitary monadic and underlies the equaliser of 1 and 2 in Monadic /C.

Proof. This follows straightforwardly from Proposition 2.47 and the fact that the forgetful functor from any slice category to the base category creates equalisers (see the proof of [Bor94b, Proposition 2.16.3]).

Returning to the proof of Proposition 2.47, let us start with the following two lemmas.

Lemma 2.49. Finitary monads over any locally finitely presentable category form a locally finitely presentable category.

Proof sketch (see [START_REF] Lack | On the monadicity of finitary monads[END_REF]). Let C be locally presentable. Then C is small, so [C , C] is again locally presentable. Now, finitary monads on C are equivalently monoids for the composition tensor product in [C , C], hence also algebras for a finitary monad on a locally presentable category, which allows us to conclude by the following lemma.

Lemma 2.50. The category of algebras for a finitary monad on any locally finitely presentable category is again locally finitely presentable.

Proof. This is [AR94, Remark 2.78] with = .

We now need to recall three standard definitions, and prove two more lemmas.

Definition 2.51. A functor : C → D is conservative iff, for any morphism : → ′ in C such that ( ) is an isomorphism, so is . Definition 2.52. A functor : C → D is amnestic iff, for any isomorphism : → ′ in C such that ( ) = ( ′ ) and ( ) = id, we have = ′ and = id.

Lemma 2.53. For any conservative and amnestic functor : C → D and morphism in C, if ( ) is an identity, then so is .

Proof. By conservativeness, is an isomorphism. But then by amnesia is an identity. Definition 2.54. A functor : C → D is an iso-fibration iff, for any isomorphism of the form : → ( ), there exists an isomorphism : ′ → such that ( ) = .

Lemma 2.55. Any continuous, conservative, amnestic iso-fibration from a complete category creates limits.

Proof. Consider any continuous, amnestic iso-fibration F : C → D with C complete, and any functor : X → C such that has a limiting cone, say : → . Then, because C is complete, also has a limiting cone, say : → . Because is continuous, ( ) : ( ) → is again limiting, hence we get an isomorphism : → ( ) of cones over . Because is an iso-fibration, we then lift to an isomorphism : ′ → in C such that ( ) = . The cone : ′ → is thus limiting, and an antecedent of . It thus remains to show that it is the only antecedent of . Let thus ′′ : ′′ → be any antecedent of . Because is limiting, there exists a unique cone morphism : ′′ → ′ . But now ( ) is a cone endomorphism → , hence ( ) = id. By Lemma 2.53, we then get ′′ = ′ and = , thus proving that ′′ = as desired.

At last, we have:

Proof of Proposition 2.47. By Corollary 2.46, Monadic /C is equivalent to Mnd (C) op . But the latter is complete as the opposite of Mnd (C), which is locally finitely presentable by Lemma 2.49. Thus, Monadic /C is complete. Moreover, the forgetful functor Monadic /C → CAT/C is continuous. Indeed, it is equivalent (in CAT → ) to the composite Finally, the forgetful functor Monadic /C → CAT/C is a conservative, amnestic isofibration:

Mnd (C) op ↩→ Mnd(C) op → CAT/C,
• it is conservative and amnestic as a full subcategory embedding, and • an iso-fibration because the subcategory in question is replete (otherwise said, monadic functors are closed under isomorphisms). The result thus follows by Lemma 2.55.

Transition monads

In this section, we introduce the main new mathematical notion of the paper: transition monads. In §3.1 we give an informal description and in §3.2, we give our formal definition. In §3.3, we provide an equivalent definition based on the notion of relative monad. Finally, in §3.4, we sketch a proof-irrelevant variant of transition monads.

Overview of transition monads.

Placetakers and states

In standard -calculus, we have terms, variables are placeholders for terms, and transitions relate a source term to a target term. In a general transition monad we still have variables and transitions, but placetakers for variables and endpoints of transitions can be of a different nature, which we phrase as follows: variables are placeholders for placetakers, while transitions relate a source state with a target state.

The categories for placetakers and for states

In standard -calculi, we have a set T of types for terms (and variables); for instance in the untyped version, T is a singleton. Accordingly, terms form a monad on the category Set T . In a general transition monad we have a set P of placetaker types, and placetakers form a monad on the category Set P ; similarly, we have a set S of transition types, and the family of possible states (depending on a given family of variables) forms an object in Set S . For example, for the simply-typed -calculus, P = S is the set of simple types.

The object of variables

In our view of the untyped -calculus, there is a (variable!) set of variables and everything is parametric in this 'variables set'. Similarly, in a general transition monad , there is a 'variables object' in Set P and everything is functorial in this variables object. In particular, we have a placetaker object ( ) in Set P and a source (resp. target) state object in Set S , both depending upon the variables object.

The state functors 1 and 2

While in the -calculus, states are the same as placetakers, in a general transition monad, they may differ, and more precisely both state objects are derived from the placetaker object by applying the state functors 1 , 2 : Set P → Set S .

The transition structure

In standard -calculi, there is a (typed!) set of transitions, which yields a graph on the set of terms. That is to say, if is the variables object, and

( ) the placetaker object, there is a transition object Trans ( ) equipped with two maps src , tgt : Trans ( ) → ( ). Note that we consider 'proof-relevant' transitions here, in the sense that two different transitions may have the same source and target (see 3.4 for the proof-irrelevant variant).

In a general transition monad , we still have a transition object Trans ( ), which now lives in Set S , together with state objects 1 ( ( )) and 2 ( ( )), so that the pairing src , forms a morphism Trans ( ) → 1 ( ( )) × 2 ( ( )). One main feature of transition monads is that transitions are closed under substitution. Technically, this is realised by taking the transition object Trans ( ) to be a -module, and that the morphism Trans ( ) → 1 ( ( )) × 2 ( ( )) to be a -module morphism.

The definition of transition monad.

Here is our formal definition: Definition 3.1. Given two sets P and S, a transition monad over (P, S) consists of • a finitary monad on Set P , called the placetaker monad,

• two finitary functors 1 , 2 : Set P → Set S , called state functors, and

• a transition structure src,tgt -------→ 1 × 2 consisting of -a finitary -module : Set P → Set S , called the transition module, -a source -module morphism src : → 1 , recalling from Notation 2.22 that 1 is the free -module on 1 , -a target -module morphism tgt : → 2 . Definition 3.2. For any sets P and S, finitary monad over Set P , and finitary functors 1 , 2 : Set P → Set S , we let TransStruct P,S ( , 1 , 2 ) denote the class of transition structures over , 1 , and 2 .

Furthermore, let TransMnd P,S denote the coproduct , 1 , 2 TransStruct P,S ( , 1 , 2 ). In Definition §5.13, we will upgrade these classes into categories with the same names.

Transition monads as relative monads.

In our definition of transition monad, we have required the two state modules to take the form 1 and 2 , but this is not essential in our development. Moreover, it probably leaves some relevant examples out of reach. We think in particular about the standard presentation of the -calculus as a labelled transition system. Our original reason for this design choice was purely aesthetic: it ensures that our transition monads are relative monads, as were the reduction monads introduced in [AHLM20] (in particular the untyped -calculus). These were monads relative to the 'discrete graph' functor from sets to graphs, and in our extended context, we have to replace graphs by -graphs. Let us provide more detail.

Let us first recall [ACU15] that, given any functor : C → D, a monad relative to , or -relative monad, consists of • an object mapping : ob(C) → ob(D), together with • morphisms : ( ) → ( ), and • for each morphism : ( ) → ( ), an extension ★ : ( ) → ( ), satisfying coherence conditions. Any -relative monad has an underlying functor C → D, and is said finitary when this functor is. Note that a monad is nothing but a -relative monad, for the identity endofunctor. Now we define -graphs:

Definition 3.3. For any pair = ( 1 , 2 ) of functors Set P → Set S , an -graph over an object ∈ Set P consists of • an object (of edges) in Set S , and

• a morphism : → 1 ( ) × 2 ( ).
Accordingly, an -graph consists of an object ∈ Set P and an -graph over .

We can now say that in a general transition monad, transitions form an -graph over the placetaker object (the whole thing depending upon the variables object...). Before proceeding, we must introduce the category of -graphs: a morphism → ′ consists of a morphism for vertices :

→ ′ together with a morphism for edges :

→ ′ making the following diagram commute. ′ 1 ( ) × 2 ( ) 1 ( ′ ) × 2 ( ′ ) 1 ( )× 2 ( ) ′ Proposition 3.4.
For any pair = ( 1 , 2 ) of functors Set P → Set S , -graphs form a category -Gph.

The proof is a straightforward verification. We will consider monads relative to the following functors:

Definition 3.5. For any pair = ( 1 , 2 ) of functors Set P → Set S , the discrete -graph functor : Set P → -Gph maps any ∈ Set P to the -graph over with no edges. Now we are ready to deliver our characterisation of transition monads as relative monads: Proposition 3.6. Given finitary functors 1 , 2 : Set P → Set S , transition monads with state functors 1 and 2 are exactly monads relative to the discrete -graph functor for = ( 1 , 2 ), such that the induced functor Set P → -Gph is finitary.

The proof consists merely in unfolding the definitions. Since we do not use this result, we do not give further details.

3.4. The proof-irrelevant variant. Although we have chosen a "proof-relevant" notion of transition monad, we can sketch a presentation of a "proof-irrelevant" variant. Definition 3.7. Let ITransStruct P,S ( , 1 , 2 ) denote the subset of TransStruct P,S ( , 1 , 2 ) consisting of transition monads src, tgt : → 1 × 2 such that src, tgt is a pointwise inclusion.

Remark 3.8. We have a natural retraction TransStruct P,S ( , 1 , 2 ) ։ ITransStruct P,S ( , 1 , 2 ), which maps a transition structure : → 1 × 2 to the monomorphism ↩→ 1 × 2 obtained from the (strong epi)-mono factorisation; this factorisation exists [AR94, Proposition 1.61] since the category of finitary Set-valued -modules is a presheaf category [Ahr15, Definition 2.71]. In Proposition 6.19, we will upgrade this retraction into a coreflection of categories.

Examples of transition monads

In this section, we present very informally the announced examples of transition monads. This presentation should eventually be compared to the one via signatures given in §11.

4.1.

The call-by-value, simply-typed, big-step -calculus. The notion of transition monad accounts for many different variants of the -calculus. Let us detail the case of the simply-typed, call-by-value, big-step -calculus. Most often, big-step semantics describes evaluation of closed terms. Here we consider a variant describing the evaluation of open terms [START_REF] Paolini | Call-by-value solvability[END_REF][START_REF] Lassen | Higher Order Operational Techniques in Semantics, chapter Relational reasoning about contexts[END_REF]. In this setting, the main subtlety lies in the fact that variables are only placeholders for values.

We fix some set of base types, ranged over by and define successively types, values and terms, typing contexts, well-typed terms, and transitions, as follows.

⇓ 1 ⇓ . 3 2 ⇓ 3 [ ↦ → ] ⇓
This calculus forms a transition monad as follows.

Placetakers and transition types As foreshadowed by the notation, because variables and values are indexed by (simple) types, we take P = S to be the set of types.

Placetaker monad The placetaker monad over Set P is given by well-typed values: given any Γ ∈ Set P , the placetaker object (Γ) ∈ Set P assigns to each type the set (Γ) of value typing derivations, i.e., the set of typing derivations with conclusion of the form Γ ⊢ : .

∈ Γ Γ ⊢ 1 : Γ ⊢ 1 : → Γ ⊢ 1 ′ : Γ ⊢ 1 ′ : • If Γ is a typing context, 1 ( (Γ))
is indeed the set of general typing derivations with variables in Γ.

Transition module Finally, the transition module maps any Γ ∈ Set P to the family, over all ∈ P, of transition proofs of some ⇓ with ∈ 1 ( (Γ)) and ∈ (Γ) . Such transition proofs are stable under value substitution, so we obtain a transition monad.

Remark 4.7.

. | → [ ↦ → ] . | ′ • → [ ↦ → ′ ]| .
Reduction may occur "everywhere", so it involves programs and stacks as well.

Let us show how this gives rise to a transition monad.

Placetaker types In the transition rules above, we see that placetakers may be programs or stacks. So, we take two placetaker types: P := 2 = {p, s}. A variables object is an element of Set P , that is, a pair of sets: the first one gives the available free program variables, and the second one the available free stack variables.

Placetaker monad The syntax may be viewed as a monad : Set P → Set P : given a variables object = ( p , s ) ∈ Set P , the placetaker object ( ( ) p , ( ) s ) ∈ Set P consists of the sets of program and stack terms with free variables in , up to bound variable renaming. As usual, monad multiplication is given by capture-avoiding substitution.

Transition types and state functors As mentioned above, transitions involve programs and stacks as well as commands. Thus, we take three transition types: S = 3 = {c, p, s}. Furthermore, commands are pairs of a program and a stack, so that, setting

1 ( ) = 2 ( ) = ( p × s , p , s ), we get ( ( )) = ( ( ) p × ( ) s , ( ) p , ( ) s ) for = 1, 2, as desired.
Transition module Finally, transitions with free variables in form a triple of graphs with vertices respectively in ( ) p × ( ) s (the set of commands taking free variables in ), ( ) p , and ( ) s . This family is natural in and commutes with substitution, hence forms a -module morphism, which completes our transition monad. 4.3. The -calculus. For an example involving equations on placetakers, let us recall the following standard presentation of (a simple variant of) the -calculus [START_REF] Sangiorgi | The -calculus -a theory of mobile processes[END_REF]. The syntax for processes is given by

, | 0 | ( | ) | . | ¯ . | ( ). ,
where ranges over process variables, and range over channel names, and is bound in . and ( ). . Processes are identified when related by the smallest context-closed equivalence relation

≡ satisfying 0| ≡ | ≡ | |( | ) ≡ ( | )| ( . )| ≡ .( | )
, where in the last equation should not occur free in . Transitions are then given by the following rules.

¯ . | ( ). -→ |( [ ↦ → ]) -→ | -→ | -→ . -→ .
Remark 4.8. Please note that there are no context rules for inputs or outputs, so that nothing happens under them.

The -calculus gives rise to a transition monad as follows.

Placetaker types We consider two placetaker types, one for channels and one for processes. Hence, P = 2 = {c, p}.

Placetaker monad Then, the syntax may be viewed as a monad : Set P → Set P : given a variables object = ( c , p ) ∈ Set P , the placetaker object ( ) = ( c , ( ) p ) ∈ Set P consists of the sets of channels and processes with free variables in (modulo ≡). Note that ( ) c = c as there is no operation on channels.

Transition type and state functors Transitions relate processes, so we take S = 1 and

1 ( ) = 2 ( ) = p .
Transition module Transitions are generated by the above three rules, and obviously stable under substitution. We thus obtain a transition monad.

Let us now describe a second way of organising the -calculus as a transition monad, this time over a single placetaker type. For this, we consider the same calculus, albeit without process variables, so that the syntax becomes

, : : = 0 | ( | ) | . | ¯ . | ( ). .
Placetaker In this variant of the -calculus, all that needs substitution is channels, so we set P = 1.

Placetaker monad Since the syntax contains no channel constructor, the placetaker monad is merely the identity monad.

Transition types and state functors However, since transitions relate processes, we need to fit the syntax into the state functors. We thus take S = 1 and 1 ( ) = 2 ( ) to be the set of processes with free channels in .

Transition module Transitions are generated as above, and stable under channel renaming, hence again form a transition monad.

Remark 4.9. Neither of our presentations would work in the presence of the mismatch operator [START_REF] Sangiorgi | The -calculus -a theory of mobile processes[END_REF]p13], which breaks stability of reduction under renaming. 4.4. Positive GSOS systems. An example involving labelled transitions is given by Positive GSOS systems [START_REF] Bloom | Bisimulation can't be traced[END_REF]p246]. They specify labelled transition systems, in which transitions have the shape -→ , where is drawn from some fixed set A of labels. Let us further fix a set of operations with arities in N and an infinite set of variables, ranged over by , ,... • for all ∈ , is a natural number, • the variables and , are all distinct, and • is an expression potentially depending on all the variables. A Positive GSOS system is a set of Positive GSOS rules.

The semantics of a Positive GSOS rule is that of a "rule scheme", in the following sense.

Definition 4.11. The labelled transition relation generated by a Positive GSOS system is the smallest A-labelled transition system on expressions generated by , such that for all rules (4.1), and expressions 1 , .

•

Remark 4.12. The general notion of GSOS system includes negative rules, which means rules that may have premises of the shape / . Their semantics is significantly more involved, so we leave their integration as an open problem. Each Positive GSOS system yields a transition monad as follows.

Placetaker and transition types We take P = 1, because we are in an untyped setting, and S = 1 because states are terms.

Placetaker monad

The selected family of operations (or rather arities) specifies the term monad .

State functors

In order to take labels into account, we take 1 ( ) = and 2 ( ) = A × . Transitions thus form a set over × (A × ) as desired.

Remark 4.13. We could as well take 1 ( ) = A × and 2 ( ) = , as ultimately only the product 1 ( ) × 2 ( ) matters.

Transition structure As before, we take as transitions the set of all proofs generated by the rules, which is indeed stable under substitution by construction. 4.5. The differential -calculus. Let us finally sketch how differential -calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF] provides a further example with 1 ≠ 2 . Following Vaux [START_REF] Vaux | calcul différentiel et logique classique : interactions calculatoires[END_REF]§6], its syntax may be defined by

, , | . | | • (terms) , 0 | + (multiterms),
where terms and multiterms are considered equivalent up to the following equations.

+ ′ + = ′ + + ( • ) • = ( • ) • .
The definition of transitions is based on two auxiliary constructions:

(1) Unary multiterm substitution [ ↦ → ] of a multiterm for a variable in a term , which returns a multiterm (not to be confused with unary monadic substitution, which handles the particular case where is a mere singleton).

(2) Partial derivative

• of a term w.r.t. a term variable along a multiterm . This again returns a multiterm.

Both are defined by induction on (see [Vau07, Definition 6.3 and 6.4]).

We may now define the transition relation as the smallest context-closed relation satisfying the rules below.

( . ) → [ ↦ → ] ( . ) • → . •
The compact formulation of the second rule relies on the abbreviation .( 1 + . . . + ) := . 1 + . . . + . . Let us now sketch how this forms a transition monad.

Placetaker monad Terms induce a monad on Set, which we take as the placetaker monad (hence P = 1).

State functors Transitions relate terms to multiterms, hence S = 1, 1 is the identity, and 2 = ! is the functor mapping any set to the set of (finite) multisets over . Transition structure Transitions are stable under substitution by terms, hence we again have a transition monad.

Signatures for transition monads

In the previous section, we have shown that several significant (abstract) programming languages may be organised as transition monads. We are now interested in specifying such languages by signatures. We first introduce registers, as announced in the introduction, and then our register for transition monads. 5.1. Signatures registers. In this section, we introduce signatures registers, which are a formalisation of the notion of signature, at least in the context of initial algebra semantics.

The idea is that each signature over a fixed category C should give rise to a particular category -alg, equipped with a "forgetful" functor to C, the specified object spec ( ) being the carrier of the initial object of -alg: Definition 5.1. An abstract signature over a category C consists of a category E with an initial object, equipped with a functor E → C. We denote by SemSig C the class of abstract signatures over C. Notation 5.2. We denote the components of any abstract signature over a category C by -alg and U , so that is precisely U : -alg → C. Accordingly, we call objects of -alg -algebras, or models of .

Definition 5.3. A register R for a given category C consists of • a class Sig R of signatures, and

• a semantics map -R : Sig R → SemSig C .
Terminology 5.4. We say that any ∈ Sig R is a signature for spec ( ) := U (0) (0 here denotes the initial object in -alg), or alternatively that specifies spec ( ). Finally, when we define our registers below, we first introduce signatures and associate a functor E → C to each signature. It then remains to prove that E has an initial object: as mentioned in §1, we call such proofs validity proofs.

Most of our registers will be monadic in the following sense.

Definition 5.5. A register R is monadic when the abstract signature E → C associated to any signature in Sig R is finitary and monadic.

Remark 5.6. Strictly speaking, we should call this "finitary monadic". We omit the "finitary" for readability.

Notation 5.7. When a register is monadic, we denote by ★ the monad induced by any signature , in the sense that we have an isomorphism -alg ★ -alg of categories over C (i.e., which commutes with forgetful functors). In such cases we have

★ (0 C ) spec ( ) = U (0 -alg ).
Let us now introduce a simple notion of morphism between registers.

Definition 5.8. A compilation from a register 1 on a category C to a register 2 on the same category is a map : Sig 1 → Sig 2 preserving the semantics up to isomorphism, in the sense that for any Σ ∈ Sig 1 , there is an isomorphism Σ 1 (Σ) 2 as objects of CAT/C. We say that 1 is a subregister of 2 if there exists a compilation of 1 to 2 .

Let us finish this subsection by recasting a well-known fact as the definition of a register. The well-known fact is the following. Proposition 5.9 [START_REF] Reiterman | A left adjoint construction related to free triples[END_REF]p62]. For any finitary endofunctor on a cocomplete category C, the forgetful functor -alg → C is monadic, and the left adjoint maps any object ∈ C to the initial algebra * ( ) of the functor ↦ → + ( ), i.e., the least fixed point .( + ( )), with -algebra structure given by

( * ( )) ↩→ + ( * ( )) * ( ).
And here comes the register:

Definition 5.10. For a given cocomplete category C, we define the monadic register EF C , called the endofunctor register, as follows.

Signatures: A signature is a finitary endofunctor on C. Semantics: The abstract signature associated to any finitary endofunctor is the forgetful functor : -alg → C.

Validity proof: By Proposition 5.9.

Remark 5.11. Let be any finitary endofunctor on a cocomplete category C. Please note the difference between ★ (0) and * (0): ★ (0) denotes the object specified by qua signature of EF C , while * (0) denotes the (carrier of the) initial -algebra. In this case, of course, the denotations coincide, but this will no longer be the case, for instance, in §7.3. There, ★ (0) will denote the initial -monoid, while * (0) will still denote the initial -algebra.

Let us conclude by naming all registers defined by compilation into EF C .

Definition 5.12. We call endofunctorial all subregisters of EF C .

5.2.

A register for transition monads. Our goal is to define a register for transition monads. Thus, we should at least organise them into a category in the first place:

Definition 5.13. For any sets P and S, finitary monad over Set P , and finitary functors

1 , 2 : Set P → Set S , let TransStruct P,S ( , 1 , 2 ) = -Mod (Set S )/ 1 × 2
denote the slice of the category of finitary, Set S -valued -modules over 1 × 2 . And for any sets P and S, we let TransMnd P,S := , 1 , 2 TransStruct P,S ( , 1 , 2 ).

Remark 5.14. Reduction monads [START_REF] Ahrens | Reduction monads and their signatures[END_REF] correspond to the case when 1 = 2 = Id, with P = S = 1, but contrary to the present work, morphisms there can live between reduction monads with different underlying monads. We don't need such morphisms in the present work because we enforce that models of a signature share the same underlying monad. This allows for a simpler notion of signature, at the cost of reducing the scope of the recursion principle.

In the coming sections, we will introduce • a register RegMnd (Set P ) for finitary monads on the category Set P , • a register Reg[Set P , Set S ] for finitary functors Set P → Set S , and • for any finitary monad and functors 1 and 2 , a register RegTransStruct P,S ( , 1 , 2 )

for transition structures over , 1 , and 2 . Assuming this is done, we may already give our register for transition monads:

Definition 5.15. We define the register RegTransMnd P,S for the category TransMnd P,S as follows.

Signatures: A signature, which we call a transition signature, consists of • a signature Σ of RegMnd (Set P ), specifying a finitary monad on Set P ,

• signatures Σ 1 and Σ 2 of Reg[Set P , Set S ] , specifying functors 1 , 2 : Set P → Set S , and • a signature Σ Trans of RegTransStruct P,S ( , 1 , 2 ). Semantics: The abstract signature associated to a signature

(Σ, Σ 1 , Σ 2 , Σ Trans ) is Σ Trans -alg U Σ Trans ------→ TransStruct P,S ( , 1 , 2 ) ↩→ TransMnd P,S .
Validity proof: We need to prove that Σ Trans -alg has an initial object; but this follows from RegTransStruct P,S ( , 1 , 2 ) being a register, which will be proved below.

It remains to introduce the registers RegMnd (Set P ) for monads, Reg[Set P , Set S ] for functors, and RegTransStruct P,S ( , 1 , 2 ) for transition structures. The most novel is clearly the latter. It is furthermore independent from the others, so we introduce it first.

For the reader's convenience, we list our registers in Figure 1, together with corresponding categories.

Registers for transition structures

In this section, we define the register RegTransStruct P,S ( , 1 , 2 ) for transition structures on fixed , 1 , 2 . Since these are Set S -valued -modules over 1 × 2 , this register should specify objects of the slice category -Mod (Set S )/ 1 × 2 . We will in fact design a register for more general slice categories C/ , where C is a locally finitely presentable category and an object of C. The desired register RegTransStruct P,S ( , 1 , 2 ) will then be obtained as an instance by taking C = -Mod and = 1 × 2 .

In §6.1, we first present a basic register Reg 0 (C/ ) that would work for the untyped case without variable binding. Then, in §6.2, we extend Reg 0 (C/ ) to a more powerful register Reg 1 (C/ ) that deals with variable binding. Observing that this register is slightly heavy to use in the typed setting, we design a more convenient variant, called Reg(C/ ). Finally, in §6.4, we focus on instances of this register to categories of the form C = -Mod /( Monoidal eq. systems Mon(C) 9.29 For R * , R is assumed to be an endofunctorial register (Definition 5.12).

Figure 1: Registers essentially as in usual operational semantics literature. Finally, in §6.5, we derive a register for the proof-irrelevant variant of transition monads.

6.1. Small register for slice categories. In this section, we introduce a first, limited register for slice categories.

Example 6.1. Let P denote the set of simple types over a given set of basic types, as in §4.1, and consider the arity for application, i.e., the endofunctor Σ app : Set P → Set P defined by

Σ app ( ) ( ) = ( → ) × ( ).
Across the equivalence Set P ≃ Set/P, one way of presenting this endofunctor, which is perhaps closer to the syntactic inference rule for application, is as the span

P 2 arr, 2 ←------P 2 1 --→ P,
where arr( , ) = ( → ). Indeed, Σ app ( ) corresponds to • taking the product of → P with itself in the arrow category,

• pulling back along arr, 2 , and • postcomposing with 1 .

To see this, let us observe that after pulling back, we obtain a family ′ over P 2 such that ′ ( , ) = ( → ) × ( ). Postcomposing, we take the disjoint union over as desired.

Generalising from this example, we obtain the following "small" register. Definition 6.2. For any locally finitely presentable category C and object ∈ C, we define the endofunctorial register Reg 0 (C/ ) for the slice category C/ as follows.

Signatures: A signature consists of:

• a metavariable object ;

• a list of premise morphisms ( -→ ) ∈ denoted by

ì - → ; • a conclusion morphism - → . Semantics: A model of a signature ( ì ← - - →
) is an algebra for the endofunctor mapping any -→ to ′ → -→ , where ′ → denotes the following pullback.

′ ì

Morphisms of models are morphisms of algebras.

Validity proof: All we have to show is that the induced endofunctor is finitary. But this functor is a composite of three functors

C/ (-) / ------→ C/ ì * -→ C/ ! -→ C/ ,
where • (-) / denotes -fold self-product in the arrow category,

• ì * denotes pullback along ì , and • ! denotes postcomposition with .

The last two functors, as left adjoints, are cocontinuous, hence finitary. Finally, the forgetful functor C/ → C creates colimits, so it suffices to show that the composite functor

C/ (-) / ------→ C/ → C is finitary. But this in turn is the composite of C/ → C (-)
---→ C. Because the first component creates, hence preserves all colimits, it suffices to show that (-) is finitary, which holds since filtered colimits commute with finite limits in locally finitely presentable categories [AR94, Proposition 1.59].

Example 6.3. Let P = 1 so that Set P Set, and denote the monad for pure -calculus syntax. Taking C = -Mod (Set) and the product module 2 = × , let us consider the left congruence rule for application -→ -→ as a signature of Reg 0 (C/ ). For this, we take • as metavariable module = 3 , • a single premise given by 1 , 2 : 3 → 2 , and • as conclusion the morphism : 3 → 2 mapping any ( , , ) to ( , ).

Let us now see what it means for a module morphism → 2 to be a model. In this case, the pullback along 1 , 2 yields × , and so a model structure amounts to a morphism × → making the following square commute.

× 2 × 2
Unfolding the definition, such a map associates to any transition ∈ ( ) over ( , ) ∈ 2 ( ) and term ∈ ( ) a transition over ( , , ) = ( , ), as desired.

6.2. Binding register for slice categories. In this section, we observe that the register Reg 0 (C/ ) is not expressive enough in the presence of variable binding, hence we refine it.

Example 6.4. Let P = 1 so that Set P Set, and denote the monad for pure -calculus syntax. Taking C = -Mod and = 2 as in Example 6.3, let us consider the -rule

→ . → . •
The natural metavariable module for this is (1) × (1) , because and have an additional, fresh variable, and the natural premise would be the identity map thereon. However, the register Reg 0 (C/ ) only allows premises to target powers of .

In order to rectify the situation, we refine Reg 0 (C/ ) to obtain the following more general register. Definition 6.5. For any locally finitely presentable category C and object ∈ C, we define the endofunctorial register Reg 1 (C/ ) for the slice category C/ as follows. Signatures: A signature consists of:

• a metavariable object ;

• a list of premise morphisms ( -→ ) ∈ , where each is a finitary endofunctor on C, denoted by • We first take as metavariable module := (1) × (1) , as planned.

• We then take as unique premise the identity on . For this we should justify that does have the desired form ( 2 ). This is the case with ( ) = (1) since ( 2 ) (1) = ( (1) ) 2 .

• Finally, we take as conclusion := (1) × (1) × ---→ × .

Remark 6.7. We may generalise this register to permit a conclusion between terms with additional free variables, by having the conclusion morphism target rather than , for some finitary right adjoint functor . For example, exploiting the adjunction -(1) ⊢ -× in the category of -modules [AHLM18, Proposition 13], the application of untyped -calculus can be viewed as an operation app : → (1) . Anticipating on §6.4, the corresponding modified -rule is app ( ( )) •

The point here is that for any set and ∈ (1) ( ), both terms app ( ( )) and lie in (1) ( ).

6.3. Typed variant. In this section, we observe that the medium register Reg 1 (C/ ) is slightly inconvenient in a typed setting, and propose our last register Reg(C/ ) for slice categories.

Example 6.8. As in §4.1, let P denote the set of simple types over a given set of ground types and : Set P → Set P denote the monad for simply-typed -calculus values. Furthermore, let us recall the first state functor 1 : Set P → Set P : 1 ( ) is the set of typed application binary trees with leaves in . Let us consider the -rule

1 ⇓ ( 3 ) 2 ⇓ 3 [ ] ⇓ 1 2 ⇓ •
Implicitly, this is in fact a family of rules indexed over all pairs ( , ) ∈ P 2 of types. For any such ( , ), we have 1 ∈ 1 ( ) → , 2 ∈ 2 ( ) , and 1 2 ∈ 1 ( ) . But these are all Set-valued modules, while the transition module → 1 × 2 is Set P -valued.

In order to work with Set-valued modules, we now want to introduce a refinement of the register Reg 1 (C/ ). Let us first sketch on this example how it should look like. First of all, because 1 2 and have type , we would like to replace the Set P -valued module 1 × 2 with the Set-valued ( 1 × 2 ) . We would then use as metavariable module the product

= ( 1 ) → × ( 1 ) × ( 1 ) ( ) × × ,
whose elements are tuples ( 1 , 2 , 3 , , ) as in the rule. The conclusion of our rule should then consist of a morphism → ( 1 × 2 ) , and similarly for the premises (see Example 6.11 below). The crucial ingredient here is the functor (-) : -Mod (Set S ) → -Mod (Set). Furthermore, in order to prove the existence of an initial model, it is important that this functor has a left adjoint (-) • y , as in Proposition 2.29.

Abstracting over this situation, we are led to: Definition 6.9. For any locally finitely presentable category C and object ∈ C, we define the endofunctorial register Reg(C/ ) for the slice category C/ as follows. Signatures: A signature, called a rule, consists of:

• a category D and a right adjoint : C → D;

• a metavariable object ∈ D; where the first functor denotes transposition, we obtain an endofunctor Σ , and define the abstract signature associated to to be the forgetful functor

Σ -alg → C/ .
Remark 6.10. Equivalently, a model is a morphism : → equipped with a map making the following triangle commute, ′ ( )

( ) Σ ( , ) ( )
and a morphism of models ( , ) → ( , ) is a morphism in C/ making the following square commute. Validity proof: The endofunctor Σ is obtained by composing Σ with (6.1), so it suffices to show that both of these functors are finitary. The composite (6.1) is in fact cocontinuous, because colimits in slice categories are computed on domains, and, on domains, (6.1) acts like the left adjoint .

Let us now consider the functor Σ . It is a composite of three functors, so it suffices to show that each of these functors is finitary. The last two, pullback along ì and postcomposition with , have right adjoints, hence are even cocontinuous. Finally, the first functor

C/ → D/ ( ), mapping any -→ to ( ) ( )
-------→ ( ) is finitary because colimits in slice categories are computed on domains, and, on domains, this functor acts like ↦ → ( ), which is a finite product of finitary functors -and filtered colimits commute with finite products in locally finitely presentable categories. Example 6.11. Let us now treat the big-step -rule, finishing Example 6.8. For any types and , we define the following rule: • we take D = -Mod (Set) and : -Mod (Set S ) → -Mod (Set) to be pointwise evaluation at , which is indeed right adjoint to (-) • y (Proposition 2.29); • we further take := ( 1 ) → × ( 1 ) × ( 1 ) ( ) × × as metavariable object; • we have three premises → 1 × 2 , which, at any ∈ Set P , respectively map any

( 1 , 2 , 2 , , ) ∈ ( ) to: -( 1 , , ( 3 )), -( 2 , ), and -( 3 [ ], ); • the conclusion maps any such ( 1 , 2 , 2 , , ) ∈ ( ) to (app , ( 1 , 2 ), ).
Using the notation of §6.4 below, this will look much like the standard, syntactic rule. Definition 6.12. Let RegTransStruct 0 P,S ( , 1 , 2 ) = Reg( -Mod (Set S )/ 1 × 2 ). Finally, we would like signatures to consist of families of rules. For this, we use the following generic construction of registers. Definition 6.13. For any endofunctorial register R for a category with coproducts, we denote by R * the endofunctorial register whose signatures are families of signatures in Sig R , and whose semantics maps any family to the coproduct of associated endofunctors.

We may at last define our register for the category TransStruct P,S ( , 1 , 2 ) of transition structures, which we recall is by definition the slice category -Mod (Set S )/ 1 × 2 . For this, we take as signatures all families of signatures in RegTransStruct 0 P,S ( , 1 , 2 ): Definition 6.14. Let RegTransStruct P,S ( , 1 , 2 ) = RegTransStruct 0 P,S ( , 1 , 2 ) * .

6.4.

A format for displaying signatures in rule-based registers. In all of our examples of signatures in RegTransStruct 0 P,S ( , 1 , 2 ), the metavariable object is a functor to Set, so the premises and conclusion are set-maps (which are in fact module morphisms). In this case, we adopt the following notational conventions.

• For each premise or conclusion → ↦ → of a rule, we write : ⊢ : .

• Furthermore, we organise the premises and conclusion as usual:

: Remark 6.16. The module is often a product and thus is a tuple. Remark 6.17 [START_REF] Ahrens | Reduction monads and their signatures[END_REF]. In practice, there are several choices for building the transition rule out of such a schematic presentation, depending on the order of metavariables. This order is irrelevant: all interpretations yield isomorphic semantics, in the obvious sense. Remark 6.18. This format could be generalised to any metavariable object, by using the internal language of categories. 6.5. Proof-irrelevant variant. In this section, we introduce a register for the proofirrelevant variant of transition monads. The idea is very simple: we keep the same signatures as in the proof-relevant setting, and interpret each signature in a proof-irrelevant way. This is done by constructing a functor from proof-relevant transition monads to proof-irrelevant ones.

Proposition 6.19. Let ITransStruct P,S ( , 1 , 2 ) denote the full subcategory of transition structures src, tgt :

→ 1 × 2 such that src, tgt is a pointwise inclusion. Then, the embedding , 1 , 2 : ITransStruct P,S ( , 1 , 2 ) ↩→ TransStruct P,S ( , 1 , 2 ) is reflective. Consequently, letting ITransMnd P,S := , 1 , 2 ITransStruct P,S ( , 1 , 2 ), the induced embedding ITransMnd P,S ↩→ TransMnd P,S is also reflective.

Proof. Refining Remark 3.8, by [Ahr15, Definition 2.71], the category of finitary -modules is a category of presheaves on a small category. Thus, by [Bor94b, Example 4.3.10.g], all epimorphisms are strong. Furthermore, by [START_REF] Borceux | Handbook of Categorical Algebra, volume 1 of Encyclopedia of Mathematics and its Applications[END_REF]Proposition 4.4.3], it admits (strong epi)-mono factorisations.

Using this, we define the left adjoint

: TransStruct P,S ( , 1 , 2 ) → ITransStruct P,S ( , 1 , 2 )
to map a transition structure : → 1 × 2 to the monomorphism ↩→ 1 × 2 obtained from the (strong epi)-mono factorisation of . Then, the natural bijection

TransStruct P,S ( , 1 , 2 ) ( 1 ,
2 ) ≃ ITransStruct P,S ( , 1 , 2 ) ( 1 , 2 ) follows from the lifting property of strong epimorphisms.

Let us now introduce the relevant register. For this, we first observe that postcomposition with a functor : C → D turns a register for C into one for D. Definition 6.20 (Post-composition register). For any functor : C → D and register R on C, let ! (R) denote the register for D with Sig ! (R) = Sig R and ! (R) = • R . Definition 6.21. The register RegITransMnd P,S is defined as ! (RegTransMnd P,S ), where : TransMnd P,S → ITransMnd P,S denotes the reflection.

Registers for monads

In this section and the next, we design the missing registers, respectively for monads and state functors. The registers are mostly adapted from existing constructions and results in the literature [AHLM19, FPT99, Fio08, FH09]. The novelty here lies in our new explicit description of initial algebras. The basic idea for specifying operations in our register for monads is that the arity of an operation consists of • an "input" (Set-valued) parametric module, in the sense of §2.4.2, together with • an "output" placetaker type ∈ P. The role of parametric modules lies in specifying how capture-avoiding substitution should interact with operations. A similar role is played in [START_REF] Fiore | Abstract syntax and variable binding[END_REF][START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF] by "pointed strong" endofunctors; we explain the connection in §9.2.

In §7.1, we construct a first register RegMnd 0 (Set P ), which only allows to specify operations. We then deal with equations in §7.2. Finally, we characterise initial algebras in §7.3. All proofs are deferred to §10.

7.1. The register RegMnd 0 (Set P ) for specifying operations. This section is devoted to defining the monadic register RegMnd 0 (Set P ).

Signatures will rely on parametric modules, but these need to be restricted in order to ensure existence of an initial algebra (and even monadicity).

Proposition 7.1. For any set P, 1 , . . . , ∈ P, and finitary functor : Set P → Set, the assignment , ↦ → ( ( + ∈ y )) defines a parametric module denoted by ( • Θ) ( 1 ,..., ) . Proof. By Example 2.28. Definition 7.2. A parametric module is elementary if it is isomorphic to some finite product of parametric modules of the shape ( • Θ) ( 1 ,..., ) .

Example 7.3. Typically, taking ( ) = ( ), any finite product of parametric modules of the shape Θ ( 1 ,..., ) , for some , 1 , . . . , ∈ P, is elementary.

Example 7.4. Recall that the idea of our register is that an operation will be specified by two parametric modules, one for the source and another (very simple) for the target.

× Θ s ) ( ) ( ) = ( ) p × ( ) s .
Definition 7.5. Given any set P, a modular signature is a family of pairs ( , ) where

• is an elementary parametric module, and

• ∈ P.
Given any modular signature = ( , ) ∈ , an -algebra is a finitary monad equipped with -module morphisms ( ) → for all ∈ . An -algebra morphism is a monad morphism commuting with these morphisms. We denote by -alg → Mnd (Set P ) the forgetful functor. Definition 7.6. We define the monadic register RegMnd 0 (Set P ) for Mnd (Set P ) as follows, for any set P. Signatures: A signature is a modular signature.

Semantics:

The abstract signature associated to any signature is the forgetful functor -alg → Mnd (Set P ).

Validity proof: By Corollary 10.21 below.

7.2. The register RegMnd (Set P ). We now define our register RegMnd (Set P ), where a signature will consist of a signature of RegMnd 0 (Set P ), plus a family of "equations". An equation is essentially a pair of "derived operations" with a common "arity". The arity consists of an input arity, which intuitively models the metavariables of the equation, and an output arity, which models the output type. The input arity will be an elementary parametric module , and the output arity will be a placetaker type ∈ P. For a family of equations, the arity thus is a family of such pairs ( , ) i.e., a modular signature. An equation will then consist of two derived operations with the same arity, in the following sense.

Definition 7.7. Given any modular signatures and ′ , an -derived operation of arity ′ is a functor : -alg → ′ -alg over Mnd (Set P ), i.e., making the following triangle commute.

-alg ′ -alg

Mnd (Set P )
We call operations of basic, by contrast with the derived operations of ′ . More concretely, we may introduce derived operations in two stages, as follows: • an -module morphism → between parametric modules and is a natural family of morphisms ( : ( ) -→ ( )) ∈ -alg , such that is a -module morphism, for each -algebra ;

• letting ′ = ( , ) ∈ , an -derived operation of arity ′ is a family of parametric module morphisms → Θ , for all ∈ .

Remark 7.8. Concretely, an -derived operation of arity ′ associates to each -algebra a family of -module morphisms ( ) → , naturally in . Equivalently, by Proposition 2.29, an -derived operation of arity ′ associates to each a single, Set P -valued -module morphism H ′ ( ) → , where H ′ ( ) := Returning to the general case, we now define our notion of signature for monads.

Definition 7.10. An equational modular signature consists of • a modular signature called the modular signature for operations, or the operations modular signature,

• a modular signature ′ called the modular signature for equations, or the equations modular signature, together with • a pair of -derived operations of arity ′ . For any equational modular signature = ( , ′ , , ), an -algebra is an -algebra such that the ′ -algebra structures ( ) and ( ) coincide, i.e., ( ) = ( ). A morphism of -algebras is a morphism of -algebras. We let -alg denote the category of -algebras and morphisms between them.

Let us at last define our register.

Definition 7.11. We define the monadic register RegMnd (Set P ) for Mnd (Set P ) as follows, for any set P. Signatures: A signature is an equational modular signature. Semantics: The abstract signature associated to any equational modular signature is the forgetful functor -alg → Mnd (Set P ).

Validity proof: This is Corollary 10.24(i) below.

Let us conclude this subsection by introducing some convenient notation for specifying equations.

Notation 7.12 (Format for equations). We write any equational modular signature whose equations modular signature is a singleton ′ = ( , ), say with derived operations given by → Θ 2 ↦ → ( , ), as : ⊢ ≡ : Θ (leaving the operations modular signature implicit), or even just ≡ when the rest may be inferred. Furthermore, given any common (implicit) operations modular signature , any family ( : ⊢ ≡ : Θ ) ∈ will accordingly denote the equational modular signature • whose equations modular signature is ′ = ( , ) ∈ , and • whose -derived operations of arity ′ are given at any -algebra by the morphisms ( ) : ( ) → and ( ) : ( ) → , for each ∈ .

Example 7.13. We write associativity from Example 7.9 as just par( , par( , )) ≡ par(par( , ), ).

In this case, the argument is the triple ( , , ).

Explicit description of initial algebras.

In this final subsection, we provide an explicit description of the initial -algebra, for any equational modular signature . We first deal with the case without equations, recalling the standard identification of the initial -algebra as a free algebra for a suitable endofunctor. In the presence of equations, we then characterise the initial -algebra as a coequaliser of free algebras.

In order to compute the initial algebra for a modular signature , we first observe that the induced homogeneous parametric module H in fact comes from an endofunctor. Definition 7.14. For any modular signature , we define its associated endofunctor Σ on [Set P , Set P ] as follows.

• For any elementary = ( • Θ) ( 1 ,..., ) and ∈ P, let

Σ ( , ) ( ) = ( • ) ( 1 ,..., ) • y .
• For a family = ( , ), let Σ = ∈ Σ ( , ) . Explicitly, we have for any ( , ):

Σ ( , ) ( ) ( ) := ( ( ( + y ))) • y .
In perhaps more elementary terms, we have

Σ ( , ) ( ) ( ) ( ) = ( ( + y )) Σ ( , ) ( ) ( ) ( ′ ) = ∅ for ′ ≠ .
By construction, we have:

Proposition 7.15. For any modular signature , the following square commute,

Mnd (Set P ) Mod(Set P , Set P ) [Set P , Set P ] [Set P , Set P ] H Σ
where the right-hand functor maps any pair ( , ) to .

Let us now turn to the explicit description of the initial -algebra. The mathematical contents essentially date back to [START_REF] Fiore | Abstract syntax and variable binding[END_REF].

Proposition 7.16. For any modular signature , the forgetful functor -alg → Mnd (Set P ) is monadic, and furthermore the free Σ -algebra Σ * (id) on the identity has a canonicalalgebra structure, which is initial.

Proof. This is Corollary 10.21 below.

We now seek an explicit description of the initial -algebra, for any equational modular signature .

Definition 7.17. Let = ( , ′ , , ) denote any equational modular signature, with = ( , ) ∈ and ′ = ( , ) ∈ .

• Let + ′ denote the "disjoint union", i.e., the modular signature ( , ) ∈ , where

-= + , -( , ) is * ( , ) if = 1 ( ) and * ( , ) if = 2 ( ).
• The ′ -algebra structures given by (spec ( )) and (spec ( )) on spec ( ), together with its canonical -algebra structure, yield two ( + ′ )-algebra structures. By initiality of spec ( + ′ ), we thus obtain two ( + ′ )-algebra morphisms ˇ , ˇ : spec ( + ′ ) → spec ( ),

or equivalently, by Proposition 7.16, ˇ , ˇ :

(Σ + Σ ′ ) * (id) → Σ * (id). (7.2)
Theorem 7.18. For any equational modular signature = ( , ′ , , ), the coequaliser of the pair ˇ , ˇ : (Σ + Σ ′ ) * (id) → Σ * (id) in [Set P , Set P ] admits a unique -algebra structure such that the coequalising morphism is an -algebra morphism. Furthermore, this structure is in fact an -algebra structure. Finally, it makes the coequaliser into an initial -algebra.

Proof. By Corollary 10.24 below.

Remark 7.19.

• The coequaliser may be computed as a pointwise quotient of Σ * (id), as follows. As explained by Hamana [START_REF] Hamana | Free Σ-monoids: A higher-order syntax with metavariables[END_REF], Σ * (id) may be defined as a term language, each Σ * (id) ( ) ( ) being the set of terms of type , with free variables of each type ∈ P in ( ) -as in §4.1, the pair ( , ) may be thought of as a sequent ⊢ . Now, coequalisers (as all limits and colimits) are pointwise in functor categories [Mac98, §V.4], so for any ∈ Set P and ∈ P, spec ( ) ( ) ( ) is the coequaliser of

(Σ + Σ ′ ) * (id) ( ) ( ) → Σ * (id) ( ) ( ) in Set.
And this is well known to be the quotient of Σ * (id) ( ) ( ) by the smallest equivalence relation identifying all ˇ , ( ) with ˇ , ( ), for all ∈ (Σ + Σ ′ ) * (id) ( ) ( ).

Intuitively, following Hamana again, (Σ + Σ ′ ) * (id) is an extension of the term language Σ * (id) with operations, say , with arities ( , ), for all (where ′ = ( , ) ∈ as before), and ˇ and ˇ inductively translate this language to Σ * (id) by interpreting using (Σ * (id)) and (Σ * (id)), respectively. • We could consider computing the coequaliser of a simpler parallel pair spec ( ′ ) → spec ( ), (7.3) constructed similarly. Let us show on a simple example that this does not compute the desired functor. The intuition is that this coequaliser identifies terms modulo a relation which is not a congruence. Let P = 1, and consist of a single, binary operation, i.e., = {(Θ 2 , ★)}. Thus, an -algebra is merely a monad on sets, equipped with a binary -module morphism : 2 → . Furthermore, let ′ consist of a single, ternary operation . Finally, for any -algebra ( , ), let ( ) and ( ) denote the -module morphisms

3 × ---→ 2 -→ 3 × ---→ 2 -→ .
By Proposition 7.16, for any set , spec ( ) ( ) consists of binary trees with leaves in . Similarly, spec ( ′ ) ( ) consists of ternary trees with leaves in . Now, the parallel pair (7.3) maps ternary trees to binary trees, replacing any ternary node ( 1 , 2 , 3 ), respectively with (( 1 , 2 ), 3 ) and ( 1 , ( 2 , 3 )). Thus, e.g., assuming ∈ , the binary trees ((( , ), ), ) and (( , ( , )), ), having an even number of leaves, are not in the image of the parallel pair, hence are not identified in the coequaliser.

• A perhaps higher-level understanding of this, which will be developped in §10, is as follows.

The derived operations induce monad morphisms ( ′ ) ★ → ★ , of which the desired monad ★ is the coequaliser in Mnd (Set P ). However, coequalisers of monads are generally not pointwise [START_REF] Adámek | Coproducts of monads on set[END_REF]. Fortunately, reflexive coequalisers are, so the desired monad may be computed as the pointwise coequaliser of the obvious parallel pair ★ + ( ′ ) ★ → ★ . Finally, roughly because (-) ★ is a left adjoint in this case, we have ★ + ( ′ ) ★ ( + ′ ) ★ , which directly leads to our formula.

Registers for (state) functors

In this section, we define a register Reg[Set P , Set S ] , which is a variant of RegMnd (Set P ) for the case of state functors. Operations, equations, and models will be defined exactly as for monads, and a signature in Reg[Set P , Set S ] will again consist of families of operations and equations, the only difference being that instead of parametric modules, we will use facets. We start by presenting the auxiliary notion of facets, which is a simple variant of the parametric modules of §7. Next, we introduce a register Reg 0 [Set P , Set S ] for operations, and then a refinement Reg[Set P , Set S ] with equations. Again, validity proofs are deferred to §10.

8.1. Facets. We start in this section by introducing facets. Let us first explain how they naturally come up in the case of call-by-value, simply-typed -calculus. We have seen in §4.1 that the source state functor 1 for call-by-value, simply-typed -calculus consists of application binary trees. The goal now is to design a register for specifying such a functor 1 . Intuitively, it has two (type-indexed families of) operations: • a first operation for injecting values into application binary trees, of type → 1 ( ) for all ∈ Set P and ∈ P, and • a second operation for application, of type 1 ( ) → × 1 ( ) → 1 ( ) , for all ∈ Set P and , ∈ P. The type for application is really similar to what we had in §7: for any type ∈ P, denoting by Θ : [Set P , Set P ] → [Set P , Set] the functor defined by Θ ( ) ( ) = ( ) , application of a function of type → has arity

Θ → × Θ → Θ .
The type for value injection does not make any sense in the context of modules over monads, because the functor ( ) ( ) = does not form a module. But here in the context of state functors, we may well define I : • For any facets and , the product × in the (functor) category of facets is again a facet. • For any ∈ P, let Θ = Φ ev .

• For any ∈ S, let I = Ψ ev .

• For any facet for [Set P , Set S ] and 1 , . . . , ∈ P, let ( 1 ,..., ) ( ) ( ) = ( ( + y 1 + . . . + y )).

Remark 8.4. Let Θ denote the identity endofunctor on [Set P , Set S ] , and

I : [Set P , Set S ] → [Set P , Set P ]
the constant functor mapping anything to the identity endofunctor. Post-composing with evaluation at any ∈ P, resp. ∈ S, we recover the facets I and Θ .

Remark 8.5. The notation Θ introduced above for the identity endofunctor is compatible with the one denoting the parametric module mapping a monad on Set P to as a module over itself (Example 2.28) in the sense that, for example, the functor underlying the module coincides with the functor underlying the monad .

Example 8.6. The arities for application binary trees will be given by I → Θ and Θ → × Θ → Θ , for all types and .

8.2. The register Reg 0 [Set P , Set S ] for specifying operations. In order to adapt the notion of signature for operations from RegMnd 0 (Set P ), we merely need to adapt the notion of elementariness, which becomes the following:

Definition 8.7. A facet for [Set P , Set S ] is elementary if it is isomorphic to some finite product of facets of the shape ( • I, Θ ) ( 1 ,..., ) for some 1 , . . . , ∈ P and finitary functor : Set P × Set S → Set.

Remark 8.8. The notation ( • I, Θ ) ( 1 ,..., ) deserves some explanation. We have I : [Set P , Set S ] → [Set P , Set P ] and Θ : [Set P , Set S ] → [Set P , Set S ], and we mean

( • I, Θ ) ( 1 ,..., ) ( ) ( ) := ( , ( )).
Example 8.9. Typically, any product of facets of the shape I ( 1 ,..., ) or Θ ( 1 ,..., ) , for some , 1 , . . . , ∈ P and ∈ S, is elementary.

Definition 8.10. A facet-based signature is a family of pairs ( , ) consisting of an elementary facet and a transition type ∈ S.

Definition 8.11. For any facet-based signature = ( , ) ∈ , an -algebra is a finitary functor : Set P → Set S , equipped with natural transformations ( ) → Θ ( ) for all ∈ . A morphism of -algebras is a natural transformation commuting with these morphisms. Let -alg denote the category of -algebras, and : -alg → [Set P , Set S ] the forgetful functor.

Definition 8.12. For any sets P and S, we define the monadic register Reg 0 [Set P , Set S ] as follows. -alg ′ -alg

[Set P , Set S ]
We call basic the operations of , by contrast with the derived operations of ′ . More concretely, as in Definition 7.7, we may introduce derived operations in two stages, as follows:

• an -facet morphism → between facets and is a natural family of natural transformations ( : ( ) -→ ( )) ∈ -alg ;

• letting ′ = ( , ) ∈ , an -derived operation of arity ′ is a family of -facet morphisms → Θ , for all ∈ .

Remark 8.14. Concretely, an -derived operation of arity ′ associates to each -algebra a family of -facet morphisms ( ) → , naturally in . For any equational facet-based signature = ( , ′ , , ), an -algebra is an -algebra such that the ′ -algebra structures ( ) and ( ) coincide, i.e., ( ) = ( ). A morphism of -algebras is a morphism of -algebras. We let -alg denote the category of -algebras and morphisms between them.

( ) = 2 ( ) = ( p × s , p , s ) -|-: I p × I s → Θ c p : I p → Θ p s : I s → Θ s 1 ( ) = 2 ( ) = p I p → Θ Call-by-value, simply-typed 2 ( ) = : I → Θ (for all ) Positive GSOS specifications 1 ( ) = I → Θ 2 ( ) = A × A × I → Θ Notation 8.18.
In examples, we will present equational facet-based signatures as families of equations. For this, we will use Notation 7.12, which extends to facet-based equations. E.g., Example 7.13 applies verbatim for associativity of multiset union in the target state functor for differential -calculus.

8.4. Explicit description of initial algebras. In this section, we state monadicity of the register Reg[Set P , Set S ] of equational facet-based signatures, and give our explicit description of initial algebras. We first deal with facet-based signatures , identifying the initial -algebra as a free algebra for a suitable endofunctor. We then characterise the initial -algebra as a coequaliser of free algebras, for any equational facet-based signature .

Definition 8.19. For any facet-based signature , we define its associated endofunctor Σ on [Set P , Set S ] as follows.

• For any elementary = ( • I, Θ ) ( 1 ,..., ) and ∈ S, let

Σ ( , ) ( ) = ( • id, ) ( 1 ,..., ) • y .
• For a family = ( , ), let Σ := ∈ Σ ( , ) .

Remark 8.20. Explicitly, we have for any ( , ):

Σ ( , ) ( ) ( ) := ( ( + y , ( + y ))) • y .
Proposition 8.21. For any facet-based signature , the forgetful functor : -alg → [Set P , Set S ] is monadic. Furthermore, the free -algebra on a functor ∈ [Set P , Set S ] is the free Σ -algebra Σ * ( ), as characterised in Proposition 5.9.

Proof. A direct consequence of Proposition 10.25 below.

We now want to characterise the initial -algebra, for any equational facet-based signature . The development closely follows §7.3. Definition 8.22. Let = ( , ′ , , ) denote any equational facet-based signature, with = ( , ) ∈ and ′ = ( , ) ∈ .

• Let + ′ denote the "disjoint union", i.e., the facet-based signature ( , ) ∈ , where

-= + , -( , ) is * ( , ) if = 1 ( ) and * ( , ) if = 2 ( ).
• The ′ -algebra structures given by (spec ( )) and (spec ( )) on spec ( ), together with its canonical -algebra structure, yield two ( + ′ )-algebra structures. By initiality of spec ( + ′ ), we thus obtain two ( + ′ )-algebra morphisms ˇ , ˇ : spec ( + ′ ) → spec ( ).

(8.1)

Theorem 8.23. For any equational facet-based signature = ( , ′ , , ), the coequaliser of the pair ˇ , ˇ : spec ( + ′ ) → spec ( ) in [Set P , Set S ] admits a unique -algebra structure such that the coequalising morphism is an -algebra morphism. Furthermore, this structure is in fact an -algebra structure. Finally, it makes the coequaliser into an initial -algebra.

General registers

We have now introduced all the needed registers for our register RegTransMnd P,S of Definition 5.15 to make sense, including two registers featuring equations, respectively for monads (Definition 7.11) and functors (Definition 8.16). In this section, in preparation for the missing validity proofs and the announced explicit descriptions of initial algebras, we introduce a fundamental register featuring equations, for a general category, ES C , whose signatures are Fiore and Hur's equational systems [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]. In order to deal more specifically with monads, we then introduce a second register, PSEF C , based on Fiore, Plotkin, and Turi's pointed strong endofunctors, which incorporates variable binding and substitution. We then "merge" both registers into a single register MES C , suited for syntax with variable binding, substitution, and equations. Proofs are again deferred to §10. 9.1. Equational systems. A general device for constructing monadic functors is Fiore and Hur's equational systems [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]. In this section, we view equational systems on a category C as the signatures of a register ES C for C, called the equational register, which refines with equations the endofunctorial register EF C (see Definition 5.10).

Briefly, an equational system consists of two parts: • an endofunctor Σ on C, which intuitively specifies operations, • and equations.

We present them in a slightly non-standard way, and make the link with the original in Propositions 9.5 and 9.8 below.

Definition 9.1. For any endofunctor Γ and monad on a category C, a functorial -term of arity Γ is a natural transformation Γ → .

Example 9.2. Let us consider the finitary endofunctor Σ on sets defined by Σ( ) = 2 , so that Σ * ( ) denotes the set of binary trees with leaves in , as generated by the following grammar, , | op( , )

where ranges over . Since Σ-algebras are sets equipped with a binary operation, a natural equation to impose on them is associativity. Taking Γ( ) = 3 , the relevant functorial Σ *terms and of arity Γ are defined by ( 1 , 2 , 3 ) = op(op( 1 , 2 ), 3 ), and

( 1 , 2 , 3 ) = op( 1 , op( 2 , 3 )).
Example 9.3. We will do this right in Example 9.26 below, but for illustrative purposes, let us describe a failed attempt at specifying pure -terms modulo by an equational system. We first take C = [Set, Set] to consist of finitary endofunctors on sets, and Σ( ) ( ) = + ( ) 2 + ( + 1). The first summand models variables, the second application, and the third, abstraction. Indeed, any algebra comes equipped with maps app : ( ) 2 → ( ) and : ( + 1) → ( ), for all . The first member of the -equation, app ( ( ), ), would be modelled by setting Γ( ) ( ) = ( +1)× ( ) and taking the natural transformation Γ → Σ * mapping any ( , ) ∈ ( + 1) × ( ) to app ( ( ), ) (omitting the monad unit : id → Σ * ). This works fine, but we have neglected to build substitution into the model, so we cannot define the right-hand side of . This will be rectified in Example 9.26, after observing that (part of) Σ is in fact pointed strong in Example 9.15.

The following should now look natural. Remark 9.6. The expert will have noticed that Fiore and Hur's equational systems use (iii), in a slightly more general setting: they do not assume C to be locally finitely presentable, nor Σ and Γ to be finitary.

Let us now define the models of an equational system. Definition 9.7. For any equational system E = (C : Γ ⊢ = : Σ), an E-algebra is a Σ-algebra whose induced Σ * -algebra structure coequalises

, : Γ( ) ⇒ Σ * ( ).
Let E -alg denote the category of E-algebras, with Σ-algebra morphisms between them, and let E : E -alg → C denote the forgetful functor.

Let us readily transfer this definition across the various correspondences of Proposition 9.5. Remark 9.9. The equivalence of (a) and (c) entails that our notion of algebra coincides with Fiore and Hur's (apart from the differences noted in Remark 9.6).

Remark 9.10. Families ( = ) of equations are covered by taking the coproduct of all involved endofunctors, say Γ , and the pointwise copairing of functorial terms. Definition 9.11. For a given locally finitely presentable category C, we define the monadic register ES C , called the equational register, as follows. Signatures: A signature is an equational system. Semantics: The abstract signature associated to any signature E is the forgetful functor E -alg → C.

Validity proof: By Theorem 10.14 below.

Example 9.12. Given a cocomplete category C, the endofunctor register EF C is a subregister of ES C , by mapping any finitary endofunctor Σ to the (finitary) equational system given by taking Γ = 0, and the unique and . 9.2. The register PSEF C for monoids. In the previous subsection, we reviewed a fundamental register available for general locally finitely presentable categories. Here, we review another fundamental register called PSEF C , available for the category of monoids in a convenient monoidal category. This register is essentially due to Fiore, Plotkin, and Turi [START_REF] Fiore | Abstract syntax and variable binding[END_REF]. Signatures in the register PSEF C will be pointed strong endofunctors on the monoidal category C. The point of the register PSEF C is to specify monads. In fact, monads may be specified by the previous register, ES C , but at the cost of including in the signature • operations for the monad multiplication and unit, and • equations for associativity and unitality. Instead, the register PSEF C will directly specify monoids in any (sufficiently nice) monoidal category C, hence be more economical. This in particular covers the case of finitary monads on a locally finitely presentable category.

Let us first describe the announced monadic abstract signature. We start by recalling what a pointed strong endofunctor is, and showing how it yields a parametric module (in the sense of Definition 2.15) on C.

Pointed strong endofunctors -→ ( )

( 1 ) -----→ ( + 1) and 1

( ) 1 ----→ (1) ( 2 )
-----→ ( + 1). We use this in defining the pointed strength to map any 2 ( )( ), where ∈ ( + 1) and : → ( ), to 2 ( ( ↑ )). This will ensure the usual equation ( ) [ ] = ( [ ↑ ]).

The parametric module Σ stmod Let us now show how every pointed strong endofunctor induces a parametric module.

Definition 9.16. We define the parametric module Σ stmod on C as assigning to any monoid ∈ C, the object Σ( ), equipped with the action given by the composite

Σ( ) ⊗ → Σ( ⊗ ) → Σ( ).
The verification that this assignment indeed defines a parametric module is straightforward.

The category Σ -Mon of models We now introduce Σ-monoids. These are exactly the classical Σ-monoids, which we present from a point of view better suited to our purpose. They are monoids equipped with a "compatible" algebra structure: Definition 9.17. A Σ-monoid is a monoid , equipped with an -module morphism : Σ stmod ( ) → . A Σ-monoid morphism is a monoid morphism : → making the following square commute.

Σ stmod ( ) Σ stmod ( ) Σ stmod ( )
We let Σ -Mon denote the category of Σ-monoids and morphisms between them, while Σ : Σ -Mon → Mon(C) denotes the obvious forgetful functor.

Let us first prove that this agrees with the standard definition.

Proposition 9.18. The category Σ -Mon is isomorphic over Mon(C) to the following category.

• Objects are monoids equipped with Σ-algebra structure : Proof. By definition of Σ stmod , it is equivalent for a morphism Σ( ) → to be an -module morphism, and for the condition (9.1) to hold.

Σ( ) → making the diagram Σ( ) ⊗ Σ( ⊗ ) Σ( ) ⊗ , ⊗ Σ
Let us finally check that we have defined an abstract signature.

Theorem 9.19. For any finitary, pointed strong endofunctor on a convenient monoidal category C, the category Σ -Mon and the forgetful functor Σ : Σ -Mon → Mon(C) form a monadic abstract signature. In fact, the forgetful functor Σ : Σ -Mon → Mon(C) is finitary monadic.

Proof. We have a commuting triangle

Σ -Mon Mon(C) C, Σ U Σ -Mon U Mon(C)
where, by [FH09, §7.2], U Σ -Mon and U Mon(C) are both monadic, the corresponding monads being finitary (noting that Mon(C) 0 -Mon). By [AR94, Remark 2.78] with = , it follows that all three categories are locally finitely presentable, hence in particular cocomplete. The result thus follows by Proposition 2.40 and Lemma 2.41.

We now want to recall a standard characterisation of the monad induced by the monadic functor Σ -Mon , but before that let us fix some notation. Notation 9.20. Let us refine Notation 5.7 and Remark 5.11. For a pointed strong endofunctor Σ on a convenient monoidal category C, Σ ★ (0) might be read as different objects of C, according to whether Σ is viewed as a finitary endofunctor or a finitary pointed strong endofunctor. Since Σ-monoids are also monadic over monoids, it might even be understood as a monoid in C. We choose the following convention: • Σ ★ denotes the "free Σ-monoid" monad C, • Σ ⊛ denotes the "free Σ-monoid" monad on Mon(C), • Σ * denotes the "free Σ-algebra" monad on C. Proposition 9.21. For any pointed strong endofunctor Σ on a convenient monoidal category C, the monad Σ ★ induced by the right adjoint functor Σ -Mon → Mon(C) → C maps any object ∈ C to .( + Σ( ) + ⊗ ). As a consequence of Proposition 5.9, the carrier Σ ★ (0) of the initial Σ-monoid is then isomorphic to Σ * ( ).

Proof. This is more or less known since [FPT99, FH09, FS17], see [BHL20, Theorem 2.15] for an explicit, complete, yet slightly more general statement.

Let us finally define our register for monoids. • Given any : -alg → Γ -Mon over Mon(C), consider the morphism ↓ : Γ stmod → monmod defined at any monoid by

Γ( ) Γ( ) -----→ Γ( ( )) ( ( )) -------→ ( ).
This indeed defines a morphism of the claimed type, by a simple diagram chasing, and furthermore this assignment is clearly natural in Γ and . • Conversely, given any : Γ stmod → monmod , let ↑ : -alg → Γ -Mon map any -algebra structure : ( ) → on a monoid to the Γ-algebra structure Γ( ) ---→ ( ) -→ .

Again, a simple diagram chase shows that this Γ-algebra structure satisfies the coherence law of Γ-monoids.

These two maps are easily checked to be mutually inverse, thus proving the claim.

1 ( 1 (0)) 1 ( 2 (0)) 1 ( Z (0)) 2 ( 1 (0)) 2 ( 2 (0)) 2 ( Z (0)) Z ( 1 (0)) Z ( 2 (0)) Z ( Z (0)
) By construction all columns are reflexive coequalisers, and by friendliness so are all rows. By [BW05, Lemma 8.4.2], the diagonal is thus again a (reflexive) coequaliser. Finally, by interchange of colimits, we obtain that ★ 1 ⇒ ★ 2 ։ ★ is also a coequaliser, as desired.

Corollary 10.9. Reflexive coequalisers of friendly monads on a finitely presentable category C are computed pointwise.

Similarly, reflexive coequalisers of finitary monads on a category of the form Set P for some set P, are computed pointwise.

Proof. The first point follows directly from the proposition. For the second, we additionally use the fact that [Set P , Set P ] is friendly (Example 10.7). 10.2. Initial algebras for equational systems. In this section, we want to apply the previous corollary to characterise the induced monad and initial algebra for equational systems. For this, we should show that the monads D and E underlying the relevant parallel pair D ⇒ E in Monadic /C are indeed friendly. What helps us here is that these monads are free on a friendly endofunctor, as we now show. We again state this in the abstract context of a convenient monoidal category.

Proposition 10.10. In any convenient monoidal category, the free monoid on a friendly object is again friendly.

Proof. We in fact prove the more general result that if ∈ C preserves D-colimits for a given category D, in the sense that ⊗preserves D-colimits, then so does ★ ⊗ -. By Corollary 2.34, it is enough to show that the forgetful functor from the category of algebras for the monad ★ ⊗creates D-colimits. But, by [Kel80, Proposition 23.2], this category of algebras is isomorphic (over C) to the category of algebras for the endofunctor ⊗ -. Thus, we are left with showing that the forgetful functor from this latter category creates D-colimits, which follows from the next lemma.

The following is analogous to Proposition 2.32, with an endofunctor instead of a monad.

Lemma 10.11. Let be an endofunctor on a category C. Then, the forgetful functor -alg → C creates any colimit that preserves. More specifically, given a category D such that preserves colimits of all diagrams : D → C, then the forgetful functor -alg → C creates colimits of all diagrams : D → -alg.

Proof. Straightforward.

Corollary 10.12. The free monad on a friendly endofunctor on a finitely presentable category is friendly. (iv) The initial -algebra is the coequaliser of ( ′′ ) 0 , ( ′′ ) 0 : (Σ + Σ ′ ) * (id) ⇒ Σ * (id), equipped with its canonical -algebra structure. the facet morphisms : ( ) → correspond to natural transformations ˜ : ( )•y → , hence by copairing to Σ -algebra structure Σ ( ) → . This correspondence extends straightforwardly to morphisms, hence defining the desired functor -alg → Σ -alg over [Set P , Set S ] . Since it is bijective, the functor is an isomorphism.

We now want to show that, for any equational facet-based signature , the forgetful functor -alg → [Set P , Set S ] is monadic, and to explicitly characterise the corresponding monad and initial algebra. For this, we can exhibit -alg as an equaliser of finitary monadic functors over [Set P , Set S ] and apply Corollary 2.48: (iv) The initial -algebra is the coequaliser of ( ′ ) 0 , ( ′ ) 0 : (Σ + Σ ′ ) * (0) ⇒ Σ * (0), equipped with its canonical -algebra structure.

Applications

In this section, we design a signature in RegTransMnd P,S for each of the announced languages. One exception is Positive GSOS systems: for them, we go further, by recasting them as the signatures of a subregister of RegTransMnd P,S .

11.1. The call-by-value, simply-typed, big-step -calculus. Recall from §4.1, that the simply-typed, call-by-value, big-step -calculus forms a transition monad, where we take P = S to be the set of types (generated from some fixed set of type constants). The monad over Set P is given by values, the source state functor 1 is given by application binary trees, and the second state functor 2 is the identity.

Let us now design a signature for this transition monad. Let : Set P → Set S be specified by the signature of Reg[Set P , Set S ] consisting of two families of operations app , : Θ → × Θ → Θ and val : I → Θ . Our signature for call-by-value, simplytyped, big-step -calculus is presented in the following table

Monad and state functors 1 ( ( ( ))) ↓ 1 ( ) 1 ( ( )) , with ˜ ′ : y → ( ) corresponding to ′ ∈ ( ) by Yoneda; • 1 = and 2 = Id are specified by easy signatures as in Remark 8.17;

• the rules should be understood as families of rules indexed by suitable types. In a bit more detail, the first rule is indexed by the type of . The second one is indexed by two types and . There are five metavariables, 1 , 2 , 3 , , and . We thus take := ( 1 ) → × ( 1 ) × ( 1 ) ( ) × × .

11.2. The ¯ -calculus. Recall from §4.2 that the -calculus [START_REF] Herbelin | Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes[END_REF][START_REF] Vaux | calcul différentiel et logique classique : interactions calculatoires[END_REF] forms a transition monad with P = 2 = {p, s}, where p stands for "programs" and s for "stacks". The placetaker monad on Set P is given by programs and stacks. The set of transition types is S = 3 = {c, p, s}, where c stands for "commands", and both state functors Remark 11.4. We have accounted for the presentation of the -calculus through a reduction relation, but there is an important, alternative presentation based on a labelled transition system [SW01, Table 1.5 p38]. Let us explain why our framework cannot cover such a presentation. The problem is that it includes an input transition ( ).

( ) ---→ [ ↦ → ] in which may be fresh. Letting denote the monad for syntax as in §4.3, the correct way to model the fresh case is to take as corresponding component of the target state functor 2 the -module (c) p , whose elements are processes with a fresh variable. Because the module (c) p is not of the shape 2 • , this goes beyond the framework of transition monads. , where the variables and , are all distinct, op ∈ is an operation with arity , and is an expression potentially depending on all the variables. We saw in §4.4 that each family of operations and rules yields a transition monad where • P = 1, because we are in an untyped setting, • S = 1 because states are terms, • denotes the term monad, • 1 ( ) = , and • 2 ( ) = A × , where A denotes the set of labels.

Let us now define a register GSOS + for specifying positive GSOS systems [START_REF] Bloom | Bisimulation can't be traced[END_REF]. This is a subregister of our register RegTransMnd P,S , for untyped (P = S = 1) transition monads. Let us recall that signatures in this register consist of tuples (Σ , Σ 1 , Σ 2 , Σ Trans ), where, as for above, we implicitly coerce some module morphisms to into module morphisms to ! , also lifting some of their arguments from to ! , namely we use

(-) • -: ! × ! → ! ( , ) ↦ → , • --: ! × ! → ! ( , ) → + : ! × ! → ! ( , ) → + .
Remark 11.7.

• The first lifting is only used in cases where one of its arguments is a singleton multiset, i.e., we need • and • , but not • . • In the second case, only the first argument needs lifting, i.e., we have ( 1 + . . . + ) = 1 + . . . + . • The last lifting is in fact mere multiset union.

Conclusion and perspectives

We have introduced transition monads as a generalisation of reduction monads, and demonstrated that they cover relevant new examples. We have introduced a register of signatures for specifying them. Let us briefly assess the scope of our register for transition monads, or more generally of the notion of transition monad itself.

All combinations of call-by-value vs. call-by-name, small-step vs. big-step, or simplytyped vs. untyped variants of -calculus should be handled smoothly.

Simple imperative languages like IMP [Win93, Chapter 2] may also be organised into transition monads, at least in a trivial way since, in the absence of first-class functions, reduction is generally defined on closed programs.

Languages whose transition rules involve some kind of evaluation contexts, such as ML [Pie04, Chapter 10], -calculi with let rec [START_REF] Ariola | Skew confluence and the lambda calculus with letrec[END_REF], or the substitution calculus [START_REF] Accattoli | A fresh look at the lambda-calculus (invited talk)[END_REF], should also fit into the framework, although with a bit more work.

A first class of languages which clearly cannot be organised naturally as transition monads is those whose transitions involve non-free modules, as noticed in Remark 11.4. Extending the register Reg[Set P , Set S ] of §8 to cover such examples seems at hand.

Another, more problematic class of languages is those with advanced type systems, e.g., polymorphic or dependent types. Covering such examples is one of our longer-term goals.

Another limitation of our approach is the weakness of the induced induction principle. As discussed in §1, this is the price to pay for its simplicity. What is missing, in comparison with previous work like [START_REF] Ahrens | Reduction monads and their signatures[END_REF], is a kind of Grothendieck construction for signatures/registers. This works smoothly in most examples. However, in cases like the differential -calculus, this would require extending the definition of unary multiterm substitution and partial derivation (Lemma 11.6) to all models of the syntax. And this appears to leave some design choices open, which might be a reflection of the diversity of categorical semantics for differential -calculus [START_REF] Richard Blute | Differential categories[END_REF][START_REF] Fiore | Differential structure in models of multiplicative biadditive intuitionistic linear logic[END_REF][START_REF] Ehrhard | An introduction to differential linear logic: proof-nets, models and antiderivatives[END_REF][START_REF] Hyland | The linear-non-linear substitution 2-monad[END_REF].

In the longer term, we plan to refine our register in a way ensuring that the generated transition system satisfies important properties like congruence of useful behavioural equivalences, confluence, or type soundness. In this direction, a result on congruence of

2. 4 .

 4 (Parametric) modules over monoids and monads. 2.4.1. (Parametric) modules over monoids. Let us fix a monoidal category C. We first recall the standard notions of monoid and (right) module over a monoid in a monoidal category, and then introduce the notion of parametric module, inspired by [HM07]. Definition 2.11. Let Mon(C) denote the category of monoids, in any monoidal category C [Mac98, VII.3].

  Definition 2.14. Let Mod(C) denote the category • whose objects are pairs ( , ) where is a monoid and is an -module, and • whose morphisms ( , ) → ( , ) are pairs ( , ) of a monoid morphism : → and a morphism : → in C such that the following diagram commutes. ⊗ ⊗ ⊗ Let U Mod : Mod(C) → Mon(C) denote the forgetful functor. Definition 2.15. A parametric module over C is a section of the forgetful functor U Mod : Mod(C) → Mon(C), i.e., a functor : Mon(C) → Mod(C) such that U Mod • = id Mon(C) .

Remark 2 .

 2 21. D-valued -modules are algebras for the monad -• on [C, D] . When D = C, these are the same as -modules in [C, C] in the sense of Definition 2.12.

:

  Set P denotes the family with a single element, sitting over ∈ P, and • the left adjoint maps any :Set P → Set to the endofunctor ( ∈ Set P ) ↦ → ( ) • y , i.e.,(( ) • y ) ( ) = ( ) and ( ( ) • y ) ( ) = ∅ when ≠ . Indeed, we have a natural isomorphism ( ) • y → ( ) ( ) → ( ) ( ) = = = = = = = = = = = = = = = = = = = = = = = = = = = = = • Proposition 2.29. These adjunctions lift to a P-indexed family of adjunctions Mod(Set P , Set) ⊥ Mod(Set P , Set P ). (-) •y (-)

  Proposition 2.45. The functor (-) -alg : Mnd(C) op → Monadic/C mapping any monad to the forgetful functor -alg → C is an equivalence. Proof. The functor is essentially surjective by definition of monadic functors. It is also full and faithful by [Bar70, Proposition 5.3]. Corollary 2.46. Let C be cocomplete. The equivalence (-) -alg : Mnd(C) op → Monadic/C of Proposition 2.45 lifts to a functor (-) -alg : Mnd (C) op → Monadic /C, which is again an equivalence.

  whose first component is continuous by [Bla76, Proposition 5.6], while the second is by[START_REF] Kelly | A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on[END_REF] Proposition 26.3].

  Definition 4.10. A Positive GSOS rule has the shape . . . , ---→ , . . . ( ∈ , ∈ ) op( 1 , . . . , ) -→ , (4.1) where • op ∈ is an operation with arity ,

  is an algebra for the functor mapping -→ to ′ → -→ , where ′ denotes the pullback Similar to Definition 6.2, with the following composite endofunctor.Example 6.6. Let us now treat the -rule, rectifying Example 6.4.

•Σ

  a list of premise morphisms ( -→ ) ∈ , where each : C → D is a finitary functor, denoted by ì -→ ; • a conclusion morphism -→ ( ). Semantics: Let us consider any signature , consisting of : C → D, with left adjoint : D → C, and morphisms ( : C/ → D/ ( ) mapping any -→ to ′ → -→ ( ), where ′ denotes the following pullback.

  Consider associativity of parallel composition in the -calculus, |( | ) ≡ ( | )| : the metavariables are , , and . The corresponding input arity is Θ 3p , and the output arity is p. Recalling §4.3, and anticipating on §11.3 below, the basic signature contains in particular an operation par : Θ 2 p → Θ p for parallel composition, and the derived operations for associativity respectively map any algebra ( , par : 2 p → p , . . .) to

  [Set P , Set P ] → [Set P , Set] by I ( ) ( ) = , for any ∈ P. Such functors Θ and I are examples of facets, which we now introduce more formally. Definition 8.1. For any categories C and D, a facet for [C, D] is a finitary functor [C, D] → [C, Set] . Let Facet(C, D) := [[C, D] , [C, Set] ] denote the category of facets. Notation 8.2. We abbreviate Facet(Set P , Set S ) to Facet(P, S), for readability. Definition 8.3. Here are a few basic constructions of facets, the first three in the general case, and the next three for [Set P , Set S ] . • Any functor : D → Set induces a facet Φ defined by Φ ( ) = • . • Similarly, any functor : C → Set induces a facet Ψ defined by Ψ ( ) ( ) = ( ).

  Signatures: A signature is a facet-based signature. Semantics: The abstract signature associated to any facet-based signature is the forgetful functor -alg → [Set P , Set S ] . Validity proof: By Proposition 10.25 below. 8.3. The register Reg[Set P , Set S ] . Definition 8.13. Given any facet-based signatures and ′ , an -derived operation of arity ′ is a functor : -alg → ′ -alg over [Set P , Set S ] , i.e., making the following triangle commute.

Definition 8. 15 .

 15 An equational facet-based signature consists of • a facet-based signature called the operations facet-based signature, • a facet-based signature ′ called the equations facet-based signature, and • a pair of -derived operations of arity ′ .

Definition 9. 4 .

 4 An equational system E = (C : Γ ⊢ = : Σ) consists of • a locally finitely presentable category C, • finitary endofunctors Σ and Γ, together with • functorial Σ * -terms and of arity Γ. This differs slightly from Fiore and Hur's [FH09] definition, so let us readily bridge the gap. Proposition 9.5. Given any finitary endofunctors Σ and Γ on a locally finitely presentable category C, there are natural isomorphisms (in Σ and Γ) between (i) functorial Σ * -terms of arity Γ, i.e., natural transformations Γ → Σ * , (ii) monad morphisms Γ * → Σ * , (iii) functors Σ -alg → Γ -alg over C, (iv) monad morphisms (Σ + Γ) * → Σ * with section the canonical morphism Σ * → (Σ + Γ) * , (v) functors Σ -alg → (Σ + Γ) -alg over C which are sections of the canonical functor (Σ + Γ) -alg → Σ -alg, and (vi) natural transformations Γ • Σ → Σ . Proof. • (i) ⇔ (ii) This is precisely the universal property of Γ * . • (ii) ⇔ (iii) This is precisely Corollary 2.46. • (ii) ⇔ (iv) By (Σ + Γ) * Σ * + Γ * , which holds (in Mnd (C)) because (-) * is a left adjoint, hence preserves coproducts. • (iii) ⇔ (v) By (Σ+Γ) -alg Σ -alg× C Γ -alg, with the canonical functor (Σ+Γ) -alg → Σ -alg as left projection. • (iii) ⇔ (vi) By merely unfolding definitions.

Proposition 9. 8 .

 8 For any equational system E = (C : Γ ⊢ = : Σ) and Σ * -algebra : Σ * ( ) → , the following are equivalent: (a) coequalises , : Γ( ) → Σ * ( ), (b) coequalises the corresponding morphisms Γ * ( ) → Σ * ( ), (c) the induced Σ-algebra structure Σ( ) → belongs to the equaliser of the corresponding functors Σ -alg → Γ -alg over C, (d) coequalises the corresponding morphisms (Σ + Γ) * ( ) → Σ * ( ), (e) the induced Σ-algebra structure Σ( ) → belongs to the equaliser of the corresponding functors Σ -alg → (Σ + Γ) -alg over C, (f) the corresponding natural transformations Γ • Σ → Σ have the same components at the induced Σ-algebra structure Σ( ) → . Proof. • (a) ⇔ (c) Each functor Σ -alg → Γ -alg corresponding to ∈ { , } maps the induced Σ-algebra to Γ( ) -→ Σ * ( ) -→ , so both sides unfold to the same thing. • (b) ⇒ (a) Follows from the fact that precomposing the induced morphisms Γ * → Σ * by Γ → Γ * yields the original and by construction. • (c) ⇒ (b) This holds because (b) is equivalent to equality of induced Γ * -algebra structures, which is further equivalent to equality of induced Γ-algebra structures. The rest follows similarly.

•

  Morphisms are morphisms in C which are both monoid and Σ-algebra morphisms.

( i )

 i monoidal functorial Σ ⊛ -terms of arity Γ, or in other words parametric module morphismsΓ stmod → (Σ ⊛ ) monmod (Definition 2.26), (ii) morphisms Γ ⊛ → Σ ⊛ of monads on Mon(C), (iii) functors Σ -Mon → Γ -Mon over Mon(C), (iv) morphisms (Σ + Γ) ⊛ → Σ ⊛ of monads on Mon(C), with section the canonical morphism Σ ⊛ → (Σ + Γ) ⊛ , (v) functors Σ -Mon → (Σ + Γ) -Mon over Mon(C) which are sections of the forgetful functor (Σ + Γ) -Mon → Σ -Mon, and (vi) natural transformations Mon Both equivalences (ii) ⇔ (iii) and (iv) ⇔ (v) follow directly from Proposition 2.45 because by definition we have Σ ⊛ -alg Σ -Mon, and similarly for Γ and Σ + Γ. Furthermore, (vi) ⇔ (iii) and (iii) ⇔ (v) both follow by mere definition unfolding. This leaves us with proving that the first point agrees with one of the others. For this, we exhibit a natural isomorphism -alg → Γ -Mon (over Mon(C)) Γ stmod → monmod = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = for any monad on Mon(C). The result thus follows by taking = Σ ⊛ .

  Corollary 10.23. The assignment = ( , ′ , , ) ↦ → E := (Σ ′ ⊢ ′′ = ⊗ ′′ : Σ ) induces a compilation RegMnd (Set P ) → MES [Set P ,Set P ] . More concretely, for any equational modular signature , we have an isomorphism -alg E -Mon of categories over Mnd (Set P ). As a result, we readily obtain by Theorem 10.16: Corollary 10.24. Let = ( , ′ , , ) be any equational modular signature. Then: (i) The forgetful functor -alg → Mnd (Set P ) is finitary monadic. (ii) The finitary monad ★ underlying the forgetful functor -alg → [Set P , Set P ] is the reflexive coequaliser in Mnd ([Set P , Set P ] ) of ′′ , ′′ : (Σ + Σ ′ ) ★ ⇒ Σ ★ . (iii) The above coequaliser is created by the forgetful functor Mnd ([Set P , Set P ] ) → [[Set P , Set P ] , [Set P , Set P ] ] , hence computed pointwise.

10. 5 .

 5 Initial algebras for Reg[Set P , Set S ] . In this section, we prove monadicity of the register Reg[Set P , Set S ] of equational facet-based signatures, and characterise underlying monads and initial algebras. For this, we proceed essentially as in the previous section, but more simply since the intricacies related to Σ-monoids do not arise. We are thus able to compile• Reg 0 [Set P , Set S ]to the register EF [Set P ,Set S ] of endofunctors on [Set P , Set S ] , and • Reg[Set P , Set S ] to the register ES [Set P ,Set S ] of equational systems over [Set P , Set S ] . Recalling from Definition 8.19 the endofunctor Σ associated to any facet-based signature , we have: Proposition 10.25. The assignment ↦ → Σ defines a compilation Reg 0 [Set P , Set S ] → EF [Set P ,Set S ] . More concretely, for any facet-based signature = ( , ) ∈ , there exists an isomorphism -alg Σ -alg of categories over [Set P , Set S ] . Proof. As in the proof of Proposition 10.20, by the adjunction [Set P , Set S ] ⊥ [Set P , Set] , (-) •y (-)

  Proposition 10.26. For any equational facet-based signature = ( , ′ , , ), -alg is the equaliser in CAT of and .Proof. Straightforward.But in fact, perhaps more conveniently, we can also compile into equational systems. By Proposition 10.25, and induce functors ′ , ′ : Σ -alg → Σ ′ -alg over [Set P , Set S ] making the following square commute serially. Corollary 10.27. The assignment = ( , ′ , , ) ↦ → E := (Σ ′ ⊢ ′ = ′ : Σ ) induces a compilation Reg[Set P , Set S ] → ES [Set P ,Set S ] . More concretely, for any equational facet-based signature = ( , ′ , , ), we have isomorphisms -alg E -alg of categories over [Set P , Set S ] , and ★ E ★ of finitary monads thereupon. As a result, we readily obtain by Theorem 10.14: Corollary 10.28. Let = ( , ′ , , ) be any equational facet-based signature. Then: (i) The forgetful functor -alg → [Set P , Set S ] is finitary monadic. (ii) The finitary monad ★ which underlies the forgetful functor -alg → [Set P , Set S ] is the reflexive coequaliser in Mnd ([Set P , Set S ] ) of ′ , ′ : (Σ + Σ ′ ) * ⇒ Σ * . (iii) The above coequaliser is created by the forgetful functor Mnd ([Set P , Set S ] ) → [[Set P , Set S ] , [Set P , Set S ] ] , hence computed pointwise.

  app , ( 1 , 2 ) where • -[-] : ( 1 ) ( ) ×→ ( 1 ) denotes the substitution morphism1 ( ( + y )) × ( ) ′ ∈ ( ) 1 ( ( + y )) ↓ [ 1 ( [ ,˜ ′ ]) ] ∈ ( )

1 , 2 :

 2 Set P → Set S are given by 1 ( ) = 2 ( ) = ( p × s , p , s ). Let us repeat the grammar for the reader's convenience.Commands| Programs | . | .Stacks| •Transitions are generated by the congruence rules and the following two rules. | → [ ↦ → ] . | ′ • → [ ↦ → ′ ]| . 0 : 1 → Θ p | : Θ p × Θ p → Θ p : Θ (c) p → Θ p : Θ 2 c × Θ p → Θ p : Θ c × Θ ≡ ( |w c ( )),almost copied verbatim from the standard presentation above, where w c ( ) denotes the action of ( ) → ( + y c ) on . Finally, the transition rules are as follows, denotes the action of( + y c ) p × ( ) c ∈ ( ) c ( + y c ) p [ [ , ˜ ] p ] ∈ ( ) c ----------------→ ( ( )) p ( ) p -----→ ( ) pon ( , ), with ˜ : y c → ( ) corresponding to ∈ ( ) c by Yoneda.Remark 11.2. The third rule has as metavariable module := (Θ (c) p ) 2 . Remark 11.3. The alternative presentation mentioned in §4.3 may be specified in a similar way.

11. 4 .

 4 A register for Positive GSOS systems. Finally, let us recall that Positive GSOS rules have the shape

  In this context, functors that preserve filtered colimits are important. They are called finitary.Definition 2.6. Let [C, D] denote the category of finitary functors C → D for any categories C and D.Proposition 2.7. If C and D are locally finitely presentable, then so is [C, D] . Convenient monoidal categories. We sometimes work in a monoidal category satisfying some additional properties. We call such monoidal categories convenient.

	Proof. See [KP93, Section 4] for the more general enriched case.
	2.3. Definition 2.8. A monoidal category is convenient when
	• it is locally finitely presentable;

Example 2.4 [AR94, Example 1.12]. Any presheaf category is locally finitely presentable. Proposition 2.5 [AR94, Corollary 1.28]. Any locally finitely presentable category is complete.

  Transition proofs are not stable under general substitution. E.g., the following proof

	. ⇓ .	⇓	⇓
		( . ) ⇓
				presenta-
	tion [Vau07, §2.4.4], its grammar is given by
	Commands	Programs	Stacks
	|	|	. | .	| • ,
	where and range over two disjoint sets of variables, called stack and program variables,
	respectively. Both constructions	and bind their variable in the body. Reduction is
	generated by the following two basic transition rules concerning commands:

of ( . ) ⇓ becomes invalid if we replace with any non-value term . Indeed, ⇓ does not hold. And in fact, the conclusion itself becomes invalid: we cannot have ( . ) ⇓ since evaluation results are all values. 4.2. The ¯ -calculus. The -calculus, introduced by Herbelin [Her95], models the computational contents of cut elimination in the sequent calculus. Following Vaux's

  Let us give the parametric modules for a few operations from our examples. In the above table, p, s, and c are placetaker types, and the subscripts on Θ refer to the notation introduced in Example 2.28. Thus, e.g., (Θ p

	Language	Operation	Source Target
	Pure	Push •	Θ p × Θ s	Θ s
	Pure -calculus	Abstraction . Input ( ).	Θ (p) p Θ c × Θ (c) p	Θ p Θ p

  Definition 8.16. For any sets P and S, we define the monadic register Reg[Set P , Set S ] for [Set P , Set S ] as follows. Signatures: A signature is an equational facet-based signature. Semantics: The abstract signature associated to any equational facet-based signature is the forgetful functor -alg → [Set P , Set S ] .

	Validity proof: By Corollary 10.28 below.
	Remark 8.17. Any finitary functor admits a trivial signature consisting of the family
	(( • I) → Θ ) ∈S of operations, which does not prevent other signatures from being more
	convenient (see the case of Example 8.6). Here are a few examples from §4:
	Language	State functor	Trivial signature
	1

  Definition 9.22. For any convenient monoidal category C, the monadic register PSEF C for the category Mon(C) of monoids in C is defined as follows. Signatures: A signature is a finitary, pointed strong endofunctor on C. Semantics: The abstract signature associated to any signature Σ is the forgetful functor Σ -Mon → Mon(C). Monoidal equational systems. In this section, we combine the registers ES C and PSEF C of the two previous sections, yielding a new register MES C obtained from PSEF C by 'adding monoidal equations'. Definition 9.24. A monoidal equational system E = (C : Γ ⊢ = ⊗ : Σ) consists of • a convenient monoidal category C, • two pointed strong endofunctors Σ and Γ on C, and • a parallel pair , : Γ stmod ⇒ (Σ ⊛ ) monmod of monoidal functorial Σ ⊛ -terms, which we call a monoidal equation. Proposition 9.25. Given any locally finitely presentable category C, there are natural isomorphisms (in Σ and Γ) between

	Validity proof: By Theorem 9.19.
	9.3.

Definition 9.23. Given finitary, pointed strong endofunctors Σ and Γ on a convenient monoidal category C, a monoidal functorial Σ ⊛ -term of arity Γ is a parametric module morphism Γ stmod → (Σ ⊛ ) monmod , where we recall Γ stmod from Definition 9.16 and (Σ ⊛ ) monmod from Notation 9.20 and Example 2.17.

Here "algebra" and "forgetful" have no technical meaning and are chosen by analogy.

Remark 4.4. The extended context Γ, : is isomorphic to Γ + y , where y denotes the Yoneda embedding P ↩→ Set P , viewing P as a discrete category. Indeed, because P is discrete, y ( ) is empty when ≠ , and y ( ) is a singleton. Thus Γ + y is Γ, plus one element of type . Definition 4.5. Well-typed terms are inductively defined by the following rules.Γ ⊢ :( ∈ Γ ) Γ, : ⊢ :

State functorsIn big-step semantics, transitions relate terms to values. Hence, we are seeking state functors 1 , 2 : Set P → Set P such that 1 ( (Γ)) is the set of typing derivations of type with free variables in Γ, and 2 ( (Γ)) is the subset of value typing derivations therein. For 2 , we should clearly take the identity functor since consists of all value typing derivations. For 1 , we first observe that -terms can be described as application binary trees whose leaves are values (internal nodes being typed applications). More formally, let 1 (Γ) denotes the set of typing derivations with conclusion of the form Γ ⊢ 1 : inductively generated by the following rules.

). In this case, we introduce special notation, which allows us to write signatures

Definition 9.13. A pointed strong endofunctor on a monoidal category (C, ⊗, ) is an endofunctor Σ equipped with a pointed strength, i.e., a natural transformation with components , : Σ( ) ⊗ → Σ( ⊗ ) between functors C × /C → C, making the following diagrams commute (pointed objects : → are denoted by their codomains for readability),

where /C inherits monoidal structure ( , ⊗, . . .) from C in the obvious way [START_REF] Weber | Generic morphisms, parametric representations and weakly cartesian monads[END_REF].

Remark 9.14. There is a simpler notion of strong endofunctor, which also involves a natural transformation , : Σ( ) ⊗ → Σ( ⊗ ), although with not pointed. Strong endofunctors embed into pointed strong endofunctors, which are thus more general. The generalisation is necessary to cover variable binding, as shown by the following example.

Example 9.15. For defining -calculus syntax, we take C := [Set, Set] to be the category of finitary endofunctors on sets with the composition tensor product, and Σ( ) ( ) = ( ) 2 + ( + 1) (using the equivalence [Set, Set] ≃ [Set , Set], where Set is the full category spanning finite ordinals). The tensor product is defined on [Set , Set] by the coend formula [Mac98, §IX.6]

which is in one-to-one correspondence with ( ( )). Elements of ( ⊗ ) ( ) may be thought of as explicit substitutions ( ), with ∈ ( ) and : → ( ), considered equivalent up to standard equations, compactly summarised by ( • )( ) = ( • ), for all : → , ∈ ( ) and : → ( ), where • is shorthand for ( ) ( ).

A monoid structure on any ∈ C thus amounts to • a substitution operation ⊗ → mapping any such explicit substitution ( ) ∈ ( ⊗ ) ( ) to some proper substitution, which we denote by [ ] ∈ ( ),

• together with a morphism → , which, because ( ) = id( ) = , amounts to identifying available variables within each ( ). These data are required to satisfy the usual associativity and unitality conditions, which amount to standard substitution lemmas.

Returning to pointed strengths ( , ) : Σ( ) ( ( )) → Σ( ( ( ))), intuitively, they describe the behaviour of substitution w.r.t. application and abstraction. E.g., for application, we define it to map ( 1 ( 1 , 2 ))( ) to 1 ( 1 ( ), 2 ( )), which will ensure the usual equation

Abstraction is the point where pointedness of comes into play. Indeed, supposing that is equipped with a point : → , we may define ↑ : + 1 → ( + 1) by copairing of Example 9.26. Recall from Example 9.15 the pointed strong endofunctor Σ( ) ( ) = ( ) 2 + ( + 1) for pure -calculus on [Set, Set] . As promised, let us now use this to complete the aborted treatment of the -equation in Example 9.26. This is made possible by working directly at the level of monoids (which we think of as objects equipped with substitution). We again take Γ( ) ( ) = ( +1) × ( ), and define and at any Σ-monoid to map any ( , ) ∈ ( + 1) × ( ) to ( ) and [ ] respectively, where [ ] denotes the result of substituting for the ( + 1)th variable of . More precisely, [ ] = • ( ), where :

Let us now turn to defining algebras for a monoidal equational system.

Definition 9.27. For any monoidal equational system E = (C :

). An E-algebra morphism is a morphism between underlying Σ ⊛ -algebras (a.k.a. Σ-monoids). We let E : E -alg → Mon(C) denote the forgetful functor.

Mimicking Proposition 9.8, we now transfer this definition across the various correspondences of Proposition 9.25.

Proposition 9.28. For any monoidal equational system E = (C : Γ ⊢ = ⊗ : Σ) and Σ ⊛ -algebra : Σ ⊛ ( ) → , the following are equivalent:

(a) coequalises , : Γ stmod ( ) → (Σ ⊛ ) monmod ( ), (b) coequalises the corresponding morphisms Γ ⊛ ( ) → Σ ⊛ ( ), (c) the induced Σ-monoid structure Σ stmod ( ) → belongs to the equaliser of the corresponding functors Σ -Mon → Γ -Mon, (d) the induced Σ-monoid structure Σ stmod ( ) → belongs to the equaliser of the induced functors Σ -Mon → Γ -alg, (e) coequalises the corresponding morphisms (Σ + Γ) ⊛ ( ) → Σ ⊛ ( ), (f) the induced Σ stmod -algebra structure Σ stmod ( ) → belongs to the equaliser of the corresponding functors Σ -Mon → (Σ + Γ) -Mon, (g) the corresponding natural transformations Γ stmod • Σ → (-) monmod • Σ have the same components at the induced Σ-algebra structure Σ stmod ( ) → .

Proof.

• (a) ⇔ (c) The corresponding functors Σ -Mon → Γ -Mon map the induced Σ stmod -algebra to Γ stmod ( ) -→ (Σ ⊛ ) monmod ( ) -→ , for = , , so both sides unfold to the same thing.

Follows from the fact that precomposing the induced morphisms

by Γ stmod → (Γ ⊛ ) monmod yields the original and by construction.

which is further equivalent to equality of induced Γ-algebra structures. The rest follows easily. Definition 9.29. For a given convenient monoidal category C, we define the monadic register MES C , called the monoidal equational register, as follows. Signatures: A signature is a monoidal equational system.

Semantics:

The abstract signature associated to a signature E is the forgetful functor E -alg → Mon(C).

Validity proof: By Theorem 10.16 below.

Computing initial algebras in the presence of equations

In this section, we establish the announced explicit descriptions of initial algebras, thereby proving that the registers introduced in §7 and §8 are valid. For this, we in passing also prove the validity of the registers from §9, and establish useful explicit descriptions of initial algebras for them too. In order, we characterise the underlying monad and initial algebra for suitable signatures in our registers featuring equations, namely the registers Because (finitary) monads are monoids in the category of (finitary) endofunctors, we can in fact generalise the result to monoids in a suitable category (see Proposition 10.17 below). Preservation of reflexive coequalisers plays a fundamental role in the study of algebraic theories [START_REF] Adámek | Algebraic Theories: A Categorical Introduction to General Algebra[END_REF]. As we will use it a lot, let us give it a name.

Definition 10.1.

• A reflexive pair of morphisms is a pair , : → of parallel morphisms, sharing a common section , i.e., : → such that = id = . • A reflexive coequaliser is a coequaliser of a reflexive pair.

• A functor is friendly when it is finitary and preserves reflexive coequalisers.

Remark 10.2. By [ARV10, Theorem 7.7], when the considered categories are cocomplete, this is equivalent to preserving all sifted colimits. Definition 10.3. An object of a monoidal category is ⊗-friendly (pronounced "tensorfriendly") when the functor ⊗is friendly.

Proposition 10.4. For any locally finitely presentable category C, a finitary endofunctor on C is friendly iff it is ⊗-friendly as an object of [C, C] (viewed as monoidal for the composition tensor product).

Proof. Colimits of functors are computed pointwise [Mac98, §V.4].

Notation 10.5. By the proposition, in all of our use cases, ⊗-friendliness and friendliness are synonymous, hence we use the latter for simplicity.

Definition 10.6. A monoidal category is friendly when it is convenient and all objects are friendly.

Example 10.7.

• The composition monoidal structure on finitary endofunctors on any locally finitely presentable category is convenient, though not friendly in general. By Proposition 10.4, the friendly objects are precisely the endofunctors preserving reflexive coequalisers. • On categories of the form Set P for some set P, though, by [ARV10, Corollary 6.30], all finitary endofunctors are friendly, hence [Set P , Set P ] is friendly.

Proposition 10.8. For any convenient monoidal category C, the forgetful functor

creates reflexive coequalisers of friendly objects. More concretely, given a reflexive pair ⇒ of monoid morphisms, if and are friendly, then the coequaliser in C lifts uniquely to a cocone of monoids, which is again a coequaliser.

Proof. Monoids are the algebras of the "free monoid" monad, which we denote by (-) ★ in this proof. Furthermore, a forgetful functor from monad algebras always creates those colimits that the monad preserves (Proposition 2.32). It thus suffices to show that (-) ★ preserves reflexive coequalisers of friendly objects.

Let thus 1 ⇒ 2 ։ denote a reflexive coequaliser, with 1 and 2 friendly. Let us first show that is again friendly. For this, we consider any reflexive coequaliser 1 ⇒ 2 ։ . Then, we have:

Furthermore, by Proposition 9.21 (with Σ = 0), ★ is the initial algebra of the endofunctor = + ⊗ -. Morevoer, is the coequaliser of 1 ⇒ 2 , i.e., ( + 1 ⊗ -) ⇒ ( + 2 ⊗ -).

We then prove by induction that 1 (0) ⇒ 2 (0) ։ (0) is again a (reflexive) coequaliser, for all ∈ N.

• The base case is trivial.

• Assuming that 1 (0) ⇒ 2 (0) ։ (0) is a coequaliser, we consider the following diagram.

We now want to apply Corollary 10.9 to prove a first free+quotient explicit description of initial algebras for equational systems. The exact same technique will then be applied to other registers in the following subsections, namely to monoidal equational systems, equational modular signatures, and equational facet-based signatures.

Before giving the explicit description, we need to introduce the following.

Definition 10.13. For any functorial term : Γ → Σ * , let ˜ denote the monad morphism

where ′ : Γ * → Σ * denotes the monad morphism induced by by freeness of Γ * .

We may now state:

Theorem 10.14. Let E = (C : Γ ⊢ = : Σ) be any equational system. Then: (i) The forgetful functor E -alg → C is finitary monadic.

(ii) The finitary monad E * underlying the forgetful functor E -alg → C is the coequaliser (in Mnd (C)) of ˜ , ˜ : (Σ + Γ) * ⇒ Σ * . Furthermore, if Σ and Γ are friendly (which is in particular the case when C is [Set P , Set P ] for some set P), we have:

(iii) The above coequaliser E * is created by the forgetful functor

with its canonical Σ-algebra structure.

Proof. We start by expressing the category E -alg as an equaliser in CAT.

For any functorial term : Γ → Σ * , let ′ : Σ -alg → Γ -alg map any Σ-algbra : Σ( ) → to the composite

where ˜ denotes the induced Σ * -algebra structure on .

The category E -alg is then the equaliser of the (generally non-reflexive) pair below left,

which already entails monadicity by Corollary 2.48. But it is also an equaliser of the reflexive pair above right, which entails (ii) by Corollary 2.46. The rest then follows from Corollary 10.9 using Corollary 10.12.

Example 10.15. Let us recall Example 9.2, where we introduced an equational system whose algebras are sets equipped with an associative binary operation. Because we know how to compute coequalisers in sets, the theorem says that the free algebra on any ∈ Set is obtained by quotienting the free Σ-algebra Σ * ( ) by following relation ∼. We first construct the free (Σ + Γ)-algebra (Σ + Γ) * ( ) on , obtained by freely adding a binary operation and a ternary operation, say , to . We then define two maps , : (Σ + Γ) * ( ) → Σ * ( ), by recursively interpreting ( , , ) as ( + ) + , resp. + ( + ). We finally define ∼ to be the smallest equivalence relation such that ∼ whenever = ( ) and = ( ) for some ∈ (Σ + Γ) * ( ).

10.3. Initial algebras for monoidal equational systems. In this section, we characterise the induced monad and initial algebra of monoidal equational systems, under mild additional hypotheses.

Theorem 10.16. Let E = (C : Γ ⊢ = ⊗ : Σ) be any monoidal equational system. Then: (i) The forgetful functor E -alg → Mon(C) is finitary monadic.

(ii) The finitary monad E ★ induced by the forgetful functor E -alg → C is the coequaliser of , :

, where we recall that, for any finitary, pointed strong endofunctor , ★ denotes the "free -monoid" monad on C. If Σ and Γ are friendly, which is in particular the case when C is [Set P , Set P ] for some set P, then:

(iii) The above coequaliser E ★ is created by the forgetful functor Mnd (C) → [C, C] , hence computed pointwise. (iv) The initial E-algebra is the coequaliser of 0 , 0 : (Σ + Γ) * (id) ⇒ Σ * (id), equipped with its canonical Σ-monoid structure.

Proof. By Theorem 9.19, both forgetful functors Σ -Mon → C and Γ -Mon → C are finitary monadic. Corollaries 2.46 and 2.48 thus directly entail (i) and (ii). The rest will follow from Corollary 10.9 if we prove that both monads (Σ + Γ) ★ and Σ ★ are friendly. This is proved in the next lemma.

Proposition 10.17. For any finitary, pointed strong endofunctor on a friendly monoidal category C, if is friendly, then so is the "free -monoid" monad ★ .

Proof. This is a direct generalisation of the proof of Proposition 10.8 (which corresponds to the case = 0), using the fact that the free -monoid monad maps to the initial algebra of ↦ → + ⊗ + ( ), as recalled in Proposition 9.21.

10.4. Initial algebras for RegMnd (Set P ). In this section, we characterise the underlying monad and initial algebra of equational modular signatures, i.e., signatures of the register RegMnd (Set P ), filling in the missing bits from §7.3. We first deal with the register RegMnd 0 (Set P ) without equations, by compiling (in the sense of Definition 5.8) to the register PSEF [Set P ,Set P ] of pointed strong endofunctors on [Set P , Set P ] . We then tackle the whole register RegMnd (Set P ), using friendliness.

Let us first deal with the case without equations. Recalling from Definition 7.14 the endofunctor Σ on [Set P , Set P ] induced by a modular signature , the idea in this case is that the assignment ↦ → Σ may be viewed as mapping signatures of RegMnd 0 (Set P ) to signatures of PSEF [Set P ,Set P ] , i.e., pointed strong endofunctors. We first establish this by equipping Σ with a pointed strength, then use compilation to transport the problem, and conclude.

Proposition 10.18. For any modular signature , the endofunctor Σ admits a pointed strength given at any ∈ [Set P , Set P ] , ∈ id/[Set P , Set P ] , ∈ Set P , and operation of arity ( , ), say with = ( • Θ) ( 1 ,..., ) , by applying ( (-)) • y to the obvious morphism ( ) + y → ( + y ).

Proof. Straightforward.

Remark 10.19. In a bit more detail, letting = ( , ) ∈ , we have Σ = ∈ Σ , . The pointed strength is defined as the coproduct (of morphisms)

where for all ∈ , say with ( •Θ) ( 1 ,..., ) and ∈ P, , , is the obvious morphism ( ( ( )

Proposition 10.20. The assignment ↦ → Σ defines a compilation

More concretely, for any modular signature = ( , ) ∈ , there exists an isomorphism -alg Σ -Mon of categories over Mnd (Set P ).

Proof. Any family of Set-valued module morphisms : ( ) → corresponds by the adjunction of Proposition 2.29 to a family ˜ : ( ) • y → of Set P -valued module morphisms, hence by copairing to one compatible module morphism Σ stmod ( ) → (recalling Definition 9.16), and thus to Σ -monoid structure on . This correspondence extends straightforwardly to morphisms, hence defining the desired functor -alg → Σ -Mon over Mnd (Set P ). Since it is bijective, the functor is an isomorphism.

Corollary 10.21. For any modular signature , the forgetful functor -alg → Mnd (Set P ) is monadic, and furthermore the free -algebra on an endofunctor ∈ [Set P , Set P ] is the free Σ -monoid Σ ★ ( ), as characterised in Proposition 9.21.

In particular, Σ * (id) has a canonical -algebra structure, which is initial.

We now want to characterise the initial -algebra, for any equational modular signature = ( , ′ , , ), where we recall that and are functors -alg → ′ -alg over Mnd (Set P ). Clearly: Proposition 10.22. For any equational modular signature = ( , ′ , , ), -alg is the equaliser in CAT of and .

By Proposition 10.20, and induce functors ′ , ′ : Σ -Mon → Σ ′ -Mon over Mnd (Set P ) making the following square commute serially.

-alg ′ -alg

By Corollary 2.46, ′ and ′ induce a reflexive parallel pair of monad morphisms ′′ , ′′ :

The tuple (Σ , Σ + ′ , ′′ , ′′ ) forms a monoidal equational system E , over the category [Set P , Set P ] , whose algebras are by construction isomorphic to -algebras. This readily entails:

Let us see how to specify this transition monad using our register. We saw in Remark 8.17 that both state functors may be specified by operations

with no equation.

The basic transition rules are almost as usual:

• The various substitution morphisms -[-] are defined analogously as in §11.1.

• The first rule has metavariable module :=

s × s , the argument being ( , ′ , ). • The second rule has := (p) p × p × s . Let us finish by listing the various congruence rules.

Commands:

Stacks:

11.3. The -calculus. Recall from §4.3 that the -calculus [SW01] also forms a transition monad with P = 2 = {c, p} (c for "channels", p for "processes"). The placetaker monad is the identity on channels, and is defined on processes by the grammar Let us recall that we denote any object ∈ Set P by = ( c , p ), so that we have ( ) = ( c , ( ) p ) ∈ Set P . Furthermore, transitions relate processes, so we have S = 1 and 1 ( )

Let us see how to specify this transition monad using our register. The state functor has been specified in Remark 8.17, by a single operation : I p → Θ. The placetaker monad is specified by operations where = spec (Σ ), 1 = spec (Σ 1 ), 2 = spec (Σ 2 ), and Σ Trans is a signature in the register RegTransStruct P,S ( , 1 , 2 ).

In order to describe this subregister, we have to describe its class of signatures, and then assign to each such signature a tuple (Σ , Σ 1 , Σ 2 , Σ Trans ) as above.

A signature of the register GSOS + consists of • three sets (for operations), A (for labels), and (for rules),

• for each element of , a number (the arity), • for each rule, -an operation ∈ (for the source of the conclusion), -a label ∈ A (the label of the conclusion), -for each 1 ≤ ≤ , * a number (the number of premises for this argument), * for each 1 ≤ ≤ , an element of A (for the label of the premise), -a term in the syntax generated by , potentially depending on + variables.

We now describe the tuple (Σ , Σ 1 , Σ 2 , Σ Trans ) associated to a signature as above: • the signatures for both state functors have been given in Remark 8.17: 1 is specified by a single operation I → Θ, while 2 is specified by a single operation A × I → Θ; • the signature for the underlying monad is the family (Θ → Θ) ∈ (following §7.1); • finally, each Positive GSOS rule yields a rule

in the corresponding signature Σ Trans (in the register RegTransStruct P,S ( , 1 , 2 )).

Remark 11.5. In a bit more detail:

• The metavariable module is = + ∈ , of which a typical element is a tuple := (( ) ∈ , ( , ) ∈ , ∈ ) ∈

+ ( ).

• There are ∈ premises. • The ( , )th premise maps any tuple to ( , ( , , , )).

• The conclusion maps it to ( ( 1 , . . . ,

), ( , ( ))), where : → is the target expression viewed as a -module morphism. 11.5. The differential -calculus. Recall from §4.5 that the differential -calculus syntax is defined by , ,

where terms and multiterms are considered equivalent up to the following equations.

Based on unary multiterm substitution [ ↦ → ] and partial derivation • , the transition relation is defined as the smallest context-closed relation satisfying the rules below,

where is linearly extended to multiterms: .( 1 + . . . + ) is notation for . 1 + . . . + . . We saw that this all forms a transition monad with one placetaker type and one transition type (P = S = 1).

Let us now design a signature specifying this transition monad. Such a signature consists of signatures for the state functors and monad, together with a signature for the transition module.

Signature for the placetaker monad Recalling that ! denote the finite multiset functor, the monad of differential -calculus is specified by the signature with operations :

and one equation:

By taking !Θ as type for the second argument of application, we directly identify multiterms as finite multisets, which explains why we do not need any further equation for enforcing order irrelevance of +.

Signature for the state functors Our state functors are 1 = Id and 2 = !, which are specified by easy signatures in the sense of Remark 8.17.

Signature for transitions Specifying the transition rules requires the following lemma.

Lemma 11.6. There exist -module morphisms :

(1) × ! → ! and :

(1) × ! → ! (1) , respectively called unary multiterm substitution and partial derivation, satisfying the equations of [Vau07, Definition 6.3 and 6.4].

Proof sketch. By the explicit description of Corollary 10.24, is a quotient of the initial Σ -monoid by Equation (11.1). We thus first define both operations from (1) by induction following [Vau07, Definition 6.3 and 6.4], then check that both obtained morphisms coequalise the relevant parallel pair to extend them to morphisms from (1) . Finally, we check that both obtained morphisms are indeed module morphisms, which follows from [Vau07, Lemma 6.10].

Now that both auxiliary operations and are defined, the main transition rules are

where we implicitly coerce : (1) → into a morphism ! (1) → ! . Furthermore, because reduction in the differential -calculus is context-closed, we need to include the following congruence rules, detailed in [START_REF] Vaux | calcul différentiel et logique classique : interactions calculatoires[END_REF]Definition 6.18