Edit on GitHub

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.FinFunction — Type

Function 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 — Type

Finite 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.FinRelations.BoolRig — Type

The 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.FinRelation — Type

Binary 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).

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 — Module

Free 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 — Type

A 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.bundle_legs — Method

Bundle 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.Limits.colimit — Function

Colimit 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 — Function

Limit 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 — Method

Pullback 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 — Method

Pushout 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.Theories.coequalizer — Method

Coequalizer 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 — Method

Copairing 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 — Method

Coproduct of objects.

To implement for a type T, define the method colimit(::ObjectPair{T}) and/or colimit(::DiscreteDiagram{T}).

Catlab.Theories.create — Method

Unique morphism out of an initial object.

To implement for a type T, define the method universal(::Initial{T}, ::SMulticospan{0,T}).

Catlab.Theories.delete — Method

Unique morphism into a terminal object.

To implement for a type T, define the method universal(::Terminal{T}, ::SMultispan{0,T}).

Catlab.Theories.equalizer — Method

Equalizer 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 — Method

Factor 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 — Method

Initial object.

To implement for a type T, define the method colimit(::EmptyDiagram{T}).

Catlab.Theories.pair — Method

Pairing 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 — Method

Product of objects.

To implement for a type T, define the method limit(::ObjectPair{T}) and/or limit(::DiscreteDiagram{T}).

Catlab.Theories.terminal — Method

Terminal object.

To implement for a type T, define the method limit(::EmptyDiagram{T}).

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
ACSet with elements V = 1:4, E = 1:5
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/AttributedCSetTypeprovides 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.ACSetTransformation — Type

Transformation 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.homomorphism — Method

Find 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.is_natural — Method

Is 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.StructuredCospans.StructuredCospan — Type

Structured 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.