2020/11/12 by Ivan Di Liberti, Fosco Loregian, Chad Nester +1 · 8 citations
Computer Science · Mathematics · #Algebra over a field #Cartesian closed category #Class (philosophy) #Expressivity #Homotopy and Cohomology in Algebraic Topology #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Partial function #Semantics (computer science) #String (physics) #Universal algebra #cs.LO #math.CT #msc:03C05 #msc:18B10 #msc:18C10 #msc:18C35
paper · pdf · doi:10.1145/3434338
published in Proceedings of the ACM on Programming Languages 5(POPL), 1-28 (Association for Computing Machinery) · 27 pages
arxiv created 2020/11/12 · arxiv updated 2020/11/16 · openalex created_date 2020/11/23 · openalex publication_date 2021/01/04 · openalex updated_date 2026/08/05
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.