Document Open Access Logo

List Objects with Algebraic Structure

Authors Marcelo Fiore, Philip Saville

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.16.pdf
  • Filesize: 0.51 MB
  • 18 pages

Document Identifiers

Author Details

Marcelo Fiore
Philip Saville

Cite As Get BibTex

Marcelo Fiore and Philip Saville. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.16

Abstract

We introduce and study the notion of list object with algebraic structure. The first key aspect of our development is that the notion of list object is considered in the context of monoidal structure; the  second key aspect is that we further equip list objects with algebraic structure in this setting. Within our framework, we observe that list objects give rise to free monoids and moreover show that this remains so in the presence of algebraic structure. In addition, we provide a basic theory explicitly describing as an inductively defined object such free monoids with suitably compatible algebraic structure in common practical situations. This theory is accompanied by the study of two technical themes that, besides being of interest in their own right, are important for establishing applications. These themes are: parametrised initiality, central to the universal property defining list objects; and approaches to algebraic structure, in particular in the context of monoidal theories. The latter leads naturally to a notion of nsr (or near semiring) category of independent interest. With the theoretical development in place, we touch upon a variety of applications, considering Natural Numbers Objects in domain theory, giving a universal property for the monadic list transformer, providing free instances of algebraic extensions of the Haskell Monad type class, elucidating the algebraic character of the construction of opetopes in higher-dimensional algebra, and considering free models of second-order algebraic theories.

Subject Classification

Keywords
  • list object
  • free monoid
  • strong monad
  • (cartesian
  • linear
  • and second-order) algebraic theory
  • near semiring
  • Haskell Monad type class
  • opetope

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. Adámek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae, 015(4):589-602, 1974. Google Scholar
  2. S. Alves, M. Fernández, M. Florido, and I. Mackie. Linear recursive functions. In Rewriting, Computation and Proof: Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pages 182-195. Springer, 2007. Google Scholar
  3. R. Backhouse, M. Bijsterveld, R. van Geldrop, and J. van der Woude. Categorical fixed point calculus. In Category Theory and Computer Science, CTCS 1995, volume 953 of Lecture Notes in Computer Science, pages 159-179. Springer, 1995. Google Scholar
  4. J. C. Baez and J. Dolan. Higher-dimensional algebra III. n-categories and the algebra of opetopes. Advances in Mathematics, 135(2):145-206, 1998. URL: http://dx.doi.org/10.1006/aima.1997.1695.
  5. J. M. Boardman and R. M. Vogt. Homotopy-everything H-spaces. Bull. Amer. Math. Soc., 74(6):1117-1122, 11 1968. Google Scholar
  6. A. Burroni. Récursivité graphique (1^e partie) : catégorie des fonctions récursives primitives formelles. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 27(1):49-79, 1986. Google Scholar
  7. J. R. B. Cockett. List-arithmetic distributive categories: Locoi. Journal of Pure and Applied Algebra, 66(1):1-29, 1990. URL: http://dx.doi.org/10.1016/0022-4049(90)90121-W.
  8. P. M. Cohn. Universal algebra. Reidel, 2nd edition, 1981. Google Scholar
  9. M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press, 1996. Google Scholar
  10. M. Fiore. Second-order and dependently-sorted abstract syntax. In Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, LICS'08, pages 57-68. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.38.
  11. M. Fiore. An equational metalogic for monadic equational systems. Theory and Applications of Categories, 27(18):464-492, 2013. Google Scholar
  12. M. Fiore. An algebraic combinatorial approach to opetopic structure. Notes and https://www.mpim-bonn.mpg.de/node/6586, Seminar on Higher Structures, Program on Higher Structures in Geometry and Physics, Max Planck Institute for Mathematics, February-March 2016.
  13. M. Fiore and C.-K. Hur. On the construction of free algebras for equational systems. Theoretical Computer Science, 410(18):1704-1729, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2008.12.052.
  14. M. Fiore and C.-K. Hur. Second-order equational logic. In Computer Science Logic, CSL 2010, volume 6247 of Lecture Notes in Computer Science, pages 320-335. Springer, 2010. Google Scholar
  15. M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS'99. IEEE Computer Society, 1999. Google Scholar
  16. G. Gonzalez. The list-transformer package, 2016. URL: https://hackage.haskell.org/package/list-transformer.
  17. M. Hamana. Term rewriting with variable binding: An initial algebra approach. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP'03, pages 148-159. ACM, 2003. Google Scholar
  18. A. Hirschowitz and M. Maggesi. Modules over monads and linearity. In WoLLIC 2007, number 4576 in Lecture Notes in Computer Science, pages 218-237. Springer, 2005. Google Scholar
  19. M. Jaskelioff. Lifting of Operations in Modular Monadic Semantics. PhD thesis, University of Nottingham, 2009. Google Scholar
  20. A. Joyal. Foncteurs analytiques et espèces de structures. In Combinatoire Énumérative, volume 1234 of Lecture Notes in Mathematics, pages 126-159. Springer, 1986. Google Scholar
  21. A. Joyal. The Gödel incompleteness theorem, a categorical approach (abstract). Cah. Top. Géom. Diff. Cat., 16(3), 2005. Short abstract of the talk given at the International conference Charles Ehresmann: 100 ans, Amiens, 7-9 October, 2005. Google Scholar
  22. O. Kammar. Algebraic construction of the list transformer. Private communication, 2014. Google Scholar
  23. G. M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 22(1):1-83, 1980. URL: http://dx.doi.org/10.1017/S0004972700006353.
  24. A. Kock. Bilinearity and cartesian closed monads. Mathematica Scandinavica, 29(2):161-174, 1971. Google Scholar
  25. A. Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23(1):113-120, 1972. URL: http://dx.doi.org/10.1007/BF01304852.
  26. J. Kock, A. Joyal, M. Batanin, and J.-F. Mascari. Polynomial functors and opetopes. Advances in Mathematics, 224(6):2690-2737, 2010. URL: http://dx.doi.org/10.1016/j.aim.2010.02.012.
  27. J. Lambek. Multicategories revisited. In Categories in Computer Science and Logic: Proc. of the Joint Summer Research Conference, pages 217-239. American Mathematical Society, 1989. Google Scholar
  28. F. W. Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(5):869-872, 1963. Google Scholar
  29. F. W. Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52(6):1506-1511, 1964. Google Scholar
  30. D. J. Lehmann and M. B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14(1):97-139, 1981. URL: http://dx.doi.org/10.1007/BF01752392.
  31. T. Leinster. Higher Operads, Higher Categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press, 2004. Google Scholar
  32. S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 2nd edition, 1998. Google Scholar
  33. M. E. Maietti. Joyal’s arithmetic universe as list-arithmetic pretopos. Theory and Applications of Categories, 24(3):39-83, 2010. Google Scholar
  34. M. Markl. Operads and PROPs. In Handbook of Algebra, Volume 5, pages 87-140. Elsevier, 2008. Google Scholar
  35. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  36. J. P. May. The Geometry of Iterated Loop Spaces, volume 271 of Lecture Notes in Mathematics. Springer, 1972. Google Scholar
  37. B. Nordström, K. Peterson, and J. Smith. Programming in Martin Löf’s Type Theory. Clarendon Press, 1990. Google Scholar
  38. R. Paré and L. Román. Monoidal categories with Natural Numbers Object. Studia Logica, 48(3):361-376, Sep 1989. URL: http://dx.doi.org/10.1007/BF00370829.
  39. Maciej Piróg. Eilenberg-Moore monoids and backtracking monad transformers. In Proceedings 6th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2016, pages 23-56, 2016. URL: http://dx.doi.org/10.4204/EPTCS.207.2.
  40. B. Plotkin. Universal Algebra, Algebraic Logic, and Databases. Springer, 1994. Google Scholar
  41. J. Power. Enriched Lawvere theories. Theory and Applications of Categories, 6:83-93, 1999. Google Scholar
  42. E. Rivas, M. Jaskelioff, and T. Schrijvers. From monoids to near-semirings: The essence of MonadPlus and Alternative. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming. ACM, 2015. Google Scholar
  43. R. M. Robinson. Primitive recursive functions. Bull. Amer. Math. Soc., 53(10):925-942, 10 1947. Google Scholar
  44. J. M. Spivey. Algebras for combinatorial search. J. Funct. Program., 19(3-4):469-487, 2009. URL: http://dx.doi.org/10.1017/S0956796809007321.
  45. S. Szawiel and M. Zawadowski. The web monoid and opetopic sets. Journal of Pure and Applied Algebra, 217:1105-1140, 2013. URL: http://dx.doi.org/10.1016/j.jpaa.2012.09.030.
  46. T. Uustalu. A divertimento on MonadPlus and nondeterminism. Journal of Logical and Algebraic Methods in Programming, 85(5):1086-1094, 2016. URL: http://dx.doi.org/10.1016/j.jlamp.2016.06.004.
  47. W. G. Van Hoorn and B. Van Rootselaar. Fundamental notions in the theory of seminearrings. Compositio Mathematica, 18(1-2):65-78, 1967. Google Scholar
  48. H. Wolff. Monads and monoids on symmetric monoidal closed categories. Archiv der Mathematik, 24(1):113-120, 1973. URL: http://dx.doi.org/10.1007/BF01228184.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact