# Categorical algebra

## FinSet and FinRel

The following APIs implement FinSet, the category of Finite Sets (actually the skeleton of FinSet). The objects of this category are natural numbers where `n`

represents a set with `n`

elements. The morphisms are functions between such sets. We use the skeleton of FinSet in order to ensure that all sets are finite and morphisms can be stored using lists of integers. Finite relations are built out of FinSet and can be used to do some relational algebra.

`Catlab.CategoricalAlgebra.FinSets`

— ModuleThe category of finite sets and functions, and its skeleton.

`Catlab.CategoricalAlgebra.FinSets.FinDomFunction`

— TypeFunction out of a finite set.

This class of functions is convenient because it is exactly the class that can be represented explicitly by a vector of values from the codomain.

`Catlab.CategoricalAlgebra.FinSets.FinFunction`

— TypeFunction between finite sets.

The function can be defined implicitly by an arbitrary Julia function, in which case it is evaluated lazily, or explictly by a vector of integers. In the vector representation, the function (1↦1, 2↦3, 3↦2, 4↦3), for example, is represented by the vector [1,3,2,3].

This type is mildly generalized by `FinDomFunction`

.

`Catlab.CategoricalAlgebra.FinSets.FinSet`

— TypeFinite set.

This generic type encompasses the category **FinSet** of finite sets and functions, through types `FinSet{S} where S <: AbstractSet`

, as well as the skeleton of this category, through the type `FinSet{Int}`

. In the latter case, the object `FinSet(n)`

represents the set ${1,...,n}$.

`Catlab.CategoricalAlgebra.FinSets.HashJoin`

— TypeHash join algorithm.

`Catlab.CategoricalAlgebra.FinSets.JoinAlgorithm`

— TypeAlgorithm for limit of spans or multispans out of finite sets.

In the context of relational databases, such limits are joins.

`Catlab.CategoricalAlgebra.FinSets.NestedLoopJoin`

— TypeNested-loop join algorithm.

This is the naive algorithm for computing joins.

`Catlab.CategoricalAlgebra.FinSets.SmartJoin`

— TypeMeta-algorithm for joins that attempts to pick an appropriate algorithm.

`Catlab.CategoricalAlgebra.FinSets.SortMergeJoin`

— TypeSort-merge join algorithm.

`Catlab.CategoricalAlgebra.FinSets.SubFinSet`

— TypeSubset of a finite set represented as an inclusion map.

`Catlab.CategoricalAlgebra.FinSets.SubOpBoolean`

— TypeAlgorithm to compute subobject operations using elementwise boolean logic.

`Catlab.CategoricalAlgebra.FinSets.force`

— MethodForce evaluation of lazy function or relation.

`Catlab.CategoricalAlgebra.FinSets.is_indexed`

— MethodWhether the given function is indexed, i.e., supports efficient preimages.

`Catlab.CategoricalAlgebra.FinSets.preimage`

— MethodThe preimage (inverse image) of the value y in the codomain.

`Catlab.CategoricalAlgebra.FinRelations`

— ModuleThe category of finite sets and relations, and its skeleton.

`Catlab.CategoricalAlgebra.FinRelations.BoolRig`

— TypeThe rig of booleans.

This struct is needed because in base Julia, the product of booleans is another boolean, but the sum of booleans is coerced to an integer: `true + true == 2`

.

`Catlab.CategoricalAlgebra.FinRelations.FinRel`

— TypeObject in the category of finite sets and relations.

See also: `FinSet`

.

`Catlab.CategoricalAlgebra.FinRelations.FinRelation`

— TypeBinary relation between finite sets.

A morphism in the category of finite sets and relations. The relation can be represented implicitly by an arbitrary Julia function mapping pairs of elements to booleans or explicitly by a matrix (dense or sparse) taking values in the rig of booleans (`BoolRig`

).

`Catlab.CategoricalAlgebra.FinRelations.FinRelationCallable`

— TypeRelation in FinRel defined by a callable Julia object.

`Catlab.CategoricalAlgebra.FinRelations.FinRelationMatrix`

— TypeRelation in FinRel represented by a boolean matrix.

Boolean matrices are also known as logical matrices or relation matrices.

## Diagrams, Limits, and Colimts

The following modules define diagrams in an arbitrary category and specify limit and colimt cones over said diagrams. Thes constructions enjoy the fullest support for FinSet and are used below to define presheaf categories as C-Sets. The general idea of these functions is that you set up a limit computation by specifying a diagram and asking for a limit or colimit cone, which is returned as a struct containing the apex object and the leg morphisms. This cone structure can be queried using the functions `apex`

and `legs`

. Julia's multiple dispatch feature is heavily used to specialize limit and colimit computations for various diagram shapes like product/coproduct and equalizer/coequalizer. As a consumer of this API, it is highly recommended that you use multiple dispatch to specialize your code on the diagram shape whenever possible.

`Catlab.CategoricalAlgebra.FreeDiagrams`

— ModuleFree diagrams in a category.

A free diagram in a category is a diagram whose shape is a free category. Examples include the empty diagram, pairs of objects, discrete diagrams, parallel morphisms, spans, and cospans. Limits and colimits are most commonly taken over free diagrams.

`Catlab.CategoricalAlgebra.FreeDiagrams.BipartiteFreeDiagram`

— TypeA free diagram that is bipartite.

Such diagrams include most of the fixed shapes, such as spans, cospans, and parallel morphisms. They are the generic shape of diagrams for limits and colimits arising from undirected wiring diagrams. For limits, the boxes correspond to vertices in $V₁$ and the junctions to vertics in $V₂$. Colimits are dual.

`Catlab.CategoricalAlgebra.FreeDiagrams.Cospan`

— TypeCospan of morphisms in a category.

A common special case of `Multicospan`

. See also `Span`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.DiscreteDiagram`

— TypeDiscrete diagram: a diagram whose only morphisms are identities.

`Catlab.CategoricalAlgebra.FreeDiagrams.FixedShapeFreeDiagram`

— TypeAbstract type for free diagram of fixed shape.

`Catlab.CategoricalAlgebra.FreeDiagrams.Multicospan`

— TypeMulticospan of morphisms in a category.

A multicospan is like a `Cospan`

except that it may have a number of legs different than two. A limit of this shape is a pullback.

`Catlab.CategoricalAlgebra.FreeDiagrams.Multispan`

— Type`Catlab.CategoricalAlgebra.FreeDiagrams.ParallelMorphisms`

— TypeParallel morphims in a category.

Parallel morphisms are just morphisms with the same domain and codomain. A (co)limit of this shape is a (co)equalizer.

For the common special case of two morphisms, see `ParallelPair`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.ParallelPair`

— TypePair of parallel morphisms in a category.

A common special case of `ParallelMorphisms`

.

`Catlab.CategoricalAlgebra.FreeDiagrams.Span`

— Type`Catlab.CategoricalAlgebra.FreeDiagrams.apex`

— Method`apex(span::Multispan)`

returns the object at the top of the multispan, which is the domain of all the legs.

`Catlab.CategoricalAlgebra.FreeDiagrams.bundle_legs`

— MethodBundle together legs of a multi(co)span.

For example, calling `bundle_legs(span, SVector((1,2),(3,4)))`

on a multispan with four legs gives a span whose left leg bundles legs 1 and 2 and whose right leg bundles legs 3 and 4. Note that in addition to bundling, this function can also permute legs and discard them.

The bundling is performed using the universal property of (co)products, which assumes that these (co)limits exist.

`Catlab.CategoricalAlgebra.FreeDiagrams.feet`

— Method`feet(span::Multispan)`

returns the collection of feet in the multspan, which are the codomains of the legs.

`Catlab.CategoricalAlgebra.FreeDiagrams.legs`

— Method`legs(span::Multispan)`

returns the collection of legs in the multspan, which are the morphisms sharing a common domain.

`Catlab.CategoricalAlgebra.Limits`

— ModuleLimits and colimits in a category.

`Catlab.CategoricalAlgebra.Limits.AbstractColimit`

— TypeAbstract type for colimit in a category.

The standard concrete subtype is `Colimit`

, although for computational reasons certain categories may use different subtypes to include extra data.

`Catlab.CategoricalAlgebra.Limits.AbstractLimit`

— TypeAbstract type for limit in a category.

The standard concrete subtype is `Limit`

, although for computational reasons certain categories may use different subtypes to include extra data.

`Catlab.CategoricalAlgebra.Limits.Colimit`

— TypeColimit in a category.

`Catlab.CategoricalAlgebra.Limits.ColimitAlgorithm`

— TypeAlgorithm for computing colimits.

`Catlab.CategoricalAlgebra.Limits.ComposeCoproductCoequalizer`

— TypeCompute pushout by composing a coproduct with a coequalizer.

See also: `ComposeProductEqualizer`

.

`Catlab.CategoricalAlgebra.Limits.ComposeProductEqualizer`

— TypeCompute pullback by composing a product with an equalizer.

See also: `ComposeCoproductCoequalizer`

.

`Catlab.CategoricalAlgebra.Limits.Limit`

— TypeLimit in a category.

`Catlab.CategoricalAlgebra.Limits.LimitAlgorithm`

— TypeAlgorithm for computing limits.

`Catlab.CategoricalAlgebra.Limits.colimit`

— FunctionColimit of a diagram.

To define colimits in a category with objects `Ob`

, override the method `colimit(::FreeDiagram{Ob})`

for general colimits or `colimit(::D)`

with suitable type `D <: FixedShapeFreeDiagram{Ob}`

for colimits of specific shape, such as coproducts or coequalizers.

See also: `limit`

`Catlab.CategoricalAlgebra.Limits.limit`

— FunctionLimit of a diagram.

To define limits in a category with objects `Ob`

, override the method `limit(::FreeDiagram{Ob})`

for general limits or `limit(::D)`

with suitable type `D <: FixedShapeFreeDiagram{Ob}`

for limits of specific shape, such as products or equalizers.

See also: `colimit`

`Catlab.CategoricalAlgebra.Limits.pullback`

— MethodPullback of a pair of morphisms with common codomain.

To implement for a type `T`

, define the method `limit(::Cospan{T})`

and/or `limit(::Multicospan{T})`

or, if you have already implemented products and equalizers, rely on the default implementation.

`Catlab.CategoricalAlgebra.Limits.pushout`

— MethodPushout of a pair of morphisms with common domain.

To implement for a type `T`

, define the method `colimit(::Span{T})`

and/or `colimit(::Multispan{T})`

or, if you have already implemented coproducts and coequalizers, rely on the default implementation.

`Catlab.CategoricalAlgebra.Limits.universal`

— Function`Catlab.Theories.coequalizer`

— MethodCoequalizer of morphisms with common domain and codomain.

To implement for a type `T`

, define the method `colimit(::ParallelPair{T})`

or `colimit(::ParallelMorphisms{T})`

.

`Catlab.Theories.copair`

— MethodCopairing of morphisms: universal property of coproducts/pushouts.

To implement for coproducts of type `T`

, define the method `universal(::BinaryCoproduct{T}, ::Cospan{T})`

and/or `universal(::Coproduct{T}, ::Multicospan{T})`

and similarly for pushouts.

`Catlab.Theories.coproduct`

— MethodCoproduct of objects.

To implement for a type `T`

, define the method `colimit(::ObjectPair{T})`

and/or `colimit(::DiscreteDiagram{T})`

.

`Catlab.Theories.create`

— MethodUnique morphism out of an initial object.

To implement for a type `T`

, define the method `universal(::Initial{T}, ::SMulticospan{0,T})`

.

`Catlab.Theories.delete`

— MethodUnique morphism into a terminal object.

To implement for a type `T`

, define the method `universal(::Terminal{T}, ::SMultispan{0,T})`

.

`Catlab.Theories.equalizer`

— MethodEqualizer of morphisms with common domain and codomain.

To implement for a type `T`

, define the method `limit(::ParallelPair{T})`

and/or `limit(::ParallelMorphisms{T})`

.

`Catlab.Theories.factorize`

— MethodFactor morphism through (co)equalizer, via the universal property.

To implement for equalizers of type `T`

, define the method `universal(::Equalizer{T}, ::SMultispan{1,T})`

. For coequalizers of type `T`

, define the method `universal(::Coequalizer{T}, ::SMulticospan{1,T})`

.

`Catlab.Theories.initial`

— MethodInitial object.

To implement for a type `T`

, define the method `colimit(::EmptyDiagram{T})`

.

`Catlab.Theories.pair`

— MethodPairing of morphisms: universal property of products/pullbacks.

To implement for products of type `T`

, define the method `universal(::BinaryProduct{T}, ::Span{T})`

and/or `universal(::Product{T}, ::Multispan{T})`

and similarly for pullbacks.

`Catlab.Theories.product`

— MethodProduct of objects.

To implement for a type `T`

, define the method `limit(::ObjectPair{T})`

and/or `limit(::DiscreteDiagram{T})`

.

`Catlab.Theories.terminal`

— MethodTerminal object.

To implement for a type `T`

, define the method `limit(::EmptyDiagram{T})`

.

`Catlab.CategoricalAlgebra.Limits.@cartesian_monoidal_instance`

— MacroDefine cartesian monoidal structure using limits.

Implements an instance of `CartesianCategory`

assuming that finite products have been implemented following the limits interface.

`Catlab.CategoricalAlgebra.Limits.@cocartesian_monoidal_instance`

— MacroDefine cocartesian monoidal structure using colimits.

Implements an instance of `CocartesianCategory`

assuming that finite coproducts have been implemented following the colimits interface.

# Acsets

## Overview and Theory

For an in depth look into the theory behind acsets, we refer the reader to our paper on the subject, which also gives some sense as to how the implementation works. Here, we give a brief tutorial before the the API documentation.

The most essential part of the acset machinery is the schema. The schema *parameterizes* the acset: each schema corresponds to a different type of acset. Schemas consist of four parts.

- Objects $X,Y$ (
`(X,Y,Z)::Ob`

) - Homomorphisms $f \colon X \to Y$ (
`f :: Hom(X,Y)`

), which go from objects to objects - Data types $\mathtt{T}$ (
`T :: Data`

) - Attributes $a \colon X \to \mathtt{T}$ (
`a :: Attr(X,T)`

), which go from objects to data types

For those with a categorical background, a schema is a presentation of a category $|S|$ along with a functor $S$ from $|S|$ to the arrow category $0 \to 1$, such that $S^{-1}(1)$ is discrete.

An acset $F$ on a schema consists of...

- a set $F(X)$ of "primary keys" for each object
- a function $F(f) \colon F(X) \to F(Y)$ for each morphism
- a Julia data type $F(\mathtt{T})$ for each data type $\mathtt{T}$
- a function $F(a) \colon F(X) \to F(\mathtt{T})$ for each attribute $a$.

For those with a categorical background, an acset on a schema $S$ consists of a functor from $S$ to $\mathsf{Set}$, such that objects in $S^{-1}(0)$ map to finite sets, and objects in $S^{-1}(1)$ map to sets that represent types. For any particular functor $K \colon S^{-1}(1) \to \mathsf{Set}$, we can also take the category of acsets that restrict to this map on $S^{-1}$.

We can also add relations to this presentation, but we currently do nothing with those relations in the implementation; they mostly serve as documentation.

We will now give an example of how this all works in practice.

```
using Catlab, Catlab.CategoricalAlgebra
# Write down the schema for a weighted graph
@present TheoryWeightedGraph(FreeSchema) begin
V::Ob
E::Ob
src::Hom(E,V)
tgt::Hom(E,V)
T::Data
weight::Attr(E,T)
end
# Construct the type used to store acsets on the previous schema
# We *index* src and tgt, which means that we store not only
# the forwards map, but also the backwards map.
const WeightedGraph = ACSetType(TheoryWeightedGraph, index=[:src,:tgt])
# Construct a weighted graph, with floats as edge weights
g = @acset WeightedGraph{Float64} begin
V = 4
E = 5
src = [1,1,1,2,3]
tgt = [2,3,4,4,4]
weight = [7.2, 9.3, 9.4, 0.1, 42.0]
end
```

E | src | tgt | weight |
---|---|---|---|

1 | 1 | 2 | 7.2 |

2 | 1 | 3 | 9.3 |

3 | 1 | 4 | 9.4 |

4 | 2 | 4 | 0.1 |

5 | 3 | 4 | 42.0 |

## API

We first give an overview of the data types used in the acset machinery.

`FreeSchema`

A finite presentation of a category that will be used as the schema of a database in the *algebraic databases* conception of categorical database theory. Functors out of a schema into FinSet are combinatorial structures over the schema. Attributes in a schema allow you to encode numerical (any julia type) into the database. You can find several examples of schemas in `Catlab.Graphs`

where they define categorical versions of graph theory.

`CSet/AttributedCSet`

is a struct/constructors whose values (tables, indices) are parameterized by a CatDesc/AttrDesc. These are in memory databases over the schema equiped with `ACSetTranformations`

as natural transformations that encode relationships between database instances.

`CSetType/AttributedCSetType`

provides a function to construct a julia type for ACSet instances, parameterized by CatDesc/AttrDesc. This function constructs the new type at runtime. In order to have the interactive nature of Julia, and to dynamically construct schemas based on runtime values, we need to define new Julia types at runtime. This function converts the schema spec to the corresponding Julia type.

`CatDesc/AttrDesc`

the encoding of a schema into a Julia type. These exist because Julia only allows certain kinds of data in the parameter of a dependent type. Thus, we have to serialize a schema into those primitive data types so that we can use them to parameterize the ACSet type over the schema. This is an implementation detail subject to complete overhaul.

`Catlab.CategoricalAlgebra.CSets`

— ModuleCategories of C-sets and attributed C-sets.

`Catlab.CategoricalAlgebra.CSets.ACSetTransformation`

— TypeTransformation between attributed C-sets.

A homomorphism of C-sets is a natural transformation: a transformation between functors C → Set satisfying the naturality axiom for all morphisms in C. This struct records the data of a transformation; it does not enforce naturality, but see `is_natural`

.

A C-set transformation has a component for every object in C. When C-sets have attributes, the data types are assumed to be fixed. Thus, the naturality axiom for data attributes is a commutative triangle, rather than a commutative square.

`Catlab.CategoricalAlgebra.CSets.generate_json_acset`

— MethodSerialize an ACSet object to a JSON string

`Catlab.CategoricalAlgebra.CSets.homomorphism`

— MethodFind a homomorphism between two attributed $C$-sets.

Returns `nothing`

if no homomorphism exists. For many categories $C$, the $C$-set homomorphism problem is NP-complete and thus this procedure generally runs in exponential time. It works best when the domain object is small.

This procedure uses the classic backtracking search algorithm for a combinatorial constraint satisfaction problem (CSP). As is well known, the homomorphism problem for relational databases is reducible to CSP. Since the C-set homomorphism problem is "the same" as the database homomorphism problem (insofar as attributed C-sets are "the same" as relational databases), it is also reducible to CSP. Backtracking search for CSP is described in many computer science textbooks, such as (Russell & Norvig 2010, *Artificial Intelligence*, Third Ed., Chapter 6: Constraint satisfaction problems, esp. Algorithm 6.5). In our implementation, the search tree is ordered using the popular heuristic of "minimum remaining values" (MRV), also known as "most constrained variable."

To restrict to *monomorphisms*, or homomorphisms whose components are all injective functions, set the keyword argument `monic=true`

. To restrict only certain components to be injective or bijective, use `monic=[...]`

or `iso=[...]`

. For example, setting `monic=[:V]`

for a graph homomorphism ensures that the vertex map is injective but imposes no constraints on the edge map.

To restrict the homomorphism to a given partial assignment, set the keyword argument `initial`

. For example, to fix the first source vertex to the third target vertex in a graph homomorphism, set `initial=(V=Dict(1 => 3),)`

.

See also: `homomorphisms`

, `isomorphism`

.

`Catlab.CategoricalAlgebra.CSets.homomorphisms`

— MethodFind all homomorphisms between two attributed $C$-sets.

This function is at least as expensive as `homomorphism`

and when no homomorphisms exist, it is exactly as expensive.

`Catlab.CategoricalAlgebra.CSets.is_homomorphic`

— MethodIs the first attributed $C$-set homomorphic to the second?

A convenience function based on `homomorphism`

.

`Catlab.CategoricalAlgebra.CSets.is_isomorphic`

— MethodAre the two attributed $C$-sets isomorphic?

A convenience function based on `isomorphism`

.

`Catlab.CategoricalAlgebra.CSets.is_natural`

— MethodIs the transformation between C-sets a natural transformation?

Uses the fact that to check whether a transformation is natural, it suffices to check the naturality equation on a generating set of morphisms.

`Catlab.CategoricalAlgebra.CSets.isomorphism`

— MethodFind an isomorphism between two attributed $C$-sets, if one exists.

See `homomorphism`

for more information about the algorithms involved.

`Catlab.CategoricalAlgebra.CSets.isomorphisms`

— MethodFind all isomorphisms between two attributed $C$-sets.

This function is at least as expensive as `isomorphism`

and when no homomorphisms exist, it is exactly as expensive.

`Catlab.CategoricalAlgebra.CSets.parse_json_acset`

— MethodDeserialize a dictionary from a parsed JSON string to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.parse_json_acset`

— MethodDeserialize a JSON string to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.read_json_acset`

— MethodRead a JSON file to an object of the given ACSet type

`Catlab.CategoricalAlgebra.CSets.write_json_acset`

— MethodSerialize an ACSet object to a JSON file

`Catlab.CategoricalAlgebra.StructuredCospans`

— ModuleStructured cospans.

This module provides a generic interface for structured cospans with a concrete implementation for attributed C-sets.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— TypeStructured cospan.

The first type parameter `L`

encodes a functor L: A → X from the base category `A`

, often FinSet, to a category `X`

with "extra structure." An L-structured cospan is then a cospan in X whose feet are images under L of objects in A. The category X is assumed to have pushouts.

Structured cospans form a double category with no further assumptions on the functor L. To obtain a symmetric monoidal double category, L must preserve finite coproducts. In practice, L usually has a right adjoint R: X → A, which implies that L preserves all finite colimits. It also allows structured cospans to be constructed more conveniently from an object x in X plus a cospan in A with apex R(x).

See also: `StructuredMulticospan`

.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— MethodConstruct structured cospan in R-form.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan`

— MethodConstruct structured cospan in L-form.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospanOb`

— TypeObject in the category of L-structured cospans.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan`

— TypeStructured multicospan.

A structured multicospan is like a structured cospan except that it may have a number of legs different than two.

See also: `StructuredCospan`

.

`Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan`

— MethodConstruct structured multicospan in R-form.

`Catlab.CategoricalAlgebra.StructuredCospans.OpenACSetTypes`

— MethodCreate types for open attributed C-sets from an attributed C-set type.

The resulting types, for objects and morphisms, each have the same type parameters for data types as the original type.

See also: `OpenCSetTypes`

.

`Catlab.CategoricalAlgebra.StructuredCospans.OpenCSetTypes`

— MethodCreate types for open C-sets from a C-set type.

Returns two types, for objects, a subtype of `StructuredCospanOb`

, and for morphisms, a subtype of `StructuredMulticospan`

.

See also: `OpenACSetTypes`

.