Day algebras

Reference. Day algebras

In this paper we show that the Day monoidal product generalises in a straightforward way to other algebraic constructions and partial algebraic constructions on categories. This generalisation was motivated by its applications in logic, for example in hybrid and separation logic. We use the description of the Day monoidal product using profunctors to show that the definition generalises to an extension of an arbitrary algebraic structure on a category to a pseudo-algebraic structure on a functor category. We provide two further extensions. First we consider the case where some of the operations on the category are partial, and second we show that the resulting operations on the functor category have adjoints (they are residuated).

Cite

Cite as @robinson_wrigley_2026 (helia, typst) · \cite{robinson_wrigley_2026} (LaTeX)

BibTeX

bibtex · 13 lines

@article{robinson_wrigley_2026,
 title = {Day algebras},
 author = {Robinson, Edmund and Wrigley, Joshua},
 year = {2026},
 doi = {10.1017/S0960129525100221},
 url = {https://arxiv.org/abs/2504.06200},
 journal = {Mathematical Structures in Computer Science},
 volume = {36},
 pages = {e6},
 note = {arXiv:2504.06200v2 [math.CT], 10 Dec 2025},
 eprint = {2504.06200},
 archiveprefix = {arXiv}
}

hayagriva YAML (typst)

yaml · 17 lines

robinson_wrigley_2026:
  type: article
  title: Day algebras
  author:
  - Robinson, Edmund
  - Wrigley, Joshua
  date: 2026
  page-range: e6
  url: https://arxiv.org/abs/2504.06200
  serial-number:
    arxiv: '2504.06200'
    doi: 10.1017/S0960129525100221
  note: arXiv:2504.06200v2 [math.CT], 10 Dec 2025
  parent:
    type: periodical
    title: Mathematical Structures in Computer Science
    volume: 36

Download: robinson_wrigley_2026.bib · robinson_wrigley_2026.yml

Cited by (1)

Definition. Types over an Algebraic Theory theory-type

Fix a finitary algebraic theory $𝒯︀$ : sorts $𝑆$ , a signature $𝜎$ , equations, and a set $𝑉$ of generators. Write $𝑴$ for the free $𝒯︀$ -model on $𝑉$ and $| 𝑴 |_{𝑠}$ for its carrier at sort $𝑠$ .

A $𝒯︀$ -type of sort $𝑠$ is a family $𝐴 : | 𝑴 |_{𝑠} \to 𝖳𝗒𝗉𝖾$ .

For $𝒯︀$ -types $𝐴$ and $𝐵$ of sort $𝑠$ we have the additives, defined pointwise,

(𝐴 & 𝐵) (𝑚) = 𝐴 (𝑚) \times 𝐵 (𝑚), (𝐴 \oplus 𝐵) (𝑚) = 𝐴 (𝑚) + 𝐵 (𝑚), (𝐴 \Rightarrow 𝐵) (𝑚) = 𝐴 (𝑚) \to 𝐵 (𝑚),

along with $⊤$ , $⊥$ , and their indexed versions.

Each operation $𝑜 : 𝑠_{0}, \dots, 𝑠_{𝑛 - 1} \to 𝑠$ of $𝒯︀$ gives a multiplicative, defined by Day convolution,

\otimes [𝑜] (𝐴_{0}, \dots, 𝐴_{𝑛 - 1}) (𝑚) = Σ_{𝑜 (𝑚_{0}, \dots, 𝑚_{𝑛 - 1}) = 𝑚} \times Π_{𝑖 < 𝑛} 𝐴_{𝑖} (𝑚_{𝑖}) .

Each lifted operation also has closed structure: a residual in each of its arguments. Day algebras [1] give a more general convolutional definition.

When $𝒯︀$ is the theory of monoids and $𝑉$ is an alphabet, $𝒯︀$ -types are formal grammars. Multiplication gives $\otimes$ , the unit gives $𝜀$ , and we recover Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ .

Cites 27 works (4 here)

With notes (4)

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002

In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.

DOI

BI as an assertion language for mutable data structures ishtiaq_ohearn_bi_2001POPL · 2001

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O’Hearn and Pym. We begin by giving a model in which the law of the excluded middle holds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI’s spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triples that allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don’t change, to be inferred automatically.

PDF · DOI · pldb

The logic of bunched implications ohearn_pym_bi_1999BSL · 1999

We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI’s proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers [inline image] and [inline image] which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

Categories for the Working Mathematician maclane_19711971

Web

External (23)

Two-dimensional Kripke Semantics I: Presheaves (2024)
(Co)end Calculus (2021)
Reasoning over Permissions Regions in Concurrent Separation Logic (2020)
Separation logic (2019)
Free skew monoidal categories (2018)
Henkin and Hybrid Logic (2014)
Skew-monoidal categories and bialgebroids (2012)
Hybrid Logic and its Proof-Theory (2011)
Possible worlds and resources: the semantics of BI (2004)
Higher Operads, Higher Categories (2004)
Logic in computer science - modelling and reasoning about systems (2. ed.) (2004)
Lax monoids, pseudo-operads, and convolution (2003)
Local Reasoning about Programs that Alter Data Structures (2001)
Modal Logic (Chagrov, Zakharyaschev; Oxford Logic Guides 35) (1997)
Topoi: the Categorial Analysis of Logic (1984)
Relations et carrés exacts (1980)
The temporal logic of programs (1977)
On closed categories of functors II (1974)
On closed categories of functors (1970)
Introduction to bicategories (1967)
On MacLane's conditions for coherence of natural associativities, commutativities, etc (1964)
Residuated lattices (1939)
Operads in 2-categories and models of structure interchange