Generic models for computational effects. (English) Zbl 1123.18005
The paper contains a development of a theory of Freyd-categories (a subtle generalisation of the notion of a category with finite products) and various examples of applications of Freyd-categories, including those of modelling effects in Moggi’s computational lambda-calculus. The analysis of computational effects given by monads is refined here by decomposition of the construction of the Kleisli category for a monad.
The setting of Freyd-categories can also be appropriately extended to account for recursion and effects that inherently contain it: partiality, non-determinism, or probablistic non-determinism. This is done through enrichment over a category which is locally countably presentable as a cartesian closed category (this includes the characteristic examples of categories \(\omega {\mathcal C}po\) and \({\mathcal P}oset\)).
The setting of Freyd-categories can also be appropriately extended to account for recursion and effects that inherently contain it: partiality, non-determinism, or probablistic non-determinism. This is done through enrichment over a category which is locally countably presentable as a cartesian closed category (this includes the characteristic examples of categories \(\omega {\mathcal C}po\) and \({\mathcal P}oset\)).
Reviewer: Vladimir Komendantsky (Sophia Antipolis)
MSC:
| 18D10 | Monoidal, symmetric monoidal and braided categories (MSC2010) |
| 18A15 | Foundations, relations to logic and deductive systems |
| 18C20 | Eilenberg-Moore and Kleisli constructions for monads |
| 18C50 | Categorical semantics of formal languages |
| 18A40 | Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) |
| 18A35 | Categories admitting limits (complete categories), functors preserving limits, completions |
References:
| [1] | Blackwell, R.; Kelly, G. M.; Power, A. J., Two-dimensional monad theory, J. Pure Appl. Algebra, 59, 1-41 (1989) · Zbl 0675.18006 |
| [2] | Carboni, A.; Lack, S.; Walters, R. F.C., Introduction to extensive and distributive categories, J. Pure Appl. Algebra, 84, 145-158 (1993) · Zbl 0784.18001 |
| [3] | Hyland, M.; Plotkin, G. D.; Power, A. J., Combining computational effects: commutativity and sum, (Proc. IFIP Conf. on Theoretical Computer Science (2002), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 474-484 |
| [4] | Hyland, M.; Plotkin, G. D.; Power, A. J., Combining computational effects: sum and tensor, Theoret. Comput. Sci., 357, 70-99 (2006) · Zbl 1096.68088 |
| [5] | Im, G. B.; Kelly, G. M., A universal property of the convolution monoidal structure, J. Pure Appl. Algebra, 43, 75-88 (1986) · Zbl 0604.18004 |
| [6] | Kelly, G. M., Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Notes Series, Vol. 64 (1982), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0478.18005 |
| [7] | Kelly, G. M., Structures defined by finite limits in the enriched context, Cah. Topol. Geom. Differ. Categ., 23, 3-42 (1982) · Zbl 0538.18006 |
| [8] | Kinoshita, Y.; Power, A. J., Data-refinement in call-by-value languages, (Proc. of CSL, Lecture Notes in Computer Science, Vol. 1683 (1999)), 562-576 · Zbl 0944.68034 |
| [9] | Levy, P. B.; Power, A. J.; Thielecke, H., Modelling environments in call-by-value programming languages, Inform. and Comput., 185, 182-210 (2003) · Zbl 1069.68073 |
| [10] | Mac Lane, S., Categories for the Working Mathematician (1971), Springer: Springer Berlin · Zbl 0232.18001 |
| [11] | Moggi, E., Computational lambda-calculus and monads, (Proc. of LICS 1989 (1989), IEEE Computer Society Press), 14-23 · Zbl 0716.03007 |
| [12] | Moggi, E., Notions of computation and monads, Inform. and Comput., 93, 55-92 (1991) · Zbl 0723.68073 |
| [13] | Plotkin, G. D.; Power, A. J., Adequacy for algebraic effects, (Proc. of FOSSACS 2000, Lecture Notes in Computer Science, Vol. 2030 (2001)), 1-24 · Zbl 0986.68055 |
| [14] | Plotkin, G. D.; Power, A. J., Semantics for algebraic operations, (Proc. of MFPS 2001, Electronic Notes in Theoretical Computer Science, Vol. 45 (2001)) · Zbl 1260.68220 |
| [15] | Plotkin, G. D.; Power, A. J., Notions of computation determine monads, (Proc. of FOSSACS 2001, Lecture Notes in Computer Science, Vol. 2303 (2002)), 342-356 · Zbl 1077.68676 |
| [16] | Plotkin, G. D.; Power, A. J., Computational effects and operations: an overview, (Proc. of Domains 2002, Electronic Notes in Theoretical Computer Science, Vol. 73 (2002)) · Zbl 1273.68213 |
| [17] | Plotkin, G. D.; Power, A. J., Algebraic operations and generic effects, Appl. Categ. Structures, 11, 69-94 (2003) · Zbl 1023.18006 |
| [18] | Plotkin, G. D.; Power, A. J., Logic for computational effects, (Proc. of IWFM 2003, British Computer Society Electronic Workshops in Computing (2003)) |
| [19] | Power, A. J., Enriched Lawvere theories, Theory Appl. Categ., 6, 83-93 (1999) · Zbl 0943.18003 |
| [20] | Power, A. J., Models for the computational \(\lambda \)-calculus, (Proc. of MFCSIT 2000, Electronic Notes in Theoretical Computer Science, Vol. 40 (2001)) · Zbl 0677.18006 |
| [21] | Power, A. J., Premonoidal categories as categories with algebraic structure, Theoret. Comput. Sci., 278, 303-321 (2002) · Zbl 1002.68089 |
| [22] | Power, A. J., A universal embedding for the higher order structure of computational effects, (Proc. of TLCA 2003, Lecture Notes in Computer Science, Vol. 2701 (2003)), 301-315 · Zbl 1041.03010 |
| [23] | Power, A. J., Canonical models for computational effects, (Proc. of FOSSACS 2004, Lecture Notes in Computer Science, Vol. 2987 (2004)), 438-452 · Zbl 1126.68336 |
| [24] | A.J. Power, Countable Lawvere theories and computational effects, in: Proc. of MFCSIT 2004, Electronic Notes in Theoretical Computer Science, to appear.; A.J. Power, Countable Lawvere theories and computational effects, in: Proc. of MFCSIT 2004, Electronic Notes in Theoretical Computer Science, to appear. · Zbl 1276.68100 |
| [25] | Power, A. J.; Robinson, E. P., Premonoidal categories and notions of computation, (Proc. of LDPL 96, Math Structures in Computer Science, Vol. 7 (1997)), 453-468 · Zbl 0897.18002 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
