Incremental presheaf hom-set updating

General
1

Introduction

Many applications of scientific modeling with C-sets require enumerating the full set of homomorphisms between some pattern C-set, A, and some target C-set, X. Catlab implements an NP-complete backtracking search algorithm which can do this for any finite A and X. Here we are concerned with how we can update \text{Hom}(A,X) in light of small changes in X, rather than computing \text{Hom}(A,X') from scratch. In particular, this is relevant to implementing graph rewriting-based simulations, where we frequently make small changes to the state of the world X yet also need to maintain many hom-sets into X so that the simulation can randomly sample the next action to take.

Motivated by the graph rewriting scenario, there are two types of changes to X which we need to be prepared for. The first is restriction of X to a subobject, specified by a map X \leftarrowtail X'. This kind of update can only shrink \text{Hom}(A,X), so we can simply filter the set, keeping morphisms whose image lies in the subobject X'. While deletion is simple to handle, the addition of data requires more effort.

Example

Weā€™ll use directed multigraphs for our example C-sets. The underlying vertex sets will be labeled {1,ā€¦,n}. I will refer to vertex n of graph G as G_n. All graphs in this post will happen to have at most one edge between any pair of vertices, so an edge from G_n to G_m can be referred to as G_{n\rightarrow m}. A function from one vertex set \{1,...,n\} to another \{1,...,m\} can be represented as a vector of length n with elements which are between 1 and m.

Consider a path graph with two edges as the pattern, A, we are tracking. Given our initial state of the world, X, \text{Hom}(A,X) has two matches (one which sends the three vertices of A to [1,2,2], the other which sends them to [2,2,2]).

One possible deletion X \leftarrowtail X' removes X_{1\rightarrow 2}. We can easily filter the hom set to remove morphisms which touch upon the removed data, and the resulting singleton hom set correctly represents \text{Hom}(A,X').

Handling addition: precomputation

Addition of data is captured by the notion of a pushout:

I will refer to O \rightarrowtail B as an adder; itā€™s a recipe for adding data. O represents an ā€œoverlapā€ C-set, and B represents some data to be added with respect to that overlap. This morphism O \rightarrowtail B can be used to add data to multiple places within X; thus a match morphism O \rightarrow X is also required data for any particular addition of data X\rightarrow X'.

There are two regions of X' worth distinguishing. Every element of X' can be in the image or not of B and O. Being in the image of B but not O is to be a brand-new element introduced by the addition. Being outside of the image of B is to be in the old region of X', i.e. unrelated to the addition.

Intuitively, in order to update \text{Hom}(A,X) to \text{Hom}(A,X'), we want to add morphisms A \rightarrow X' that touch upon some brand new elements. It is difficult to encode this kind of existentially-quantified constraint into the backtracking search procedure itself.[1]

The approach here will rely on the fact that we are not expecting arbitrary adders to our world state; we consider some predeclared set of adders.[2] We want to do some hard work ahead of time for fixed A and O \rightarrowtail B such that, when handed an arbitrary match O\rightarrow X at runtime, we can update \text{Hom}(A,X) to \text{Hom}(A,X').

The key precomputation is enumerating the set of partial maps {A \leftarrowtail \bullet \rightarrow B}. There are many of these, but A and B are often small in practice. One can think of each of these as a distinct way in which the pattern can intersect with the newly-added material. An element of A not being in the domain of the partial map means that the morphism A\rightarrow X' will assign that element to somewhere in the old region of X', as defined above. The next section shows how we attempt to extend each of these into homomorphisms A \rightarrow X'.

Example

Our example adder O \rightarrowtail B will take some preexisting edge and turn it into a triangle by adding a vertex and two edges. At runtime, a match which sends O_{1\rightarrow 2} \mapsto X_{1 \rightarrow 2} will result in an addition which introduces two maps A \rightarrow X': one which sends vertices of A to [3,2,2] and one that sends them to [1,3,2].

Catlab computes the 13 subobjects of A and 89 partial maps {A \leftarrowtail \bullet \rightarrow B}. As a first round of filtering, we can safely ignore 33 of these partial maps, as their images have no intersection with brand-new material. Here are three examples from the remaining 56 partial maps:

841Ɨ189 26.2 KB

We can understand these three partial maps as respectively saying:

  1. The three vertices of A and A_{1\rightarrow 2} will be assigned in the image of B (in the particular way specified by the partial map), but A_{2\rightarrow 3} must be sent to from the old region of X'. At runtime, this overlap will lead to finding the map A \rightarrow X', which sends the vertices of A to [3,2,2].
  2. The entirety of A will live in the image of B. At runtime, this will lead to finding the other new map A \rightarrow X', which sends the vertices of A to [1,3,2].
  3. A_1 must go to the newly-introduced vertex X'_3, but A_{1\rightarrow 2} must be sent to the old region of X'. However, itā€™s not possible for an edge in the old region to have a newly-introduced vertex as its source, so we can ignore this overlap.

In fact, after this second level of filtering, we are left with only seven possible ways in which the pushout O \rightarrowtail B can lead to new matches for A.

724Ɨ420 38.4 KB

Handling addition: Runtime computation

At runtime we are told a specific addition was made: this data is an adder O\rightarrowtail B and match morphism O \rightarrow X.

We can postcompose with the resulting pushout map update to push forward each element of \text{Hom}(A,X) into \text{Hom}(A,X'). All that remains is to consider the contribution of each partial map {A \leftarrowtail \bullet \rightarrow B} to the hom-set \text{Hom}(A,X'). These are each considered in isolation. Here we use the backtracking homomorphism search algorithm, but the data of the partial map gives us some constraints:

  1. The square above must commute, which is enforced by initializing assignment values of the homomorphism search.
  2. Elements which are not initialized as above must be mapped to the old region of X', i.e. outside of the image of bmap. Whenever there is a match which could be found by assigning such an element to something in the image of bmap, then one of our other partial overlaps will address that case.

These constraints are amenable to efficient integration with the backtracking search algorithm. In our example above, we would run seven very constrained searches at runtime to discover the two new homomorphisms A \rightarrow X'.

Example

For the first of the seven partial maps above, the homomorphism search initialization that makes the square commute already is the full data of a homomorphism A \rightarrow X', so search terminates instantly.

For the second partial map, the vertex assignment is initialized [3,2,?] and the edge assignment is [3\rightarrow 2, ?]. Homomorphism search would then try to assign to assign A_{2\rightarrow 3} to some outgoing edge of X'_2 (which must be in the old region of X'). There is only one such option: X_{2\rightarrow 2}. Lastly, it tries to assign A_3; however the constraint that it must lie in the old region of X' means that the only candidate (X'_2) is not eligible, so the search returns no results. If the starting graph X were to have some additional vertex connected via an outgoing edge from X_2, then this partial overlap would have found an additional match to add to \text{Hom}(A,X').

The fifth partial map leads to a homomorphism search similar to the one just described up until the assignment of A_3; however, in this case we initialized A_3 \mapsto X'_2, and the homomorphism search successfully returns the new match with vertex assignment [3,2,2].

Final thoughts

  • This work came about from very helpful conversations with Ben Bumpus.
  • A natural next step is to consider merging data by relaxing some of the monic constraints.
  • Iā€™m hoping to see how this relates to preexisting work about incremental queries in a variety of contexts (graphs, databases).
  • There is an implementation of this in AlgebraicRewriting.jl which does dramatically improve performance, relative to recomputing the whole hom set.
    • That implementation decomposes the pattern A into its connected components and maintains (under the hood) a separate incremental morphism tracker for each of them, which can be a big efficiency gain.
  • This algorithm is nowhere near as categorical as Iā€™d like: ideally I could leverage Evanā€™s great work with the bi-Heyting propositional logic of C-Sets, but important concepts like ā€œthe brand-new elements of X'ā€ arenā€™t actually subobjects.
    • A more abstract characterization of what the algorithm is doing would help in proving that it is correct, if it is. (It has been tested over many randomly-generated examples, though.)

  1. When working with just graphs, rather than C-sets, one can consider a ā€˜diameterā€™ d of A and restrict search to a subgraph of X' that is within distance d of the newly-introduced material. This doesnā€™t generalize cleanly to C-sets and still will generate false positives (matches which already exist in \text{Hom}(A,X) which need to be filtered). ā†©ļøŽ

  2. In the setting where you do not have the adders predeclared, itā€™s still possible to do this precomputation the first time you encounter a new adder. ā†©ļøŽ

4 Likes