Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show that in a Freyd category, these notions are equivalent, generalizing a well-known theorem relating traces and Conway operators in cartesian categories.
Keywords: traces, fixed point operators, premonoidal categories, recursion, monads
@article{ITA_2003__37_4_273_0,
author = {Benton, Nick and Hyland, Martin},
title = {Traced premonoidal categories},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {273--299},
year = {2003},
publisher = {EDP Sciences},
volume = {37},
number = {4},
doi = {10.1051/ita:2003020},
mrnumber = {2053028},
zbl = {1110.68356},
language = {en},
url = {https://www.numdam.org/articles/10.1051/ita:2003020/}
}
TY - JOUR AU - Benton, Nick AU - Hyland, Martin TI - Traced premonoidal categories JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2003 SP - 273 EP - 299 VL - 37 IS - 4 PB - EDP Sciences UR - https://www.numdam.org/articles/10.1051/ita:2003020/ DO - 10.1051/ita:2003020 LA - en ID - ITA_2003__37_4_273_0 ER -
%0 Journal Article %A Benton, Nick %A Hyland, Martin %T Traced premonoidal categories %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2003 %P 273-299 %V 37 %N 4 %I EDP Sciences %U https://www.numdam.org/articles/10.1051/ita:2003020/ %R 10.1051/ita:2003020 %G en %F ITA_2003__37_4_273_0
Benton, Nick; Hyland, Martin. Traced premonoidal categories. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 273-299. doi: 10.1051/ita:2003020
[1] , Using circular programs to eliminate multiple traversals of data. Acta Informatica 21 (1984) 239-250. | Zbl
[2] ,, and, Lava: Hardware design in Haskell, in International Conference on Functional Programming (1998).
[3] and, Axiomatizing schemes and their behaviors. J. Comput. Syst. Sci. 31 (1985) 375-393. | Zbl | MR
[4] and, Iteration Theories. EATCS Monographs on Theoretical Computer Science, Springer-Verlag (1993). | Zbl | MR
[5] and, A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization. Theor. Comput. Sci. 99 (1992) 1-63. | Zbl | MR
[6] and, Observable sharing for functional circuit description, in Asian Computing Science Conference (1999).
[7] , Regular Algebra and Finite Machines. Chapman Hall (1971). | Zbl
[8] and, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Inf. Comput. 98 (1992) 171-210. | Zbl | MR
[9] , Value Recursion in Monadic Computations. Ph.D. thesis, Oregon Graduate Institute, OHSU (October 2002).
[10] , and, Semantics of value recursion for monadic input/output. RAIRO Theoret. Informatics Appl. 36 (2002) 155-180. | Zbl | MR | Numdam
[11] , Axiomatizing iteration categories. Acta Cybernet. 14 (1999). | Zbl | MR
[12] , Group axioms for iteration. Inf. Comput. 148 (1999) 131-180 | Zbl | MR
[13] and, Recursion is a computational effect. Technical Report 546, Computer Science Department, Indiana University (December 2000).
[14] , and, An equational notion of lifting monad. Theor. Comput. Sci. 294 (2003) 31-60. | Zbl | MR
[15] , Towards a geometry of interaction, in Categories in Computer Science and Logic, edited by J.W. Gray and A. Scedrov. Contemp. Math. 92 (1989) 69-108. | Zbl | MR
[16] , Models of Sharing Graphs (A Categorical Semantics of Let and Letrec). Distinguished Dissertations in Computer Science, Springer-Verlag (1999). | Zbl | MR
[17] , The uniformity principle on traced monoidal categories, edited by R. Blute and P. Selinger. Elsevier, Electronic Notes in Theor. Comput. Sci. (2003). | MR
[18] , Generalising monads to arrows. Sci. Comput. Program. 37 (2000) 67-112. | Zbl | MR
[19] and, Symmetric monoidal sketches, in Proc. of the 2nd Conference on Principles and Practice of declarative Programming (2000) 280-288.
[20] , Premondoidal categories and a graphical view of programs. http://www.cogs.susx.ac.uk/users/alanje/premon/ (June 1998).
[21] , and, Traced monoidal categories. Math. Proc. Cambridge Philoso. Soc. 119 (1996). | Zbl | MR
[22] and, Recursive monadic bindings, in International Conference on Functional Programming (2000).
[23] , and, On embedding a microarchitectural design language within Haskell. International Conference on Functional Programming (1999).
[24] and, State in Haskell. Lisp and Symbolic Computation 8 (1995) 293-341.
[25] , Notions of computation and monads. Inf. Comput. 93 (1991) 55-92. | Zbl | MR
[26] and, An abstract monadic semantics for value recursion, in Proc. of the 2003 Workshop on Fixed Points in Computer Science (April 2003). | MR | Numdam
[27] , Strong monads, algebras and fixed points, in Applications of Categories in Computer Science, edited by M.P. Fourman, P.T. Johnstone and A.M. Pitts. LMS Lecture Notes 177 (1992) 202-216. | Zbl | MR
[28] , A new notation for arrows, in Proc. of the International Conference on Functional Programming. ACM Press (September 2001).
[29] , Arrows and computation, in The Fun of Programming, edited by J. Gibbons and O. de Moor. Palgrave (2003) 201-222.
[30] and, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. | Zbl | MR
[31] and, Closed Freyd and -categories. International Conference on Automata, Languages and Programming (1999). | Zbl | MR
[32] and, Complete axioms for categorical fixed-point operators, in Proc. of 15th Annual Symposium on Logic in Computer Science. IEEE Computer Society (2000). | MR
[33] , The essence of functional programming, in Proc. of the 19th Symposium on Principles of Programming Languages. ACM (1992).
Cité par Sources :
