Question. Has this proposal (or anything like it) for a category of partial $\mathsf{T}$-algebras been considered anywhere, and if so, where, and if not, does it have any obvious flaws or deficits?

Let $\mathsf{T}$ denote a Lawvere theory with generating object $\Box$.

I was thinking that a reasonable definition of "partial $\mathsf{T}$-algebra" might go something like this.

Firstly, let $\mathbf{PSet}$ denote the category of pointed sets. View $\mathbf{PSet}$ as a symmetric monoidal category with $\otimes$ as smash product, and note that there's reasonable-looking choices for projection maps like $X \otimes Y \rightarrow X$ and diagonals like $X \rightarrow X\otimes X$.

Secondly, define that a morphism of pointed sets $f : (X,\bot_X) \rightarrow (X,\bot_Y)$ is tight iff $f^{-1}(\bot_Y) = \{\bot_X\}$. See here for relevant nonsense.

Thirdly, make $\mathbf{PSet}$ into a (thin) $2$-category by defining that for each pair of morphisms $$f,g : (X,\bot_X) \rightarrow (Y,\bot_Y),$$ we have $f \leq g$ iff $$\forall x \in X(f(x) \neq \bot_Y \rightarrow f(x)=g(x)).$$

Fourthly, define that a partial $\mathsf{T}$-algebra is an oplax functor $F : \mathsf{T} \rightarrow \mathbf{PSet}$ with data $F(\Box^n) \cong (F\Box)^{\otimes n}$, and which turns each canonical projection $\pi_i : \Box^n \rightarrow \Box$ into the corresponding canonical projection $\pi_i:(F\Box)^{\otimes n} \rightarrow F\Box$ and the same for the diagonals.

And fifthly, define that a morphism $X \rightarrow Y$ of partial $\mathsf{T}$-algebras is just a lax natural transformation $f:X \rightarrow Y$ whose component at $\Box$ is tight. By "lax", mean that $$f_\Box \circ X(j) \leq Y(j) \circ f_{{\Box}^{\otimes n}}.$$

It would be nice, for example, if the partial $\mathsf{T}$-algebras for $\mathsf{T}$ equal to the Lawvere theory of commutative monoids were precisely the partial commutative monoids. This is probably too much to hope for, but at least its a guiding example.

  • 1
    $\begingroup$ Are you looking for (a) an analogue of Lawvere theories which allows some operations to be partial, or are you looking for (b) models of ordinary Lawvere theories in categories of partial maps? $\endgroup$ – Andrej Bauer Aug 25 '16 at 17:58
  • $\begingroup$ Isn't pointed sets with smash product a non-cartesian monoidal category? In particular the ordinary cartesian product is the product in the category of pointed sets (cf mathoverflow.net/questions/36810/…). So I wonder how you define the projections. $\endgroup$ – David Roberts Aug 25 '16 at 23:22
  • 1
    $\begingroup$ @AndrejBauer, what I've tried to define is (b). But since any answer to (a) is likely to also yield an answer to (b), hence by extension, I'm interested in (a). $\endgroup$ – goblin Aug 26 '16 at 6:12
  • $\begingroup$ @DavidRoberts, there's a unique morphism of pointed sets $\pi_0 : X \otimes Y \rightarrow X$ such that for all $x \in X$ and $y \in Y_{\neq \bot}$, we have $\pi_0(x \otimes y) = x$. So we can define projection morphisms from a smash product in a sensible way. This won't make $\mathbf{PSet}$ into a cartesian monoidal category, but we can nonetheless define them. Does that answer your question? $\endgroup$ – goblin Aug 26 '16 at 6:14
  • $\begingroup$ So the obvious problem here is tha categories of partial maps that you are considering do not have products, or else there would be nothing to do. $\endgroup$ – Andrej Bauer Aug 26 '16 at 8:15

The closest reference to what you are asking for that I know is

Erik Palmgren and Steve Vickers: Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic. Volume 145, Issue 3, March 2007, Pages 314-353. (DOI, PDF)

To get the universal partial algebra going one has to address partiallity in a serious way. For instance, it matters how complicated the domains of definition may be, or to put it another way, what is the language for expressing definedness conditions? The above paper addresses this, which is why it the title talks about "Horn logic" but is really (also) about universal partial algebra.

Another place to look is essentially algebraic theories.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.