`AlgebraicRewriting.Rewrite.Inplace.Compiler`

— Typeassignment allows us to

- set attributes to things that were matched by original hom search

`AlgebraicRewriting.Rewrite.Inplace.rewrite_match!`

— MethodApply a DPO rewrite to a specific match morphism. This will modify the codom of the match morphism and returns a map from the R of the rule into the result.

`AlgebraicRewriting.Rewrite.Inplace.set_attr`

— MethodRecord how to set f(ob#i)

`AlgebraicRewriting.CategoricalAlgebra.CSets.Migrate`

— MethodMap a functor over the data of a schedule

`AlgebraicRewriting.Schedules.Wiring.AgentBox`

— TypeType for primitive boxes used in a schedule. These are the generating morphisms of a traced monoidal category, with objects being lists of ACSets.

`ACSets.DenseACSets.sparsify`

— MethodMap sparisfication over the data of a schedule

`AlgebraicRewriting.Schedules.Wiring.merge_wires`

— FunctionThe comonoid structure - merging multiple wires into one. This is unproblematic because the world state only ever exists on one wire at a given time.

`AlgebraicRewriting.Schedules.Wiring.mk_sched`

— MethodMake a wiring diagram with ob/hom generators using @program macro

TODO double check that this does not introduce any wire splitting.

`AlgebraicRewriting.Schedules.Wiring.singleton`

— MethodMake a wiring diagram around a box

`AlgebraicRewriting.Schedules.Wiring.str_hom`

— MethodVisualize the data of a CSet homomorphism

`AlgebraicRewriting.Schedules.Wiring.wire_vals`

— Method1 = inwire, 2 = outwire

`AlgebraicRewriting.Rewrite.PBPO.PBPORule`

— Type` 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.

`AlgebraicRewriting.Rewrite.PBPO.canon`

— MethodTake 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"

`AlgebraicRewriting.Rewrite.PBPO.partial_abstract`

— MethodThis 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/)

`AlgebraicRewriting.Rewrite.PBPO.test_adherence`

— MethodSee `get_matches(::PBPORule, ::ACSet)`

`AlgebraicRewriting.Rewrite.Utils.get_expr_binding_map`

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

`AlgebraicRewriting.Rewrite.Utils.get_matches`

— MethodPBPO 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 α.

`AlgebraicRewriting.Rewrite.Utils.rewrite_match_maps`

— Method```
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)

`AlgebraicRewriting.Incremental.IncrementalHom`

— ModuleThings for incremental hom sets, not particular to any specific implementation.

`AlgebraicRewriting.Incremental.IncrementalHom.IncHomSet`

— TypeThere are currently two types of IncHomSets. Common to both is a separation of the data required to specify which hom-set is being maintained (`static`

) and the data structure required to be maintained as some target `X`

is changing (`runtime`

). We also distinguish between general static data for maintaining an incremental hom-set from further static data about various constraints on that process (`constraints`

).

These are all currently designed to work with `DenseParts`

ACSets but could be straightforwardly modified to work with `MarkAsDeleted`

ACSets (which would be even more efficient.)

`AlgebraicRewriting.Incremental.IncrementalHom.IncRuntime`

— TypeRuntimes must have a `state`

, `key_vect`

, and `key_dict`

.

`state`

: The current state of the world, into which we are maintaining a hom-set.

`key_vect::Vector{K}`

: A vector of keys into the ground source of truth, which stores the data of the morphisms. The structure of this source of truth and key type K depends on which kind of `IncRuntime`

is being used. This may contain references to invalidated homs.

`key_dict::Dict{K, Int}`

: Contains an entry for each current element of the hom-set. The values are used to index `key_vect`

.

`AlgebraicRewriting.Incremental.IncrementalHom.IncStatic`

— TypeA incremental hom-set has a fixed pattern, `pattern`

(sometimes referred to by a variable, `L`

). It is updated with respect to a class of changes to `state`

(sometimes referred to by a variable `X`

).

The state, X, can be changed via restriction to subobjects or by pushout with any of the predeclared monic `addition`

morphisms, though we won't know the match morphism •→X until runtime.

```
additionⱼ
I >--------> R
↓ ⌜ ↓
X ---------> X′
```

Cached `overlaps`

data helps compute how the hom set updates with respect to a given addition being applied. The cache records in element i data for when we are updating the hom set after having applied addition i. It stores partial overlaps between L and Rᵢ which have *some* data that hits upon the new content added.

`AlgebraicRewriting.Incremental.IncrementalHom.addition!`

— MethodPerform a pushout addition given a match morphism from the domain.

`AlgebraicRewriting.Rewrite.Inplace.rewrite!`

— MethodPerform a rewrite! with an arbitrary match

`AlgebraicRewriting.Rewrite.Inplace.rewrite!`

— MethodUse a rewrite rule to induce a deletion followed by an addition.

Returns the keys of deleted and added matches, respectively.

`AlgebraicRewriting.Incremental.IncrementalSum`

— ModuleMulti-connected-component incremental hom-sets

`AlgebraicRewriting.Incremental.IncrementalSum.IncSumHomSet`

— TypeAn incremental Hom Set for a pattern made of distinct connected components

`AlgebraicRewriting.Incremental.IncrementalSum.IncSumStatic`

— Type`iso`

is an isomorphism: apex(coprod) ≅ pattern

`AlgebraicRewriting.Incremental.IncrementalHom.addition!`

— MethodCompute additions component-wise, then aggregate results

`AlgebraicRewriting.Incremental.IncrementalHom.deletion!`

— MethodCompute deletions component-wise, then aggregate results

`AlgebraicRewriting.Incremental.IncrementalHom.matches`

— MethodUniversal property of coprod: induce map from pattern, given component maps

`AlgebraicRewriting.Incremental.IncrementalHom.validate`

— MethodCheck, with brute computational effort, that the IncrementalHomSet is well formed.

`AlgebraicRewriting.Incremental.IncrementalSum.add_keys!`

— MethodAdd keys to a component of a IncSumHomSet. This implicitly adds composite keys for every combination of existing keys in the other components' hom sets.

Returns the *composite keys* which are added as an explicit list.

`AlgebraicRewriting.Incremental.IncrementalSum.delete_add_keys!`

— MethodPropagate deletion/addition for a component to the composite key level

`AlgebraicRewriting.Incremental.IncrementalSum.delete_keys!`

— MethodDelete keys from a component of a IncSumHomSet. This implicitly deletes all composite keys that make reference to those keys.

Returns the *composite keys* which are deleted as an explicit list.

`Base.length`

— MethodHow many additions we've seen so far (including the initialization of the hom set). Could be confused with `length(h.components)`

or `length(keys(h))`

`Catlab.Theories.universal`

— MethodApply universal property and the isomorphism

`AlgebraicRewriting.CategoricalAlgebra.CSets.Migrate`

— TypeTODO: check if functorial

`AlgebraicRewriting.CategoricalAlgebra.CSets.cascade_subobj`

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

`AlgebraicRewriting.CategoricalAlgebra.CSets.check_pb`

— MethodY 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_ = π₂.

`AlgebraicRewriting.CategoricalAlgebra.CSets.fibers`

— MethodEvery 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.

`AlgebraicRewriting.CategoricalAlgebra.CSets.gluing_conditions`

— MethodCheck both id condition and dangling condition

`AlgebraicRewriting.CategoricalAlgebra.CSets.invert_hom`

— MethodInvert 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.

`AlgebraicRewriting.CategoricalAlgebra.CSets.invert_iso`

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

`AlgebraicRewriting.CategoricalAlgebra.CSets.sub_vars`

— FunctionGiven 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]], ...)`

`AlgebraicRewriting.CategoricalAlgebra.CSets.var_eqs`

— MethodFurther induced equations between AttrVars, given a specific match morphism

`AlgebraicRewriting.CategoricalAlgebra.CSets.var_pullback`

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

This relies on implementation details of `abstract`

.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.can_pushout_complement`

— MethodCan a pushout complement be constructed for a composable pair?

Even in nice categories, this is not generally possible.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.pushout_complement`

— MethodPushout complement: extend composable pair to a pushout square.

Pushout complements are the essential ingredient for double pushout (DPO) rewriting.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.pushout_complement`

— MethodCompute 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`

.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.pushout_complement`

— Method`pushout_complement(f::SliceHom, g::SliceHom)`

Compute a pushout complement in a slice category by using the pushout complement in the underlying category.

` f`

B <– A –-⌝ | ↘ ↙ | g| X | f′ ↓ ↗ ↖ cx | D <–- C <– g′

`Catlab.CategoricalAlgebra.HomSearch.homomorphisms`

— MethodThis could be made more efficient as a constraint during homomorphism finding.

`AlgebraicRewriting.Incremental.Cast`

— ModuleCast between IncCC and IncSum

`AlgebraicRewriting.Incremental.IncrementalCC.IncCCHomSet`

— MethodCast a sum homset into a single 'connected component'

`AlgebraicRewriting.Incremental.IncrementalHom.IncHomSet`

— MethodAutomatically determine whether one creates an IncCC or an IncHom.

`single`

keyword forces the pattern to be treated as a single CC, even if it's not one. Having any constraints will also force it to be treated as a single CC.

`AlgebraicRewriting.Incremental.IncrementalHom.IncHomSet`

— MethodInitialize an Incremental hom set from a rule, using it's pattern `L`

as the domain of the hom set. Any additions other than the map `I->R`

can be passed in by `additions`

, and the schema Presentation can be passed as `S`

.

`AlgebraicRewriting.Incremental.IncrementalSum.IncSumHomSet`

— MethodCast a CC to a singleton sum

`AlgebraicRewriting.Schedules.Poly`

— ModuleMealy machines (augmented with monadic output) are a user-friendly format for specifying a behavior tree. Behavior trees in general are not finitely expressible, but we focus on trees which can be lazily generated by functions.

Although it is conceptually simple to think of a single set of "input doors" out "output doors" to enter/leave the Mealy machine, such that a Mealy machine has type A → B, we use Σᵢ Aᵢ → Σⱼ Bⱼ, where Aᵢ and Bⱼ are Julia types. This allows us to represent a Mealy machine with (Int + String)-many input doors, for example.

`AlgebraicRewriting.Schedules.Poly.List`

— Constant"The list monad returns the set of packages labeled with a natural number N, each of which has N-many slots."

`AlgebraicRewriting.Schedules.Poly.Maybe`

— Constant"The Maybe monad, y+1, consists of two packages, one with one slot and the other with no slots."

`AlgebraicRewriting.Schedules.Poly.BTree`

— TypeLazily grown behavior tree induced by a Mealy machine. The future behavior is dictated by the inputs seen thus far (i.e. a vector of WireVals).

Each vertex is identified by a sequence of inputs and has a state of the Mealy machine associated with it.

Each nonempty sequence of inputs has a MealyRes associated with it.

`AlgebraicRewriting.Schedules.Poly.BTree`

— MethodGrow a tree and return the result.

`AlgebraicRewriting.Schedules.Poly.Mealy`

— TypeA function that maintains a state (initially s0) and has monadic output for some polynomial monad t.

The function f must be of type S × WireVal → S × (t ◁ WireVal)

` (i.e. S × Wireval → MealyRes)`

`AlgebraicRewriting.Schedules.Poly.MealyRes`

— TypeOutput of a Mealy machine

newS - The new state of the Mealy machine mval - outputs along with their monadic values (e.g. probability weights) msg - A message reporting something about the computation

`AlgebraicRewriting.Schedules.Poly.PMonad`

— TypeQuotes in this docstring and others taken from David Spivak: https://topos.site/blog/2023/09/powers-of-polynomial-monads/#exponentiating-monads

"A polynomial monad is a polynomial functor t with coherent maps η: y → t and μ: t ◁ t → t.

Polynomial monads can be thought of as offering compositional (possibly labeled) packages with some number of slots. The compositionality of this packaging says that (via the monad unit) we know how to package up a given element of any set, and that (via the monad multiplication) we can take a package of packages and simplify it to a single package."

We consider monads t of the form: t = Σ_{i ∈ t(1)} y^{t[i]}

I is the type of labels, e.g. probability weights.

`AlgebraicRewriting.Schedules.Poly.Simulator`

— TypeEquips a wiring diagram description of a simulator with mutable data structures (now behavior trees for each box, but possibly incremental homomorphism caches in the future). Requires that all the boxes of the WiringDiagram be convertable to BTrees.

`AlgebraicRewriting.Schedules.Poly.TrajStep`

— TypeA trajectory step is a box being fed a particular value

This only makes sense with reference to a WiringDiagram which `box`

refers to.

`AlgebraicRewriting.Schedules.Poly.WireVal`

— TypeFor an in/output, Σᵢ Aᵢ, provide wire index + value on wire

`AlgebraicRewriting.Schedules.Poly.add_edge`

— MethodAppend without mutating

`AlgebraicRewriting.Schedules.Poly.apply_schedule`

— MethodIn theory applying a schedule should result in a list of ACSets associated with out ports and monad labels (e.g. probabilities), and if one were to want to recover the trajectory of the output one would have to use a Writer monad of some sort. For simplicity, the application of a schedule will simply return the trajectories themselves (monadic multiplication could in principle condense this output to the pure output).

`AlgebraicRewriting.Schedules.Poly.apply_traj_step`

— MethodA particular trajectory enters a box. Out of the box comes a list of trajectories.

`AlgebraicRewriting.Schedules.Poly.curr_state`

— MethodCurrent state of the world

`AlgebraicRewriting.Schedules.Poly.currwire`

— MethodGet the wire which the traj is currently on

`AlgebraicRewriting.Schedules.Poly.joindist`

— Method"The lotteries monad returns the set of packages labeled with a lottery (a natural number N and a probability distribution on it) and again containing N-many slots."

`AlgebraicRewriting.Schedules.Poly.joinstr`

— MethodWriter monad

`AlgebraicRewriting.Schedules.Queries.Query`

— TypeHas an A input/output and a B input/output (by default, the B input can be changed to some other type if needed).

```
A R ---------↖
↓ ↓ []
```

⌜–––-⌝ [] | Query | [agent subroutine] ⌞–––-⌟ [] ↓ ↓ ↓ [] A B ∅ [] ↘–––––-↗ Performs one action per element of Hom(B,X), optionally with some constraints. (i.e. sends you out along the B wire with agent Bₙ->X).

After you have done this for all Bₙ, then you exit the A port (you need to update the A->X map, and, if at any point the agent was deleted, then you exit a third door typed by 0).

A constraint optionally will be applied to (1) the A->W<-B cospan of old agent and purported new agent. (the new agent is the first argument to the constraint)

`AlgebraicRewriting.Processes.RWStep`

— TypeThe relevant maps of an application of a single DPO rewrite.

`AlgebraicRewriting.Processes.find_deps`

— MethodFor a concrete sequence of rewrites applications [a₁,a₂...aₙ], compute a poset on the set of applications which reflects their casual connections, where a < b mean that a must occur temporaly before b.

`AlgebraicRewriting.Processes.rw_steps`

— MethodConvert a vector of rewrite rule followed by match morphism to RWSteps

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.check_eqs`

— MethodConfirm a C-Set satisfies its equational axioms

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.eval_path`

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

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.partial_map_classifier_eta`

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

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.partial_map_classifier_universal_property`

— MethodA 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).

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.partial_map_functor_hom`

— MethodBecause 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).

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.partial_map_functor_ob`

— MethodA 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:

- for all X ∈ Ob(C), η(X):X⟶T(X) is monic. m f ϕ(m,f)
- 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).

`AlgebraicRewriting.CategoricalAlgebra.PartialMap.topo_obs`

— MethodGet topological sort of objects of a schema. Fail if cyclic.

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.StructuredMultiCospanHom`

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

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.openrule`

— TypeA span of StructuredMulticospanHoms, interpreted as a DPO rewrite rule

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.composeH_`

— Method`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₂₋ₘ

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.composeH_`

— MethodCospan composition given by pushout

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.composeV_`

— MethodFinset span composition given by pullback

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.composeV_`

— Method`composeV_(r₁, r₂)`

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

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.id2H_`

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

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.idV_`

— MethodVertical arrows are spans of invertible finfunctions

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.open_pushout_complement`

— MethodInitial 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ᵢ), ...]

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.open_rewrite`

— MethodApply 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.

`AlgebraicRewriting.CategoricalAlgebra.StructuredCospans.open_rewrite_match`

— MethodExtract the rewritten structured cospan from the induced rewrite rule

`Catlab.CategoricalAlgebra.HomSearch.homomorphisms`

— MethodFind 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.

`AlgebraicRewriting.Rewrite.Utils.rewrite_match_maps`

— Method`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.

`AlgebraicRewriting.Schedules.Theories.ThTracedMonoidalWithBidiagonals`

— ModuleNo documentation found.

`AlgebraicRewriting.Schedules.Theories.##4224`

is of type `Nothing`

.

**Summary**

`struct Nothing`

**ThTracedMonoidalWithBidiagonals**

```
Ob::TYPE ⊣ []
#= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =#
Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob]
#= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =#
compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)]
(assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)]
id(a)::Hom(a, a) ⊣ [a::Ob]
(idl := compose(id(a), f) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)]
(idr := compose(f, id(b)) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)]
#= /juliateam/.julia/packages/Catlab/77h9f/src/theories/Monoidal.jl:28 =#
otimes(A, B)::Ob ⊣ [A::Ob, B::Ob]
otimes(f, g)::Hom(otimes(A, C), otimes(B, D)) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A, B), g::Hom(C, D)]
munit()::Ob ⊣ []
(otimes(otimes(A, B), C) == otimes(A, otimes(B, C))) ⊣ [A::Ob, B::Ob, C::Ob]
(otimes(munit(), A) == A) ⊣ [A::Ob]
(otimes(A, munit()) == A) ⊣ [A::Ob]
(otimes(otimes(f, g), h) == otimes(f, otimes(g, h))) ⊣ [A::Ob, B::Ob, C::Ob, X::Ob, Y::Ob, Z::Ob, f::Hom(A, X), g::Hom(B, Y), h::Hom(C, Z)]
(otimes(id(munit()), f) == f) ⊣ [A::Ob, B::Ob, f::Hom(A, B)]
(otimes(f, id(munit())) == f) ⊣ [A::Ob, B::Ob, f::Hom(A, B)]
(compose(otimes(f, g), otimes(h, k)) == otimes(compose(f, h), compose(g, k))) ⊣ [A::Ob, B::Ob, C::Ob, X::Ob, Y::Ob, Z::Ob, f::Hom(A, B), h::Hom(B, C), g::Hom(X, Y), k::Hom(Y, Z)]
(id(otimes(A, B)) == otimes(id(A), id(B))) ⊣ [A::Ob, B::Ob]
braid(A, B)::Hom(otimes(A, B), otimes(B, A)) ⊣ [A::Ob, B::Ob]
#= /juliateam/.julia/packages/Catlab/77h9f/src/theories/Monoidal.jl:87 =#
(compose(braid(A, B), braid(B, A)) == id(otimes(A, B))) ⊣ [A::Ob, B::Ob]
(braid(A, otimes(B, C)) == compose(otimes(braid(A, B), id(C)), otimes(id(B), braid(A, C)))) ⊣ [A::Ob, B::Ob, C::Ob]
(braid(otimes(A, B), C) == compose(otimes(id(A), braid(B, C)), otimes(braid(A, C), id(B)))) ⊣ [A::Ob, B::Ob, C::Ob]
(braid(A, munit()) == id(A)) ⊣ [A::Ob]
(braid(munit(), A) == id(A)) ⊣ [A::Ob]
(compose(otimes(f, g), braid(B, D)) == compose(braid(A, C), otimes(g, f))) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A, B), g::Hom(C, D)]
trace(X, A, B, f)::Hom(A, B) ⊣ [X::Ob, A::Ob, B::Ob, f::Hom(otimes(X, A), otimes(X, B))]
mmerge(A)::Hom(otimes(A, A), A) ⊣ [A::Ob]
#= /juliateam/.julia/packages/AlgebraicRewriting/6TZlx/src/schedules/Theories.jl:11 =#
create(A)::Hom(munit(), A) ⊣ [A::Ob]
#= /juliateam/.julia/packages/AlgebraicRewriting/6TZlx/src/schedules/Theories.jl:13 =#
```

`AlgebraicRewriting.CategoricalAlgebra.CSets.Migrate`

— MethodApply migration to all literals in the constraint

`AlgebraicRewriting.Rewrite.Constraints.BoolAnd`

— TypeConjunction of multiple expressions

`AlgebraicRewriting.Rewrite.Constraints.BoolConst`

— TypeConstant, independent of context

`AlgebraicRewriting.Rewrite.Constraints.BoolExpr`

— TypeSomething that, in a context, can be evaluated to a bool

`AlgebraicRewriting.Rewrite.Constraints.BoolNot`

— TypeNegation of an expression

`AlgebraicRewriting.Rewrite.Constraints.BoolOr`

— TypeDisjunction of multiple expressions

`AlgebraicRewriting.Rewrite.Constraints.CGraph`

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

`AlgebraicRewriting.Rewrite.Constraints.Commutes`

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

`AlgebraicRewriting.Rewrite.Constraints.Constraint`

— TypeA constraint graph and a BoolExpr (which refers to the constraint graph)

`AlgebraicRewriting.Rewrite.Constraints.Quantifier`

— TypeQuantified 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

`AlgebraicRewriting.Rewrite.Constraints.AppCond`

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

` f₁`

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

`AlgebraicRewriting.Rewrite.Constraints.LiftCond`

— Method` ∀₂`

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

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

`AlgebraicRewriting.Rewrite.Constraints.arity`

— MethodNumber of variables in a constraint graph

`AlgebraicRewriting.Rewrite.Constraints.check_expr`

— MethodValidate a commutative diagram constraint makes sense

`AlgebraicRewriting.Rewrite.Constraints.eval_boolexpr`

— MethodCheck whether homs are equal by looping over domain.

`AlgebraicRewriting.Rewrite.Constraints.get_ob`

— MethodGet the C-Set associated with a vertex in a CGraph

`AlgebraicRewriting.Rewrite.Constraints.merge_graphs`

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

`Catlab.Theories.:⊕`

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

`Catlab.Theories.:⊗`

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

`AlgebraicRewriting.Schedules.Eval`

— ModuleSpecialized code for handling rewriting of ACSets with the identity monad

`AlgebraicRewriting.Schedules.Eval.interpret!`

— Methodinterpret a wiring diagram, with each box updating its state in place

`AlgebraicRewriting.Schedules.Eval.interpret`

— MethodInterpret a wiring diagram, recording the trajectory taken

`AlgebraicRewriting.CategoricalAlgebra.FinSets.id_condition`

— MethodCheck 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.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.pushout_complement`

— MethodCompute 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`

.

`AlgebraicRewriting.CategoricalAlgebra.FinSets.pushout_complement`

— MethodGiven a monic VarFunction (which only sends AttrVars to AttrVars) and a VarFunction which only sends AttrVars to concrete values, we have a unique means of first sending vars to concrete

`AlgebraicRewriting.Schedules.RuleApps.RuleApp`

— TypeHas the semantics of applying the rule to *some* match that is found (no guarantees on *which* one, which should be controlled by application conditions). If rewrite occurs, exit mode 1, else exit mode 2.

The agent is related to the L and R patterns of the rule. This can be done via a Span, or implicitly as a homomorphism into "I" of the rewrite rule, and alternatively just from the shape of the agent alone (if it is identical to I, take the id map, otherwise take the unique morphism into I).

`AlgebraicRewriting.Schedules.RuleApps.has_match`

— MethodA box that takes the first output iff there is a match from a rule into the current state

`AlgebraicRewriting.Schedules.RuleApps.loop_rule`

— MethodFeed the "rewrite applied" output back into the input of the rule application

`AlgebraicRewriting.Rewrite.Utils.rewrite_match_maps`

— Method`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`

`AlgebraicRewriting.Incremental.Algorithms.all_subobjects`

— MethodGet all subobjects as monos into X

`AlgebraicRewriting.Incremental.Algorithms.compute_overlaps`

— MethodFind all partial maps from the pattern to the addition, with some restrictions:

*Something*must be mapped into the newly added material.- Anything in L incident to a part mapped onto newly added material must be mapped to newly added material

`AlgebraicRewriting.Incremental.Algorithms.connected_acset_components`

— MethodBreak an ACSet into connected components, represented as a coproduct and an isomorphism from the original ACSet into the colimit apex.

`AlgebraicRewriting.Incremental.Algorithms.deattr`

— MethodRemove attributes from a schema

`AlgebraicRewriting.Incremental.Algorithms.good_overlap`

— Method```
subobj
O ↣ L
↓h
I ↣ R
```

Subobject O is presumed to be abstract, i.e. has only (distinct) variables

`AlgebraicRewriting.Incremental.Algorithms.is_combinatorially_monic`

— MethodVarFunctions can both bind variables to concrete values or merge variables together. Although the overall VarFunction is not monic if either of these happens, it is only combinatorially non-monic if variables are merged together.

`AlgebraicRewriting.Incremental.Algorithms.nac_overlap`

— MethodGoal: find overlaps between a negative application condition, N, and some current state of the world, X, such that we can efficiently check if something has been deleted generates a match by allowing it to satisfy the NAC. The data:

`u`

: X ↢ X' (we are updating via some deletion) `nac`

: L → N

X and X' are big. L and N are small. X ∖ X' is small.

Let η ↣ ~N be any subobject of ~N, the complement of N, which is our best approximation to N ∖ L.

We want matches η -> X that send everything in L to something in X'. But *something* in η must map to something *not* in X'. We look at all matches and then filter.

But we can do something more efficient than enumerating Hom(η, X), as we we need only generate matches into ~u (our best approximation to the part of X that got deleted, X ∖ X').

Thus, our process for finding overlaps requires only searching for morphisms between two things which are themselves pattern-sized.

`AlgebraicRewriting.Incremental.Algorithms.partition_image`

— MethodGet the pairs for each component of the image and its component

`AlgebraicRewriting.Incremental.Algorithms.pull_back`

— MethodGiven f: L->X and m: X' ↣ X, find the unique map L -> X' making the triangle commute, if it exists.

TODO rewrite with @comptime

`AlgebraicRewriting.Incremental.Algorithms.subobject_cache`

— MethodCompute and cache the subobject classifier; reuse if already computed. Some schemas have no finitely presentable subobject classifier. Return `nothing`

in that case.

`AlgebraicRewriting.Incremental.Algorithms.to_subobj`

— MethodConvert a morphism X → Ω into a subobject X'↣X, assuming that Ω was generated by Catlab's `subobject_classifier`

function.

`AlgebraicRewriting.Rewrite.SPO.partial_pushout`

— MethodC ← 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"

`AlgebraicRewriting.Incremental.IncrementalCC`

— ModuleAn implementation for incremental hom sets where the pattern is a single connectect component (or otherwise has constraints that prevent the pattern from being broken up)

`AlgebraicRewriting.Incremental.IncrementalCC.IncCCHomSet`

— TypePackage static and runtime data together

`AlgebraicRewriting.Incremental.IncrementalCC.IncCCRuntime`

— TypeThis assumes the state of the world is changed in discrete updates.

`match_vect`

: ground source of truth. It stores, for each update to `state`

, what *new* matches were found at that time (+ still exist in the present state - hence the data must be a Dict{Int} rather than a vector, so that we can delete elements).

`key_vect`

: way of indexing this list of dicts where the first element refers to an index of `match_vect`

and the second element refers to the keys in the associated Dict. This gives us a single-integer value way of referring to *every* hom that has been seen, including the deleted ones. Thus the current # of matches is *not* `length(key_vect)`

.

`key_dict`

: the relationship between `match_vect`

and `key_vect`

. There is an one element in the dictionary for every key (across all the dictionaries in `match_vect`

). The keys of this dictionary are keys of `match_vect`

, and the values are the keys of `key_vect`

. So the current # of matches *is* length(key_dict), modulo any post-hoc constraints.

`AlgebraicRewriting.Incremental.IncrementalCC.IncCCStatic`

— TypeFor `IncCCHomSet`

the pattern (`L`

) ought be a single connected component or have constraints forcing it to be treated all at once instead of componentwise.

`AlgebraicRewriting.Incremental.IncrementalCC.add_match!`

— MethodAdd a match during a deletion

`AlgebraicRewriting.Incremental.IncrementalCC.new_nac_dpo!`

— MethodGiven dpo, a composable pair I→L→X, we use the latter morphism as a key into the NAC to access a complete set of overlaps L ↢ O → N that send *some* part of N/L to some part of L/I.

`AlgebraicRewriting.Incremental.IncrementalCC.new_nac_homs!`

— MethodGeneral method for discovering the newly added homs that arise from deleting some part of the world due to a NAC.

This function does NOT assume we have done DPO rewriting, where the possible deletions are subobjects of the pattern. Deletion can extend beyond some statically known context, a less efficient algorithm is needed.

Given an overlap which has been constructed to have *some* part intersecting with the *deleted* portion of X, we extend this to a full match N->X. This is done by forcing the overlap triangle to commute, and forcing everything not in the overlap (as well as everything in the image of `n`

, even if it is in the overlap) to go to non-deleted portions of X. Every such morphism, g, is then pulled back to X', and then precomposed with n to get a new match from P that was made possible due to the deletion X ↢ X'.

```
n
O → N ← P
↓ ↙g ↓ ↙
X ← X'
f
```

`AlgebraicRewriting.Incremental.IncrementalHom.addition!`

— MethodAdd to `matches`

based on an addition #i specified via a pushout (rmap, update)

```
For all overlaps: apex ↪ L
↓ ⇣ (find all of these!)
```

Hom(L, X*old) => Hom(L, X) Rᵢ ⟶ X rmap ⌞ ↑ update X*old

However, we only want maps L → X where elements not in the image of L are all sent to X elements which outside of the image of rmap.

This is to avoid double-counting with a slightly bigger overlap which has already been calculated between L and Rᵢ.

Note, adding things can also invalidate old matches if there are negative application or dangling conditions.

Returns the 'keys' of the deleted matches and added matches.

`AlgebraicRewriting.Incremental.IncrementalHom.deletion!`

— MethodDelete / modify existing matches based on the target ACSet being permuted or reduced to a subobject. If a match touches upon something which is deleted, remove the match. Given X ↩ X′ we are updating Hom(L, X) => Hom(L, X′)

In the presence of negative application conditions / dangling condition, a deletion can also *add* new matches. When deletion is performed by DPO, we can know statically where to search for newly added morphisms. However, if we simply have an arbitrary deletion, this is harder.

A NAC has been deactivated if there exists a morphism N ⇾ X that sends all of L to the nondeleted part of X & *some* of N to the deleted portion. The deleted portion should be *tiny* compared to the not deleted portion, so it's pretty bad to search for all morphisms N->X and filter by those which have something which has something in the deleted portion. This means we ought to compute the overlaps on the fly in the non-DPO case.

The `dpo`

flag signals that `f`

was produced via pushout complement, such that any NAC can take advantage of its cached overlaps if it has them. If it is not nothing, it contains the morphism `L ↢ I`

that was used in POC.

Returns the 'keys' of the deleted matches and added matches.

`AlgebraicRewriting.Incremental.IncrementalHom.validate`

— MethodCheck, with brute computational effort, that the IncrementalHomSet is well formed.

`Base.length`

— MethodHow many additions we've seen so far (including the initialization of the hom set). This could be confused with giving the total number of matches, which is instead `length(keys(hset))`

`Base.push!`

— MethodConsider a new addition (and compute its partial overlaps w/ the pattern)

`AlgebraicRewriting.Schedules.Theories.ThTracedMonoidalWithBidiagonals.Meta.theory`

— ConstantNo documentation found.

`AlgebraicRewriting.Schedules.Theories.##4224`

is of type `Nothing`

.

**Summary**

`struct Nothing`

**ThTracedMonoidalWithBidiagonals**

```
Ob::TYPE ⊣ []
#= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =#
Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob]
#= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =#
compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)]
(assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)]
id(a)::Hom(a, a) ⊣ [a::Ob]
(idl := compose(id(a), f) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)]
(idr := compose(f, id(b)) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)]
#= /juliateam/.julia/packages/Catlab/77h9f/src/theories/Monoidal.jl:28 =#
otimes(A, B)::Ob ⊣ [A::Ob, B::Ob]
otimes(f, g)::Hom(otimes(A, C), otimes(B, D)) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A, B), g::Hom(C, D)]
munit()::Ob ⊣ []
(otimes(otimes(A, B), C) == otimes(A, otimes(B, C))) ⊣ [A::Ob, B::Ob, C::Ob]
(otimes(munit(), A) == A) ⊣ [A::Ob]
(otimes(A, munit()) == A) ⊣ [A::Ob]
(otimes(otimes(f, g), h) == otimes(f, otimes(g, h))) ⊣ [A::Ob, B::Ob, C::Ob, X::Ob, Y::Ob, Z::Ob, f::Hom(A, X), g::Hom(B, Y), h::Hom(C, Z)]
(otimes(id(munit()), f) == f) ⊣ [A::Ob, B::Ob, f::Hom(A, B)]
(otimes(f, id(munit())) == f) ⊣ [A::Ob, B::Ob, f::Hom(A, B)]
(compose(otimes(f, g), otimes(h, k)) == otimes(compose(f, h), compose(g, k))) ⊣ [A::Ob, B::Ob, C::Ob, X::Ob, Y::Ob, Z::Ob, f::Hom(A, B), h::Hom(B, C), g::Hom(X, Y), k::Hom(Y, Z)]
(id(otimes(A, B)) == otimes(id(A), id(B))) ⊣ [A::Ob, B::Ob]
braid(A, B)::Hom(otimes(A, B), otimes(B, A)) ⊣ [A::Ob, B::Ob]
#= /juliateam/.julia/packages/Catlab/77h9f/src/theories/Monoidal.jl:87 =#
(compose(braid(A, B), braid(B, A)) == id(otimes(A, B))) ⊣ [A::Ob, B::Ob]
(braid(A, otimes(B, C)) == compose(otimes(braid(A, B), id(C)), otimes(id(B), braid(A, C)))) ⊣ [A::Ob, B::Ob, C::Ob]
(braid(otimes(A, B), C) == compose(otimes(id(A), braid(B, C)), otimes(braid(A, C), id(B)))) ⊣ [A::Ob, B::Ob, C::Ob]
(braid(A, munit()) == id(A)) ⊣ [A::Ob]
(braid(munit(), A) == id(A)) ⊣ [A::Ob]
(compose(otimes(f, g), braid(B, D)) == compose(braid(A, C), otimes(g, f))) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A, B), g::Hom(C, D)]
trace(X, A, B, f)::Hom(A, B) ⊣ [X::Ob, A::Ob, B::Ob, f::Hom(otimes(X, A), otimes(X, B))]
mmerge(A)::Hom(otimes(A, A), A) ⊣ [A::Ob]
#= /juliateam/.julia/packages/AlgebraicRewriting/6TZlx/src/schedules/Theories.jl:11 =#
create(A)::Hom(munit(), A) ⊣ [A::Ob]
#= /juliateam/.julia/packages/AlgebraicRewriting/6TZlx/src/schedules/Theories.jl:13 =#
```

`AlgebraicRewriting.Incremental`

— ModuleIncremental homomorphism search

`AlgebraicRewriting.Rewrite.Utils.Rule`

— TypeRewrite 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)

`AlgebraicRewriting.Rewrite.Utils.can_match`

— MethodReturns 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

`AlgebraicRewriting.Rewrite.Utils.freevars`

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

`AlgebraicRewriting.Rewrite.Utils.get_expr_binding_map`

— MethodDon't bind variables for things that are not ACSets

`AlgebraicRewriting.Rewrite.Utils.get_expr_binding_map`

— MethodGiven 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′

`AlgebraicRewriting.Rewrite.Utils.get_match`

— MethodGet one match (if any exist) otherwise return

`AlgebraicRewriting.Rewrite.Utils.get_matches`

— MethodGet 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.

`AlgebraicRewriting.Rewrite.Utils.get_matches`

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

`AlgebraicRewriting.Rewrite.Utils.get_pmap`

— MethodExtract the partial map (derived rule) from full output data

`AlgebraicRewriting.Rewrite.Utils.get_rmap`

— MethodExtract the map from the R to the result from the full output data

`AlgebraicRewriting.Rewrite.Utils.rewrite`

— Method`rewrite(r::Rule, G; kw...)`

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

`AlgebraicRewriting.Rewrite.Utils.rewrite_match`

— Method`rewrite_match(r::Rule, m; kw...)`

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

`AlgebraicRewriting.Schedules.Basic.Initialize`

— TypeA box that spits out a constant ACSet with an empty agent above it. Possibly, it does not take any inputs, so it can act as a comonoid counit.

`AlgebraicRewriting.Schedules.Basic.Strengthen`

— TypeAdds to both agent and the state of the world via a pushout.

```
Agent₁ → Agent₂
↓ ⇣
World₁ -->⌜World₂
```

`AlgebraicRewriting.Schedules.Basic.Weaken`

— TypeChange the agent to a subobject of the current agent without changing the world

`AlgebraicRewriting.Rewrite.Migration.pres_hash`

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

`AlgebraicRewriting.Schedules.Conditionals.Conditional`

— TypeA primitive box in a NestedDWD which does not change the state but redirects it out of one of n wires.

It contains a function (A->X) -> ℝⁿ. This optionally depends on the internal state. This weights probability for n outports, conditional on the status of an ACSet. If the function just depends on X rather than the whole morphism, `withagent`

is `false`

. If the function does not depend on the internal state (assumed to be true iff initial state is `nothing`

), then `withstate`

is `false`

.

The state and update function are by default trivial.

`AlgebraicRewriting.Schedules.Conditionals.const_cond`

— MethodCreate a branching point with fixed probabilities for each branch

`AlgebraicRewriting.Schedules.Conditionals.for_schedule`

— MethodPerform a 1-1 schedule `n`

times

`AlgebraicRewriting.Schedules.Conditionals.if_cond`

— MethodEnter the 1st branch iff the world state evaluates to true

`AlgebraicRewriting.Schedules.Conditionals.uniform`

— MethodA uniform chance of leaving each of n branches

`AlgebraicRewriting.Schedules.Conditionals.while_schedule`

— MethodPerform a 1-1 schedule until a condition is met

`AlgebraicRewriting.Incremental.IncrementalConstraints.AC`

— TypeAn application condition (w/r/t a pattern, L) is given by a morphism out of L. This can be given two semantics, based on the existence of a particular morphism making a triangle commute. We can furthermore impose monic constraints on that derived morphism.

`AlgebraicRewriting.Incremental.IncrementalConstraints.AC`

— TypeCoerce a general `Constraint`

into a simple application condition, if possible. This works if the `Constraint`

was created by `AppCond`

.

`AlgebraicRewriting.Incremental.IncrementalConstraints.IncConstraints`

— TypeWe may not be merely interested maintaining a set of matches Hom(L,X), but instead we care only about the monic morphisms, or morphisms that satisfy some positive/negative application conditions (PAC/NAC). In particular, NAC poses a new challenge: deletion can introduce new matches. There are various ways of dealing with this, one of which would require predeclaring `deletion`

morphisms `L ↢ I`

. However, that approach would only work for DPO. So a less efficient approach that uses only the data of X ↢ X′ and I→N is to search for all morphisms that send *some* part of N to a deleted part of X and all of L to the nondeleted part of X (this will find all of the new morphisms, only the new morphisms, but will possibly contain duplicates).

TODO add `dangling`

field

`AlgebraicRewriting.Incremental.IncrementalConstraints.NAC`

— TypeA negative application condition L -> N means a match L -> X is invalid if there exists a commuting triangle.

We cache the subobjects of ~N (our best approximation to the things that are in N but not in L), as this can be taken advantage of in detecting new matches when we delete something.

dpo argument allows us to pass in a morphism I->L so that we can compute the staticly known overlaps beforehand, rather than at runtime. These are partial overlaps between N and L, which enumerate the possible ways a part of N can be sent to something that is deleted (part of L/I).

`AlgebraicRewriting.Incremental.IncrementalConstraints.PAC`

— TypeA positive application condition L -> P means a match L -> X is valid only if there does not exist a commuting triangle.

When we add something via some addition: O -> R, this could activate hitherto invalid matches which were blocked by a PAC. To detect these incrementally, we cache overlaps (indexed by possible additions) that store the ways in which the addition could intersect with P.

`AlgebraicRewriting.Incremental.IncrementalConstraints.can_match`

— MethodCheck whether a putative hom meets the constraints. Kwargs control which checks are run. Often these homs are generated via hom search using the monic constraint, so the monic constraint is usually not checked.

`AlgebraicRewriting.Incremental.IncrementalConstraints.compat_constraints`

— MethodCheck if a rule imposes the same constraints as captured by an IncConstraint

TODO handle dangling condition specially (add it as a field to IncConstraints)

`AlgebraicRewriting.Rewrite.SqPO.final_pullback_complement`

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

`AlgebraicRewriting.Rewrite.Utils.rewrite_match_maps`

— Method`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