一句话：提出偏理论的 Lawvere 式句法定义，用弦图项给出等式推理，并证明其模型范畴恰为局部有限可表范畴。
论文为偏理论（允许部分定义运算的等式理论）给出 Lawvere 风格的范畴语义。传统等式理论假设运算处处有定义，难以直接刻画偏组合代数、笛卡尔闭范畴等结构。作者采用一类合适的弦图作为项，构造句法范畴，从而可对偏理论定义的模型类进行等式推理；同时证明所得模型范畴恰为局部有限可表范畴，并给出自由模型的存在性。多个例子展示了该框架的表达力，表明在增加句法表达力的同时仍保持性质良好的函子语义。
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.
@article{paperbot1144,
title = {Functorial semantics for partial theories},
author = {Ivan Di Liberti and Fosco Loregian and Chad Nester and Paweł Sobociński},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434338}
}