catlog/stdlib/
theories.rs

1//! Standard library of double theories.
2
3use ustr::ustr;
4
5use crate::dbl::theory::*;
6use crate::one::fin_category::{FinMor, UstrFinCategory};
7
8/** The empty theory, which has a single model, the empty model.
9
10As a double category, this is the initial double category.
11 */
12pub fn th_empty() -> UstrDiscreteDblTheory {
13    let cat: UstrFinCategory = Default::default();
14    DiscreteDblTheory::from(cat)
15}
16
17/** The theory of categories, aka the trivial double theory.
18
19As a double category, this is the terminal double category.
20 */
21pub fn th_category() -> UstrDiscreteDblTheory {
22    let mut cat: UstrFinCategory = Default::default();
23    cat.add_ob_generator(ustr("Object"));
24    DiscreteDblTheory::from(cat)
25}
26
27/** The theory of database schemas with attributes.
28
29As a double category, this is the "walking proarrow".
30 */
31pub fn th_schema() -> UstrDiscreteDblTheory {
32    let mut cat: UstrFinCategory = Default::default();
33    let (x, y, p) = (ustr("Entity"), ustr("AttrType"), ustr("Attr"));
34    cat.add_ob_generator(x);
35    cat.add_ob_generator(y);
36    cat.add_mor_generator(p, x, y);
37    DiscreteDblTheory::from(cat)
38}
39
40/** The theory of signed categories.
41
42A *signed category* is a category sliced over the group of (nonzero) signs. Free
43signed categories are signed graphs, a simple mathematical model of [regulatory
44networks](crate::refs::RegNets) and causal loop diagrams.
45 */
46pub fn th_signed_category() -> UstrDiscreteDblTheory {
47    let mut sgn: UstrFinCategory = Default::default();
48    let (x, n) = (ustr("Object"), ustr("Negative"));
49    sgn.add_ob_generator(x);
50    sgn.add_mor_generator(n, x, x);
51    sgn.set_composite(n, n, FinMor::Id(x));
52    DiscreteDblTheory::from(sgn)
53}
54
55/** The theory of delayable signed categories.
56
57Free delayable signed categories are causal loop diagrams with delays, often
58depicted as [caesuras](https://en.wikipedia.org/wiki/Caesura).
59 */
60pub fn th_delayable_signed_category() -> UstrDiscreteDblTheory {
61    let mut cat: UstrFinCategory = Default::default();
62    let (x, neg) = (ustr("Object"), ustr("Negative"));
63    let (pos_slow, neg_slow) = (ustr("PositiveSlow"), ustr("NegativeSlow"));
64    cat.add_ob_generator(x);
65    cat.add_mor_generator(neg, x, x);
66    cat.add_mor_generator(pos_slow, x, x);
67    cat.add_mor_generator(neg_slow, x, x);
68    cat.set_composite(neg, neg, FinMor::Id(x));
69    cat.set_composite(neg, pos_slow, FinMor::Generator(neg_slow));
70    cat.set_composite(neg, neg_slow, FinMor::Generator(pos_slow));
71    cat.set_composite(pos_slow, neg, FinMor::Generator(neg_slow));
72    cat.set_composite(neg_slow, neg, FinMor::Generator(pos_slow));
73    cat.set_composite(pos_slow, pos_slow, FinMor::Generator(pos_slow));
74    cat.set_composite(neg_slow, neg_slow, FinMor::Generator(pos_slow));
75    cat.set_composite(neg_slow, pos_slow, FinMor::Generator(neg_slow));
76    cat.set_composite(pos_slow, neg_slow, FinMor::Generator(neg_slow));
77    DiscreteDblTheory::from(cat)
78}
79
80/** The theory of nullable signed categories.
81
82A *nullable signed category* is a category sliced over the monoid of signs,
83including zero.
84 */
85pub fn th_nullable_signed_category() -> UstrDiscreteDblTheory {
86    let mut sgn: UstrFinCategory = Default::default();
87    let (x, n, z) = (ustr("Object"), ustr("Negative"), ustr("Zero"));
88    sgn.add_ob_generator(x);
89    sgn.add_mor_generator(n, x, x);
90    sgn.add_mor_generator(z, x, x);
91    sgn.set_composite(n, n, FinMor::Id(x));
92    sgn.set_composite(z, z, FinMor::Generator(z));
93    sgn.set_composite(n, z, FinMor::Generator(z));
94    sgn.set_composite(z, n, FinMor::Generator(z));
95    DiscreteDblTheory::from(sgn)
96}
97
98/** The theory of categories with scalars.
99
100A *category with scalars* is a category sliced over the monoid representing a walking
101idempotent. The morphisms over the identity are interpreted as scalars, which are closed
102under composition, as are the non-scalar morphisms.
103
104The main intended application is to categories
105enriched in `M`-sets for a monoid `M` such as the positive real numbers under multiplication,
106but to remain within simple theories the theory defined here is more general.
107 */
108pub fn th_category_with_scalars() -> UstrDiscreteDblTheory {
109    let mut idem: UstrFinCategory = Default::default();
110    let (x, s) = (ustr("Object"), ustr("Nonscalar"));
111    idem.add_ob_generator(x);
112    idem.add_mor_generator(s, x, x);
113    idem.set_composite(s, s, FinMor::Generator(s));
114    DiscreteDblTheory::from(idem)
115}
116
117/** The theory of categories with links.
118
119A *category with links* is a category `C` together with a profunctor from `C` to
120`Arr(C)`, the arrow category of C.
121
122[Primitive stock and flow diagrams](crate::refs::StockFlow) are free categories
123with links.
124 */
125pub fn th_category_links() -> UstrDiscreteTabTheory {
126    let mut th: UstrDiscreteTabTheory = Default::default();
127    let x = ustr("Object");
128    th.add_ob_type(x);
129    th.add_mor_type(
130        ustr("Link"),
131        TabObType::Basic(x),
132        th.tabulator(th.hom_type(TabObType::Basic(x))),
133    );
134    th
135}
136
137#[cfg(test)]
138mod tests {
139    use super::*;
140    use crate::validate::Validate;
141
142    #[test]
143    fn theories() {
144        assert!(th_empty().validate().is_ok());
145        assert!(th_category().validate().is_ok());
146        assert!(th_schema().validate().is_ok());
147        assert!(th_signed_category().validate().is_ok());
148        assert!(th_delayable_signed_category().validate().is_ok());
149        assert!(th_nullable_signed_category().validate().is_ok());
150        assert!(th_category_with_scalars().validate().is_ok());
151        // TODO: Validate discrete tabulator theories.
152        th_category_links();
153    }
154}
catlog/stdlib/theories.rs

catlog/stdlib/
theories.rs
