#diagram #testing #algebra #proofs #commutative

commuter

Provides tooling to test diagrams for commutativity, allowing automated tests on algebraic systems

6 releases

0.1.8 Jan 16, 2023
0.1.7 Jan 13, 2023

#409 in Math

MIT license

28KB
579 lines

Commuter

A tool for testing commutative diagrams

As an example, the following tests associativity on a given (subset of) the integers:


 use itertools::Itertools;
 use commuter::diagram::{Diagram, Set, Map, diagram_commutes, CommutativeDiagramResult};

 let generating_integers: Vec<i32> = (0..20).collect();

 let left_add = |(a, b, c): &(i32, i32, i32)| (a + b, *c);
 let right_add = |(a, b, c): &(i32, i32, i32)| (*a, b + c);

 // Build the sets (triplets, pairs, integers) so that summing operations can be well-defined later
 let triplets: Vec<(i32, i32, i32)> = (generating_integers)
     .clone()
     .iter()
     .cartesian_product(generating_integers.clone())
     .cartesian_product(generating_integers.clone().iter())
     .map(|((a, b), c)| (*a, b, *c))
     .collect();

 // Construct the diagram
 let diagram = Diagram::new(
     vec[
         Set::new(triplets), // This set gets some generating elements, on which the diagram will be tested
         Set::<(i32, i32)>::new_no_generating_set(), // We only test on pairs that are generated by the given maps from the triplets, so no explicit elements are added here
         Set::new(vec[(5, 3), (100, 100)]), // We can also insert some additional generating elements into an intermediate set
         Set::<i32>::new_no_generating_set(),
     ],
     vec[
         Map::new(0, 1, left_add, "(+,id)"),
         Map::new(0, 2, right_add, "(id,+)"),
         Map::new(2, 3, |(a, b): &(i32, i32)| a + b, "(+)"),
         Map::new(1, 3, |(a, b): &(i32, i32)| a + b, "(+)"),
     ],
 );

 assert!(match diagram_commutes(&diagram).unwrap() {
     CommutativeDiagramResult::Commutes => true,
     CommutativeDiagramResult::DoesNotCommute(reason) => panic("{}", reason),
 });

Dependencies

~2MB
~42K SLoC