Functorial Semantics for Partial Theories

TL;DR

This paper introduces a Lawvere-style framework for partial theories with partially defined operations, enabling equational reasoning and preserving well-behaved semantics, demonstrated through examples like partial combinatory algebras.

Contribution

It extends classical equational theories to include partial operations using string diagrams, providing a syntactic and semantic foundation for reasoning about partial models.

Findings

Categories of models are locally finitely presentable

Free models exist for partial theories

Framework applies to partial combinatory algebras and cartesian closed categories

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.