RFC-0001: tracking issue

[tim-at-topos]

This is the tracking issue for freezing RFC-0001 (#1052). It should be closed once we're happy that we've "fully operationalised" the RFC.

[tim-at-topos]

Having spoken with @epatters and @tslil-topos , here is my current sketch plan:

A. Dev facing

1. Allow for non-unital double theories
   Add flag and typing to DblTheory to match RFC-0001 #1145
   Make modal theories generic over kind of double theory #1161
2. Implement the non-unital modal double theory of Polynomial ODE systems (4.1 in the RFC), i.e. non-unital symmetric multicategories; hard-code models for Lotka–Volterra, linear ODE, and mass-action in catlog/src/stdlib/models.rs
   feature: allow NonUnital ModalDblModel, implement theory of non-unital symmetric mult-categories, implement toy Lotka-Volterra style model #1162
3. Refactor the corresponding analyses* to use these models

*currently this will just be mass-action, unless #965 gets resolved before we hit this point

B. User facing

1. Make a logic for Polynomial ODE systems
2. Configure some notebook cell editors to allow users to build models in this theory in a nice-looking way

Once these are done, I would consider this RFC addressed. The obvious next step would be to think about the "Future possibilities" section, which would probably look like the following:

C. Future possibilities

1. Create a "Custom ODE dynamics" analysis that allows users to apply their own ODE models to their own e.g. CLD models
2. Figure out how much this implementation differs from the mathematical story sketched out in the RFC
3. Bridge the gap

[tim-at-topos]

@epatters I'm a bit confused about step A.3 above. Here are two interpretations (using an entirely made-up language, sorry) that tslil and I came up with:

1. In e.g. lotka_volterra.rs, when we iterate over morphisms in the model we use lotka_volterra_dynamics() to figure out what polynomials we should build

for ob in model.objects
  system[src] += lotka_volterra_dynamics(x = ob)
end

for mor in model.morphisms
  system[src] += lotka_volterra_dynamics(a = mor.src, b = mor.tgt)
end

2. In e.g. lotka_volterra.rs, when we iterate over morphisms in the model we use lotka_volterra_dynamics() to build an entire new model in the theory of polynomial ODE systems, and then elsewhere have a thing that actually turns such models into something a solver can solve (e.g. by building a PolynomialSystem from it)

for ob in model.objects
  ode_model.instantiate(lotka_volterra_dynamics(x = ob))
end

for mor in model.morphisms
  ode_model.instantiate(lotka_volterra_dynamics(a = mor.src, b = mor.tgt))
end

solve(ode_model)

Do either of these sound like what you were envisioning? Sitting down and thinking about it made me realise that I only actually understand the mathematical aspect of this story, not the implementation one!