GitHub

Categorical algebra

Sets and Relations

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.

Free Diagrams, Limits, and Colimits

The following modules define free diagrams in an arbitrary category and specify limit and colimit 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.Cats.Functors.fmap — Method

Informal requirement of FreeDiagram implementations: fmap takes an function on objects and a function on homs and replaces the obs and homs of FreeDiagram while preserving the edges and vertices.

source
Catlab.CategoricalAlgebra.Cats.LimitsColimits.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.

source

Categories

Catlab.CategoricalAlgebra.Cats.FinCats — Module

2-category of finitely presented categories.

This module is for the 2-category Cat what the module FinSets is for the category Set: a finitary, combinatorial setting where explicit calculations can be carried out. We emphasize that the prefix Fin means "finitely presented," not "finite," as finite categories are too restrictive a notion for many purposes. For example, the free category on a graph is finite if and only if the graph is DAG, which is a fairly special condition. This usage of Fin is also consistent with FinSet because for sets, being finite and being finitely presented are equivalent.

source

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
  • Attribute types $\mathtt{T}$ (T :: AttrType)
  • 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 equations to this presentation, but we currently do nothing with those equations in the implementation; they mostly serve as documentation.

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

using GATlab, Catlab.CategoricalAlgebra

# Write down the schema for a weighted graph
@present SchWeightedGraph(FreeSchema) begin
  V::Ob
  E::Ob
  src::Hom(E,V)
  tgt::Hom(E,V)
  T::AttrType
  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.
@acset_type WeightedGraph(SchWeightedGraph, 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
Main.__atexample__317.WeightedGraph{Float64} {V:4, E:5, T:0}
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

The mathematical abstraction of an acset can of course be implemented in many different ways. Currently, there are three implementations of acsets in Catlab, which share a great deal of code.

These implementations can be split into two categories.

The first category is static acset types. In this implementation, different schemas correspond to different Julia types. Methods on these Julia types are then custom-generated for the schema, using CompTime.jl.

Under this category, there are two classes of static acset types. The first class is acset types that are generated using the @acset_type macro. These acset types are custom-derived structs. The advantage of this is that the structs have names like Graph or WiringDiagram that are printed out in error messages. The disadvantage is that if you are taking in schemas at runtime, you have to eval code in order to use them.

Here is an example of using @acset_type

@acset_type WeightedGraph(SchWeightedGraph, index=[:src,:tgt])
g = WeightedGraph()

The second class is AnonACSets. Like acset types derived from @acset_type, these contain the schema in their type. However, they also contain the type of their fields in their types, so the types printed out in error messages are long and ugly. The advantage of these is that they can be used in situations where the schema is passed in at runtime, and they don't require using eval to create a new acset type.

Here is an example of using AnonACSet

const WeightedGraph = AnonACSetType(SchWeightedGraph, index=[:src,:tgt])
g = WeightedGraph()

The second category is dynamic acset types. Currently, there is just one type that falls under this category: DynamicACSet. This type has a field for the schema, and no code-generation is done for operations on acsets of this type. This means that if the schema is large compared to the data, this type will often be faster than the static acsets.

However, dynamics acsets are a new addition to Catlab, and much of the machinery of limits, colimits, and other high-level acset constructions assumes that the schema of an acset can be derived from the type. Thus, more work will have to be done before dynamic acsets become a drop-in replacement for static acsets.

Here is an example of using a dynamic acset

g = DynamicACSet("WeightedGraph", SchWeightedGraph; index=[:src,:tgt])
Catlab.CategoricalAlgebra.Cats.Transformations.is_natural — Method

Check naturality condition for a purported ACSetTransformation, α: X→Y. For each hom in the schema, e.g. h: m → n, the following square must commute:

     αₘ
  Xₘ --> Yₘ
Xₕ ↓  ✓  ↓ Yₕ
  Xₙ --> Yₙ
     αₙ

You're allowed to run this on a named tuple partly specifying an ACSetTransformation, though at this time the domain and codomain must be fully specified ACSets.

source
Catlab.CategoricalAlgebra.Cats.Transformations.naturality_failures — Method

Returns a dictionary whose keys are contained in the names in arrows(S) and whose value at :f, for an arrow (f,c,d), is a lazy iterator over the elements of X(c) on which α's naturality square for f does not commute. Components should be a NamedTuple or Dictionary with keys contained in the names of S's morphisms and values vectors or dicts defining partial functions from X(c) to Y(c).

source
Catlab.CategoricalAlgebra.Pointwise.Chase — Module

The chase is an algorithm which subjects a C-Set instance to constraints expressed in the language of regular logic, called embedded dependencies (EDs, or 'triggers').

A morphism S->T, encodes an embedded dependency. If the pattern S is matched (via a homomorphism S->I), we demand there exist a morphism T->I (for some database instance I) that makes the triangle commute in order to satisfy the dependency (if this is not the case, then the trigger is 'active').

Homomorphisms can merge elements and introduce new ones. The former kind are called "equality generating dependencies" (EGDs) and the latter "tuple generating dependencies" (TGDs). Any homomorphism can be factored into EGD and TGD components by, respectively, restricting the codomain to the image or restricting the domain to the coimage.

source
Catlab.CategoricalAlgebra.Pointwise.Chase.chase — Method
chase(I::ACSet, Σ::AbstractDict, n::Int)

Chase a C-Set or C-Rel instance given a list of embedded dependencies. This may not terminate, so a bound n on the number of iterations is required.

[,]

ΣS ⟶ Iₙ ⊕↓ ⋮ (resulting morphism) ΣT ... Iₙ₊₁

There is a copy of S and T for each active trigger. A trigger is a map from S into the current instance. What makes it 'active' is that there is no morphism from T to I that makes the triangle commute.

Each iteration constructs the above pushout square. The result is a morphism, so that one can keep track of the provenance of elements in the original CSet instance within the chased result.

Whether or not the result is due to success or timeout is returned as a boolean flag.

TODO: this algorithm could be made more efficient by homomorphism caching.

source
Catlab.CategoricalAlgebra.Pointwise.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.

source
Catlab.CategoricalAlgebra.Pointwise.StructuredCospans.OpenACSetTypes — Method

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

The type parameters of the given acset type should not be instantiated with specific Julia types. This function returns a pair of types, one for objects, a subtype of StructuredCospanOb, and one for morphisms, a subtype of StructuredMulticospan. Both types will have the same type parameters for attribute types as the given acset type.

Mathematically speaking, this function sets up structured (multi)cospans with a functor $L: A → X$ between categories of acsets that creates "discrete acsets." Such a "discrete acset functor" is a functor that is left adjoint to a certain kind of forgetful functor between categories of acsets, namely one that is a pullback along an inclusion of schemas such that the image of inclusion has no outgoing arrows. For example, the schema inclusion ${V} ↪ {E ⇉ V}$ has this property but ${E} ↪ {E ⇉ V}$ does not.

See also: OpenCSetTypes.

source