catlog/dbl/discrete_tabulator/
theory.rs

1//! Discrete tabulator theories.
2
3use std::hash::{BuildHasher, BuildHasherDefault, Hash, RandomState};
4use std::ops::Range;
5
6use derivative::Derivative;
7use ref_cast::RefCast;
8use ustr::{IdentityHasher, Ustr};
9
10use crate::dbl::{category::*, graph::ProedgeGraph, tree::DblTree};
11use crate::one::{Graph, Path};
12use crate::zero::*;
13
14//use crate::zero::*;
15
16/// Object type in a discrete tabulator theory.
17#[derive(Clone, Debug, PartialEq, Eq, Hash)]
18pub enum TabObType<V, E> {
19    /// Basic or generating object type.
20    Basic(V),
21
22    /// Tabulator of a morphism type.
23    Tabulator(Box<TabMorType<V, E>>),
24}
25
26/// Morphism type in a discrete tabulator theory.
27#[derive(Clone, Debug, PartialEq, Eq, Hash)]
28pub enum TabMorType<V, E> {
29    /// Basic or generating morphism type.
30    Basic(E),
31
32    /// Hom type on an object type.
33    Hom(Box<TabObType<V, E>>),
34}
35
36/// Projection onto object type in a discrete tabulator theory.
37#[derive(Clone, Debug, PartialEq, Eq)]
38pub enum TabObProj<V, E> {
39    /// Projection from tabulator onto source of morphism type.
40    Src(TabMorType<V, E>),
41
42    /// Projection from tabulator onto target of morphism type.
43    Tgt(TabMorType<V, E>),
44}
45
46impl<V, E> TabObProj<V, E> {
47    /// Morphism type that the tabulator is of.
48    pub fn mor_type(&self) -> &TabMorType<V, E> {
49        match self {
50            TabObProj::Src(m) | TabObProj::Tgt(m) => m,
51        }
52    }
53}
54
55/// Operation on objects in a discrete tabulator theory.
56pub type TabObOp<V, E> = Path<TabObType<V, E>, TabObProj<V, E>>;
57
58/// Projection onto morphism type in a discrete tabulator theory.
59#[derive(Clone, Debug, PartialEq, Eq)]
60pub enum TabMorProj<V, E> {
61    /// Projection from a tabulator onto the original morphism type.
62    Cone(TabMorType<V, E>),
63
64    /// Projection from tabulator onto source of morphism type.
65    Src(TabMorType<V, E>),
66
67    /// Projection from tabulator onto target of morphism type.
68    Tgt(TabMorType<V, E>),
69}
70
71impl<V, E> TabMorProj<V, E> {
72    /// Morphism type that the tabulator is of.
73    pub fn mor_type(&self) -> &TabMorType<V, E> {
74        match self {
75            TabMorProj::Cone(m) | TabMorProj::Src(m) | TabMorProj::Tgt(m) => m,
76        }
77    }
78
79    /// Source projection.
80    fn src(self) -> TabObProj<V, E> {
81        match self {
82            TabMorProj::Cone(m) | TabMorProj::Src(m) => TabObProj::Src(m),
83            TabMorProj::Tgt(m) => TabObProj::Tgt(m),
84        }
85    }
86
87    /// Target projection
88    fn tgt(self) -> TabObProj<V, E> {
89        match self {
90            TabMorProj::Src(m) => TabObProj::Src(m),
91            TabMorProj::Cone(m) | TabMorProj::Tgt(m) => TabObProj::Tgt(m),
92        }
93    }
94}
95
96/// Operation on morphisms in a discrete tabulator theory.
97#[derive(Clone, Debug, PartialEq, Eq)]
98pub struct TabMorOp<V, E> {
99    dom: Path<TabObType<V, E>, TabMorType<V, E>>,
100    projections: Vec<TabMorProj<V, E>>,
101}
102
103/** A discrete tabulator theory.
104
105Loosely speaking, a discrete tabulator theory is a [discrete double
106theory](crate::dbl::theory::DiscreteDblTheory) extended to allow tabulators.
107That doesn't quite make sense as stated because a
108[tabulator](https://ncatlab.org/nlab/show/tabulator) comes with two projection
109arrows and a projection cell, which cannot exist in a nontrivial discrete double
110category. A **discrete tabulator theory** is thus a small double category with
111tabulators and with no arrows or cells beyond the identities and tabulator
112projections.
113 */
114#[derive(Clone, Derivative)]
115#[derivative(Default(bound = "S: Default"))]
116pub struct DiscreteTabTheory<V, E, S = RandomState> {
117    ob_types: HashFinSet<V, S>,
118    mor_types: HashFinSet<E, S>,
119    src: HashColumn<E, TabObType<V, E>, S>,
120    tgt: HashColumn<E, TabObType<V, E>, S>,
121    compose_map: HashColumn<(E, E), TabMorType<V, E>>,
122}
123
124/// Discrete tabulator theory with names of type `Ustr`.
125pub type UstrDiscreteTabTheory = DiscreteTabTheory<Ustr, Ustr, BuildHasherDefault<IdentityHasher>>;
126
127impl<V, E, S> DiscreteTabTheory<V, E, S>
128where
129    V: Eq + Clone + Hash,
130    E: Eq + Clone + Hash,
131    S: BuildHasher,
132{
133    /// Creates an empty discrete tabulator theory.
134    pub fn new() -> Self
135    where
136        S: Default,
137    {
138        Default::default()
139    }
140
141    /// Constructs a tabulator of a morphism type.
142    pub fn tabulator(&self, m: TabMorType<V, E>) -> TabObType<V, E> {
143        TabObType::Tabulator(Box::new(m))
144    }
145
146    /// Constructs a unary projection cell for a tabulator.
147    pub fn unary_projection(&self, proj: TabMorProj<V, E>) -> TabMorOp<V, E> {
148        TabMorOp {
149            dom: self.unit(self.tabulator(proj.mor_type().clone())).unwrap().into(),
150            projections: vec![proj],
151        }
152    }
153
154    /// Adds a generating object type to the theory.
155    pub fn add_ob_type(&mut self, v: V) -> bool {
156        self.ob_types.insert(v)
157    }
158
159    /// Adds a generating morphism type to the theory.
160    pub fn add_mor_type(&mut self, e: E, src: TabObType<V, E>, tgt: TabObType<V, E>) -> bool {
161        self.src.set(e.clone(), src);
162        self.tgt.set(e.clone(), tgt);
163        self.make_mor_type(e)
164    }
165
166    /// Adds a generating morphim type without initializing its source/target.
167    pub fn make_mor_type(&mut self, e: E) -> bool {
168        self.mor_types.insert(e)
169    }
170}
171
172/// Graph of objects and projection arrows in discrete tabulator theory.
173#[derive(RefCast)]
174#[repr(transparent)]
175struct DiscTabTheoryProjGraph<V, E, S>(DiscreteTabTheory<V, E, S>);
176
177impl<V, E, S> Graph for DiscTabTheoryProjGraph<V, E, S>
178where
179    V: Eq + Clone + Hash,
180    E: Eq + Clone + Hash,
181    S: BuildHasher,
182{
183    type V = TabObType<V, E>;
184    type E = TabObProj<V, E>;
185
186    fn has_vertex(&self, x: &Self::V) -> bool {
187        self.0.has_ob(x)
188    }
189    fn has_edge(&self, proj: &Self::E) -> bool {
190        self.0.has_proarrow(proj.mor_type())
191    }
192
193    fn src(&self, proj: &Self::E) -> Self::V {
194        TabObType::Tabulator(Box::new(proj.mor_type().clone()))
195    }
196    fn tgt(&self, proj: &Self::E) -> Self::V {
197        match proj {
198            TabObProj::Src(m) => self.0.src(m),
199            TabObProj::Tgt(m) => self.0.tgt(m),
200        }
201    }
202}
203
204impl<V, E, S> VDblCategory for DiscreteTabTheory<V, E, S>
205where
206    V: Eq + Clone + Hash,
207    E: Eq + Clone + Hash,
208    S: BuildHasher,
209{
210    type Ob = TabObType<V, E>;
211    type Arr = TabObOp<V, E>;
212    type Pro = TabMorType<V, E>;
213    type Cell = TabMorOp<V, E>;
214
215    fn has_ob(&self, ob: &Self::Ob) -> bool {
216        match ob {
217            TabObType::Basic(v) => self.ob_types.contains(v),
218            TabObType::Tabulator(m) => self.has_proarrow(m),
219        }
220    }
221    fn has_arrow(&self, path: &Self::Arr) -> bool {
222        path.contained_in(DiscTabTheoryProjGraph::ref_cast(self))
223    }
224    fn has_proarrow(&self, pro: &Self::Pro) -> bool {
225        match pro {
226            TabMorType::Basic(e) => self.mor_types.contains(e),
227            TabMorType::Hom(x) => self.has_ob(x),
228        }
229    }
230    fn has_cell(&self, cell: &Self::Cell) -> bool {
231        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
232        if !cell.dom.contained_in(graph) {
233            return false;
234        }
235        let (src, tgt) = (self.cell_src(cell), self.cell_tgt(cell));
236        self.has_arrow(&src)
237            && self.has_arrow(&tgt)
238            && cell.dom.src(graph) == self.dom(&src)
239            && cell.dom.tgt(graph) == self.dom(&tgt)
240    }
241
242    fn dom(&self, path: &Self::Arr) -> Self::Ob {
243        path.src(DiscTabTheoryProjGraph::ref_cast(self))
244    }
245    fn cod(&self, path: &Self::Arr) -> Self::Ob {
246        path.tgt(DiscTabTheoryProjGraph::ref_cast(self))
247    }
248    fn src(&self, m: &Self::Pro) -> Self::Ob {
249        match m {
250            TabMorType::Basic(e) => {
251                self.src.apply_to_ref(e).expect("Source of morphism type should be defined")
252            }
253            TabMorType::Hom(x) => (**x).clone(),
254        }
255    }
256    fn tgt(&self, m: &Self::Pro) -> Self::Ob {
257        match m {
258            TabMorType::Basic(e) => {
259                self.tgt.apply_to_ref(e).expect("Target of morphism type should be defined")
260            }
261            TabMorType::Hom(x) => (**x).clone(),
262        }
263    }
264
265    fn cell_dom(&self, cell: &Self::Cell) -> Path<Self::Ob, Self::Pro> {
266        cell.dom.clone()
267    }
268    fn cell_cod(&self, cell: &Self::Cell) -> Self::Pro {
269        self.composite(cell.dom.clone()).expect("Path should have a composite")
270    }
271    fn cell_src(&self, cell: &Self::Cell) -> Self::Arr {
272        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
273        Path::collect(cell.projections.iter().cloned().map(|proj| proj.src()))
274            .unwrap_or_else(|| Path::empty(cell.dom.src(graph)))
275    }
276    fn cell_tgt(&self, cell: &Self::Cell) -> Self::Arr {
277        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
278        Path::collect(cell.projections.iter().cloned().map(|proj| proj.tgt()))
279            .unwrap_or_else(|| Path::empty(cell.dom.tgt(graph)))
280    }
281
282    fn compose(&self, path: Path<Self::Ob, Self::Arr>) -> Self::Arr {
283        path.flatten()
284    }
285
286    fn compose_cells(&self, tree: DblTree<Self::Arr, Self::Pro, Self::Cell>) -> Self::Cell {
287        let graph = UnderlyingDblGraph::ref_cast(self);
288        let dom = tree.dom(graph);
289        let src = self.compose(tree.src(graph));
290        let tgt = self.compose(tree.tgt(graph));
291        assert_eq!(src.len(), tgt.len(), "Source/target boundaries should have equal length");
292        let projections = std::iter::zip(src, tgt)
293            .map(|pair| match pair {
294                (TabObProj::Src(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Cone(m),
295                (TabObProj::Src(m), TabObProj::Src(n)) if m == n => TabMorProj::Src(m),
296                (TabObProj::Tgt(m), TabObProj::Tgt(n)) if m == n => TabMorProj::Tgt(m),
297                _ => panic!("Projection cells should have compatible source/target boundaries"),
298            })
299            .collect();
300        TabMorOp { dom, projections }
301    }
302}
303
304impl<V, E, S> VDCWithComposites for DiscreteTabTheory<V, E, S>
305where
306    V: Eq + Clone + Hash,
307    E: Eq + Clone + Hash,
308    S: BuildHasher,
309{
310    fn composite2(&self, m: Self::Pro, n: Self::Pro) -> Option<Self::Pro> {
311        let mn = match (m, n) {
312            (m, TabMorType::Hom(y)) if self.tgt(&m) == *y => m,
313            (TabMorType::Hom(x), n) if self.src(&n) == *x => n,
314            (TabMorType::Basic(d), TabMorType::Basic(e)) => {
315                self.compose_map.apply((d, e)).expect("Composition should be defined")
316            }
317            _ => panic!("Ill-typed composite of morphism types in discrete tabulator theory"),
318        };
319        Some(mn)
320    }
321    fn unit(&self, x: Self::Ob) -> Option<Self::Pro> {
322        Some(TabMorType::Hom(Box::new(x)))
323    }
324    fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
325        Some(path.reduce(|x| self.unit(x).unwrap(), |m, n| self.composite2(m, n).unwrap()))
326    }
327
328    fn composite_ext(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Cell> {
329        Some(TabMorOp {
330            dom: path,
331            projections: vec![],
332        })
333    }
334
335    fn through_composite(&self, cell: Self::Cell, range: Range<usize>) -> Option<Self::Cell> {
336        let graph = ProedgeGraph::ref_cast(UnderlyingDblGraph::ref_cast(self));
337        let TabMorOp { dom, projections } = cell;
338        Some(TabMorOp {
339            dom: dom.replace_subpath(graph, range, |sub| self.composite(sub).unwrap().into()),
340            projections,
341        })
342    }
343}
344
345#[cfg(test)]
346mod tests {
347    use super::*;
348    use crate::dbl::theory::DblTheory;
349
350    #[test]
351    fn theory_interface() {
352        let mut th = DiscreteTabTheory::<char, char>::new();
353        th.add_ob_type('*');
354        let x = TabObType::Basic('*');
355        assert!(th.has_ob_type(&x));
356        let tab = th.tabulator(th.hom_type(x.clone()));
357        assert!(th.has_ob_type(&tab));
358        assert!(th.has_mor_type(&th.hom_type(tab.clone())));
359
360        th.add_mor_type('m', x.clone(), tab.clone());
361        let m = TabMorType::Basic('m');
362        assert!(th.has_mor_type(&m));
363        assert_eq!(th.src_type(&m), x);
364        assert_eq!(th.tgt_type(&m), tab);
365
366        let proj = th.unary_projection(TabMorProj::Cone(th.hom_type(x.clone())));
367        let cell = th.compose_cells2(
368            [th.composite2_ext(th.hom_type(tab.clone()), th.hom_type(tab.clone())).unwrap()],
369            proj.clone(),
370        );
371        assert!(th.has_mor_op(&cell));
372        assert!(matches!(th.src_op(&cell).only(), Some(TabObProj::Src(_))));
373        assert!(matches!(th.tgt_op(&cell).only(), Some(TabObProj::Tgt(_))));
374
375        let proj_src = th.unary_projection(TabMorProj::Src(th.hom_type(x.clone())));
376        let cell_alt = th.compose_cells2(
377            [proj_src, proj],
378            th.composite2_ext(th.hom_type(x.clone()), th.hom_type(x.clone())).unwrap(),
379        );
380        assert!(th.has_mor_op(&cell_alt));
381        assert_eq!(cell, cell_alt);
382    }
383}
catlog/dbl/discrete_tabulator/theory.rs

catlog/dbl/discrete_tabulator/
theory.rs
