Reflecting algebraically compact functors. (English) Zbl 07453968
Baez, John (ed.) et al., Proceedings of the applied category theory 2019, ACT 2019, University of Oxford, UK, July 15–19, 2019. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 323, 15-23 (2020).
Summary: A compact \(T\)-algebra is an initial \(T\)-algebra whose inverse is a final \(T\)-coalgebra. Functors with this property are said to be algebraically compact. This is a very strong property used in programming semantics which allows one to interpret recursive datatypes involving mixed-variance functors, such as function space. The construction of compact algebras is usually done in categories with a zero object where some form of a limit-colimit coincidence exists. In this paper we consider a more abstract approach and show how one can construct compact algebras in categories which have neither a zero object, nor a (standard) limit-colimit coincidence by reflecting the compact algebras from categories which have both. In doing so, we provide a constructive description of a large class of algebraically compact functors (satisfying a compositionality principle) and show our methods compare quite favorably to other approaches from the literature.
For the entire collection see [Zbl 1466.68006].
For the entire collection see [Zbl 1466.68006].
References:
| [1] | S. Abramsky & A. Jung (1994): Domain Theory. Handbook of Logic in Computer Science (Vol. 3), pp. 1-168. Available at http://dl.acm.org/citation.cfm?id=218742.218744. |
| [2] | Jiří Adámek (1974): Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae 15(4), pp. 589-602. · Zbl 0293.18006 |
| [3] | M. Barr (1992): Algebraically compact functors. Journal of Pure and Applied Algebra 82(3), pp. 211 -231, doi:10.1016/0022-4049(92)90169-G. · Zbl 0777.18005 · doi:10.1016/0022-4049(92)90169-G |
| [4] | F. Borceux (1994): Handbook of Categorical Algebra 2: Categories and Structures. Cambridge University Press, doi:10.1017/CBO9780511525865. · Zbl 0843.18001 · doi:10.1017/CBO9780511525865 |
| [5] | M. P. Fiore (1994): Axiomatic domain theory in categories of partial maps. Ph.D. thesis, University of Edinburgh, UK. |
| [6] | Marcelo Fiore & Gordon Plotkin (1994): An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC. In: LICS, doi:10.1109/LICS.1994.316083. · doi:10.1109/LICS.1994.316083 |
| [7] | P. Freyd (1990): Recursive types reduced to inductive types. In: LICS 1990, pp. 498-507, doi:10.1109/LICS.1990.113772. · doi:10.1109/LICS.1990.113772 |
| [8] | P. Freyd (1991): Algebraically complete categories. In: Category Theory: Proceedings of the International Conference held in Como, Italy, doi:10.1007/BFb0084215. · Zbl 0815.18005 · doi:10.1007/BFb0084215 |
| [9] | Daniel J Lehmann & Michael B Smyth (1981): Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, doi:10.1007/BF01752392. · Zbl 0457.68035 · doi:10.1007/BF01752392 |
| [10] | Bert Lindenhovius, Michael Mislove & Vladimir Zamdzhiev (2018): Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams. In: LICS 2018, ACM, doi:10.1145/3209108.3209196. · Zbl 1454.03023 · doi:10.1145/3209108.3209196 |
| [11] | Bert Lindenhovius, Michael Mislove & Vladimir Zamdzhiev (2020): Se-mantics for a Lambda Calculus for String Diagrams. Available at https://homepages.loria.fr/VZamdzhiev/papers/lambda-calculus-string-diagrams.pdf. Preprint. · Zbl 1454.03023 |
| [12] | Bert Lindenhovius, Michael W. Mislove & Vladimir Zamdzhiev (2019): Mixed linear and non-linear recur-sive types. Proc. ACM Program. Lang. 3(ICFP), pp. 111:1-111:29, doi:10.1145/3341715. · doi:10.1145/3341715 |
| [13] | Bert Lindenhovius, Michael W. Mislove & Vladimir Zamdzhiev (2020): LNL-FPC: The Linear/Non-linear Fixpoint Calculus. Available at http://arxiv.org/abs/1906.09503. Preprint. · Zbl 1535.68045 |
| [14] | Romain Péchoux, Simon Perdrix, Mathys Rennela & Vladimir Zamdzhiev (2020): Quantum Programming with Inductive Datatypes. Available at https://homepages.loria.fr/VZamdzhiev/papers/qpl-inductive.pdf. Preprint. · Zbl 1442.68034 |
| [15] | Romain Péchoux, Simon Perdrix, Mathys Rennela & Vladimir Zamdzhiev (2020): Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. In Jean Goubault-Larrecq & Barbara König, editors: Foundations of Software Science and Computation Structures -23rd International Conference, FOS-SACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Lecture Notes in Computer Science 12077, Springer, pp. 562-581, doi:10.1007/978-3-030-45231-5_29. · Zbl 1442.68034 · doi:10.1007/978-3-030-45231-5_29 |
| [16] | Francisco Rios & Peter Selinger (2017): A categorical model for a quantum circuit description language. In: QPL 2017, pp. 164-178, doi:10.4204/EPTCS.266.11. · Zbl 1486.81067 · doi:10.4204/EPTCS.266.11 |
| [17] | M.B. Smyth & G.D. Plotkin (1982): The Category-theoretic Solution of Recursive Domain Equations. Siam J. Comput., doi:10.1137/0211062. · Zbl 0493.68022 · doi:10.1137/0211062 |
| [18] | Vladimir Zamdzhiev (2020): Semantics for first-order affine inductive data types via slice categories. In: Coalgebraic Methods in Computer Science, to appear. Available at https://arxiv.org/abs/2001.06905. · Zbl 1480.68011 |
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.
