kris-brown/combinatorialenumeration.jl

Enumerate models of finite limit sketches up to isomorphism

CombinatorialEnumeration.jl

This package implements a constrained search algorithm, with constraints specified in the language of sketches / category theory. Formally, given a finite (co)- limit sketch, we enumerate its models up to isomorphism. See more in the documentation and some examples are in the examples directory (e.g. reflexive graphs, coequalizers, categories, jointly surjective maps) underneath src and test.

Status

This is very experimental code, so there may be frequent breaking changes. There is great opportunity for massive speed-ups - really the most basic implementations to get something running is all that is written so far, but done so in a modular way (e.g. enforcing cone constraints, enforcing cocone constraints) so that bottlenecks can be identified and improved piecemeal.

combinatorialenumeration.jl's Issues

Logic based interface

One ought to be able to write a series of (geometric) logic statements and have a sketch produced automatically.

Take advantage of previous computations via filters/pushouts

If enumerating models of a theory that simply adds constraints to a previous theory that has been enumerated, then we can get models merely by filtering previous results.

If a theory is expressible as a pushout of two other theories, then enumerating its models is just the database join of the enumerations of the smaller theories (which should often be easier to compute).

These should be implemented. Are there other tricks that can take advantage of the structure of theories?

More sophisticated distinction than "free" vs "derived"

Presently we can treat the objects that are NOT the apex of a (co)cone as "real" / "immutable" data (cannot merge two elements, cannot add elements) whereas (co)limit objects are viewed as something more flexible - we might need more or fewer depending on how things shake out.

It's harder to make inferences about the derived objects. It seems like something is missing if we treat a product of two real objects A and B (with size |A|*|B|) as having a cardinality that can change.

We should keep track of which objects and morphisms are "determined". When all objects + morphisms in a diagram are 'determined', then the apex + legs become 'determined' as well.

explore performance improvements by not calling nauty so much

The code currently calls nauty very aggressively to prevent duplicate work, but this appears to be a bottleneck. Looking at the exploration space of premodels, it seems like rarely does this quotienting actually prune (except when branching a foreign key on a bunch of options which are symmetric).

Something to benchmark, then, is:

1. only use nauty at the very end of the search process, when a verified model is found
2. When branching a foreign key, use is_isomorphic on the candidates to remove redundant options

thread parallelism

The main search process iteratively constructs a tree by iterating through vertices and (depending on the results of a pure function) possibly adding more vertices. This process ought be parallelizable, as there are many unchecked vertices to process at a given point in time, but it's not clear how to do this.

Take advantage of nauty's orbits

There are many points where we consider all possible assignments of a foreign key (such as branching on an unassigned one, or at many points in the colimit code e.g. detecting if two components are connectable via some assignment).

However, many of these assignments are equal up to symmetry, captured by the orbits produced by CSetAutomorphisms.jl. We could greatly reduce some branching factors by only considering distinct orbits.

It would be helpful to address this issue though.

create a web interface

inspiration: http://combos.org/

However, we want users to be able to parameterize search by drawing an ACSet (with Semagrams)

Implement category of sketches

https://ncatlab.org/nlab/show/sketch "The category of sketches is well behaved: it is complete, cocomplete, cartesian closed and has a second symmetric monoidal closed structure."

Sketches are quite unwieldy to work with directly, though they'd much easier to work with as (co)limits of simpler building block sketches. We can also take advantage of this higher structure when enumerating models (#2)