catlog/stdlib/
theories.rs

1//! Standard library of double theories.
2
3use crate::dbl::theory::*;
4use crate::one::{Path, fp_category::FpCategory};
5use crate::zero::name;
6
7/// The empty theory, which has a single model, the empty model.
8///
9/// As a double category, this is the initial double category.
10pub fn th_empty() -> DiscreteDblTheory {
11    FpCategory::new().into()
12}
13
14/// The theory of categories, aka the trivial double theory.
15///
16/// As a double category, this is the terminal double category.
17pub fn th_category() -> DiscreteDblTheory {
18    let mut cat = FpCategory::new();
19    cat.add_ob_generator(name("Object"));
20    cat.into()
21}
22
23/// The theory of database schemas with attributes.
24///
25/// As a double category, this is the "walking proarrow".
26pub fn th_schema() -> DiscreteDblTheory {
27    let mut cat = FpCategory::new();
28    cat.add_ob_generator(name("Entity"));
29    cat.add_ob_generator(name("AttrType"));
30    cat.add_mor_generator(name("Attr"), name("Entity"), name("AttrType"));
31    cat.into()
32}
33
34/// The theory of signed categories.
35///
36/// A *signed category* is a category sliced over the group of (nonzero) signs. Free
37/// signed categories are signed graphs, a simple mathematical model of [regulatory
38/// networks](crate::refs::RegNets) and causal loop diagrams.
39pub fn th_signed_category() -> DiscreteDblTheory {
40    let mut sgn = FpCategory::new();
41    sgn.add_ob_generator(name("Object"));
42    sgn.add_mor_generator(name("Negative"), name("Object"), name("Object"));
43    sgn.equate(Path::pair(name("Negative"), name("Negative")), Path::empty(name("Object")));
44    sgn.into()
45}
46
47/// The theory of delayable signed categories.
48///
49/// Free delayable signed categories are causal loop diagrams with delays, often
50/// depicted as [caesuras](https://en.wikipedia.org/wiki/Caesura).
51pub fn th_delayable_signed_category() -> DiscreteDblTheory {
52    let mut cat = FpCategory::new();
53    cat.add_ob_generator(name("Object"));
54    cat.add_mor_generator(name("Negative"), name("Object"), name("Object"));
55    cat.add_mor_generator(name("Slow"), name("Object"), name("Object"));
56    cat.equate(Path::pair(name("Negative"), name("Negative")), Path::empty(name("Object")));
57    cat.equate(Path::pair(name("Slow"), name("Slow")), name("Slow").into());
58    cat.equate(
59        Path::pair(name("Negative"), name("Slow")),
60        Path::pair(name("Slow"), name("Negative")),
61    );
62
63    // NOTE: These aliases are superfluous but are included for backwards
64    // compatibility with the previous version of the theory, defined by an
65    // explicit multiplication table.
66    cat.add_mor_generator(name("PositiveSlow"), name("Object"), name("Object"));
67    cat.add_mor_generator(name("NegativeSlow"), name("Object"), name("Object"));
68    cat.equate(name("PositiveSlow").into(), name("Slow").into());
69    cat.equate(name("NegativeSlow").into(), Path::pair(name("Negative"), name("Slow")));
70
71    cat.into()
72}
73
74/// The theory of nullable signed categories.
75///
76/// A *nullable signed category* is a category sliced over the monoid of signs,
77/// including zero.
78pub fn th_nullable_signed_category() -> DiscreteDblTheory {
79    let mut sgn = FpCategory::new();
80    sgn.add_ob_generator(name("Object"));
81    sgn.add_mor_generator(name("Negative"), name("Object"), name("Object"));
82    sgn.add_mor_generator(name("Zero"), name("Object"), name("Object"));
83    sgn.equate(Path::pair(name("Negative"), name("Negative")), Path::empty(name("Object")));
84    sgn.equate(Path::pair(name("Negative"), name("Zero")), name("Zero").into());
85    sgn.equate(Path::pair(name("Zero"), name("Negative")), name("Zero").into());
86    sgn.equate(Path::pair(name("Zero"), name("Zero")), name("Zero").into());
87    sgn.into()
88}
89
90/// The theory of categories with scalars.
91///
92/// A *category with scalars* is a category sliced over the monoid representing a walking
93/// idempotent. The morphisms over the identity are interpreted as scalars, which are closed
94/// under composition, as are the non-scalar morphisms.
95///
96/// The main intended application is to categories
97/// enriched in `M`-sets for a monoid `M` such as the positive real numbers under multiplication,
98/// but to remain within simple theories the theory defined here is more general.
99pub fn th_category_with_scalars() -> DiscreteDblTheory {
100    let mut idem = FpCategory::new();
101    idem.add_ob_generator(name("Object"));
102    idem.add_mor_generator(name("Nonscalar"), name("Object"), name("Object"));
103    idem.equate(Path::pair(name("Nonscalar"), name("Nonscalar")), name("Nonscalar").into());
104    idem.into()
105}
106
107/// The theory of categories with links.
108///
109/// A *category with links* is a category `C` together with a profunctor from `C` to
110/// `Arr(C)`, the arrow category of C.
111///
112/// [Primitive stock and flow diagrams](crate::refs::StockFlow) are free categories
113/// with links.
114pub fn th_category_links() -> DiscreteTabTheory {
115    let mut th = DiscreteTabTheory::new();
116    th.add_ob_type(name("Object"));
117    let ob_type = TabObType::Basic(name("Object"));
118    th.add_mor_type(name("Link"), ob_type.clone(), th.tabulator(th.hom_type(ob_type)));
119    th
120}
121
122/// The theory of categories with signed links.
123///
124/// It can be useful to consider a version of stock and flow diagrams where the
125/// links are labelled with a sign: positive or negative.
126pub fn th_category_signed_links() -> DiscreteTabTheory {
127    let mut th = DiscreteTabTheory::new();
128    th.add_ob_type(name("Object"));
129    let ob_type = TabObType::Basic(name("Object"));
130    th.add_mor_type(name("Link"), ob_type.clone(), th.tabulator(th.hom_type(ob_type.clone())));
131    th.add_mor_type(
132        name("NegativeLink"),
133        ob_type.clone(),
134        th.tabulator(th.hom_type(ob_type.clone())),
135    );
136    th
137}
138
139/// The theory of strict monoidal categories.
140pub fn th_monoidal_category() -> ModalDblTheory<Unital> {
141    th_list_algebra(List::Plain)
142}
143
144/// The theory of lax monoidal categories.
145pub fn th_lax_monoidal_category() -> ModalDblTheory<Unital> {
146    th_list_lax_algebra(List::Plain)
147}
148
149/// The theory of strict symmetric monoidal categories.
150pub fn th_sym_monoidal_category() -> ModalDblTheory<Unital> {
151    th_list_algebra(List::Symmetric)
152}
153
154/// The theory of a strict algebra of a list monad.
155///
156/// This is a modal double theory, parametric over which variant of the double list
157/// monad is used.
158fn th_list_algebra(list: List) -> ModalDblTheory<Unital> {
159    let m = Modality::List(list);
160
161    let mut th = ModalDblTheory::new();
162    th.add_ob_type(name("Object"));
163    let x = ModeApp::new(name("Object"));
164    th.add_ob_op(name("tensor"), x.clone().apply(m), x.clone());
165    let a = ModeApp::new(name("tensor").into());
166
167    th.equate_ob_ops(
168        Path::pair(a.clone().apply(m), a.clone()),
169        Path::pair(ModeApp::new(ModalOp::Concat(list, 2, x.clone())), a.clone()),
170    );
171    th.equate_ob_ops(
172        Path::empty(x.clone()),
173        Path::pair(ModeApp::new(ModalOp::Concat(list, 0, x)), a),
174    );
175    th
176}
177
178/// The theory of a lax algebra over a list monad.
179fn th_list_lax_algebra(list: List) -> ModalDblTheory<Unital> {
180    let m = Modality::List(list);
181
182    let mut th = ModalDblTheory::new();
183    th.add_ob_type(name("Object"));
184    let x = ModeApp::new(name("Object"));
185    th.add_ob_op(name("tensor"), x.clone().apply(m), x.clone());
186    let a = ModeApp::new(name("tensor").into());
187
188    th.add_special_mor_op(
189        name("Associator"),
190        Path::pair(a.clone().apply(m), a.clone()),
191        Path::pair(ModeApp::new(ModalOp::Concat(list, 2, x.clone())), a.clone()),
192    );
193    th.add_special_mor_op(
194        name("Unitor"),
195        Path::empty(x.clone()),
196        Path::pair(ModeApp::new(ModalOp::Concat(list, 0, x)), a),
197    );
198    // TODO: Coherence equations
199    th
200}
201
202/// The theory of a (non-symmetric) multicategory.
203pub fn th_multicategory() -> ModalDblTheory<Unital> {
204    th_generalized_multicategory(List::Plain)
205}
206
207/// The theory of a symmetric multicategory.
208pub fn th_sym_multicategory() -> ModalDblTheory<Unital> {
209    th_generalized_multicategory(List::Symmetric)
210}
211
212/// The theory of simple polynomial ODE systems.
213pub fn th_polynomial_ode_system() -> ModalDblTheory<NonUnital> {
214    let mut th = ModalDblTheory::new();
215    th.add_ob_type(name("State"));
216    let x = ModeApp::new(name("State"));
217    th.add_mor_type(name("Contribution"), x.clone().apply(Modality::List(List::Symmetric)), x);
218    th
219}
220
221/// The theory of simple signed polynomial ODE systems.
222pub fn th_signed_polynomial_ode_system() -> ModalDblTheory<NonUnital> {
223    let mut th = ModalDblTheory::new();
224    th.add_ob_type(name("State"));
225    let x = ModeApp::new(name("State"));
226    th.add_mor_type(
227        name("Contribution"),
228        x.clone().apply(Modality::List(List::Symmetric)),
229        x.clone(),
230    );
231    th.add_mor_type(
232        name("NegativeContribution"),
233        x.clone().apply(Modality::List(List::Symmetric)),
234        x,
235    );
236    th
237}
238
239/// The theory of a generalized multicategory over a list monad.
240fn th_generalized_multicategory(list: List) -> ModalDblTheory<Unital> {
241    let mut th = ModalDblTheory::new();
242    th.add_ob_type(name("Object"));
243    let x = ModeApp::new(name("Object"));
244    th.add_mor_type(name("Multihom"), x.clone().apply(Modality::List(list)), x);
245    // TODO: Axioms, which depend on implementing composites and restrictions.
246    th
247}
248
249/// A theory of a power system.
250///
251/// Free models of this theory are models (in the colloquial sense) of a power
252/// system, such as a power grid.
253///
254/// ## Motivation
255///
256/// This theory is inspired by the ontology behind [PyPSA](https://pypsa.org/)
257/// (Python for Power System Analysis), described with admirable precision in
258/// the [Design](https://docs.pypsa.org/latest/user-guide/design/) section of
259/// the PyPSA User Guide.
260///
261/// According to PyPSA's ontology, the fundamental nodes in a power system are
262/// **buses** and the connections between nodes are **branches**. Types of
263/// branches include:
264///
265/// 1. **Passive** branches: power flow is determined passively by impedances
266///    and power imbalances
267///    - **lines** include power transmission and distribution lines
268///    - **transformers** change AC voltage levels
269/// 2. **Controllable** branches: power flow can be actively controlled by optimization
270///    - **links** encompass all controllable directed flows in PyPSA
271///
272/// These types of branches implicitly form a hierarchy, made explicit in the
273/// compositional formalization of this theory.
274///
275/// ## Formalization
276///
277/// Morphisms between buses are lines; hence a composite of lines is again a
278/// line. This makes sense as lines are the most primitive type of branch, and
279/// it is standard to approximate a physical transmission line by a series of
280/// standard line components. See, for example, (Bergen & Vittal, *Power Systems
281/// Analysis*, 2nd ed, Section 4.3) and ([Aljanaideh & Bernstein
282/// 2019](https://doi.org/10.1109/MCS.2019.2925257), p. 105).
283///
284/// Transformers generalize lines. At least, comparing PyPSA's [line
285/// model](https://docs.pypsa.org/latest/user-guide/power-flow/#line-model) and
286/// [transformer
287/// model](https://docs.pypsa.org/latest/user-guide/power-flow/#transformer-model),
288/// the analytical model of a line is seen to specialize that of a transformer
289/// (set the tap ratio to one and the phase shift to zero). Lines and
290/// transformers are the *only* types of passive branch in PyPSA's ontology.
291/// Rather than introducing a morphism type just for transformers, we introduce
292/// a morphism type for all passive branches along with a promonad structure
293/// relating lines and passive branches. Thus, every line can be cast to a
294/// passive branch, the composite of passive branches is another passive branch,
295/// and a generating passive branche is generically a transformer. Note that
296/// [sub-networks](https://docs.pypsa.org/latest/user-guide/components/sub-networks/)
297/// formed by passive branches are meaningful.
298///
299/// Controllable branches are handled by another layer of promonad structure.
300/// Thus, every passive branch can be cast to a branch, the composite of
301/// branches is another branch, and a generating branch is generically a link.
302///
303/// In summary, the compositional structure of a power system is formalized as a
304/// (free) category graded by the linear order `Line < Passive < Branch`.
305pub fn th_power_system() -> DiscreteDblTheory {
306    let mut cat = FpCategory::new();
307    cat.add_ob_generator(name("Bus"));
308    cat.add_mor_generator(name("Passive"), name("Bus"), name("Bus"));
309    cat.add_mor_generator(name("Branch"), name("Bus"), name("Bus"));
310    cat.equate(Path::pair(name("Passive"), name("Passive")), name("Passive").into());
311    cat.equate(Path::pair(name("Passive"), name("Branch")), name("Branch").into());
312    cat.equate(Path::pair(name("Branch"), name("Passive")), name("Branch").into());
313    cat.equate(Path::pair(name("Branch"), name("Branch")), name("Branch").into());
314    cat.into()
315}
316
317// Not yet using a modal theory since instantiation is currently only supported in
318// models of discrete theories.
319#[allow(dead_code)]
320fn modal_th_power_system() -> ModalDblTheory<Unital> {
321    let mut th = ModalDblTheory::new();
322
323    // Object type for buses, whose hom type is the morphism type for lines.
324    th.add_ob_type(name("Bus"));
325    let bus = ModeApp::new(name("Bus"));
326
327    // Morphism type for passive branches.
328    th.add_mor_type(name("Passive"), bus.clone(), bus.clone());
329    let passive = ModeApp::new(name("Passive"));
330    th.set_composite(passive.clone(), passive.clone(), passive.clone().into());
331    th.add_globular_mor_op(name("line_is_passive"), Path::Id(bus.clone()), passive.clone().into());
332    // TODO: Promonad cell equations
333
334    // Morphism type for generic branches.
335    th.add_mor_type(name("Branch"), bus.clone(), bus.clone());
336    let branch = ModeApp::new(name("Branch"));
337    th.set_composite(branch.clone(), passive.clone(), branch.clone().into());
338    th.set_composite(passive.clone(), branch.clone(), branch.clone().into());
339    th.set_composite(branch.clone(), branch.clone(), branch.clone().into());
340    th.add_globular_mor_op(
341        name("passive_is_branch"),
342        Path::single(passive.clone().into()),
343        branch.clone().into(),
344    );
345    // TODO: Cell equations
346
347    th
348}
349
350#[cfg(test)]
351mod tests {
352    use super::*;
353    use crate::{one::Category, validate::Validate};
354    use nonempty::nonempty;
355
356    #[test]
357    fn validate_discrete_theories() {
358        assert!(th_empty().validate().is_ok());
359        assert!(th_category().validate().is_ok());
360        assert!(th_schema().validate().is_ok());
361        assert!(th_signed_category().validate().is_ok());
362        assert!(th_delayable_signed_category().validate().is_ok());
363        assert!(th_nullable_signed_category().validate().is_ok());
364        assert!(th_category_with_scalars().validate().is_ok());
365        assert!(th_power_system().validate().is_ok());
366    }
367
368    #[test]
369    fn validate_discrete_tabulator_theories() {
370        // TODO: Implementation validation for discrete tabulator theories.
371        th_category_links();
372    }
373
374    #[test]
375    fn validate_modal_theories() {
376        assert!(th_monoidal_category().validate().is_ok());
377        assert!(th_lax_monoidal_category().validate().is_ok());
378        assert!(th_multicategory().validate().is_ok());
379        assert!(th_sym_multicategory().validate().is_ok());
380        assert!(modal_th_power_system().validate().is_ok());
381        assert!(th_polynomial_ode_system().validate().is_ok());
382    }
383
384    #[test]
385    fn delayable_signed_categories() {
386        // Check the nontrivial computer algebra in this theory.
387        let th = th_delayable_signed_category();
388        assert!(th.has_mor_type(&name("Negative").into()));
389        assert!(th.has_mor_type(&name("Slow").into()));
390        let path =
391            Path::Seq(nonempty![name("Negative"), name("Slow"), name("Negative"), name("Slow")]);
392        assert!(th.0.morphisms_are_equal(path, name("Slow").into()));
393    }
394}
catlog/stdlib/theories.rs

catlog/stdlib/
theories.rs
