Final Dialgebras: From Categories to Allegories

Roland Backhouse; Paul Hoogendijk

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 4-5, page 401-426
  • ISSN: 0988-3754

Abstract

top
The study of inductive and coinductive types (like finite lists and streams, respectively) is usually conducted within the framework of category theory, which to all intents and purposes is a theory of sets and functions between sets. Allegory theory, an extension of category theory due to Freyd, is better suited to modelling relations between sets as opposed to functions between sets. The question thus arises of how to extend the standard categorical results on the existence of final objects in categories (for example, coalgebras and products) to their existence in allegories. The motivation is to streamline current work on generic programming, in which the use of a relational theory rather than a functional theory has proved to be desirable. In this paper, we define the notion of a relational final dialgebra and prove, for an important class of dialgebras, that a relational final dialgebra exists in an allegory if and only if a final dialgebra exists in the underlying category of maps. Instances subsumed by the class we consider include coalgebras and products. An important lemma expresses bisimulations in allegorical terms and proves this equivalent to Aczel and Mendler's categorical definition.

How to cite

top

Backhouse, Roland, and Hoogendijk, Paul. "Final Dialgebras: From Categories to Allegories." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 401-426. <http://eudml.org/doc/221963>.

@article{Backhouse2010,
abstract = { The study of inductive and coinductive types (like finite lists and streams, respectively) is usually conducted within the framework of category theory, which to all intents and purposes is a theory of sets and functions between sets. Allegory theory, an extension of category theory due to Freyd, is better suited to modelling relations between sets as opposed to functions between sets. The question thus arises of how to extend the standard categorical results on the existence of final objects in categories (for example, coalgebras and products) to their existence in allegories. The motivation is to streamline current work on generic programming, in which the use of a relational theory rather than a functional theory has proved to be desirable. In this paper, we define the notion of a relational final dialgebra and prove, for an important class of dialgebras, that a relational final dialgebra exists in an allegory if and only if a final dialgebra exists in the underlying category of maps. Instances subsumed by the class we consider include coalgebras and products. An important lemma expresses bisimulations in allegorical terms and proves this equivalent to Aczel and Mendler's categorical definition. },
author = {Backhouse, Roland, Hoogendijk, Paul},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Programming theory; theory of datatypes; inductive type; co-inductive type; relation algebra; category theory; allegory theory; generic programming; polytypic programming.; coinductive types},
language = {eng},
month = {3},
number = {4-5},
pages = {401-426},
publisher = {EDP Sciences},
title = {Final Dialgebras: From Categories to Allegories},
url = {http://eudml.org/doc/221963},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Backhouse, Roland
AU - Hoogendijk, Paul
TI - Final Dialgebras: From Categories to Allegories
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 4-5
SP - 401
EP - 426
AB - The study of inductive and coinductive types (like finite lists and streams, respectively) is usually conducted within the framework of category theory, which to all intents and purposes is a theory of sets and functions between sets. Allegory theory, an extension of category theory due to Freyd, is better suited to modelling relations between sets as opposed to functions between sets. The question thus arises of how to extend the standard categorical results on the existence of final objects in categories (for example, coalgebras and products) to their existence in allegories. The motivation is to streamline current work on generic programming, in which the use of a relational theory rather than a functional theory has proved to be desirable. In this paper, we define the notion of a relational final dialgebra and prove, for an important class of dialgebras, that a relational final dialgebra exists in an allegory if and only if a final dialgebra exists in the underlying category of maps. Instances subsumed by the class we consider include coalgebras and products. An important lemma expresses bisimulations in allegorical terms and proves this equivalent to Aczel and Mendler's categorical definition.
LA - eng
KW - Programming theory; theory of datatypes; inductive type; co-inductive type; relation algebra; category theory; allegory theory; generic programming; polytypic programming.; coinductive types
UR - http://eudml.org/doc/221963
ER -

References

top
  1. C.J. Aarts, R.C. Backhouse, P. Hoogendijk, T.S. Voermans and J. van der Woude, A relational theory of datatypes. Available via World-Wide Web at http://www.win.tue.nl/cs/wp/papers (September 1992).  
  2. P. Aczel, Non Well-Founded Sets, Number 14 in CSLI Lecture Notes. Center for the Study of Language and Information (Stanford, California, 1988).  
  3. P. Aczel and N. Mendler, A final coalgebra theorem, D.H. Pitt, Ed., Category Theory and Computer Science. Springer Verlag, Lecture Notes in Comput. Sci. (1989) 357-365.  
  4. R.C. Backhouse, P. de Bruin, P. Hoogendijk, G. Malcolm, T.S. Voermans and J. van der Woude, Polynomial relators, M. Nivat, C.S. Rattray, T. Rus and G. Scollo, Eds., in Proc. of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST'91. Springer-Verlag, Workshops in Computing (1992) 303-326.  
  5. R. Bird, O. de Moor and P. Hoogendijk, Generic functional programming with types and relations. J. Funct. Programming6 (1996) 1-28.  
  6. R.S. Bird and O. de Moor, Algebra of Programming. Prentice-Hall International (1996).  
  7. H. Doornbos, Reductivity arguments and program construction. Ph.D. Thesis, Eindhoven University of Technology, Department of Mathematics and Computing Science (1996).  
  8. P.J. Freyd and A. Scedrov, Categories, Allegories. North-Holland (1990).  
  9. T. Hagino, A typed lambda calculus with categorical type constructors, D.H. Pitt, A. Poigne and D.E. Rydeheard, Eds., Category Theory and Computer Science. Springer-Verlag, Lecture Notes in Comput. Sci.283 (1988) 140-57.  
  10. P. Hoogendijk, A Generic Theory of Datatypes. Ph.D. Thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology (1997).  
  11. P. Hoogendijk and R. Backhouse, When do datatypes commute? E. Moggi and G. Rosolini, Eds., Category Theory and Computer Science, 7th International Conference. Springer-Verlag, Lecture Notes in Comput. Sci.1290 (1997) 242-260.  
  12. P. Hoogendijk and O. de Moor, What is a datatype? Technical Report 96/16, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1996. J. Funct. Programming, to appear.  
  13. B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. Bull. Eur. Assoc. Theor. Comput. Sci. EATCS62 (1997) 222-259.  
  14. P. Jansson and J. Jeuring, PolyP - a polytypic programming language extension. In POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press (1997) 470-482.  
  15. C.B. Jay, A semantics for shape. Sci. Comput. Programming25 (1995) 251-283.  
  16. C.B. Jay and J.R.B. Cockett, Shapely types and shape polymorphism, D. Sannella, Ed., ESOP '94: 5th European Symposium on Programming. Springer Verlag, Lecture Notes in Comput. Sci. (1994) 302-316.  
  17. J. Jeuring, Polytypic pattern matching. In Conference Record of FPCA '95, SIGPLAN-SIGARCH-WG2.8 Conference on Functional Programming Languages and Computer Architecture (1995) 238-248.  
  18. J. Jeuring and P. Jansson, Polytypic programming, J. Launchbury, E. Meijer and T. Sheard, Eds., Proceedings of the Second International Summer School on Advanced Functional Programming Techniques. Springer-Verlag, Lecture Notes in Comput. Sci.1129 (1996) 68-114.  
  19. J. Lambek, A fixpoint theorem for complete categories. Math. Z.103 (1968) 151-161.  
  20. J. Lambek, Subequalizers. Canad. Math. Bull.13 (1970) 337-349.  
  21. S. MacLane, Categories for the Working Mathematician. Springer-Verlag, New York (1971).  
  22. L. Meertens, Calculate polytypically! H. Kuchen and S. Doaitse Swierstra, Eds., Proceedings of the Eighth International Symposium PLILP '96 Programming Languages: Implementations, Logics and Programs. Springer Verlag, Lecture Notes in Comput. Sci.1140 (1996) 1-16.  
  23. E. Meijer, M.M. Fokkinga and R. Paterson, Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA91: Functional Programming Languages and Computer Architecture. Springer-Verlag, Lecture Notes in Comput. Sci.523 (1991) 124-144.  
  24. S.D. Swierstra and O. de Moor, Virtual data structures, H. Partsch, B. Möller and S. Schuman, Eds., Formal Program Development. Springer-Verlag, Lecture Notes in Comput. Sci.755 (1993) 355-371.  

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.