catlog/dbl/modal/
model.rs

1//! Models of modal double theories.
2
3use std::fmt::Debug;
4use std::hash::{BuildHasher, Hash, RandomState};
5use std::rc::Rc;
6
7use derive_more::From;
8use itertools::Itertools;
9use ref_cast::RefCast;
10
11use super::theory::*;
12use crate::dbl::VDblGraph;
13use crate::dbl::model::{DblModel, FgDblModel, MutDblModel};
14use crate::one::computad::*;
15use crate::{one::*, zero::*};
16
17/// Object in a model of a modal double theory.
18#[derive(Clone, Debug, PartialEq, Eq, From)]
19pub enum ModalOb<Id, ThId> {
20    /// Generating object.
21    #[from]
22    Generator(Id),
23
24    /// Application of a generating object operation.
25    App(Box<Self>, ThId),
26
27    /// List of objects in a [list modality](List).
28    List(List, Vec<Self>),
29}
30
31/// Morphism is a model of a modal double theory.
32#[derive(Clone, Debug, PartialEq, Eq, From)]
33pub enum ModalMor<Id, ThId> {
34    /// Generating morphism.
35    #[from]
36    Generator(Id),
37
38    /// Composite of morphisms.
39    Composite(Box<Path<ModalOb<Id, ThId>, Self>>),
40
41    /// Application of a basic morphism operation.
42    App(Box<Path<ModalOb<Id, ThId>, Self>>, ThId),
43
44    /// Application of the hom operation on a basic object operation.
45    HomApp(Box<Path<ModalOb<Id, ThId>, Self>>, ThId),
46
47    /// List of morphisms.
48    List(MorListData, Vec<Self>),
49}
50
51/// Extra data associated with a list of morphisms in a [list modality](List).
52#[derive(Clone, Debug, PartialEq, Eq)]
53pub enum MorListData {
54    /// No extra data for a morphism in the [plain list](List::Plain) modality.
55    Plain(),
56
57    /** Data for a morphism in the [symmetric list](List::Symmetric) modality.
58
59    A permutation on the indexing set of the list, which acts on the list of
60    codomain objects.
61     */
62    Symmetric(SkelColumn),
63}
64
65impl MorListData {
66    fn list_type(&self) -> List {
67        match self {
68            MorListData::Plain() => List::Plain,
69            MorListData::Symmetric(..) => List::Symmetric,
70        }
71    }
72}
73
74/// A model of a modal double theory.
75#[derive(Clone)]
76pub struct ModalDblModel<Id, ThId, S = RandomState> {
77    theory: Rc<ModalDblTheory<ThId, S>>,
78    ob_generators: HashFinSet<Id>,
79    mor_generators: ComputadTop<ModalOb<Id, ThId>, Id>,
80    // TODO: Equations
81    ob_types: HashColumn<Id, ModalObType<ThId>>,
82    mor_types: HashColumn<Id, ModalMorType<ThId>>,
83}
84
85impl<Id, ThId, S> ModalDblModel<Id, ThId, S> {
86    /// Creates an empty model of the given theory.
87    pub fn new(theory: Rc<ModalDblTheory<ThId, S>>) -> Self {
88        Self {
89            theory,
90            ob_generators: Default::default(),
91            mor_generators: Default::default(),
92            ob_types: Default::default(),
93            mor_types: Default::default(),
94        }
95    }
96
97    /// Gets the computing generating the morphisms of the model.
98    fn computad(&self) -> Computad<'_, ModalOb<Id, ThId>, ModalDblModelObs<Id, ThId, S>, Id> {
99        Computad::new(ModalDblModelObs::ref_cast(self), &self.mor_generators)
100    }
101}
102
103#[derive(RefCast)]
104#[repr(transparent)]
105struct ModalDblModelObs<Id, ThId, S>(ModalDblModel<Id, ThId, S>);
106
107impl<Id, ThId, S> Set for ModalDblModelObs<Id, ThId, S>
108where
109    Id: Eq + Clone + Hash + Debug,
110    ThId: Eq + Clone + Hash + Debug,
111    S: BuildHasher,
112{
113    type Elem = ModalOb<Id, ThId>;
114
115    fn contains(&self, ob: &Self::Elem) -> bool {
116        match ob {
117            ModalOb::Generator(id) => self.0.ob_generators.contains(id),
118            ModalOb::App(x, op_id) => {
119                self.contains(x) && self.0.ob_type(x) == self.0.theory.tight_computad().src(op_id)
120            }
121            ModalOb::List(_, xs) => xs.iter().all(|x| self.contains(x)),
122        }
123    }
124}
125
126impl<Id, ThId, S> Category for ModalDblModel<Id, ThId, S>
127where
128    Id: Eq + Clone + Hash + Debug,
129    ThId: Eq + Clone + Hash + Debug,
130    S: BuildHasher,
131{
132    type Ob = ModalOb<Id, ThId>;
133    type Mor = ModalMor<Id, ThId>;
134
135    fn has_ob(&self, ob: &Self::Ob) -> bool {
136        ModalDblModelObs::ref_cast(self).contains(ob)
137    }
138    fn has_mor(&self, mor: &Self::Mor) -> bool {
139        let graph = UnderlyingGraph::ref_cast(self);
140        match mor {
141            ModalMor::Generator(id) => self.computad().has_edge(id),
142            ModalMor::Composite(path) => path.contained_in(graph),
143            // TODO: Check morphism type equals domain of operation.
144            ModalMor::App(path, _) | ModalMor::HomApp(path, _) => path.contained_in(graph),
145            ModalMor::List(MorListData::Plain(), fs) => fs.iter().all(|f| self.has_mor(f)),
146            ModalMor::List(MorListData::Symmetric(sigma), fs) => {
147                sigma.is_permutation(fs.len()) && fs.iter().all(|f| self.has_mor(f))
148            }
149        }
150    }
151
152    fn dom(&self, mor: &Self::Mor) -> Self::Ob {
153        let graph = UnderlyingGraph::ref_cast(self);
154        match mor {
155            ModalMor::Generator(id) => self.computad().src(id),
156            ModalMor::Composite(path) => path.src(graph),
157            ModalMor::App(path, op_id) => {
158                self.ob_act(path.src(graph), &self.theory.dbl_computad().square_src(op_id))
159            }
160            ModalMor::HomApp(path, op_id) => {
161                ModalOp::from(op_id.clone()).ob_act(path.src(graph)).unwrap()
162            }
163            ModalMor::List(data, fs) => {
164                ModalOb::List(data.list_type(), fs.iter().map(|f| self.dom(f)).collect())
165            }
166        }
167    }
168
169    fn cod(&self, mor: &Self::Mor) -> Self::Ob {
170        let graph = UnderlyingGraph::ref_cast(self);
171        match mor {
172            ModalMor::Generator(id) => self.computad().tgt(id),
173            ModalMor::Composite(path) => path.tgt(graph),
174            ModalMor::App(path, op_id) => {
175                self.ob_act(path.tgt(graph), &self.theory.dbl_computad().square_tgt(op_id))
176            }
177            ModalMor::HomApp(path, op_id) => {
178                ModalOp::from(op_id.clone()).ob_act(path.tgt(graph)).unwrap()
179            }
180            ModalMor::List(MorListData::Plain(), fs) => {
181                ModalOb::List(List::Plain, fs.iter().map(|f| self.cod(f)).collect())
182            }
183            ModalMor::List(MorListData::Symmetric(sigma), fs) => {
184                ModalOb::List(List::Symmetric, sigma.values().map(|j| self.cod(&fs[*j])).collect())
185            }
186        }
187    }
188
189    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
190        // TODO: Normalize composites of lists by composing elementwise.
191        ModalMor::Composite(path.into())
192    }
193}
194
195impl<Id, ThId, S> FgCategory for ModalDblModel<Id, ThId, S>
196where
197    Id: Eq + Clone + Hash + Debug,
198    ThId: Eq + Clone + Hash + Debug,
199    S: BuildHasher,
200{
201    type ObGen = Id;
202    type MorGen = Id;
203
204    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
205        self.ob_generators.iter()
206    }
207    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
208        self.mor_generators.edge_set.iter()
209    }
210    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
211        self.computad().src(f)
212    }
213    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
214        self.computad().tgt(f)
215    }
216}
217
218impl<Id, ThId, S> DblModel for ModalDblModel<Id, ThId, S>
219where
220    Id: Eq + Clone + Hash + Debug,
221    ThId: Eq + Clone + Hash + Debug,
222    S: BuildHasher,
223{
224    type ObType = ModalObType<ThId>;
225    type MorType = ModalMorType<ThId>;
226    type ObOp = ModalObOp<ThId>;
227    type MorOp = ModalMorOp<ThId>;
228    type Theory = ModalDblTheory<ThId, S>;
229
230    fn theory(&self) -> &Self::Theory {
231        &self.theory
232    }
233
234    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
235        match ob {
236            ModalOb::Generator(id) => self.ob_generator_type(id),
237            ModalOb::App(_, op_id) => self.theory.tight_computad().tgt(op_id),
238            ModalOb::List(list_type, vec) => vec
239                .iter()
240                .map(|ob| self.ob_type(ob))
241                .all_equal_value()
242                .expect("All objects in list should have the same type")
243                .apply((*list_type).into()),
244        }
245    }
246
247    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
248        match mor {
249            ModalMor::Generator(id) => self.mor_generator_type(id),
250            ModalMor::Composite(_) => panic!("Composites not implemented"),
251            ModalMor::App(_, op_id) => self.theory.dbl_computad().square_cod(op_id),
252            ModalMor::HomApp(_, op_id) => ShortPath::Zero(self.theory.tight_computad().tgt(op_id)),
253            ModalMor::List(data, fs) => fs
254                .iter()
255                .map(|mor| self.mor_type(mor))
256                .all_equal_value()
257                .expect("All morphisms in list should have the same type")
258                .apply(data.list_type().into()),
259        }
260    }
261
262    fn ob_act(&self, ob: Self::Ob, path: &Self::ObOp) -> Self::Ob {
263        path.iter().cloned().fold(ob, |ob, op| op.ob_act(ob).unwrap())
264    }
265
266    fn mor_act(&self, path: Path<Self::Ob, Self::Mor>, tree: &Self::MorOp) -> Self::Mor {
267        let (Some(mor), Some(node)) = (path.only(), tree.clone().only()) else {
268            panic!("Morphism action only implemented for basic operations");
269        };
270        match node {
271            ModalNode::Basic(op) => op.mor_act(mor, false).unwrap(),
272            ModalNode::Unit(op) => op.mor_act(mor, true).unwrap(),
273            ModalNode::Composite(_) => mor,
274        }
275    }
276}
277
278impl<Id, ThId, S> FgDblModel for ModalDblModel<Id, ThId, S>
279where
280    Id: Eq + Clone + Hash + Debug,
281    ThId: Eq + Clone + Hash + Debug,
282    S: BuildHasher,
283{
284    fn ob_generator_type(&self, id: &Self::ObGen) -> Self::ObType {
285        self.ob_types.apply_to_ref(id).expect("Object should have object type")
286    }
287    fn mor_generator_type(&self, id: &Self::MorGen) -> Self::MorType {
288        self.mor_types.apply_to_ref(id).expect("Morphism should have morphism type")
289    }
290    fn ob_generators_with_type(&self, typ: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
291        self.ob_types.preimage(typ)
292    }
293    fn mor_generators_with_type(&self, typ: &Self::MorType) -> impl Iterator<Item = Self::MorGen> {
294        self.mor_types.preimage(typ)
295    }
296}
297
298impl<Id, ThId, S> MutDblModel for ModalDblModel<Id, ThId, S>
299where
300    Id: Eq + Clone + Hash + Debug,
301    ThId: Eq + Clone + Hash + Debug,
302    S: BuildHasher,
303{
304    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) {
305        self.ob_types.set(x.clone(), ob_type);
306        self.ob_generators.insert(x);
307    }
308    fn add_mor(&mut self, f: Self::MorGen, dom: Self::Ob, cod: Self::Ob, mor_type: Self::MorType) {
309        self.mor_types.set(f.clone(), mor_type);
310        self.mor_generators.add_edge(f, dom, cod);
311    }
312    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) {
313        self.mor_types.set(f.clone(), mor_type);
314        self.mor_generators.edge_set.insert(f);
315    }
316
317    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
318        self.mor_generators.src_map.get(f)
319    }
320    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
321        self.mor_generators.tgt_map.get(f)
322    }
323    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) {
324        self.mor_generators.tgt_map.set(f, x);
325    }
326    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) {
327        self.mor_generators.tgt_map.set(f, x);
328    }
329}
330
331impl<ThId> ModeApp<ModalOp<ThId>>
332where
333    ThId: Clone,
334{
335    fn ob_act<Id>(mut self, ob: ModalOb<Id, ThId>) -> Result<ModalOb<Id, ThId>, String> {
336        match self.modalities.pop() {
337            Some(Modality::List(list_type)) => {
338                if let ModalOb::List(other_type, vec) = ob
339                    && other_type == list_type
340                {
341                    let maybe_vec: Result<Vec<_>, _> =
342                        vec.into_iter().map(|ob| self.clone().ob_act(ob)).collect();
343                    Ok(ModalOb::List(list_type, maybe_vec?))
344                } else {
345                    Err(format!("Object should be a list of type {list_type:?}"))
346                }
347            }
348            Some(Modality::Discrete()) | Some(Modality::Codiscrete()) | None => self.arg.ob_act(ob),
349        }
350    }
351
352    fn mor_act<Id>(
353        mut self,
354        mor: ModalMor<Id, ThId>,
355        is_unit: bool,
356    ) -> Result<ModalMor<Id, ThId>, String> {
357        match self.modalities.pop() {
358            Some(Modality::List(list_type)) => {
359                if let ModalMor::List(data, vec) = mor
360                    && data.list_type() == list_type
361                {
362                    let maybe_vec: Result<Vec<_>, _> =
363                        vec.into_iter().map(|mor| self.clone().mor_act(mor, is_unit)).collect();
364                    Ok(ModalMor::List(data, maybe_vec?))
365                } else {
366                    Err(format!("Morphism should be a list of type {list_type:?}"))
367                }
368            }
369            Some(modality) => panic!("Modality {modality:?} is not implemented"),
370            None => self.arg.mor_act(mor, is_unit),
371        }
372    }
373}
374
375impl<ThId> ModalOp<ThId> {
376    fn ob_act<Id>(self, ob: ModalOb<Id, ThId>) -> Result<ModalOb<Id, ThId>, String> {
377        match self {
378            ModalOp::Generator(id) => Ok(ModalOb::App(Box::new(ob), id)),
379            ModalOp::Concat(list_type, n, _) => {
380                Ok(ModalOb::List(list_type, flatten_ob_list(ob, list_type, n)?))
381            }
382        }
383    }
384
385    fn mor_act<Id>(
386        self,
387        mor: ModalMor<Id, ThId>,
388        is_unit: bool,
389    ) -> Result<ModalMor<Id, ThId>, String> {
390        match self {
391            ModalOp::Generator(id) => Ok(if is_unit {
392                ModalMor::HomApp(Box::new(mor.into()), id)
393            } else {
394                ModalMor::App(Box::new(mor.into()), id)
395            }),
396            ModalOp::Concat(list_type, n, _) => match list_type {
397                List::Plain => Ok(ModalMor::List(MorListData::Plain(), flatten_mor_list(mor, n)?)),
398                _ => panic!("Flattening of functions is not implemented"),
399            },
400        }
401    }
402}
403
404/// Recursively flatten a nested list of objects of the given depth.
405fn flatten_ob_list<Id, ThId>(
406    ob: ModalOb<Id, ThId>,
407    list_type: List,
408    depth: usize,
409) -> Result<Vec<ModalOb<Id, ThId>>, String> {
410    if depth == 0 {
411        Ok(vec![ob])
412    } else if let ModalOb::List(other_type, vec) = ob
413        && other_type == list_type
414    {
415        if depth == 1 {
416            Ok(vec)
417        } else {
418            let maybe_vec: Result<Vec<_>, _> =
419                vec.into_iter().map(|ob| flatten_ob_list(ob, list_type, depth - 1)).collect();
420            Ok(maybe_vec?.into_iter().flatten().collect())
421        }
422    } else {
423        Err(format!("Object should be a list of type {list_type:?}"))
424    }
425}
426
427/// Recursively flatten a nested list of morphisms of the given depth.
428fn flatten_mor_list<Id, ThId>(
429    mor: ModalMor<Id, ThId>,
430    depth: usize,
431) -> Result<Vec<ModalMor<Id, ThId>>, String> {
432    if depth == 0 {
433        Ok(vec![mor])
434    } else if let ModalMor::List(MorListData::Plain(), vec) = mor {
435        if depth == 1 {
436            Ok(vec)
437        } else {
438            let maybe_vec: Result<Vec<_>, _> =
439                vec.into_iter().map(|mor| flatten_mor_list(mor, depth - 1)).collect();
440            Ok(maybe_vec?.into_iter().flatten().collect())
441        }
442    } else {
443        Err(format!("Morphism should be a list of type {:?}", List::Plain))
444    }
445}
446
447#[cfg(test)]
448mod tests {
449    use super::*;
450    use crate::dbl::theory::DblTheory;
451    use crate::stdlib::theories::*;
452    use crate::{dbl::tree::DblNode, one::tree::OpenTree};
453    use ustr::ustr;
454
455    #[test]
456    fn monoidal_category() {
457        let th = Rc::new(th_monoidal_category());
458        let ob_type = ModeApp::new(ustr("Object"));
459
460        // Lists of objects.
461        let mut model = ModalDblModel::new(th.clone());
462        let (w, x, y, z) = (ustr("w"), ustr("x"), ustr("y"), ustr("z"));
463        model.add_ob(x, ob_type.clone());
464        model.add_ob(y, ob_type.clone());
465        assert!(model.has_ob(&x.into()));
466        let pair = ModalOb::List(List::Plain, vec![x.into(), y.into()]);
467        assert!(model.has_ob(&pair));
468        assert!(!model.has_ob(&ModalOb::List(List::Plain, vec![x.into(), z.into()])));
469
470        // Nested lists of objects.
471        model.add_ob(w, ob_type.clone());
472        model.add_ob(z, ob_type.clone());
473        let pairs = ModalOb::List(
474            List::Plain,
475            vec![
476                ModalOb::List(List::Plain, vec![w.into(), x.into()]),
477                ModalOb::List(List::Plain, vec![y.into(), z.into()]),
478            ],
479        );
480        assert!(model.has_ob(&pairs));
481        assert_eq!(
482            model.ob_act(pairs, &ModalObOp::concat(List::Plain, 2, ob_type.clone())),
483            ModalOb::List(List::Plain, vec![w.into(), x.into(), y.into(), z.into()])
484        );
485        assert_eq!(
486            model.ob_act(x.into(), &ModalObOp::concat(List::Plain, 0, ob_type.clone())),
487            ModalOb::List(List::Plain, vec![x.into()])
488        );
489
490        // Products of objects.
491        assert_eq!(model.ob_type(&pair), ob_type.clone().apply(List::Plain.into()));
492        let mul_op = ModalObOp::generator(ustr("Mul"));
493        let prod = model.ob_act(pair, &mul_op);
494        assert!(model.has_ob(&prod));
495        assert_eq!(model.ob_type(&prod), ob_type);
496
497        // Lists of morphisms.
498        let (f, g) = (ustr("f"), ustr("g"));
499        model.add_mor(f, x.into(), y.into(), th.hom_type(ob_type.clone()));
500        model.add_mor(g, w.into(), z.into(), th.hom_type(ob_type.clone()));
501        assert!(model.has_mor(&f.into()));
502        let pair = ModalMor::List(MorListData::Plain(), vec![f.into(), g.into()]);
503        assert!(model.has_mor(&pair));
504        assert_eq!(model.mor_type(&pair), th.hom_type(ob_type.clone().apply(List::Plain.into())));
505        let dom_list = ModalOb::List(List::Plain, vec![x.into(), w.into()]);
506        let cod_list = ModalOb::List(List::Plain, vec![y.into(), z.into()]);
507        assert_eq!(model.dom(&pair), dom_list);
508        assert_eq!(model.cod(&pair), cod_list);
509
510        // Products of morphisms.
511        let ob_op = ModeApp::new(ustr("Mul").into());
512        let hom_op = OpenTree::single(DblNode::Cell(ModalNode::Unit(ob_op)), 1).into();
513        let prod = model.mor_act(pair.into(), &hom_op);
514        assert!(model.has_mor(&prod));
515        assert_eq!(model.mor_type(&prod), th.hom_type(ob_type.clone()));
516        assert_eq!(model.dom(&prod), model.ob_act(dom_list, &mul_op));
517        assert_eq!(model.cod(&prod), model.ob_act(cod_list, &mul_op));
518    }
519
520    #[test]
521    fn sym_monoidal_category() {
522        let th = Rc::new(th_sym_monoidal_category());
523        let ob_type = ModeApp::new(ustr("Object"));
524
525        // Lists of morphisms, with permutation.
526        let mut model = ModalDblModel::new(th.clone());
527        let (w, x, y, z, f, g) = (ustr("w"), ustr("x"), ustr("y"), ustr("z"), ustr("f"), ustr("g"));
528        for id in [w, x, y, z] {
529            model.add_ob(id, ob_type.clone());
530        }
531        model.add_mor(f, x.into(), y.into(), th.hom_type(ob_type.clone()));
532        model.add_mor(g, w.into(), z.into(), th.hom_type(ob_type.clone()));
533        let pair = ModalMor::List(
534            MorListData::Symmetric(SkelColumn::new(vec![1, 0])),
535            vec![f.into(), g.into()],
536        );
537        assert!(model.has_mor(&pair));
538        assert_eq!(model.dom(&pair), ModalOb::List(List::Symmetric, vec![x.into(), w.into()]));
539        assert_eq!(model.cod(&pair), ModalOb::List(List::Symmetric, vec![z.into(), y.into()]));
540        // Bad permutation.
541        let pair = ModalMor::List(
542            MorListData::Symmetric(SkelColumn::new(vec![0, 0])),
543            vec![f.into(), g.into()],
544        );
545        assert!(!model.has_mor(&pair));
546    }
547}
catlog/dbl/modal/model.rs

catlog/dbl/modal/
model.rs
