Representing Knowledge and Querying Data using Double-Functorial Semantics

Introduction

This section discusses the application of category theory to knowledge representation and databases. The ontology or database schema is represented as a small category, and instance data is a structure-preserving functor from the schema into a category like Set.

Knowledge representation emphasizes rich schemas and expressive languages (categorical structure), while databases focus on data instances and transformations between them. The paper introduces the concept of a "double olog," which is a small double category of relations with specific properties. An instance of a double olog is a structure-preserving double functor into the double category of sets, functions, relations, and implications (Rel).

Compared to previous approaches like functional and relational ologs, double ologs recognize functions and relations as fundamental concepts and grant them equal status. They possess the four elements of a logic fibered over a type theory: objects as types, arrows as terms, proarrows as predicates, and cells as judgments or implications.

Double ologs allow queries on instance data to be formulated internally within the schema, rather than through external mappings. Basic operations of relational algebra (permutations, projections, joins) appear directly as operations in the double category of relations.

The paper aims to explain the features of double ologs through an accessible, example-driven style, while also providing technical definitions for readers familiar with double category theory.

Representing Knowledge

The section discusses how double categories can enhance the expressive power of ologs (ontology logs) beyond functional or relational ologs. It shows how facts can be expressed using commutative diagrams, and how individual constants like people can be included. It demonstrates expressing one-to-many relationships like a Jaffa's past or current service as First Prime to System Lords using relations rather than functions.

The section then explains how tabulators allow creating new types from relations, such as the type of all people who have hosted a symbiote. Local products allow forming conjunctions of propositions, illustrated with an example about whether people's expertise matches their team's mission. The local product identifies people whose skills fit their assigned remit.

Overall, the section highlights how double categories with relations, tabulators, and local products increase the expressiveness of ologs compared to just functional or relational structures alone.

Querying Data

The provided section discusses how various database operations like select, filter, and join can be expressed in the framework of double categories of relations.

Select is performed by taking an extension along projection morphisms to retrieve desired columns from a relation table.

Filter is achieved by taking restrictions, isolating rows that satisfy a given criteria like a specific attribute value.

Inner join of two tables is computed as a pullback, taking the cartesian product of the two tables and matching on the shared column(s) to combine information across relations.

The operations are illustrated with concrete examples and data tables. The key idea is that querying corresponds to composing the basic operations of extension, restriction, and product available in double categories of relations. This provides an internal way to express queries within the schema instead of handling them externally.

Appendix A Background on Double Category Theory

This appendix reviews background on double category theory and proves a new characterization of partial maps in a "double category of relations."

A double category of relations is a double category that is cartesian, an equipment, and satisfies a discreteness condition. It has finite products, and the source-target projection functor is a bifibration, allowing cells to be completed to cartesian or opcartesian cells (restrictions and extensions).

Local products of proarrows can be constructed by restricting products of relations along diagonals. Inner joins match two relations along a common domain.

A partial map is characterized by the condition R^†⊗R ≤ id_B, where R^† is the reverse relation of R. This forces the domain projection d of R to be monic, making the span (d, c) a genuine partial map.

In a unit-pure double category of relations with tabulators, a proarrow r is a partial map if and only if the domain d of the tabulator of r is monic. This generalizes the previous characterization using the reverse relation condition.