Catlab supports the expression of equations in an arbitrary category via diagrams, or functors from a finitely presented category. This view of diagrammatic equations builds on the Catlab approach to functorial semantics by asserting that a system of equations of shape J is a functor F: J โ†’ ๐‚. We can draw these equations with Graphviz, where each node is an object in X:Ob(J) labeled with its type F(X) and each edge is a morphism in J labeled with its image under F.

using Catlab, Catlab.Theories, Catlab.CategoricalAlgebra
using Catlab.Graphs, Catlab.Graphics, Catlab.Programs
using Catlab.Graphs.BasicGraphs: TheoryGraph
using Catlab.Graphics.Graphviz

draw(D::FinFunctor) = to_graphviz(D, node_labels=true, edge_labels=true, prog="neato")
draw (generic function with 1 method)

Present a diagram in a given category

Recall that a diagram in a category $C$ is a functor $F: J โ†’ C$ from a small category $J$ into $C$. Given the category $C$, this macro presents a diagram in $C$, i.e., constructs a finitely presented indexing category $J$ together with a functor $F: J โ†’ C$. This method of simultaneous definition is often more convenient than defining $J$ and $F$ separately. often more convenient than defining $J$ and $F$ separately, as could be accomplished by calling @fincat and then @finfunctor. For example, the limit of the following diagram consists of the paths of length two in a graph:

Dโ‚‚ = @free_diagram TheoryGraph begin
  (eโ‚, eโ‚‚)::E
  tgt(eโ‚) == v
  src(eโ‚‚) == v
FinFunctor(Catlab.Theories.FreeSchema.Ob{:generator}[V, E, E], Catlab.Theories.FreeSchema.Hom{:generator}[tgt, src], FinCat(NamedGraph {V = 3, E = 2}), FinCat(Presentation{Schema, Symbol}(Catlab.Theories.FreeSchema, (Ob = Catlab.Theories.FreeSchema.Ob{:generator}[V, E], Hom = Catlab.Theories.FreeSchema.Hom{:generator}[src, tgt], AttrType = Catlab.Theories.FreeSchema.AttrType{:generator}[], Attr = Catlab.Theories.FreeSchema.Attr{:generator}[]), Dict(:src=>(:Hom=>1), :V=>(:Ob=>1), :E=>(:Ob=>2), :tgt=>(:Hom=>2)), Pair[])))

Morphisms in the indexing category can be left unnamed, which is convenient for defining free diagrams (see also @free_diagram. Of course, unnamed morphisms cannot be referenced by name within the @diagram call or in other settings, which can sometimes be problematic.

We can also draw the resulting diagrams.


For small equations the point-free notation commonly employed in functional programming is very convenient; however, there is a reason it is not the standard approach to presenting equations in mathematical writing. Variables are just too useful! As the size of the system of equations grows, it becomes more and more convenient to use variable names. This is why Catlab.Programs.@program exists to help people write SMC morphisms with the point-ful notation they are familiar with in imperative or procedural programming.

We can describe a triangle in a graph using the vertex variables vโ‚, vโ‚‚, vโ‚ƒ and edge variables eโ‚, eโ‚‚, eโ‚ƒ. Then we use the equation notation to assert the src and tgt relationships between the edges and vertices.

Dโ‚ƒ = @free_diagram TheoryGraph begin
  (vโ‚, vโ‚‚, vโ‚ƒ)::V
  (eโ‚, eโ‚‚, eโ‚ƒ)::E
  src(eโ‚) == vโ‚
  tgt(eโ‚) == vโ‚‚
  src(eโ‚‚) == vโ‚‚
  src(eโ‚ƒ) == vโ‚
  tgt(eโ‚‚) == vโ‚ƒ
  tgt(eโ‚ƒ) == vโ‚ƒ
FinFunctor(Catlab.Theories.FreeSchema.Ob{:generator}[V, V, V, E, E, E], Catlab.Theories.FreeSchema.Hom{:generator}[src, tgt, src, src, tgt, tgt], FinCat(NamedGraph {V = 6, E = 6}), FinCat(Presentation{Schema, Symbol}(Catlab.Theories.FreeSchema, (Ob = Catlab.Theories.FreeSchema.Ob{:generator}[V, E], Hom = Catlab.Theories.FreeSchema.Hom{:generator}[src, tgt], AttrType = Catlab.Theories.FreeSchema.AttrType{:generator}[], Attr = Catlab.Theories.FreeSchema.Attr{:generator}[]), Dict(:src=>(:Hom=>1), :V=>(:Ob=>1), :E=>(:Ob=>2), :tgt=>(:Hom=>2)), Pair[])))

You can see the shape of a triangle when you draw this diagram. This coincidence can be systematically understood (by an experienced category theorist) via the Grothendieck construction and representable functors.


Sequences in

In any category with an endomorphism f: A โ†’ A, we can think of recurrence equations as aโ‚™ = f(aโ‚™โ‚‹โ‚)) starting at aโ‚€.

@present ๐—–(FreeCartesianCategory) begin

seqโ‚ƒ = @free_diagram ๐—– begin
  aโ‚ == f(aโ‚€)
  aโ‚‚ == f(aโ‚)
  aโ‚ƒ == f(aโ‚‚)


Inspired by linear recurrence relations like the Fibonacci sequence we can think of A and B as vector spaces. An endomorphism f: A โ†’ A and morphism g: A โ†’ B defines a linear recurrence by applying f to update the system state and g to compute the current term in the sequence. This can be visualized as follows.

obs_seqโ‚ƒ = @free_diagram ๐—– begin
  (bโ‚, bโ‚‚, bโ‚ƒ )::B
  aโ‚ == f(aโ‚€)
  bโ‚ == g(aโ‚)
  aโ‚‚ == f(aโ‚)
  bโ‚‚ == g(aโ‚‚)
  aโ‚ƒ == f(aโ‚‚)
  bโ‚ƒ == g(aโ‚ƒ)

In the case of the Fibonacci sequence A is โ„ยฒ and B is โ„ with f = [1 1; 1 0] and g = ฯ€โ‚.

@present ๐ƒ(FreeCartesianCategory) begin

fib_seqโ‚ƒ = @free_diagram ๐ƒ begin
  (bโ‚, bโ‚‚, bโ‚ƒ )::โ„
  aโ‚ == f(aโ‚€)
  bโ‚ == ฯ€โ‚(aโ‚)
  aโ‚‚ == f(aโ‚)
  bโ‚‚ == ฯ€โ‚(aโ‚‚)
  aโ‚ƒ == f(aโ‚‚)
  bโ‚ƒ == ฯ€โ‚(aโ‚ƒ)


A lift of this diagram is a choice of vectors aโ‚€,โ€ฆ,aโ‚ƒ and scalars bโ‚,โ€ฆ,bโ‚ƒ that satisfy the linear recurrence formulation of the Fibonacci sequence. The arrows in ๐ƒ are treated as fixed for the purpose of the lifting problem. Suppose you knew bโ‚,โ€ฆ,bโ‚ƒ, and wanted to infer the state vectors aโ‚,โ€ฆ,aโ‚ƒ. This can be seen as a boundary value problem where you have observations on a subspace playing the role of boundary conditions and want to infer the system state on the interior of the domain. As you can see from this diagram, solving the lifting problem with only partial information can require some creativity. You need to use the structure of the codomain category, in this case ๐ƒ which is a subcategory of finite dimensional vector spaces over โ„ and the combinatorics of ๐‰ to set up some equations you can solve. In order to obtain an efficient algorithm for the lifting problem, you would need to exploit the structure of the morphisms f,ฯ€โ‚ to create a system of equations.

An observation that [ฯ€โ‚f;ฯ€โ‚] = f lets you set up the equation [bโ‚ƒ ; bโ‚‚] = f aโ‚‚ and then you can use the fact that f is invertable to solve for a unique aโ‚‚. Once you have a single value of aแตข you can get the rest from the application of f or fโปยน. A general purpose algorithm for solving lifting problems in arbitrary categories would be a wildly powerful tool.

Newton's Method

The equations that we have seen aren't particularly interesting, so we turn to a classic of numerical methods. Newton's method for root finding. For an overview of Netwon's method see Fundamentals of Numerical Computation. The following presentation doesn't know that fโ€ฒ is the derivative of f, they are just two functions that are evocatively named. We could use CombinatorialSpaces.jl to formulate this in a richer categorical setting where we could assert fโ€ฒ := d/dx(f).

@present Analytic(FreeCartesianCategory) begin
  ฯ€โ‚::Hom(โ„ยฒ, โ„)
  ฯ€โ‚‚::Hom(โ„ยฒ, โ„)
  plus ::Hom(โ„ยฒ, โ„)
  times::Hom(โ„ยฒ, โ„)
  f    ::Hom(โ„,โ„)
  fโ€ฒ   ::Hom(โ„,โ„)
Presentation{CartesianCategory, Symbol}(Catlab.Theories.FreeCartesianCategory, (Ob = Catlab.Theories.FreeCartesianCategory.Ob{:generator}[โ„, โ„ยฒ], Hom = Catlab.Theories.FreeCartesianCategory.Hom{:generator}[ฯ€โ‚, ฯ€โ‚‚, plus, times, f, fโ€ฒ]), Dict(:f => (:Hom => 5), :fโ€ฒ => (:Hom => 6), :times => (:Hom => 4), :โ„ยฒ => (:Ob => 2), :ฯ€โ‚ => (:Hom => 1), :โ„ => (:Ob => 1), :ฯ€โ‚‚ => (:Hom => 2), :plus => (:Hom => 3)), Pair[])

According to the standard formula xโ‚–โ‚Šโ‚ = xโ‚– - f(xโ‚–)/fโ€ฒ(xโ‚–). The standard presentation of Newton's method relies on the fact that โ„ is a field to use division in the definition of the iterative procedure. Because of the constraint that you can't divide by 0 in a field, fields are not models of any algebraic theory. Because of this, we can multiply both sides by fโ€ฒ(xโ‚–) and define a Newton's method iteration without reference to division. We also can avoid negation by adding the f(xโ‚–) term on both sides.

Once we have put Newton's method into this relational form we can use a prefix notation for operators which makes the structure closer to the diagrammatic approach plus(times(fโ€ฒ(xโ‚–), xโ‚–โ‚Šโ‚), f(xโ‚–)) == times(fโ€ฒ(xโ‚–), xโ‚–).

newtons = @free_diagram Analytic begin
  (xโ‚–, xโ‚–โ‚Šโ‚, dโ‚–, fx, v, โˆ)::โ„
  (pโ‚, pโ‚‚, pโ‚ƒ)::โ„ยฒ
  dโ‚–  == fโ€ฒ(xโ‚–)
  ฯ€โ‚(pโ‚) == dโ‚–
  ฯ€โ‚‚(pโ‚) == xโ‚–โ‚Šโ‚
  โˆ == times(pโ‚)
  fx == f(xโ‚–)
  ฯ€โ‚(pโ‚‚) == โˆ
  ฯ€โ‚‚(pโ‚‚) == fx
  plus(pโ‚‚) == v
  ฯ€โ‚(pโ‚ƒ) == dโ‚–
  ฯ€โ‚‚(pโ‚ƒ) == xโ‚–
  times(pโ‚ƒ) == v


This is definitely a case where standard mathematical notation wins for brevity and clarity. To compete with traditional notation, we need a few ergonamic improvements to the diagrammatic equation approach.

  1. The ability to assert equations without introducing temporary variables,
  2. The ability to represent morphisms f: Aร—B โ†’ C as bivariate functions like f(a:A, b:B),

While encoding simple equations can be more verbose than the traditional notation, the diagrammatic encoding provides a direct route to creating a category whose objects are systems of equations and whose morphisms are relationships between systems of equations. That category is the first step towards leveraging the constructive approach in Catlab to making hierarchical representations of complex systems of equations.