ABSTRACT
Distributive laws give a way of combining two algebraic structures expressed as monads; in this paper we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from ${\mathbf {Cat}}$ to $\mathbf {Prof}$, and factorisation systems respectively. We exhibit comparison functors between $\mathbf {CAT}$ and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws.
► BibTeX data
► References
[1] T. Altenkirch, J. Chapman and T. Uustualu. Monads need not be endofunctors. Ong L. (Eds) Foundations of Software Science and Computational Structures, FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. Also E-print 1412.7148. https://doi.org/10.1007/978-3-642-12032-9_21.
https://doi.org/10.1007/978-3-642-12032-9_
[2] J. Beck. Distributive laws. Lecture Notes in Mathematics, 80:119–140, 1969. https://doi.org/10.1007/BFb0083084.
https://doi.org/10.1007/BFb0083084
[3] J. Bénabou. Les distributeurs. Université Catholique de Louvain, Institut de Mathématique Pure et Appliquée, rapport 33, 1973.
[4] F. Bonchi, P. Sobociński, F. Zanasi Deconstructing Lawvere with distributive laws. Journal of Logical and Algebraic Methods in Programming, 95:128–146, 2018. https://doi.org/10.1016/j.jlamp.2017.12.002.
https://doi.org/10.1016/j.jlamp.2017.12.002
[5] E. Cheng. Iterated distributive laws. Mathematical Proceedings of the Cambridge Philosophical Society, 150(3):459–487, 2011. Also E-print 0710.1120. http://doi.org/10.1017/S0305004110000599.
https://doi.org/10.1017/S0305004110000599
[6] E. Cheng, M. Hyland, and J. Power. Pseudo-distributive laws. Electronic Notes in Theoretical Computer Science, 83, 2004. https://doi.org/10.1016/ S1571-0661(03)50012-3.
https://doi.org/10.1016/%20S1571-0661(03)50012-3
[7] M. Hyland. Elements of a theory of algebraic theories. Theoretical Computer Science, 546:132–144, 2014. Also E-print 1311.7642. https://doi.org/10.1016/j.tcs.2014.03.005.
https://doi.org/10.1016/j.tcs.2014.03.005
[8] M. Hyland and J. Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science, 172:437–458, 2007. https://doi.org/10.1016/j.entcs.2007.02.019.
https://doi.org/10.1016/j.entcs.2007.02.019
[9] S. Lack and J. Rosický. Notions of Lawvere theory. Applied Categorical Structures, 175(1):243–265, 2011. Special volume celebrating the 70th birthday of Professor Max Kelly. https://doi.org/10.1007/s10485-009-9215-2.
https://doi.org/10.1007/s10485-009-9215-2
[10] S. Lack. Composing PROPs. Theory and Applications of Categories, 13:147–163, 2004.
http://www.tac.mta.ca/tac/volumes/13/9/13-09abs.html
[11] F. W. Lawvere. Functional semantics of algebraic theories. PhD thesis, Columbia University, 1963. Also available as Theory and Applications of Ccategories, Reprint 5. https://doi.org/10.1073/pnas.50.5.869.
https://doi.org/10.1073/pnas.50.5.869
[12] F. E. J. Linton. Some aspects of equational theories. In Proc. Conf. on Categorical Algebra at La Jolla, pages 84–95, 1966. https://doi.org/10.1007/978-3-642-99902-4_3.
https://doi.org/10.1007/978-3-642-99902-4_
[13] E. Manes. Algebraic Theories. Springer, 1976. https://doi.org/10.1007/978-1-4612-9860-1.
https://doi.org/10.1007/978-1-4612-9860-1
[14] J. Power. Enriched Lawvere theories. Theory and Applications of Categories, 6(7):83–93, 1999.
http://www.tac.mta.ca/tac/volumes/6/n7/6-07abs.html
[15] E. Riehl, Factorization systems. Preprint available at http://www.math.jhu.edu/ eriehl/factorization.pdf.
http://www.math.jhu.edu/~eriehl/factorization.pdf
[16] R. Rosebrugh and R. Wood. Distributive laws and factorization. J. Pure Appl. Algebra, 175:327–353, 2002. https://doi.org/10.1016/S0022-4049(02)00140-8.
https://doi.org/10.1016/S0022-4049(02)00140-8
[17] R. Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2:149–168, 1972. https://doi.org/10.1016/0022-4049(72)90019-9.
https://doi.org/10.1016/0022-4049(72)90019-9
Cited by
[1] Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński, "Functorial semantics for partial theories", Proceedings of the ACM on Programming Languages 5 POPL, 1 (2021).
[2] Cole Comfort, "The ZX&-calculus: A complete graphical calculus for classical circuits using spiders", Electronic Proceedings in Theoretical Computer Science 340, 60 (2021).
The above citations are from Crossref's cited-by service (last updated successfully 2024-04-25 11:14:04). The list may be incomplete as not all publishers provide suitable and complete citation data.
On SAO/NASA ADS no data on citing works was found (last attempt 2024-04-25 11:14:04).
This Paper is published in Compositionality under the Creative Commons Attribution 4.0 International (CC BY 4.0) license. Copyright remains with the original copyright holders such as the authors or their institutions.