catlog/one/
fp_category.rs

1//! Finitely presented categories.
2//!
3//! A *finitely presented category*, or *f.p. category* for short, is a [finite
4//! graph](super::graph::FinGraph) together with a finite set of [path
5//! equations](super::path::PathEq). This data defines a category whose objects are
6//! the vertices of the graph and morphisms are paths in the graphs, regarded as
7//! equivalent under the congruence relation generated by the path equations. For a
8//! detailed description of this congruence relation, see ([Spivak
9//! 2014](crate::refs::CTForTheSciences), Definition 4.5.2.3).
10//!
11//! In general, this congruence relation---the word problem for finitely presented
12//! categories---cannot be decided, though in practice it often can be. The data
13//! structure in this module uses [e-graphs](https://en.wikipedia.org/wiki/E-graph)
14//! to check for equivalence of paths under the congruence.
15
16use std::cell::RefCell;
17use std::fmt::Debug;
18use std::{collections::HashMap, hash::Hash};
19
20use derivative::Derivative;
21use egglog::ast::{Command, Expr, RunConfig, Schedule, Schema};
22use egglog::prelude::*;
23use nonempty::NonEmpty;
24use thiserror::Error;
25
26use super::{category::*, graph::*, path::*};
27use crate::egglog_util::EGraphUtils;
28use crate::validate::{self, Validate};
29use crate::zero::QualifiedName;
30
31/// A finitely presented category backed by an e-graph.
32///
33/// A data structure for a f.p. category in which the congruence relation generated
34/// by the path equations is maintained by an e-graph. The question of whether paths
35/// in the presented category are equivalent is referred to the e-graph.
36///
37/// # Interior mutability
38///
39/// Checking equivalence of paths requires mutating the underlying e-graph. However,
40/// we do not want to regard this check as mutating, for the theoretical reason that
41/// the check does not change the category presented and the practical reason that
42/// it would cause mutable references to be aggressively propagated throughout the
43/// codebase. Thus, we use the [interior
44/// mutability](https://doc.rust-lang.org/book/ch15-05-interior-mutability.html)
45/// pattern to encapsulate the mutability of the e-graph and perform borrow checking
46/// at runtime. The current implementation allows only *single-threaded* usage.
47#[derive(Clone, Derivative)]
48#[derivative(Debug(bound = "V: Debug, E: Debug"))]
49#[derivative(Default(bound = "", new = "true"))]
50#[derivative(PartialEq(bound = "V: Eq + Hash, E: Eq + Hash"))]
51#[derivative(Eq(bound = "V: Eq + Hash, E: Eq + Hash"))]
52pub struct FpCategory<V, E> {
53    generators: HashGraph<V, E>,
54    equations: Vec<PathEq<V, E>>,
55    #[derivative(Debug = "ignore", PartialEq = "ignore")]
56    state: RefCell<CategoryEGraph<V, E>>,
57}
58
59/// A finitely presented category whose generators have qualified names.
60pub type QualifiedFpCategory = FpCategory<QualifiedName, QualifiedName>;
61
62impl<V, E> FpCategory<V, E>
63where
64    V: Eq + Clone + Hash,
65    E: Eq + Clone + Hash,
66{
67    /// Gets the generating graph of the category presentation.
68    pub fn generators(&self) -> &(impl FinGraph<V = V, E = E> + use<V, E>) {
69        &self.generators
70    }
71
72    /// Gets the path equations of the category presentation.
73    pub fn equations(&self) -> impl Iterator<Item = &PathEq<V, E>> {
74        self.equations.iter()
75    }
76
77    /// Is the category freely generated?
78    pub fn is_free(&self) -> bool {
79        self.equations.is_empty()
80    }
81
82    /// Adds an object generator.
83    pub fn add_ob_generator(&mut self, v: V) {
84        assert!(self.generators.add_vertex(v.clone()), "Object generator already exists");
85        let state = self.state.get_mut();
86        let expr = state.ob_generator(v);
87        state.egraph.run_action(action!((unquote expr))).unwrap();
88    }
89
90    /// Adds several object generators at once.
91    pub fn add_ob_generators(&mut self, iter: impl IntoIterator<Item = V>) {
92        for v in iter {
93            self.add_ob_generator(v)
94        }
95    }
96
97    /// Adds a morphism generator.
98    pub fn add_mor_generator(&mut self, e: E, dom: V, cod: V) {
99        assert!(
100            self.generators.add_edge(e.clone(), dom.clone(), cod.clone()),
101            "Morphism generator already exists"
102        );
103        let state = self.state.get_mut();
104        let (dom, cod) = (state.ob_generator(dom), state.ob_generator(cod));
105        let mor = state.mor_generator(e);
106        let actions = actions![
107            (unquote mor.clone())
108            (union (unquote dom) (dom (unquote mor.clone())))
109            (union (unquote cod) (cod (unquote mor)))
110        ];
111        state.egraph.run_actions(actions).unwrap();
112    }
113
114    /// Adds a morphism generator without declaring its (co)domain.
115    pub fn make_mor_generator(&mut self, e: E) {
116        assert!(self.generators.make_edge(e.clone()), "Morphism generator already exists");
117        let state = self.state.get_mut();
118        let expr = state.mor_generator(e);
119        state.egraph.run_action(action!((unquote expr))).unwrap();
120    }
121
122    /// Gets the domain of a morphism generator.
123    pub fn get_dom(&self, e: &E) -> Option<&V> {
124        self.generators.get_src(e)
125    }
126
127    /// Gets the codomain of a morphism generator.
128    pub fn get_cod(&self, e: &E) -> Option<&V> {
129        self.generators.get_tgt(e)
130    }
131
132    /// Sets the domain of a morphism generator.
133    pub fn set_dom(&mut self, e: E, v: V) {
134        assert!(
135            self.generators.set_src(e.clone(), v.clone()).is_none(),
136            "Domain of morphism generator should not already be set"
137        );
138        let state = self.state.get_mut();
139        let (mor, ob) = (state.mor_generator(e), state.ob_generator(v));
140        let action = action!((union (unquote ob) (dom (unquote mor))));
141        state.egraph.run_action(action).unwrap();
142    }
143
144    /// Sets the codomain of a morphism generator.
145    pub fn set_cod(&mut self, e: E, v: V) {
146        assert!(
147            self.generators.set_tgt(e.clone(), v.clone()).is_none(),
148            "Codomain of morphism generator should not already be set"
149        );
150        let state = self.state.get_mut();
151        let (mor, ob) = (state.mor_generator(e), state.ob_generator(v));
152        let action = action!((union (unquote ob) (cod (unquote mor))));
153        state.egraph.run_action(action).unwrap();
154    }
155
156    /// Adds a path equation to the presentation.
157    pub fn add_equation(&mut self, eq: PathEq<V, E>) {
158        self.equations.push(eq.clone());
159        let (lhs, rhs) = (self.path_expr(eq.lhs), self.path_expr(eq.rhs));
160        let action = action!((union (unquote lhs) (unquote rhs)));
161        self.state.get_mut().egraph.run_action(action).unwrap();
162    }
163
164    /// Equates two path in the presentation.
165    pub fn equate(&mut self, lhs: Path<V, E>, rhs: Path<V, E>) {
166        self.add_equation(PathEq::new(lhs, rhs));
167    }
168
169    fn path_expr(&self, path: Path<V, E>) -> Expr {
170        path.map_reduce(
171            |v| {
172                let ob = self.state.borrow_mut().ob_generator(v);
173                expr!((id (unquote ob)))
174            },
175            |e| self.state.borrow_mut().mor_generator(e),
176            |f, g| expr!((compose (unquote f) (unquote g))),
177        )
178    }
179
180    /// Iterates over failures to be a well-defined presentation of a category.
181    pub fn iter_invalid(&self) -> impl Iterator<Item = InvalidFpCategory<E>> + '_ {
182        let generator_errors = self.generators.iter_invalid().map(|err| match err {
183            InvalidGraph::Src(e) => InvalidFpCategory::Dom(e),
184            InvalidGraph::Tgt(e) => InvalidFpCategory::Cod(e),
185        });
186        let equation_errors = self.equations.iter().enumerate().filter_map(|(i, eq)| {
187            Some(InvalidFpCategory::Eqn(i, eq.validate_in(&self.generators).err()?))
188        });
189        generator_errors.chain(equation_errors)
190    }
191}
192
193impl<V, E> Category for FpCategory<V, E>
194where
195    V: Eq + Clone + Hash,
196    E: Eq + Clone + Hash,
197{
198    type Ob = V;
199    type Mor = Path<V, E>;
200
201    fn has_ob(&self, x: &Self::Ob) -> bool {
202        self.generators.has_vertex(x)
203    }
204    fn has_mor(&self, path: &Self::Mor) -> bool {
205        path.contained_in(&self.generators)
206    }
207    fn dom(&self, path: &Self::Mor) -> Self::Ob {
208        path.src(&self.generators)
209    }
210    fn cod(&self, path: &Self::Mor) -> Self::Ob {
211        path.tgt(&self.generators)
212    }
213
214    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
215        path.flatten_in(&self.generators).expect("Paths should be composable")
216    }
217    fn compose2(&self, path1: Self::Mor, path2: Self::Mor) -> Self::Mor {
218        path1
219            .concat_in(&self.generators, path2)
220            .expect("Target of first path should equal source of second path")
221    }
222
223    fn morphisms_are_equal(&self, path1: Self::Mor, path2: Self::Mor) -> bool {
224        let (lhs, rhs) = (self.path_expr(path1), self.path_expr(path2));
225        self.state.borrow_mut().check_equal(lhs, rhs)
226    }
227}
228
229impl<V, E> FgCategory for FpCategory<V, E>
230where
231    V: Eq + Clone + Hash,
232    E: Eq + Clone + Hash,
233{
234    type ObGen = V;
235    type MorGen = E;
236
237    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
238        self.generators.vertices()
239    }
240    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
241        self.generators.edges()
242    }
243    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
244        self.generators.src(f)
245    }
246    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
247        self.generators.tgt(f)
248    }
249}
250
251impl<V, E> Validate for FpCategory<V, E>
252where
253    V: Eq + Clone + Hash,
254    E: Eq + Clone + Hash,
255{
256    type ValidationError = InvalidFpCategory<E>;
257
258    fn validate(&self) -> Result<(), NonEmpty<Self::ValidationError>> {
259        validate::wrap_errors(self.iter_invalid())
260    }
261}
262
263/// A failure of a finite presentation of a category to be well defined.
264#[derive(Debug, Error)]
265pub enum InvalidFpCategory<E> {
266    /// Morphism generator with an invalid domain.
267    #[error("Domain of morphism generator `{0}` is not in the category")]
268    Dom(E),
269
270    /// Morphism generator with an invalid codomain.
271    #[error("Codomain of morphism generator `{0}` is not in the category")]
272    Cod(E),
273
274    /// Path equation with one or more errors.
275    #[error("Path equation `{0}` is not valid: `{1:?}`")]
276    Eqn(usize, NonEmpty<InvalidPathEq>),
277}
278
279/// E-graph state for computing with categories in egglog.
280///
281/// Wraps an [`EGraph`] initialized with the theory of categories, along with
282/// mappings from vertices and edges in the category's generating graph to numeric
283/// IDs for generator terms in egglog.
284#[derive(Clone)]
285struct CategoryEGraph<V, E> {
286    egraph: EGraph,
287    ob_generators: HashMap<V, usize>,
288    mor_generators: HashMap<E, usize>,
289}
290
291impl<V, E> CategoryEGraph<V, E>
292where
293    V: Eq + Hash,
294    E: Eq + Hash,
295{
296    /// Constructs an object generator expression, assigning an ID if needed.
297    fn ob_generator(&mut self, v: V) -> Expr {
298        let n = self.ob_generators.len();
299        let id: i64 = (*self.ob_generators.entry(v).or_insert(n))
300            .try_into()
301            .expect("Shouldn't have too many object generators");
302        expr!((ObGen (unquote exprs::int(id))))
303    }
304
305    /// Constructs a morphism generator expression, assigning an ID if needed.
306    fn mor_generator(&mut self, e: E) -> Expr {
307        let n = self.mor_generators.len();
308        let id: i64 = (*self.mor_generators.entry(e).or_insert(n))
309            .try_into()
310            .expect("Shouldn't have too many morphism generators");
311        expr!((MorGen (unquote exprs::int(id))))
312    }
313}
314
315impl<V, E> CategoryEGraph<V, E> {
316    /// Checks whether two morphism expressions are equal.
317    ///
318    /// The category axioms are saturated before performing the check.
319    fn check_equal(&mut self, lhs: Expr, rhs: Expr) -> bool {
320        let schedule = Schedule::Saturate(
321            span!(),
322            Box::new(Schedule::Run(
323                span!(),
324                RunConfig { ruleset: "CatAxioms".into(), until: None },
325            )),
326        );
327        let prog = vec![
328            Command::Action(action!((unquote lhs.clone()))),
329            Command::Action(action!((unquote rhs.clone()))),
330            Command::RunSchedule(schedule),
331        ];
332        self.egraph.run_program(prog).unwrap();
333        self.egraph.check_equal(lhs, rhs).unwrap()
334    }
335}
336
337impl<V, E> Default for CategoryEGraph<V, E> {
338    fn default() -> Self {
339        let mut egraph = EGraph::default();
340        init_category_egraph(&mut egraph).expect("Unexpected egglog error");
341        Self {
342            egraph,
343            ob_generators: Default::default(),
344            mor_generators: Default::default(),
345        }
346    }
347}
348
349/// Initializes an e-graph with the theory of categories.
350fn init_category_egraph(egraph: &mut EGraph) -> Result<(), egglog::Error> {
351    // Types: objects and morphisms with generators.
352    datatype!(egraph, (datatype Ob (ObGen i64 :cost 0)));
353    datatype!(egraph, (datatype Mor (MorGen i64 :cost 0) (compose Mor Mor :cost 1)));
354
355    // Additional constructors: (co)domain and identity.
356    for name in ["dom", "cod"] {
357        add_constructor(
358            egraph,
359            name,
360            Schema {
361                input: vec!["Mor".into()],
362                output: "Ob".into(),
363            },
364            Some(1),
365            false,
366        )?;
367    }
368    add_constructor(
369        egraph,
370        "id",
371        Schema {
372            input: vec!["Ob".into()],
373            output: "Mor".into(),
374        },
375        Some(1),
376        false,
377    )?;
378
379    // Predicate: is the morphism well-typed?
380    add_relation(egraph, "is_mor_valid", vec!["Mor".into()])?;
381
382    // Rule set: all the axioms for a category.
383    add_ruleset(egraph, "CatAxioms")?;
384
385    // Rule: every morphism generator is well-typed.
386    rule(egraph, "CatAxioms", facts![(= f (MorGen name))], actions![(is_mor_valid f)])?;
387
388    // Rule: every identity morphism is well-typed.
389    rule(egraph, "CatAxioms", facts![(= f (id x))], actions![(is_mor_valid f)])?;
390
391    // Rule: a composite of two morphisms is well-typed if both
392    // morphisms are well-typed and their (co)domains are compatible.
393    rule(
394        egraph,
395        "CatAxioms",
396        facts![
397            (= fg (compose f g))
398            (is_mor_valid f)
399            (is_mor_valid g)
400            (= (cod f) (dom g))
401        ],
402        actions![(is_mor_valid fg)],
403    )?;
404
405    // Rules: (co)domains of composites and identities.
406    rule(
407        egraph,
408        "CatAxioms",
409        facts![
410            (= fg (compose f g))
411            (is_mor_valid fg)
412        ],
413        actions![
414            (union (dom fg) (dom f))
415            (union (cod fg) (cod g))
416        ],
417    )?;
418    rule(egraph, "CatAxioms", facts![(= lhs (dom (id x)))], actions![(union lhs x)])?;
419    rule(egraph, "CatAxioms", facts![(= lhs (cod (id x)))], actions![(union lhs x)])?;
420
421    // Associativity axioms (bidirectional).
422    rule(
423        egraph,
424        "CatAxioms",
425        facts![
426            (= fgh (compose (compose f g) h))
427            (is_mor_valid fgh)
428        ],
429        actions![(union fgh (compose f (compose g h)))],
430    )?;
431    rule(
432        egraph,
433        "CatAxioms",
434        facts![
435            (= fgh (compose f (compose g h)))
436            (is_mor_valid fgh)
437        ],
438        actions![(union fgh (compose (compose f g) h))],
439    )?;
440
441    // Unitality axioms.
442    rule(
443        egraph,
444        "CatAxioms",
445        facts![(= lhs (compose f (id (cod f))))],
446        actions![(union lhs f)],
447    )?;
448    rule(
449        egraph,
450        "CatAxioms",
451        facts![(= lhs (compose (id (dom f)) f))],
452        actions![(union lhs f)],
453    )?;
454
455    Ok(())
456}
457
458#[cfg(test)]
459use crate::zero::name;
460
461/// The schema for graphs, an f.p. category.
462#[cfg(test)]
463pub fn sch_graph() -> QualifiedFpCategory {
464    let mut cat = FpCategory::new();
465    cat.add_ob_generators([name("V"), name("E")]);
466    cat.add_mor_generator(name("src"), name("E"), name("V"));
467    cat.add_mor_generator(name("tgt"), name("E"), name("V"));
468    cat
469}
470
471/// The schema for symmetric graphs, an f.p. category.
472#[cfg(test)]
473pub fn sch_sgraph() -> QualifiedFpCategory {
474    let mut cat = FpCategory::new();
475    cat.add_ob_generators([name("V"), name("E")]);
476    cat.add_mor_generator(name("src"), name("E"), name("V"));
477    cat.add_mor_generator(name("tgt"), name("E"), name("V"));
478    cat.add_mor_generator(name("inv"), name("E"), name("E"));
479    cat.equate(Path::pair(name("inv"), name("inv")), Path::empty(name("E")));
480    cat.equate(Path::pair(name("inv"), name("src")), Path::single(name("tgt")));
481    cat.equate(Path::pair(name("inv"), name("tgt")), Path::single(name("src")));
482    cat
483}
484
485/// The schema for half-edge graphs, an f.p. category.
486#[cfg(test)]
487pub fn sch_hgraph() -> QualifiedFpCategory {
488    let mut cat = FpCategory::new();
489    cat.add_ob_generators([name("V"), name("H")]);
490    cat.add_mor_generator(name("vert"), name("H"), name("V"));
491    cat.add_mor_generator(name("inv"), name("H"), name("H"));
492    cat.equate(Path::pair(name("inv"), name("inv")), Path::empty(name("H")));
493    cat
494}
495
496#[cfg(test)]
497mod tests {
498    use super::*;
499    use nonempty::nonempty;
500
501    #[test]
502    fn sch_sgraph_equations() {
503        let sch = sch_sgraph();
504        assert!(!sch.is_free());
505        assert!(sch.validate().is_ok());
506
507        assert!(!sch.morphisms_are_equal(Path::single(name("src")), Path::single(name("tgt"))));
508        assert!(
509            sch.morphisms_are_equal(Path::pair(name("inv"), name("inv")), Path::empty(name("E")))
510        );
511        assert!(sch.morphisms_are_equal(
512            Path::Seq(nonempty![name("inv"), name("inv"), name("inv"), name("src")]),
513            Path::single(name("tgt"))
514        ));
515    }
516}
catlog/one/fp_category.rs

catlog/one/
fp_category.rs
