Representing Knowledge and Querying Data using Double-Functorial Semantics (Lambert & Patterson, 2024)

Lambert & Patterson (2024): Representing Knowledge and Querying Data using Double-Functorial Semantics

Bibliographic Reference

Lambert, M., & Patterson, E. (2024). Representing knowledge and querying data using double-functorial semantics. In D. Jaz Myers & M. Johnson (Eds.), International Conference on Applied Category Theory 2024 (ACT 2024). EPTCS 429, pp. 174–189. https://doi.org/10.4204/EPTCS.429.9

Core Argument

Category theory offers a mathematical foundation for knowledge representation. Existing approaches model databases as functors into Set (functional ologs: Spivak & Kent, 2012) or as 2-functors into Rel (relational ologs: Patterson, 2017). This paper unifies both approaches by introducing double-categorical ologs (double ologs): a schema is a small double category equipped with cartesian equipment structure, and an instance is a structure-preserving double functor D → Rel.

The key unification: a double olog has all four elements of a logic fibered over a type theory — types (objects), terms (vertical arrows/functions), predicates (horizontal proarrows/relations), and judgments (cells/implications between predicates). Functional ologs are missing predicates and judgments; relational ologs are missing terms. The double olog gives both first-class status.

Critically for the wiki: the three basic operations of Codd’s relational algebra — selection (project columns), filtering (WHERE clause), and inner joins — appear directly as operations in a double category of relations (extensions, restrictions, and local products). As the paper’s slogan states: querying is double-functorial semantics.

Methods

The paper develops its framework in an accessible, example-driven style using the Stargate SG-1 universe as a running example. The formal backbone is Lambert’s (2022) “double categories of relations” — locally posetal cartesian equipments satisfying a discreteness (Frobenius) axiom. Key technical components:

• Cartesian equipment: finitely complete double category where the source-target projection D₁ → D₀ × D₀ is a bifibration, giving rise to restriction and extension cells
• Tabulators: right adjoint to the external identity functor, providing comprehension — associating a type to each proarrow (automatic subtype construction)
• Local products: binary products in hom-categories, computing conjunction of relations and inner joins without external machinery
• Discreteness axiom: ensures the horizontal bicategory is compact closed, giving a good notion of partial maps via the condition R† ⊗ R ≤ id

Appendix A provides rigorous background on double category theory, including a new characterization of partial maps (Theorem A.1): in a unit-pure double category of relations with tabulators, a proarrow is a partial map iff its tabulator span has monic domain arrow.

Key Findings

1. Double ologs unify functional and relational approaches. A double olog possesses types, terms, predicates, and judgments natively — the full logical fibered-over-type-theory structure that neither functional nor relational ologs alone can provide. “By contrast, a functional olog is missing predicates and judgments, whereas a relational olog is missing terms” (§1).

2. Queries are formulated internally to the schema. Unlike Spivak’s (2012) functorial data migration, which handles queries externally through adjoint triples between copresheaf categories, double-categorical queries use the primitive operations of a double category of relations: extensions for column projection, restrictions for row filtering, and local products for inner joins. These map directly to Codd’s relational algebra primitives (§3).

3. Tabulators enable type creation from relations. A proarrow (relation) can be reified as a subtype via its tabulator — e.g., from the relation “is hosted” (person ⇝ symbiote), derive the type “hosts” (the comprehension of those persons who have hosted). This is the formal analogue of SQL’s CREATE TYPE from a query result (§2.2).

4. Local products express inner joins without external machinery. The inner join of two relations along a shared type is computed as a restriction of their cartesian product along a diagonal morphism — an operation internal to the double category. This avoids the external adjoint-functor machinery of Spivak’s approach and directly mirrors the relational algebra JOIN operation (§3.3, Appendix A.2).

5. Partial maps are formally characterized. In a unit-pure double category of relations with tabulators, a proarrow R: A ⇝ B is a partial map iff R† ⊗ R ≤ id_B holds — a condition equivalent to the domain arrow of the tabulator span being monic (Theorem A.1). This provides a categorical criterion for distinguishing partial functions from general relations (§2.2, Appendix A.3).

Concepts Introduced or Used

Concept	Status	Definition
Double olog	New	A small double category of relations — a locally posetal cartesian equipment with discreteness axiom, optionally with tabulators
Functional olog	Existing (Spivak & Kent, 2012)	A small category with finite limits and colimits; instance = set-valued functor
Relational olog	Existing (Patterson, 2017)	A small bicategory of relations; instance = structure-preserving 2-functor into Rel
Double category of relations	Existing (Lambert, 2022)	A locally posetal cartesian equipment satisfying a discreteness/Frobenius axiom
Equipment	Existing (Shulman, 2008)	A double category where the source-target projection is a bifibration
Tabulator	Existing (Grandis, 2019)	Right adjoint to the external identity functor; comprehension of a proarrow as an object
Extension cell	Existing	Opcartesian cell in an equipment; computes image/column projection in Rel
Restriction cell	Existing	Cartesian cell in an equipment; computes pullback/row filtering in Rel
Local product	Existing (Patterson, 2024)	Binary product in a hom-category; computes conjunction of relations and inner joins
Partial map	Existing (Carboni & Walters, 1987)	A proarrow R satisfying R† ⊗ R ≤ id; a relation that is functional and injective on its domain

Entities Referenced

• Michael Lambert — University of Massachusetts-Boston. Originator of “double categories of relations” (2022).
• Evan Patterson — Topos Institute. Originator of “relational ologs” (2017) and “products in double categories, revisited” (2024).
• David Spivak — Topos Institute. Originator of functional ologs (with Kent, 2012) and functorial data migration (2012).
• ACT 2024 — International Conference on Applied Category Theory 2024. Venue for this paper.
• Topos Institute — Research institute for applied category theory. Affiliated with Patterson and Spivak.

Limitations (as stated by authors)

1. No implementation exists. “Design considerations for an engineered system have not been addressed” (§4). A query language, evaluation algorithms, and SQL reduction are all future work.
2. Data attributes not yet supported. Types valued in fixed types (strings, dates) are not formalized; “at least one [approach] should be adapted to double-categorical databases” (§4).
3. Aggregation not supported. “It should be investigated whether our functorial approach to querying can be extended to support aggregation” (§4). SUM, COUNT, AVG, GROUP BY are absent.
4. Short conference paper. 16 pages including references and appendix; the core examples are illustrative rather than exhaustive.
5. No treatment of cross-domain mappings. The paper addresses single-domain knowledge representation and querying; functors between double ologs are not discussed.

Relevance to Clonal Evolution

This paper is directly relevant to the wiki’s olog program for three reasons:

1. Our ologs are functional-only. The cancer evolution, ecology invasion, and compression progress ologs are all built on Spivak & Kent (2012) functional ologs. This forces arrows that are inherently relational (e.g., metastasizes, invades, enables, predicts, decompresses) into functional form. Lambert & Patterson (2024) provides the formalism to give these relational arrows proper first-class status as proarrows.

2. Our commutativity conditions are prose, not formal structure. The 24 commutativity conditions across the three domain ologs exist outside the category — English descriptions of what should commute. In a double olog, commutativity conditions become cells (2-morphisms), which are composable, verifiable, and preserved by double functors. The cross-domain framework’s central claim — that ecological invasion and compression progress map onto cancer evolution — would become a formal claim about double-functorial preservation of logical structure.

3. Our cross-domain functors are 1-functors between functional ologs. F: Ecology→Cancer, G: Compression→Cancer, and H: Ecology→Compression are defined at the wrong structural level. They should be double functors preserving not just functional composition but also relational structure and logical implications (cells). The paper’s core methodology — querying is double-functorial semantics — is the formal basis for upgrading the wiki’s functorial framework.

A detailed gap analysis is recorded in the context anchor for 2026-07-06 and in [[cross-domain-functors]] §Double-Categorical Enrichment.

---

Revision history

• 2026-07-06 — Source summary created. Evidence level VII (conference paper, peer-reviewed). Verification: DOI resolves (10.4204/EPTCS.429.9), published in EPTCS 429 (indexed proceedings). Key claims verified against PDF: unification claim (§1), query primitives mapping to relational algebra (§3), tabulators for type creation (§2.2), local products for inner joins (§3.3, Appendix A.2), partial maps characterization (Theorem A.1). No factual discrepancies. (lambert2024-double-functorial-semantics)