Functorial semantics for partial theories
Ivan Di Liberti, Fosco Loregiàn, Chad Nester, Pawel Sobocinski
Abstract
. 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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers2
- Evidential Decision Theory via Partial Markov CategoriesElena Di Lavore, Mario RománLICS 2023 · 7 citations
- Incremental Certified ProgrammingTomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric TanterOOPSLA 2025
Related papers
- Algebraic models of simple type theories: A polynomial approachNathanael Arkor, Marcelo FioreLICS 2020 · 10 citations
- Bialgebraic Reasoning on Higher-order Program EquivalenceSergey Goncharov, Stefan Milius, Stelios Tsampas, Henning UrbatLICS 2024 · 4 citations
- Parametricity and Semi-Cubical TypesHugo MoeneclaeyLICS 2021
- A Syntax for Strictly Associative and Unital ∞-CategoriesEric Finster, Alex Rice, Jamie VicaryLICS 2024
- TensorRocq: Enabling Diagrammatic Reasoning in RocqBen Caldwell, William Spencer, Aleks Kissinger, Robert RandOOPSLA 2026
