We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of …
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of Eugenio Moggi's monads as notions of computation, exhibit a representation theorem for our premonoidal setting in terms of monads, and give a fibrational setting for the structure.
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and …
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and Kleisli constructions for each of these possibilities. Then we consider two applications of these weakened notions of distributivity in detail. We characterise Turi and Plotkin's model of GSOS as a distributive law of a monad over a co-pointed endofunctor, and we analyse generalised coiteration and coalgebraic coinduction "up-to" in terms of a distributive law of the underlying pointed endofunctor of a monad over an endofunctor.
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a …
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a category with ordinary transition systems as objects and with morphisms characterised in terms of a linear notion of bisimulation. The final object in this category is the canonical abstract model for trace equivalence and can be obtained by extending the final coalgebra of the deterministic action behaviour to the Kleisli category of the non-empty powerset monad. The corresponding final coalgebra semantics is fully abstract with respect to trace equivalence.
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into …
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterize naturally arising trees and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of model. By taking the forgetful functor from the category of comodels …
We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of model. By taking the forgetful functor from the category of comodels to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of comodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.
We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of …
We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of Marmolejo and Lack, we develop the definition of a pseudo-distributive law between pseudo-monads, and we show how the definition and the main theorems about it may be used to model several such structures simultaneously. Specifically, we address the relationship between pseudo-distributive laws and the lifting of one pseudo-monad to the 2-category of algebras and to the Kleisli bicategory of another. This, for instance, sheds light on the preservation of some structures but not others along the Yoneda embedding. Our leading examples are given by the use of open maps to model bisimulation and by the logic of bunched implications.
In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard …
In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a tensor C⊗M of the comodel with the model that allows operations to flow between the two. We describe such a tensor implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle …
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad.
We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H —Coalg of H-coalgebras. We give …
We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H —Coalg of H-coalgebras. We give conditions under which completeness, cocompleteness, symmetric monoidal closed structure, local presentability, and subobject classifiers lift. Our proof of the latter uses a general result about the existance of a subobject classifier in a category containing a small dense subcategory. Our leading example has C = Set with H the endofunctor for which a coalgebra is a finitely branching (labelled) transition system. We explain that example in detail.
Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more …
Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle than might appear at first glance: final coalgebras can form monads just as easily as comonads, and, dually, initial algebras form both monads and comonads.In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by first defining a notion of cosignature and coequation and then proving that the models of such coalgebraic presentations are precisely the coalgebras of the representing comonad.
Abstract Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set …
Abstract Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set . We generalise that relationship from Set to an arbitrary locally presentable category such as Poset and ω Cpo or functor categories such as [ Inj , Set ] and [ Inj , ω Cpo ]. That involves allowing the arities of Lawvere theories to be extended to being size-restricted objects of the locally presentable category. We develop a body of theory at this level of generality, in particular explaining how the relationship between generalised Lawvere theories and monads extends Gabriel–Ulmer duality.
We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first …
We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first consider the class of closed -categories, a natural and direct generalisation of the notion of cartesian closed category. We then consider closed ·-categories, which are based upon indexed categories and which are closely related to modern compiling technology. Finally, we consider the class of cartesian closed categories · together with a ·-enriched monad. The latter class has the most developed abstract theory, which one can adopt and by which one can dispense with coherence details in the spirit of Mac Lane involving strengths.
We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do …
We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and ωCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad T$_{fp}$ on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [F, Set] to [(SA)$^{op}$, V$^{A}$]. We define a substitution monoidal structure on [(SA)$^{op}$, V$^{A}$], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previouswork by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.
We introduce the notion of pseudo-commutative monad together with that of pseudo-closed 2-category, the leading example being given by the 2-monad on Cat whose 2-category of algebras is the 2-category …
We introduce the notion of pseudo-commutative monad together with that of pseudo-closed 2-category, the leading example being given by the 2-monad on Cat whose 2-category of algebras is the 2-category of small symmetric monoidal categories. We prove that for any pseudo-commutative 2-monad on Cat, its 2-category of algebras is pseudo-closed. We also introduce supplementary definitions and results, and we illustrate this analysis with further examples such as those of small categories with finite products, and examples arising from wiring, interaction, contexts, and the logic of Bunched Implication.
We consider an extant infinitary variant of Lawvere's finitary definition of extensivity of a category $\mathcal V$. In the presence of cartesian closedness and finite limits in $\mathcal V$, we …
We consider an extant infinitary variant of Lawvere's finitary definition of extensivity of a category $\mathcal V$. In the presence of cartesian closedness and finite limits in $\mathcal V$, we give two characterisations of the condition in terms of a biequivalence between the bicategory of matrices over $\mathcal V$ and the bicategory of spans over discrete objects in $\mathcal V$. Using the condition, we prove that $\mathcal{V}﹣\mathrm{Cat}$ and the category $\mathrm{Cat}_\mathrm{d}(\mathcal{V})$ of internal categories in $\mathcal V$ with a discrete object of objects are equivalent. Our leading example has $\mathcal{V} = \mathrm{Cat}$, making $\mathcal{V}﹣\mathrm{Cat}$ the category of all small 2-categories and $\mathrm{Cat}_\mathrm{d}(\mathcal{V})$ the category of small double categories with discrete category of objects. We further show that if $\mathcal V$ is extensive, then so are $\mathcal{V}﹣\mathrm{Cat}$ and $\mathrm{Cat}(\mathcal{V})$, allowing the process to iterate.
Motivated by a model for syntactic control of interference, we introduce a general categorical concept of bireflectivity. Bireflective subcategories of a category A are subcategories with left and right adjoint …
Motivated by a model for syntactic control of interference, we introduce a general categorical concept of bireflectivity. Bireflective subcategories of a category A are subcategories with left and right adjoint equal, subject to a coherence condition. We characterize them in terms of split-idempotent natural transformations on id A . In the special case that A is a presheaf category, we characterize them in terms of the domain, and prove that any bireflective subcategory of A is itself a presheaf category. Given a small symmetric monoidal category C , we define diagonal structure on C , which is that structure and a little less than those axioms required to prove the monoidal structure is finite product structure. We then obtain a bireflective subcategory of [ C op, Set] and deduce results relating its finite product structure with the monoidal structure of [ C op, Set] determined by that of C . We also investigate closed structure.
We introduce a potential application of two-dimensional linear algebra to concurrency. Motivated by the structure of categories of wirings, in particular in action calculi but also in other models of …
We introduce a potential application of two-dimensional linear algebra to concurrency. Motivated by the structure of categories of wirings, in particular in action calculi but also in other models of concurrency, we investigate the notion of symmetric monoidal sketch for providing an abstract notion of category of wirings. Every symmetric monoidal sketch generates a generic model. If the sketch is single-sorted, the generic model can be characterised as a free structure on 1, with structure defined coalgebraically. We investigate how these results generalise results about categories of wirings given by Milner and others, and we outline how the constructs may be extended to model controls and dynamics.
In this paper, we explore, enrich, and otherwise mildly generalise a prominent definition of weak n-category by Batanin, as refined by Leinster, to give a definition of weak n-dimensional V-category, …
In this paper, we explore, enrich, and otherwise mildly generalise a prominent definition of weak n-category by Batanin, as refined by Leinster, to give a definition of weak n-dimensional V-category, with a view to applications in programming semantics. We require V to be locally presentable and to be (infinitarily) extensive, a condition which ensures that coproducts are suitably well-behaved. Our leading example of such a V is the category ω-Cpo, ω-Cpo-enriched bicategories already having been used in denotational semantics. We illuminate the implicit use of recursion in Leinster's definition, generating the higher dimensions by a process of repeated enrichment. The key fact is that if V is a locally presentable and extensive category, then so are the categories of small V-graphs and small V-categories. Iterating, this produces categories of n-dimensional V-graphs and strict n-dimensional V-categories that are also locally presentable and extensive. We show that the free strict n-dimensional V-category monad on the category of n-dimensional V-graphs is cartesian. This, along with results due to Garner, allows us to follow Batanin and Leinster's approach for defining weak n-categories. In the case that V = Set, the resulting definition of weak n-dimensional V-category agrees with Leinster's definition.
We give a new account of the correspondence, first established by Nishizawa--Power, between finitary monads and Lawvere theories over an arbitrary locally finitely presentable base. Our account explains this correspondence …
We give a new account of the correspondence, first established by Nishizawa--Power, between finitary monads and Lawvere theories over an arbitrary locally finitely presentable base. Our account explains this correspondence in terms of enriched category theory: the passage from a finitary monad to the corresponding Lawvere theory is exhibited as an instance of free completion of an enriched category under a class of absolute colimits. This extends work of the first author, who established the result in the special case of finitary monads and Lawvere theories over the category of sets; a novel aspect of the generalisation is its use of enrichment over a bicategory, rather than a monoidal category, in order to capture the monad--theory correspondence over all locally finitely presentable bases simultaneously. Comment: 24 pages
We consider an extant infinitary variant of Lawvere's finitary definition of extensivity of a category $\mathcal V$. In the presence of cartesian closedness and finite limits in $\mathcal V$, we …
We consider an extant infinitary variant of Lawvere's finitary definition of extensivity of a category $\mathcal V$. In the presence of cartesian closedness and finite limits in $\mathcal V$, we give two characterisations of the condition in terms of a biequivalence between the bicategory of matrices over $\mathcal V$ and the bicategory of spans over discrete objects in $\mathcal V$. Using the condition, we prove that $\mathcal{V}﹣\mathrm{Cat}$ and the category $\mathrm{Cat}_\mathrm{d}(\mathcal{V})$ of internal categories in $\mathcal V$ with a discrete object of objects are equivalent. Our leading example has $\mathcal{V} = \mathrm{Cat}$, making $\mathcal{V}﹣\mathrm{Cat}$ the category of all small 2-categories and $\mathrm{Cat}_\mathrm{d}(\mathcal{V})$ the category of small double categories with discrete category of objects. We further show that if $\mathcal V$ is extensive, then so are $\mathcal{V}﹣\mathrm{Cat}$ and $\mathrm{Cat}(\mathcal{V})$, allowing the process to iterate.
We give a new account of the correspondence, first established by Nishizawa--Power, between finitary monads and Lawvere theories over an arbitrary locally finitely presentable base. Our account explains this correspondence …
We give a new account of the correspondence, first established by Nishizawa--Power, between finitary monads and Lawvere theories over an arbitrary locally finitely presentable base. Our account explains this correspondence in terms of enriched category theory: the passage from a finitary monad to the corresponding Lawvere theory is exhibited as an instance of free completion of an enriched category under a class of absolute colimits. This extends work of the first author, who established the result in the special case of finitary monads and Lawvere theories over the category of sets; a novel aspect of the generalisation is its use of enrichment over a bicategory, rather than a monoidal category, in order to capture the monad--theory correspondence over all locally finitely presentable bases simultaneously.
A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on …
A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on $P_fP_f$, describes derivations by resolution. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic programs with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.
A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on …
A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on $P_fP_f$, describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi's saturation semantics for logic programming that complements lax semantics.
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into …
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterize naturally arising trees and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into …
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterise naturally arising trees, and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
Abstract Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set …
Abstract Motivated by the search for a body of mathematical theory to support the semantics of computational effects, we first recall the relationship between Lawvere theories and monads on Set . We generalise that relationship from Set to an arbitrary locally presentable category such as Poset and ω Cpo or functor categories such as [ Inj , Set ] and [ Inj , ω Cpo ]. That involves allowing the arities of Lawvere theories to be extended to being size-restricted objects of the locally presentable category. We develop a body of theory at this level of generality, in particular explaining how the relationship between generalised Lawvere theories and monads extends Gabriel–Ulmer duality.
In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard …
In seeking a unified study of computational effects, one must take account of the coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C, typically the final one, and a model M, typically free; one then seeks a tensor C⊗M of the comodel with the model that allows operations to flow between the two. We describe such a tensor implicit in the abstract category theoretic literature, explain its significance for computational effects, and calculate it in leading classes of examples, primarily involving state.
We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do …
We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and ωCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad T$_{fp}$ on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [F, Set] to [(SA)$^{op}$, V$^{A}$]. We define a substitution monoidal structure on [(SA)$^{op}$, V$^{A}$], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previouswork by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.
We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of model. By taking the forgetful functor from the category of comodels …
We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of model. By taking the forgetful functor from the category of comodels to Set, every (countable) Lawvere theory generates a comonad on Set. But while Lawvere theories are equivalent to finitary monads on Set, and that result extends to higher cardinality, no such result holds for comonads, and that is not only for size reasons: it is primarily because, while Set is cartesian closed, Setop is not. So every monad with rank on Set generates a comonad on Set, but not conversely. Our leading example is given by the countable Lawvere theory for global state: its category of comodels is the category of arrays, yielding a precise relationship between global state and arrays. Restricting from arbitrary comonads to those comonads generated by Lawvere theories allows us to study new and interesting constructions, in particular that of tensor product.
We introduce a potential application of two-dimensional linear algebra to concurrency. Motivated by the structure of categories of wirings, in particular in action calculi but also in other models of …
We introduce a potential application of two-dimensional linear algebra to concurrency. Motivated by the structure of categories of wirings, in particular in action calculi but also in other models of concurrency, we investigate the notion of symmetric monoidal sketch for providing an abstract notion of category of wirings. Every symmetric monoidal sketch generates a generic model. If the sketch is single-sorted, the generic model can be characterised as a free structure on 1, with structure defined coalgebraically. We investigate how these results generalise results about categories of wirings given by Milner and others, and we outline how the constructs may be extended to model controls and dynamics.
Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more …
Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle than might appear at first glance: final coalgebras can form monads just as easily as comonads, and, dually, initial algebras form both monads and comonads.In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by first defining a notion of cosignature and coequation and then proving that the models of such coalgebraic presentations are precisely the coalgebras of the representing comonad.
We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of …
We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of Marmolejo and Lack, we develop the definition of a pseudo-distributive law between pseudo-monads, and we show how the definition and the main theorems about it may be used to model several such structures simultaneously. Specifically, we address the relationship between pseudo-distributive laws and the lifting of one pseudo-monad to the 2-category of algebras and to the Kleisli bicategory of another. This, for instance, sheds light on the preservation of some structures but not others along the Yoneda embedding. Our leading examples are given by the use of open maps to model bisimulation and by the logic of bunched implications.
We introduce the notion of pseudo-commutative monad together with that of pseudo-closed 2-category, the leading example being given by the 2-monad on Cat whose 2-category of algebras is the 2-category …
We introduce the notion of pseudo-commutative monad together with that of pseudo-closed 2-category, the leading example being given by the 2-monad on Cat whose 2-category of algebras is the 2-category of small symmetric monoidal categories. We prove that for any pseudo-commutative 2-monad on Cat, its 2-category of algebras is pseudo-closed. We also introduce supplementary definitions and results, and we illustrate this analysis with further examples such as those of small categories with finite products, and examples arising from wiring, interaction, contexts, and the logic of Bunched Implication.
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle …
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad.
We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first …
We consider several different sound and complete classes of models for the computational ·-calculus, explain the definitions, and outline why one might be interested in the various classes. We first consider the class of closed -categories, a natural and direct generalisation of the notion of cartesian closed category. We then consider closed ·-categories, which are based upon indexed categories and which are closely related to modern compiling technology. Finally, we consider the class of cartesian closed categories · together with a ·-enriched monad. The latter class has the most developed abstract theory, which one can adopt and by which one can dispense with coherence details in the spirit of Mac Lane involving strengths.
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and …
We generalise the notion of a distributive law between a monad and a comonad to consider weakened structures such as pointed or co-pointed endofunctors, or endofunctors. We investigate Eilenberg-Moore and Kleisli constructions for each of these possibilities. Then we consider two applications of these weakened notions of distributivity in detail. We characterise Turi and Plotkin's model of GSOS as a distributive law of a monad over a co-pointed endofunctor, and we analyse generalised coiteration and coalgebraic coinduction "up-to" in terms of a distributive law of the underlying pointed endofunctor of a monad over an endofunctor.
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a …
We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a category with ordinary transition systems as objects and with morphisms characterised in terms of a linear notion of bisimulation. The final object in this category is the canonical abstract model for trace equivalence and can be obtained by extending the final coalgebra of the deterministic action behaviour to the Kleisli category of the non-empty powerset monad. The corresponding final coalgebra semantics is fully abstract with respect to trace equivalence.
Given a class F of weights, one can consider the construction that<br />takes a small category C to the free cocompletion of C under weighted colimits, for which the weight …
Given a class F of weights, one can consider the construction that<br />takes a small category C to the free cocompletion of C under weighted colimits, for which the weight lies in F. Provided these free Fcocompletions are small, this construction generates a 2-monad on Cat, or more generally on V-Cat for monoidal biclosed complete and cocomplete V. We develop the notion of a dense 2-monad on V-Cat and characterise free F-cocompletions by dense KZ-monads on V-Cat. We prove various corollaries about the structure of such 2-monads and their Kleisli 2-categories, as needed for the use of open maps in giving an axiomatic study of bisimulation in concurrency. This requires the introduction of the concept of a pseudo-commutativity for a strong 2-monad on a symmetric monoidal 2-category, and a characterisation of it in terms of structure on the Kleisli 2-category.
We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H —Coalg of H-coalgebras. We give …
We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H —Coalg of H-coalgebras. We give conditions under which completeness, cocompleteness, symmetric monoidal closed structure, local presentability, and subobject classifiers lift. Our proof of the latter uses a general result about the existance of a subobject classifier in a category containing a small dense subcategory. Our leading example has C = Set with H the endofunctor for which a coalgebra is a finitely branching (labelled) transition system. We explain that example in detail.
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of …
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of Eugenio Moggi's monads as notions of computation, exhibit a representation theorem for our premonoidal setting in terms of monads, and give a fibrational setting for the structure.
Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20.
Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20.
Many problems lead to the consideration of “algebras”, given by an object A of a category A together with “actions” T k A → A on A of one or …
Many problems lead to the consideration of “algebras”, given by an object A of a category A together with “actions” T k A → A on A of one or more endofunctors of A, subjected to equational axioms. Such problems include those of free monads and free monoids, of cocompleteness in categories of monads and of monoids, of orthogonal subcategories (= generalized sheaf-categories), of categories of continuous functors, and so on; apart from problems involving the algebras for their own sake. Desirable properties of the category of algebras - existence of free ones, cocompleteness, existence of adjoints to algebraic functors - all follow if this category can be proved reflective in some well-behaved category: for which we choose a certain comma-category T/A We show that the reflexion exists and is given as the colimit of a simple transfinite sequence, if A is cocomplete and the T k preserve either colimits or unions of suitably-long chains of subobjects. The article draws heavily on the work of earlier authors, unifies and simplifies this, and extends it to new problems. Moreover the reflectivity in T/A is stronger than any earlier result, and will be applied in forthcoming articles, in an enriched version, to the study of categories with structure.
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of …
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of Eugenio Moggi's monads as notions of computation, exhibit a representation theorem for our premonoidal setting in terms of monads, and give a fibrational setting for the structure.
With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be …
With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be complete but do admit a wide class of limits. Accordingly, we introduce a variety of particular 2-categorical limits of practical importance, and show that certain of these suffice for the existence of indexed lax- and pseudo-limits. Other important 2-categories fail to admit even pseudo-limits, but do admit the weaker bilimits; we end by discussing these.
The notion of commutative monad was defined by the author in [4]. The content of the present paper may briefly be stated: The category of algebras for a commutative monad …
The notion of commutative monad was defined by the author in [4]. The content of the present paper may briefly be stated: The category of algebras for a commutative monad can in a canonical way be made into a closed category, the two adjoint functors connecting the category of algebras with the base category are in a canonical way closed functors, and the front- and end-adjunctions are closed transformations. (The terms ‘Closed Category’ etc. are from the paper [2] by Eilenberg and Kelly). In particular, the monad itself is a ‘closed monad’; this fact was also proved in [4].
We apply to logic programming some recently emerging ideas from the field of reductionbased communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms …
We apply to logic programming some recently emerging ideas from the field of reductionbased communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational machinery of such a programming paradigm. The semantic framework we have chosen for presenting our results is tile logic , which has the advantage of allowing a uniform treatment of goals and observations and of applying abstract categorical tools for proving the results. As main contributions, we mention the finitary presentation of abstract unification, and a concurrent and coordinated abstract semantics consistent with the most common semantics of logic programming. Moreover, the compositionality of the tile semantics is guaranteed by standard results, as it reduces to check that the tile systems associated to logic programs enjoy the tile decomposition property . An extension of the approach for handling constraint systems is also discussed.
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into …
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterize naturally arising trees and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.
We consider the behaviour of the terminal sequence of an accessible endofunctor T on a locally presentable category K. The preservation of monics by T is sufficient to imply convergence, …
We consider the behaviour of the terminal sequence of an accessible endofunctor T on a locally presentable category K. The preservation of monics by T is sufficient to imply convergence, necessarily to a terminal coalgebra. We can say much more if K is Set, and κ is ω. In that case it is well known that we do not necessarily get convergence at ω, however we show that to ensure convergence we don't need to go to a higher cardinal, just to the next limit ordinal, ω + ω. For an ω-accessible endofunctor T on Set the construction of the terminal coalgebra can thus be seen as a two stage construction, with each stage being finitary. The first stage obtains the Cauchy completion of the initial T-algebra as the ω-th object in the terminal sequence Aω. In the second stage this object is pruned to get the final coalgebra Aω+ω. We give an example where Aω is the solution of the corresponding domain equation in the category of complete ultra-metric spaces.
Bialgebrae provide an abstract framework encompassing the semantics of different kinds of computational models. In this paper we propose a bialgebraic approach to the semantics of logic programming. Our methodology …
Bialgebrae provide an abstract framework encompassing the semantics of different kinds of computational models. In this paper we propose a bialgebraic approach to the semantics of logic programming. Our methodology is to study logic programs as reactive systems and exploit abstract techniques developed in that setting. First we use saturation to model the operational semantics of logic programs as coalgebrae on presheaves. Then, we make explicit the underlying algebraic structure by using bialgebrae on presheaves. The resulting semantics turns out to be compositional with respect to conjunction and term substitution. Also, it encodes a parallel model of computation, whose soundness is guaranteed by a built-in notion of synchronisation between different threads.
We present a parallel implementation of Coalgebraic Logic Programming (CoALP) in the programming language Go. CoALP was initially introduced to reflect coalgebraic semantics of logic programming, with coalgebraic derivation algorithm …
We present a parallel implementation of Coalgebraic Logic Programming (CoALP) in the programming language Go. CoALP was initially introduced to reflect coalgebraic semantics of logic programming, with coalgebraic derivation algorithm featuring both corecursion and parallelism. Here, we discuss how the coalgebraic semantics influenced our parallel implementation of logic programming.
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic …
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic phenomenon: let H be an endofunctor such that for every object X a final coalgebra, TX, of H(_) + X exists. Then TX is an object-part of a monad which is completely iterative. Moreover, a similar contruction of a "completely iterative monoid" is possible in every monoidal category satisfying mild side conditions.
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions …
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.