Library Reference

Apply migration to all literals in the constraint

Conjunction of multiple expressions

Constant, independent of context

Something that, in a context, can be evaluated to a bool

Negation of an expression

Disjunction of multiple expressions

"nothing" means something that will be determined via a quantifier Ints are explicit arguments provided when apply_constraint is called

A commutative diagram with multiple parallel paths, asserted to either commute or to not commute

A constraint graph and a BoolExpr (which refers to the constraint graph)

Quantified edge

e - which edge is filled in kind - Exists, Forall, or Exists! st - "such that", restrict the domain of quantification via a condition monic - restrict domain of quanitification to only monic matches

Constraint a constraint that asserts (or denies) the existence of a triangle commuting.

 f₁

(1) <- (2) ∃₂↘ ↓ λ₃ (3)

  ∀₂

(1) → (3) ₁↓ ↗∃₃ ↓ λ₅ (2) → (4) ⁴

Test a map (3)→(4), given maps (1)->(2)->(4).

Number of variables in a constraint graph

Validate a commutative diagram constraint makes sense

Check whether homs are equal by looping over domain.

Get the C-Set associated with a vertex in a CGraph

Take two CGraphs and merge them along their overlapping vertices and edges Returns an ACSetColimit

Combine two constraints disjunctively, sharing as much of the computation graph as possible.

Combine two constraints conjunctively, sharing as much of the computation graph as possible (i.e. pushout along the maximum common subgraph)

Rewrite rules which are (usually) encoded as spans. The L structure encodes a pattern to be matched. The R morphism encodes a replacement pattern to be substituted in. They are related to each other by an interface I with maps: L ⟵ I ⟶ R

A semantics (DPO, SPO, CoNeg, or SqPO) must be chosen.

Control the match-finding process by specifying whether the match is intended to be monic or not, as well as an optional application condition(s)

Returns nothing if the match is acceptable for rewriting according to the rule, otherwise returns the reason why it should be rejected

homsearch = if we know ahead of time that m was obtained m via automatic hom search, then we do not need to make certain checks

Get a list of AttrVar indices which are NOT bound by the I→R morphism

Don't bind variables for things that are not ACSets

Given the match morphism and the result, construct a map X → X′ which binds any free variables introduced into the result.

L <- I -> R m ↓ ↓ ↓ res G <- • -> X ↓ X′

Get one match (if any exist) otherwise return

Get list of possible matches based on the constraints of the rule

This function has the same behavior as the generic get_matches, but it is more performant because we do not have to query all homomorphisms before finding a valid match, in case n=1.

If not rewriting ACSets, we have to compute entire Hom(L,G).

Extract the partial map (derived rule) from full output data

Extract the map from the R to the result from the full output data

rewrite(r::Rule, G; kw...)

Perform a rewrite (automatically finding an arbitrary match) and return result.

rewrite_match(r::Rule, m; kw...)

Perform a rewrite (with a supplied match morphism) and return result.

rewrite_match_maps(r::Rule{:DPO}, m)

Apply a DPO rewrite rule (given as a span, L<-I->R) to a ACSet using a match morphism m which indicates where to apply the rewrite. l r L <- I -> R m ↓ ↓ ↓ G <- K -> H

This works for any type that implements pushout_complement and pushout

rewrite_match_maps(r::Rule{:CoNeg}, m)

Apply a CoNegation rewrite rule (given as a span, L↩I->R) to a ACSet using a monic match morphism m which indicates where to apply the rewrite. l r L <- I -> R m ↓ ↓ ↓ G <- K -> H where K = ~L ∨ I

This works for any type that implements bi-Heyting logic operators ~ and ∨.

This is described here. Essentially, it is partway between DPO and SPO. Suppose the rule tries to delete two things, one of which satisfies the dangling condition, the other violates it. While DPO would fail to apply at all, and SPO would delete both things (cascading the deletion for the latter), co-negation rewriting would simply delete the item which can be deleted without cascading and ignore the other element.

It includes a quote which indicates that this method should work even when the match morphism isn't monic, if it satisfies the identification condition. Supporting this is not yet implemented.

Match morphisms which bind attribute variables are not monic, hence we this form of rewriting doesn't support VarACSets. Intuitively, it feels like this restriction could be relaxed.

C ← Ag ↪ A ↩ Af → B

A ↩ f∇g → Bgf ↪ B ↓ ⌜ ↓ C ↩ Cfg -> D

Implementation of Construction 6 in Löwe's "Algebraic approach to SPO graph transformation"

See Theorem 2 of 'Concurrency Theorems for Non-linear Rewriting Theories' f B <–- A m ↓ ↓ n C <– D g

rewrite_match_maps(r::Rule{:SqPO},m; pres::Union{Nothing, Presentation}=nothing)

Sesqui-pushout is just like DPO, except we use a final pullback complement instead of a pushout complement.

r.L  r.R

L <-⌞K -> R m ↓ ↓k ↓ r I <- • ->⌜O i o

  l    r

L ⟵ K ⟶ R tl ↓ ↓ tk <== tl, tk must be monic L' ⟵ K'

It is assumed we never want the typing/adherence match to be monic, but we can optionally restrict the match L → G to be monic.

We can attach application conditions to both the match morphism as well as the adherence morphism. Until morphism search under constraints becomes efficient, it's sometimes needed to just directly state the adherence morphism as a function of the match morphism.

Take a PBPO rule and put into normal form, i.e. where the lower square forms a pullback

See Prop 2.4 of "The PBPO graph transformation approach"

This construction addresses the following problem: ideally when we 'abstract' an ACSet from X to A->X, maps into X, say B->X, can be canonically pulled back to maps B->A which commute. However, A won't do here, because there may not even exist any maps B->A. If B has concrete attributes, then those cannot be sent to an AttrVar in A. Furthermore, if B has multiple 'references' to an AttrVar (two different edges, each with AttrVar(1), sent to two different edges with the same atttribute value in X), then there is no longer a canonical place to send AttrVar(1) to in A, as there is a distinct AttrVar for every single part+attr in X. So we need a construction which does two things to A->X, starting with a map B->X. 1.) replaces exactly the variables we need with concrete values in order to allow a map B->A, 2.) quotients variables in A so that there is exactly one choice for where to send attrvars in B such that the triangle commutes.

Starting with a map L -> G (where G has no AttrVars), we want the analogous map into a "partially abstracted" version of G that has concrete attributes replaced with AttrVars EXCEPT for those attributes which are mapped to by concrete attributes of L. Likewise, multiple occurences of the same variable in L correspond to AttrVars which should be merged in the partially-abstracted G.

For example, for a schema with a single Ob and Attr (where all combinatorial maps are just {1↦1, 2↦2}):

• L = [AttrVar(1), :foo]

• G = [:bar, :foo, :baz]

• abs(G) = [AttrVar(1), AttrVar(2), AttrVar(3)]

• expected result: [AttrVar(1), :foo, AttrVar(2)]

  L -> Partial_abs(G) ↓ ↑ G <- abs(G)

This function computes the top arrow of this diagram starting with the left arrow. The bottom arrow is computed by abstract_attributes and the right arrow by sub_vars. Furthermore, a map from Partial_abs(G) to G is provided.

This is the factorization system arising from a coreflective subcategory.

(see https://ncatlab.org/nlab/show/reflective+factorization+system and https://blog.algebraicjulia.org/post/2023/06/varacsets/)

See get_matches(::PBPORule, ::ACSet)

Use exprs and k_exprs to fill in variables introduced by applying the rw rule.

PBPO matches consist of two morphisms. First, a match m: L → G, and secondly a typing G → L′. With attributes, it is not so simple because G has concrete values for attributes and L′ may have variables. Therefore, we actually change the typing to map out of A, an abstracted version of G (with its attributes replaced by variables). So we lift matches L->G to matches L->A, then search α∈Hom(A,L′).

In general, we want α to be uniquely determined by m, so by default α_unique is set to true.

 m

L⌟ ⟶ G || ↓ α L ⟶ L′ tl

 m

L ⟶ G tl ↓ ↘a ↑ (abs = partial abstraction. Note a is Labs in the code.) L′⟵ A α

The "strong match" condition we enforce is that: tl⁻¹(α(A)) = a⁻¹(A). This means we can deduce precisely what m is by looking at α.

         r
      K ----> R
gₗ    u ↓ gᵣ ⌜ ↓ w

Gₗ <–– Gk ––> Gᵣ α ↓ ⌞ ↓ u' L′ <– K′ tₗ

For the adherence morphism α to be valid, it must satisfy a condition with m, tₗ. This is checked for matches provided by get_matches, so by default we do not check it.

L <–⌞• m ↓ ↓ G ⟵ Gk

See Lemma 7.2 of "TERMINATION OF GRAPH TRANSFORMATION SYSTEMS USING WEIGHTED SUBGRAPH COUNTING" by Overbeek and Endrullis (2023)

Want a filename that is stable to multiple Julia sessions but changes when the schema changes. This minimizes the need to clear the cache.

Compute a pushout complement of finite sets, if possible.

Given functions $l: I → L$ and $m: L → G$ to form a pushout square

l

L ← I m ↓ ↓k G ← K g

define the set $K := G / m(L / l(I))$ and take $g: K ↪ G$ to be the inclusion. Then the map $k: I → K$ is determined by the map $l⋅m: I → G$ from the requirement that the square commutes.

Pushout complements exist only if the identification condition is satisfied. An error will be raised if the pushout complement cannot be constructed. To check this in advance, use can_pushout_complement.

Compute a pushout complement of finite sets, if possible.

Given functions $l: I → L$ and $m: L → G$ to form a pushout square

l

L ← I m ↓ ↓k G ← K g

define the set $K := G ∖ m(L ∖ l(I))$ and take $g: K ↪ G$ to be the inclusion. Then the map $k: I → K$ is determined by the map $l⋅m: I → G$ from the requirement that the square commutes.

For example, if L = I = {1} and G = {1,2}, then l({1}) = {1}, L ∖ l(I) = {} and G∖ m({}) = {1,2}.

Pushout complements exist only if the identification condition is satisfied. An error will be raised if the pushout complement cannot be constructed. To check this in advance, use can_pushout_complement.

Because l is monic, the map l:I+T ↣ L+T secretly is just a map l′:I↣L and T=T

We'll also assume that the map m: L+T->G+T is secretly just a map L->T (G=∅).

Kleisli composition

Check identification condition for pushout complement of finite sets.

The identification condition says that the functions do not map (1) both a deleted item and a preserved item in L to the same item in G or (2) two distinct deleted items to the same item. It is trivially satisfied for injective functions.

Returns pair of iterators of

(1) a nondeleted item that maps to a deleted item in G (2) a pair of distinct items in L that are deleted yet mapped to the same item in G.

TODO: check if functorial

Compute pushout complement of attributed C-sets, if possible.

The pushout complement is constructed pointwise from pushout complements of finite sets. If any of the pointwise identification conditions fail (in FinSet), this method will raise an error. If the dangling condition fails, the resulting C-set will be only partially defined. To check all these conditions in advance, use the function can_pushout_complement.

Recursively delete anything, e.g. deleting a vertex deletes its edge

Y i↘ f_ X → • g_ ↓ ⌟ ↓ f • → • g

Check whether (X, f,g) is the pullback of (f,g), up to isomorphism (i.e. the pullback of f and g produces (Y,π₁,π₂), where Y is isomorphic to X and i⋅f_ = π₁ & i⋅g_ = π₂.

Every morphism induces a partition of the parts of the domain. This function finds every nontrivial partition (size greater than one element) for the objects of the schema.

Invert a morphism which may not be monic nor epic. When the morphism is not monic, an arbitrary element of the preimage is mapped to. When it is not epic, a completely arbitrary element is mapped to.

Invert some (presumed iso) components of an ACSetTransformation (given by s)

Given f: A->C and g: B->C, find all morphisms A->B that make the triangle commute

                ??? 
              A  ⇉  B 
              f ↘ ↙ g
                 C

Given a value for each variable, create a morphism X → X′ which applies the substitution. We do this via pushout.

O –> X where C has AttrVars for merge equivalence classes ↓ and O has only AttrVars (sent to concrete values or eq classes C in the map to C.

subs and merge are dictionaries keyed by attrtype names

subs values are int-keyed dictionaries indicating binding, e.g. ; subs = (Weight = Dict(1 => 3.20, 5 => 2.32), ...)

merge values are vectors of vectors indicating equivalence classes, e.g. ; merge = (Weight = [[2,3], [4,6]], ...)

Further induced equations between AttrVars, given a specific match morphism

Take an ACSet pullback combinatorially and freely add variables for all attribute subparts.

This relies on implementation details of abstract.

A component-wise map between two cospans. The first component given is the apex map, with the following maps being the legs.

A span of StructuredMulticospanHoms, interpreted as a DPO rewrite rule

composeH_(r₁, r₂)

compose two rewrite rules horizontally (via pushouts) as shown below: L₁₋₍ₙ₋₁₎-> L <- Lₙ X₁ -> X <- X₂₋ₘ L₁₋₍ₙ₋₁₎ -> L +Lₙ X <- X₂₋ₘ ↑ λ ↑ ↑ ↑ ↑ χ ↑ ↑ ↑ ↑ I₁₋₍ₙ₋₁₎-> I <- Iₙ ∘h Y₁ -> Y <- Y₂₋ₘ = I₁₋₍ₙ₋₁₎ -> I +Iₙ Y <- Y₂₋ₘ ↓ ρ ↓ ↓ ↓ ↓ ζ ↓ ↓ ↓ ↓ R₁₋₍ₙ₋₁₎-> R <- Rₙ Z₁ -> Z <- Z₂₋ₘ R₁₋₍ₙ₋₁₎ -> R +Rₙ Z <- Z₂₋ₘ

Cospan composition given by pushout

Finset span composition given by pullback

composeV_(r₁, r₂)

compose two rewrite rules vertically with pullbacks, as shown below: L₁₋ₙ -> L ↑ ↑ I₁₋ₙ -> I ↓ ↓ L₁₋ₙ -> L R₁₋ₙ -> R ↑ ↑ ∘v = I₁₋ₙ ×ᵣ₁₋ₙ Θ₁₋ₙ -> I ×ᵣ Θ Λ₁₋ₙ -> Λ ↓ ↓ ↑ ↑ Ω₁₋ₙ -> Ω Θ₁₋ₙ -> Θ ↓ ↓ Ω₁₋ₙ -> Ω

Pass dummy value in because a span of invertible FinFunctions does not retain L type

Vertical arrows are spans of invertible finfunctions

Initial data: 4 structured cospans + 3 cospan morphisms: μ, λ, ρ g G₁₋ₙ –> G ↑ l ↑ μ L₁₋ₙ –> L ↑ i ↑ λ I₁₋ₙ –> I ↓ r ↓ ρ R₁₋ₙ –> R

Computed data: 2 new structured cospans + 4 cospan morphisms: γ, η, ik, rh G₁₋ₙ G ↑ k ↑ γ ik I₁₋ₙ -> K₁₋ₙ –> K <– I ↓ h ↓ η rh R₁₋ₙ -> H₁₋ₙ –> H <– R In the context of the legs of a multicospan, the indices 1-n refer to the n legs of the cospan. In the context of a map of multicospans, there are 1-(n+1) maps, with the first one designating the map of the apexes. Hence it can make sense to have the elements: zip(legs, maps[2:end]) = [(legᵢ, mapᵢ), ...]

Apply a rewrite rule to a structured multicospan, where a matching cospan homomorphism is found automatically. If multiple matches are found, a particular one can be selected using m_index. Returns nothing if none are found.

Extract the rewritten structured cospan from the induced rewrite rule

Find homomorphisms between structured cospans. These are constrained to be iso on the legs of the cospans. Solving this w/ homomorphism finding requires a dynamic acset, and the current hack will be replaced once those are available.

A homomorphism backend that uses SAT/SMT would also make this viable to do without hacking.

Confirm a C-Set satisfies its equational axioms

Take a GATExpr (an id morphism, a generator, or a composite) and evaluate, starting at a particular point.

The natural injection from X ⟶ T(X) When evaluated on the terminal object, this gives the subobject classfier.

A partial function is defined by the following span: m f A ↩ X → B

We compute ϕ(m,f): A ⟶ T(B) such that the following is a pullback square: f X ⟶ B m ↓ ↓ η(B) A ⟶ T(B) ϕ

Essentially, ϕ sends elements of A to the 'real' values in T(B) when A is in the subobject picked out by X. When A is 'deleted', it picks out the right element of the additional data added by T(B).

Because the functorial embedding of objects keeps a copy of the original data, what to do with morphisms is just carry them along. Because our implementation adds all of the additional stuff afterwards, index-wise, we can use literally the same data for a morphism lifted from X⟶Y to T(X)⟶T(Y).

However, we still need to map the extra stuff in T(X) to the proper extra stuff in T(Y).

A functor T, playing the role of Maybe in Set, but generalized to C-Sets.

When called on the terminal object, this produces the subobject classifier: See Mulry "Partial map classifiers and cartesian closed categories" (1994)

This function specifies what T does on objects. The key properties:

1. for all X ∈ Ob(C), η(X):X⟶T(X) is monic. m f ϕ(m,f)
2. for each span A ↩ X → B, there exists a unique morphism A ⟶ T(B) such that (m,f) is the pullback of ϕ(m,f),η(B))

Not only do we add an extra element to each component of the C-Set, but we need to consider the possibility that a component (with n outgoing morphisms) has any combination of the targets of those morphisms deleted (like the subobject classifier, there are different ways for something to be deleted).

For example, in Graph, an edge can be deleted that goes between any two vertices of the graph. We can't map all deleted edges to the same point in T(E) (if we're going to satisfy that desired property #2), so we need an extra edge in T(E) for every possibility (from V1 to V2, from V1 to V3, ..., from [Deleted] to V1, ..., from V2 to [Deleted], ... from [Deleted] to [Deleted]), where [Deleted] is our name for the extra element added to T(V).

                [src]     [tgt]

Thus, T(E) ≅ |E| + (|V|+1) × (|V|+1).

In general, T(X) ≅ |X| + ∏ₕ(|T(codom(h))|) for each outgoing morphism h::X⟶Y

• the |X| corresponds to the 'real' elements of X
• the second term corresponds to the possible ways an X can be deleted.
• This recursive formula means we require the schema of the C-set to be acyclic otherwise the size is infinite (assumes schema is free).

Get topological sort of objects of a schema. Fail if cyclic.