Traced Premonoidal Categories

Nick Benton; Martin Hyland

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 37, Issue: 4, page 273-299
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Benton, Nick, and Hyland, Martin. "Traced Premonoidal Categories." RAIRO - Theoretical Informatics and Applications 37.4 (2010): 273-299. <http://eudml.org/doc/92724>.

@article{Benton2010,
abstract = { 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. },
author = {Benton, Nick, Hyland, Martin},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Traces; fixed point operators; premonoidal categories; recursion; monads.; Freyd category; Conway operators in Cartesian categories},
language = {eng},
month = {3},
number = {4},
pages = {273-299},
publisher = {EDP Sciences},
title = {Traced Premonoidal Categories},
url = {http://eudml.org/doc/92724},
volume = {37},
year = {2010},
}

TY - JOUR
AU - Benton, Nick
AU - Hyland, Martin
TI - Traced Premonoidal Categories
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 37
IS - 4
SP - 273
EP - 299
AB - 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.
LA - eng
KW - Traces; fixed point operators; premonoidal categories; recursion; monads.; Freyd category; Conway operators in Cartesian categories
UR - http://eudml.org/doc/92724
ER -

References

top
  1. R.S. Bird, Using circular programs to eliminate multiple traversals of data. Acta Informatica21 (1984) 239-250.  
  2. P. Bjesse, K. Claessen, M. Sheeran and S. Singh, Lava: Hardware design in Haskell, in International Conference on Functional Programming (1998).  
  3. S.L. Bloom and Z. Ésik, Axiomatizing schemes and their behaviors. J. Comput. Syst. Sci.31 (1985) 375-393.  
  4. S.L. Bloom and Z. Ésik, Iteration Theories. EATCS Monographs on Theoretical Computer Science, Springer-Verlag (1993).  
  5. V.E. Cazanescu and Gh. Stefanescu, A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization. Theor. Comput. Sci.99 (1992) 1-63 .  
  6. K. Claessen and D. Sands, Observable sharing for functional circuit description, in Asian Computing Science Conference (1999).  
  7. J.H. Conway, Regular Algebra and Finite Machines. Chapman Hall (1971).  
  8. R.L. Crole and A.M. Pitts, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Inf. Comput.98 (1992) 171-210.  
  9. L. Erkök, Value Recursion in Monadic Computations. Ph.D. thesis, Oregon Graduate Institute, OHSU (October 2002).  
  10. L. Erkök, J. Launchbury and A. Moran, Semantics of value recursion for monadic input/output. RAIRO Theoret. Informatics Appl.36 (2002) 155-180.  
  11. Z. Ésik, Axiomatizing iteration categories. Acta Cybernet.14 (1999).  
  12. Z. Ésik, Group axioms for iteration. Inf. Comput.148 (1999) 131-180 
  13. D.P. Friedman and A. Sabry, Recursion is a computational effect. Technical Report 546, Computer Science Department, Indiana University (December 2000).  
  14. C. Fuhrmann, A. Bucalo and A. Simpson, An equational notion of lifting monad. Theor. Comput. Sci.294 (2003) 31-60 .  
  15. J.-Y. Girard, 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.  
  16. M. Hasegawa, Models of Sharing Graphs (A Categorical Semantics of Let and Letrec). Distinguished Dissertations in Computer Science, Springer-Verlag (1999).  
  17. M. Hasegawa, The uniformity principle on traced monoidal categories, edited by R. Blute and P. Selinger. Elsevier, Electronic Notes in Theor. Comput. Sci. (2003).  
  18. J. Hughes, Generalising monads to arrows. Sci. Comput. Program.37 (2000) 67-112 .  
  19. M. Hyland and A.J. Power, Symmetric monoidal sketches, in Proc. of the 2nd Conference on Principles and Practice of declarative Programming (2000) 280-288.  
  20. A. Jeffrey, Premondoidal categories and a graphical view of programs. (June 1998).  URIhttp://www.cogs.susx.ac.uk/users/alanje/premon/
  21. A. Joyal, R. Street and D. Verity, Traced monoidal categories. Math. Proc. Cambridge Philoso. Soc.119 (1996).  
  22. J. Launchbury and L. Erkök, Recursive monadic bindings, in International Conference on Functional Programming (2000).  
  23. J. Launchbury, J.R. Lewis and B. Cook, On embedding a microarchitectural design language within Haskell. International Conference on Functional Programming (1999).  
  24. J. Launchbury and S.L. Peyton Jones, State in Haskell. Lisp and Symbolic Computation8 (1995) 293-341.  
  25. E. Moggi, Notions of computation and monads. Inf. Comput.93 (1991) 55-92.  
  26. E. Moggi and A. Sabry, An abstract monadic semantics for value recursion, in Proc. of the 2003 Workshop on Fixed Points in Computer Science (April 2003).  
  27. P.S. Mulry, 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 Notes177 (1992) 202-216.  
  28. R. Paterson, A new notation for arrows, in Proc. of the International Conference on Functional Programming. ACM Press (September 2001).  
  29. R. Paterson, Arrows and computation, in The Fun of Programming, edited by J. Gibbons and O. de Moor. Palgrave (2003) 201-222.  
  30. A.J. Power and E.P. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci.7 (1997) 453-468.  
  31. A.J. Power and H. Thielecke, Closed Freyd and κ -categories. International Conference on Automata, Languages and Programming (1999).  
  32. A.K. Simpson and G.D. Plotkin, Complete axioms for categorical fixed-point operators, in Proc. of 15th Annual Symposium on Logic in Computer Science. IEEE Computer Society (2000).  
  33. P. Wadler, The essence of functional programming, in Proc. of the 19th Symposium on Principles of Programming Languages. ACM (1992).  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.