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.
Mots-clés : 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}, publisher = {EDP-Sciences}, volume = {37}, number = {4}, year = {2003}, doi = {10.1051/ita:2003020}, mrnumber = {2053028}, zbl = {1110.68356}, language = {en}, url = {http://archive.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 - http://archive.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 http://archive.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. http://archive.numdam.org/articles/10.1051/ita:2003020/
[1] Using circular programs to eliminate multiple traversals of data. Acta Informatica 21 (1984) 239-250. | Zbl
,[2] Lava: Hardware design in Haskell, in International Conference on Functional Programming (1998).
, , and ,[3] Axiomatizing schemes and their behaviors. J. Comput. Syst. Sci. 31 (1985) 375-393. | MR | Zbl
and ,[4] Iteration Theories. EATCS Monographs on Theoretical Computer Science, Springer-Verlag (1993). | MR | Zbl
and ,[5] A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization. Theor. Comput. Sci. 99 (1992) 1-63. | MR | Zbl
and ,[6] Observable sharing for functional circuit description, in Asian Computing Science Conference (1999).
and ,[7] Regular Algebra and Finite Machines. Chapman Hall (1971). | Zbl
,[8] New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Inf. Comput. 98 (1992) 171-210. | MR | Zbl
and ,[9] Value Recursion in Monadic Computations. Ph.D. thesis, Oregon Graduate Institute, OHSU (October 2002).
,[10] Semantics of value recursion for monadic input/output. RAIRO Theoret. Informatics Appl. 36 (2002) 155-180. | Numdam | MR | Zbl
, and ,[11] Axiomatizing iteration categories. Acta Cybernet. 14 (1999). | MR | Zbl
,[12] Group axioms for iteration. Inf. Comput. 148 (1999) 131-180 | MR | Zbl
,[13] Recursion is a computational effect. Technical Report 546, Computer Science Department, Indiana University (December 2000).
and ,[14] An equational notion of lifting monad. Theor. Comput. Sci. 294 (2003) 31-60. | MR | Zbl
, and ,[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. | MR | Zbl
,[16] Models of Sharing Graphs (A Categorical Semantics of Let and Letrec). Distinguished Dissertations in Computer Science, Springer-Verlag (1999). | MR | Zbl
,[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. | MR | Zbl
,[19] Symmetric monoidal sketches, in Proc. of the 2nd Conference on Principles and Practice of declarative Programming (2000) 280-288.
and ,[20] Premondoidal categories and a graphical view of programs. http://www.cogs.susx.ac.uk/users/alanje/premon/ (June 1998).
,[21] Traced monoidal categories. Math. Proc. Cambridge Philoso. Soc. 119 (1996). | MR | Zbl
, and ,[22] Recursive monadic bindings, in International Conference on Functional Programming (2000).
and ,[23] On embedding a microarchitectural design language within Haskell. International Conference on Functional Programming (1999).
, and ,[24] State in Haskell. Lisp and Symbolic Computation 8 (1995) 293-341.
and ,[25] Notions of computation and monads. Inf. Comput. 93 (1991) 55-92. | MR | Zbl
,[26] An abstract monadic semantics for value recursion, in Proc. of the 2003 Workshop on Fixed Points in Computer Science (April 2003). | Numdam | MR
and ,[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. | MR | Zbl
,[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] Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. | MR | Zbl
and ,[31] Closed Freyd and -categories. International Conference on Automata, Languages and Programming (1999). | MR | Zbl
and ,[32] Complete axioms for categorical fixed-point operators, in Proc. of 15th Annual Symposium on Logic in Computer Science. IEEE Computer Society (2000). | MR
and ,[33] The essence of functional programming, in Proc. of the 19th Symposium on Principles of Programming Languages. ACM (1992).
,Cité par Sources :