{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,12]],"date-time":"2026-10-12T18:24:14Z","timestamp":1791829454361,"version":"4.3.4"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["EXPRO 20-31529X and RVO: 67985840"],"award-info":[{"award-number":["EXPRO 20-31529X and RVO: 67985840"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000782","name":"European Science Foundation","doi-asserted-by":"publisher","award":["Estonian IT Academy research measure (project 2014-2020.4.05.19-0001)"],"award-info":[{"award-number":["Estonian IT Academy research measure (project 2014-2020.4.05.19-0001)"]}],"id":[{"id":"10.13039\/501100000782","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.<\/jats:p>","DOI":"10.1145\/3434338","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Functorial semantics for partial theories"],"prefix":"10.1145","volume":"5","author":[{"given":"Ivan","family":"Di Liberti","sequence":"first","affiliation":[{"name":"Czech Academy of Sciences, Czechia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fosco","family":"Loregian","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chad","family":"Nester","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pawe\u0142","family":"Soboci\u0144ski","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"J. Ad\u00e1mek F.W. Lawvere and J. Rosicky`. 2003. On the duality between varieties and algebraic theories. Algebra universalis 49 1 ( 2003 ) 35-49.","DOI":"10.1007\/s000120300002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"J. Adamek and J. Rosicky`. 1994. Locally Presentable and Accessible Categories. Cambridge University Press.","DOI":"10.1017\/CBO9780511600579"},{"key":"e_1_2_1_3_1","volume-title":"and E.M. Vitale","author":"Ad\u00e1mek J.","year":"2011","unstructured":"J. Ad\u00e1mek, J. Rosicky`, and E.M. Vitale. 2011. Algebraic theories. Cambridge Tracts in Mathematics 184 ( 2011 ), 1."},{"key":"e_1_2_1_4_1","unstructured":"I. Bethke. 1988. Notes on Partial Combinatory Algebras. Ph.D. Dissertation. Universiteit von Amsterdam."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9"},{"key":"e_1_2_1_7_1","unstructured":"F. Bonchi D. Pavlovic and P. Sobocinski. 2017. Functorial Semantics for Relational Theories. arXiv preprint arXiv:1711.08699 ( 2017 )."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"F. Bonchi P. Soboci\u0144ski and F. Zanasi. 2018. Deconstructing Lawvere with Distributive Laws. Journal of Logical and Algebraic Methods in Programming 95 ( 2018 ) 128-146. https:\/\/doi.org\/10.1016\/j.jlamp. 2017. 12.002 F. Borceux and D. Dejean. 1986. Cauchy completion in category theory. Cahiers de Topologie et G\u00e9om\u00e9trie Dif\u00e9rentielle Cat\u00e9goriques 27 2 ( 1986 ) 133-146.","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(91)90057-F"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"A. Carboni and R.F.C. Walters. 1987. Cartesian Bicategories I. Journal of Pure and Applied Algebra 49 ( 1987 ) 11-32.","DOI":"10.1016\/0022-4049(87)90121-6"},{"key":"e_1_2_1_11_1","unstructured":"C. Centazzo. 2004. Generalised Algebraic Models. Presses universitaires de Louvain. https:\/\/books.google.cz\/books?id= WKTk1n6ggKsC"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"C. Centazzo and E.M. Vitale. 2002. A duality relative to a limit doctrine. Theory and Applications of Categories 10 ( 2002 ) 486-497.","DOI":"10.70930\/tac\/satiqc1q"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"E. Cheng. 2020. Distributive laws for Lawvere theories. Compositionality 2 ( 2020 ) 1.","DOI":"10.32408\/compositionality-2-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"J.R.B. Cockett X. Guo and J.W Hofstra P. 2012. Range Categories II: towards regularity. Theory and Applications of Categories 26 ( 2012 ) 453-500.","DOI":"10.70930\/tac\/4gy91eot"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"J.R.B. Cockett and P.J.W. Hofstra. 2008. Introduction to Turing Categories. Annals of Pure and Applied Logic 156 ( 2008 ) 183-209.","DOI":"10.1016\/j.apal.2008.04.005"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"J.R.B. Cockett and S. Lack. 2002. Restriction Categories I: categories of partial maps. Theoretical Computer Science 270 ( 2002 ) 223-259.","DOI":"10.1016\/S0304-3975(00)00382-0"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"J.R.B. Cockett and S. Lack. 2007. Restriction Categories III: colimits partial limits and extensivity. Mathematical Structures in Computer Science 17 ( 2007 ) 775-817.","DOI":"10.1017\/S0960129507006056"},{"key":"e_1_2_1_18_1","first-page":"298","article-title":"Interacting Quantum Observables","volume":"08","author":"Coecke B.","year":"2008","unstructured":"B. Coecke and R. Duncan. 2008. Interacting Quantum Observables. In ICALP' 08. 298-310.","journal-title":"ICALP'"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"P.L. Curien and A. Obtu\u0142owicz. 1989. Partiality Cartesian Closedness and Toposes. Information and Computation 80 ( 1989 ) 50-95.","DOI":"10.1016\/0890-5401(89)90023-0"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"D. Dugger. 2001. Combinatorial model categories have presentations. Advances in Mathematics 164 1 ( 2001 ) 177-201.","DOI":"10.1006\/aima.2001.2015"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"T. Fox. 1976. Coalgebras and cartesian categories. Communications in Algebra 4 ( 1976 ) 665-667.","DOI":"10.1080\/00927877608822127"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4064\/cm-14-1-89-106"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"P. Freyd. 1972. Aspects of topoi. Bulletin of the Australian Mathematical Society 7 1 ( 1972 ) 1-76.","DOI":"10.1017\/S0004972700044828"},{"key":"e_1_2_1_24_1","unstructured":"P.J. Freyd and A. Scedrov. 1990. Categories allegories. North-Holland."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"P. Gabriel and F. Ulmer. 1971. Lokal pr\u00e4sentierbare Kategorien. Springer-Verlag Berlin. v+ 200 pages.","DOI":"10.1007\/BFb0059396"},{"key":"e_1_2_1_26_1","unstructured":"B. Giles. 2014. An Investigation of some Theoretical Aspects of Reversible Computing. Ph.D. Dissertation. The University of Calgary."},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"M. Hyland and J. Power. 2007. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science 172 ( 2007 ) 437-458.","DOI":"10.1016\/j.entcs.2007.02.019"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511615443"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"S. Lack. 2004. Composing PROPs. Theory and Applications of Categories 13 9 ( 2004 ) 147-163.","DOI":"10.70930\/tac\/py4jt3en"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-99902-4_3"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30362-3"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"S. Mac Lane. 1965. Categorical algebra. Bull. Amer. Math. Soc. 71 1 ( 1965 ) 40-106.","DOI":"10.1090\/S0002-9904-1965-11234-4"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/104"},{"key":"e_1_2_1_35_1","unstructured":"E. Palmgren. 2009. Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"E. Palmgren and S.J. Vickers. 2007. Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic 145 ( 2007 ) 314-353.","DOI":"10.1016\/j.apal.2006.10.001"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"D. Pavlovic. 2013. Monoidal Computer I: Basic Computability by String Diagrams. Information and Computation 226 ( 2013 ) 94-116.","DOI":"10.1016\/j.ic.2013.03.007"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"J. Power. 2006. Countable Lawvere theories and computational efects. Electronic Notes in Theoretical Computer Science 161 ( 2006 ) 59-71.","DOI":"10.1016\/j.entcs.2006.04.025"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"E.P. Robinson and G. Rosolini. 1988. Categories of Partial Maps. Information and Computation 79 ( 1988 ) 94-130.","DOI":"10.1016\/0890-5401(88)90034-X"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434338","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434338","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:26:47Z","timestamp":1781854007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434338"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434338"],"URL":"https:\/\/doi.org\/10.1145\/3434338","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}