A graphical language for rewriting-based programs and agent-based models

Kris Brown, David Spivak - ACT 2023


(press s for speaker notes)

8/1/23

Introduction - examples

$$

$$

• Game of Life

• COVID modeling

• Discrete Lotka Volterra

Let me start right off with the engineering problem we’re trying to tackle. An important class of scientific models are agent-based models - there are types of agents and they interact in various ways, not much more you can say in general about them. Here are three motivating examples:

Now the problem: how do we represent these models? Whether we are researchers or professional engineers, it’s important that people can communicate their models of the world and perform high-level operations on them, such as comparing, combining, editing, visualizing. Unfortunately, the status quo for agent-based models is that, despite the modeler’s high-level conceptual understanding of the model, the only formal artifact is a piece of code.

Introduction - examples

• Game of Life (link)

mutable struct Cell <: AbstractAgent
  id::Int; pos::Tuple{Int,Int}; status::Bool
end

function ca_step!(model)
  new_status = fill(false, nagents(model))
  for (agid, ag) in model.agents
      nlive = nlive_neighbors(ag, model)
      if ag.status == true && (nlive ≤ model.rules[4] && nlive ≥ model.rules[1])
          new_status[agid] = true
      elseif ag.status == false && (nlive ≥ model.rules[3] && nlive ≤ model.rules[4])
          new_status[agid] = true
      end
  end

  for k in keys(model.agents)
      model.agents[k].status = new_status[k]
  end
end

• COVID modeling (link)

mutable struct Agent <: AbstractAgent
  id::Int; pos::NTuple{2,Float64}
  vel::NTuple{2,Float64};  mass::Float64
end

function elastic_collision!(a, b, f = nothing)
  v1, v2, x1, x2 = a.vel, b.vel, a.pos, b.pos
  length(v1) != 2 && error("This function works only for two dimensions.")
  r1 = x1 .- x2; r2 = x2 .- x1
  m1, m2 = f == nothing ? (1.0, 1.0) : (getfield(a, f), getfield(b, f))
  !(dot(r2, v1) > 0 && dot(r2, v1) > 0) && return false
  f1,f2 = (2m2/(m1+m2)), (2m1/(m1+m2))
  ken = norm(v1)^2 + norm(v2)^2
  dx = a.pos .- b.pos
  dv = a.vel .- b.vel
  n = norm(dx)^2
  n == 0 && return false # do nothing if they are at the same position
  a.vel = v1 .- f1 .* ( dot(v1 .- v2, r1) / n ) .* (r1)
  b.vel = v2 .- f2 .* ( dot(v2 .- v1, r2) / n ) .* (r2)
  return true
end

• Discrete Lotka Volterra (link)

create-sheep initial-number-sheep  ; create the sheep, then init vars
[
  set shape  "sheep"
  set color white
  set size 1.5  ; easier to see
  set label-color blue - 2
  set energy random (2 * sheep-gain-from-food)
  setxy random-xcor random-ycor
]

to eat-sheep  ; wolf procedure
  let prey one-of sheep-here                    ; grab a random sheep
  if prey != nobody  [                          ; did we get one? if so,
    ask prey [ die ]                            ; kill it, and...
    set energy energy + wolf-gain-from-food     ; get energy from eating
  ]
end

to death  ; turtle procedure (i.e. both wolf and sheep procedure)
  ; when energy dips below zero, die
  if energy < 0 [ die ]
end

; stop the model if there are no wolves and no sheep
; stop the model if there are no wolves and the number of sheep gets very large
if not any? wolves and count sheep > max-sheep [ user-message "The sheep have inherited the earth" stop ]
ask sheep [
  move
  ; in this version, sheep eat grass, grass grows, and it costs sheep energy to move
  if model-version = "sheep-wolves-grass" [
    set energy energy - 1  ; deduct energy for sheep only if running sheep-wolves-grass model version
    eat-grass  ; sheep eat grass only if running the sheep-wolves-grass model version
    death ; sheep die from starvation only if running the sheep-wolves-grass model version
  ]
  reproduce-sheep  ; sheep reproduce at a random rate governed by a slider
]
ask wolves [
  move
  set energy energy - 1  ; wolves lose energy as they move
  eat-sheep ; wolves eat a sheep on their patch
  death ; wolves die if they run out of energy
  reproduce-wolves ; wolves reproduce at a random rate governed by a slider
]

On the left the models are in Julia using a library called Agents.jl. The general workflow is to make a custom data type for each agent and to describe their interactions via arbitrary Julia functions. On the right, the wolf-sheep model was written in NetLogo, a language designed for agent-based modeling. You can see the declaration of the sheep agent, some of its interactions, as well as the overall control flow for the whole simulation.

Introduction - ACT philosophy

General-purpose code not a great syntax for scientific modeling

Some desired properties for a model representation:

• Compositional, e.g.
  • Straightforward to make the Game of Life into a 3D game
  • Straightforward to share behaviors between wolves and sheep
  • Straightforward to combine COVID dynamics with a vaccination model

• Transparent / verifiable / visualizable

• Serializable + Implementation-agnostic

• Flexible, e.g. 

  • Straightforward to change semantics (deterministic, nondeterministic, probabilistic)

But these properties do tend to follow from giving a nice syntax category (e.g. presheaves, Poly) a computational semantics.

. . .

What is inadequate about “the code is the model”? We want the following virtues… But general purpose code is lacking in many ways. Making changes to one part of the code may have unpredictable consequences elsewhere. Combining two models at a high level via a limit or colimit is not feasible.

Introduction - problem statement

Rewrite rules (e.g. DPO, SPO) are a good syntax for small / local changes

How can we design a model with rewrite rules as primitive building blocks?

• Need to specify control flow (if…then…else, while…)
• Need to specify rewrite rules as well as control their matches

E.g. for each vertex \(v\):

• If \(v\) has no neighbors, delete it
• Else, look at its neighbors \(v\rightarrow v'\)
  • Flip a coin
  • If heads, add a loop to \(v'\)

function simulate(G::Graph)
  for v in vertices(G)
    vsᵢ, vsₒ = inneighbors(G, v), outneighbors(G, v)
    if isempty(vsᵢ ∪ vsₒ)
      apply_rule(DELETE_VERTEX, G; initial=(V=[v],))
    else
      for v′ in vsₒ
        if rand([false, true])
          apply_rule(ADD_LOOP, G; initial(V=[v′],))
        end
      end
    end
  end
end

We do have a good category-theoretic understanding of rewrite rules. What might be surprising is that there didn’t exist a principled strategy for combining these rules into larger workflows. The most straightforward way of accomplishing this is to use a general programming language as the glue which does this, including control of how we apply the rewrite rules.

Punchline

function simulate(G::Graph)
  for v in vertices(G)
    vsᵢ, vsₒ = inneighbors(G, v), outneighbors(G, v)
    if isempty(vsᵢ ∪ vsₒ)
      apply_rule(DELETE_VERTEX, G; initial=(V=[v],))
    else
      for v′ in vsₒ
        if rand([false, true])
          apply_rule(ADD_LOOP, G; initial(V=[v′],))
        end
      end
    end
  end
end

This is what we’re building towards - I hope you’ll be able to understand this graphical program on the left as performing the same simulation as the code on the right.

Introduction: AlgebraicJulia & AlgebraicRewriting.jl

AlgebraicJulia is a computational category-theoretic software ecosystem.

Catlab.jl defines the core data structures and algorithms with a focus on computing with presheaf categories. For example, consider the category Grph of presheaves on the schema (i.e. small category) \(E \rightrightarrows V\)

using Catlab
g = path_graph(Graph, 3)

Graph with elements V = 1:3, E = 1:2

E	src	tgt
1	1	2
2	2	3

# Visualize with Graphviz
to_graphviz(g)

AlgebraicRewriting.jl extends Catlab.jl to include many constructions developed by the graph transformation community.

using AlgebraicRewriting  # create DPO rule: • <- • -> •↺
add_loop = Rule(id(Graph(1)), delete(Graph(1)))
rewrite(add_loop, g) |> to_graphviz

One possibility is to work in the AlgebraicJulia ecosystem, which supports programming with category-theoretic abstractions. The basic data structure here is the C-set, i.e. a copresheaf or a functor from a small category C into Set. This is also thought of as a category of databases on the schema, C. One particular schema has two objects and two nonidentity arrows, for the category of directed multigraphs.

AlgebraicRewriting’s most basic feature is to declare rewrite rules and apply them to instances.

Outline

1. Introduction
   • Example models, Other approaches, ACT philosophy, AlgebraicJulia
2. Motivating the dynamic Kleisli category, \(DK_t\)
   • Mealy Machines
     • Rewrite and ControlFlow generators
     • Agent-based modeling: controlling match morphisms
   • Quotienting by behavioral equivalence
   • Enriching in \(\mathbf{Cat}^\#\)
   • Parameterizing by polynomial monad
3. Conjecture: \(DK_t\) is traced
4. More primitive generators
   • Query, Weaken, Fail generators
   • Putting it all together
   • Examples: Game of Life, COVID, Lotka Voltera

So I will introduce the various pieces of our solution gradually in order to explain why they were necessary for our purposes. I’ll briefly comment about a conjecture of ours which licenses us to use wiring diagrams with feedback loops, though this point is fairly irrelevant because the formalism has already proven itself useful in guiding an implementation that addresses the problems I’ve mentioned. So I’ll try to spend most of the time explaining how we can view compositions of a few generating morphisms in our Dynamic Kleisli category as a syntax for the sorts of graph rewriting programs and agent-based models we are interested in.

Towards dynamic Kleisli categories - Mealy Machines

\[Ob_{\mathbf{Meal}} := Ob(\mathsf{Set})\] \[Hom_{\mathbf{Meal}}(A,B) := \left\{\left(S : \mathsf{Set},\ s_0 : S,\ \phi\colon A\times S\to S\times B\right)\right\}\]

Consider a case with \(S=1\), e.g. the rewrite rule add_loop as a morphism \(Grph \rightarrow Grph + Grph\):

Loop = RuleApp(:add_loop, add_loop) |> singleton
view_sched(Loop)

extract(res) = res |> traj_res |> traj_res
@test apply_schedule(Loop, Graph())[2] |> extract == Graph()

Test Passed

res = apply_schedule(Loop, path_graph(Graph,3))
res[1] |> extract |> to_graphviz

Our starting point is the symmetric monoidal category of Mealy Machines. We also call these “dynamic” functions because they are like a function which you can run, but the input can alter the ‘internal state’ of the function and change its behavior.

. . .

We visualize using the symmetric monoidal structure of Set and coproducts.

Agent-based modeling

A wire labeled by \(A \in Ob(\mathsf{C})\) represents the set \(Ob(A/\mathsf{\mathsf{C}}\text{-}\mathsf{Set})\).

\(A\) is the shape of an agent living in a world \(X\) given by the morphism \(A \rightarrow X\). Being able to keep track of a distinguished subobject enables us to have control over matches.

Previously, the morphism add_loop had the semantics of ‘add a loop to some vertex’

With the ability to have distinguished agents, this morphism has the semantics of ‘add a loop to this vertex’.

Primitive generators

Previously a Grph rewrite was \(Grph \rightarrow Grph + Grph\); now it is \(A/Grph \rightarrow B/Grph + A/Grph\) (in shorthand: \(A \rightarrow B + A\)).

• two output ports, depending on whether the rule is successfully applied.
• AlgebraicRewriting.jl rules can have application conditions and alternate semantics (e.g. SPO, SqPO).

G0, G1 = Graph(), Graph(1)
del_v = Rule(create(G1), id(G0))
aL = RuleApp(:addLoop, add_loop, G1) # agent in = agent out = • 
dV = RuleApp(:delV, del_v, id(G1), id(G0)) # explicit agents
recipe = aL ⋅ merge_wires(G1) ⋅ dV
view_sched(recipe)

# Example: second vertex is current focus
G = homomorphisms(G1, path_graph(Graph, 3))[2] 
res1, res2 = apply_schedule(recipe, G)
@assert isempty(res1)
res2 |> extract |> to_graphviz

A rewrite rule is no longer Grph -> Grph+Grph but rather A/Grph -> A/Grph+B/Grph

Towards dynamic Kleisli categories - Mealy Machines

Control flow: consider a class of Mealy machines \(A \rightarrow A + A\) with \(S=\mathbb{N},s_0=3\) that acts as a for loop, by returning the first element iff \(s > 0\).

Loop2 = for_schedule(Loop⋅merge_wires(Graph()), 2)
view_sched(Loop2)

res = apply_schedule(Loop2, path_graph(Graph,3))
res[1] |> extract |> to_graphviz

The Condition (or ControlFlow) primitive morphism is allowed to have nontrivial state but does not alter its inputs. Thus it must be a morphism \(A \rightarrow n \times A\).

We might imagine a different kind of function we want as a building block.

Towards dynamic Kleisli categories - Mealy Machines

Let’s make a morphism which behaves like add_loop for the first three times the function is run and subsequently like delete_vertex:

\[ Grph \rightarrow Grph + Grph \] \[For3 \operatorname{⨟}(AddLoop \otimes DelVertex) \operatorname{⨟}(id_{Grph} \otimes \sigma_{Grph,Grph} \otimes id_{Grph}) \operatorname{⨟}\nabla_{Grph} \otimes \nabla_{Grph} \]

Here is an example composition of both sorts of Mealy Machines. We are off to a good start, as we have a formalism that can incorporate rewrite rules as well as control flow. Here we are using the braid icons and the merging of wires coming from basic operations in Set.

Towards dynamic Kleisli categories - Quotienting by behavioral equivalence

Our monoidal product \(\otimes\) comes from the coproduct in Set, but it is not a coproduct in Meal.

Up until this point we have been speaking of the Mealy machines and their behavior fairly interchangably, but there is an important difference. Two distinct Mealy machines could have the same behavior (for example, due to having different state spaces). It turns out we really want to be talking about behaviors rather than the Mealy machines themselves. This is evidenced by the fact that the coproduct in Set is not a coproduct in Meal (which would require the pictured equality to hold). To address this, we need to think of Mealy machines as just convenient presentations of our real object of study.

Towards dynamic Kleisli categories - Quotienting by behavioral equivalence

The behavior of a morphism \(A \rightarrow B\) is an infinite tree whose nodes are functions \(A \rightarrow B\) and which has a branching factor of \(A\).

Impractical to draw the behavior tree explicitly with infinite sets.

However, for a Mealy machine with domain \(\Sigma_i A_i\):

• It can be the case that state update \(\phi;\pi_1: S \times \Sigma_i A_i \rightarrow S\) is purely determined by \(S \times I\).
• When this condition is met, we can draw the tree as branching on the number of input wires into a box.

We represent behaviors with trees. It’s difficult to visualize these when the domain is infinite, but we can draw these with a finite branching factor if this diagram commutes.

Towards dynamic Kleisli categories - Quotienting by behavioral equivalence

Consider this variant and its behavior tree:

bt = BTree(Mealy(RuleApp(:add_loop, add_loop), Maybe))
bt.S

Dict{Vector{BTreeEdge}, Any} with 1 entry:
  [] => nothing

wv = WireVal(1, Traj(create(Graph())))
(outedge, msg), = bt(BTreeEdge[], wv)
outedge.o

WireVal(2, Traj(ACSetTransformation((V = FinFunction(Int64[], 0, 0), E = FinFunction(Int64[], 0, 0)), Graph {V = 0, E = 0}, Graph {V = 0, E = 0}), TrajStep[TrajStep(ACSetTransformation((V = FinFunction(Int64[], 0, 0), E = FinFunction(Int64[], 0, 0)), Graph {V = 0, E = 0}, Graph {V = 0, E = 0}), Multispan{Graph, StructTightACSetTransformation{TypeLevelBasicSchema{Symbol, Tuple{:V, :E}, Tuple{(:src, :E, :V), (:tgt, :E, :V)}, Tuple{}, Tuple{}}, NamedTuple{(:V, :E), Tuple{Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}, Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}}}, Graph, Graph}, StaticArraysCore.SVector{2, StructTightACSetTransformation{TypeLevelBasicSchema{Symbol, Tuple{:V, :E}, Tuple{(:src, :E, :V), (:tgt, :E, :V)}, Tuple{}, Tuple{}}, NamedTuple{(:V, :E), Tuple{Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}, Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}}}, Graph, Graph}}}(Graph:
  V = 1:0
  E = 1:0
  src : E → V = Int64[]
  tgt : E → V = Int64[], StructTightACSetTransformation{TypeLevelBasicSchema{Symbol, Tuple{:V, :E}, Tuple{(:src, :E, :V), (:tgt, :E, :V)}, Tuple{}, Tuple{}}, NamedTuple{(:V, :E), Tuple{Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}, Catlab.CategoricalAlgebra.FinSets.FinDomFunctionVector{Int64, UnitRange{Int64}, Catlab.CategoricalAlgebra.FinSets.FinSetInt}}}, Graph, Graph}[ACSetTransformation((V = FinFunction(1:0, 0, 0), E = FinFunction(1:0, 0, 0)), Graph {V = 0, E = 0}, Graph {V = 0, E = 0}), ACSetTransformation((V = FinFunction(1:0, 0, 0), E = FinFunction(1:0, 0, 0)), Graph {V = 0, E = 0}, Graph {V = 0, E = 0})]))]))

bt.S

Dict{Vector{BTreeEdge}, Any} with 2 entries:
  []                                                                  => nothing
  [BTreeEdge(WireVal(1, Traj(ACSetTransformation((V = FinFunction(In… => nothing

A behavior tree factors out the dependence on state into the structure of the tree, so two morphisms presented by different Mealy machines could have identical behavior trees.

The nothing here is the internal state, which is the unit for stateless boxes like rewrite rules.

Towards dynamic Kleisli categories - Quotienting by behavioral equivalence

\[Ob_{\mathbf{Meal/\sim}} := Ob(\mathsf{Set})\] \[Hom_{\mathbf{Meal/\sim}}(A,B) := Ob(\mathfrak{c}([Ay,By]))\]

\[Ob_{\mathbf{DynMeal}} := Ob(\mathsf{Set})\] \[Hom_{\mathbf{DynMeal}}(A,B) := \mathfrak{c}([Ay,By])\]

Where

• \([p,q]\) is the internal hom in Poly
• \(\mathfrak{c}\) is the cofree comonad functor \(\mathbf{Poly} \rightarrow \mathbf{Cat^\#}\)
• \(\mathbf{Cat^\#}\) is the category of categories and cofunctors.

The set of behavior trees is in bijection with the underlying set of the final coalgebra on \(X \rightarrow B^AX^A\). But we prefer to think about the category of morphisms \(A \rightarrow B\):

• this category makes explicit the dynamic nature of these systems, rather than just being a static object with a (fixed) initial state.

One way of characterizing this set of behavior trees is by observing that they are the objects of a particular category,

Why poly (cofree comond) over coalg?

1. It’s weird to encode the current state into coalg, natural for cofree (tree has a root)
2. behavioral equivalence is extra for coalg,
3. Everything is in poly, can apply monads, etc. Staying in a sandbox.

. . .

Our set of homs now have morphisms among them encoding the possible evolutions (producing a new morphism in DynMeal, i.e. a new system ready for input). We no longer have to ‘run’ the dynamic functions in our heads, outside of the formalism.

Towards dynamic Kleisli categories - Monadic output

\[Ob_{\mathbf{DK_t}} := Ob(\mathsf{Set})\] \[Hom_{\mathbf{DK_t}}(A,B) := \mathfrak{c}([Ay,t \triangleleft By])\]

We can readily generalize our notion of a morphism \(A \rightarrow B\).

\[Maybe = y+1\]

\[Writer = My\]

\[List = \sum_{N : \mathbb{N}} y^N\]

\[Lott = \sum_{N : \mathbb{N}} \Delta_N y^N\]

where \(M\) is a monoid and \(\Delta_N:=\{P:N\rightarrow [0,1]\ |\ 1=\sum P(i)\}\)

Because we intend to use control flow with loops, is essential that we at least work with something like the maybe monad, otherwise our formalism doesn’t have the resources to describe an infinite looping computation. But we need not be restricted to Maybe, we might be interested in non-deterministic computations
or probabalistic ones (where a morphism takes an input and returns a distribution on its outputs).

Conjectured trace structure

A trace structure licenses a graphical syntax with feedback loops.

Even without proving the purported trace structure, the theory has influenced an implementation.

We show ours is an enrichment of the trace of partial functions. The description of the trace of partial functions feels like a process, we think that we are describing the process.

Below we have an example of how the theory underlies our implementation. This is a composite of three primitive morphisms, which each have a behavior tree being lazily expanded as necessary. \(b_1\) is fed to \(f\) to start the process, which updates the corresponding tree. A singleton list is computed to be the output.

Conjectured trace structure

A trace structure licenses a graphical syntax with feedback loops.

Even without proving the purported trace structure, the theory has influenced an implementation.

These three values are separate trajectories which are run through the entire morphism. They each enter \(g\) and each produce a singleton value which ends up going to \(f\), and so on. We follow all the trajectories until they have all collected at the rightmost outports and then apply our monadic multiplication (in this case, concatenation) to produce output values.

Towards dynamic Kleisli categories - Enriching in \(\mathbf{Cat}^\#\)

Poly morphisms are forwards on positions (trees) and backwards on directions (ways of updating): composition builds larger trees from smaller ones and decomposes updates of the larger system into corresponding updates of the smaller systems.

What was our justification for maintaining a separate behavior tree for each primitive morphisms rather than combining them all into one gigantic one?

The composition of subsystems leads to a decomposition of behaviors: given a behavior of a composite system, we can compute how the corresponding components must have updated.

Towards dynamic Kleisli categories - Enriching in \(\mathbf{Cat}^\#\)

Here’s an example of ‘running’ this morphism three times with inputs left, right, left (aka bottom top bottom). This ‘running’ is itself a morphism between morphisms, from the composite to the composite prime, and the data of this composite as the composition of \(\phi\) and \(\psi\) tells us how to obtain morphisms \(\phi\rightarrow \phi'\) and \(\psi\rightarrow \psi'\)

More primitive generators

Although RuleApp and ControlFlow are the workhorse generators, we need others to facilitate the changing of control from agent to agent. Consider the Query morphism \(A + B' \rightarrow A + B + 0\), whose basic behavior is determined by the types \(A\) and \(B\) on its ports:

Empty, Dot = Symbol(" "), Symbol("•")
N=Names(Dict(" " => Graph(), "•" => Graph(1)))
recipe = agent(tryrule(aL))
view_sched(recipe; names=N)

apply_schedule(recipe, path_graph(Graph, 3)) |> first |> extract |> to_graphviz

So now we understand what underlies our Rewrite and ControlFlow boxes and the category they live in, such that we can draw traced diagrams. These are the ‘heavy lifting’ generators but we need a couple more in order to make usable agent-based models. Them missing ingredient is the ability to switch control flow.

Query boxes play the role of “for all agents (i.e. subobjects of shape \(B\)), do this subroutine”. Afterwards we return to our original agent.

(If our original agent no longer exists (e.g. the map \(A \rightarrow X\) points to something that got deleted in the process of running the subroutine for every \(B\)), then we can still exit with the trivial/empty agent, which is the third outport.)

More primitive generators

The last two generators of importance are Weaken and Fail. Both are stateless.

• Weaken is a morphism \(B \rightarrow A\) and is specified by a morphism \(Hom_{C\mathsf{Set}}(A,B)\).
  • It acts upon an agent via precomposition.

• Fail is a morphism which throws the monadic exception.

Weaken takes an agent and changes focus to a subagent of that agent.

Putting it all together

If \(v\) has no neighbors, delete it else…

\(\forall v\rightarrow v'\), if coin flip is heads, add a loop to \(v'\)

G0, G1 = Graph.(0:1); arr = path_graph(Graph, 2)
N=Names(Dict(" "=>G0,"•"=>G1,"•→•"=>arr));Arr=Symbol("•→•")
s_hom, t_hom = homomorphisms(G1, arr);

add_loop = RuleApp(:add_loop, Rule(id(G1), delete(G1)), G1);
del_vertex = RuleApp(:del_vertex, del_v, id(G1), id(G0))
per_edge = mk_sched((;),(i=Arr,), N, 
  (flip=uniform(2, Graph(1)), weak=Weaken(:Switch_to_tgt, t_hom), rule=add_loop), 
  quote
    flip_yes, flip_no = flip(weak(i))
    rule_yes, rule_no = rule(flip_yes)
    return [flip_no, rule_yes, rule_no]
  end
);

view_sched(per_edge; names=N)

constr = Constraint(@acset(CGraph, begin V=3; E=3; src=[2,1,2]; tgt=[1,3,3]; vlabel=[arr, G1, nothing]; elabel=[s_hom, 1, 2] end), Commutes([1,2],[3]))
edge_loop = agent(per_edge, G1; n=:out_edge, 
                  ret=G1, constraint=constr)
view_sched(edge_loop; names=N)

wv = Weaken(:Discard_vertex, create(G1))
per_vertex = (del_vertex ⋅ 
  (id([G0]) ⊗ (edge_loop ⋅ wv)) ⋅ merge_wires(G0))
per_vertex_loop = agent(per_vertex; n=:vertex, ret=G0)
view_sched(per_vertex_loop; names=N)

This is building up the simulation we originally set out to make (using the Maybe monad semantics for all the generators). We start out by building per_edge which says what we want to do with each edge \(v \rightarrow v'\) (this is visualized on the bottom left). We then wrap that in a query that runs for every edge out of \(v\). We then wrap that in a query which runs for every \(v\), though first we try to apply delete_vertex and we only do the edge query if that fails (which is true iff the edge is not isolated).

Putting it all together

function simulate(G::Graph)
  for v in vertices(G)
    vsᵢ, vsₒ = inneighbors(G, v), outneighbors(G, v)
    if isempty(vsᵢ ∪ vsₒ)
      apply_rule(DELETE_VERTEX, G; initial=(V=[v],))
    else
      for v′ in vsₒ
        if rand([false, true])
          apply_rule(ADD_LOOP, G; initial(V=[v′],))
        end
      end
    end
  end
end

And we’re back here again. The visualization shows the trajectory as it passes through various boxes. Below we show the before and after of each box. You can see the agent shifting and modifications to the state. We now have a structured representation (a morphism in a category with lots of structure) that can be given the same computational semantics as the original, unstructured Julia program.

Putting the formalism to work

• Game of Life

• Lotka Volterra

• COmplexVID19

• Expository blog post

This was obviously a complete toy example, but the real goal has been to apply this to more meaty problems, such as representing epidemiology models. Here is a rendition of the recipe for a lotka-volterra ecology model.

Conclusion

• Game of Life

• Lotka Volterra

• COmplexVID19

• Expository blog post

Much more to say about performance

• Unbiased vs biased implementations
• In-place rewriting
• Mark-as-deleted
• Schema-specific code compilation
• Incremental homomorphism search

Advantages from formalism

• Compositional, e.g. data migration
• Transparent / verifiable / visualizable
• Serializable + Implementation-agnostic
• Flexible to change semantics

GCM 2023 paper: Dynamic Tracing: a graphical language for rewriting protocols

\[\text{Thank you for listening!}\]

Thank you!

Bonus slide - other approaches

What is a good syntax for talking about the algorithmic application of rewrite rules?

• Need to specify control flow (if…then…else, while…)
• Need to specify rewrite rules as well as control their matches

General strategies

1. Unordered rules, but control via constraints / maintain program state ‘in the graph’
   • Unwieldly / complex / indirect control flow via application conditions
   • Incorporation of implementation details into graph / world state

So these are the desiderata.

. . . Let me classify some approaches this problem into broadly three camps. The first is to allow rules to be applied so long as they are valid, but to take extreme care in crafting things like positive and negative application conditions (as well as putting in special nodes into one’s graph to control the flow). This is not very transparent, even if it’s not arbitrary code, and it blends together the ‘real’ parts of the model and the ‘implementation details’.

Bonus slide - other approaches

What is a good syntax for talking about the algorithmic application of rewrite rules?

• Need to specify control flow (if…then…else, while…)
• Need to specify rewrite rules as well as control their matches

General strategies

1. Unordered rules, but control via constraints / maintain program state ‘in the graph’
2. Directed graph of rewrite rules
   • No control of matches
   • No complex control flow

Second option. Problem. Can be mitigated if we take recourse to strategy 1, but we don’t want to do that.

Bonus slide - other approaches

What is a good syntax for talking about the algorithmic application of rewrite rules?

• Need to specify control flow (if…then…else, while…)
• Need to specify rewrite rules as well as control their matches

General strategies

1. Unordered rules, but control via constraints / maintain program state ‘in the graph’
2. Directed graph of rewrite rules
3. General program with rewrite primatives
   • No explicit control of matches
   • Program language syntax

The third option which is very practical is to just use a general programming language that has access to a graph rewriting library and use rewrites to perform the heavy lifting. This has the aforementioned issues from making one’s syntax a general purpose programming language, although by factoring out a large portion of the model into rewrite rules the situation is still greatly improved from the status quo.

In this talk I will something ‘in between’ these last two options, something expressive yet still working in a category with nice structure which can then be given a computational semantics.